cprover
example.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: A minimalistic BDD library, following Bryant's original paper
4
and Andersen's lecture notes
5
6
Author: Daniel Kroening, kroening@kroening.com
7
8
\*******************************************************************/
9
13
14
#include "
miniBDD.h
"
15
16
#include <iostream>
17
18
int
main
()
19
{
20
miniBDD::mgr mgr;
21
miniBDD::BDD result;
22
23
#if 0
24
{
25
auto
x=mgr.Var(
"x"
);
26
auto
y=mgr.Var(
"y"
);
27
auto
z=mgr.Var(
"z"
);
28
result=x | (y &z);
29
}
30
#elif 0
31
{
32
auto
y=mgr.Var(
"y"
);
33
auto
x=mgr.Var(
"x"
);
34
auto
z=mgr.Var(
"z"
);
35
result=x | (y &z);
36
}
37
#elif 0
38
{
39
auto
x1=mgr.Var(
"x_1"
);
40
auto
x2=mgr.Var(
"x_2"
);
41
auto
x3=mgr.Var(
"x_3"
);
42
auto
x4=mgr.Var(
"x_4"
);
43
result=(x1&x2)|(x3&x4);
44
}
45
#elif 0
46
{
47
auto
x1=mgr.Var(
"x_1"
);
48
auto
x2=mgr.Var(
"x_2"
);
49
auto
x3=mgr.Var(
"x_3"
);
50
auto
x4=mgr.Var(
"x_4"
);
51
auto
tmp=(x1&x2)|(x3&x4);
52
result=
restrict
(tmp, x2.var(), 0);
53
}
54
#else
55
{
56
auto
a=mgr.Var(
"a"
);
57
auto
b=mgr.Var(
"b"
);
58
auto
f=!a|b;
59
auto
fp=!b;
60
result=f==fp;
61
}
62
#endif
63
64
mgr.DumpTikZ(std::cout);
65
}
main
int main()
Definition:
example.cpp:18
miniBDD.h
Small BDD implementation.
restrict
mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
Definition:
miniBDD.cpp:557
solvers
miniBDD
example.cpp
Generated by
1.8.16