From cbba675854f129dd6a81511ba5035b34e256afb4 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 26 Jan 2012 09:09:34 +0000
Subject: [PATCH] Improvement. Don't clean up the advanced CNF generator after
 it's been called >1 time. This makes solving a stream of 2000 easy problems
 twice as fast.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1527 e59a4935-1847-0410-ae03-e826735625c1
---
 src/c_interface/c_interface.cpp |  3 +++
 src/main/main.cpp               |  2 ++
 src/to-sat/AIG/ToSATAIG.cpp     | 16 +++++++++++++---
 src/to-sat/AIG/ToSATAIG.h       |  2 ++
 4 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 5034c39..bfbab66 100644
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -13,6 +13,7 @@
 #include "fdstream.h"
 #include "../printer/printers.h"
 #include "../cpp_interface/cpp_interface.h"
+#include "../extlib-abc/cnf_short.h"
 
 //These typedefs lower the effort of using the keyboard to type (too
 //many overloaded meanings of the word type)
@@ -1705,6 +1706,8 @@ void vc_Destroy(VC vc) {
     persist.clear();
   }
 
+  Cnf_ClearMemory();
+
   delete decls;
   delete (stpstar)vc;
   BEEV::GlobalSTP = NULL;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index d5e127d..48c7b2f 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -17,6 +17,7 @@
 #include "../cpp_interface/cpp_interface.h"
 #include <sys/time.h>
 #include <memory>
+#include "../extlib-abc/cnf_short.h"
 
 
 #ifdef EXT_HASH_MAP
@@ -555,6 +556,7 @@ int main(int argc, char ** argv) {
   delete GlobalSTP;
   delete ParserBM;
 
+  Cnf_ClearMemory();
 
   return 0;
 }//end of Main
diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index 550163a..62d5c98 100644
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -5,6 +5,8 @@
 namespace BEEV
 {
 
+    int ToSATAIG::cnf_calls=0;
+
     bool
     ToSATAIG::CallSAT(SATSolver& satSolver, const ASTNode& input, bool needAbsRef)
     {
@@ -107,9 +109,17 @@ namespace BEEV
       if (bm->UserFlags.output_bench_flag)
         cerr << "Converting to CNF via ABC's AIG package can't yet print out bench format" << endl;
 
-	  Cnf_ClearMemory();
-	  Cnf_DataFree(cnfData);
-	  cnfData = NULL;
+
+      // This releases the memory used by the CNF generator, particularly some data tables.
+      // If CNF generation is going to be called lots, we'd rather keep it around.
+      // because the datatables are expensive to generate.
+       if (cnf_calls != 0)
+           Cnf_ClearMemory();
+
+       cnf_calls++;
+
+        Cnf_DataFree(cnfData);
+        cnfData = NULL;
 
 	// Minisat doesn't, but simplifying minisat and cryptominsat eliminate variables during their
         // simplification phases. The problem is that we may later add clauses in that refer to those
diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h
index 5a795cb..8e1fbff 100644
--- a/src/to-sat/AIG/ToSATAIG.h
+++ b/src/to-sat/AIG/ToSATAIG.h
@@ -47,6 +47,8 @@ namespace BEEV
         arrayTransformer = NULL;
     }
 
+    static int cnf_calls;
+
   public:
 
     void setArrayTransformer(ArrayTransformer *at)
-- 
2.47.3