From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 16 Jun 2010 03:51:37 +0000 (+0000)
Subject: Speedup. When printing out the counter example, don't call the toplevel print (which... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8a8d71243658adc1f715748494850477425ac29a;p=francis%2Fstp.git

Speedup. When printing out the counter example, don't call the toplevel print (which does lots of extra work). Instead call the low level print.



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 73acbe6..da96c91 100644
--- 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 cd66294..da15251 100644
--- 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,