Improvement. Don't clean up the advanced CNF generator after it's been called >1...

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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 5034c39caa1e780a9eaa749d1281e3d836c0f38e..bfbab6603c85017fa127b27b61691dd35b0df5a1 100644 (file)
--- 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 d5e127d3871d2ac2bba81c84be2500af0f373223..48c7b2fc5e5fd45cd93007e9271453e47a20b082 100644 (file)
--- 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 550163a04dc67d561caaa2a137a4a75c3366b49a..62d5c9843e44efad2fff15532804b4943e3ae8d0 100644 (file)
--- 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 5a795cb154bff0e1c48febbef81f1266192a7fe2..8e1fbff6d0d0801143fc9208b1475dafff6d4f83 100644 (file)
--- 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)