Turn on bit-blast equivalency detection again.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index e6c0e02f5584f2cd88c6083ca6f221712622197d..c0855e8cb5825341832a9cd58859153f9658e4da 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -114,7 +114,7 @@ namespace BEEV {
         ASTNodeMap fromTo;
         ASTNodeMap equivs;
         bb.getConsts(simplified_solved_InputToSAT, fromTo,equivs);
-#if 0
+
         if (equivs.size() > 0)
           {
             /* These nodes have equivalent AIG representations, so even though they have different
@@ -124,22 +124,11 @@ namespace BEEV {
              * TODO: I replace with the lower id node, sometimes though we replace with much more
              * difficult looking ASTNodes.
             */
-            //cerr << "eQUIV";
-
-            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++;
-              }
-
             ASTNodeMap cache;
             simplified_solved_InputToSAT = SubstitutionMap::simple_replace(simplified_solved_InputToSAT, equivs, cache,&nf);
             bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT);
           }
-#endif
+
         if (fromTo.size() > 0)
           {
             ASTNodeMap cache;