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
|
#include "../../src/cadical.hpp"
#ifdef NDEBUG
#undef NDEBUG
#endif
#include <cassert>
#include <cstdlib>
#include <string>
extern "C" {
#include <sys/types.h>
#include <unistd.h>
}
using namespace CaDiCaL;
using namespace std;
#include "../../src/checker.hpp"
#include "../../src/file.hpp"
#include "../../src/frattracer.hpp"
#include "../../src/lratchecker.hpp"
#include "../../src/lrattracer.hpp"
#include "../../src/testing.hpp"
#include "../../src/tracer.hpp"
#define LOG(...) \
do { \
} while (0)
// This is the example from the header file
int main () {
Solver *solver = new Solver;
Internal *internal = Testing (solver).internal ();
char lrat_proof_path[128];
char frat_proof_path[128];
char veripb_proof_path[128];
const char *prefix = "/tmp/cadical-api-test-example-tracer";
size_t pid = (size_t) getpid ();
snprintf (lrat_proof_path, 128, "%s-%zu-lrat.proof", prefix, pid);
snprintf (frat_proof_path, 128, "%s-%zu-frat.proof", prefix, pid);
snprintf (veripb_proof_path, 128, "%s-%zu-veripb.proof", prefix, pid);
File *f1 = File::write (internal, lrat_proof_path);
File *f2 = File::write (internal, frat_proof_path);
InternalTracer *t1 = new LratChecker (internal);
InternalTracer *t2 = new Checker (internal);
FileTracer *ft1 = new LratTracer (internal, f1, 0);
FileTracer *ft2 = new FratTracer (internal, f2, 0, 0);
StatTracer *st1 = new LratChecker (internal);
StatTracer *st2 = new Checker (internal);
// ------------------------------------------------------------------
solver->connect_proof_tracer (t1, 1);
solver->connect_proof_tracer (t2, 0);
solver->connect_proof_tracer (ft1, 1);
solver->set ("veripb", 4);
solver->trace_proof (veripb_proof_path);
solver->connect_proof_tracer (ft2, 0, 1);
solver->connect_proof_tracer (st1, 1);
solver->connect_proof_tracer (st2, 0);
solver->add (1);
solver->add (2);
solver->add (0);
solver->add (-1);
solver->add (-2);
solver->add (0);
solver->add (1);
solver->add (-2);
solver->add (0);
solver->constrain (-1);
solver->constrain (2);
solver->constrain (0);
solver->solve ();
solver->failed (1);
solver->conclude ();
solver->add (-1);
solver->add (2);
solver->add (0);
solver->solve ();
solver->conclude ();
// tracers that are not disconnected are deleted when deleting solver
//
solver->disconnect_proof_tracer (t1);
solver->disconnect_proof_tracer (ft1);
solver->disconnect_proof_tracer (st1);
// ------------------------------------------------------------------
delete t1;
delete ft1;
delete st1;
delete solver;
unlink (lrat_proof_path);
unlink (frat_proof_path);
unlink (veripb_proof_path);
return 0;
}
|
