Improvements.

* Add a function to update the substitution map that avoids the expensive checks. This is used by unconstrained variable elimination.
* use a --config flag to enable the xor solver.
* Update the dependencies with functions for unconstrained elimination.

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

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index 014bec502abb2066437cf66ae2ab2d954d2309f0..5c2bac1912721727619cb0e9b1bb843162b20bbe 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -112,6 +112,18 @@ public:
                        return false;
        }
 
+       // It's depressingly expensive to perform all of the loop checks etc.
+       // If you use this function you are promising:
+       // 1) That UpdateSubstitutionMap(e0,e1) would have returned true.
+       // 2) That all of the substitutions will be written in fully before other code
+        bool UpdateSubstitutionMapFewChecks(const ASTNode& e0, const ASTNode& e1)
+        {
+          assert(e0.GetKind() == SYMBOL);
+          assert (!CheckSubstitutionMap(e0));
+          (*SolverMap)[e0] = e1;
+          return true;
+        }
+
        // The substitutionMap will be updated, given x <-> f(w,z,y), iff,
        // 1) x doesn't appear in the rhs.
        // 2) x hasn't already been stored in the substitution map.

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 44afb80859e2c81d2935f0681f0a85cc846fa94e..56e2dabd3a412e75ff0bfeb01b98708eb5238d42 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -541,7 +541,7 @@ namespace BEEV
   // to do. Flatten the XOR.
   ASTNode BVSolver::solveForXOR(const ASTNode& xorNode)
   {
-    assert(_bm->UserFlags.solve_for_XORS_flag);
+    assert(_bm->UserFlags.isSet("xor-solve","1"));
 
     if (xorNode.GetKind() != XOR)
       {
@@ -628,7 +628,7 @@ namespace BEEV
    ASTNode
   BVSolver::solveForAndOfXOR(const ASTNode& n)
   {
-    assert(_bm->UserFlags.solve_for_XORS_flag);
+    assert(_bm->UserFlags.isSet("xor-solve","1"));
 
     if (n.GetKind() != AND)
       return n;
@@ -670,7 +670,7 @@ namespace BEEV
       }
 
     Kind k = input.GetKind();
-    if (XOR ==k && _bm->UserFlags.solve_for_XORS_flag)
+    if (XOR ==k && _bm->UserFlags.isSet("xor-solve","1"))
     {
        ASTNode output = solveForXOR(_input);
        UpdateAlreadySolvedMap(_input, output);
@@ -787,7 +787,7 @@ namespace BEEV
     if (evens != ASTTrue)
       output = _bm->CreateNode(AND, output, evens);
 
-    if (_bm->UserFlags.solve_for_XORS_flag)
+    if (_bm->UserFlags.isSet("xor-solve","1"))
       output = solveForAndOfXOR(output);
 
     // Imagine in the last conjunct A is replaced by B. But there could

diff --git a/src/simplifier/constantBitP/Dependencies.h b/src/simplifier/constantBitP/Dependencies.h
index f636e9afd53083bbec594f58a57f928dd38d9295..2ec2c06b312f8c1ebc14cd3abdb5168d5c1156ce 100644 (file)
--- a/src/simplifier/constantBitP/Dependencies.h
+++ b/src/simplifier/constantBitP/Dependencies.h
@@ -20,6 +20,7 @@ namespace simplifier
 
       const set<ASTNode> empty;
 
+    public:
       // All the nodes that depend on the value of a particular node.
       void
       build(const ASTNode & current, const ASTNode & prior)
@@ -75,6 +76,18 @@ namespace simplifier
           }
       }
 
+      void replaceFresh(const ASTNode& old, const ASTNode& newN, set<ASTNode> *newNDepends,
+                        ASTVec& variables)
+      {
+        NodeToDependentNodeMap::const_iterator it = dependents.find(old);
+        if (it == dependents.end())
+          return;
+
+        it->second->erase(old);
+        dependents.insert(make_pair(newN,newNDepends));
+        variables.push_back(newN);
+      }
+
       // The "toRemove" node is being removed. Used by unconstrained elimination.
       void removeNode(const ASTNode& toRemove, ASTVec& variables)
       {
@@ -147,6 +160,17 @@ namespace simplifier
         return s->count(higher) > 0;
       }
 
+      bool isUnconstrained(const ASTNode& n)
+      {
+        if (n.GetKind() != SYMBOL)
+          return false;
+
+        NodeToDependentNodeMap::const_iterator it = dependents.find(n);
+        assert(it != dependents.end());
+        return it->second->size() ==1;
+      }
+
+#if 0
       void
       getAllVariables(ASTVec& v)
       {
@@ -156,6 +180,7 @@ namespace simplifier
               v.push_back(it->first);
           }
       }
+#endif
 
     };
 

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index be85f9513ceded8d7bf17f654d6d1b9f0cf3cb9c..87b6b450c0f5df06fea36d32338e2f0126d42c43 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -151,6 +151,10 @@ namespace BEEV
   {
          return substitutionMap.CheckSubstitutionMap(key);
   }
+  bool Simplifier::UpdateSubstitutionMapFewChecks(const ASTNode& e0, const ASTNode& e1)
+  {
+          return substitutionMap.UpdateSubstitutionMapFewChecks(e0,e1);
+  }
 
   bool Simplifier::UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1)
   {
@@ -609,6 +613,9 @@ namespace BEEV
 
     const unsigned len = left.GetValueWidth();
 
+    if(_bm->UserFlags.isSet("inequality-simplifications","1"))
+    {
+
     const int constStart = std::min(mostSignificantConstants(left),mostSignificantConstants(right));
     int comparator =0;
 
@@ -633,56 +640,54 @@ namespace BEEV
        return pushNeg ?  nf->CreateNode(NOT, status) : status;
     }
 
-    if (comparator!=0 && (k == BVSGT || k == BVSGE))
-    {
-       // one is bigger than the other.
-               int sign_a = getConstantBit(left, 0);
-               int sign_b = getConstantBit(right, 0);
-               if (sign_a < sign_b)
-               {
-                       comparator =1; // a > b.
-               }
-               if (sign_a > sign_b)
-                       comparator =-1;
+    if (comparator != 0 && (k == BVSGT || k == BVSGE))
+          {
+            // one is bigger than the other.
+            int sign_a = getConstantBit(left, 0);
+            int sign_b = getConstantBit(right, 0);
+            if (sign_a < sign_b)
+              {
+                comparator = 1; // a > b.
+              }
+            if (sign_a > sign_b)
+              comparator = -1;
 
-       ASTNode status = (comparator ==1)? ASTTrue: ASTFalse;
-       return pushNeg ?  nf->CreateNode(NOT, status) : status;
-    }
+            ASTNode status = (comparator == 1) ? ASTTrue : ASTFalse;
+            return pushNeg ? nf->CreateNode(NOT, status) : status;
+          }
 
-    {
-               ASTNodeSet visited0, visited1;
-               vector<ASTNode> l0,l1;
+          {
+            ASTNodeSet visited0, visited1;
+            vector<ASTNode> l0, l1;
 
-               // Sound overapproximation. Doesn't consider the equalities.
-               if (getPossibleValues(left, visited0, l0) && getPossibleValues(right,visited1, l1))
-               {
-                       {
-                               bool (*comp)(const ASTNode&, const ASTNode&);
-                               if (k == BVSGT || k == BVSGE)
-                                       comp = signedGreaterThan;
-                               else
-                                       comp = unsignedGreaterThan;
-                               {
-                                       ASTNode minLHS = *max_element(l0.begin(), l0.end(),
-                                                       comp);
-                                       ASTNode maxRHS = *min_element(l1.begin(), l1.end(),
-                                                       comp);
-
-                                       if (comp(minLHS, maxRHS))
-                                               return pushNeg ? ASTFalse : ASTTrue;
-                               }
-                               {
-                                       ASTNode maxLHS = *min_element(l0.begin(), l0.end(),
-                                                       comp);
-                                       ASTNode minRHS = *max_element(l1.begin(), l1.end(),
-                                                       comp);
-
-                                       if (comp(minRHS, maxLHS))
-                                               return pushNeg ? ASTTrue : ASTFalse;
-                               }
-                       }
-               }
-       }
+            // Sound overapproximation. Doesn't consider the equalities.
+            if (getPossibleValues(left, visited0, l0) && getPossibleValues(right, visited1, l1))
+              {
+                  {
+                    bool
+                    (*comp)(const ASTNode&, const ASTNode&);
+                    if (k == BVSGT || k == BVSGE)
+                      comp = signedGreaterThan;
+                    else
+                      comp = unsignedGreaterThan;
+                      {
+                        ASTNode minLHS = *max_element(l0.begin(), l0.end(), comp);
+                        ASTNode maxRHS = *min_element(l1.begin(), l1.end(), comp);
+
+                        if (comp(minLHS, maxRHS))
+                          return pushNeg ? ASTFalse : ASTTrue;
+                      }
+                      {
+                        ASTNode maxLHS = *min_element(l0.begin(), l0.end(), comp);
+                        ASTNode minRHS = *max_element(l1.begin(), l1.end(), comp);
+
+                        if (comp(minRHS, maxLHS))
+                          return pushNeg ? ASTTrue : ASTFalse;
+                      }
+                  }
+              }
+          }
+      }
 
     const ASTNode unsigned_min = _bm->CreateZeroConst(len);
     const ASTNode one = _bm->CreateOneConst(len);
@@ -1784,15 +1789,15 @@ namespace BEEV
             {
               output = zero;
             }
-          else if (BVMULT == k 
-                   && 1 == nonconstkids.size() 
+          else if (BVMULT == k
+                   && 1 == nonconstkids.size()
                    && constoutput == max)
             {
               //useful special case opt: when input is BVMULT(max_const,t),
               //then output = BVUMINUS(t). this is easier on the bitblaster
-              output = 
+             output =
                 nf->CreateTerm(BVUMINUS, inputValueWidth, nonconstkids);
-            }
+           }
           else
             {
               if (0 < nonconstkids.size())

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index e85572f6164604e3d1936cfdd3491f5120a50043..0e0d640f4b36305282d5b73472c61c1c63901cb9 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -115,6 +115,7 @@ namespace BEEV
     bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output);
     bool CheckSubstitutionMap(const ASTNode& a);
     bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1);
+    bool UpdateSubstitutionMapFewChecks(const ASTNode& e0, const ASTNode& e1);
 
     ASTNode applySubstitutionMap(const ASTNode& n);
     ASTNode applySubstitutionMapUntilArrays(const ASTNode& n);