#include "../sat/SimplifyingMinisat.h"
#include "../sat/MinisatCore.h"
#include "../sat/CryptoMinisat.h"
+#include <memory>
namespace BEEV {
bm->start_abstracting = false;
bm->TermsAlreadySeenMap_Clear();
do
- {
- inputToSAT = simplified_solved_InputToSAT;
+ {
+ inputToSAT = simplified_solved_InputToSAT;
if(bm->UserFlags.optimize_flag)
{
bm->ASTNodeStats("after simplification: ",
simplified_solved_InputToSAT);
}
-
+
// The word level solver uses the simplifier to apply the rewrites it makes,
// without optimisations enabled. It will enter infinite loops on some input.
// Instead it could use the apply function of the substitution map, but it
bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
}
- } while (inputToSAT != simplified_solved_InputToSAT);
-
+ } while (inputToSAT != simplified_solved_InputToSAT);
+
bm->ASTNodeStats("After SimplifyWrites_Inplace: ",
simplified_solved_InputToSAT);
if(bm->UserFlags.stats_flag)
simp->printCacheStatus();
+ const bool useAIGToCNF = !arrayops || !bm->UserFlags.arrayread_refinement_flag || bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_SOLVER;
+ const bool maybeRefinement = arrayops && bm->UserFlags.arrayread_refinement_flag;
- // If it doesn't contain array operations, use ABC's CNF generation.
- if (!arrayops || !bm->UserFlags.arrayread_refinement_flag)
- {
- simplifier::constantBitP::ConstantBitPropagation* cb = NULL;
+ simplifier::constantBitP::ConstantBitPropagation* cb = NULL;
+ std::auto_ptr<simplifier::constantBitP::ConstantBitPropagation> cleaner;
if (bm->UserFlags.bitConstantProp_flag)
- {
- bm->ASTNodeStats("Before Constant Bit Propagation begins: ",
- simplified_solved_InputToSAT);
-
- bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation);
-
- cb = new simplifier::constantBitP::ConstantBitPropagation(simp, bm->defaultNodeFactory,simplified_solved_InputToSAT);
+ {
+ bm->ASTNodeStats("Before Constant Bit Propagation begins: ",
+ simplified_solved_InputToSAT);
- bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation);
+ bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation);
+ cb = new simplifier::constantBitP::ConstantBitPropagation(simp, bm->defaultNodeFactory,simplified_solved_InputToSAT);
+ cleaner.reset(cb);
+ bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation);
- if (cb->isUnsatisfiable())
- simplified_solved_InputToSAT = bm->ASTFalse;
- }
+ if (cb->isUnsatisfiable())
+ simplified_solved_InputToSAT = bm->ASTFalse;
+ }
ToSATAIG toSATAIG(bm,cb);
+ ToSATBase* satBase = useAIGToCNF? ((ToSAT*)&toSATAIG) : tosat;
+
+ // If it doesn't contain array operations, use ABC's CNF generation.
res =
Ctr_Example->CallSAT_ResultCheck(NewSolver,
simplified_solved_InputToSAT,
orig_input,
- &toSATAIG
- );
-
- }
- else
- {
- res =
- Ctr_Example->CallSAT_ResultCheck(NewSolver,
- simplified_solved_InputToSAT,
- orig_input,
- tosat
- );
-
- }
+ satBase,
+ maybeRefinement);
if (SOLVER_UNDECIDED != res)
{
- CountersAndStats("print_func_stats", bm);
+ // If the aig converter knows that it is never going to be called again,
+ // it deletes the constant bit stuff before calling the SAT solver.
+ if (toSATAIG.cbIsDestructed())
+ cleaner.release();
+
+ CountersAndStats("print_func_stats", bm);
return res;
}
assert(arrayops); // should only go to abstraction refinement if there are array ops.
assert(bm->UserFlags.arrayread_refinement_flag); // Refinement must be enabled too.
+ // Unfortunately how I implemented the incremental CNF generator in ABC means that
+ // cryptominisat and simplifying minisat may simplify away variables that we later need.
+
res =
Ctr_Example->SATBased_ArrayReadRefinement(NewSolver,
simplified_solved_InputToSAT,
orig_input,
- tosat);
+ satBase);
if (SOLVER_UNDECIDED != res)
{
- CountersAndStats("print_func_stats", bm);
+ if (toSATAIG.cbIsDestructed())
+ cleaner.release();
+
+ CountersAndStats("print_func_stats", bm);
return res;
}
res =
- Ctr_Example->SATBased_ArrayWriteRefinement(NewSolver, orig_input,tosat);
+ Ctr_Example->SATBased_ArrayWriteRefinement(NewSolver, orig_input,satBase);
if (SOLVER_UNDECIDED != res)
{
- CountersAndStats("print_func_stats", bm);
+ if (toSATAIG.cbIsDestructed())
+ cleaner.release();
+
+ CountersAndStats("print_func_stats", bm);
return res;
}
res =
Ctr_Example->SATBased_ArrayReadRefinement(NewSolver,
simplified_solved_InputToSAT,
- orig_input,tosat);
+ orig_input,
+ satBase);
if (SOLVER_UNDECIDED != res)
{
- CountersAndStats("print_func_stats", bm);
+ if (toSATAIG.cbIsDestructed())
+ cleaner.release();
+
+
+ CountersAndStats("print_func_stats", bm);
return res;
}
CallSAT_ResultCheck(SATSolver& SatSolver,
const ASTNode& modified_input,
const ASTNode& original_input,
- ToSATBase* tosat);
+ ToSATBase* tosat,
+ bool refinement);
//creates array write axiom only for the input term or formula, if
//necessary. If there are no axioms to produce then it simply
assert ((SYMBOL == arrsym.GetKind() || BVCONST == arrsym.GetKind()));
read_node_symbols.push_back(arrsym);
+
jKind.push_back(listOfIndices[i].GetKind());
concreteIndexes.push_back(TermToConstTermUsingModel(the_index));
concreteValues.push_back(TermToConstTermUsingModel(arrsym));
+
}
//loop over the list of indices for the array and create LA,
res2 = CallSAT_ResultCheck(SatSolver,
FalseAxioms,
original_input,
- tosat);
+ tosat,
+ true);
FalseAxiomsVec.clear();
if (SOLVER_UNDECIDED != res2)
RemainingAxioms);
bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement);
return CallSAT_ResultCheck(SatSolver, RemainingAxioms, original_input,
- tosat);
+ tosat,true);
}
+
bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement);
+
return SOLVER_UNDECIDED;
} //end of SATBased_ArrayReadRefinement
writeAxiom = (FalseAxioms.size() != 1) ? bm->CreateNode(AND,
FalseAxioms) : FalseAxioms[0];
bm->ASTNodeStats("adding false writeaxiom to SAT: ", writeAxiom);
- res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input, tosat);
+ res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input, tosat,true);
}
if (SOLVER_UNDECIDED != res2)
res2 = CallSAT_ResultCheck(SatSolver,
writeAxiom,
original_input,
- tosat);
+ tosat, true);
}
return res2;
} //end of SATBased_ArrayWriteRefinement
}
else
{
- return val;
+ return val;
}
}
}
else
{
- cerr << "TermToConstTermUsingModel: termITE: "
- "value of conditional is wrong: " << condcompute << endl;
FatalError(" TermToConstTermUsingModel: termITE: "
"cannot compute ITE conditional against model: ", term);
}
}
else
{
- cerr << "TermToConstTermUsingModel: termITE: "
- << "value of conditional is wrong: " << condcompute << endl;
FatalError(" TermToConstTermUsingModel: termITE: cannot "
"compute ITE conditional against model: ", term);
}
ASTNode ff = TermToConstTermUsingModel(*it, ArrayReadFlag);
o.push_back(ff);
}
- output = bm->hashingNodeFactory->CreateTerm(k, term.GetValueWidth(), o);
- //output is a CONST expression. compute its value and store it
- //in the CounterExampleMap
- output = simp->BVConstEvaluator(output);
- break;
+
+ output = NonMemberBVConstEvaluator(term.GetSTPMgr() , k, o, term.GetValueWidth());
+ break;
}
}
ASTNode
AbsRefine_CounterExample::ComputeFormulaUsingModel(const ASTNode& form)
{
- const ASTNode& in = form;
const Kind k = form.GetKind();
if (!(is_Form_kind(k) && BOOLEAN_TYPE == form.GetType()))
{
}
//cerr << "Input to ComputeFormulaUsingModel:" << form << endl;
- ASTNodeMap::iterator it1;
+ ASTNodeMap::const_iterator it1;
if ((it1 = ComputeFormulaMap.find(form)) != ComputeFormulaMap.end())
{
- ASTNode res = it1->second;
+ const ASTNode& res = it1->second;
if (ASTTrue == res || ASTFalse == res)
{
return res;
for (ASTVec::const_iterator it = form.begin(), itend = form.end(); it
!= itend; it++)
- {
+ {
children.push_back(TermToConstTermUsingModel(*it, false));
}
- output = simp->BVConstEvaluator(bm->CreateNode(k, children));
+ output = NonMemberBVConstEvaluator(form.GetSTPMgr() , k, children, form.GetValueWidth());
//evaluate formula to false if bvdiv execption occurs while
//counterexample is being checked during refinement.
children.push_back( ComputeFormulaUsingModel(*it));
}
- output = simp->BVConstEvaluator(bm->CreateNode(k, children));
+ output = NonMemberBVConstEvaluator(form.GetSTPMgr() , k, children, form.GetValueWidth());
//evaluate formula to false if bvdiv execption occurs while
//counterexample is being checked during refinement.
break;
}
- //cout << "ComputeFormulaUsingModel output is:" << output << endl;
assert(ASTUndefined != output);
assert(output.isConstant());
ComputeFormulaMap[form] = output;
SOLVER_RETURN_TYPE
AbsRefine_CounterExample::CallSAT_ResultCheck(SATSolver& SatSolver,
- const ASTNode& modified_input, const ASTNode& original_input, ToSATBase* tosat)
+ const ASTNode& modified_input, const ASTNode& original_input, ToSATBase* tosat, bool refinement)
{
- bool sat = tosat->CallSAT(SatSolver, modified_input);
+ bool sat = tosat->CallSAT(SatSolver, modified_input, refinement);
if (!sat)
{
namespace BEEV
{
- void
- BBNodeManagerAIG::toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar, const UserDefinedFlags& uf)
- {
- assert(cnfData == NULL);
-
- Aig_ObjCreatePo(aigMgr, top.n);
- Aig_ManCleanup(aigMgr); // remove nodes not connected to the PO.
- Aig_ManCheck(aigMgr); // check that AIG looks ok.
-
- assert(Aig_ManPoNum(aigMgr) == 1);
-
- // UseZeroes gives assertion errors.
- // Rewriting is sometimes very slow. Can it be configured to be faster?
- // What about refactoring???
-
- int nodeCount = aigMgr->nObjs[AIG_OBJ_AND];
- if (uf.stats_flag)
- cerr << "Nodes before AIG rewrite:" << nodeCount <<endl;
-
-
- if (uf.enable_AIG_rewrites_flag && aigMgr->nObjs[AIG_OBJ_AND] < 5000)
- {
- Dar_LibStart();
- Aig_Man_t * pTemp;
- Dar_RwrPar_t Pars, * pPars = &Pars;
- Dar_ManDefaultRwrParams( pPars );
-
- // Assertion errors occur with this enabled.
- // pPars->fUseZeros = 1;
-
- // For mul63bit.smt2 with iterations =3 & nCutsMax = 8
- // CNF generation was taking 139 seconds, solving 10 seconds.
-
- // With nCutsMax =2, CNF generation takes 16 seconds, solving 10 seconds.
- // The rewriting doesn't remove as many nodes of course..
- int iterations = 3;
-
- for (int i=0; i < iterations;i++)
- {
- aigMgr = Aig_ManDup( pTemp = aigMgr, 0 );
- Aig_ManStop( pTemp );
- Dar_ManRewrite( aigMgr, pPars );
-
- aigMgr = Aig_ManDup( pTemp = aigMgr, 0 );
- Aig_ManStop( pTemp );
-
- if (uf.stats_flag)
- cerr << "After rewrite [" << i << "] nodes:" << aigMgr->nObjs[AIG_OBJ_AND] << endl;
-
- if (nodeCount == aigMgr->nObjs[AIG_OBJ_AND])
- break;
- }
- }
- if (aigMgr->nObjs[AIG_OBJ_AND] < 2000000)
- cnfData = Cnf_Derive(aigMgr, 0);
- else
- cnfData = Cnf_DeriveSimple(aigMgr, 0);
-
- BBNodeManagerAIG::SymbolToBBNode::const_iterator it;
-
- assert(nodeToVar.size() ==0);
-
- // Each symbol maps to a vector of CNF variables.
- for (it = symbolToBBNode.begin(); it != symbolToBBNode.end(); it++)
- {
- const ASTNode& n = it->first;
- const vector<BBNodeAIG> &b = it->second;
- assert (nodeToVar.find(n) == nodeToVar.end());
-
- const int width = (n.GetType() == BOOLEAN_TYPE) ? 1: n.GetValueWidth();
-
- // INT_MAX for parts of symbols that didn't get encoded.
- vector<unsigned> v(width, ~((unsigned) 0));
+}
- for (unsigned i = 0; i < b.size(); i++)
- {
- if (!b[i].IsNull())
- {
- Aig_Obj_t * pObj;
- pObj = (Aig_Obj_t*)Vec_PtrEntry( aigMgr->vPis, b[i].symbol_index );
- v[i] = cnfData->pVarNums[pObj->Id];
- }
- }
- nodeToVar.insert(make_pair(n, v));
- }
- assert(cnfData != NULL);
- }
-}
// Creates AIG nodes with ABC and wraps them in BBNodeAIG's.
class BBNodeManagerAIG
{
+public:
Aig_Man_t *aigMgr;
// Map from symbols to their AIG nodes.
typedef map<ASTNode, vector<BBNodeAIG> > SymbolToBBNode;
- SymbolToBBNode symbolToBBNode;
+ SymbolToBBNode symbolToBBNode;
+private:
// AIGs can only take two parameters. This makes a log_2 height
// tower of varadic inputs.
Aig_Obj_t * makeTower(Aig_Obj_t * (*t)(Aig_Man_t *, Aig_Obj_t *,
return BBNodeAIG(Aig_ManConst0(aigMgr));
}
- void toCNF(const BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar, const UserDefinedFlags& uf);
-
// The same symbol always needs to return the same AIG node,
// if it doesn't you will get the wrong answer.
BBNodeAIG CreateSymbol(const ASTNode& n, unsigned i)
{
- assert(n.GetKind() == SYMBOL);
+ assert(n.GetKind() == SYMBOL);
// booleans have width 0.
const unsigned width = std::max((unsigned)1, n.GetValueWidth());
--- /dev/null
+#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)
+{
+ BBNodeManagerAIG::SymbolToBBNode::const_iterator it;
+ // Each symbol maps to a vector of CNF variables.
+ for (it = mgr.symbolToBBNode.begin(); it != mgr.symbolToBBNode.end(); it++) {
+ const ASTNode& n = it->first;
+ const vector<BBNodeAIG> &b = it->second;
+
+ const int width = (n.GetType() == BOOLEAN_TYPE) ? 1 : n.GetValueWidth();
+
+ // INT_MAX for parts of symbols that didn't get encoded.
+ vector<unsigned> v(width, ~((unsigned) 0));
+
+ for (unsigned i = 0; i < b.size(); i++) {
+ if (!b[i].IsNull()) {
+ Aig_Obj_t * pObj;
+ pObj = (Aig_Obj_t*) Vec_PtrEntry(mgr.aigMgr->vPis,
+ b[i].symbol_index);
+ v[i] = cnfData->pVarNums[pObj->Id];
+ }
+ }
+ 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,
+ ToSATBase::ASTNodeToSATVar& nodeToVar,
+ bool needAbsRef, BBNodeManagerAIG& mgr) {
+ assert(cnfData == NULL);
+
+ Aig_ObjCreatePo(mgr.aigMgr, top.n);
+ if (!needAbsRef) {
+ Aig_ManCleanup( mgr.aigMgr); // remove nodes not connected to the PO.
+ }
+ Aig_ManCheck( mgr.aigMgr); // check that AIG looks ok.
+
+ assert(Aig_ManPoNum(mgr.aigMgr) == 1);
+
+ // UseZeroes gives assertion errors.
+ // Rewriting is sometimes very slow. Can it be configured to be faster?
+ // What about refactoring???
+
+ int nodeCount = mgr.aigMgr->nObjs[AIG_OBJ_AND];
+ if (uf.stats_flag)
+ cerr << "Nodes before AIG rewrite:" << nodeCount << endl;
+
+ if (!needAbsRef && uf.enable_AIG_rewrites_flag
+ && mgr.aigMgr->nObjs[AIG_OBJ_AND] < 5000) {
+ Dar_LibStart();
+ Aig_Man_t * pTemp;
+ Dar_RwrPar_t Pars, *pPars = &Pars;
+ Dar_ManDefaultRwrParams(pPars);
+
+ // Assertion errors occur with this enabled.
+ // pPars->fUseZeros = 1;
+
+ // For mul63bit.smt2 with iterations =3 & nCutsMax = 8
+ // CNF generation was taking 139 seconds, solving 10 seconds.
+
+ // With nCutsMax =2, CNF generation takes 16 seconds, solving 10 seconds.
+ // The rewriting doesn't remove as many nodes of course..
+ int iterations = 3;
+
+ for (int i = 0; i < iterations; i++) {
+ mgr.aigMgr = Aig_ManDup(pTemp = mgr.aigMgr, 0);
+ Aig_ManStop(pTemp);
+ Dar_ManRewrite(mgr.aigMgr, pPars);
+
+ mgr.aigMgr = Aig_ManDup(pTemp = mgr.aigMgr, 0);
+ Aig_ManStop(pTemp);
+
+ if (uf.stats_flag)
+ cerr << "After rewrite [" << i << "] nodes:"
+ << mgr.aigMgr->nObjs[AIG_OBJ_AND] << endl;
+
+ if (nodeCount == mgr.aigMgr->nObjs[AIG_OBJ_AND])
+ break;
+ }
+ }
+ if (!needAbsRef && mgr.aigMgr->nObjs[AIG_OBJ_AND] < 2000000) {
+ cnfData = Cnf_Derive(mgr.aigMgr, 0);
+ } else {
+ cnfData = Cnf_DeriveSimple(mgr.aigMgr, 0);
+ }
+
+ BBNodeManagerAIG::SymbolToBBNode::const_iterator it;
+
+ assert(nodeToVar.size() == 0);
+
+ //todo. cf. with addvariables above...
+ // Each symbol maps to a vector of CNF variables.
+ for (it = mgr.symbolToBBNode.begin(); it != mgr.symbolToBBNode.end(); it++) {
+ const ASTNode& n = it->first;
+ const vector<BBNodeAIG> &b = it->second;
+ assert(nodeToVar.find(n) == nodeToVar.end());
+
+ const int width = (n.GetType() == BOOLEAN_TYPE) ? 1 : n.GetValueWidth();
+
+ // INT_MAX for parts of symbols that didn't get encoded.
+ vector<unsigned> v(width, ~((unsigned) 0));
+
+ for (unsigned i = 0; i < b.size(); i++) {
+ if (!b[i].IsNull()) {
+ Aig_Obj_t * pObj;
+ pObj = (Aig_Obj_t*) Vec_PtrEntry(mgr.aigMgr->vPis,
+ b[i].symbol_index);
+ v[i] = cnfData->pVarNums[pObj->Id];
+ }
+ }
+
+ nodeToVar.insert(make_pair(n, v));
+ }
+ assert(cnfData != NULL);
+}
+};
--- /dev/null
+#ifndef TOCNFAIG_H_
+#define TOCNFAIG_H_
+
+#include "../../extlib-abc/aig.h"
+#include "../../extlib-abc/cnf_short.h"
+#include "../../extlib-abc/dar.h"
+#include "../ToSATBase.h"
+#include "BBNodeManagerAIG.h"
+
+namespace BEEV {
+
+class ToCNFAIG {
+ Cnf_Dat_t* priorCnfData;
+
+ // no copy. no assignment.
+ ToCNFAIG& operator = (const ToCNFAIG& other);
+ ToCNFAIG(const ToCNFAIG& other);
+
+ const UserDefinedFlags& uf;
+
+
+public:
+ ToCNFAIG(const UserDefinedFlags& _uf):
+ uf(_uf)
+ {
+ priorCnfData = NULL;
+ }
+
+ ~ToCNFAIG() {
+ if (NULL != priorCnfData)
+ Cnf_DataFree(priorCnfData);
+ }
+
+ 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;
+ }
+
+};
+
+}
+#endif /* TOCNFAIG_H_ */
namespace BEEV
{
- // Can not be used with abstraction refinement.
bool
- ToSATAIG::CallSAT(SATSolver& satSolver, const ASTNode& input)
+ ToSATAIG::CallSAT(SATSolver& satSolver, const ASTNode& input, bool needAbsRef)
{
if (cb != NULL && cb->isUnsatisfiable())
return false;
- BBNodeManagerAIG mgr;
- Simplifier *simp = new Simplifier(bm);
- BitBlaster<BBNodeAIG, BBNodeManagerAIG> *bb = new BitBlaster<BBNodeAIG, BBNodeManagerAIG>(&mgr,cb,simp,bm->defaultNodeFactory,&bm->UserFlags);
+ if (simp == NULL)
+ simp = new Simplifier(bm);
- // Even if we cleared the tables we could still have the hash table's buckets sitting around.
- delete simp;
- simp = NULL;
+ if (bb== NULL)
+ bb = new BitBlaster<BBNodeAIG, BBNodeManagerAIG>(&mgr,cb,simp,bm->defaultNodeFactory,&bm->UserFlags);
bm->GetRunTimes()->start(RunTimes::BitBlasting);
BBNodeAIG BBFormula = bb->BBForm(input);
bm->GetRunTimes()->stop(RunTimes::BitBlasting);
- delete bb;
- bb = NULL;
- //Clear out all the constant bit stuff before sending the SAT.
- if (cb != NULL)
- {
- delete cb;
- cb = NULL;
- }
+ // It's not incremental.
+ delete cb;
+ cb = NULL;
+ bb->cb = NULL;
+
+ if (!needAbsRef)
+ {
+ delete simp;
+ simp = NULL;
+ delete bb;
+ bb = NULL;
+ }
- assert(satSolver.nVars() ==0);
+ 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.
Cnf_Dat_t* cnfData = NULL;
bm->GetRunTimes()->start(RunTimes::CNFConversion);
- mgr.toCNF(BBFormula, cnfData, nodeToSATVar,bm->UserFlags);
+ if (first)
+ {
+ toCNF.toCNF(BBFormula, cnfData, nodeToSATVar,needAbsRef,mgr);
+ }
+ else
+ {
+ assert(needAbsRef);
+ toCNF.toCNF_renter(BBFormula, cnfData, nodeToSATVar,mgr);
+ }
bm->GetRunTimes()->stop(RunTimes::CNFConversion);
- // Free the memory in the AIGs.
- BBFormula = BBNodeAIG(); // null node
- mgr.stop();
+ if (!needAbsRef)
+ {
+ // Free the memory in the AIGs.
+ BBFormula = BBNodeAIG(); // null node
+ mgr.stop();
+ }
+
+ if (bm->UserFlags.output_CNF_flag)
+ {
+ stringstream fileName;
+ fileName << "output_" << CNFFileNameCounter++ << ".cnf";
+ Cnf_DataWriteIntoFile(cnfData, (char*)fileName.str().c_str(), 0);
+ }
+ first = false;
+
bm->GetRunTimes()->start(RunTimes::SendingToSAT);
- for (int i = 0; i < cnfData->nVars; i++)
+ // Create a new sat variable for each of the variables in the CNF.
+ int satV = satSolver.nVars();
+ for (int i = 0; i < cnfData->nVars - satV ; i++)
satSolver.newVar();
+
SATSolver::vec_literals satSolverClause;
for (int i = 0; i < cnfData->nClauses; i++)
{
+ 1]; pLit < pStop; pLit++)
{
SATSolver::Var var = (*pLit) >> 1;
- assert(var < satSolver.nVars());
+ if (!(var < satSolver.nVars()))
+ {
+ cerr << var << " ";
+ cerr << satSolver.nVars();
+ exit(1);
+ }
Minisat::Lit l = SATSolver::mkLit(var, (*pLit) & 1);
satSolverClause.push(l);
}
}
bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
- if (bm->UserFlags.output_CNF_flag)
- Cnf_DataWriteIntoFile(cnfData, "output_0.cnf", 0);
-
if (bm->UserFlags.output_bench_flag)
cerr << "Converting to CNF via ABC's AIG package can't yet print out bench format" << endl;
- Cnf_ClearMemory();
- Cnf_DataFree(cnfData);
+ if (!needAbsRef)
+ {
+ Cnf_ClearMemory();
+ Cnf_DataFree(cnfData);
+ cnfData = NULL;
+ }
+ else
+ {
+ toCNF.setPrior(cnfData);
+ }
if (bm->UserFlags.exit_after_CNF)
{
return satSolver.okay();
}
+ ToSATAIG::~ToSATAIG()
+ {
+ delete bb;
+ delete simp;
+ ClearAllTables();
+ }
+
+
}
#include "../STPManager/STPManager.h"
#include "../BitBlaster.h"
#include "BBNodeManagerAIG.h"
+#include "ToCNFAIG.h"
namespace BEEV
{
- // NB You can't use this with abstraction refinement!!!
class ToSATAIG : public ToSATBase
{
private:
ToSATAIG& operator = (const ToSATAIG& other);
ToSATAIG(const ToSATAIG& other);
+ int count;
+ bool first;
+ BitBlaster<BBNodeAIG, BBNodeManagerAIG> *bb;
+ int CNFFileNameCounter;
+ BBNodeManagerAIG mgr;
+ Simplifier *simp;
+
+ ToCNFAIG toCNF;
+
+ void init()
+ {
+ count = 0;
+ first = true;
+ bb = NULL;
+ CNFFileNameCounter =0;
+ simp = NULL;
+ }
+
public:
+ bool cbIsDestructed()
+ {
+ return cb == NULL;
+ }
+
+
ToSATAIG(STPMgr * bm) :
- ToSATBase(bm)
+ ToSATBase(bm), toCNF(bm->UserFlags)
{
cb = NULL;
+ init();
}
ToSATAIG(STPMgr * bm, simplifier::constantBitP::ConstantBitPropagation* cb_) :
- ToSATBase(bm)
+ ToSATBase(bm), cb(cb_), toCNF(bm->UserFlags)
{
cb = cb_;
+ init();
}
+ ~ToSATAIG();
+
void
ClearAllTables()
{
return nodeToSATVar;
}
- // Can not be used with abstraction refinement.
- bool CallSAT(SATSolver& satSolver, const ASTNode& input);
+ bool CallSAT(SATSolver& satSolver, const ASTNode& input, bool needAbsRef);
};
}
//can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or
//SOLVER_UNDECIDED
bool ToSAT::CallSAT(SATSolver& SatSolver,
- const ASTNode& input)
+ const ASTNode& input, bool refinement)
{
bm->GetRunTimes()->start(RunTimes::BitBlasting);
// Bitblasts, CNF conversion and calls toSATandSolve()
bool CallSAT(SATSolver& SatSolver,
- const ASTNode& input);
+ const ASTNode& input, bool refinement);
ASTNodeToSATVar& SATVar_to_SymbolIndexMap()
{
BBNode BBTrue, BBFalse;
- simplifier::constantBitP::ConstantBitPropagation* cb;
-
// Memo table for bit blasted terms. If a node has already been
// bitblasted, it is mapped to a vector of Boolean formulas for
// the
public:
+ simplifier::constantBitP::ConstantBitPropagation* cb;
+
// Bit blast a bitvector term. The term must have a kind for a
// bitvector term. Result is a ref to a vector of formula nodes
// representing the boolean formula.
void PrintOutput(SOLVER_RETURN_TYPE ret);
// Bitblasts, CNF conversion and calls toSATandSolve()
- virtual bool CallSAT(SATSolver& SatSolver, const ASTNode& input) =0;
+ virtual bool CallSAT(SATSolver& SatSolver, const ASTNode& input, bool doesAbsRef) =0;
virtual ASTNodeToSATVar& SATVar_to_SymbolIndexMap()= 0;
projects / francis / stp.git / commitdiff