Fix simplifying minisat. Previously when the SIMP flag was set, simplifying minisat...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@515 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/sat/core/Solver.h b/src/sat/core/Solver.h
index 3aa419e13bb373789ce774b8a803831c7f6dd117..ecac792426a98e88eb22d5c20898e5ebffdf8ed4 100644 (file)
--- a/src/sat/core/Solver.h
+++ b/src/sat/core/Solver.h
@@ -100,15 +100,15 @@ public:
 
     // Problem specification:
     //
-    Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
-    bool    addClause (vec<Lit>& ps);                           // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
+    virtual Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
+    virtual bool    addClause (vec<Lit>& ps);                           // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
 
 
     // Solving:
     //
-    bool    simplify     ();                        // Removes already satisfied clauses.
+    virtual bool    simplify     ();                        // Removes already satisfied clauses.
     bool    solve        (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
-    bool    solve        ();                        // Search without assumptions.
+    virtual bool    solve        ();                        // Search without assumptions.
     bool    okay         () const;                  // FALSE means solver is in a conflicting state
 
     // Variable mode:

diff --git a/src/sat/simp/SimpSolver.h b/src/sat/simp/SimpSolver.h
index 98d4a8b2997bb9b35679dc97eafd249a33286148..f5747712ddc4099d46af9438fc57a02fa461bf1f 100644 (file)
--- a/src/sat/simp/SimpSolver.h
+++ b/src/sat/simp/SimpSolver.h
@@ -98,7 +98,7 @@ class SimpSolver : public Solver {
     // Solving:
     //
     bool    solve     (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
-    bool    solve     (bool do_simp = true, bool turn_off_simp = false);
+    bool    solve     ();
     bool    eliminate (bool turn_off_elim = false);  // Perform variable elimination based simplification. 
 
     // Generate a (possibly simplified) DIMACS file:
@@ -208,7 +208,7 @@ inline vec<Clause*>& SimpSolver::getOccurs(Var x) {
 
 inline bool  SimpSolver::isEliminated (Var v) const { return v < elimtable.size() && elimtable[v].order != 0; }
 inline void  SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } }
-inline bool  SimpSolver::solve        (bool do_simp, bool turn_off_simp) { vec<Lit> tmp; return solve(tmp, do_simp, turn_off_simp); }
+inline bool  SimpSolver::solve        () { vec<Lit> tmp; return solve(tmp, true, false); }
 
 //=================================================================================================
 };