From: trevor_hansen Date: Sat, 3 Jul 2010 13:15:31 +0000 (+0000) Subject: Bitblast formula that don't contain arrays into and-inverter graphs. This uses the... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=6acdcaffa8121c5fed09d00466bd6200228ae6e6;p=francis%2Fstp.git Bitblast formula that don't contain arrays into and-inverter graphs. This uses the AIG implementation provided by the ABC package. This has some advantages: * The AIG nodes are smaller than our ASTNodes, so it uses less memory. * The CNFs generated by ABC are smaller, so generally solving is quicker. Some notes: * I haven't made the CNF converter incremental, so bitblasting to AIGs is only enabled for bit-vector problems (which STP bitblasts eagerly). * AIG re-writing isn't enabled yet. * From prior experience some big problems fail in CNF encoding. All of our test cases pass though. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@913 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp index d564e09..d8efe42 100644 --- a/src/AST/RunTimes.cpp +++ b/src/AST/RunTimes.cpp @@ -15,7 +15,7 @@ #include "RunTimes.h" // BE VERY CAREFUL> Update the Category Names to match. -std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation"}; +std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification"}; namespace BEEV { diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h index 20ccd3b..fbf686b 100644 --- a/src/AST/RunTimes.h +++ b/src/AST/RunTimes.h @@ -28,7 +28,8 @@ public: BVSolver, CreateSubstitutionMap, SendingToSAT, - CounterExampleGeneration + CounterExampleGeneration, + SATSimplifying }; static std::string CategoryNames[]; diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index cc4608d..00dff41 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -9,6 +9,7 @@ #include "STP.h" #include "DifficultyScore.h" +#include "../to-sat/AIG/ToSATAIG.h" namespace BEEV { @@ -189,8 +190,9 @@ namespace BEEV { cerr << "Final Difficulty Score:" << final_difficulty_score <UserFlags.optimize_flag; - if (final_difficulty_score > 2 *initial_difficulty_score && !containsArrayOps(orig_input)) + if (final_difficulty_score > 2 *initial_difficulty_score && !arrayops) { // If the simplified problem is harder, than the // initial problem we revert back to the initial @@ -232,16 +234,26 @@ namespace BEEV { delete bvsolver; bvsolver = new BVSolver(bm,simp); + { + ToSATAIG toSATAIG(bm); + + // If it doesn't contain array operations, use ABC's CNF generation. res = Ctr_Example->CallSAT_ResultCheck(NewSolver, simplified_solved_InputToSAT, - orig_input); + orig_input, + (arrayops ? ((ToSATBase*)tosat): ((ToSATBase*)&toSATAIG)) + ); + } + if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats", bm); return res; } + assert(arrayops); // should only go to abstraction refinement if there are array ops. + // res = SATBased_AllFiniteLoops_Refinement(NewSolver, orig_input); // if (SOLVER_UNDECIDED != res) // { @@ -252,7 +264,8 @@ namespace BEEV { res = Ctr_Example->SATBased_ArrayReadRefinement(NewSolver, simplified_solved_InputToSAT, - orig_input); + orig_input, + tosat); if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats", bm); @@ -260,7 +273,7 @@ namespace BEEV { } res = - Ctr_Example->SATBased_ArrayWriteRefinement(NewSolver, orig_input); + Ctr_Example->SATBased_ArrayWriteRefinement(NewSolver, orig_input,tosat); if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats", bm); @@ -270,7 +283,7 @@ namespace BEEV { res = Ctr_Example->SATBased_ArrayReadRefinement(NewSolver, simplified_solved_InputToSAT, - orig_input); + orig_input,tosat); if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats", bm); diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h index a858a28..76a463d 100644 --- a/src/absrefine_counterexample/AbsRefine_CounterExample.h +++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h @@ -14,7 +14,7 @@ #include "../STPManager/STPManager.h" #include "../simplifier/simplifier.h" #include "../AST/ArrayTransformer.h" -#include "../to-sat/ToSAT.h" +#include "../to-sat/ToSATBase.h" namespace BEEV { @@ -52,7 +52,7 @@ namespace BEEV ArrayTransformer * ArrayTransform; // Ptr to ToSAT - ToSAT * tosat; + //ToSATBase * tosat; // Checks if the counterexample is good. In order for the // counterexample to be ok, every assert must evaluate to true @@ -73,14 +73,21 @@ namespace BEEV //Converts a vector of bools to a BVConst ASTNode BoolVectoBVConst(HASHMAP * w, unsigned int l); + //Converts MINISAT counterexample into an AST memotable (i.e. the + //function populates the datastructure CounterExampleMap) + void ConstructCounterExample(MINISAT::Solver& newS, ToSATBase::ASTNodeToSATVar& satVarToSymbol); + + // Prints MINISAT assigment one bit at a time, for debugging. + void PrintSATModel(MINISAT::Solver& S, ToSATBase::ASTNodeToSATVar& satVarToSymbol); + + public: // Constructor AbsRefine_CounterExample(STPMgr * b, Simplifier * s, - ArrayTransformer * at, - ToSAT * t) : - bm(b), simp(s), ArrayTransform(at), tosat(t) + ArrayTransformer * at) : + bm(b), simp(s), ArrayTransform(at) { ASTTrue = bm->CreateNode(TRUE); ASTFalse = bm->CreateNode(FALSE); @@ -97,9 +104,6 @@ namespace BEEV ComputeFormulaMap.clear(); } - //Converts MINISAT counterexample into an AST memotable (i.e. the - //function populates the datastructure CounterExampleMap) - void ConstructCounterExample(MINISAT::Solver& S); //Prints the counterexample to stdout void PrintCounterExample(bool t, std::ostream& os = cout); @@ -128,16 +132,15 @@ namespace BEEV ASTNode ComputeFormulaUsingModel(const ASTNode& form); - // Prints MINISAT assigment one bit at a time, for debugging. - void PrintSATModel(MINISAT::Solver& S); - /**************************************************************** * Array Refinement functions * ****************************************************************/ SOLVER_RETURN_TYPE CallSAT_ResultCheck(MINISAT::Solver& SatSolver, const ASTNode& modified_input, - const ASTNode& original_input); + const ASTNode& original_input, + ToSATBase* tosat); + //creates array write axiom only for the input term or formula, if //necessary. If there are no axioms to produce then it simply //generates TRUE @@ -148,11 +151,13 @@ namespace BEEV SOLVER_RETURN_TYPE SATBased_ArrayReadRefinement(MINISAT::Solver& newS, const ASTNode& modified_input, - const ASTNode& original_input); + const ASTNode& original_input, + ToSATBase* tosat); SOLVER_RETURN_TYPE SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, - const ASTNode& orig_input); + const ASTNode& orig_input, + ToSATBase *tosat); // SOLVER_RETURN_TYPE // SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& newS, diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp index c051722..10b28e6 100644 --- a/src/absrefine_counterexample/AbstractionRefinement.cpp +++ b/src/absrefine_counterexample/AbstractionRefinement.cpp @@ -42,7 +42,8 @@ namespace BEEV AbsRefine_CounterExample:: SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, const ASTNode& inputAlreadyInSAT, - const ASTNode& original_input) { + const ASTNode& original_input, + ToSATBase* tosat) { //printf("doing array read refinement\n"); // if (!bm->UserFlags.arrayread_refinement_flag) // { @@ -153,7 +154,8 @@ namespace BEEV res2 = CallSAT_ResultCheck(SatSolver, FalseAxioms, - original_input); + original_input, + tosat); oldFalseAxiomsSize = FalseAxiomsVec.size(); } //printf("spot 02, res2 = %d\n", res2); @@ -169,7 +171,8 @@ namespace BEEV bm->ASTNodeStats("adding remaining readaxioms to SAT: ", RemainingAxioms); return CallSAT_ResultCheck(SatSolver, RemainingAxioms, - original_input); + original_input, + tosat); } //end of SATBased_ArrayReadRefinement @@ -181,7 +184,9 @@ namespace BEEV SOLVER_RETURN_TYPE AbsRefine_CounterExample:: SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, - const ASTNode& original_input) + const ASTNode& original_input, + ToSATBase *tosat + ) { ASTNode writeAxiom; ASTNodeMap::const_iterator it = simp->ReadOverWriteMap()->begin(); @@ -219,7 +224,8 @@ namespace BEEV { res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, - original_input); + original_input, + tosat); oldFalseAxiomsSize = FalseAxioms.size(); } if (SOLVER_UNDECIDED != res2) @@ -233,7 +239,8 @@ namespace BEEV bm->ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom); res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, - original_input); + original_input, + tosat); if (SOLVER_UNDECIDED != res2) { return res2; diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index 576a64e..5191713 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -10,6 +10,7 @@ #include "../sat/sat.h" #include "AbsRefine_CounterExample.h" #include "../printer/printers.h" +#include "../to-sat/AIG/ToSATAIG.h" const bool debug_counterexample = false; @@ -25,7 +26,8 @@ namespace BEEV * populate the CounterExampleMap data structure (ASTNode -> BVConst) */ void - AbsRefine_CounterExample::ConstructCounterExample(MINISAT::Solver& newS) + AbsRefine_CounterExample::ConstructCounterExample(MINISAT::Solver& newS, + ToSATBase::ASTNodeToSATVar& satVarToSymbol) { //iterate over MINISAT counterexample and construct a map from AST //terms to vector of bools. We need this iteration step because @@ -42,9 +44,8 @@ namespace BEEV CopySolverMap_To_CounterExample(); - ToSAT::ASTNodeToVar m = tosat->SATVar_to_SymbolIndexMap(); - - for (ToSAT::ASTNodeToVar::const_iterator it = m.begin(); it != m.end(); it++) + for (ToSATBase::ASTNodeToSATVar::const_iterator it = satVarToSymbol.begin(); it + != satVarToSymbol.end(); it++) { const ASTNode& symbol = it->first; const vector& v = it->second; @@ -106,7 +107,7 @@ namespace BEEV //iterate over the ASTNode_to_Bitvector data-struct and construct //the the aggregate value of the bitvector, and populate the //CounterExampleMap datastructure - for (ASTtoBitvectorMap::iterator it = _ASTNode_to_BitvectorMap.begin(), + for (ASTtoBitvectorMap::iterator it = _ASTNode_to_BitvectorMap.begin(), itend = _ASTNode_to_BitvectorMap.end(); it != itend; it++) { ASTNode var = it->first; @@ -114,8 +115,8 @@ namespace BEEV //cerr << var; if (SYMBOL != var.GetKind()) { - FatalError("ConstructCounterExample:"\ - "error while constructing counterexample: "\ + FatalError("ConstructCounterExample:" + "error while constructing counterexample: " "not a variable: ", var); } //construct the bitvector value @@ -132,10 +133,9 @@ namespace BEEV //In this loop, we compute the value of each array read, the //corresponding ITE against the counterexample generated above. - for (ASTNodeMap::const_iterator - it = ArrayTransform->ArrayRead_IteMap()->begin(), - itend = ArrayTransform->ArrayRead_IteMap()->end(); - it != itend; it++) + for (ASTNodeMap::const_iterator it = + ArrayTransform->ArrayRead_IteMap()->begin(), itend = + ArrayTransform->ArrayRead_IteMap()->end(); it != itend; it++) { //the array read ASTNode arrayread = it->first; @@ -146,8 +146,7 @@ namespace BEEV //construct the appropriate array-read and store it in the //counterexample ASTNode arrayread_index = TermToConstTermUsingModel(arrayread[1]); - ASTNode key = bm->CreateTerm(READ, - arrayread.GetValueWidth(), + ASTNode key = bm->CreateTerm(READ, arrayread.GetValueWidth(), arrayread[0], arrayread_index); //Get the ITE corresponding to the array-read and convert it @@ -181,9 +180,9 @@ namespace BEEV //4. If (the boolean variable 'ArrayReadFlag' is false) && ArrayRead //4. doesn't have a value in the counterexample then return 0 as the //4. value of the arrayread. - ASTNode - AbsRefine_CounterExample:: - TermToConstTermUsingModel(const ASTNode& t, bool ArrayReadFlag) + ASTNode + AbsRefine_CounterExample::TermToConstTermUsingModel(const ASTNode& t, + bool ArrayReadFlag) { bm->Begin_RemoveWrites = false; bm->SimplifyWrites_InPlace_Flag = false; @@ -194,21 +193,18 @@ namespace BEEV //cerr << "Input to TermToConstTermUsingModel: " << term << endl; if (!is_Term_kind(k)) { - FatalError("TermToConstTermUsingModel: "\ - "The input is not a term: ", - term); + FatalError("TermToConstTermUsingModel: " + "The input is not a term: ", term); } if (k == WRITE) { - FatalError("TermToConstTermUsingModel: "\ - "The input has wrong kind: WRITE : ", - term); + FatalError("TermToConstTermUsingModel: " + "The input has wrong kind: WRITE : ", term); } if (k == SYMBOL && BOOLEAN_TYPE == term.GetType()) { - FatalError("TermToConstTermUsingModel: "\ - "The input has wrong kind: Propositional variable : ", - term); + FatalError("TermToConstTermUsingModel: " + "The input has wrong kind: Propositional variable : ", term); } ASTNodeMap::iterator it1; @@ -228,10 +224,9 @@ namespace BEEV //the value part of the map if (term == val) { - FatalError("TermToConstTermUsingModel: "\ + FatalError("TermToConstTermUsingModel: " "The input term is stored as-is " - "in the CounterExample: Not ok: ", - term); + "in the CounterExample: Not ok: ", term); } return TermToConstTermUsingModel(val, ArrayReadFlag); } @@ -264,64 +259,53 @@ namespace BEEV ASTNode index = term[1]; if (0 == arrName.GetIndexWidth()) { - FatalError("TermToConstTermUsingModel: "\ + FatalError("TermToConstTermUsingModel: " "array has 0 index width: ", arrName); } - if (WRITE == arrName.GetKind()) //READ over a WRITE { - ASTNode wrtterm = - Expand_ReadOverWrite_UsingModel(term, ArrayReadFlag); + ASTNode wrtterm = Expand_ReadOverWrite_UsingModel(term, + ArrayReadFlag); if (wrtterm == term) { - FatalError("TermToConstTermUsingModel: "\ - "Read_Over_Write term must be expanded "\ + FatalError("TermToConstTermUsingModel: " + "Read_Over_Write term must be expanded " "into an ITE", term); } - ASTNode rtterm = - TermToConstTermUsingModel(wrtterm, ArrayReadFlag); + ASTNode rtterm = TermToConstTermUsingModel(wrtterm, ArrayReadFlag); assert(ArrayReadFlag || (BVCONST == rtterm.GetKind())); return rtterm; } else if (ITE == arrName.GetKind()) //READ over an ITE { // The "then" and "else" branch are arrays. - ASTNode indexVal = - TermToConstTermUsingModel(index, ArrayReadFlag); + ASTNode indexVal = TermToConstTermUsingModel(index, ArrayReadFlag); - ASTNode condcompute = - ComputeFormulaUsingModel(arrName[0]); // Get the truth value. + ASTNode condcompute = ComputeFormulaUsingModel(arrName[0]); // Get the truth value. unsigned int wid = arrName.GetValueWidth(); if (ASTTrue == condcompute) { - const ASTNode & result = - TermToConstTermUsingModel(bm->CreateTerm(READ, - wid, - arrName[1], - indexVal), + const ASTNode & result = TermToConstTermUsingModel( + bm->CreateTerm(READ, wid, arrName[1], indexVal), ArrayReadFlag); assert(ArrayReadFlag || (BVCONST == result.GetKind())); return result; } else if (ASTFalse == condcompute) { - const ASTNode & result = - TermToConstTermUsingModel(bm->CreateTerm(READ, - wid, - arrName[2], - indexVal), + const ASTNode & result = TermToConstTermUsingModel( + bm->CreateTerm(READ, wid, arrName[2], indexVal), ArrayReadFlag); assert(ArrayReadFlag || (BVCONST == result.GetKind())); return result; } else { - cerr << "TermToConstTermUsingModel: termITE: "\ + cerr << "TermToConstTermUsingModel: termITE: " "value of conditional is wrong: " << condcompute << endl; - FatalError(" TermToConstTermUsingModel: termITE: "\ - "cannot compute ITE conditional against model: ", - term); + FatalError(" TermToConstTermUsingModel: termITE: " + "cannot compute ITE conditional against model: ", term); } FatalError("bn23143 Never Here"); } @@ -331,24 +315,21 @@ namespace BEEV { //index has a const value in the CounterExampleMap //ASTNode indexVal = CounterExampleMap[index]; - ASTNode indexVal = - TermToConstTermUsingModel(CounterExampleMap[index], - ArrayReadFlag); - modelentry = - bm->CreateTerm(READ, arrName.GetValueWidth(), - arrName, indexVal); + ASTNode indexVal = TermToConstTermUsingModel( + CounterExampleMap[index], ArrayReadFlag); + modelentry = bm->CreateTerm(READ, arrName.GetValueWidth(), arrName, + indexVal); } else { //index does not have a const value in the //CounterExampleMap. compute it. - ASTNode indexconstval = - TermToConstTermUsingModel(index, ArrayReadFlag); + ASTNode indexconstval = TermToConstTermUsingModel(index, + ArrayReadFlag); //update model with value of the index //CounterExampleMap[index] = indexconstval; - modelentry = - bm->CreateTerm(READ, arrName.GetValueWidth(), - arrName, indexconstval); + modelentry = bm->CreateTerm(READ, arrName.GetValueWidth(), arrName, + indexconstval); } //modelentry is now an arrayread over a constant index BVTypeCheck(modelentry); @@ -356,8 +337,7 @@ namespace BEEV //if a value exists in the CounterExampleMap then return it if (CounterExampleMap.find(modelentry) != CounterExampleMap.end()) { - output = - TermToConstTermUsingModel(CounterExampleMap[modelentry], + output = TermToConstTermUsingModel(CounterExampleMap[modelentry], ArrayReadFlag); } else if (ArrayReadFlag) @@ -367,8 +347,8 @@ namespace BEEV } else { - // Has been simplified out. Can take any value. - output = bm->CreateMaxConst(modelentry.GetValueWidth()); + // Has been simplified out. Can take any value. + output = bm->CreateMaxConst(modelentry.GetValueWidth()); } break; } @@ -386,9 +366,8 @@ namespace BEEV else { cerr << "TermToConstTermUsingModel: termITE: " - << "value of conditional is wrong: " - << condcompute << endl; - FatalError(" TermToConstTermUsingModel: termITE: cannot "\ + << "value of conditional is wrong: " << condcompute << endl; + FatalError(" TermToConstTermUsingModel: termITE: cannot " "compute ITE conditional against model: ", term); } break; @@ -397,9 +376,9 @@ namespace BEEV { const ASTVec& c = term.GetChildren(); ASTVec o; - o.reserve(c.size()); - for (ASTVec::const_iterator - it = c.begin(), itend = c.end(); it != itend; it++) + o.reserve(c.size()); + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it + != itend; it++) { ASTNode ff = TermToConstTermUsingModel(*it, ArrayReadFlag); o.push_back(ff); @@ -432,11 +411,10 @@ namespace BEEV //every writeindex until, either it evaluates to TRUE or all //(readIndex=writeIndex) evaluate to FALSE ASTNode - AbsRefine_CounterExample:: - Expand_ReadOverWrite_UsingModel(const ASTNode& term, bool arrayread_flag) + AbsRefine_CounterExample::Expand_ReadOverWrite_UsingModel( + const ASTNode& term, bool arrayread_flag) { - if (READ != term.GetKind() - || WRITE != term[0].GetKind()) + if (READ != term.GetKind() || WRITE != term[0].GetKind()) { FatalError("RemovesWrites: Input must be a READ over a WRITE", term); } @@ -453,7 +431,7 @@ namespace BEEV //of a key in the substitutionmap is always a constant. if (term == val) { - FatalError("TermToConstTermUsingModel: The input term is "\ + FatalError("TermToConstTermUsingModel: The input term is " "stored as-is " "in the CounterExample: Not ok: ", term); } @@ -483,7 +461,8 @@ namespace BEEV } write = write[0]; - } while (WRITE == write.GetKind()); + } + while (WRITE == write.GetKind()); const unsigned int width = term.GetValueWidth(); newRead = bm->CreateTerm(READ, width, write, readIndex); @@ -497,14 +476,14 @@ namespace BEEV /* FUNCTION: accepts a non-constant formula, and checks if the * formula is ASTTrue or ASTFalse w.r.t to a model */ - ASTNode + 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())) { - FatalError(" ComputeConstFormUsingModel: "\ + FatalError(" ComputeConstFormUsingModel: " "The input is a non-formula: ", form); } @@ -519,7 +498,7 @@ namespace BEEV } else { - FatalError("ComputeFormulaUsingModel: "\ + FatalError("ComputeFormulaUsingModel: " "The value of a formula must be TRUE or FALSE:", form); } } @@ -533,7 +512,7 @@ namespace BEEV break; case SYMBOL: if (BOOLEAN_TYPE != form.GetType()) - FatalError(" ComputeFormulaUsingModel: "\ + FatalError(" ComputeFormulaUsingModel: " "Non-Boolean variables are not formulas", form); if (CounterExampleMap.find(form) != CounterExampleMap.end()) { @@ -561,25 +540,28 @@ namespace BEEV case BVSLT: case BVSLE: case BVSGT: - case BVSGE: { - ASTVec children; - children.reserve(form.Degree()); + case BVSGE: + { + ASTVec children; + children.reserve(form.Degree()); - for (ASTVec::const_iterator it = form.begin(), itend = form.end(); it - != itend; it++) { - children.push_back(TermToConstTermUsingModel(*it, false)); - } + 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 = simp->BVConstEvaluator(bm->CreateNode(k, children)); - //evaluate formula to false if bvdiv execption occurs while - //counterexample is being checked during refinement. - if (bm->bvdiv_exception_occured - && bm->counterexample_checking_during_refinement) { - output = ASTFalse; - } + //evaluate formula to false if bvdiv execption occurs while + //counterexample is being checked during refinement. + if (bm->bvdiv_exception_occured + && bm->counterexample_checking_during_refinement) + { + output = ASTFalse; + } - } + } break; case NAND: @@ -590,14 +572,15 @@ namespace BEEV case IFF: case IMPLIES: case OR: - { - ASTVec children; - children.reserve(form.Degree()); + { + ASTVec children; + children.reserve(form.Degree()); - for (ASTVec::const_iterator it = form.begin(), itend = form.end(); it != itend; it++) - { - children.push_back( ComputeFormulaUsingModel(*it)); - } + for (ASTVec::const_iterator it = form.begin(), itend = form.end(); it + != itend; it++) + { + children.push_back( ComputeFormulaUsingModel(*it)); + } output = simp->BVConstEvaluator(bm->CreateNode(k, children)); @@ -609,7 +592,7 @@ namespace BEEV output = ASTFalse; } - } + } break; case ITE: @@ -620,7 +603,7 @@ namespace BEEV else if (ASTFalse == t0) output = ComputeFormulaUsingModel(form[2]); else - FatalError("ComputeFormulaUsingModel: ITE: "\ + FatalError("ComputeFormulaUsingModel: ITE: " "something is wrong with the formula: ", form); } break; @@ -629,12 +612,12 @@ namespace BEEV output = ComputeFormulaUsingModel(output); break; case FOR: - //output = Check_FiniteLoop_UsingModel(form); + //output = Check_FiniteLoop_UsingModel(form); output = ASTTrue; break; default: - cerr << _kind_names[k]; - FatalError(" ComputeFormulaUsingModel: "\ + cerr << _kind_names[k]; + FatalError(" ComputeFormulaUsingModel: " "the kind has not been implemented", ASTUndefined); break; } @@ -646,7 +629,8 @@ namespace BEEV return output; } - void AbsRefine_CounterExample::CheckCounterExample(bool t) + void + AbsRefine_CounterExample::CheckCounterExample(bool t) { //input is valid, no counterexample to check if (bm->ValidFlag) @@ -654,36 +638,36 @@ namespace BEEV //t is true if SAT solver generated a counterexample, else it is false if (!t) - FatalError("CheckCounterExample: "\ + FatalError("CheckCounterExample: " "No CounterExample to check", ASTUndefined); const ASTVec c = bm->GetAsserts(); if (bm->UserFlags.stats_flag) - printf("checking counterexample\n"); + printf("checking counterexample\n"); - for (ASTVec::const_iterator - it = c.begin(), itend = c.end(); it != itend; it++) + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) { - if (debug_counterexample) - cerr << "checking" << *it; + if (debug_counterexample) + cerr << "checking" << *it; if (ASTFalse == ComputeFormulaUsingModel(*it)) FatalError("CheckCounterExample:counterexample bogus:" - "assert evaluates to FALSE under counterexample: "\ + "assert evaluates to FALSE under counterexample: " "NOT OK", *it); } // The smtlib ones don't have a query defined. - if ((bm->GetQuery() != ASTUndefined) && ASTTrue == ComputeFormulaUsingModel(bm->GetQuery())) + if ((bm->GetQuery() != ASTUndefined) && ASTTrue + == ComputeFormulaUsingModel(bm->GetQuery())) FatalError("CheckCounterExample:counterexample bogus:" - "query evaluates to TRUE under counterexample: "\ + "query evaluates to TRUE under counterexample: " "NOT OK", bm->GetQuery()); } /* FUNCTION: queries the CounterExampleMap object with 'expr' and * returns the corresponding counterexample value. */ - ASTNode + ASTNode AbsRefine_CounterExample::GetCounterExample(bool t, const ASTNode& expr) { //input is valid, no counterexample to get @@ -712,7 +696,8 @@ namespace BEEV // FUNCTION: prints a counterexample for INVALID inputs. iterate // through the CounterExampleMap data structure and print it to // stdout - void AbsRefine_CounterExample::PrintCounterExample(bool t, std::ostream& os) + void + AbsRefine_CounterExample::PrintCounterExample(bool t, std::ostream& os) { //input is valid, no counterexample to print if (bm->ValidFlag) @@ -754,40 +739,38 @@ namespace BEEV if (ARRAY_TYPE == se.GetType()) { - FatalError("TermToConstTermUsingModel: "\ + FatalError("TermToConstTermUsingModel: " "entry in counterexample is an arraytype. bogus:", se); } //skip over introduced variables - if (f.GetKind() == SYMBOL && - (ArrayTransform->FoundIntroducedSymbolSet(f))) + if (f.GetKind() == SYMBOL && (ArrayTransform->FoundIntroducedSymbolSet( + f))) { continue; } - if (f.GetKind() == SYMBOL || - (f.GetKind() == READ && - f[0].GetKind() == SYMBOL && - f[1].GetKind() == BVCONST)) + if (f.GetKind() == SYMBOL || (f.GetKind() == READ && f[0].GetKind() + == SYMBOL && f[1].GetKind() == BVCONST)) { os << "ASSERT( "; printer::PL_Print1(os,f,0,false); - if(BOOLEAN_TYPE == f.GetType()) + if(BOOLEAN_TYPE == f.GetType()) { os << "<=>"; } - else + else { os << " = "; } if (BITVECTOR_TYPE == se.GetType()) { - ASTNode rhs = TermToConstTermUsingModel(se, false); - assert(rhs.isConstant()); - printer::PL_Print1(os,rhs,0,false); + ASTNode rhs = TermToConstTermUsingModel(se, false); + assert(rhs.isConstant()); + printer::PL_Print1(os,rhs,0,false); } else { - printer::PL_Print1(os,se,0,false); + printer::PL_Print1(os,se,0,false); } os << " );" << endl; } @@ -804,7 +787,8 @@ namespace BEEV * not print anything. This function was specifically written for * Dawson Engler's group (bug finding research group at Stanford) */ - void AbsRefine_CounterExample::PrintCounterExample_InOrder(bool t) + void + AbsRefine_CounterExample::PrintCounterExample_InOrder(bool t) { //global command-line option to print counterexample. we do not //want both counterexample printers to print at the sametime. @@ -833,8 +817,8 @@ namespace BEEV //vector to store the integer values std::vector out_int; cout << "% "; - for (ASTVec::iterator it = bm->ListOfDeclaredVars.begin(), - itend = bm->ListOfDeclaredVars.end(); it != itend; it++) + for (ASTVec::iterator it = bm->ListOfDeclaredVars.begin(), itend = + bm->ListOfDeclaredVars.end(); it != itend; it++) { if (ARRAY_TYPE == it->GetType()) { @@ -858,12 +842,10 @@ namespace BEEV it->PL_Print(cout, 2); for (int j = 0; j < n; j++) { - ASTNode index = - bm->CreateBVConst(it->GetIndexWidth(), j); - ASTNode readexpr = - bm->CreateTerm(READ, it->GetValueWidth(), *it, index); - ASTNode val = - GetCounterExample(t, readexpr); + ASTNode index = bm->CreateBVConst(it->GetIndexWidth(), j); + ASTNode readexpr = bm->CreateTerm(READ, it->GetValueWidth(), + *it, index); + ASTNode val = GetCounterExample(t, readexpr); //cout << "ASSERT( "; //cout << " = "; out_int.push_back(val.GetUnsignedConst()); @@ -878,18 +860,17 @@ namespace BEEV } //End of PrintCounterExample_InOrder // Prints Satisfying assignment directly, for debugging. - void AbsRefine_CounterExample::PrintSATModel(MINISAT::Solver& newS) + void + AbsRefine_CounterExample::PrintSATModel(MINISAT::Solver& newS, + ToSATBase::ASTNodeToSATVar& m) { if (!newS.okay()) FatalError("PrintSATModel: NO COUNTEREXAMPLE TO PRINT", ASTUndefined); - if (!(bm->UserFlags.stats_flag - && bm->UserFlags.print_nodes_flag)) + if (!(bm->UserFlags.stats_flag && bm->UserFlags.print_nodes_flag)) return; - ToSAT::ASTNodeToVar m = tosat->SATVar_to_SymbolIndexMap(); - cout << "Satisfying assignment: " << endl; - for (ToSAT::ASTNodeToVar::const_iterator it= m.begin(); it != m.end();it++) + for (ToSATBase::ASTNodeToSATVar::const_iterator it = m.begin(); it != m.end(); it++) { ASTNode symbol = it->first; vector v = it->second; @@ -915,14 +896,13 @@ namespace BEEV } //end of PrintSATModel() //FUNCTION: this function accepts a boolvector and returns a BVConst - ASTNode - AbsRefine_CounterExample:: - BoolVectoBVConst(HASHMAP * w, unsigned int l) + ASTNode + AbsRefine_CounterExample::BoolVectoBVConst(HASHMAP * w, + unsigned int l) { if (l < (unsigned)w->size()) FatalError("BoolVectorBVConst : " - "length of bitvector does not match HASHMAP size:", - ASTUndefined, l); + "length of bitvector does not match HASHMAP size:", ASTUndefined, l); CBV cc = CONSTANTBV::BitVector_Create(l,true); for (unsigned int jj = 0; jj < l; jj++) @@ -930,30 +910,30 @@ namespace BEEV if ((*w)[jj] == true) CONSTANTBV::BitVector_Bit_On(cc,l-1-jj); else - CONSTANTBV::BitVector_Bit_Off(cc,l-1-jj); + CONSTANTBV::BitVector_Bit_Off(cc,l-1-jj); } return bm->CreateBVConst(cc,l); } //end of BoolVectoBVConst() - void AbsRefine_CounterExample::CopySolverMap_To_CounterExample(void) + void + AbsRefine_CounterExample::CopySolverMap_To_CounterExample(void) { - + if (!simp->Return_SolverMap()->empty()) { - CounterExampleMap.insert(simp->Return_SolverMap()->begin(), + CounterExampleMap.insert(simp->Return_SolverMap()->begin(), simp->Return_SolverMap()->end()); } } - SOLVER_RETURN_TYPE - AbsRefine_CounterExample:: - CallSAT_ResultCheck(MINISAT::Solver& SatSolver, - const ASTNode& modified_input, - const ASTNode& original_input) + SOLVER_RETURN_TYPE + AbsRefine_CounterExample::CallSAT_ResultCheck(MINISAT::Solver& SatSolver, + const ASTNode& modified_input, const ASTNode& original_input, ToSATBase* tosat) { - bool sat = tosat->CallSAT(SatSolver, - modified_input); + + bool sat = tosat->CallSAT(SatSolver, modified_input); + if (!sat) { //PrintOutput(true); @@ -961,13 +941,16 @@ namespace BEEV } else if (SatSolver.okay()) { - bm->GetRunTimes()->start(RunTimes::CounterExampleGeneration); - CounterExampleMap.clear(); - ConstructCounterExample(SatSolver); - if (bm->UserFlags.stats_flag - && bm->UserFlags.print_nodes_flag) + bm->GetRunTimes()->start(RunTimes::CounterExampleGeneration); + CounterExampleMap.clear(); + + ToSAT::ASTNodeToSATVar satVarToSymbol = + tosat->SATVar_to_SymbolIndexMap(); + ConstructCounterExample(SatSolver, satVarToSymbol); + if (bm->UserFlags.stats_flag && bm->UserFlags.print_nodes_flag) { - PrintSATModel(SatSolver); + ToSAT::ASTNodeToSATVar m = tosat->SATVar_to_SymbolIndexMap(); + PrintSATModel(SatSolver, m); } //check if the counterexample is good or not ComputeFormulaMap.clear(); @@ -975,7 +958,7 @@ namespace BEEV bm->bvdiv_exception_occured = false; ASTNode orig_result = ComputeFormulaUsingModel(original_input); if (!(ASTTrue == orig_result || ASTFalse == orig_result)) - FatalError("TopLevelSat: Original input must compute to "\ + FatalError("TopLevelSat: Original input must compute to " "true or false against model"); bm->GetRunTimes()->stop(RunTimes::CounterExampleGeneration); @@ -985,21 +968,20 @@ namespace BEEV if (ASTTrue == orig_result) { if (bm->UserFlags.check_counterexample_flag) - CheckCounterExample(SatSolver.okay()); + CheckCounterExample(SatSolver.okay()); - if (bm->UserFlags.stats_flag || bm->UserFlags.print_counterexample_flag) + if (bm->UserFlags.stats_flag + || bm->UserFlags.print_counterexample_flag) { PrintCounterExample(SatSolver.okay()); PrintCounterExample_InOrder(SatSolver.okay()); } - return SOLVER_INVALID; } // counterexample is bogus: flag it else { - if (bm->UserFlags.stats_flag - && bm->UserFlags.print_nodes_flag) + if (bm->UserFlags.stats_flag && bm->UserFlags.print_nodes_flag) { cout << "Supposedly bogus one: \n"; PrintCounterExample(true); @@ -1015,4 +997,5 @@ namespace BEEV return SOLVER_ERROR; } } //end of CALLSAT_ResultCheck() -}; +} +; diff --git a/src/absrefine_counterexample/Makefile b/src/absrefine_counterexample/Makefile index bce9db9..89d91a5 100644 --- a/src/absrefine_counterexample/Makefile +++ b/src/absrefine_counterexample/Makefile @@ -15,4 +15,4 @@ clean: depend: $(SRCS) @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ -#-include depend \ No newline at end of file +-include depend \ No newline at end of file diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index fc6111c..a352dd8 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -165,8 +165,8 @@ VC vc_createValidityChecker(void) { BEEV::AbsRefine_CounterExample * Ctr_Example = new BEEV::AbsRefine_CounterExample(bm, simp, - arrayTransformer, - tosat); + arrayTransformer + ); BEEV::ParserBM = bm; stpstar stp = diff --git a/src/main/main.cpp b/src/main/main.cpp index f1d7a35..0342196 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -83,7 +83,7 @@ int main(int argc, char ** argv) { ArrayTransformer * arrayTransformer = new ArrayTransformer(bm, simp); ToSAT * tosat = new ToSAT(bm); AbsRefine_CounterExample * Ctr_Example = - new AbsRefine_CounterExample(bm, simp, arrayTransformer, tosat); + new AbsRefine_CounterExample(bm, simp, arrayTransformer); itimerval timeout; ParserBM = bm; diff --git a/src/to-sat/AIG/BBNodeAIG.h b/src/to-sat/AIG/BBNodeAIG.h index c050131..425325e 100644 --- a/src/to-sat/AIG/BBNodeAIG.h +++ b/src/to-sat/AIG/BBNodeAIG.h @@ -16,12 +16,47 @@ namespace BEEV { // This class wraps around a pointer to an AIG (provided by the ABC tool). + // uses the default copy constructor and assignment operator. class BBNodeAIG { + // This is only useful for printing small instances for debuging. + void print(Aig_Obj_t* node) const + { + Aig_Obj_t *c0 = node->pFanin0, *c1 = node->pFanin1; + bool c0Not = Aig_IsComplement(c0), c1Not = Aig_IsComplement(c1); + if (c0Not) + c0 = Aig_Not(c0); + if (c1Not) + c1 = Aig_Not(c1); + cerr << node->Id; + cerr << "[" << node->Type << "]"; + cerr << ": ("; + if (c0 !=0 ) + { + if (c0Not) + cerr << "-"; + cerr << c0->Id; + cerr <<","; + } + if (c1 !=0 ) + { + if (c1Not) + cerr << "-"; + + cerr << c1->Id; + } + cerr << ")" << endl; + if (c0 !=0 ) + print(c0); + if (c1 !=0 ) + print(c1); + } public: + // If the pointer is odd. Then it's the NOT of the pointer one less. Aig_Obj_t * n; + BBNodeAIG() { n = NULL; @@ -30,6 +65,15 @@ public: BBNodeAIG(Aig_Obj_t * _n) { n = _n; + assert(n!=NULL); + if (Aig_IsComplement(n)) + { + assert(Aig_Not(n)->Type != 0); // don't want nodes of type UNKNOWN> + } + else + { + assert(n->Type!=0); + } } bool IsNull() const @@ -53,12 +97,14 @@ public: return n < other.n; } -}; -std::ostream& operator<<(std::ostream& output, const BBNodeAIG& h) + + + void print() const { - FatalError("This isn't implemented yet sorry;"); - return output; + print(n); } + +}; } ; diff --git a/src/to-sat/AIG/BBNodeManagerAIG.h b/src/to-sat/AIG/BBNodeManagerAIG.h index 2c1afb8..94f6f6d 100644 --- a/src/to-sat/AIG/BBNodeManagerAIG.h +++ b/src/to-sat/AIG/BBNodeManagerAIG.h @@ -71,9 +71,14 @@ class BBNodeManagerAIG return t(aigMgr, a, b); } + // no copy. no assignment. + BBNodeManagerAIG& operator = (const BBNodeManagerAIG& other); + BBNodeManagerAIG(const BBNodeManagerAIG& other); + + public: - BBNodeManagerAIG(STPMgr*& _stp) + BBNodeManagerAIG() { aigMgr = Aig_ManStart(0); // fancier strashing. @@ -87,27 +92,16 @@ public: BBNodeAIG getTrue() { - return BBNodeAIG((aigMgr->pConst1)); + return BBNodeAIG(Aig_ManConst1(aigMgr)); } BBNodeAIG getFalse() { - return BBNodeAIG(Aig_Not(aigMgr->pConst1)); + return BBNodeAIG(Aig_ManConst0(aigMgr)); } - void - toCNF(BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToVar& nodeToVar) + void toCNF_experimental(BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar) { - assert(cnfData == NULL); - - Aig_Man_t *aigMgr; - - 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); - //cerr << "SAFDASDF"; // copied from darScript.c: Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig ) @@ -134,9 +128,22 @@ public: //Dar_RwrPar_t pPars; //Dar_ManDefaultRwrParams( &pPars ); //Dar_ManRewrite( aigMgr, &pPars ); + } + void + toCNF(BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToSATVar& nodeToVar) + { + assert(cnfData == NULL); + assert(nodeToVar.size() ==0); + + 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); - // Cnf_Derive seems more advanced, but gives assertion errors sometimes. + // Cnf_Derive gives errors sometimes. + //cnfData = Cnf_DeriveSimple(aigMgr, 0); cnfData = Cnf_Derive(aigMgr, 0); BBNodeManagerAIG::SymbolToBBNode::const_iterator it; @@ -157,6 +164,7 @@ public: vector& v = nodeToVar[n]; for (unsigned i = 0; i < b.size(); i++) { + if (!b[i].IsNull()) v[i] = cnfData->pVarNums[b[i].n->Id]; } } @@ -194,11 +202,14 @@ public: BBNodeAIG CreateNode(Kind kind, vector& children) { Aig_Obj_t * pNode; + assert (children.size() != 0); + + for (int i =0; i < children.size();i++) + assert(!children[i].IsNull()); switch (kind) { case AND: - assert (children.size() != 0); if (children.size() == 1) pNode = children[0].n; else if (children.size() == 2) @@ -208,7 +219,9 @@ public: break; case OR: - if (children.size() == 2) + if (children.size() == 1) + pNode = children[0].n; + else if (children.size() == 2) pNode = Aig_Or(aigMgr, children[0].n, children[1].n); else pNode = makeTower(Aig_Or, children); @@ -233,8 +246,10 @@ public: pNode = Aig_Not(pNode); break; case XOR: - assert(children.size() ==2); + if (children.size() == 2) pNode = Aig_Exor(aigMgr, children[0].n, children[1].n); + else + pNode = makeTower(Aig_Exor, children); break; case IFF: assert(children.size() ==2); diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h index b36ce40..424c6ba 100644 --- a/src/to-sat/AIG/ToSATAIG.h +++ b/src/to-sat/AIG/ToSATAIG.h @@ -11,22 +11,26 @@ #define TOSATAIG_H #include -#include "ToCNF.h" - #include "../AST/AST.h" #include "../AST/RunTimes.h" #include "../STPManager/STPManager.h" -#include "BitBlaster.h" +#include "../BitBlaster.h" #include "BBNodeManagerAIG.h" namespace BEEV { + // NB You can't use this with abstraction refinement!!! class ToSATAIG : public ToSATBase { private: - ASTNodeToVar nodeToVar; + ASTNodeToSATVar nodeToSATVar; + + // don't assign or copy construct. + ToSATAIG& operator = (const ToSATAIG& other); + ToSATAIG(const ToSATAIG& other); + public: ToSATAIG(STPMgr * bm) : @@ -34,37 +38,82 @@ namespace BEEV { } - void ClearAllTables() + void + ClearAllTables() { - nodeToVar.clear(); + nodeToSATVar.clear(); } - ASTNodeToVar& SATVar_to_SymbolIndexMap() + // Used to read out the satisfiable answer. + ASTNodeToSATVar& + SATVar_to_SymbolIndexMap() { - return nodeToVar; + return nodeToSATVar; } + // Can not be used with abstraction refinement. bool - CallSAT(MINISAT::Solver& SatSolver, const ASTNode& input) + CallSAT(MINISAT::Solver& satSolver, const ASTNode& input) { - BBNodeManagerAIG mgr(bm); - BitBlasterNew bb(bm); - BitBlasterNew::BBNodeSet support; + BBNodeManagerAIG mgr; + BitBlaster bb(&mgr); + set support; + BBNodeAIG BBFormula = bb.BBForm(input, support); + assert(support.size() ==0); // hot handled yet.. + assert(satSolver.nVars() ==0); + Cnf_Dat_t* cnfData = NULL; - mgr.toCNF(BBFormula, cnfData, nodeToVar); + mgr.toCNF(BBFormula, cnfData, nodeToSATVar); + + bm->GetRunTimes()->start(RunTimes::SendingToSAT); + + for (int i = 0; i < cnfData->nVars; i++) + satSolver.newVar(); + + MINISAT::vec satSolverClause; + for (int i = 0; i < cnfData->nClauses; i++) + { + satSolverClause.clear(); + for (int * pLit = cnfData->pClauses[i], *pStop = cnfData->pClauses[i + + 1]; pLit < pStop; pLit++) + { + Var var = (*pLit) >> 1; + assert(var < satSolver.nVars()); + MINISAT::Lit l(var, (*pLit) & 1); + satSolverClause.push(l); + } + + satSolver.addClause(satSolverClause); + if (!satSolver.okay()) + break; + } + bm->GetRunTimes()->stop(RunTimes::SendingToSAT); + + if (bm->UserFlags.output_CNF_flag) + Cnf_DataWriteIntoFile(cnfData, "output.cnf", 0); Cnf_ClearMemory(); Cnf_DataFree(cnfData); - // TO DO Solve. - // TODO Return the answer - FatalError("not implemented"); + bm->GetRunTimes()->start(RunTimes::SATSimplifying); + if (!satSolver.simplify()) + { + bm->GetRunTimes()->stop(RunTimes::SATSimplifying); return false; + } + bm->GetRunTimes()->stop(RunTimes::SATSimplifying); + + bm->GetRunTimes()->start(RunTimes::Solving); + satSolver.solve(); + bm->GetRunTimes()->stop(RunTimes::Solving); + if (bm->UserFlags.stats_flag) + bm->PrintStats(satSolver); + return satSolver.okay(); } }; } diff --git a/src/to-sat/BBNodeManagerASTNode.h b/src/to-sat/BBNodeManagerASTNode.h index 09a29f7..8011a41 100644 --- a/src/to-sat/BBNodeManagerASTNode.h +++ b/src/to-sat/BBNodeManagerASTNode.h @@ -13,6 +13,10 @@ class BBNodeManagerASTNode { ASTNode ASTTrue, ASTFalse; STPMgr *stp; + //no copy, no assign. + BBNodeManagerASTNode& operator = (const BBNodeManagerASTNode& other); + BBNodeManagerASTNode(const BBNodeManagerASTNode& other); + public: BBNodeManagerASTNode(STPMgr *_stp) { diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index 38234eb..73e2a05 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -1263,6 +1263,12 @@ BBNode BitBlaster::BBEQ(const BBNodeVec& left, const BBNo template class BitBlaster; template class BitBlaster; +std::ostream& operator<<(std::ostream& output, const BBNodeAIG& h) +{ + FatalError("This isn't implemented yet sorry;"); + return output; +} + #undef BBNodeVec #undef BBNodeVecMap #undef BBNodeSet diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index 93e9e70..e3e747d 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -89,7 +89,7 @@ private: // This implements a variant of binary long division. // q and r are "out" parameters. rwidth puts a bound on the // recursion depth. Unsigned only, for now. -public: + void BBDivMod(const vector &y, const vector &x, vector &q, vector &r, unsigned int rwidth, set& support); @@ -106,6 +106,11 @@ public: void BBLShift(vector& x, unsigned int shift); void BBRShift(vector& x, unsigned int shift); + // no copy, no assign. + BitBlaster& operator = (const BitBlaster& other); + BitBlaster(const BitBlaster& other); + + public: BBNodeManagerT* nf; @@ -114,21 +119,19 @@ public: // representing the boolean formula. const vector BBTerm(const ASTNode& term, set& support); -public: - /**************************************************************** * Public Member Functions * ****************************************************************/ - BitBlaster(STPMgr * bm) + BitBlaster(BBNodeManagerT* bnm) { - nf = new BBNodeManagerT(bm); + nf = bnm; } + ~BitBlaster() { BBTermMemo.clear(); BBFormMemo.clear(); - delete nf; } //Bitblast a formula diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 9f0c952..69770ef 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -345,7 +345,8 @@ namespace BEEV ASTNode BBFormula; { - BitBlaster BB(bm); + BBNodeManagerASTNode nm(bm); + BitBlaster BB(&nm); set set; BBFormula = BB.BBForm(input,set); assert(set.size() == 0); // doesn't yet work. diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h index a66858a..5b6002a 100644 --- a/src/to-sat/ToSAT.h +++ b/src/to-sat/ToSAT.h @@ -45,7 +45,7 @@ namespace BEEV // Reverse map used in building counterexamples. MINISAT returns a // model in terms of MINISAT Vars, and this map helps us convert // it to a model over ASTNode variables. - ASTNodeToVar SATVar_to_SymbolIndex; + ASTNodeToSATVar SATVar_to_SymbolIndex; int CNFFileNameCounter; int benchFileNameCounter; @@ -94,7 +94,7 @@ namespace BEEV bool CallSAT(MINISAT::Solver& SatSolver, const ASTNode& input); - ASTNodeToVar& SATVar_to_SymbolIndexMap() + ASTNodeToSATVar& SATVar_to_SymbolIndexMap() { return SATVar_to_SymbolIndex; } diff --git a/src/to-sat/ToSATBase.h b/src/to-sat/ToSATBase.h index 97292ff..17e84b7 100644 --- a/src/to-sat/ToSATBase.h +++ b/src/to-sat/ToSATBase.h @@ -20,7 +20,7 @@ namespace BEEV ASTNode, vector, ASTNode::ASTNodeHasher, - ASTNode::ASTNodeEqual> ASTNodeToVar; + ASTNode::ASTNodeEqual> ASTNodeToSATVar; // Constructor ToSATBase(STPMgr * bm) : @@ -40,7 +40,7 @@ namespace BEEV // Bitblasts, CNF conversion and calls toSATandSolve() virtual bool CallSAT(MINISAT::Solver& SatSolver, const ASTNode& input) =0; - virtual ASTNodeToVar& SATVar_to_SymbolIndexMap()= 0; + virtual ASTNodeToSATVar& SATVar_to_SymbolIndexMap()= 0; virtual void ClearAllTables(void) =0; };