39 if (d_core->outOfResources())
return ABORT;
41 if (d_core->inconsistent()) {
42 TRACE(
"search",
"checkValidRec => ", d_core->inconsistentThm(),
43 " (context inconsistent) }");
44 d_decisionEngine->goalSatisfied();
45 thm = d_core->inconsistentThm();
50 bool workingOnGoal =
true;
51 if (d_goal.get().getExpr().isTrue()) {
52 e = d_nonLiterals.get();
53 workingOnGoal =
false;
59 simp = d_commonRules->iffMP(simp, d_core->find(rhs));
63 if (workingOnGoal) d_goal.set(simp);
64 else d_nonLiterals.set(simp);
67 TRACE(
"search",
"checkValidRec => ", simp,
" (rhs=false) }");
68 d_decisionEngine->goalSatisfied();
73 if (workingOnGoal || !d_core->checkSATCore()) {
74 return checkValidRec(thm);
76 TRACE(
"search",
"checkValidRec => ",
"Null (true)",
"}");
80 Expr splitter = d_decisionEngine->findSplitter(rhs);
82 d_decisionEngine->pushDecision(splitter);
85 d_decisionEngine->popDecision();
86 d_decisionEngine->pushDecision(splitter,
false);
88 qres = checkValidRec(thm2);
90 d_decisionEngine->popDecision();
91 thm = d_rules->caseSplit(splitter, thm, thm2);
104 d_goal(core->getCM()->getCurrentContext()),
105 d_nonLiterals(core->getCM()->getCurrentContext()),
106 d_simplifiedThm(core->getCM()->getCurrentContext())
136 "checkValid: Expected true goal");
138 d_goal.get().getLeafAssumptions(a);
140 for (vector<Expr>::iterator i=a.begin(), iend=a.end(); i != iend; ++i) {
149 TRACE_MSG(
"search terse",
"checkValid => true}");
158 TRACE_MSG(
"search terse",
"checkValid => false}");
159 TRACE_MSG(
"search",
"checkValid => false; }");
170 TRACE(
"search",
"checkValid(", e,
") {");
171 TRACE_MSG(
"search terse",
"checkValid() {");
175 (
"checking validity of a non-boolean expression:\n\n "
177 +
"\n\nwhich has the following type:\n\n "
192 TRACE_MSG(
"search terse",
"checkValid: Asserting !e: ");
193 TRACE(
"search",
"checkValid: Asserting !e: ", not_e2,
"");
209 TRACE(
"search",
"restart(", e,
") {");
210 TRACE_MSG(
"search terse",
"restart() {");
214 (
"argument to restart is a non-boolean expression:\n\n "
216 +
"\n\nwhich has the following type:\n\n "
221 throw Exception(
"Call to restart with no current query");
227 TRACE_MSG(
"search terse",
"restart: Asserting e: ");
228 TRACE(
"search",
"restart: Asserting e: ", e,
"");
~SearchSimple()
Destructor.
Data structure of expressions in CVC3.
QueryResult checkValidInternal(const Expr &e)
Checks the validity of a formula in the current context.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Decision Engine for use with the Search EngineAuthor: Clark Barrett.
CDO< Theorem > d_nonLiterals
Non-literals generated by DP's.
CDO< int > d_bottomScope
The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid)...
An exception to be thrown at typecheck error.
Theorem d_lastValid
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.
QueryResult checkValidRec(Theorem &thm)
Recursive DPLL algorithm used by checkValid.
bool incomplete()
Check if the current decision branch is marked as incomplete.
#define DebugAssert(cond, str)
CommonProofRules * d_commonRules
Common proof rules.
void addNonLiteralFact(const Theorem &thm)
Notify the search engine about a new non-literal fact.
Abstract proof rules interface to the simple search engine.
#define TRACE_MSG(flag, msg)
DecisionEngine * d_decisionEngine
Decision Engine.
ExprTransform * getExprTrans() const
CDMap< Expr, Theorem > d_assumptions
Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().
std::string toString() const
Print the expression to a string.
ExprHashMap< bool > d_lastCounterExample
Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample.
Theorem newUserAssumption(const Expr &e)
Generate and add a new assertion to the set of assertions in the current context. This should only be...
virtual Theorem andIntro(const Theorem &e1, const Theorem &e2)=0
std::string toString() const
void processResult(const Theorem &res, const Expr &e)
Process result of checkValid.
int scopeLevel()
Return the current scope level (for convenience)
virtual Theorem trueTheorem()=0
==> TRUE
ContextManager * getCM() const
API to to a generic proof search engine (a.k.a. SAT solver)
virtual Theorem iffContrapositive(const Theorem &thm)=0
e1 <=> e2 ==> ~e1 <=> ~e2
CDO< Theorem > d_simplifiedThm
Theorem which records simplification of the last query.
virtual Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0
QueryResult restartInternal(const Expr &e)
Reruns last check with e as an additional assumption.
Type getType() const
Get the type. Recursively compute if necessary.
CDO< Theorem > d_goal
Formula being checked.
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...
virtual Theorem symmetryRule(const Theorem &a1_eq_a2)=0
(same for IFF)
TheoryCore * d_core
Access to theory reasoning.
QueryResult checkValidMain(const Expr &e2)
Private helper function for checkValid and restart.