CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
dpllt.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file dpllt.h
4
*\brief Generic DPLL(T) module
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Mon Dec 12 16:28:08 2005
9
*/
10
/*****************************************************************************/
11
12
#ifndef _cvc3__include__dpllt_h_
13
#define _cvc3__include__dpllt_h_
14
15
#include "
queryresult.h
"
16
#include "
cnf.h
"
17
#include "
cnf_manager.h
"
18
#include "
proof.h
"
19
#include "
theory_core.h
"
20
21
namespace
SAT {
22
23
class
DPLLT
{
24
public
:
25
26
enum
ConsistentResult
{
INCONSISTENT
,
MAYBE_CONSISTENT
,
CONSISTENT
};
27
28
class
TheoryAPI
{
29
public
:
30
TheoryAPI
() {}
31
virtual
~TheoryAPI
() {}
32
33
//! Set a checkpoint for backtracking
34
virtual
void
push
() = 0;
35
//! Restore most recent checkpoint
36
virtual
void
pop
() = 0;
37
38
//! Notify theory when a literal is set to true
39
virtual
void
assertLit
(
Lit
l) = 0;
40
41
//! Check consistency of the current assignment.
42
/*! The result is either INCONSISTENT, MAYBE_CONSISTENT, or CONSISTENT
43
* Most of the time, fullEffort should be false, and the result will most
44
* likely be either INCONSISTENT or MAYBE_CONSISTENT. To force a full
45
* check, set fullEffort to true. When fullEffort is set to true, the
46
* only way the result can be MAYBE_CONSISTENT is if there are new clauses
47
* to get (via getNewClauses).
48
* \param cnf should be empty initially. If INCONSISTENT is returned,
49
* then cnf will contain one or more clauses ruling out the current
50
* assignment when it returns. Otherwise, cnf is unchanged.
51
* \param fullEffort true for a full check, false for a fast check
52
*/
53
virtual
ConsistentResult
checkConsistent
(
CNF_Formula
& cnf,
bool
fullEffort) = 0;
54
55
56
//! Check if the work budget has been exceeded
57
/*! If true, it means that the engine should quit and return ABORT.
58
* Otherwise, it should proceed normally. This should be checked regularly.
59
*/
60
virtual
bool
outOfResources
() = 0;
61
62
//! Get a literal that is implied by the current assignment.
63
/*! This is theory propagation. It can be called repeatedly and returns a
64
* Null literal when there are no more literals to propagate. It should
65
* only be called when the assignment is not known to be inconsistent.
66
*/
67
virtual
Lit
getImplication
() = 0;
68
69
//! Get an explanation for a literal that was implied
70
/*! Given a literal l that is true in the current assignment as a result of
71
* an earlier call to getImplication(), this method returns a set of clauses which
72
* justifies the propagation of that literal. The clauses will contain the
73
* literal l as well as other literals that are in the current assignment.
74
* The clauses are such that they would have propagated l via unit
75
* propagation at the time getImplication() was called.
76
* \param l the literal
77
* \param c should be empty initially. */
78
virtual
void
getExplanation
(
Lit
l,
CNF_Formula
& c) = 0;
79
80
//! Get new clauses from the theory.
81
/*! This is extended theory learning. Returns false if there are no new
82
* clauses to get. Otherwise, returns true and new clauses are added to
83
* cnf. Note that the new clauses (if any) are theory lemmas, i.e. clauses
84
* that are valid in the theory and not dependent on the current
85
* assignment. The clauses may contain new literals as well as literals
86
* that are true in the current assignment.
87
* \param cnf should be empty initially. */
88
virtual
bool
getNewClauses
(
CNF_Formula
& cnf) = 0;
89
90
};
91
92
class
Decider
{
93
public
:
94
Decider
() {}
95
virtual
~Decider
() {}
96
97
//! Make a decision.
98
/* Returns a NULL Lit if there are no more decisions to make */
99
virtual
Lit
makeDecision
() = 0;
100
101
};
102
103
protected
:
104
TheoryAPI
*
d_theoryAPI
;
105
Decider
*
d_decider
;
106
107
public
:
108
//! Constructor
109
/*! The client constructing DPLLT must provide an implementation of
110
* TheoryAPI. It may also optionally provide an implementation of Decider.
111
* If decider is NULL, then the DPLLT class must make its own decisions.
112
*/
113
DPLLT
(
TheoryAPI
*
theoryAPI
,
Decider
*
decider
)
114
:
d_theoryAPI
(theoryAPI),
d_decider
(decider) {}
115
virtual
~DPLLT
() {}
116
117
TheoryAPI
*
theoryAPI
() {
return
d_theoryAPI
; }
118
Decider
*
decider
() {
return
d_decider
; }
119
120
void
setDecider
(
Decider
*
decider
) {
d_decider
=
decider
; }
121
122
//! Set a checkpoint for backtracking
123
/*! This should effectively save the current state of the solver. Note that
124
* it should also result in a call to TheoryAPI::push.
125
*/
126
virtual
void
push
() = 0;
127
128
//! Restore checkpoint
129
/*! This should return the state to what it was immediately before the last
130
* call to push. In particular, if one or more calls to checkSat,
131
* continueCheck, or addAssertion have been made since the last push, these
132
* should be undone. Note also that in this case, a single call to
133
* DPLLT::pop may result in multiple calls to TheoryAPI::pop.
134
*/
135
virtual
void
pop
() = 0;
136
137
//! Add new clauses to the SAT solver
138
/*! This is used to add clauses that form a "context" for the next call to
139
* checkSat
140
*/
141
virtual
void
addAssertion
(
const
CNF_Formula
& cnf) = 0;
142
143
virtual
std::vector<SAT::Lit>
getCurAssignments
() =0 ;
144
virtual
std::vector<std::vector<SAT::Lit> >
getCurClauses
() =0 ;
145
146
//! Check the satisfiability of a set of clauses in the current context
147
/*! If the result is SATISFIABLE, UNKNOWN, or ABORT, the DPLLT engine should
148
* remain in the state it is in until pop() is called. If the result is
149
* UNSATISFIABLE, the DPLLT engine should return to the state it was in when
150
* called. Note that it should be possible to call checkSat multiple times,
151
* even if the result is true (each additional call should use the context
152
* left by the previous call).
153
*/
154
virtual
CVC3::QueryResult
checkSat
(
const
CNF_Formula
& cnf) = 0;
155
156
//! Continue checking the last check with additional constraints
157
/*! Should only be called after a previous call to checkSat (or
158
* continueCheck) that returned SATISFIABLE. It should add the clauses in
159
* cnf to the existing clause database and search for a satisfying
160
* assignment. As with checkSat, if the result is not UNSATISFIABLE, the
161
* DPLLT engine should remain in the state containing the satisfiable
162
* assignment until pop() is called. Similarly, if the result is
163
* UNSATISFIABLE, the DPLLT engine should return to the state it was in when
164
* checkSat was last called.
165
*/
166
virtual
CVC3::QueryResult
continueCheck
(
const
CNF_Formula
& cnf) = 0;
167
168
//! Get value of variable: unassigned, false, or true
169
virtual
Var::Val
getValue
(
Var
v) = 0;
170
171
//! Get the proof from SAT engine.
172
virtual
CVC3::Proof
getSatProof
(
CNF_Manager
*,
CVC3::TheoryCore
*) = 0 ;
173
174
};
175
176
}
177
178
#endif
Generated on Tue May 14 2013 09:02:05 for CVC3 by
1.8.3.1