/usr/share/doc/depqbf/examples/basic-api-example3.c is in depqbf 5.0-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 124 125 126 127 128 129 130 131 132 133 134 135 136 | #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);
qdpll_add (depqbf, 99);
/* Close open scope. */
qdpll_add (depqbf, 0);
assert(qdpll_is_var_declared (depqbf, 1));
assert(qdpll_is_var_declared (depqbf, 99));
assert(!qdpll_is_var_declared (depqbf, 50));
assert(!qdpll_is_var_declared (depqbf, 51));
assert(!qdpll_is_var_declared (depqbf, 52));
/* 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);
/* Var 99 still is declared although no clauses were added containing literals of 99 before. */
assert(qdpll_is_var_declared (depqbf, 1));
assert(qdpll_is_var_declared (depqbf, 99));
assert(!qdpll_is_var_declared (depqbf, 50));
assert(!qdpll_is_var_declared (depqbf, 51));
assert(!qdpll_is_var_declared (depqbf, 52));
/* 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");
/* 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");
/* At this point, the formula looks as follows:
p cnf 2 3
a 1 0
e 2 0
1 -2 0
-1 2 0 */
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);
}
|