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
|
#include "../../contrib/craigtracer.hpp"
#include "../../src/cadical.hpp"
#ifdef NDEBUG
#undef NDEBUG
#endif
#include <cassert>
#include <vector>
int main () {
CaDiCaL::Solver *solver = new CaDiCaL::Solver ();
CaDiCraig::CraigTracer *tracer = new CaDiCraig::CraigTracer ();
solver->connect_proof_tracer (tracer, true);
tracer->set_craig_construction (CaDiCraig::CraigConstruction::ASYMMETRIC);
tracer->label_variable (1, CaDiCraig::CraigVarType::A_LOCAL);
tracer->label_variable (2, CaDiCraig::CraigVarType::B_LOCAL);
tracer->label_variable (3, CaDiCraig::CraigVarType::GLOBAL);
tracer->label_clause (1, CaDiCraig::CraigClauseType::A_CLAUSE);
tracer->label_clause (2, CaDiCraig::CraigClauseType::B_CLAUSE);
solver->add (1);
solver->add (0);
solver->add (2);
solver->add (0);
// ------------------------------------------------
// A side is UNSATISFIABLE => Craig interpolant is CONSTANT0
solver->assume (-1);
assert (solver->solve () == CaDiCaL::Status::UNSATISFIABLE);
int next_var = 2;
std::vector<std::vector<int>> clauses;
CaDiCraig::CraigCnfType result = tracer->create_craig_interpolant (
CaDiCraig::CraigInterpolant::ASYMMETRIC, clauses, next_var);
assert (result == CaDiCraig::CraigCnfType::CONSTANT0);
assert (clauses == std::vector<std::vector<int>>{{}});
assert (next_var == 2);
// ------------------------------------------------
// B side is UNSATISFIABLE
solver->assume (-2);
assert (solver->solve () == CaDiCaL::Status::UNSATISFIABLE);
result = tracer->create_craig_interpolant (
CaDiCraig::CraigInterpolant::ASYMMETRIC, clauses, next_var);
assert (result == CaDiCraig::CraigCnfType::CONSTANT1);
assert (clauses == std::vector<std::vector<int>>{});
assert (next_var == 2);
// ------------------------------------------------
tracer->label_clause (3, CaDiCraig::CraigClauseType::A_CLAUSE);
tracer->label_constraint (CaDiCraig::CraigClauseType::B_CLAUSE);
solver->add (-1);
solver->add (3);
solver->add (0);
solver->constrain (-2);
solver->constrain (-3);
solver->constrain (0);
assert (solver->solve () == CaDiCaL::Status::UNSATISFIABLE);
result = tracer->create_craig_interpolant (
CaDiCraig::CraigInterpolant::ASYMMETRIC, clauses, next_var);
assert (result == CaDiCraig::CraigCnfType::NORMAL);
assert (clauses == std::vector<std::vector<int>>{{3}});
assert (next_var == 2);
solver->disconnect_proof_tracer (tracer);
delete tracer;
delete solver;
return 0;
}
|
