From 1aa3f10a67b0037793f112d13798b707846d0651 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 19 Jun 2011 09:06:06 +0000 Subject: [PATCH] Use the advanced CNF generator to encode array problems into CNF. Array axioms are generated by hand. NB. This slows down the CVC regressions substantially. Adding about 40 seconds to them. The CVC array problems are very easy, so the extra effort in generating a better CNF is wasted. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1345 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ArrayTransformer.cpp | 51 +++- src/AST/ArrayTransformer.h | 7 +- .../AbstractionRefinement.cpp | 229 ++++++++++++++---- src/to-sat/AIG/ToCNFAIG.cpp | 23 +- src/to-sat/AIG/ToCNFAIG.h | 21 +- src/to-sat/AIG/ToSATAIG.cpp | 100 +++----- src/to-sat/AIG/ToSATAIG.h | 8 +- 7 files changed, 282 insertions(+), 157 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index af1853c..acd080e 100644 --- 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& mapper = iset->second; + + for (map::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 12d5ceb..93c5bb6 100644 --- 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 6a1aeaa..a7c6614 100644 --- 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 & 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 v_a; + vector 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 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& 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 RemainingAxiomsVec; + vector 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 concreteValues; concreteValues.reserve(mapper.size()); + ASTVec index_symbols; + for (map::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 60d08c2..0a845bf 100644 --- 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 077b840..5e54365 100644 --- 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 5f096c6..b9bf1bc 100644 --- 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(&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 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 1d1fde2..3a33b17 100644 --- 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 *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) { -- 2.47.3