1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
#include <string.h>
#include <stdlib.h>
#include <stdio.h>
#include <assert.h>
#include "../qdpll.h"
int main (int argc, char** argv)
{
/* The header file 'qdpll.h' has some comments regarding the usage of the
API. */
/* Please see also the file 'basic-manual-selectors.c'. */
/* Create solver instance. */
QDPLL *depqbf = qdpll_create ();
/* Use the linear ordering of the quantifier prefix. */
qdpll_configure (depqbf, "--dep-man=simple");
/* Enable incremental solving. */
qdpll_configure (depqbf, "--incremental-use");
/* Add and open a new leftmost universal block at nesting level 1. */
qdpll_new_scope_at_nesting (depqbf, QDPLL_QTYPE_FORALL, 1);
/* Add a fresh variable with 'id == 1' to the open block. */
qdpll_add (depqbf, 1);
/* Close open scope. */
qdpll_add (depqbf, 0);
/* Add a new existential block at nesting level 2. */
qdpll_new_scope_at_nesting (depqbf, QDPLL_QTYPE_EXISTS, 2);
/* Add a fresh variable with 'id == 2' to the existential block. */
qdpll_add (depqbf, 2);
/* Close open scope. */
qdpll_add (depqbf, 0);
/* Add clause: 1 -2 0 */
qdpll_add (depqbf, 1);
qdpll_add (depqbf, -2);
qdpll_add (depqbf, 0);
/* Add clause: -1 2 0 */
qdpll_add (depqbf, -1);
qdpll_add (depqbf, 2);
qdpll_add (depqbf, 0);
/* At this point, the formula looks as follows:
p cnf 2 3
a 1 0
e 2 0
1 -2 0
-1 2 0 */
/* Print formula. */
qdpll_print (depqbf, stdout);
QDPLLResult res = qdpll_sat (depqbf);
/* Expecting that the formula is satisfiable. */
assert (res == QDPLL_RESULT_SAT);
/* res == 10 means satisfiable, res == 20 means unsatisfiable. */
printf ("result is: %d\n", res);
/* Must reset the solver before adding further clauses or variables. */
qdpll_reset (depqbf);
/* Open a new frame of clauses. Clauses added after the 'push' can be
removed later by calling 'pop'. */
qdpll_push (depqbf);
/* Add clause: 1 2 0 */
qdpll_add (depqbf, 1);
qdpll_add (depqbf, 2);
qdpll_add (depqbf, 0);
printf ("added clause '1 2 0' to a new stack frame.\n", res);
/* At this point, the formula looks as follows:
p cnf 2 3
a 1 0
e 2 0
1 -2 0
-1 2 0
1 2 0 */
qdpll_print (depqbf, stdout);
res = qdpll_sat (depqbf);
/* Expecting that the formula is unsatisfiable due to the most recently
added clause. */
assert (res == QDPLL_RESULT_UNSAT);
printf ("result is: %d\n", res);
/* Print partial countermodel as a value of the leftmost universal variable. */
QDPLLAssignment a = qdpll_get_value (depqbf, 1);
printf ("partial countermodel - value of 1: %s\n", a == QDPLL_ASSIGNMENT_UNDEF ? "undef" :
(a == QDPLL_ASSIGNMENT_FALSE ? "false" : "true"));
qdpll_reset (depqbf);
/* Discard the clause '1 2 0' by popping off the topmost frame. */
qdpll_pop (depqbf);
printf ("discarding clause '1 2 0' by a 'pop'.\n", res);
/* At this point, the formula looks as follows:
p cnf 2 3
a 1 0
e 2 0
1 -2 0
-1 2 0 */
qdpll_print (depqbf, stdout);
res = qdpll_sat (depqbf);
/* The formula is satisfiable again because we discarded the clause '1 2 0'
by a 'pop'. */
assert (res == QDPLL_RESULT_SAT);
printf ("result after pop is: %d\n", res);
/* Delete solver instance. */
qdpll_delete (depqbf);
}
|
