Speedup. When printing out the counter example, don't call the toplevel print (which...

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

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 73acbe6f82803544539a4c2671566d15241efa01..da96c91e57602b0e0c30fe704e28bdea31ad7dd4 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -9,6 +9,7 @@
 
 #include "../sat/sat.h"
 #include "AbsRefine_CounterExample.h"
+#include "../printer/printers.h"
 
 const bool debug_counterexample =  false;
 
@@ -742,6 +743,11 @@ namespace BEEV
         return;
       }
 
+    bm->PLPrintNodeSet.clear();
+    bm->NodeLetVarMap.clear();
+    bm->NodeLetVarVec.clear();
+    bm->NodeLetVarMap1.clear();
+
     // Take a copy of the counterexample map, 'cause TermToConstTermUsingModel
     // changes it. Which breaks the iterator otherwise.
     const ASTNodeMap c(CounterExampleMap);
@@ -772,7 +778,7 @@ namespace BEEV
              f[1].GetKind() == BVCONST))
           {
             os << "ASSERT( ";
-            f.PL_Print(os,0);
+            printer::PL_Print1(os,f,0,false);
             if(BOOLEAN_TYPE == f.GetType()) 
               {
                 os << "<=>";
@@ -785,11 +791,11 @@ namespace BEEV
               {
                ASTNode rhs = TermToConstTermUsingModel(se, false);
                                assert(rhs.isConstant());
-               rhs.PL_Print(os, 0);
+                               printer::PL_Print1(os,rhs,0,false);
               }
             else
               {
-                se.PL_Print(os, 0);
+               printer::PL_Print1(os,se,0,false);
               }
             os << " );" << endl;
           }

diff --git a/src/printer/printers.h b/src/printer/printers.h
index cd662949668161fcc468dff743e87ebb670dda12..da15251e0aa01149f4b41cb782f01050ce606254 100644 (file)
--- a/src/printer/printers.h
+++ b/src/printer/printers.h
@@ -26,6 +26,9 @@ namespace printer
   ostream& PL_Print(ostream &os, 
                     const BEEV::ASTNode& n, int indentation=0);
 
+  void PL_Print1(ostream& os, const ASTNode& n,int indentation, bool letize);
+
+
   ostream& Lisp_Print(ostream &os, 
                       const BEEV::ASTNode& n,  int indentation=0);
   ostream& Lisp_Print_indent(ostream &os,