From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 9 Feb 2012 03:46:58 +0000 (+0000)
Subject: Turn on bit-blast equivalency detection again.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=02db7e34725c701701bf760c236be5193865a87b;p=francis%2Fstp.git

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 e6c0e02..c0855e8 100644
--- 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;