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
#include "../../src/cadical.hpp"
#ifdef NDEBUG
#undef NDEBUG
#endif
#include <cassert>

// This is the example from the header file

int main () {

 CaDiCaL::Solver * solver = new CaDiCaL::Solver;

 // ------------------------------------------------------------------
 // Encode Problem and check without assumptions.

 enum { TIE = 1, SHIRT = 2 };

 solver->add (-TIE), solver->add (SHIRT),  solver->add (0);
 solver->add (TIE),  solver->add (SHIRT),  solver->add (0);
 solver->add (-TIE), solver->add (-SHIRT), solver->add (0);

 int res = solver->solve ();    // Solve instance.
 assert (res == 10);            // Check it is 'SATISFIABLE'.

 res = solver->val (TIE);       // Obtain assignment of 'TIE'.
 assert (res < 0);              // Check 'TIE' assigned to 'false'.

 res = solver->val (SHIRT);     // Obtain assignment of 'SHIRT'.
 assert (res > 0);              // Check 'SHIRT' assigned to 'true'.

 // ------------------------------------------------------------------
 // Incrementally solve again under one assumption.

 solver->assume (TIE);          // Now force 'TIE' to true.

 res = solver->solve ();        // Solve again incrementally.
 assert (res == 20);            // Check it is 'UNSATISFIABLE'.

 res = solver->failed (TIE);    // Check 'TIE' responsible.
 assert (res);                  // Yes, 'TIE' in core.

 res = solver->failed (SHIRT);  // Check 'SHIRT' responsible.
 assert (!res);                 // No, 'SHIRT' not in core.

 // ------------------------------------------------------------------
 // Incrementally solve with constraint.

 solver->constrain (TIE), solver->constrain (-SHIRT), solver->constrain (0);

 res = solver->solve ();        // Solve again incrementally.
 assert (res == 20);            // Check it is 'UNSATISFIABLE'.

 res =
  solver->failed_constraint (); // Check constraint responsible.
 assert (res);                  // Yes, constraint was used.

 // ------------------------------------------------------------------
 // Incrementally solve once more under another assumption.

 solver->assume (-SHIRT);       // Now force 'SHIRT' to false.

 res = solver->solve ();        // Solve again incrementally.
 assert (res == 20);            // Check it is 'UNSATISFIABLE'.

 res = solver->failed (TIE);    // Check 'TIE' responsible.
 assert (!res);                 // No, 'TIE' not in core.

 res = solver->failed (-SHIRT); // Check '!SHIRT' responsible.
 assert (res);                  // Yes, '!SHIRT' in core.

 // ------------------------------------------------------------------


 delete solver;

 return 0;
}