CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
sat_api.h
Go to the documentation of this file.
1
///////////////////////////////////////////////////////////////////////////////
2
// //
3
// File: sat_api.h //
4
// Author: Clark Barrett //
5
// Created: Tue Oct 22 11:30:54 2002 //
6
// Description: Generic enhanced SAT API //
7
// //
8
///////////////////////////////////////////////////////////////////////////////
9
10
#ifndef _SAT_API_H_
11
#define _SAT_API_H_
12
13
#include <vector>
14
#include <iostream>
15
16
///////////////////////////////////////////////////////////////////////////////
17
// //
18
// Class: SAT //
19
// Author: Clark Barrett //
20
// Created: Tue Oct 22 12:02:53 2002 //
21
// Description: API for generic SAT solver with enhanced interface features. //
22
// //
23
///////////////////////////////////////////////////////////////////////////////
24
class
SatSolver
{
25
public
:
26
typedef
enum
SATStatus
{
27
UNKNOWN
,
28
UNSATISFIABLE
,
29
SATISFIABLE
,
30
BUDGET_EXCEEDED
,
31
OUT_OF_MEMORY
32
}
SATStatus
;
33
34
// Constructor and Destructor
35
SatSolver
() {}
36
virtual
~SatSolver
() {}
37
38
// Implementation must provide this function
39
static
SatSolver
*
Create
();
40
41
/////////////////////////////////////////////////////////////////////////////
42
// Variables, Literals, and Clauses //
43
/////////////////////////////////////////////////////////////////////////////
44
45
// Variables, literals and clauses are all simple union classes. This makes
46
// it easy to use integers or pointers to some more complex data structure
47
// for the implementation while at the same time increasing safety by
48
// imposing strict type requirements on users of the API.
49
// The value -1 is reserved to represent an empty or NULL value
50
51
union
Var
{
52
long
id
;
53
void
*
vptr
;
54
Var
() :
id
(-1) {}
55
bool
IsNull
() {
return
id
== -1; }
56
void
Reset
() {
id
= -1; }
57
};
58
59
union
Lit
{
60
long
id
;
61
void
*
vptr
;
62
Lit
() :
id
(-1) {}
63
bool
IsNull
() {
return
id
== -1; }
64
void
Reset
() {
id
= -1; }
65
};
66
67
union
Clause
{
68
long
id
;
69
void
*
vptr
;
70
Clause
() :
id
(-1) {}
71
bool
IsNull
() {
return
id
== -1; }
72
void
Reset
() {
id
= -1; }
73
};
74
75
// Return total number of variables
76
virtual
int
NumVariables
()=0;
77
78
// Returns the first of nvar new variables.
79
virtual
Var
AddVariables
(
int
nvars)=0;
80
81
// Return a new variable
82
Var
AddVariable
() {
return
AddVariables
(1); }
83
84
// Get the varIndexth variable. varIndex must be between 1 and
85
// NumVariables() inclusive.
86
virtual
Var
GetVar
(
int
varIndex)=0;
87
88
// Return the index (between 1 and NumVariables()) of v.
89
virtual
int
GetVarIndex
(
Var
v)=0;
90
91
// Get the first variable. Returns a NULL Var if there are no variables.
92
virtual
Var
GetFirstVar
()=0;
93
94
// Get the next variable after var. Returns a NULL Var if var is the last
95
// variable.
96
virtual
Var
GetNextVar
(
Var
var)=0;
97
98
// Return a literal made from the given var and phase (0 is positive phase, 1
99
// is negative phase).
100
virtual
Lit
MakeLit
(
Var
var,
int
phase)=0;
101
102
// Get var from literal.
103
virtual
Var
GetVarFromLit
(Lit lit)=0;
104
105
// Get phase from literal ID.
106
virtual
int
GetPhaseFromLit
(Lit lit)=0;
107
108
// Return total number of clauses
109
virtual
int
NumClauses
()=0;
110
111
// Add a new clause. Lits is a vector of literal ID's. Note that this
112
// function can be called at any time, even after the search for solution has
113
// started. A clause ID is returned which can be used to refer to this
114
// clause in the future.
115
virtual
Clause
AddClause
(std::vector<Lit>& lits)=0;
116
117
// Delete a clause. This can only be done if the clause has unassigned
118
// literals and it must delete not only the clause in question, but
119
// any learned clauses which depend on it. Since this may be difficult to
120
// implement, implementing this function is not currently required.
121
// DeleteClause returns true if the clause was successfully deleted, and
122
// false otherwise.
123
virtual
bool
DeleteClause
(
Clause
clause) {
return
false
; }
124
125
// Get the clauseIndexth clause. clauseIndex must be between 0 and
126
// NumClauses()-1 inclusive.
127
virtual
Clause
GetClause
(
int
clauseIndex)=0;
128
129
// Get the first clause. Returns a NULL Clause if there are no clauses.
130
virtual
Clause
GetFirstClause
()=0;
131
132
// Get the next clause after clause. Returns a NULL Clause if clause is
133
// the last clause.
134
virtual
Clause
GetNextClause
(Clause clause)=0;
135
136
// Returns in lits the literals that make up clause. lits is assumed to be
137
// empty when the function is called.
138
virtual
void
GetClauseLits
(Clause clause, std::vector<Lit>* lits)=0;
139
140
141
/////////////////////////////////////////////////////////////////////////////
142
// Checking Satisfiability and Retrieving Solutions //
143
/////////////////////////////////////////////////////////////////////////////
144
145
146
// Main check for satisfiability. The parameter allowNewClauses tells the
147
// solver whether to expect additional clauses to be added by the API during
148
// the search for a solution. The default is that no new clauses will be
149
// added. If new clauses can be added, then certain optimizations such as
150
// the pure literal rule must be disabled.
151
virtual
SATStatus
Satisfiable
(
bool
allowNewClauses=
false
)=0;
152
153
// Get current value of variable. -1=unassigned, 0=false, 1=true
154
virtual
int
GetVarAssignment
(
Var
var)=0;
155
156
// After Satisfiable has returned with a SATISFIABLE result, this function
157
// may be called to search for the next satisfying assignment. If one is
158
// found then SATISFIABLE is returned. If there are no more satisfying
159
// assignments then UNSATISFIABLE is returned.
160
virtual
SATStatus
Continue
()=0;
161
162
// Pop all decision levels and remove all assignments, but do not delete any
163
// clauses
164
virtual
void
Restart
()=0;
165
166
// Pop all decision levels, remove all assignments, and delete all clauses.
167
virtual
void
Reset
()=0;
168
169
170
/////////////////////////////////////////////////////////////////////////////
171
// Advanced Features //
172
/////////////////////////////////////////////////////////////////////////////
173
174
175
// The following four methods allow callback functions to be registered.
176
// Each function that is registered may optionally provide a cookie (void *)
177
// which will be passed back to that function whenever it is called.
178
179
// Register a function f which is called every time the decision level
180
// increases or decreases (i.e. every time the stack is pushed or popped).
181
// The argument to f is the change in decision level. For example, +1 is a
182
// Push, -1 is a Pop.
183
virtual
void
RegisterDLevelHook
(
void
(*f)(
void
*,
int
),
void
*cookie)=0;
184
185
// Register a function to replace the built-in decision heuristics. Every
186
// time a new decision needs to be made, the solver will call this function.
187
// The function should return a literal which should be set to true. If the
188
// bool pointer is returned with the value false, then a literal was
189
// successfully chosen. If the value is true, this signals the solver to
190
// exit with a satisfiable result. If the bool value is false and the
191
// literal is NULL, then this signals the solver to use its own internal
192
// method for making the next decision.
193
virtual
void
RegisterDecisionHook
(Lit (*f)(
void
*,
bool
*),
void
*cookie)=0;
194
195
// Register a function which is called every time the value of a variable is
196
// changed (i.e. assigned or unassigned). The first parameter is the
197
// variable ID which has changed. The second is the new value: -1=unassigned,
198
// 0=false, 1=true
199
virtual
void
RegisterAssignmentHook
(
void
(*f)(
void
*,
Var
,
int
),
200
void
*cookie)=0;
201
202
// Register a function which will be called after Boolean propagation and
203
// before making a new decision. Note that the hook function may add new
204
// clauses and this should be handled correctly.
205
virtual
void
RegisterDeductionHook
(
void
(*f)(
void
*),
void
*cookie)=0;
206
207
208
/////////////////////////////////////////////////////////////////////////////
209
// Setting Parameters //
210
/////////////////////////////////////////////////////////////////////////////
211
212
213
// Implementations are not required to implement any of these
214
// parameter-adjusting routines. Each function will return true if the request
215
// is successful and false otherwise.
216
217
// Implementation will define budget. An example budget would be time.
218
virtual
bool
SetBudget
(
int
budget) {
return
false
; }
219
220
// Set memory limit in bytes.
221
virtual
bool
SetMemLimit
(
int
mem_limit) {
return
false
; }
222
223
// Set parameters controlling randomness. Implementation defines what this
224
// means.
225
virtual
bool
SetRandomness
(
int
n) {
return
false
; }
226
virtual
bool
SetRandSeed
(
int
seed) {
return
false
; }
227
228
// Enable or disable deletion of conflict clauses to help control memory.
229
virtual
bool
EnableClauseDeletion
() {
return
false
; }
230
virtual
bool
DisableClauseDeletion
() {
return
false
; }
231
232
233
///////////////////////////////////////////////////////////////////////////////
234
// Statistics //
235
///////////////////////////////////////////////////////////////////////////////
236
237
238
// As with the parameter functions, the statistics-gathering functions may or
239
// may not be implemented. They return -1 if not implemented, and the
240
// correct value otherwise.
241
242
// Return the amount of the budget (set by SetBudget) which has been used
243
virtual
int
GetBudgetUsed
() {
return
-1; }
244
245
// Return the amount of memory in use
246
virtual
int
GetMemUsed
() {
return
-1; }
247
248
// Return the number of decisions made so far
249
virtual
int
GetNumDecisions
() {
return
-1; }
250
251
// Return the number of conflicts (equal to the number of backtracks)
252
virtual
int
GetNumConflicts
() {
return
-1; }
253
254
// Return the number of conflicts generated by the registered external
255
// conflict generator
256
virtual
int
GetNumExtConflicts
() {
return
-1; }
257
258
// Return the elapsed CPU time (in seconds) since the call to Satisfiable()
259
virtual
float
GetTotalTime
() {
return
-1; }
260
261
// Return the CPU time spent (in seconds) inside the SAT solver
262
// (as opposed to in the registered hook functions)
263
virtual
float
GetSATTime
() {
return
-1; }
264
265
// Return the total number of literals in all clauses
266
virtual
int
GetNumLiterals
() {
return
-1; }
267
268
// Return the number of clauses that were deleted
269
virtual
int
GetNumDeletedClauses
() {
return
-1; }
270
271
// Return the total number of literals in all deleted clauses
272
virtual
int
GetNumDeletedLiterals
() {
return
-1; }
273
274
// Return the number of unit propagations
275
virtual
int
GetNumImplications
() {
return
-1; }
276
277
// Return the maximum decision level reached
278
virtual
int
GetMaxDLevel
() {
return
-1; }
279
280
// Print all implemented statistics
281
void
PrintStatistics
(std::ostream & os = std::cout);
282
283
};
284
285
#endif
Generated on Tue May 14 2013 14:44:52 for CVC3 by
1.8.3.1