From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 16 Dec 2009 05:33:31 +0000 (+0000)
Subject: Fix simplifying minisat. Previously when the SIMP flag was set, simplifying minisat... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=87ecd8442f870bb2328abdd133bd9d7913428f8c;p=francis%2Fstp.git

Fix simplifying minisat. Previously when the SIMP flag was set, simplifying minisat would not be used. The simplifying solver derived from Minisat, but the solve() method etc. of the base class were not virtual.


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 3aa419e..ecac792 100644
--- 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 98d4a8b..f574771 100644
--- 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); }
 
 //=================================================================================================
 };