Improvement. Simplifying minisat now uses the advanced CNF generator by default.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 2fe332a4bc3aa6ce909e7f9f5b379fa6b978a248..69b01d6983c53cca954142f2a9fbf83bbf1711be 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -446,9 +446,6 @@ namespace BEEV {
     if (bm->UserFlags.stats_flag)
       simp->printCacheStatus();
 
-    const bool useAIGToCNF = (!arrayops || !bm->UserFlags.arrayread_refinement_flag || bm->UserFlags.solver_to_use
-        == UserDefinedFlags::MINISAT_SOLVER) && !bm->UserFlags.isSet("traditional-cnf", "0");
-
     const bool maybeRefinement = arrayops && bm->UserFlags.arrayread_refinement_flag;
 
     simplifier::constantBitP::ConstantBitPropagation* cb = NULL;
@@ -469,8 +466,9 @@ namespace BEEV {
       }
 
     ToSATAIG toSATAIG(bm, cb);
+    toSATAIG.setArrayTransformer(arrayTransformer);
 
-    ToSATBase* satBase = useAIGToCNF ? ((ToSAT*) &toSATAIG) : tosat;
+    ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ;
 
     // If it doesn't contain array operations, use ABC's CNF generation.
     res = Ctr_Example->CallSAT_ResultCheck(NewSolver, simplified_solved_InputToSAT, orig_input, satBase,

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index 658a1d737fa70c3b6882a736dd204d20b96abdcb..5617807bb9a83eb876d3f840904991b3018f5ffe 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -36,7 +36,12 @@ namespace BEEV
                 assert(a.GetKind() == SYMBOL);
                 // It was ommitted from the initial problem, so assign it freshly.
                 for (int i = 0; i < a.GetValueWidth(); i++)
-                    v_a.push_back(SatSolver.newVar());
+                    {
+                        SATSolver::Var v = SatSolver.newVar();
+                        // We probably don't want the variable eliminated.
+                        SatSolver.setFrozen(v);
+                        v_a.push_back(v);
+                    }
                 satVar.insert(make_pair(a, v_a));
             }
     }

diff --git a/src/sat/MinisatCore.cpp b/src/sat/MinisatCore.cpp
index e90b10b787bfc9d6d2b7bb6f178d9e70834a6d8a..b85fd1b5f777385423a19fe5adafc0dad9def9e7 100644 (file)
--- a/src/sat/MinisatCore.cpp
+++ b/src/sat/MinisatCore.cpp
@@ -86,5 +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>;
+  //template class MinisatCore<Minisat::SimpSolver>;
 };

diff --git a/src/sat/SATSolver.h b/src/sat/SATSolver.h
index 7cad410c97ef4db3909d87a1fdfad47e3e394916..ea3aba5c88dc4574477c360466f746a13d391ad1 100644 (file)
--- a/src/sat/SATSolver.h
+++ b/src/sat/SATSolver.h
@@ -55,6 +55,10 @@ namespace BEEV
     virtual lbool false_literal() =0;
     virtual lbool undef_literal() =0;
 
+    // The simplifying solvers shouldn't eliminate index / value variables.
+    virtual void setFrozen(Var x)
+    {}
+
   };
 };
 #endif

diff --git a/src/sat/SimplifyingMinisat.cpp b/src/sat/SimplifyingMinisat.cpp
index e1e1115d8d6236633f11e82298a3fdd438b9098e..7bd529596dbe7b4c1925189a8cb7aa3bcbae7dfa 100644 (file)
--- a/src/sat/SimplifyingMinisat.cpp
+++ b/src/sat/SimplifyingMinisat.cpp
@@ -32,8 +32,6 @@ 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();
   }
 
@@ -76,4 +74,8 @@ namespace BEEV
     printf("CPU time              : %g s\n", cpu_time);
   }
 
+  void SimplifyingMinisat::setFrozen(Var x)
+  {
+      s->setFrozen(x,true);
+  }
 };

diff --git a/src/sat/SimplifyingMinisat.h b/src/sat/SimplifyingMinisat.h
index c71b02715674213304bcdb44497c858b72998a6d..314b188b01c6bb49378a11ea38ee26ea0dbfa0d3 100644 (file)
--- a/src/sat/SimplifyingMinisat.h
+++ b/src/sat/SimplifyingMinisat.h
@@ -48,6 +48,7 @@ namespace BEEV
     virtual lbool false_literal()  {return ((uint8_t)1);}
     virtual lbool undef_literal()  {return ((uint8_t)2);}
 
+    virtual void setFrozen(Var x);
  };
 }
 ;

diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index b9bf1bcd5f56ca4603b78791dac82fb7eec3e686..d48cb820f173debc9e46b279f83b9ac3a0e43658 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -111,6 +111,36 @@ namespace BEEV
          Cnf_DataFree(cnfData);
          cnfData = NULL;
 
+         // Minisat doesn't, but simplifying minisat and cryptominsat eliminate variables during their
+         // simplification phases. The problem is that we may later add clauses in that refer to those
+         // simplified-away variables. Here we mark them as frozen which prevents them from being removed.
+         for (ArrayTransformer::ArrType::iterator it = arrayTransformer->arrayToIndexToRead.begin(); it
+                != arrayTransformer->arrayToIndexToRead.end(); it++)
+            {
+                ArrayTransformer::arrTypeMap& atm = it->second;
+
+                for (ArrayTransformer::arrTypeMap::const_iterator it2 = atm.begin(); it2 != atm.end(); it2++)
+                    {
+                        const ArrayTransformer::ArrayRead& ar = it2->second;
+                        ASTNodeToSATVar::iterator it = nodeToSATVar.find(ar.index_symbol);
+                        if (it != nodeToSATVar.end())
+                            {
+                                vector<unsigned>& v = it->second;
+                                for (int i=0; i < v.size(); i++)
+                                    satSolver.setFrozen(v[i]);
+                            }
+
+                        it = nodeToSATVar.find(ar.symbol);
+                        if (it != nodeToSATVar.end())
+                            {
+                                vector<unsigned>& v = it->second;
+                                for (int i=0; i < v.size(); i++)
+                                    satSolver.setFrozen(v[i]);
+                            }
+                    }
+            }
+
+
       bm->GetRunTimes()->start(RunTimes::Solving);
       satSolver.solve();
       bm->GetRunTimes()->stop(RunTimes::Solving);

diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h
index 3a33b17752f5e42c32fd68064442ac8ecba57875..f5b4e4bb1852c0661981653a9a8d82c5921d7bd3 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.h
+++ b/src/to-sat/AIG/ToSATAIG.h
@@ -17,6 +17,7 @@
 #include "../BitBlaster.h"
 #include "BBNodeManagerAIG.h"
 #include "ToCNFAIG.h"
+#include "../../AST/ArrayTransformer.h"
 
 namespace BEEV
 {
@@ -28,6 +29,8 @@ namespace BEEV
     ASTNodeToSATVar nodeToSATVar;
     simplifier::constantBitP::ConstantBitPropagation* cb;
 
+    ArrayTransformer *arrayTransformer;
+
     // don't assign or copy construct.
     ToSATAIG&  operator = (const ToSATAIG& other);
     ToSATAIG(const ToSATAIG& other);
@@ -43,10 +46,16 @@ namespace BEEV
         count = 0;
         first = true;
         CNFFileNameCounter =0;
+        arrayTransformer = NULL;
     }
 
   public:
 
+    void setArrayTransformer(ArrayTransformer *at)
+    {
+        arrayTransformer = at;
+    }
+
     bool cbIsDestructed()
     {
        return cb == NULL;