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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
#ifndef _tracer_hpp_INCLUDED
#define _tracer_hpp_INCLUDED
#include <cstdint>
#include <vector>
namespace CaDiCaL {
struct Internal;
enum ConclusionType { CONFLICT = 1, ASSUMPTIONS = 2, CONSTRAINT = 4 };
// Proof tracer class to observer all possible proof events,
// such as added or deleted clauses.
// An implementation can decide on which events to act.
//
class Tracer {
public:
Tracer () {}
virtual ~Tracer () {}
/*------------------------------------------------------------------------*/
/* */
/* Basic Events */
/* */
/*------------------------------------------------------------------------*/
// Notify the tracer that a original clause has been added.
// Includes ID and whether the clause is redundant or irredundant
// Arguments: ID, redundant, clause, restored
//
virtual void add_original_clause (int64_t, bool, const std::vector<int> &,
bool = false) {}
// Notify the observer that a new clause has been derived.
// Includes ID and whether the clause is redundant or irredundant
// If antecedents are derived they will be included here.
// If witness != 0 it is a RAT clause.
// Arguments: ID, redundant, clause, witness, antecedents
//
virtual void add_derived_clause (int64_t, bool, int,
const std::vector<int> &,
const std::vector<int64_t> &) {}
// Notify the observer that a clause is deleted.
// Includes ID and redundant/irredundant
// Arguments: ID, redundant, clause
//
virtual void delete_clause (int64_t, bool, const std::vector<int> &) {}
// Notify the observer that a clause is deleted.
// Includes ID and redundant/irredundant
// Arguments: ID, redundant, clause
//
virtual void demote_clause (uint64_t, const std::vector<int> &) {}
// Notify the observer to remember that the clause might be restored later
// Arguments: ID, clause
//
virtual void weaken_minus (int64_t, const std::vector<int> &) {}
// Notify the observer that a clause is strengthened
// Arguments: ID
//
virtual void strengthen (int64_t) {}
// Notify the observer that the solve call ends with status StatusType
// If the status is UNSAT and an empty clause has been derived, the second
// argument will contain its id.
// Note that the empty clause is already added through add_derived_clause
// and finalized with finalize_clause
// Arguments: int, ID
//
virtual void report_status (int, int64_t) {}
/*------------------------------------------------------------------------*/
/* */
/* Specifically non-incremental */
/* */
/*------------------------------------------------------------------------*/
// Notify the observer that a clause is finalized.
// Arguments: ID, clause
//
virtual void finalize_clause (int64_t, const std::vector<int> &) {}
// Notify the observer that the proof begins with a set of reserved ids
// for original clauses. Given ID is the first derived clause ID.
// Arguments: ID
//
virtual void begin_proof (int64_t) {}
/*------------------------------------------------------------------------*/
/* */
/* Specifically incremental */
/* */
/*------------------------------------------------------------------------*/
// Notify the observer that an assumption has been added
// Arguments: assumption_literal
//
virtual void solve_query () {}
// Notify the observer that an assumption has been added
// Arguments: assumption_literal
//
virtual void add_assumption (int) {}
// Notify the observer that a constraint has been added
// Arguments: constraint_clause
//
virtual void add_constraint (const std::vector<int> &) {}
// Notify the observer that assumptions and constraints are reset
//
virtual void reset_assumptions () {}
// Notify the observer that this clause could be derived, which
// is the negation of a core of failing assumptions/constraints.
// If antecedents are derived they will be included here.
// Arguments: ID, clause, antecedents
//
virtual void add_assumption_clause (int64_t, const std::vector<int> &,
const std::vector<int64_t> &) {}
// Notify the observer that conclude unsat was requested.
// will give either the id of the empty clause, the id of a failing
// assumption clause or the ids of the failing constrain clauses
// Arguments: conclusion_type, clause_ids
//
virtual void conclude_unsat (ConclusionType,
const std::vector<int64_t> &) {}
// Notify the observer that conclude sat was requested.
// will give the complete model as a vector.
//
virtual void conclude_sat (const std::vector<int> &) {}
// Notify the observer that conclude unknown was requested.
// will give the current trail as a vector.
//
virtual void conclude_unknown (const std::vector<int> &) {}
// Notify the observer that two literals are equivalent
//
// You receive literals, not variables. You can also get notified
// multiple times. You can also get notified of BVA variables, aka
// variables you did not declare.
virtual void notify_equivalence (int, int) {}
};
/*--------------------------------------------------------------------------*/
// Following tracers for internal use.
struct InternalTracer : public Tracer {
public:
InternalTracer () {}
virtual ~InternalTracer () {}
virtual void connect_internal (Internal *) {}
};
class StatTracer : public InternalTracer {
public:
StatTracer () {}
virtual ~StatTracer () {}
virtual void print_stats () {}
};
class FileTracer : public InternalTracer {
public:
FileTracer () {}
virtual ~FileTracer () {}
virtual bool closed () = 0;
virtual void close (bool print = false) = 0;
virtual void flush (bool print = false) = 0;
};
} // namespace CaDiCaL
#endif