During the size reducing transformations, now set the top node to true during constan...

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index dd36322c64daab26749456977694fbe53b0d1b25..5ca08832df8d37df6c3e2a70d6d57e99b835031a 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -100,27 +100,33 @@ namespace BEEV {
         bm->ASTNodeStats("After Establishing Intervals: ", simplified_solved_InputToSAT);
       }
 
+    simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer);
+    if (simp->hasUnappliedSubstitutions())
+      {
+        simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT);
+        simp->haveAppliedSubstitutionMap();
+        bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT);
+      }
+
     if (bm->UserFlags.bitConstantProp_flag)
       {
         bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation);
         SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
         simplifier::constantBitP::ConstantBitPropagation cb(simp, &nf, simplified_solved_InputToSAT);
-        simplified_solved_InputToSAT = cb.topLevelBothWays(simplified_solved_InputToSAT, false);
+        simplified_solved_InputToSAT = cb.topLevelBothWays(simplified_solved_InputToSAT, true,false);
 
         bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation);
 
         if (cb.isUnsatisfiable())
           simplified_solved_InputToSAT = bm->ASTFalse;
 
-        bm->ASTNodeStats("After Constant Bit Propagation begins: ", simplified_solved_InputToSAT);
-      }
+        if (simp->hasUnappliedSubstitutions())
+          {
+            simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT);
+            simp->haveAppliedSubstitutionMap();
+          }
 
-    simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer);
-    if (simp->hasUnappliedSubstitutions())
-      {
-        simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT);
-        simp->haveAppliedSubstitutionMap();
-        bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT);
+        bm->ASTNodeStats("After Constant Bit Propagation begins: ", simplified_solved_InputToSAT);
       }
 
     // Find pure literals.
@@ -167,19 +173,35 @@ namespace BEEV {
     BVSolver* bvSolver = new BVSolver(bm, simp);
 
     simplified_solved_InputToSAT = sizeReducing(inputToSAT, bvSolver);
-    //simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT,bvSolver);
 
     unsigned initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
+
+    // Fixed point it if it's not too difficult.
+    // Currently we discards all the state each time sizeReducing is called,
+    // so it's expensive to call.
+    if (!arrayops && initial_difficulty_score < 1000000)
+      {
+        while (true)
+          {
+            ASTNode last = simplified_solved_InputToSAT;
+            simplified_solved_InputToSAT = sizeReducing(last, bvSolver);
+            if (last == simplified_solved_InputToSAT)
+              break;
+          }
+        initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
+      }
+
     if (bm->UserFlags.stats_flag)
       cout << "Difficulty After Size reducing:" << initial_difficulty_score << endl;
 
     // Copy the solver map incase we need to revert.
     ASTNodeMap initialSolverMap;
+    ASTNode toRevertTo;
     if (!arrayops) // we don't revert for Array problems yet, so don't copy it.
       {
         initialSolverMap.insert(simp->Return_SolverMap()->begin(), simp->Return_SolverMap()->end());
+        toRevertTo = simplified_solved_InputToSAT;
       }
-    ASTNode toRevertTo = simplified_solved_InputToSAT;
 
     //round of substitution, solving, and simplification. ensures that
     //DAG is minimized as much as possibly, and ideally should

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index 53b307d196b7ba0ac139a09b053c1038b0efb677..05d970ecc0d56228d642dbba9c509f9cb0601806 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
@@ -209,9 +209,9 @@ namespace simplifier
     //    then we can replace that node by its fixed bits.
     // 2) But if we assume the top node is true, then get the bits, we need to conjoin it.
 
-    // NB: This expects that the constructor was called with teh same node. Sorry.
+    // NB: This expects that the constructor was called with the same node. Sorry.
     ASTNode
-    ConstantBitPropagation::topLevelBothWays(const ASTNode& top, bool setTopToTrue)
+    ConstantBitPropagation::topLevelBothWays(const ASTNode& top, bool setTopToTrue, bool conjoinToTop)
     {
       assert(top.GetSTPMgr()->UserFlags.bitConstantProp_flag);
       assert (BOOLEAN_TYPE == top.GetType());
@@ -261,10 +261,35 @@ namespace simplifier
         {
           const FixedBits& bits = *it->second;
 
+          const ASTNode& node = (it->first);
+
+          if (false && node.GetKind() == SYMBOL && !bits.isTotallyFixed() && bits.countFixed() > 0)
+            {
+              // replace partially known variables with new variables.
+              int leastFixed = bits.leastUnfixed();
+              int mostFixed = bits.mostUnfixed();
+              const int width = node.GetValueWidth();
+
+              int new_width = mostFixed - leastFixed +1;
+              assert(new_width > 0);
+              ASTNode fresh = node.GetSTPMgr()->CreateFreshVariable(0,new_width,"STP_REPLACE");
+              ASTNode a,b;
+              if (leastFixed > 0)
+                a= node.GetSTPMgr()->CreateBVConst(bits.GetBVConst( leastFixed-1,  0), leastFixed);
+              if (mostFixed != width-1)
+                b =  node.GetSTPMgr()->CreateBVConst(bits.GetBVConst( width-1,  mostFixed+1),width-1-mostFixed);
+              if (!a.IsNull())
+                fresh = nf->CreateTerm(BVCONCAT, a.GetValueWidth() + fresh.GetValueWidth(), fresh, a);
+              if (!b.IsNull())
+                fresh = nf->CreateTerm(BVCONCAT, b.GetValueWidth() + fresh.GetValueWidth(), b, fresh);
+              assert(fresh.GetValueWidth() == node.GetValueWidth());
+              bool r = simplifier->UpdateSubstitutionMap(node, fresh);
+              assert(r);
+            }
+
           if (!bits.isTotallyFixed())
             continue;
 
-          const ASTNode& node = (it->first);
 
           // Don't constrain nodes we already know all about.
           if (node.isConstant())
@@ -279,7 +304,7 @@ namespace simplifier
           ASTNode propositionToAssert;
           ASTNode constantToReplaceWith;
           // skip the assigning and replacing.
-          bool doAssign = true;
+          bool doAssign = false;
 
             {
               // If it is already contained in the fromTo map, then it's one of the values
@@ -297,15 +322,17 @@ namespace simplifier
                       assert(r);
                       doAssign = false;
                     }
-                  else if (bits.getValue(0))
+                  else if (conjoinToTop && bits.getValue(0))
                     {
                       propositionToAssert = node;
                       constantToReplaceWith = constNode;
+                      doAssign=true;
                     }
-                  else
+                  else if (conjoinToTop)
                     {
                       propositionToAssert = nf->CreateNode(NOT, node);
                       constantToReplaceWith = constNode;
+                      doAssign=true;
                     }
                 }
               else if (node.GetType() == BITVECTOR_TYPE)
@@ -317,10 +344,11 @@ namespace simplifier
                       assert(r);
                       doAssign = false;
                     }
-                  else
+                  else if (conjoinToTop)
                     {
                       propositionToAssert = nf->CreateNode(EQ, node, constNode);
                       constantToReplaceWith = constNode;
+                      doAssign=true;
                     }
                 }
               else
@@ -337,6 +365,7 @@ namespace simplifier
 
               fromTo.insert(make_pair(node, constantToReplaceWith));
               toConjoin.push_back(propositionToAssert);
+              assert(conjoinToTop);
             }
         }
 

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.h b/src/simplifier/constantBitP/ConstantBitPropagation.h
index 0bdb5b0289a699187d3e401dde61f0627fffb988..6159c80d3a57be112b955f13643a254bdca436ef 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitPropagation.h
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.h
@@ -73,7 +73,7 @@ public:
 
       // Returns the node after writing in simplifications from constant Bit propagation.
       BEEV::ASTNode
-      topLevelBothWays(const ASTNode& top, bool setTopToTrue = true);
+      topLevelBothWays(const ASTNode& top, bool setTopToTrue = true, bool conjoinToTop=true);
 
 
       void clearTables()

diff --git a/src/simplifier/constantBitP/FixedBits.h b/src/simplifier/constantBitP/FixedBits.h
index 859a7154b5f763acd6bc832d6edf9caf749f72c5..5b7c4bf9a5779cd3e4fe56fa7ffa7454f64f187a 100644 (file)
--- a/src/simplifier/constantBitP/FixedBits.h
+++ b/src/simplifier/constantBitP/FixedBits.h
@@ -145,7 +145,7 @@ namespace simplifier
 
       //Returns the position of the first non-fixed value.
       int
-      leastUnfixed()
+      leastUnfixed() const
       {
         int i = 0;
         for (; i < getWidth(); i++)
@@ -156,6 +156,18 @@ namespace simplifier
         return i;
       }
 
+      int
+      mostUnfixed() const
+      {
+        int i = getWidth()-1;
+        for (; i >=0; i--)
+          {
+            if (!isFixed(i))
+              break;
+          }
+        return i;
+      }
+
       // is this bit fixed to zero?
       bool
       isFixedToZero(int n) const