From a17c28c97fed566e2f2bf61218fcd5332e67af62 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Wed, 9 Sep 2009 14:35:40 +0000 Subject: [PATCH] git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@209 e59a4935-1847-0410-ae03-e826735625c1 --- scripts/Makefile.common | 21 ++- src/AST/AST.h | 21 ++- .../AbstractionRefinement.cpp | 168 ++++++++++++------ src/simplifier/simplifier.cpp | 146 ++++++++++----- src/to-sat/ToCNF.cpp | 2 +- src/to-sat/ToSAT.cpp | 54 ++++-- 6 files changed, 283 insertions(+), 129 deletions(-) diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 04c7af5..6e34f48 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -1,15 +1,18 @@ # This is a -*- makefile -*-, Emacs +# #Please refer LICENSE FILE in the home directory for licensing #information always use full screen mode to view/edit this file in #emacs #OPTIMIZE = -g -pg # Debugging and gprof-style profiling -#OPTIMIZE = -g # Debugging -OPTIMIZE = -O3 -DNDEBUG # Maximum optimization +OPTIMIZE = -g # Debugging +#OPTIMIZE = -O3 -DNDEBUG # Maximum optimization CFLAGS_BASE = $(OPTIMIZE) -# You can compile using make STATIC=true to compile a statically linked executable -# Note that you should execute liblinks.sh first. + +# You can compile using make STATIC=true to compile a statically +# linked executable Note that you should execute liblinks.sh first. + ifdef STATIC LDFLAGS_BASE = -static-libgcc -static else @@ -17,11 +20,11 @@ else endif # PKT: support for universal binaries -# NB: static libraries are poorly supported in Mac OS X. More specifically -# -static has different semantics than on ELF based systems -# Also, building mac os x universal binaries is a tad tricky -# 1. you cannot use ar on a library after calling ranlib -# 2. -MM dependency tracking does not work +# NB: static libraries are poorly supported in Mac OS X. More +# specifically -static has different semantics than on ELF based +# systems Also, building mac os x universal binaries is a tad tricky +# 1. you cannot use ar on a library after calling ranlib 2. -MM +# dependency tracking does not work # the architectures to compile for UNIVERSAL_ARCH = -arch i386 -arch ppc -arch ppc64 diff --git a/src/AST/AST.h b/src/AST/AST.h index bbffdb1..dd864fc 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -1155,12 +1155,19 @@ namespace BEEV return n; } - ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyFormula_TopLevel(const ASTNode& a, bool pushNeg); + ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a, + bool pushNeg, + ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyFormula_TopLevel(const ASTNode& a, + bool pushNeg, + ASTNodeMap* VarConstMap=NULL); ASTNode SimplifyTerm_TopLevel(const ASTNode& b); - ASTNode SimplifyFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode SimplifyTerm(const ASTNode& inputterm, ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyFormula(const ASTNode& a, + bool pushNeg, + ASTNodeMap* VarConstMap=NULL); + ASTNode SimplifyTerm(const ASTNode& inputterm, + ASTNodeMap* VarConstMap=NULL); void CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output); void BuildReferenceCountMap(const ASTNode& b); @@ -1235,7 +1242,8 @@ namespace BEEV ASTNodeMap* ParamToCurrentValMap, bool CheckUsingModel_Or_Expand); ASTNode Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop); - + ASTNode Check_FiniteLoop_UsingModel(const ASTNode& finiteloop); + //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 @@ -1539,7 +1547,8 @@ namespace BEEV void ASTNodeStats(const char * c, const ASTNode& a); //Check the map passed to SimplifyTerm - bool CheckMap(ASTNodeMap* VarConstMap, const ASTNode& key, ASTNode& output); + bool CheckMap(ASTNodeMap* VarConstMap, + const ASTNode& key, ASTNode& output); //substitution diff --git a/src/abstraction-refinement/AbstractionRefinement.cpp b/src/abstraction-refinement/AbstractionRefinement.cpp index 3597c99..03f45ac 100644 --- a/src/abstraction-refinement/AbstractionRefinement.cpp +++ b/src/abstraction-refinement/AbstractionRefinement.cpp @@ -37,9 +37,10 @@ namespace BEEV * it compares with other approaches (e.g., one false axiom at a * time or all the false axioms each time). *****************************************************************/ - SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, - const ASTNode& inputAlreadyInSAT, - const ASTNode& original_input) { + SOLVER_RETURN_TYPE + BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, + const ASTNode& inputAlreadyInSAT, + const ASTNode& original_input) { //printf("doing array read refinement\n"); if (!arrayread_refinement_flag) FatalError("SATBased_ArrayReadRefinement: Control should not reach here"); @@ -73,8 +74,10 @@ namespace BEEV //get the arrayname ASTNode ArrName = iset->first; // if(SYMBOL != ArrName.GetKind()) - // FatalError("SATBased_ArrayReadRefinement: arrname is not a SYMBOL",ArrName); - ASTNode arr_read1 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index); + // FatalError("SATBased_ArrayReadRefinement: "\ + // "arrname is not a SYMBOL",ArrName); + ASTNode arr_read1 = + CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index); //get the variable corresponding to the array_read1 ASTNode arrsym1 = _arrayread_symbol[arr_read1]; if (!(SYMBOL == arrsym1.GetKind() || BVCONST == arrsym1.GetKind())) @@ -95,9 +98,11 @@ namespace BEEV //first construct the antecedent for the LA axiom ASTNode eqOfIndices = (exprless(the_index, compare_index)) ? - CreateSimplifiedEQ(the_index, compare_index) : CreateSimplifiedEQ(compare_index, the_index); + CreateSimplifiedEQ(the_index, compare_index) : + CreateSimplifiedEQ(compare_index, the_index); - ASTNode arr_read2 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index); + ASTNode arr_read2 = + CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index); //get the variable corresponding to the array_read2 ASTNode arrsym2 = _arrayread_symbol[arr_read2]; if (!(SYMBOL == arrsym2.GetKind() || BVCONST == arrsym2.GetKind())) @@ -123,7 +128,8 @@ namespace BEEV //if (FalseAxiomsVec.size() > 0) if (FalseAxiomsVec.size() > oldFalseAxiomsSize) { - res2 = CallSAT_ResultCheck(SatSolver, FalseAxioms, original_input); + res2 = + CallSAT_ResultCheck(SatSolver, FalseAxioms, original_input); oldFalseAxiomsSize = FalseAxiomsVec.size(); } //printf("spot 02, res2 = %d\n", res2); @@ -146,8 +152,9 @@ namespace BEEV * * FIXME: Write Detailed Comment *****************************************************************/ - SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, - const ASTNode& original_input) + SOLVER_RETURN_TYPE + BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, + const ASTNode& original_input) { ASTNode writeAxiom; ASTNodeMap::iterator it = ReadOverWrite_NewName_Map.begin(); @@ -210,7 +217,8 @@ namespace BEEV { if (READ != term.GetKind() && WRITE != term[0].GetKind()) { - FatalError("Create_ArrayWriteAxioms: Input must be a READ over a WRITE", term); + FatalError("Create_ArrayWriteAxioms: "\ + "Input must be a READ over a WRITE", term); } ASTNode lhs = newvar; @@ -239,22 +247,41 @@ namespace BEEV * if the 'done' flag is true, then we terminate this refinement * loop. *****************************************************************/ - SOLVER_RETURN_TYPE BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, - const ASTNode& original_input) + SOLVER_RETURN_TYPE + BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, + const ASTNode& original_input) { - for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),iend=GlobalList_Of_FiniteLoops.end(); - i!=iend;i++) + SOLVER_RETURN_TYPE ret = SOLVER_UNDECIDED; + std::vector retvec; + for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(), + iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++) { - ASTNodeMap ParamToCurrentValMap; - SOLVER_RETURN_TYPE ret = SATBased_FiniteLoop_Refinement(SatSolver, - original_input, - *i,&ParamToCurrentValMap); - if(SOLVER_UNDECIDED != ret) + //ASTNodeMap * ParamToCurrentValMap = new ASTNodeMap; + ASTNodeMap ParamToCurrentValMap; + ret = SATBased_FiniteLoop_Refinement(SatSolver, + original_input, + *i, + &ParamToCurrentValMap); + if(SOLVER_VALID == ret) { return ret; } + retvec.push_back(ret); + } //End of For() + + //Even if one of the for loops results in SOLVER_UNDECIDED, then + //it means that the constructed model is bogus. Return this fact. + for(vector::iterator i=retvec.begin(), + iend=retvec.end();i!=iend;i++) + { + if(SOLVER_UNDECIDED == *i) + { + return SOLVER_UNDECIDED; + } } - return SOLVER_UNDECIDED; + + //All for loops are true in the model + return CallSAT_ResultCheck(SatSolver, ASTTrue, original_input); } //end of SATBased_AllFiniteLoops_Refinement() @@ -280,10 +307,11 @@ namespace BEEV // //Expand the finite loop, check against model, and add false //formulas to the SAT solver - SOLVER_RETURN_TYPE BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, - const ASTNode& original_input, - const ASTNode& finiteloop, - ASTNodeMap* ParamToCurrentValMap) + SOLVER_RETURN_TYPE + BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, + const ASTNode& original_input, + const ASTNode& finiteloop, + ASTNodeMap* ParamToCurrentValMap) { //BVTypeCheck should have already checked the sanity of the input //FOR-formula @@ -304,8 +332,10 @@ namespace BEEV { while(paramCurrentValue < paramLimit) { - SATBased_FiniteLoop_Refinement(SatSolver, original_input, - formulabody, ParamToCurrentValMap); + SATBased_FiniteLoop_Refinement(SatSolver, + original_input, + formulabody, + ParamToCurrentValMap); paramCurrentValue = paramCurrentValue + paramIncrement; //Update ParamToCurrentValMap with parameter and its current @@ -313,54 +343,70 @@ namespace BEEV // //FIXME: Possible leak since I am not freeing the previous //'value' for the same 'key' - (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + (*ParamToCurrentValMap)[parameter] = + CreateBVConst(32,paramCurrentValue); } //end of While } //end of recursion FORs - ASTVec forloopFormulaVector; + //ASTVec forloopFormulaVector; //Expand the leaf level FOR-construct completely + int AllLoopsAreTrue = 0; for(; paramCurrentValue < paramLimit; paramCurrentValue = paramCurrentValue + paramIncrement) { ASTNode currentFormula; - currentFormula = SimplifyFormula(formulabody, ParamToCurrentValMap); + currentFormula = + SimplifyFormula(formulabody, false, ParamToCurrentValMap); //Check the currentformula against the model, and add it to the //SAT solver if it is false against the model if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) { - forloopFormulaVector.push_back(currentFormula); - ASTNode forloopFormulas = - (forloopFormulaVector.size() != 1) ? - CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0]; + // forloopFormulaVector.push_back(currentFormula); ASTNode + // forloopFormulas = + // (forloopFormulaVector.size() != 1) ? + // CreateNode(AND, forloopFormulaVector) : + // forloopFormulaVector[0]; SOLVER_RETURN_TYPE result = - CallSAT_ResultCheck(SatSolver, forloopFormulas, original_input); + CallSAT_ResultCheck(SatSolver, currentFormula, original_input); if(result != SOLVER_UNDECIDED) { return result; } } + else + { + //ComputeFormulaUsingModel can either return ASTFalse or + //ASTTrue + AllLoopsAreTrue++; + } //Update ParamToCurrentValMap with parameter and its current //value // //FIXME: Possible leak since I am not freeing the previous //'value' for the same 'key' - (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + (*ParamToCurrentValMap)[parameter] = + CreateBVConst(32,paramCurrentValue); } //end of expanding the FOR loop + if(AllLoopsAreTrue == paramLimit) + { + return SOLVER_INVALID; + } + return SOLVER_UNDECIDED; } //end of the SATBased_FiniteLoop_Refinement() //SATBased_FiniteLoop_Refinement_UsingModel // - //Expand the finite loop, check against model, and add false - //formulas to the SAT solver - ASTNode BeevMgr::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop, - ASTNodeMap* ParamToCurrentValMap, - bool CheckUsingModel_Or_Expand = true) + //Expand the finite loop, check against model + ASTNode + BeevMgr::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop, + ASTNodeMap* ParamToCurrentValMap, + bool checkusingmodel_flag = true) { /* * 'finiteloop' is the finite loop to be expanded @@ -398,7 +444,8 @@ namespace BEEV while(paramCurrentValue < paramLimit) { Check_FiniteLoop_UsingModel(formulabody, - ParamToCurrentValMap, CheckUsingModel_Or_Expand); + ParamToCurrentValMap, + checkusingmodel_flag); paramCurrentValue = paramCurrentValue + paramIncrement; //Update ParamToCurrentValMap with parameter and its current @@ -406,7 +453,8 @@ namespace BEEV // //FIXME: Possible leak since I am not freeing the previous //'value' for the same 'key' - (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + (*ParamToCurrentValMap)[parameter] = + CreateBVConst(32,paramCurrentValue); } //end of While } @@ -417,9 +465,10 @@ namespace BEEV paramCurrentValue = paramCurrentValue + paramIncrement) { ASTNode currentFormula; - currentFormula = SimplifyFormula(formulabody, ParamToCurrentValMap); + currentFormula = + SimplifyFormula(formulabody, false, ParamToCurrentValMap); - if(CheckUsingModel_Or_Expand) + if(checkusingmodel_flag) { //Check the currentformula against the model, and add it to the //SAT solver if it is false against the model @@ -435,28 +484,41 @@ namespace BEEV //value //FIXME: Possible leak since I am not freeing the previous //'value' for the same 'key' - (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + (*ParamToCurrentValMap)[parameter] = + CreateBVConst(32,paramCurrentValue); } - if(CheckUsingModel_Or_Expand) + if(checkusingmodel_flag) { - ASTNode retFormula = - (forloopFormulaVector.size() != 1) ? CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0]; - return retFormula; + return ASTTrue; } else { - return ASTTrue; + ASTNode retFormula = + (forloopFormulaVector.size() != 1) ? + CreateNode(AND, forloopFormulaVector) : + forloopFormulaVector[0]; + return retFormula; } } //end of the Check_FiniteLoop_UsingModel() //Expand_FiniteLoop_For_ModelCheck - ASTNode BeevMgr::Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop) + ASTNode + BeevMgr::Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop) { ASTNodeMap ParamToCurrentValMap; - return Check_FiniteLoop_UsingModel(finiteloop, &ParamToCurrentValMap, false); + return Check_FiniteLoop_UsingModel(finiteloop, + &ParamToCurrentValMap, false); } //end of Expand_FiniteLoop_TopLevel() + ASTNode + BeevMgr::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop) + { + ASTNodeMap ParamToCurrentValMap; + return Check_FiniteLoop_UsingModel(finiteloop, + &ParamToCurrentValMap, true); + } //end of Check_FiniteLoop_UsingModel + };// end of namespace BEEV diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index b1cf8e6..701351f 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -47,7 +47,8 @@ ASTNode Flatten(const ASTNode& a) } - bool BeevMgr::CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg) + bool BeevMgr::CheckSimplifyMap(const ASTNode& key, + ASTNode& output, bool pushNeg) { ASTNodeMap::iterator it, itend; it = pushNeg ? SimplifyNegMap->find(key) : SimplifyMap->find(key); @@ -75,12 +76,12 @@ ASTNode Flatten(const ASTNode& a) } // Push any reference count used by the key to the value. - void BeevMgr::UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg) + void BeevMgr::UpdateSimplifyMap(const ASTNode& key, + const ASTNode& value, bool pushNeg) { // Don't add leaves. Leaves are easy to recalculate, no need to cache. if (0 == key.Degree()) return; - // If there are references to the key, add them to the references of the value. ASTNodeCountMap::const_iterator itKey, itValue; itKey = ReferenceCount->find(key); @@ -131,7 +132,9 @@ ASTNode Flatten(const ASTNode& a) //e0 is of the form var, and e1 is const if (1 == i && !CheckSubstitutionMap(e0)) { - assert((e1.GetKind() == TRUE) || (e1.GetKind() == FALSE) || (e1.GetKind() == BVCONST)); + assert((e1.GetKind() == TRUE) || + (e1.GetKind() == FALSE) || + (e1.GetKind() == BVCONST)); SolverMap[e0] = e1; return true; } @@ -140,7 +143,9 @@ ASTNode Flatten(const ASTNode& a) //e1 is of the form var, and e0 is const if (-1 == i && !CheckSubstitutionMap(e1)) { - assert((e0.GetKind() == TRUE) || (e0.GetKind() == FALSE) || (e0.GetKind() == BVCONST)); + assert((e0.GetKind() == TRUE) || + (e0.GetKind() == FALSE) || + (e0.GetKind() == BVCONST)); SolverMap[e1] = e0; return true; } @@ -195,9 +200,12 @@ ASTNode Flatten(const ASTNode& a) //a is of the form READ(Arr,const), and b is const, or //a is of the form var, and b is const - if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST && (k2 == BVCONST))) - // || - // k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST))) + if ((k1 == READ && + a[0].GetKind() == SYMBOL && + a[1].GetKind() == BVCONST && + (k2 == BVCONST))) + // || k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() + // == BVCONST))) return 1; if (SYMBOL == k1 && (BVCONST == k2 || TRUE == k2 || FALSE == k2)) @@ -205,7 +213,10 @@ ASTNode Flatten(const ASTNode& a) //b is of the form READ(Arr,const), and a is const, or //b is of the form var, and a is const - if ((k1 == BVCONST) && ((k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST))) + if ((k1 == BVCONST) && + ((k2 == READ && + b[0].GetKind() == SYMBOL && + b[1].GetKind() == BVCONST))) return -1; if (SYMBOL == k2 && (BVCONST == k1 || TRUE == k1 || FALSE == k1)) @@ -248,7 +259,9 @@ ASTNode Flatten(const ASTNode& a) } } - ASTNode BeevMgr::SimplifyFormula_NoRemoveWrites(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) + ASTNode + BeevMgr::SimplifyFormula_NoRemoveWrites(const ASTNode& b, + bool pushNeg, ASTNodeMap* VarConstMap) { Begin_RemoveWrites = false; ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap); @@ -282,7 +295,9 @@ ASTNode Flatten(const ASTNode& a) } } - ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg) + ASTNode + BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, + bool pushNeg, ASTNodeMap* VarConstMap) { ResetSimplifyMaps(); @@ -293,7 +308,9 @@ ASTNode Flatten(const ASTNode& a) return out; } - ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) + ASTNode + BeevMgr::SimplifyFormula(const ASTNode& b, + bool pushNeg, ASTNodeMap* VarConstMap) { if (!optimize_flag) return b; @@ -301,7 +318,8 @@ ASTNode Flatten(const ASTNode& a) Kind kind = b.GetKind(); if (BOOLEAN_TYPE != b.GetType()) { - FatalError(" SimplifyFormula: You have input a nonformula kind: ", ASTUndefined, kind); + FatalError(" SimplifyFormula: "\ + "You have input a nonformula kind: ", ASTUndefined, kind); } ASTNode a = b; @@ -323,35 +341,35 @@ ASTNode Flatten(const ASTNode& a) { case AND: case OR: - output = SimplifyAndOrFormula(a, pushNeg); + output = SimplifyAndOrFormula(a, pushNeg, VarConstMap); break; case NOT: - output = SimplifyNotFormula(a, pushNeg); + output = SimplifyNotFormula(a, pushNeg, VarConstMap); break; case XOR: - output = SimplifyXorFormula(a, pushNeg); + output = SimplifyXorFormula(a, pushNeg, VarConstMap); break; case NAND: - output = SimplifyNandFormula(a, pushNeg); + output = SimplifyNandFormula(a, pushNeg, VarConstMap); break; case NOR: - output = SimplifyNorFormula(a, pushNeg); + output = SimplifyNorFormula(a, pushNeg, VarConstMap); break; case IFF: - output = SimplifyIffFormula(a, pushNeg); + output = SimplifyIffFormula(a, pushNeg, VarConstMap); break; case IMPLIES: - output = SimplifyImpliesFormula(a, pushNeg); + output = SimplifyImpliesFormula(a, pushNeg, VarConstMap); break; case ITE: - output = SimplifyIteFormula(a, pushNeg); + output = SimplifyIteFormula(a, pushNeg, VarConstMap); break; case FOR: - output = SimplifyForFormula(a, pushNeg); + output = SimplifyForFormula(a, pushNeg, VarConstMap); break; default: //kind can be EQ,NEQ,BVLT,BVLE,... or a propositional variable - output = SimplifyAtomicFormula(a, pushNeg); + output = SimplifyAtomicFormula(a, pushNeg, VarConstMap); //output = pushNeg ? CreateNode(NOT,a) : a; break; } @@ -361,12 +379,17 @@ ASTNode Flatten(const ASTNode& a) return output; } - ASTNode BeevMgr::SimplifyForFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { + ASTNode + BeevMgr::SimplifyForFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap) + { //FIXME: Code this up properly later. Mainly pushing the negation down return a; } - ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) + ASTNode + BeevMgr::SimplifyAtomicFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap) { if (!optimize_flag) return a; @@ -381,10 +404,10 @@ ASTNode Flatten(const ASTNode& a) if (a.Degree() == 2) { //cerr << "Input to simplifyterm: left: " << a[0] << endl; - left = SimplifyTerm(a[0]); + left = SimplifyTerm(a[0], VarConstMap); //cerr << "Output of simplifyterm:left: " << left << endl; //cerr << "Input to simplifyterm: right: " << a[1] << endl; - right = SimplifyTerm(a[1]); + right = SimplifyTerm(a[1], VarConstMap); //cerr << "Output of simplifyterm:left: " << right << endl; } @@ -410,7 +433,8 @@ ASTNode Flatten(const ASTNode& a) ASTNode thebit = a[1]; ASTNode zero = CreateZeroConst(1); ASTNode one = CreateOneConst(1); - ASTNode getthebit = SimplifyTerm(CreateTerm(BVEXTRACT, 1, term, thebit, thebit)); + ASTNode getthebit = + SimplifyTerm(CreateTerm(BVEXTRACT, 1, term, thebit, thebit)); if (getthebit == zero) output = pushNeg ? ASTTrue : ASTFalse; else if (getthebit == one) @@ -450,7 +474,8 @@ ASTNode Flatten(const ASTNode& a) break; } default: - FatalError("SimplifyAtomicFormula: NO atomic formula of the kind: ", ASTUndefined, kind); + FatalError("SimplifyAtomicFormula: "\ + "NO atomic formula of the kind: ", ASTUndefined, kind); break; } @@ -459,7 +484,9 @@ ASTNode Flatten(const ASTNode& a) return output; } //end of SimplifyAtomicFormula() - ASTNode BeevMgr::CreateSimplifiedINEQ(Kind k, const ASTNode& left, const ASTNode& right, bool pushNeg) + ASTNode BeevMgr::CreateSimplifiedINEQ(Kind k, + const ASTNode& left, + const ASTNode& right, bool pushNeg) { ASTNode output; if (BVCONST == left.GetKind() && BVCONST == right.GetKind()) @@ -491,7 +518,10 @@ ASTNode Flatten(const ASTNode& a) } else { - output = pushNeg ? CreateNode(BVLE, right, left) : CreateNode(BVLT, left, right); + output = + pushNeg ? + CreateNode(BVLE, right, left) : + CreateNode(BVLT, left, right); } break; case BVLE: @@ -514,7 +544,10 @@ ASTNode Flatten(const ASTNode& a) } else { - output = pushNeg ? CreateNode(BVLT, right, left) : CreateNode(BVLE, left, right); + output = + pushNeg ? + CreateNode(BVLT, right, left) : + CreateNode(BVLE, left, right); } break; case BVGT: @@ -528,7 +561,10 @@ ASTNode Flatten(const ASTNode& a) } else { - output = pushNeg ? CreateNode(BVLE, left, right) : CreateNode(BVLT, right, left); + output = + pushNeg ? + CreateNode(BVLE, left, right) : + CreateNode(BVLT, right, left); } break; case BVGE: @@ -542,7 +578,10 @@ ASTNode Flatten(const ASTNode& a) } else { - output = pushNeg ? CreateNode(BVLT, left, right) : CreateNode(BVLE, right, left); + output = + pushNeg ? + CreateNode(BVLT, left, right) : + CreateNode(BVLE, right, left); } break; case BVSLT: @@ -578,15 +617,17 @@ ASTNode Flatten(const ASTNode& a) { if (BVLT != in[j].GetKind()) continue; - if (in[i][0] == in[j][1] && in[i][1] == in[j][0]) // parameters are swapped. + // parameters are swapped. + if (in[i][0] == in[j][1] && in[i][1] == in[j][0]) return ASTFalse; } } return in; } - // turns say (bvslt (ite a b c) (ite a d e)) INTO (ite a (bvslt b d) (bvslt c e)) - // Expensive. But makes some other simplifications possible. + // turns say (bvslt (ite a b c) (ite a d e)) INTO (ite a (bvslt b d) + // (bvslt c e)) Expensive. But makes some other simplifications + // possible. ASTNode BeevMgr::PullUpITE(const ASTNode& in) { if (2 != in.GetChildren().size()) @@ -658,7 +699,9 @@ ASTNode Flatten(const ASTNode& a) //be semantically equal. output = ASTFalse; } - else if (ITE == k1 && BVCONST == in1[1].GetKind() && BVCONST == in1[2].GetKind() && BVCONST == k2) + else if (ITE == k1 && + BVCONST == in1[1].GetKind() && + BVCONST == in1[2].GetKind() && BVCONST == k2) { //if one side is a BVCONST and the other side is an ITE over //BVCONST then we can do the following optimization: @@ -687,7 +730,9 @@ ASTNode Flatten(const ASTNode& a) output = CreateNode(EQ, in1, in2); } } - else if (ITE == k2 && BVCONST == in2[1].GetKind() && BVCONST == in2[2].GetKind() && BVCONST == k1) + else if (ITE == k2 && + BVCONST == in2[1].GetKind() && + BVCONST == in2[2].GetKind() && BVCONST == k1) { ASTNode cond = in2[0]; if (in2[1] == in1) @@ -743,7 +788,9 @@ ASTNode Flatten(const ASTNode& a) } //accepts cond == t1, then part is t2, and else part is t3 - ASTNode BeevMgr::CreateSimplifiedTermITE(const ASTNode& in0, const ASTNode& in1, const ASTNode& in2) + ASTNode BeevMgr::CreateSimplifiedTermITE(const ASTNode& in0, + const ASTNode& in1, + const ASTNode& in2) { ASTNode t0 = in0; ASTNode t1 = in1; @@ -754,12 +801,14 @@ ASTNode Flatten(const ASTNode& a) if (t1.GetValueWidth() != t2.GetValueWidth()) { cerr << "t2 is : = " << t2; - FatalError("CreateSimplifiedTermITE: the lengths of then and else branches don't match", t1); + FatalError("CreateSimplifiedTermITE: "\ + "the lengths of the two branches don't match", t1); } if (t1.GetIndexWidth() != t2.GetIndexWidth()) { cerr << "t2 is : = " << t2; - FatalError("CreateSimplifiedTermITE: the lengths of then and else branches don't match", t1); + FatalError("CreateSimplifiedTermITE: "\ + "the lengths of the two branches don't match", t1); } return CreateTerm(ITE, t1.GetValueWidth(), t0, t1, t2); } @@ -916,7 +965,9 @@ ASTNode Flatten(const ASTNode& a) } //end of SimplifyAndOrFormula - ASTNode BeevMgr::SimplifyNotFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) + ASTNode + BeevMgr::SimplifyNotFormula(const ASTNode& a, + bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; if (CheckSimplifyMap(a, output, pushNeg)) @@ -1318,7 +1369,8 @@ ASTNode Flatten(const ASTNode& a) } //This function simplifies terms based on their kind - ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm, ASTNodeMap* VarConstMap) + ASTNode + BeevMgr::SimplifyTerm(const ASTNode& actualInputterm, ASTNodeMap* VarConstMap) { ASTNode inputterm(actualInputterm); // mutable local copy. @@ -1425,7 +1477,9 @@ ASTNode Flatten(const ASTNode& a) CONSTANTBV::BitVector_Bit_On(maskedPlusOne, i); } CONSTANTBV::BitVector_increment(maskedPlusOne); - ASTNode temp = CreateTerm(BVMULT, inputValueWidth, CreateBVConst(maskedPlusOne, inputValueWidth), other); + ASTNode temp = + CreateTerm(BVMULT, inputValueWidth, + CreateBVConst(maskedPlusOne, inputValueWidth), other); output = CreateTerm(BVNEG, inputValueWidth, temp); } } @@ -2086,7 +2140,7 @@ ASTNode Flatten(const ASTNode& a) { //arr is a SYMBOL for sure ASTNode arr = inputterm[0]; - ASTNode index = SimplifyTerm(inputterm[1]); + ASTNode index = SimplifyTerm(inputterm[1], VarConstMap); out1 = CreateTerm(READ, inputValueWidth, arr, index); } } diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index 4bc3cf9..9e67212 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -1776,7 +1776,7 @@ namespace BEEV //Call the SAT solver, and check the result before returning. This //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or SOLVER_UNDECIDED SOLVER_RETURN_TYPE BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& SatSolver, - const ASTNode& modified_input, + const ASTNode& modified_input, const ASTNode& original_input) { ASTNode BBFormula = BBForm(modified_input); diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index cf6029c..ac85291 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -660,7 +660,8 @@ namespace BEEV ASTNode writeIndex = TermToConstTermUsingModel(write[1], false); ASTNode writeVal = TermToConstTermUsingModel(write[2], false); - ASTNode cond = ComputeFormulaUsingModel(CreateSimplifiedEQ(writeIndex, readIndex)); + ASTNode cond = + ComputeFormulaUsingModel(CreateSimplifiedEQ(writeIndex, readIndex)); if (ASTTrue == cond) { //found the write-value. return it @@ -837,10 +838,15 @@ namespace BEEV else if (ASTFalse == t0) output = ComputeFormulaUsingModel(form[2]); else - FatalError("ComputeFormulaUsingModel: ITE: something is wrong with the formula: ", form); + FatalError("ComputeFormulaUsingModel: ITE: "\ + "something is wrong with the formula: ", form); break; + case FOR: + output = Check_FiniteLoop_UsingModel(form); + break; default: - FatalError(" ComputeFormulaUsingModel: the kind has not been implemented", ASTUndefined); + FatalError(" ComputeFormulaUsingModel: "\ + "the kind has not been implemented", ASTUndefined); break; } @@ -931,17 +937,22 @@ namespace BEEV do { inputToSAT = simplified_solved_InputToSAT; + simplified_solved_InputToSAT = CreateSubstitutionMap(simplified_solved_InputToSAT); //printf("##################################################\n"); ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); + simplified_solved_InputToSAT = SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); + simplified_solved_InputToSAT = bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT); ASTNodeStats("after solving: ", simplified_solved_InputToSAT); - } while (inputToSAT != simplified_solved_InputToSAT); + + } + while (inputToSAT != simplified_solved_InputToSAT); ASTNodeStats("Before SimplifyWrites_Inplace begins: ", simplified_solved_InputToSAT); SimplifyWrites_InPlace_Flag = true; @@ -954,13 +965,17 @@ namespace BEEV simplified_solved_InputToSAT = CreateSubstitutionMap(simplified_solved_InputToSAT); ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); - simplified_solved_InputToSAT = + + simplified_solved_InputToSAT = SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); - simplified_solved_InputToSAT = + + simplified_solved_InputToSAT = bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT); ASTNodeStats("after solving: ", simplified_solved_InputToSAT); - } while (inputToSAT != simplified_solved_InputToSAT); + + } + while (inputToSAT != simplified_solved_InputToSAT); ASTNodeStats("After SimplifyWrites_Inplace: ", simplified_solved_InputToSAT); delete bvsolver; @@ -978,14 +993,17 @@ namespace BEEV do { inputToSAT = simplified_solved_InputToSAT; - //simplified_solved_InputToSAT = CreateSubstitutionMap(simplified_solved_InputToSAT); - //Begin_RemoveWrites = true; - //ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); + //simplified_solved_InputToSAT = + //CreateSubstitutionMap(simplified_solved_InputToSAT); + //Begin_RemoveWrites = true; ASTNodeStats("after pure + //substitution: ", simplified_solved_InputToSAT); simplified_solved_InputToSAT = SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); - //ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); - //simplified_solved_InputToSAT = bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT); - //ASTNodeStats("after solving: ", simplified_solved_InputToSAT); + //ASTNodeStats("after simplification: ", + //simplified_solved_InputToSAT); simplified_solved_InputToSAT + //= bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT); + //ASTNodeStats("after solving: ", + //simplified_solved_InputToSAT); } while (inputToSAT != simplified_solved_InputToSAT); if (start_abstracting) @@ -996,7 +1014,8 @@ namespace BEEV SimplifyWrites_InPlace_Flag = false; Begin_RemoveWrites = false; - simplified_solved_InputToSAT = TransformFormula_TopLevel(simplified_solved_InputToSAT); + simplified_solved_InputToSAT = + TransformFormula_TopLevel(simplified_solved_InputToSAT); ASTNodeStats("after transformation: ", simplified_solved_InputToSAT); TermsAlreadySeenMap.clear(); @@ -1017,6 +1036,13 @@ namespace BEEV return res; } + res = SATBased_AllFiniteLoops_Refinement(newS, orig_input); + if (SOLVER_UNDECIDED != res) + { + CountersAndStats("print_func_stats"); + return res; + } + res = SATBased_ArrayReadRefinement(newS, simplified_solved_InputToSAT, orig_input); if (SOLVER_UNDECIDED != res) { -- 2.47.3