CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
search_impl_base.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file search_impl_base.h
4
* \brief Abstract API to the proof search engine
5
*
6
* Author: Clark Barrett, Vijay Ganesh (Clausal Normal Form Converter)
7
*
8
* Created: Fri Jan 17 13:35:03 2003
9
*
10
* <hr>
11
*
12
* License to use, copy, modify, sell and/or distribute this software
13
* and its documentation for any purpose is hereby granted without
14
* royalty, subject to the terms and conditions defined in the \ref
15
* LICENSE file provided with this distribution.
16
*
17
* <hr>
18
*
19
*/
20
/*****************************************************************************/
21
22
#ifndef _cvc3__include__search_impl_base_h_
23
#define _cvc3__include__search_impl_base_h_
24
25
#include "
search.h
"
26
#include "
theory_core.h
"
27
#include "
variable.h
"
28
#include "
formula_value.h
"
29
30
namespace
CVC3 {
31
32
class
SearchEngineRules;
33
class
VariableManager;
34
35
//! API to to a generic proof search engine (a.k.a. SAT solver)
36
/*! \ingroup SE */
37
class
SearchImplBase
:
public
SearchEngine
{
38
friend
class
DecisionEngine
;
39
protected
:
40
/*! \addtogroup SE
41
* @{
42
*/
43
//! Variable manager for classes Variable and Literal
44
VariableManager
*
d_vm
;
45
46
/*! @brief The bottom-most scope for the current call to checkSAT (where conflict
47
clauses are still valid).
48
*/
49
CDO<int>
d_bottomScope
;
50
51
TheoryCore::CoreSatAPI
*
d_coreSatAPI_implBase
;
52
53
//! Representation of a DP-suggested splitter
54
class
Splitter
{
55
Literal
d_lit
;
56
public
:
57
// int priority;
58
//! Constructor
59
Splitter
(
const
Literal
& lit);
60
//! Copy constructor
61
Splitter
(
const
Splitter
& s);
62
//! Assignment
63
Splitter
&
operator=
(
const
Splitter
& s);
64
//! Descructor
65
~Splitter
();
66
operator
Literal
() {
return
d_lit
; }
67
//! The order is descending by priority ("reversed", highest first)
68
// friend bool operator<(const Splitter& s1, const Splitter& s2) {
69
// return (s1.priority > s2.priority
70
// || (s1.priority == s2.priority && s1.expr > s2.expr));
71
// }
72
};
73
//! Backtracking ordered set of DP-suggested splitters
74
CDList<Splitter>
d_dpSplitters
;
75
76
/*! @brief Theorem from the last successful checkValid call. It is
77
used by getProof and getAssumptions. */
78
Theorem
d_lastValid
;
79
/*! @brief Assumptions from the last unsuccessful checkValid call.
80
These are used by getCounterExample. */
81
ExprHashMap<bool>
d_lastCounterExample
;
82
/*! @brief Maintain the list of current assumptions (user asserts and
83
splitters) for getAssumptions(). */
84
CDMap<Expr,Theorem>
d_assumptions
;
85
86
//! Backtracking cache for the CNF generator
87
CDMap<Expr, Theorem>
d_cnfCache
;
88
//! Backtracking set of new variables generated by CNF translator
89
/*! Specific search engines do not have to split on these variables */
90
CDMap<Expr, bool>
d_cnfVars
;
91
//! Command line flag whether to convert to CNF
92
const
bool
*
d_cnfOption
;
93
//! Flag: whether to convert term ITEs into CNF
94
const
bool
*
d_ifLiftOption
;
95
//! Flag: ignore auxiliary CNF variables when searching for a splitter
96
const
bool
*
d_ignoreCnfVarsOption
;
97
//! Flag: Preserve the original formula with +cnf (for splitter heuristics)
98
const
bool
*
d_origFormulaOption
;
99
100
/*!
101
* \name CNF Caches
102
*
103
* These caches are for subexpressions of the translated formula
104
* phi, to avoid expanding phi into a tree. We cannot use
105
* d_cnfCache for that, since it is effectively non-backtracking,
106
* and we do not know if a subexpression of phi was translated at
107
* the current level, or at some other (inactive) branch of the
108
* decision tree.
109
* @{
110
*/
111
//! Cache for enqueueCNF()
112
CDMap<Expr,bool>
d_enqueueCNFCache
;
113
//! Cache for applyCNFRules()
114
CDMap<Expr,bool>
d_applyCNFRulesCache
;
115
//! Cache for replaceITE()
116
CDMap<Expr,Theorem>
d_replaceITECache
;
117
/*@}*/
// End of CNF Caches
118
119
//! Construct a Literal out of an Expr or return an existing one
120
Literal
newLiteral
(
const
Expr
& e) {
return
Literal
(
d_vm
, e); }
121
122
/*! @brief Our version of simplifier: take Theorem(e), apply
123
simplifier to get Theorem(e==e'), return Theorem(e') */
124
Theorem
simplify
(
const
Theorem
& e)
125
{
return
d_core
->
iffMP
(e,
d_core
->
simplify
(e.
getExpr
())); }
126
127
//! Notify the search engine about a new literal fact.
128
/*! It should be called by SearchEngine::addFact() only.
129
* Must be implemented by the subclasses of SearchEngine.
130
*
131
* IMPORTANT: do not call addFact() from this function; use
132
* enqueueFact() or setInconsistent() instead.
133
*/
134
virtual
void
addLiteralFact
(
const
Theorem
& thm) = 0;
135
//! Notify the search engine about a new non-literal fact.
136
/*! It should be called by SearchEngine::addFact() only.
137
* Must be implemented by the subclasses of SearchEngine.
138
*
139
* IMPORTANT: do not call addFact() from this function; use
140
* enqueueFact() or setInconsistent() instead.
141
*/
142
virtual
void
addNonLiteralFact
(
const
Theorem
& thm) = 0;
143
//! Add a new fact to the search engine bypassing CNF converter
144
/*! Calls either addLiteralFact() or addNonLiteralFact()
145
* appropriately, and converts to CNF when d_cnfOption is set. If
146
* fromCore==true, this fact already comes from the core, and
147
* doesn't need to be reported back to the core.
148
*/
149
void
addCNFFact
(
const
Theorem
& thm,
bool
fromCore=
false
);
150
151
public
:
152
153
int
getBottomScope
() {
return
d_bottomScope
; }
154
155
//! Check if e is a clause (a literal, or a disjunction of literals)
156
bool
isClause
(
const
Expr
& e);
157
158
//! Check if e is a propositional clause
159
/*! \sa isPropAtom() */
160
bool
isPropClause
(
const
Expr
& e);
161
//! Check whether e is a fresh variable introduced by the CNF converter
162
/*! Search engines do not need to split on those variables in order
163
* to be complete
164
*/
165
bool
isCNFVar
(
const
Expr
& e) {
return
(
d_cnfVars
.count(e) > 0); }
166
//! Check if a splitter is required for completeness
167
/*! Currently, it checks that 'e' is not an auxiliary CNF variable */
168
bool
isGoodSplitter
(
const
Expr
& e);
169
170
private
:
171
172
//! Translate theta to CNF and enqueue the new clauses
173
void
enqueueCNF
(
const
Theorem
& theta);
174
//! Recursive version of enqueueCNF()
175
void
enqueueCNFrec
(
const
Theorem
& theta);
176
//! FIXME: write a comment
177
void
applyCNFRules
(
const
Theorem
& e);
178
179
//! Cache a theorem phi <=> v by phi, where v is a literal.
180
void
addToCNFCache
(
const
Theorem
& thm);
181
182
//! Find a theorem phi <=> v by phi, where v is a literal.
183
/*! \return Null Theorem if not found. */
184
Theorem
findInCNFCache
(
const
Expr
& e);
185
186
//! Replaces ITE subexpressions in e with variables
187
Theorem
replaceITE
(
const
Expr
& e);
188
189
protected
:
190
191
//! Return the current scope level (for convenience)
192
int
scopeLevel
() {
return
d_core
->
getCM
()->
scopeLevel
(); }
193
194
public
:
195
//! Constructor
196
SearchImplBase
(
TheoryCore
* core);
197
//! Destructor
198
virtual
~SearchImplBase
();
199
200
virtual
void
registerAtom
(
const
Expr
& e)
201
{
d_core
->
theoryOf
(e)->
registerAtom
(e,
Theorem
()); }
202
virtual
Theorem
getImpliedLiteral
() {
return
d_core
->
getImpliedLiteral
(); }
203
virtual
void
push
() {
d_core
->
getCM
()->
push
(); }
204
virtual
void
pop
() {
d_core
->
getCM
()->
pop
(); }
205
206
///////////////////////////////////////////////////////////////////////////
207
// checkValid() is the method that subclasses must implement.
208
///////////////////////////////////////////////////////////////////////////
209
210
//! Checks the validity of a formula in the current context
211
/*! The method that actually calls the SAT solver (implemented in a
212
subclass). It should maintain d_assumptions (add all asserted
213
splitters to it), and set d_lastValid and d_lastCounterExample
214
appropriately before exiting. */
215
virtual
QueryResult
checkValidInternal
(
const
Expr
& e) = 0;
216
//! Similar to checkValidInternal(), only returns Theorem(e) or Null
217
virtual
QueryResult
checkValid
(
const
Expr
& e,
Theorem
& result);
218
//! Reruns last check with e as an additional assumption
219
virtual
QueryResult
restartInternal
(
const
Expr
& e) = 0;
220
//! Reruns last check with e as an additional assumption
221
virtual
QueryResult
restart
(
const
Expr
& e,
Theorem
& result);
222
void
returnFromCheck
()
223
{
Theorem
thm;
restart
(
d_core
->
falseExpr
(), thm); }
224
virtual
Theorem
lastThm
() {
return
d_lastValid
; }
225
226
///////////////////////////////////////////////////////////////////////////
227
// The following methods are provided by the base class, and in most
228
// cases should be sufficient. However, they are virtual so that
229
// subclasses can add functionality to them if needed.
230
///////////////////////////////////////////////////////////////////////////
231
232
/*! @brief Generate and add a new assertion to the set of assertions
233
in the current context. This should only be used by class VCL in
234
assertFormula(). */
235
Theorem
newUserAssumption
(
const
Expr
& e);
236
//! Add a new internal asserion
237
virtual
Theorem
newIntAssumption
(
const
Expr
& e);
238
//! Helper for above function
239
void
newIntAssumption
(
const
Theorem
& thm);
240
//! Get all assumptions made in this and all previous contexts.
241
/*! \param assumptions should be an empty vector which will be filled \
242
with the assumptions */
243
void
getUserAssumptions
(std::vector<Expr>& assumptions);
244
void
getInternalAssumptions
(std::vector<Expr>& assumptions);
245
virtual
void
getAssumptions
(std::vector<Expr>& assumptions);
246
//! Check if the formula has been assumed
247
virtual
bool
isAssumption
(
const
Expr
& e);
248
249
//! Add a new fact to the search engine from the core
250
/*! It should be called by TheoryCore::assertFactCore(). */
251
void
addFact
(
const
Theorem
& thm);
252
253
//! Suggest a splitter to the SearchEngine
254
/*! The higher is the priority, the sooner the SAT solver will split
255
* on it. It can be positive or negative (default is 0).
256
*
257
* The set of suggested splitters is backtracking; that is, a
258
* splitter is "forgotten" once the scope is backtracked.
259
*
260
* This method can be used either to change the priority
261
* of existing splitters, or to introduce new splitters that DPs
262
* consider relevant, even though they do not appear in existing
263
* formulas.
264
*/
265
virtual
void
addSplitter
(
const
Expr
& e,
int
priority);
266
267
virtual
void
getCounterExample
(std::vector<Expr>& assertions,
bool
inOrder =
true
);
268
269
// The following two methods should be called only after a checkValid
270
// which returns true. In any other case, they return Null values.
271
272
//! Returns the proof term for the last proven query
273
/*! It should be called only after a checkValid which returns true.
274
In any other case, it returns Null. */
275
virtual
Proof
getProof
();
276
/*! @brief Returns the set of assumptions used in the proof. It
277
should be a subset of getAssumptions(). */
278
/*! It should be called only after a checkValid which returns true.
279
In any other case, it returns Null. */
280
virtual
const
Assumptions
&
getAssumptionsUsed
();
281
282
//! Process result of checkValid
283
void
processResult
(
const
Theorem
& res,
const
Expr
& e);
284
285
//:ALEX:
286
inline
virtual
FormulaValue
getValue
(
const
CVC3::Expr
& e) {
287
FatalAssert
(
false
,
"not implemented"
);
288
return
UNKNOWN_VAL
;
289
}
290
291
/* @} */
// end of group SE
292
293
};
294
295
296
}
297
298
#endif
Generated on Mon Aug 19 2013 14:42:42 for CVC3 by
1.8.4