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,
"");