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
|
#include "test.h"
static void test_dump (void) {
printf ("First generating and solving simple CNF:\n\n");
kissat *solver = kissat_init ();
kissat_add (solver, 1);
kissat_add (solver, -2);
kissat_add (solver, 0);
kissat_add (solver, -1);
kissat_add (solver, 2);
kissat_add (solver, 0);
kissat_add (solver, 1);
kissat_add (solver, 2);
kissat_add (solver, 3);
kissat_add (solver, 0);
kissat_add (solver, 1);
kissat_add (solver, 2);
kissat_add (solver, -3);
kissat_add (solver, 0);
int res = kissat_solve (solver);
assert (res == 10);
int a = kissat_value (solver, 1);
int b = kissat_value (solver, 2);
assert (a > 0);
assert (b > 0);
#ifndef NDEBUG
void kissat_dump (kissat *);
printf ("\nCompletely dumping solver:\n\n");
kissat_dump (solver);
printf ("\nDumping also vectors:\n\n");
void kissat_dump_vectors (kissat *);
kissat_dump_vectors (solver);
#endif
kissat_release (solver);
}
void tissat_schedule_dump (void) { SCHEDULE_FUNCTION (test_dump); }
|
