Fix the rewrite generator to compile.

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

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index cb52d30aae4e70591a31593dfe54143044c89c4a..b5bade0f4e6f4f044fca9129e3df775664fc0f16 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -26,7 +26,7 @@ namespace BEEV
   class STP  : boost::noncopyable
   {
 
-    ArrayTransformer * arrayTransformer;
+    
 
           ASTNode sizeReducing(ASTNode input, BVSolver* bvSolver, PropagateEqualities *pe);
 
@@ -48,6 +48,8 @@ namespace BEEV
 
 
   public:
+ArrayTransformer * arrayTransformer;
+    
           // calls sizeReducing and the bitblasting simplification.
           ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe, const int initial_difficulty_score);
 

diff --git a/src/util/rewrite.cpp b/src/util/rewrite.cpp
index 7a16f01234f2e88d7f4d48409fb82b0c6a1c6573..d3617c26cc411ef98842b03d784dd7a57f246efe 100644 (file)
--- a/src/util/rewrite.cpp
+++ b/src/util/rewrite.cpp
@@ -15,11 +15,13 @@
 #include "../to-sat/AIG/ToSATAIG.h"
 #include "../sat/MinisatCore.h"
 #include "../STPManager/STP.h"
-#include "../simplifier/BigRewriter.h"
+
 
 using namespace std;
 using namespace BEEV;
 
+bool finished = false;
+
 extern int
 smtparse(void*);
 extern FILE *smtin;
@@ -426,7 +428,7 @@ startup()
   mgr->UserFlags.stats_flag = false;
   mgr->UserFlags.optimize_flag = true;
 
-  ss = new MinisatCore<Minisat::Solver>();
+  ss = new MinisatCore<Minisat::Solver>(finished);
 
   // Prime the cache with 100..
   for (int i = 0; i < 100; i++)
@@ -449,7 +451,7 @@ void
 clearSAT()
 {
   delete ss;
-  ss = new MinisatCore<Minisat::Solver>();
+  ss = new MinisatCore<Minisat::Solver>(finished);
 }
 
 // Return true if the negation of the query is unsatisfiable.
@@ -971,6 +973,7 @@ main(void)
 
     {
       SimplifyingNodeFactory nf(*(mgr->hashingNodeFactory), *mgr);
+#if 0
       BEEV::BigRewriter b;
 
       for (int i = 0; i < functions.size(); i++)
@@ -984,8 +987,10 @@ main(void)
             }
 
         }
+#endif
       removeDuplicates(functions);
 
+
       // There may be a single undefined element now.. remove it.
       for (int i = 0; i < functions.size(); i++)
         {