From: vijay_ganesh Date: Thu, 10 Sep 2009 19:40:49 +0000 (+0000) Subject: Added EXCEPT construct for the FOR-construct X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=541639fc4aa38d365060c7bb52a18f27d4ddeed6;p=francis%2Fstp.git Added EXCEPT construct for the FOR-construct git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@217 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/Makefile.common b/scripts/Makefile.common index efd7c20..ec45518 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -4,8 +4,8 @@ #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 = -g -pg # Debugging and gprof-style profiling +OPTIMIZE = -g # Debugging OPTIMIZE = -O3 -DNDEBUG # Maximum optimization CFLAGS_BASE = $(OPTIMIZE) diff --git a/src/AST/AST.h b/src/AST/AST.h index 7bbc83c..26ece48 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -1288,7 +1288,7 @@ namespace BEEV void printCacheStatus(); //from v8 - int TopLevelSATAux(const ASTNode& query); + SOLVER_RETURN_TYPE TopLevelSATAux(const ASTNode& query); //################################################## //################################################## @@ -1296,7 +1296,7 @@ namespace BEEV //accepts query and returns the answer. if query is valid, return //true, else return false. Automatically constructs counterexample //for invalid queries, and prints them upon request. - int TopLevelSAT(const ASTNode& query, const ASTNode& asserts); + SOLVER_RETURN_TYPE TopLevelSAT(const ASTNode& query, const ASTNode& asserts); // Debugging function to find problems in BitBlast and ToCNF. // See body in ToSAT.cpp for more explanation. @@ -1446,7 +1446,7 @@ namespace BEEV public: //print the STP solver output - void PrintOutput(bool true_iff_valid); + void PrintOutput(SOLVER_RETURN_TYPE ret); //Converts MINISAT counterexample into an AST memotable (i.e. the //function populates the datastructure CounterExampleMap) diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp index b6455de..c4a5879 100644 --- a/src/AST/printer/AssortedPrinters.cpp +++ b/src/AST/printer/AssortedPrinters.cpp @@ -287,8 +287,10 @@ namespace BEEV } //printCacheStatus() //This function prints the output of the STP solver - void BeevMgr::PrintOutput(bool true_iff_valid) + void BeevMgr::PrintOutput(SOLVER_RETURN_TYPE ret) { + bool true_iff_valid = (SOLVER_VALID == ret); + if (print_output_flag) { if (smtlib_parser_flag) diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp index c00271a..de25878 100644 --- a/src/AST/printer/PLPrinter.cpp +++ b/src/AST/printer/PLPrinter.cpp @@ -189,8 +189,11 @@ namespace printer PL_Print1(os, c[2], indentation, letize); os << ";"; PL_Print1(os, c[3], indentation, letize); - os << "){ \n"; + os << ";"; + os << "EXCEPT "; PL_Print1(os, c[4], indentation, letize); + os << "){ \n"; + PL_Print1(os, c[5], indentation, letize); os << "} \n"; } break; diff --git a/src/abstraction-refinement/AbstractionRefinement.cpp b/src/abstraction-refinement/AbstractionRefinement.cpp index e830bf6..852a076 100644 --- a/src/abstraction-refinement/AbstractionRefinement.cpp +++ b/src/abstraction-refinement/AbstractionRefinement.cpp @@ -281,7 +281,8 @@ namespace BEEV } //All for loops are true in the model - return CallSAT_ResultCheck(SatSolver, ASTTrue, original_input); + //return CallSAT_ResultCheck(SatSolver, ASTTrue, original_input); + return ret; } //end of SATBased_AllFiniteLoops_Refinement() @@ -319,7 +320,8 @@ namespace BEEV int paramInit = GetUnsignedConst(finiteloop[1]); int paramLimit = GetUnsignedConst(finiteloop[2]); int paramIncrement = GetUnsignedConst(finiteloop[3]); - ASTNode formulabody = finiteloop[4]; + ASTNode exceptFormula = finiteloop[4]; + ASTNode formulabody = finiteloop[5]; int paramCurrentValue = paramInit; //Update ParamToCurrentValMap with parameter and its current @@ -327,7 +329,7 @@ namespace BEEV (*ParamToCurrentValMap)[parameter] = CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); - SOLVER_RETURN_TYPE ret; + SOLVER_RETURN_TYPE ret = SOLVER_UNDECIDED; //Go recursively thru' all the FOR-constructs. if(FOR == formulabody.GetKind()) { @@ -344,11 +346,9 @@ namespace BEEV } - //Update ParamToCurrentValMap with parameter and its current - //value - // - //FIXME: Possible leak since I am not freeing the previous - //'value' for the same 'key' + //Update ParamToCurrentValMap with parameter and its + //current value. FIXME: Possible leak since I am not + //freeing the previous 'value' for the same 'key' paramCurrentValue = paramCurrentValue + paramIncrement; (*ParamToCurrentValMap)[parameter] = CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); @@ -361,27 +361,28 @@ namespace BEEV return ret; } //end of recursion FORs - //ASTVec forloopFormulaVector; //Expand the leaf level FOR-construct completely + //increment of paramCurrentValue done inside loop int ThisForLoopAllTrue = 0; - for(;paramCurrentValue < paramLimit; - //increment of paramCurrentValue done inside loop - ) + for(;paramCurrentValue < paramLimit;) { ASTNode currentFormula; - currentFormula = - SimplifyFormula(formulabody, false, ParamToCurrentValMap); - + ASTNode currentExceptFormula = + SimplifyFormula(exceptFormula, false, ParamToCurrentValMap); + if(ASTTrue == currentExceptFormula) + { + currentFormula = ASTTrue; + } + else + { + 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]; - currentFormula = TransformFormula_TopLevel(currentFormula); SOLVER_RETURN_TYPE result = CallSAT_ResultCheck(SatSolver, currentFormula, original_input); @@ -446,7 +447,8 @@ namespace BEEV int paramInit = GetUnsignedConst(finiteloop[1]); int paramLimit = GetUnsignedConst(finiteloop[2]); int paramIncrement = GetUnsignedConst(finiteloop[3]); - ASTNode formulabody = finiteloop[4]; + ASTNode exceptFormula = finiteloop[4]; + ASTNode formulabody = finiteloop[5]; int paramCurrentValue = paramInit; //Update ParamToCurrentValMap with parameter and its current @@ -474,11 +476,9 @@ namespace BEEV returnVec.push_back(ret); } - //Update ParamToCurrentValMap with parameter and its current - //value - // - //FIXME: Possible leak since I am not freeing the previous - //'value' for the same 'key' + //Update ParamToCurrentValMap with parameter and its + //current value. FIXME: Possible leak since I am not + //freeing the previous 'value' for the same 'key' paramCurrentValue = paramCurrentValue + paramIncrement; (*ParamToCurrentValMap)[parameter] = CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); @@ -492,20 +492,35 @@ namespace BEEV ASTVec forloopFormulaVector; //Expand the leaf level FOR-construct completely - for(;paramCurrentValue < paramLimit; - //incrementing of paramCurrentValue is done inside loop - ) + //incrementing of paramCurrentValue is done inside loop + for(;paramCurrentValue < paramLimit;) { - ASTNode currentFormula; - currentFormula = - SimplifyFormula(formulabody, false, ParamToCurrentValMap); - + ASTNode currentFormula; + + ASTNode currentExceptFormula = + SimplifyFormula(exceptFormula, false, ParamToCurrentValMap); + if(ASTTrue == currentExceptFormula) + { + currentFormula = ASTTrue; + //continue; + } + else + { + currentFormula = + SimplifyFormula(formulabody, false, ParamToCurrentValMap); + } + if(checkusingmodel_flag) { - //Check the currentformula against the model, and add it to the - //SAT solver if it is false against the model - if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) - return ASTFalse; + //Check the currentformula against the model, and return + //immediately + //cout << "Printing current Formula: " << currentFormula << "\n"; + ASTNode computedForm = ComputeFormulaUsingModel(currentFormula); + //cout << "Printing computed Formula: " << computedForm << "\n"; + if(ASTFalse == computedForm) + { + return ASTFalse; + } } else { diff --git a/src/main/main.cpp b/src/main/main.cpp index 5a99df4..16cc0eb 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -200,6 +200,7 @@ int main(int argc, char ** argv) { return 0; } //end of PrintBack if - GlobalBeevMgr->TopLevelSAT(asserts, query); + SOLVER_RETURN_TYPE ret = GlobalBeevMgr->TopLevelSAT(asserts, query); + GlobalBeevMgr->PrintOutput(ret); return 0; }//end of Main diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex index 548bb6d..30954d7 100644 --- a/src/parser/CVC.lex +++ b/src/parser/CVC.lex @@ -56,6 +56,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) "NOR" { return NOR_TOK;} "NOT" { return NOT_TOK; } "FOR" { return FOR_TOK; } +"EXCEPT" { return EXCEPT_TOK; } "OR" { return OR_TOK; } "/=" { return NEQ_TOK; } ":=" { return ASSIGN_TOK;} diff --git a/src/parser/CVC.y b/src/parser/CVC.y index fc35e6d..c163668 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -29,7 +29,7 @@ int yyerror(const char *s) { cout << "syntax error: line " << cvclineno << "\n" << s << endl; FatalError(""); - return YY_EXIT_FAILURE; /* Dill: don't know what it should return */ + return YY_EXIT_FAILURE; }; %} @@ -60,6 +60,7 @@ %token OR_TOK "OR" %token NOT_TOK "NOT" %token FOR_TOK "FOR" +%token EXCEPT_TOK "EXCEPT" %token XOR_TOK "XOR" %token NAND_TOK "NAND" %token NOR_TOK "NOR" @@ -451,7 +452,7 @@ Formula : '(' Formula ')' { $$ = $2; } delete $1; delete $3; } - | FOR_TOK '(' ForDecl ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}' + | FOR_TOK '(' ForDecl ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ';' EXCEPT_TOK Formula ')' '{' Formula '}' { //Allows a compact representation of //parameterized set of formulas (bounded @@ -473,6 +474,40 @@ Formula : '(' Formula ')' { $$ = $2; } vec.push_back(*$7); vec.push_back(*$9); vec.push_back(*$12); + vec.push_back(*$15); + ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(FOR,vec)); + GlobalBeevMgr->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + delete $7; + delete $9; + delete $12; + delete $15; + } + | FOR_TOK '(' ForDecl ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}' + { + //Allows a compact representation of + //parameterized set of formulas (bounded + //universal quantification) + // + //parameter name (a variable) + // + //initial value (BVCONST) + // + //limit value (BVCONST) + // + //increment value (BVCONST) + // + //formula (it can be a nested forloop) + + ASTVec vec; + vec.push_back(*$3); + vec.push_back(*$5); + vec.push_back(*$7); + vec.push_back(*$9); + vec.push_back(GlobalBeevMgr->CreateNode(FALSE)); + vec.push_back(*$12); ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(FOR,vec)); GlobalBeevMgr->BVTypeCheck(*n); $$ = n; diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index d538f11..5e8f864 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -1322,7 +1322,8 @@ ASTNode Flatten(const ASTNode& a) { output = t1; } - else if (CheckAlwaysTrueFormMap(CreateNode(NOT, t0)) || (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0]))) + else if (CheckAlwaysTrueFormMap(CreateNode(NOT, t0)) || + (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0]))) { output = t2; } @@ -1408,7 +1409,7 @@ ASTNode Flatten(const ASTNode& a) if (CheckSubstitutionMap(inputterm, output)) { //cout << "SolverMap:" << inputterm << " output: " << output << endl; - return SimplifyTerm(output); + return SimplifyTerm(output, VarConstMap); } if (CheckSimplifyMap(inputterm, output, false, VarConstMap)) @@ -1442,7 +1443,7 @@ ASTNode Flatten(const ASTNode& a) } if (CheckSolverMap(inputterm, output)) { - return SimplifyTerm(output); + return SimplifyTerm(output, VarConstMap); } output = inputterm; break; @@ -1523,7 +1524,7 @@ ASTNode Flatten(const ASTNode& a) //sort, and create BVPLUS/BVMULT and return for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) { - ASTNode aaa = SimplifyTerm(*it); + ASTNode aaa = SimplifyTerm(*it, VarConstMap); if (BVCONST == aaa.GetKind()) { constkids.push_back(aaa); @@ -1644,8 +1645,8 @@ ASTNode Flatten(const ASTNode& a) case BVSUB: { ASTVec c = inputterm.GetChildren(); - ASTNode a0 = SimplifyTerm(inputterm[0]); - ASTNode a1 = SimplifyTerm(inputterm[1]); + ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap); + ASTNode a1 = SimplifyTerm(inputterm[1], VarConstMap); unsigned int l = inputValueWidth; if (a0 == a1) output = CreateZeroConst(l); @@ -1654,8 +1655,8 @@ ASTNode Flatten(const ASTNode& a) //covert x-y into x+(-y) and simplify. this transformation //triggers more simplifications // - a1 = SimplifyTerm(CreateTerm(BVUMINUS, l, a1)); - output = SimplifyTerm(CreateTerm(BVPLUS, l, a0, a1)); + a1 = SimplifyTerm(CreateTerm(BVUMINUS, l, a1), VarConstMap); + output = SimplifyTerm(CreateTerm(BVPLUS, l, a0, a1), VarConstMap); } break; } @@ -1666,7 +1667,7 @@ ASTNode Flatten(const ASTNode& a) //actually 0. One way to reveal this fact is to strip bvuminus //out, and replace with something else so that combineliketerms //can catch this fact. - ASTNode a0 = SimplifyTerm(inputterm[0]); + ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap); Kind k1 = a0.GetKind(); unsigned int l = a0.GetValueWidth(); ASTNode one = CreateOneConst(l); @@ -1682,7 +1683,7 @@ ASTNode Flatten(const ASTNode& a) } case BVNEG: { - output = SimplifyTerm(CreateTerm(BVPLUS, l, a0[0], one)); + output = SimplifyTerm(CreateTerm(BVPLUS, l, a0[0], one), VarConstMap); break; } case BVMULT: @@ -1703,7 +1704,7 @@ ASTNode Flatten(const ASTNode& a) // not -(3*x). if (BVCONST == a0[0].GetKind()) { - ASTNode a00 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[0])); + ASTNode a00 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[0]), VarConstMap); output = CreateTerm(BVMULT, l, a00, a0[1]); } else @@ -1723,25 +1724,25 @@ ASTNode Flatten(const ASTNode& a) for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) { //Simplify(BVUMINUS(a1x1)) - ASTNode aaa = SimplifyTerm(CreateTerm(BVUMINUS, l, *it)); + ASTNode aaa = SimplifyTerm(CreateTerm(BVUMINUS, l, *it), VarConstMap); o.push_back(aaa); } //simplify the bvplus - output = SimplifyTerm(CreateTerm(BVPLUS, l, o)); + output = SimplifyTerm(CreateTerm(BVPLUS, l, o), VarConstMap); break; } case BVSUB: { //BVUMINUS(BVSUB(x,y)) <=> BVSUB(y,x) - output = SimplifyTerm(CreateTerm(BVSUB, l, a0[1], a0[0])); + output = SimplifyTerm(CreateTerm(BVSUB, l, a0[1], a0[0]), VarConstMap); break; } case ITE: { //BVUMINUS(ITE(c,t1,t2)) <==> ITE(c,BVUMINUS(t1),BVUMINUS(t2)) ASTNode c = a0[0]; - ASTNode t1 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[1])); - ASTNode t2 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[2])); + ASTNode t1 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[1]), VarConstMap); + ASTNode t2 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[2]), VarConstMap); output = CreateSimplifiedTermITE(c, t1, t2); break; } @@ -1758,7 +1759,7 @@ ASTNode Flatten(const ASTNode& a) //it is important to take care of wordlevel transformation in //BVEXTRACT. it exposes oppurtunities for later simplification //and solving (variable elimination) - ASTNode a0 = SimplifyTerm(inputterm[0]); + ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap); Kind k1 = a0.GetKind(); unsigned int a_len = inputValueWidth; @@ -1800,7 +1801,7 @@ ASTNode Flatten(const ASTNode& a) //Apply the following rule: // (t@u)[i:j] <==> u[i:j], if len(u) > i // - output = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, u, i, j)); + output = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, u, i, j), VarConstMap); } else if (len_a0 > i_val && j_val >= len_u) { @@ -1808,7 +1809,7 @@ ASTNode Flatten(const ASTNode& a) // (t@u)[i:j] <==> t[i-len_u:j-len_u], if len(t@u) > i >= j >= len(u) i = CreateBVConst(32, i_val - len_u); j = CreateBVConst(32, j_val - len_u); - output = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j)); + output = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j), VarConstMap); } else { @@ -1816,8 +1817,8 @@ ASTNode Flatten(const ASTNode& a) // (t@u)[i:j] <==> t[i-len_u:0] @ u[len_u-1:j] i = CreateBVConst(32, i_val - len_u); ASTNode m = CreateBVConst(32, len_u - 1); - t = SimplifyTerm(CreateTerm(BVEXTRACT, i_val - len_u + 1, t, i, zero)); - u = SimplifyTerm(CreateTerm(BVEXTRACT, len_u - j_val, u, m, j)); + t = SimplifyTerm(CreateTerm(BVEXTRACT, i_val - len_u + 1, t, i, zero), VarConstMap); + u = SimplifyTerm(CreateTerm(BVEXTRACT, len_u - j_val, u, m, j), VarConstMap); output = CreateTerm(BVCONCAT, a_len, t, u); } break; @@ -1832,7 +1833,7 @@ ASTNode Flatten(const ASTNode& a) for (ASTVec::iterator jt = c.begin(), jtend = c.end(); jt != jtend; jt++) { ASTNode aaa = *jt; - aaa = SimplifyTerm(CreateTerm(BVEXTRACT, i_val + 1, aaa, i, zero)); + aaa = SimplifyTerm(CreateTerm(BVEXTRACT, i_val + 1, aaa, i, zero), VarConstMap); o.push_back(aaa); } output = CreateTerm(a0.GetKind(), i_val + 1, o); @@ -1852,8 +1853,8 @@ ASTNode Flatten(const ASTNode& a) // (t op u)[i:j] <==> t[i:j] op u[i:j] ASTNode t = a0[0]; ASTNode u = a0[1]; - t = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j)); - u = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, u, i, j)); + t = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j), VarConstMap); + u = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, u, i, j), VarConstMap); BVTypeCheck(t); BVTypeCheck(u); output = CreateTerm(k1, a_len, t, u); @@ -1863,7 +1864,7 @@ ASTNode Flatten(const ASTNode& a) { // (~t)[i:j] <==> ~(t[i:j]) ASTNode t = a0[0]; - t = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j)); + t = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j), VarConstMap); output = CreateTerm(BVNEG, a_len, t); break; } @@ -1886,8 +1887,8 @@ ASTNode Flatten(const ASTNode& a) case ITE: { ASTNode t0 = a0[0]; - ASTNode t1 = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, a0[1], i, j)); - ASTNode t2 = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, a0[2], i, j)); + ASTNode t1 = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, a0[1], i, j), VarConstMap); + ASTNode t2 = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, a0[2], i, j), VarConstMap); output = CreateSimplifiedTermITE(t0, t1, t2); break; } @@ -1901,7 +1902,7 @@ ASTNode Flatten(const ASTNode& a) } case BVNEG: { - ASTNode a0 = SimplifyTerm(inputterm[0]); + ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap); unsigned len = inputValueWidth; switch (a0.GetKind()) { @@ -1913,8 +1914,8 @@ ASTNode Flatten(const ASTNode& a) break; // case ITE: { // ASTNode cond = a0[0]; - // ASTNode thenpart = SimplifyTerm(CreateTerm(BVNEG,len,a0[1])); - // ASTNode elsepart = SimplifyTerm(CreateTerm(BVNEG,len,a0[2])); + // ASTNode thenpart = SimplifyTerm(CreateTerm(BVNEG,len,a0[1]), VarConstMap); + // ASTNode elsepart = SimplifyTerm(CreateTerm(BVNEG,len,a0[2]), VarConstMap); // output = CreateSimplifiedTermITE(cond,thenpart,elsepart); // break; // } @@ -1927,7 +1928,7 @@ ASTNode Flatten(const ASTNode& a) case BVZX: { - ASTNode a0 = SimplifyTerm(inputterm[0]); + ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap); if (a0.GetKind() == BVCONST) output = BVConstEvaluator(CreateTerm(BVZX, inputValueWidth, a0, inputterm[1])); else @@ -1938,7 +1939,7 @@ ASTNode Flatten(const ASTNode& a) case BVSX: { //a0 is the expr which is being sign extended - ASTNode a0 = SimplifyTerm(inputterm[0]); + ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap); //a1 represents the length of the term BVSX(a0) ASTNode a1 = inputterm[1]; //output length of the BVSX term @@ -1985,7 +1986,7 @@ ASTNode Flatten(const ASTNode& a) ASTVec o; for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) { - ASTNode aaa = SimplifyTerm(CreateTerm(BVSX, len, *it, a1)); + ASTNode aaa = SimplifyTerm(CreateTerm(BVSX, len, *it, a1), VarConstMap); o.push_back(aaa); } output = CreateTerm(a0.GetKind(), len, o); @@ -1996,15 +1997,15 @@ ASTNode Flatten(const ASTNode& a) { //if you have BVSX(m,BVSX(n,a)) then you can drop the inner //BVSX provided m is greater than n. - a0 = SimplifyTerm(a0[0]); + a0 = SimplifyTerm(a0[0], VarConstMap); output = CreateTerm(BVSX, len, a0, a1); break; } case ITE: { ASTNode cond = a0[0]; - ASTNode thenpart = SimplifyTerm(CreateTerm(BVSX, len, a0[1], a1)); - ASTNode elsepart = SimplifyTerm(CreateTerm(BVSX, len, a0[2], a1)); + ASTNode thenpart = SimplifyTerm(CreateTerm(BVSX, len, a0[1], a1), VarConstMap); + ASTNode elsepart = SimplifyTerm(CreateTerm(BVSX, len, a0[2], a1), VarConstMap); output = CreateSimplifiedTermITE(cond, thenpart, elsepart); break; } @@ -2028,7 +2029,7 @@ ASTNode Flatten(const ASTNode& a) bool constant = true; for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) { - ASTNode aaa = SimplifyTerm(*it); + ASTNode aaa = SimplifyTerm(*it, VarConstMap); if (BVCONST != aaa.GetKind()) { constant = false; @@ -2070,8 +2071,8 @@ ASTNode Flatten(const ASTNode& a) } case BVCONCAT: { - ASTNode t = SimplifyTerm(inputterm[0]); - ASTNode u = SimplifyTerm(inputterm[1]); + ASTNode t = SimplifyTerm(inputterm[0], VarConstMap); + ASTNode u = SimplifyTerm(inputterm[1], VarConstMap); Kind tkind = t.GetKind(); Kind ukind = u.GetKind(); @@ -2118,7 +2119,7 @@ ASTNode Flatten(const ASTNode& a) bool constant = true; for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) { - ASTNode aaa = SimplifyTerm(*it); + ASTNode aaa = SimplifyTerm(*it, VarConstMap); if (BVCONST != aaa.GetKind()) { constant = false; @@ -2146,13 +2147,13 @@ ASTNode Flatten(const ASTNode& a) else if (ITE == inputterm[0].GetKind()) { ASTNode cond = SimplifyFormula(inputterm[0][0], false, VarConstMap); - ASTNode index = SimplifyTerm(inputterm[1]); + ASTNode index = SimplifyTerm(inputterm[1], VarConstMap); ASTNode read1 = CreateTerm(READ, inputValueWidth, inputterm[0][1], index); ASTNode read2 = CreateTerm(READ, inputValueWidth, inputterm[0][2], index); - read1 = SimplifyTerm(read1); - read2 = SimplifyTerm(read2); + read1 = SimplifyTerm(read1, VarConstMap); + read2 = SimplifyTerm(read2, VarConstMap); out1 = CreateSimplifiedTermITE(cond, read1, read2); } else @@ -2173,8 +2174,8 @@ ASTNode Flatten(const ASTNode& a) case ITE: { ASTNode t0 = SimplifyFormula(inputterm[0], false, VarConstMap); - ASTNode t1 = SimplifyTerm(inputterm[1]); - ASTNode t2 = SimplifyTerm(inputterm[2]); + ASTNode t1 = SimplifyTerm(inputterm[1], VarConstMap); + ASTNode t2 = SimplifyTerm(inputterm[2], VarConstMap); output = CreateSimplifiedTermITE(t0, t1, t2); break; } @@ -2186,7 +2187,7 @@ ASTNode Flatten(const ASTNode& a) ASTVec o; for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) { - ASTNode aaa = SimplifyTerm(*it); + ASTNode aaa = SimplifyTerm(*it, VarConstMap); o.push_back(aaa); } output = CreateTerm(k, inputValueWidth, o); diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index 9e67212..3e5b3c9 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -1752,7 +1752,8 @@ namespace BEEV }; // end of CNFMgr class - int BeevMgr::TopLevelSAT(const ASTNode& inputasserts, const ASTNode& query) + SOLVER_RETURN_TYPE BeevMgr::TopLevelSAT(const ASTNode& inputasserts, + const ASTNode& query) { ASTNode q = CreateNode(AND, inputasserts, CreateNode(NOT, query)); @@ -1793,7 +1794,7 @@ namespace BEEV if (!sat) { - PrintOutput(true); + //PrintOutput(true); return SOLVER_VALID; } else if (SatSolver.okay()) @@ -1818,7 +1819,7 @@ namespace BEEV if (ASTTrue == orig_result) { //CheckCounterExample(SatSolver.okay()); - PrintOutput(false); + //PrintOutput(false); PrintCounterExample(SatSolver.okay()); PrintCounterExample_InOrder(SatSolver.okay()); return SOLVER_INVALID; @@ -1841,7 +1842,7 @@ namespace BEEV else { //Control should never reach here - PrintOutput(true); + //PrintOutput(true); return SOLVER_ERROR; } } //end of CALLSAT_ResultCheck diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index ac85291..76232f0 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -919,7 +919,7 @@ namespace BEEV //Acceps a query, calls the SAT solver and generates Valid/InValid. //if returned 0 then input is INVALID if returned 1 then input is //VALID if returned 2 then UNDECIDED - int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) + SOLVER_RETURN_TYPE BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) { ASTNode inputToSAT = inputasserts; ASTNode orig_input = inputToSAT;