Speedup the bvsolver. Use the applySubstitutionMap function to apply the discovered...

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

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 1f24bf753b19bbd9fcbf7432db80cd63193109e4..6303505be0b65b3156a4a645578d8184218e7680 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -193,7 +193,19 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
 ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n)
 {
        ASTNodeMap cache;
-       return replace(n,*SolverMap,cache,bm->defaultNodeFactory);
+       return replace(n,*SolverMap,cache,bm->defaultNodeFactory, false);
+}
+
+ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n)
+{
+        ASTNodeMap cache;
+        return replace(n,*SolverMap,cache,bm->defaultNodeFactory, true);
+}
+
+ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
+                ASTNodeMap& cache, NodeFactory * nf)
+{
+    return replace(n,fromTo,cache,nf,false);
 }
 
 // NOTE the fromTo map is changed as we traverse downwards.
@@ -203,7 +215,7 @@ ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n)
 // will return 5, rather than y.
 
 ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
-               ASTNodeMap& cache, NodeFactory * nf)
+               ASTNodeMap& cache, NodeFactory * nf, bool stopAtArrays)
 {
 
         ASTNodeMap::const_iterator it;
@@ -217,13 +229,13 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
                        const ASTNode& r = it->second;
                        assert(r.GetIndexWidth() == n.GetIndexWidth());
                        assert(BVTypeCheck(r));
-                       ASTNode replaced = replace(r, fromTo, cache,nf);
+                       ASTNode replaced = replace(r, fromTo, cache,nf,stopAtArrays);
                        if (replaced != r)
                                fromTo[n] = replaced;
 
                        return replaced;
                }
-               ASTNode replaced = replace(it->second, fromTo, cache,nf);
+               ASTNode replaced = replace(it->second, fromTo, cache,nf,stopAtArrays);
                if (replaced != it->second)
                        fromTo[n] = replaced;
 
@@ -234,11 +246,16 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
        if (n.isConstant() || n.GetKind() == SYMBOL /*|| n.GetKind() == WRITE*/)
                return n;
 
+         if (stopAtArrays && n.GetType() == ARRAY_TYPE)
+            {
+           return n;
+            }
+
        ASTVec children;
        children.reserve(n.GetChildren().size());
        for (unsigned i = 0; i < n.GetChildren().size(); i++)
        {
-               children.push_back(replace(n[i], fromTo, cache,nf));
+               children.push_back(replace(n[i], fromTo, cache,nf,stopAtArrays));
        }
 
        // This code short-cuts if the children are the same. Nodes with the same children,

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index 834537479951ae3e89be1f712fa2dcee4c7cb919..d0aba07b379dab8b1876f3a2de002cf1c37a2538 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -122,9 +122,14 @@ public:
 
        ASTNode applySubstitutionMap(const ASTNode& n);
 
+       ASTNode applySubstitutionMapUntilArrays(const ASTNode& n);
+
        // Replace any nodes in "n" that exist in the fromTo map.
        // NB the fromTo map is changed.
        static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf);
+
+        static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf, bool stopAtArrays);
+
 };
 
 }

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 0b74b814b224949ec72b9d57f242be1a99f5de36..fa3d4cd0f2d43810a09fdcf7ca0b8ab8f0f27df9 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -741,50 +741,44 @@ namespace BEEV
         Simplifying through arrays is very expensive though. I know how to fix it, but
         don't have time. Trev.
                  */
-
 #if 1
-      ASTNode aaa =
-              (any_solved
-               && EQ == it->GetKind()) ?
-              _simp->SimplifyFormula_TopLevel(*it, false) :
-              *it;
-
+      ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->applySubstitutionMapUntilArrays(*it) : *it;
 #else
+          ASTNode aaa = *it;
 
+          if (any_solved && EQ == aaa.GetKind())
+          {
+            bool found = false;
 
-       ASTNode aaa = *it;
+            ASTNodeSet var;
+            SetofVarsSeenInTerm(aaa[0], var);
 
-       if (any_solved && EQ == aaa.GetKind())
-          {
-            bool done = false;
-            {
-                ASTNodeSet lhs;
-                SetofVarsSeenInTerm(aaa[0], lhs);
-
-                for (ASTNodeSet::const_iterator it = lhs.begin(); it != lhs.end(); it++)
-                  if (_simp->CheckSubstitutionMap(*it))
-                    {
-                      aaa = _simp->applySubstitutionMap(aaa);
-                      done = true;
-                      break;
-                    }
+            for (ASTNodeSet::const_iterator it = var.begin(); it != var.end(); it++)
+            if (_simp->CheckSubstitutionMap(*it))
+              {
+                found = true;
+                break;
               }
-            if (!done)
+
+            if (!found)
               {
-                ASTNodeSet rhs;
-                SetofVarsSeenInTerm(aaa[1], rhs);
-
-                for (ASTNodeSet::const_iterator it = rhs.begin(); it != rhs.end(); it++)
-                  if (_simp->CheckSubstitutionMap(*it))
-                    {
-                      aaa = _simp->applySubstitutionMap(aaa);
-                      done = true;
-                      break;
-                    }
+                var.clear();
+                SetofVarsSeenInTerm(aaa[1], var);
+
+                for (ASTNodeSet::const_iterator it = var.begin(); it != var.end(); it++)
+                if (_simp->CheckSubstitutionMap(*it))
+                  {
+                    found = true;
+                    break;
+                  }
               }
+            if (found)
+              aaa = _simp->applySubstitutionMapUntilArrays(aaa);
           }
+
 #endif
 
+
         //_bm->ASTNodeStats("Printing after calling simplifyformula
         //inside the solver:", aaa);
         aaa = BVSolve_Odd(aaa);
@@ -804,7 +798,9 @@ namespace BEEV
               }
           }
         if (ASTTrue == aaa)
-               any_solved=true;
+               {
+                    any_solved=true;
+               }
       }
 
     ASTNode evens;
@@ -833,6 +829,10 @@ namespace BEEV
 
     output = solveForAndOfXOR(output);
 
+    // Imagine in the last conjunct A is replaced by B. But there could
+    // be variable A's in the first conjunct. This gets rid of 'em.
+    output = _simp->applySubstitutionMapUntilArrays(output);
+
     UpdateAlreadySolvedMap(_input, output);
     _bm->GetRunTimes()->stop(RunTimes::BVSolver);
     return output;

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 7f7f746d2a1ee44a453c202f9a59b1f13b3eddf9..1e895c178c228806715f99522336730baf057cce 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -155,6 +155,12 @@ namespace BEEV
        return substitutionMap.applySubstitutionMap(n);
   }
 
+  ASTNode Simplifier::applySubstitutionMapUntilArrays(const ASTNode& n)
+  {
+        return substitutionMap.applySubstitutionMapUntilArrays(n);
+  }
+
+
   bool Simplifier::CheckSubstitutionMap(const ASTNode& key)
   {
          return substitutionMap.CheckSubstitutionMap(key);
@@ -1719,7 +1725,7 @@ namespace BEEV
                        else
                                output = actualInputterm;
 
-                       inputterm = output;
+                       inputterm = output;
                }
 
                const ASTVec& children = inputterm.GetChildren();
@@ -2863,12 +2869,13 @@ namespace BEEV
     //memoize
     UpdateSimplifyMap(inputterm, output, false, VarConstMap);
     UpdateSimplifyMap(actualInputterm, output, false, VarConstMap);
+
     //cerr << "SimplifyTerm: output" << output << endl;
     // CheckSimplifyInvariant(inputterm,output);
 
-       assert(!output.IsNull());
-       assert(inputterm.GetValueWidth() == output.GetValueWidth());
-       assert(inputterm.GetIndexWidth() == output.GetIndexWidth());
+    assert(!output.IsNull());
+    assert(inputterm.GetValueWidth() == output.GetValueWidth());
+    assert(inputterm.GetIndexWidth() == output.GetIndexWidth());
 
     return output;
   } //end of SimplifyTerm()

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 5731f38d4c72202f7138e32527a7f0e3ca99c201..09703753b50672e01c3c9a85f09f734d8220dffb 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -116,6 +116,7 @@ namespace BEEV
     bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1);
 
     ASTNode applySubstitutionMap(const ASTNode& n);
+    ASTNode applySubstitutionMapUntilArrays(const ASTNode& n);
 
     void ResetSimplifyMaps(void);