Improvement. Use AIGs to find semantically equivalent but syntactically distinct...

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index e14d99e75620842915adb824b9c76f4f731aeb62..fabb50a41c103b1e3172f3d77f3c89e577212603 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -119,11 +119,20 @@ 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: Currently only for booleans,
              * 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.
             */
+#if 0
+            ASTNodeMap::iterator it = equivs.begin();
+            while (it!=equivs.end())
+              {
+                cerr << it->first.GetNodeNum() << " " << it->second.GetNodeNum() << endl;
+                 cerr << it->first << endl;
+                cerr << it->second << endl;
+                it++;
+              }
+#endif
             ASTNodeMap cache;
             simplified_solved_InputToSAT = SubstitutionMap::simple_replace(simplified_solved_InputToSAT, fromTo, cache,&nf);
             bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT);

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index c5cbd1835aa98507c35fe862a32f0cf25c3b24e7..dc872e75edabccc3af2b86a70f3f9095ca3a7a39 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -55,7 +55,41 @@ namespace BEEV
 
   const bool conjoin_to_top = true;
 
+
+  template<class BBNode>
+  class BBVecHasher
+  {
+  public:
+    size_t operator()(const vector<BBNode>& n) const
+    {
+      int hash =0;
+      for (int i=0; i <  std::min(n.size(),(size_t)6); i++)
+        hash += n[i].GetNodeNum();
+       return hash;
+    }
+  };
+
+  template<class BBNode>
+  class BBVecEquals
+  {
+  public:
+    bool operator()(const vector<BBNode>& n0, const vector<BBNode>& n1) const
+    {
+      if (n0.size() != n1.size())
+        return false;
+
+      for (int i=0; i <  n0.size(); i++)
+        {
+          if (!(n0[i] == n1[i]))
+            return false;
+        }
+      return true;
+    }
+  };
+
+
 // Look through the maps to see what the bitblaster has discovered (if anything) is constant.
+// then looks through for AIGS that are mapped to from different ASTNodes.
   template<class BBNode, class BBNodeManagerT>
     void
     BitBlaster<BBNode, BBNodeManagerT>::getConsts(const ASTNode& form, ASTNodeMap& fromTo, ASTNodeMap& equivs)
@@ -130,7 +164,6 @@ namespace BEEV
           simp->UpdateSubstitutionMap(n, r);
         else
           fromTo.insert(make_pair(n, r));
-
         }
 
       if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv","0"))
@@ -167,8 +200,53 @@ namespace BEEV
             }
           }
       }
+
+      typedef HASHMAP<vector<BBNode>, ASTNode,BBVecHasher <BBNode>, BBVecEquals<BBNode> > M;
+      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv", "0"))
+        {
+          M lookup;
+          typename std::map<ASTNode, vector<BBNode> >::iterator it;
+          for (it = BBTermMemo.begin(); it != BBTermMemo.end(); it++)
+            {
+              const ASTNode& n = it->first;
+              if (n.isConstant())
+                continue;
+
+              const vector<BBNode>& x = it->second;
+
+              bool constNode = true;
+              for (int i = 0; i < (int) x.size(); i++)
+                {
+                  if (x[i] != BBTrue && x[i] != BBFalse)
+                    {
+                      constNode = false;
+                      break;
+                    }
+                }
+              if (!constNode)
+                continue;
+
+              if (lookup.find(x) == lookup.end())
+                {
+                  lookup.insert(make_pair(x, n));
+                }
+              else
+                {
+                  const ASTNode other = (lookup.find(x))->second;
+                  std::pair<ASTNode, ASTNode> p;
+                  if (other.GetNodeNum() > n.GetNodeNum())
+                    p = make_pair(other, n);
+                  else
+                    p = make_pair(n, other);
+
+                  cerr << "EQUIV";
+                  equivs.insert(p);
+                }
+            }
+        }
     }
 
+
   template<class BBNode, class BBNodeManagerT>
     void
     BitBlaster<BBNode, BBNodeManagerT>::commonCheck(const ASTNode& n)