I hacked in a temporary way to restart minisat for multiple queries.

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 131ac98dc7d727f7f8f274352ba9000e99b37171..247a5b096c401b7a0873ac05574390fe77475299 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -81,10 +81,6 @@ protected:
    */
   minisat::Lit lookupInCache(const Node & n) const;
 
-  /**
-   * Empties the internal translation cache.
-   */
-  void flushCache();
 
   //negotiates the mapping of atoms to literals with PropEngine
   void registerMapping(const Node & node, minisat::Lit lit, bool atom = false);
@@ -99,6 +95,12 @@ public:
    */
   CnfStream(CVC4::PropEngine *pe);
 
+
+  /**
+   * Empties the internal translation cache.
+   */
+  void flushCache();
+
   /**
    * Converts and asserts a formula.
    * @param n node to convert and assert

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 875d0cd165cdb0a58a4c3ebceff48e7873fbae67..b4df32f0f769b0126fb21a76a23c9822866cbf03 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -33,12 +33,15 @@ namespace CVC4 {
 
 PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) :
   d_de(de), 
-  d_te(te){
+  d_te(te), 
+  d_restartMayBeNeeded(false){
+  d_sat = new Solver();
   d_cnfStream = new CVC4::prop::TseitinCnfStream(this);
 }
 
 PropEngine::~PropEngine(){
   delete d_cnfStream;
+  delete d_sat;
 }
 
 
@@ -47,7 +50,7 @@ void PropEngine::assertClause(vec<Lit> & c){
    *for restarting the sat solver
    */
   //TODO assert that each lit has been mapped to an atom or requested
-  d_sat.addClause(c);
+  d_sat->addClause(c);
 }
 
 void PropEngine::registerAtom(const Node & n, Lit l){
@@ -56,21 +59,39 @@ void PropEngine::registerAtom(const Node & n, Lit l){
 }
 
 Lit PropEngine::requestFreshLit(){
-  Var v = d_sat.newVar();
+  Var v = d_sat->newVar();
   Lit l(v,false);
   return l;
 }
 
 void PropEngine::assertFormula(const Node& node) {
   d_cnfStream->convertAndAssert(node);
+  d_assertionList.push_back(node);
+}
+
+void PropEngine::restart(){
+  delete d_sat;
+  d_sat = new Solver();
+  d_cnfStream->flushCache();
+  d_atom2lit.clear();
+  d_lit2atom.clear();
+
+  for(vector<Node>::iterator iter = d_assertionList.begin();
+      iter != d_assertionList.end(); ++iter){
+    d_cnfStream->convertAndAssert(*iter);
+  }
 }
 
 void PropEngine::solve() {
+  if(d_restartMayBeNeeded)
+    restart();
 
-  //TODO: may need to restart if a previous query returned false
+  d_sat->verbosity = 1;
+  bool result = d_sat->solve();
 
-  d_sat.verbosity = 1;
-  bool result = d_sat.solve();
+  if(!result){
+    d_restartMayBeNeeded = true;
+  }
 
   Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
 }

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index f356c9e0b69e31ecb9bfa1b099512a0cabfa0189..9f5f9dac1cfc7b068369e913e5f2465b8c09c60c 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -52,7 +52,7 @@ class PropEngine {
    * and to start from scratch everytime. (Avoid push/pop problems?)
    * Is this right?
    */
-  CVC4::prop::minisat::SimpSolver d_sat;
+  CVC4::prop::minisat::Solver * d_sat;
 
 
   std::map<Node, CVC4::prop::minisat::Lit> d_atom2lit;
@@ -64,6 +64,21 @@ class PropEngine {
    */
   void registerAtom(const Node & n, CVC4::prop::minisat::Lit l);
 
+  /**
+   * Flags whether the solver may need to have its state reset before
+   * solving occurs
+   */
+  bool d_restartMayBeNeeded;
+  
+  /**
+   * Cleans existing state in the PropEngine and reinitializes the state.
+   */
+  void restart();
+
+  /**
+   * Keeps track of all of the assertions that need to be made.
+   */
+  std::vector<Node> d_assertionList;
 
 
   CVC4::prop::minisat::Lit requestFreshLit();