Improvement. Write the equivalences that the bit-blaster discovers through transitively.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index c0855e8cb5825341832a9cd58859153f9658e4da..c8038111757fdaebe4572a0c6797ff769eb86681 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -120,12 +120,11 @@ namespace BEEV {
             /* These nodes have equivalent AIG representations, so even though they have different
              * word level expressions they are identical semantically. So we pick one of the ASTnodes
              * and replace the others with it.
-             * TODO: Isn't applied transitively because it infinite loops.
              * TODO: I replace with the lower id node, sometimes though we replace with much more
              * difficult looking ASTNodes.
             */
             ASTNodeMap cache;
-            simplified_solved_InputToSAT = SubstitutionMap::simple_replace(simplified_solved_InputToSAT, equivs, cache,&nf);
+            simplified_solved_InputToSAT = SubstitutionMap::replace(simplified_solved_InputToSAT, equivs, cache,&nf,false,true);
             bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT);
           }
 

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 84e4b909571f91b1759e4992199516d41d9768de..6d27bc9a3cd879b263f0598a4c85f8435101f83e 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -62,13 +62,13 @@ ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n)
 {
        bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions);
        ASTNodeMap cache;
-       ASTNode result =  replace(n,*SolverMap,cache,nf, false);
+       ASTNode result =  replace(n,*SolverMap,cache,nf, false,false);
 
        // NB. This is an expensive check. Remove it after it's been idempotent
        // for a while.
         #ifndef NDEBUG
               cache.clear();
-              assert( result ==  replace(result,*SolverMap,cache,nf, false));
+              assert( result ==  replace(result,*SolverMap,cache,nf, false,false));
         #endif
 
        bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions);
@@ -80,7 +80,7 @@ ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n)
 {
        bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions);
        ASTNodeMap cache;
-       ASTNode result = replace(n,*SolverMap,cache,nf, true);
+       ASTNode result = replace(n,*SolverMap,cache,nf, true,false);
        bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions);
        return result;
 }
@@ -88,7 +88,7 @@ ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n)
 ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
                 ASTNodeMap& cache, NodeFactory * nf)
 {
-    return replace(n,fromTo,cache,nf,false);
+    return replace(n,fromTo,cache,nf,false,false);
 }
 
 // NOTE the fromTo map is changed as we traverse downwards.
@@ -101,7 +101,7 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
 // It's optimised for the symbol to something case.
 
 ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
-               ASTNodeMap& cache, NodeFactory * nf, bool stopAtArrays)
+               ASTNodeMap& cache, NodeFactory * nf, bool stopAtArrays , bool preventInfinite)
 {
     const Kind k = n.GetKind();
        if (k == BVCONST || k == TRUE || k == FALSE)
@@ -116,7 +116,7 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
        {
                const ASTNode& r = it->second;
                assert(r.GetIndexWidth() == n.GetIndexWidth());
-               ASTNode replaced = replace(r, fromTo, cache,nf,stopAtArrays);
+               ASTNode replaced = replace(r, fromTo, cache,nf,stopAtArrays,preventInfinite);
                if (replaced != r)
                        fromTo[n] = replaced;
 
@@ -142,7 +142,7 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
 
        for (ASTVec::const_iterator it = children.begin(); it != children.end(); it++)
        {
-               new_children.push_back(replace(*it, fromTo, cache,nf,stopAtArrays));
+               new_children.push_back(replace(*it, fromTo, cache,nf,stopAtArrays,preventInfinite));
        }
 
        assert(new_children.size() == children.size());
@@ -175,11 +175,22 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
        // I hope that this makes it idempotent.
 
        if (fromTo.find(result) != fromTo.end())
-         result = replace(result, fromTo, cache,nf,stopAtArrays);
+         {
+         // map n->result, if running replace() on result gives us 'n', it will not infinite loop.
+         // This is only currently required for the bitblast equivalence stuff.
+           if (preventInfinite)
+             cache.insert(make_pair(n,result));
+
+         result = replace(result, fromTo, cache,nf,stopAtArrays,preventInfinite);
+         }
 
        assert(result.GetValueWidth() == valueWidth);
        assert(result.GetIndexWidth() == indexWidth);
 
+       // If there is already an "n" element in the cache, the maps semantics are to ignore the next insertion.
+       if (preventInfinite)
+         cache.erase(n);
+
        cache.insert(make_pair(n,result));
        return result;
 }
@@ -310,79 +321,4 @@ bool SubstitutionMap::loops(const ASTNode& n0, const ASTNode& n1)
 
        return (loops);
        }
-
-ASTNode
-SubstitutionMap::simple_replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory * nf)
-{
-  const Kind k = n.GetKind();
-  if (k == BVCONST || k == TRUE || k == FALSE)
-    return n;
-
-  ASTNodeMap::const_iterator it;
-
-  if ((it = cache.find(n)) != cache.end())
-    return it->second;
-
-  if ((it = fromTo.find(n)) != fromTo.end())
-    {
-      const ASTNode& r = it->second;
-      assert(r.GetIndexWidth() == n.GetIndexWidth());
-      cache.insert(make_pair(n, r));
-      return r;
-    }
-
-  // These can't be created like regular nodes are
-  if (k == SYMBOL)
-    return n;
-
-  const unsigned int indexWidth = n.GetIndexWidth();
-
-  const ASTVec& children = n.GetChildren();
-  assert(children.size() > 0);
-  // Should have no leaves left here.
-
-  ASTVec new_children;
-  new_children.reserve(children.size());
-
-  for (ASTVec::const_iterator it = children.begin(); it != children.end(); it++)
-    {
-      new_children.push_back(simple_replace(*it, fromTo, cache, nf));
-    }
-
-  assert(new_children.size() == children.size());
-
-  // This code short-cuts if the children are the same. Nodes with the same children,
-  // won't have necessarily given the same node if the simplifyingNodeFactory is enabled
-  // now, but wasn't enabled when the node was created. Shortcutting saves lots of time.
-  if (new_children == children)
-    {
-      cache.insert(make_pair(n, n));
-      return n;
-    }
-
-  ASTNode result;
-  const unsigned int valueWidth = n.GetValueWidth();
-
-  if (valueWidth == 0) // n.GetType() == BOOLEAN_TYPE
-    {
-      result = nf->CreateNode(k, new_children);
-    }
-  else
-    {
-      // If the index and value width aren't saved, they are reset sometimes (??)
-      result = nf->CreateArrayTerm(k, indexWidth, valueWidth, new_children);
-    }
-
-  // We may have created something that should be mapped. For instance,
-  // if n is READ(A, x), and the fromTo is: {x==0, READ(A,0) == 1}, then
-  // by here the result will be READ(A,0). Which needs to be mapped again..
-  // I hope that this makes it idempotent.
-
-  assert(result.GetValueWidth() == valueWidth);
-  assert(result.GetIndexWidth() == indexWidth);
-
-  cache.insert(make_pair(n, result));
-  return result;
-}
-
 };

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index 08138d3e260de0cf19f1801faffbf10b27778999..60b08f2c184ffc48541c6570e3073a0a61eddfb7 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -201,9 +201,8 @@ public:
 
        // Replace any nodes in "n" that exist in the fromTo map.
        // NB the fromTo map is changed.
-        static ASTNode simple_replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf);
        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);
+       static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf, bool stopAtArrays, bool preventInfiniteLoops);
 
 
 };