CVC3

search_simple.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file search_simple.cpp
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Sat Mar 29 21:59:36 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 #include "search_simple.h"
00022 #include "theory_core.h"
00023 #include "typecheck_exception.h"
00024 #include "search_rules.h"
00025 
00026 #include "decision_engine_dfs.h"
00027 //#include "decision_engine_caching.h"
00028 //#include "decision_engine_mbtf.h"
00029 #include "expr_transform.h"
00030 #include "command_line_flags.h"
00031 
00032 
00033 using namespace std;
00034 using namespace CVC3;
00035 
00036 
00037 QueryResult SearchSimple::checkValidRec(Theorem& thm)
00038 {
00039   if (d_core->outOfResources()) return ABORT;
00040   TRACE_MSG("search", "checkValidRec() {");
00041   if (d_core->inconsistent()) {
00042     TRACE("search", "checkValidRec => ", d_core->inconsistentThm(),
00043     " (context inconsistent) }");
00044     d_decisionEngine->goalSatisfied();
00045     thm = d_core->inconsistentThm();
00046     return UNSATISFIABLE;
00047   }
00048 
00049   Theorem e = d_goal.get();
00050   bool workingOnGoal = true;
00051   if (d_goal.get().getExpr().isTrue()) {
00052     e = d_nonLiterals.get();
00053     workingOnGoal = false;
00054   }
00055 
00056   Theorem simp = simplify(e);
00057   Expr rhs = simp.getExpr();
00058   if (rhs.hasFind()) {
00059     simp = d_commonRules->iffMP(simp, d_core->find(rhs));
00060     rhs = simp.getExpr();
00061   }
00062 
00063   if (workingOnGoal) d_goal.set(simp);
00064   else d_nonLiterals.set(simp);
00065 
00066   if (rhs.isFalse()) {
00067     TRACE("search", "checkValidRec => ", simp, " (rhs=false) }");
00068     d_decisionEngine->goalSatisfied();
00069     thm = simp;
00070     return UNSATISFIABLE;
00071   }
00072   else if (rhs.isTrue()) {
00073     if (workingOnGoal || !d_core->checkSATCore()) {
00074       return checkValidRec(thm);
00075     }
00076     TRACE("search", "checkValidRec => ", "Null (true)", "}");
00077     thm = Theorem();
00078     return SATISFIABLE;
00079   }
00080   Expr splitter = d_decisionEngine->findSplitter(rhs);
00081   DebugAssert(!splitter.isNull(), "Expected splitter");
00082   d_decisionEngine->pushDecision(splitter);
00083   QueryResult qres = checkValidRec(thm);
00084   if (qres == UNSATISFIABLE) {
00085     d_decisionEngine->popDecision();
00086     d_decisionEngine->pushDecision(splitter, false);
00087     Theorem thm2;
00088     qres = checkValidRec(thm2);
00089     if (qres == UNSATISFIABLE) {
00090       d_decisionEngine->popDecision();
00091       thm = d_rules->caseSplit(splitter, thm, thm2);
00092       return qres;
00093     }
00094     thm = thm2;
00095     return qres;
00096   }
00097   return qres;
00098 }
00099 
00100 
00101 SearchSimple::SearchSimple(TheoryCore* core)
00102   : SearchImplBase(core),
00103     d_name("simple"),
00104     d_goal(core->getCM()->getCurrentContext()),
00105     d_nonLiterals(core->getCM()->getCurrentContext()),
00106     d_simplifiedThm(core->getCM()->getCurrentContext())
00107 {
00108 //   if (core->getFlags()["de"].getString() == "caching")
00109 //     d_decisionEngine = new DecisionEngineCaching(core, this);
00110 //   else if (core->getFlags()["de"].getString() == "mbtf")
00111 //     d_decisionEngine = new DecisionEngineMBTF(core, this);
00112 //   else
00113     d_decisionEngine = new DecisionEngineDFS(core, this);
00114 
00115   d_goal.set(d_commonRules->trueTheorem());
00116   d_nonLiterals.set(d_commonRules->trueTheorem());
00117 }
00118 
00119 
00120 SearchSimple::~SearchSimple()
00121 {
00122   delete d_decisionEngine;
00123 }
00124 
00125 
00126 QueryResult SearchSimple::checkValidMain(const Expr& e2)
00127 {
00128   Theorem thm;
00129 
00130   QueryResult qres = checkValidRec(thm);
00131 
00132   if (qres == SATISFIABLE && d_core->incomplete()) qres = UNKNOWN;
00133 
00134   if (qres == SATISFIABLE) {
00135     DebugAssert(d_goal.get().getExpr().isTrue(),
00136                 "checkValid: Expected true goal");
00137     vector<Expr> a;
00138     d_goal.get().getLeafAssumptions(a);
00139     d_lastCounterExample.clear();
00140     for (vector<Expr>::iterator i=a.begin(), iend=a.end(); i != iend; ++i) {
00141       d_lastCounterExample[*i] = true;
00142     }
00143   }
00144   else if (qres != UNSATISFIABLE) return qres;
00145 
00146   processResult(thm, e2);
00147 
00148   if (qres == UNSATISFIABLE) {
00149     TRACE_MSG("search terse", "checkValid => true}");
00150     TRACE("search", "checkValid => true; theorem = ", d_lastValid, "}");
00151 
00152     Theorem e_iff_e2(d_commonRules->iffContrapositive(d_simplifiedThm));
00153     d_lastValid =
00154       d_commonRules->iffMP(d_lastValid, d_commonRules->symmetryRule(e_iff_e2));
00155     d_core->getCM()->pop();
00156   }
00157   else {
00158     TRACE_MSG("search terse", "checkValid => false}");
00159     TRACE_MSG("search", "checkValid => false; }");
00160   }
00161   return qres;
00162 }
00163 
00164 
00165 QueryResult SearchSimple::checkValidInternal(const Expr& e)
00166 {
00167   DebugAssert(d_goal.get().getExpr().isTrue(),"checkValid: Expected true goal");
00168   DebugAssert(d_nonLiterals.get().getExpr().isTrue(),"checkValid: Expected true nonLiterals");
00169 
00170   TRACE("search", "checkValid(", e, ") {");
00171   TRACE_MSG("search terse", "checkValid() {");
00172 
00173   if (!e.getType().isBool()) {
00174     throw TypecheckException
00175       ("checking validity of a non-boolean expression:\n\n  "
00176        + e.toString()
00177        + "\n\nwhich has the following type:\n\n  "
00178        + e.getType().toString());
00179   }
00180 
00181   // A successful query should leave the context unchanged
00182   d_core->getCM()->push();
00183   d_bottomScope = scopeLevel();
00184 
00185   d_simplifiedThm.set(d_core->getExprTrans()->preprocess(e.negate()));
00186   TRACE("search", "checkValid: simplifiedThm = ", d_simplifiedThm, "");
00187 
00188   const Expr& not_e2 = d_simplifiedThm.get().getRHS();
00189   Expr e2 = not_e2.negate();
00190 
00191   // Assert not_e2 if it's not already asserted
00192   TRACE_MSG("search terse", "checkValid: Asserting !e: ");
00193   TRACE("search", "checkValid: Asserting !e: ", not_e2, "");
00194   Theorem not_e2_thm;
00195   if(d_assumptions.count(not_e2) == 0) {
00196     not_e2_thm = newUserAssumption(not_e2);
00197   } else {
00198     not_e2_thm = d_assumptions[not_e2];
00199   }
00200   d_core->addFact(not_e2_thm);
00201   d_goal.set(not_e2_thm);
00202 
00203   return checkValidMain(e2);
00204 }
00205 
00206 
00207 QueryResult SearchSimple::restartInternal(const Expr& e)
00208 {
00209   TRACE("search", "restart(", e, ") {");
00210   TRACE_MSG("search terse", "restart() {");
00211 
00212   if (!e.getType().isBool()) {
00213     throw TypecheckException
00214       ("argument to restart is a non-boolean expression:\n\n  "
00215        + e.toString()
00216        + "\n\nwhich has the following type:\n\n  "
00217        + e.getType().toString());
00218   }
00219 
00220   if (d_bottomScope == 0) {
00221     throw Exception("Call to restart with no current query");
00222   }
00223   d_core->getCM()->popto(d_bottomScope);
00224 
00225   Expr e2 = d_simplifiedThm.get().getRHS().negate();
00226 
00227   TRACE_MSG("search terse", "restart: Asserting e: ");
00228   TRACE("search", "restart: Asserting e: ", e, "");
00229   if(d_assumptions.count(e) == 0) {
00230     d_core->addFact(newUserAssumption(e));
00231   }
00232 
00233   return checkValidMain(e2);
00234 }
00235 
00236 
00237 void SearchSimple::addNonLiteralFact(const Theorem& thm)
00238 {
00239   d_nonLiterals.set(d_commonRules->andIntro(d_nonLiterals.get(), thm));
00240 }