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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 58a1c39f73400153b5844871256a4a3d0deef4bd..cde63ae0f70bf9fbaca595a1b2ad960a36fbf86b 100644 (file)
--- 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 003ec8167ffd27a5194b7ee580e57c7c512c00e9..7d0452d95b802efd0cabd8454de334a31ae6072a 100644 (file)
--- 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 8e1fbff6d0d0801143fc9208b1475dafff6d4f83..36fd5bdaab86ab0a92b759eb6bfcd43afa2b6dbb 100644 (file)
--- 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 142afe158a57612ec8ad75ea4ec5be0f62d11a0c..090a518ad5c3632e4b47d82b77eee579c819fc8a 100644 (file)
--- 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);