Bugfix. simplifying-minisat failed when abstraction/refinement was turned on. The...

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

diff --git a/src/sat/MinisatCore.cpp b/src/sat/MinisatCore.cpp
index 236190a11f7fbe33912f5814f0b3dae8fbe5dfdb..e90b10b787bfc9d6d2b7bb6f178d9e70834a6d8a 100644 (file)
--- a/src/sat/MinisatCore.cpp
+++ b/src/sat/MinisatCore.cpp
@@ -1,6 +1,7 @@
 #include "core/Solver.h"
 #include "MinisatCore.h"
 #include "utils/System.h"
+#include "simp/SimpSolver.h"
 
 namespace BEEV
 {
@@ -85,4 +86,5 @@ namespace BEEV
   // I was going to make SimpSolver and Solver instances of this template.
   // But I'm not so sure now because I don't understand what eliminate() does in the simp solver.
   template class MinisatCore<Minisat::Solver>;
+  template class MinisatCore<Minisat::SimpSolver>;
 };

diff --git a/src/sat/SimplifyingMinisat.cpp b/src/sat/SimplifyingMinisat.cpp
index a106f56ae3b518aee3811cd529a37f5b7481d9d7..e1e1115d8d6236633f11e82298a3fdd438b9098e 100644 (file)
--- a/src/sat/SimplifyingMinisat.cpp
+++ b/src/sat/SimplifyingMinisat.cpp
@@ -6,7 +6,7 @@ namespace BEEV
 {
   SimplifyingMinisat::SimplifyingMinisat()
   {
-    s = new Minisat::SimpSolver();
+        s = new Minisat::SimpSolver();
   }
 
   SimplifyingMinisat::~SimplifyingMinisat()
@@ -32,6 +32,8 @@ namespace BEEV
     if (!s->simplify())
       return false;
 
+    // Without the eliminate(true) call. Calling solve() multiple times returns the wrong answer.
+       s->eliminate(true);
     return s->solve();
   }