Use the advanced CNF generator to encode array problems into CNF. Array axioms are...

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index af1853c9a28861ddb44dd7c259c8c35a5345f5f6..acd080e472e317d341bc86b2dd7f38cb35a77702 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -49,9 +49,56 @@ namespace BEEV
     if (bm->UserFlags.stats_flag)
       printArrayStats();
 
-    runTimes->stop(RunTimes::Transforming);
 
-   return result;
+    // This establishes equalities between every indexes, and a fresh variable.
+    if (bm->UserFlags.arrayread_refinement_flag)
+    {
+               ASTNodeMap replaced;
+
+               ASTVec equalsNodes;
+               for (ArrayTransformer::ArrType::iterator
+                          iset = arrayToIndexToRead.begin(),
+                          iset_end = arrayToIndexToRead.end();
+                        iset != iset_end; iset++)
+                 {
+                               const ASTNode& ArrName = iset->first;
+                               map<ASTNode, ArrayTransformer::ArrayRead>& mapper = iset->second;
+
+                               for (map<ASTNode, ArrayTransformer::ArrayRead>::iterator it =mapper.begin() ; it != mapper.end();it++)
+                               {
+                                       const ASTNode& the_index = it->first;
+
+                                       if (the_index.isConstant() || the_index.GetKind() == SYMBOL)
+                                       {
+                                               it->second.index_symbol = the_index;
+                                       }
+                                       else if (replaced.find(the_index) != replaced.end()) // Already associated with a variable.
+                                       {
+                                               it->second.index_symbol = replaced.find(the_index)->second;
+                                       }
+                                       else
+                                       {
+                                               ASTNode newV = bm->CreateFreshVariable(0,the_index.GetValueWidth(), "STP__IndexVariables");
+                                               equalsNodes.push_back(nf->CreateNode(EQ, the_index, newV));
+                                               replaced.insert(make_pair(the_index,newV));
+                                               it->second.index_symbol = newV;
+                                       }
+                                       assert(it->second.index_symbol.GetValueWidth() == the_index.GetValueWidth());
+                               }
+                 }
+
+               runTimes->stop(RunTimes::Transforming);
+
+               if (equalsNodes.size() > 0)
+                       return nf->CreateNode(AND, result, equalsNodes);
+               else
+                       return result;
+    }
+    else
+    {
+       runTimes->stop(RunTimes::Transforming);
+       return result;
+    }
   }
 
   //Translates signed BVDIV,BVMOD and BVREM into unsigned variety

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index 12d5cebcb2c7f1a076daccd03dacb081e6a18488..93c5bb65f92b90b71b7afbc3562617582e1866ec 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -35,8 +35,9 @@ namespace BEEV
           symbol = _symbol;
         }
 
-        ASTNode ite;  // if not using refinement this will be the ITE for the read. Otherwise == symbol.
-        ASTNode symbol; // each read is allocated a distinct fresh variable.
+        ASTNode ite;     // if not using refinement this will be the ITE for the read. Otherwise == symbol.
+        ASTNode symbol;  // each read is allocated a distinct fresh variable.
+        ASTNode index_symbol;  // A symbol constrained to equal the index expression.
       };
 
       // MAP: This maps from arrays to their indexes.
@@ -57,7 +58,7 @@ namespace BEEV
     /****************************************************************
      * Private Typedefs and Data                                    *
      ****************************************************************/
-    
+
     // Handy defs
     ASTNode ASTTrue, ASTFalse, ASTUndefined;
 

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index 6a1aeaa161e3d0a76fa0356a77fbb052eabf45db..a7c6614da6514ac0496b5797c3b92decb90f80f1 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
  *
  * BEGIN DATE: November, 2005
  *
@@ -18,7 +18,136 @@ namespace BEEV
   /******************************************************************
    * Abstraction Refinement related functions
    ******************************************************************/  
-  
+
+enum Polarity {LEFT_ONLY, RIGHT_ONLY, BOTH};
+
+void getSatVariables(const ASTNode & a, vector<unsigned> & v_a, SATSolver & SatSolver, ToSATBase::ASTNodeToSATVar & satVar)
+ {
+       ToSATBase::ASTNodeToSATVar::iterator it = satVar.find(a);
+       if (it != satVar.end())
+               v_a = it->second;
+       else
+               if (!a.isConstant())
+               {
+                       assert(a.GetKind() == SYMBOL);
+                       // It was ommitted from the initial problem, so assign it freshly.
+                       for(int i = 0;i < a.GetValueWidth();i++)
+                               v_a.push_back(SatSolver.newVar());
+                       satVar.insert(make_pair(a,v_a));
+               }
+ }
+
+
+// This function adds the clauses to constrain (a=b)->c.
+// Because it's used to create array axionms (a=b)-> (c=d), it can be
+// used to only add one of the polarities..
+Minisat::Var getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, ToSATBase::ASTNodeToSATVar& satVar, Polarity polary= BOTH)
+{
+       const int width = a.GetValueWidth();
+       assert(width == b.GetValueWidth());
+       assert(!a.isConstant() || !b.isConstant());
+
+       vector<unsigned > v_a;
+       vector<unsigned > v_b;
+
+       getSatVariables(a,v_a,SatSolver,satVar);
+       getSatVariables(b,v_b,SatSolver,satVar);
+
+       // The only time v_a or v_b will be empty is if a resp. b is a constant.
+
+       if (v_a.size() == width && v_b.size() == width)
+       {
+               SATSolver::vec_literals all;
+               const int result = SatSolver.newVar();
+
+               for (int i=0; i < width; i++)
+               {
+                       SATSolver::vec_literals s;
+                       int nv0 = SatSolver.newVar();
+
+                       if (polary != RIGHT_ONLY)
+                       {
+                               s.push(SATSolver::mkLit(v_a[i], true));
+                               s.push(SATSolver::mkLit(v_b[i], true));
+                               s.push(SATSolver::mkLit(nv0, false));
+                               SatSolver.addClause(s);
+                               s.clear();
+
+                               s.push(SATSolver::mkLit(v_a[i], false));
+                               s.push(SATSolver::mkLit(v_b[i], false));
+                               s.push(SATSolver::mkLit(nv0, false));
+                               SatSolver.addClause(s);
+                               s.clear();
+                       }
+
+                       if (polary != LEFT_ONLY)
+                       {
+                               s.push(SATSolver::mkLit(v_a[i], true));
+                               s.push(SATSolver::mkLit(v_b[i], false));
+                               s.push(SATSolver::mkLit(nv0, true));
+                               SatSolver.addClause(s);
+                               s.clear();
+
+                               s.push(SATSolver::mkLit(v_a[i], false));
+                               s.push(SATSolver::mkLit(v_b[i], true));
+                               s.push(SATSolver::mkLit(nv0, true));
+                               SatSolver.addClause(s);
+                               s.clear();
+
+                               // result -> nv0 .. new.
+                               s.push(SATSolver::mkLit(result, true));
+                               s.push(SATSolver::mkLit(nv0, false));
+                               SatSolver.addClause(s);
+                               s.clear();
+                       }
+
+                       all.push(SATSolver::mkLit(nv0, true));
+               }
+               all.push(SATSolver::mkLit(result, false));
+
+               SatSolver.addClause(all);
+               return result;
+       }
+       else if (v_a.size() == 0 ^ v_b.size() ==0)
+       {
+               ASTNode constant = a.isConstant()? a:b;
+               vector<unsigned > vec  = v_a.size() == 0? v_b : v_a;
+               assert(constant.isConstant());
+               assert(vec.size() == width);
+
+               SATSolver::vec_literals all;
+               const int result = SatSolver.newVar();
+               all.push(SATSolver::mkLit(result, false));
+
+               CBV v = constant.GetBVConst();
+               for (int i=0; i < width; i++)
+               {
+                       if (CONSTANTBV::BitVector_bit_test(v,i))
+                               all.push(SATSolver::mkLit(vec[i], true));
+                       else
+                               all.push(SATSolver::mkLit(vec[i], false));
+
+                       if (polary != LEFT_ONLY)
+                       {
+                               SATSolver::vec_literals p;
+                               p.push(SATSolver::mkLit(result, true));
+                               if (CONSTANTBV::BitVector_bit_test(v,i))
+                                       p.push(SATSolver::mkLit(vec[i], false));
+                               else
+                                       p.push(SATSolver::mkLit(vec[i], true));
+
+                               SatSolver.addClause(p);
+                       }
+
+               }
+               SatSolver.addClause(all);
+               return result;
+       }else
+               FatalError("Unexpected, both must be constants..");
+
+}
+
+
   /******************************************************************
    * ARRAY READ ABSTRACTION REFINEMENT
    *   
@@ -38,6 +167,32 @@ namespace BEEV
    * it compares with other approaches (e.g., one false axiom at a
    * time or all the false axioms each time).
    *****************************************************************/
+  struct AxiomToBe
+  {
+         AxiomToBe(ASTNode i0, ASTNode i1, ASTNode v0, ASTNode v1)
+         {
+                 index0 = i0;
+                 index1 = i1;
+                 value0 = v0;
+                 value1 = v1;
+         }
+         ASTNode index0, index1;
+         ASTNode value0, value1;
+ };
+
+  void applyAxiomsToSolver(ToSATBase::ASTNodeToSATVar & satVar, vector<AxiomToBe>& toBe, SATSolver & SatSolver)
+   {
+        for(int i = 0;i < toBe.size();i++){
+           Minisat::Var a = getEquals(SatSolver, toBe[i].index0, toBe[i].index1, satVar, LEFT_ONLY);
+           Minisat::Var b = getEquals(SatSolver, toBe[i].value0, toBe[i].value1, satVar, RIGHT_ONLY);
+           SATSolver::vec_literals satSolverClause;
+           satSolverClause.push(SATSolver::mkLit(a, true));
+           satSolverClause.push(SATSolver::mkLit(b, false));
+           SatSolver.addClause(satSolverClause);
+       }
+        toBe.clear();
+   }
+
   SOLVER_RETURN_TYPE 
   AbsRefine_CounterExample::
   SATBased_ArrayReadRefinement(SATSolver& SatSolver,
@@ -45,7 +200,8 @@ namespace BEEV
                                const ASTNode& original_input,
                                ToSATBase* tosat) {
 
-       ASTVec FalseAxiomsVec, RemainingAxiomsVec;
+       vector<AxiomToBe> RemainingAxiomsVec;
+       vector<AxiomToBe> FalseAxiomsVec;
 
        // NB. Because we stop this timer before entering the SAT solver, the count
        // it produces isn't the number of times Array Read Refinement was entered.
@@ -81,6 +237,8 @@ namespace BEEV
        vector<ASTNode> concreteValues;
        concreteValues.reserve(mapper.size());
 
+       ASTVec index_symbols;
+
        for (map<ASTNode, ArrayTransformer::ArrayRead>::const_iterator it =mapper.begin() ; it != mapper.end();it++)
        {
            const ASTNode& the_index = it->first;
@@ -89,6 +247,8 @@ namespace BEEV
             ASTNode arrsym = it->second.symbol;
             read_node_symbols.push_back(arrsym);
 
+            index_symbols.push_back(it->second.index_symbol);
+
                        assert(read_node_symbols[0].GetValueWidth() == arrsym.GetValueWidth());
                        assert(listOfIndices[0].GetValueWidth() == the_index.GetValueWidth());
 
@@ -115,68 +275,49 @@ namespace BEEV
                // If the index is a constant, and different, then there's no reason to check.
                // Sometimes we get the same index stored multiple times in the array. Not sure why...
                if (BVCONST == iKind && jKind[j] == BVCONST && index_i != index_j)
-               {
                        continue;
-               }
-
-               //prepare for SAT LOOP
-                //first construct the antecedent for the LA axiom
-                ASTNode eqOfIndices = 
-                  (exprless(index_i, index_j)) ? 
-                  simp->CreateSimplifiedEQ(index_i, index_j) : 
-                  simp->CreateSimplifiedEQ(index_j, index_i);
-
-                if (ASTFalse == eqOfIndices)
-                       continue; // shortuct.
-
-                ASTNode eqOfReads = simp->CreateSimplifiedEQ(read_node_symbols[i], read_node_symbols[j]);
-                //construct appropriate Leibnitz axiom
-                ASTNode LeibnitzAxiom = 
-                  bm->CreateNode(IMPLIES, eqOfIndices, eqOfReads);
+
+                if (ASTFalse == simp->CreateSimplifiedEQ(index_i, index_j))
+                       continue; // shortcut.
+
+               AxiomToBe o (index_symbols[i],index_symbols[j],  read_node_symbols[i], read_node_symbols[j]);
+
                 if (concreteIndexes[i] == concreteIndexes[j] && concreteValues[i] != concreteValues[j])
                   {
-                    FalseAxiomsVec.push_back(LeibnitzAxiom);
-                    //cerr << "index:" << index_i << " " <<  index_j;
-                    //cerr << read_node_symbols[i];
-                    //cerr << read_node_symbols[j];
-                  }
+                       FalseAxiomsVec.push_back(o);
+                       //ToSATBase::ASTNodeToSATVar    & satVar = tosat->SATVar_to_SymbolIndexMap();
+                       //applyAxiomsToSolver(satVar, FalseAxiomsVec, SatSolver);
+                }
                 else
-                  {
-                    RemainingAxiomsVec.push_back(LeibnitzAxiom);
-                  }
+                       RemainingAxiomsVec.push_back(o);
               }
-            if (FalseAxiomsVec.size() > 0)
+            if ( FalseAxiomsVec.size() > 0)
             {
-                               ASTNode FalseAxioms =
-                                 (FalseAxiomsVec.size() > 1) ?
-                                 bm->CreateNode(AND, FalseAxiomsVec) : FalseAxiomsVec[0];
-                               bm->ASTNodeStats("adding false readaxioms to SAT: ", FalseAxioms);
-                               SOLVER_RETURN_TYPE res2;
+               ToSATBase::ASTNodeToSATVar      & satVar = tosat->SATVar_to_SymbolIndexMap();
+               applyAxiomsToSolver(satVar, FalseAxiomsVec, SatSolver);
+
+               SOLVER_RETURN_TYPE res2;
                                bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement);
                                res2 =  CallSAT_ResultCheck(SatSolver,
-                                                                         FalseAxioms,
+                                                                         ASTTrue,
                                                                          original_input,
                                                                          tosat,
                                                                          true);
-                               FalseAxiomsVec.clear();
 
                                if (SOLVER_UNDECIDED != res2)
-                                 {
                                        return res2;
-                                 }
                                bm->GetRunTimes()->start(RunTimes::ArrayReadRefinement);
             }
           }
       }
+
     if (RemainingAxiomsVec.size() > 0)
     {
-               ASTNode RemainingAxioms =
-                               (RemainingAxiomsVec.size() > 1) ? bm->CreateNode(AND,
-                                               RemainingAxiomsVec) : RemainingAxiomsVec[0];
-               bm->ASTNodeStats("adding remaining readaxioms to SAT: ",
-                               RemainingAxioms);
+       ToSATBase::ASTNodeToSATVar      & satVar = tosat->SATVar_to_SymbolIndexMap();
+       applyAxiomsToSolver(satVar, RemainingAxiomsVec, SatSolver);
+
                bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement);
-               return CallSAT_ResultCheck(SatSolver, RemainingAxioms, original_input,
+               return CallSAT_ResultCheck(SatSolver, ASTTrue, original_input,
                                tosat,true);
        }
 

diff --git a/src/to-sat/AIG/ToCNFAIG.cpp b/src/to-sat/AIG/ToCNFAIG.cpp
index 60d08c2168f3a29ad950deb3b8b7e2597fb4ac76..0a845bf19fb5cf5be8c909a003239f5714da1f13 100644 (file)
--- a/src/to-sat/AIG/ToCNFAIG.cpp
+++ b/src/to-sat/AIG/ToCNFAIG.cpp
@@ -1,10 +1,9 @@
 #include "ToCNFAIG.h"
 
+
 namespace BEEV
 {
 
-
-
 // Can it only add in the new variables somehow??
 void addVariables(BBNodeManagerAIG& mgr, Cnf_Dat_t*& cnfData , ToSATBase::ASTNodeToSATVar& nodeToVar)
 {
@@ -29,21 +28,6 @@ void addVariables(BBNodeManagerAIG& mgr, Cnf_Dat_t*& cnfData , ToSATBase::ASTNod
                }
                nodeToVar.insert(make_pair(n, v));
        }
-
-}
-
-
-// When we need abstraction refinement.
-void ToCNFAIG::toCNF_renter(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
-               ToSATBase::ASTNodeToSATVar& nodeToVar, BBNodeManagerAIG& mgr) {
-       assert(priorCnfData != NULL);
-       Aig_ObjCreatePo(mgr.aigMgr, top.n); // A new PO.
-
-       cnfData = Cnf_DeriveSimple_Additional(mgr.aigMgr, priorCnfData);
-       Cnf_DataFree(priorCnfData);
-       priorCnfData = cnfData;
-
-       addVariables( mgr,  cnfData , nodeToVar);
 }
 
 void ToCNFAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
@@ -97,16 +81,17 @@ void ToCNFAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
 
                        if (nodeCount == mgr.aigMgr->nObjs[AIG_OBJ_AND])
                                break;
+
                }
        }
-       if (!needAbsRef &&  !uf.isSet("simple-cnf","0")) {
+       if (!uf.isSet("simple-cnf","0")) {
                cnfData = Cnf_Derive(mgr.aigMgr, 0);
                if (uf.stats_flag)
                  cerr << "advanced CNF" << endl;
        } else {
                cnfData = Cnf_DeriveSimple(mgr.aigMgr, 0);
                 if (uf.stats_flag)
-                  cerr << "simple CNF" << endl;
+                       cerr << "simple CNF" << endl;
 
        }
 

diff --git a/src/to-sat/AIG/ToCNFAIG.h b/src/to-sat/AIG/ToCNFAIG.h
index 077b8407f041ccb983586f39fd6d01852b2be738..5e54365ea8953ff92bfd9e06dcf260a5c870454b 100644 (file)
--- a/src/to-sat/AIG/ToCNFAIG.h
+++ b/src/to-sat/AIG/ToCNFAIG.h
@@ -9,8 +9,7 @@
 
 namespace BEEV {
 
-class ToCNFAIG {
-       Cnf_Dat_t* priorCnfData;
+class ToCNFAIG{
 
     // no copy. no assignment.
        ToCNFAIG&  operator = (const ToCNFAIG& other);
@@ -18,33 +17,19 @@ class ToCNFAIG {
 
        UserDefinedFlags& uf;
 
-
 public:
        ToCNFAIG(UserDefinedFlags& _uf):
                uf(_uf)
        {
-               priorCnfData = NULL;
        }
 
-       ~ToCNFAIG() {
-               if (NULL != priorCnfData)
-                       Cnf_DataFree(priorCnfData);
+       ~ToCNFAIG()
+       {
        }
 
        void toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
                        ToSATBase::ASTNodeToSATVar& nodeToVar,
                        bool needAbsRef,  BBNodeManagerAIG& _mgr);
-
-       // assumes the above function was called first.
-       void toCNF_renter(const BBNodeAIG& top, Cnf_Dat_t*& cnfData,
-                       ToSATBase::ASTNodeToSATVar& nodeToVar, BBNodeManagerAIG& _mgr);
-
-       // The piror must be set before toCNF_reenter is called.
-       void setPrior(Cnf_Dat_t* prior)
-       {
-               priorCnfData = prior;
-       }
-
 };
 
 }

diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index 5f096c67609b94d9dc7da17f82f60c02d0b32f90..b9bf1bcd5f56ca4603b78791dac82fb7eec3e686 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -8,69 +8,54 @@ namespace BEEV
     bool
     ToSATAIG::CallSAT(SATSolver& satSolver, const ASTNode& input, bool needAbsRef)
     {
-       // Shortcut if known. This avoids calling the setup of the CNF generator.
-       // setup takes about 15ms.
-       if (input == ASTFalse && !needAbsRef)
-               return false;
+       if (cb != NULL  && cb->isUnsatisfiable())
+          return false;
 
-       if (input == ASTTrue && !needAbsRef)
-               return true;
+       if (!first)
+       {
+          assert(input == ASTTrue);
+          bm->GetRunTimes()->start(RunTimes::Solving);
+           satSolver.solve();
+           bm->GetRunTimes()->stop(RunTimes::Solving);
 
-     if (cb != NULL  && cb->isUnsatisfiable())
-        return false;
+           if(bm->UserFlags.stats_flag)
+             satSolver.printStats();
 
-      if (simp == NULL)
-         simp = new Simplifier(bm);
+           return satSolver.okay();
+       }
 
-      if (bb== NULL)
-         bb =  new BitBlaster<BBNodeAIG, BBNodeManagerAIG>(&mgr,cb,simp,bm->defaultNodeFactory,&bm->UserFlags);
+       // Shortcut if known. This avoids calling the setup of the CNF generator.
+       // setup of the CNF generator is expensive. NB, these checks have to occur
+    // after calling the sat solver (if it's not the first time.)
+      if (input == ASTFalse )
+               return false;
+
+      if (input == ASTTrue  )
+               return true;
+
+         Simplifier simp(bm);
+
+         BBNodeManagerAIG mgr;
+         BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&mgr,cb,&simp,bm->defaultNodeFactory,&bm->UserFlags);
 
       bm->GetRunTimes()->start(RunTimes::BitBlasting);
-      BBNodeAIG BBFormula = bb->BBForm(input);
+      BBNodeAIG BBFormula = bb.BBForm(input);
       bm->GetRunTimes()->stop(RunTimes::BitBlasting);
 
-      // It's not incremental.
       delete cb;
       cb = NULL;
-      bb->cb = NULL;
-
-      if (!needAbsRef)
-      {
-         delete simp;
-         simp = NULL;
+      bb.cb = NULL;
 
-         delete bb;
-         bb = NULL;
-
-      }
-
-      if (first)
-         assert(satSolver.nVars() ==0);
-
-      // Oddly the substitution map, which is necessary to output a model is kept in the simplifier.
-      // The bitblaster should never enter anything into the solver map.
-      //assert(simp.Return_SolverMap()->size() ==0);
+         assert(satSolver.nVars() ==0);
 
+         bm->GetRunTimes()->start(RunTimes::CNFConversion);
       Cnf_Dat_t* cnfData = NULL;
-
-      bm->GetRunTimes()->start(RunTimes::CNFConversion);
-      if (first)
-         {
-         toCNF.toCNF(BBFormula, cnfData, nodeToSATVar,needAbsRef,mgr);
-         }
-      else
-         {
-         assert(needAbsRef);
-         toCNF.toCNF_renter(BBFormula, cnfData, nodeToSATVar,mgr);
-         }
+         toCNF.toCNF(BBFormula, cnfData, nodeToSATVar,needAbsRef,mgr);
       bm->GetRunTimes()->stop(RunTimes::CNFConversion);
 
-      if (!needAbsRef)
-      {
-         // Free the memory in the AIGs.
-         BBFormula = BBNodeAIG(); // null node
-         mgr.stop();
-      }
+         // Free the memory in the AIGs.
+         BBFormula = BBNodeAIG(); // null node
+         mgr.stop();
 
       if (bm->UserFlags.output_CNF_flag)
       {
@@ -100,7 +85,6 @@ namespace BEEV
       for (int i = 0; i < cnfData->nVars - satV ; i++)
         satSolver.newVar();
 
-
       SATSolver::vec_literals satSolverClause;
       for (int i = 0; i < cnfData->nClauses; i++)
         {
@@ -123,17 +107,9 @@ 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;
 
-      if (!needAbsRef)
-      {
-         Cnf_ClearMemory();
-         Cnf_DataFree(cnfData);
-         cnfData = NULL;
-      }
-      else
-      {
-         toCNF.setPrior(cnfData);
-      }
-
+         Cnf_ClearMemory();
+         Cnf_DataFree(cnfData);
+         cnfData = NULL;
 
       bm->GetRunTimes()->start(RunTimes::Solving);
       satSolver.solve();
@@ -147,10 +123,6 @@ namespace BEEV
 
     ToSATAIG::~ToSATAIG()
     {
-       delete bb;
-       delete simp;
        ClearAllTables();
     }
-
-
 }

diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h
index 1d1fde2d718c2254c987107d48f858c3d862aa91..3a33b17752f5e42c32fd68064442ac8ecba57875 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.h
+++ b/src/to-sat/AIG/ToSATAIG.h
@@ -34,20 +34,15 @@ namespace BEEV
 
        int count;
        bool first;
-       BitBlaster<BBNodeAIG, BBNodeManagerAIG> *bb;
        int CNFFileNameCounter;
-       BBNodeManagerAIG mgr;
-       Simplifier *simp;
 
-    ToCNFAIG toCNF;
+       ToCNFAIG toCNF;
 
     void init()
     {
         count = 0;
         first = true;
-        bb = NULL;
         CNFFileNameCounter =0;
-        simp = NULL;
     }
 
   public:
@@ -57,7 +52,6 @@ namespace BEEV
        return cb == NULL;
     }
 
-
     ToSATAIG(STPMgr * bm) :
       ToSATBase(bm), toCNF(bm->UserFlags)
     {