Bugfix. r1018 caused wrong answers. It left out a case needed for booth recoding.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 958377e1721f70a3191de59e8c4cb2440bcfcb5d..800706a26a789da2a2dda35716a3d2823e58d34f 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -291,7 +291,6 @@ namespace BEEV {
                                        &toSATAIG
                                        );
 
-    delete cb;
     }
     else
       {

diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index 7774d6a5bf25aa9dcc562d7a494b5dd28b6dd3b4..1578115eeb09d210a2120ad5afc200f6d35d8635 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -13,13 +13,27 @@ namespace BEEV
         return false;
 
       BBNodeManagerAIG mgr;
-      Simplifier simp(bm);
-      BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&mgr,cb,&simp,bm->defaultNodeFactory,&bm->UserFlags);
+      Simplifier *simp = new Simplifier(bm);
+      BitBlaster<BBNodeAIG, BBNodeManagerAIG> *bb = new BitBlaster<BBNodeAIG, BBNodeManagerAIG>(&mgr,cb,simp,bm->defaultNodeFactory,&bm->UserFlags);
+
+      // Even if we cleared the tables we could still have the hash table's buckets sitting around.
+      delete simp;
+      simp = NULL;
 
       bm->GetRunTimes()->start(RunTimes::BitBlasting);
-      BBNodeAIG BBFormula = bb.BBForm(input);
+      BBNodeAIG BBFormula = bb->BBForm(input);
       bm->GetRunTimes()->stop(RunTimes::BitBlasting);
-      bb.ClearAllTables();
+      delete bb;
+      bb = NULL;
+
+      //Clear out all the constant bit stuff before sending the SAT.
+      if (cb != NULL)
+        {
+          delete cb;
+          cb = NULL;
+        }
+
+
 
       assert(satSolver.nVars() ==0);
 
@@ -37,10 +51,6 @@ namespace BEEV
       BBFormula = BBNodeAIG(); // null node
       mgr.stop();
 
-      //Clear out all the constant bit stuff before sending the SAT.
-      if (cb != NULL)
-         cb->clearTables();
-
       bm->GetRunTimes()->start(RunTimes::SendingToSAT);
 
       for (int i = 0; i < cnfData->nVars; i++)

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 0e08da0c46580f019e2d8c58921140e2cff02f80..10e46b75f439b9e6f56976d87e7b36d1c865edcd 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1277,7 +1277,8 @@ void BitBlaster<BBNode,BBNodeManagerT>::mult_Booth(const BBNodeVec& x_i, const B
                         pushP(products,i,y,x[i],nf);
                 }
 
-                else if (xt[i] == MINUS_ONE_MT)
+                // A bit can not be true or false, as well as one of these two.
+                if (xt[i] == MINUS_ONE_MT)
                 {
                         pushP(products,i,notY,BBTrue,nf);
                         products[i].push(BBTrue);
@@ -1288,7 +1289,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::mult_Booth(const BBNodeVec& x_i, const B
                         pushP(products,i,y,BBTrue,nf);
                 }
 
-                else if (products[i].size() == 0)
+                if (products[i].size() == 0)
                   products[i].push(BBFalse);
         }
   }