From 27feba6ada00006ae00bf6569a1b60b393acc8e5 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 7 Apr 2012 00:43:51 +0000
Subject: [PATCH] Improvement. Fix an oddity which required a method to be
 called right after construction.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1629 e59a4935-1847-0410-ae03-e826735625c1
---
 src/STPManager/STP.cpp                              |  3 +--
 .../constantBitP/ConstantBitP_MaxPrecision.cpp      |  3 +--
 src/to-sat/AIG/ToSATAIG.h                           | 13 ++++---------
 src/util/apply.cpp                                  |  3 +--
 4 files changed, 7 insertions(+), 15 deletions(-)

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 58a1c39..cde63ae 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -564,8 +564,7 @@ namespace BEEV {
           simplified_solved_InputToSAT = bm->ASTFalse;
       }
 
-    ToSATAIG toSATAIG(bm, cb);
-    toSATAIG.setArrayTransformer(arrayTransformer);
+    ToSATAIG toSATAIG(bm, cb, arrayTransformer);
 
     ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ;
 
diff --git a/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp b/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp
index 003ec81..7d0452d 100644
--- a/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp
+++ b/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp
@@ -442,8 +442,7 @@ bool maxPrecision(vector<FixedBits*> children, FixedBits& output, Kind kind, STP
         bool timeout = false;
         MinisatCore<Minisat::Solver> newS(timeout);
 
-        ToSATAIG tosat(beev);
-        tosat.setArrayTransformer(&at);
+        ToSATAIG tosat(beev,&at);
 
         SATSolver::vec_literals satSolverClause;
 
diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h
index 8e1fbff..36fd5bd 100644
--- a/src/to-sat/AIG/ToSATAIG.h
+++ b/src/to-sat/AIG/ToSATAIG.h
@@ -44,35 +44,30 @@ namespace BEEV
     {
         count = 0;
         first = true;
-        arrayTransformer = NULL;
     }
 
     static int cnf_calls;
 
   public:
-
-    void setArrayTransformer(ArrayTransformer *at)
-    {
-        arrayTransformer = at;
-    }
-
     bool cbIsDestructed()
     {
     	return cb == NULL;
     }
 
-    ToSATAIG(STPMgr * bm) :
+    ToSATAIG(STPMgr * bm , ArrayTransformer *at) :
       ToSATBase(bm), toCNF(bm->UserFlags)
     {
       cb = NULL;
       init();
+      arrayTransformer = at;
     }
 
-    ToSATAIG(STPMgr * bm, simplifier::constantBitP::ConstantBitPropagation* cb_) :
+    ToSATAIG(STPMgr * bm, simplifier::constantBitP::ConstantBitPropagation* cb_, ArrayTransformer *at ) :
     	ToSATBase(bm), cb(cb_), toCNF(bm->UserFlags)
     {
       cb = cb_;
       init();
+      arrayTransformer = at;
     }
 
     ~ToSATAIG();
diff --git a/src/util/apply.cpp b/src/util/apply.cpp
index 142afe1..090a518 100644
--- a/src/util/apply.cpp
+++ b/src/util/apply.cpp
@@ -32,8 +32,7 @@ main(int argc, char ** argv)
   Simplifier *simp = new Simplifier(mgr);
   ArrayTransformer * at = new ArrayTransformer(mgr, simp);
   AbsRefine_CounterExample* abs = new AbsRefine_CounterExample(mgr, simp, at);
-  ToSATAIG* tosat = new ToSATAIG(mgr);
-  tosat->setArrayTransformer(at);
+  ToSATAIG* tosat = new ToSATAIG(mgr,at);
 
   GlobalSTP = new STP(mgr, simp, at, tosat, abs);
 
-- 
2.47.3