From 67ee8c105fdd0e2054cc1fa44bf5b1726a32e98c Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 26 Jan 2012 03:35:05 +0000
Subject: [PATCH] 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
---
 src/STPManager/STP.h |  4 +++-
 src/util/rewrite.cpp | 11 ++++++++---
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index cb52d30..b5bade0 100644
--- 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 7a16f01..d3617c2 100644
--- 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++)
         {
-- 
2.47.3