From d974225091684b1ef89576c94fc9c3ee071b5882 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Mon, 21 Sep 2009 18:26:39 +0000 Subject: [PATCH] git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@244 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.cpp | 6 ++- src/AST/AST.h | 23 ++++++++- src/c_interface/c_interface.cpp | 92 +++++++++++++++++++++++++-------- src/c_interface/c_interface.h | 6 ++- src/main/main.cpp | 6 +-- 5 files changed, 106 insertions(+), 27 deletions(-) diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index e7f5aed..35caa2a 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -335,7 +335,7 @@ namespace BEEV ASTNode BeevMgr::CreateBVConst(unsigned int width, unsigned long long int bvconst) { if (width > (sizeof(unsigned long long int) << 3) || width <= 0) - FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, width); + FatalError("CreateBVConst: trying to create a bvconst using unsigned long long of width: ", ASTUndefined, width); CBV bv = CONSTANTBV::BitVector_Create(width, true); unsigned long c_val = (~((unsigned long) 0)) & bvconst; @@ -811,6 +811,10 @@ namespace BEEV case FALSE: case SYMBOL: return true; + case PARAMBOOL: + if(2 != n.Degree()) + FatalError("BVTypeCheck: PARAMBOOL formula can have exactly two childNodes", n); + break; case EQ: if (!(n[0].GetValueWidth() == n[1].GetValueWidth() && n[0].GetIndexWidth() == n[1].GetIndexWidth())) { diff --git a/src/AST/AST.h b/src/AST/AST.h index 41190cf..f8e5235 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -93,6 +93,11 @@ namespace BEEV // Usual constructor. ASTNode(ASTInternal *in); + //Integer that helps sort the ASTNodes. This sorting is different + //from the sorting based on NodeNum. This is used as a way of + //achieving abstraction-refinement. + unsigned int _sort_for_absrefine; + //Equal iff ASTIntNode pointers are the same. friend bool operator==(const ASTNode node1, const ASTNode node2) { @@ -117,6 +122,18 @@ namespace BEEV } public: + //Set the sorting integer for abstraction refinement + void SetAbsRefineInt(unsigned int a) {_sort_for_absrefine = a;} + + //Get the sorting integer for abstraction refinement + unsigned int GetAbsRefineInt(void) {return _sort_for_absrefine;} + + //Compare two ASTNodes based on their abstraction refinement + //number + bool CmpAbsRefine(const ASTNode node1, const ASTNode node2) { + return (node1._sort_for_absrefine < node2._sort_for_absrefine); + } + //Check if it points to a null node bool IsNull() const { @@ -194,6 +211,7 @@ namespace BEEV ASTNode() : _int_node_ptr(NULL) { + _sort_for_absrefine=0; } ; @@ -810,6 +828,9 @@ namespace BEEV ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeCountMap; +// typedef hash_map IntToASTVecMap; // Function to dump contents of ASTNodeMap ostream &operator<<(ostream &os, const ASTNodeMap &nmap); @@ -1506,7 +1527,7 @@ namespace BEEV //by PUSH/POP std::vector _asserts; //The query for the current logical context. - ASTNode _current_query; + ASTNode _current_query; //this flag, when true, indicates that counterexample is being //checked by the counterexample checker diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 3418008..40bfd2d 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -31,27 +31,25 @@ extern int cvcparse(void*); void vc_setFlags(char c) { std::string helpstring = "Usage: stp [-option] [infile]\n\n"; - helpstring += "-r : switch refinement off (optimizations are ON by default)\n"; - helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n"; + helpstring += "STP version: " + BEEV::version + "\n\n"; helpstring += "-a : switch optimizations off (optimizations are ON by default)\n"; - helpstring += "-s : print function statistics\n"; - helpstring += "-v : print nodes \n"; helpstring += "-c : construct counterexample\n"; helpstring += "-d : check counterexample\n"; - helpstring += "-p : print counterexample\n"; - helpstring += "-y : print counterexample in binary\n"; - helpstring += "-b : print STP input back to cout\n"; - helpstring += "-x : flatten nested XORs\n"; + helpstring += "-e : expand finite-for construct\n"; + helpstring += "-f : number of abstraction-refinement loops\n"; helpstring += "-h : help\n"; helpstring += "-m : use the SMTLIB parser\n"; - + helpstring += "-p : print counterexample\n"; + helpstring += "-r : switch refinement off (optimizations are ON by default)\n"; + helpstring += "-s : print function statistics\n"; + helpstring += "-v : print nodes \n"; + helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n"; + helpstring += "-x : flatten nested XORs\n"; + helpstring += "-y : print counterexample in binary\n"; + switch(c) { case 'a' : BEEV::optimize_flag = false; - BEEV::wordlevel_solve_flag = false; - break; - case 'b': - BEEV::print_STPinput_back_flag = true; break; case 'c': BEEV::construct_counterexample_flag = true; @@ -60,13 +58,26 @@ void vc_setFlags(char c) { BEEV::construct_counterexample_flag = true; BEEV::check_counterexample_flag = true; break; + case 'e': + BEEV::expand_finitefor_flag = true; + break; + case 'f': + BEEV::num_absrefine_flag = true; + //BEEV::num_absrefine = atoi(argv[++i]); + break; case 'h': + BEEV::fprintf(stderr,BEEV::usage,BEEV::prog); cout << helpstring; - BEEV::FatalError(""); + //FatalError(""); + //return -1; break; case 'n': BEEV::print_output_flag = true; break; + case 'm': + BEEV::smtlib_parser_flag=true; + BEEV::division_by_zero_returns_one = true; + break; case 'p': BEEV::print_counterexample_flag = true; break; @@ -80,8 +91,8 @@ void vc_setFlags(char c) { BEEV::stats_flag = true; break; case 'u': - BEEV::arraywrite_refinement_flag = true; - break; + BEEV::arraywrite_refinement_flag = false; + break; case 'v' : BEEV::print_nodes_flag = true; break; @@ -89,17 +100,22 @@ void vc_setFlags(char c) { BEEV::wordlevel_solve_flag = false; break; case 'x': - cinterface_exprdelete_on_flag = true; + BEEV::xor_flatten_flag = true; + break; + case 'y': + BEEV::print_binary_flag = true; break; case 'z': BEEV::print_sat_varorder_flag = true; - break; + break; default: std::string s = "C_interface: vc_setFlags: Unrecognized commandline flag:\n"; s += helpstring; BEEV::FatalError(s.c_str()); break; } + + } //Create a validity Checker. This is the global BeevMgr @@ -364,7 +380,7 @@ Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue) { ///////////////////////////////////////////////////////////////////////////// //! Assert a new formula in the current context. /*! The formula must have Boolean type. */ -void vc_assertFormula(VC vc, Expr e) { +void vc_assertFormula(VC vc, Expr e, int absrefine_num) { nodestar a = (nodestar)e; bmstar b = (bmstar)vc; @@ -372,6 +388,7 @@ void vc_assertFormula(VC vc, Expr e) { BEEV::FatalError("Trying to assert a NON formula: ",*a); b->BVTypeCheck(*a); + a->SetAbsRefineInt(absrefine_num); b->AddAssert(*a); } @@ -387,13 +404,12 @@ int vc_query(VC vc, Expr e) { if(!BEEV::is_Form_kind(a->GetKind())) BEEV::FatalError("CInterface: Trying to QUERY a NON formula: ",*a); - //printf("kill all humans\n"); //a->LispPrint(cout, 0); //printf("##################################################\n"); b->BVTypeCheck(*a); b->AddQuery(*a); - const BEEV::ASTVec v = b->GetAsserts(); + const BEEV::ASTVec v = b->GetAsserts(); node o; if(!v.empty()) { if(v.size()==1) @@ -646,6 +662,23 @@ Expr vc_orExprN(VC vc, Expr* cc, int n) { return output; } +Expr vc_bvPlusExprN(VC vc, int n_bits, Expr* cc, int n) { + bmstar b = (bmstar)vc; + nodestar * c = (nodestar *)cc; + nodelist d; + + for(int i =0; i < n; i++) + d.push_back(*c[i]); + + node o = b->CreateTerm(BEEV::BVPLUS, n_bits, d); + b->BVTypeCheck(o); + + nodestar output = new node(o); + //if(cinterface_exprdelete_on) created_exprs.push_back(output); + return output; +} + + Expr vc_iteExpr(VC vc, Expr cond, Expr thenpart, Expr elsepart){ bmstar b = (bmstar)vc; nodestar c = (nodestar)cond; @@ -721,6 +754,23 @@ Expr vc_boolToBVExpr(VC vc, Expr form) { return output; } +Expr vc_paramBoolExpr(VC vc, Expr boolvar, Expr parameter){ + bmstar b = (bmstar)vc; + nodestar c = (nodestar)boolvar; + nodestar t = (nodestar)parameter; + + b->BVTypeCheck(*c); + b->BVTypeCheck(*t); + node o; + + o = b->CreateNode(BEEV::PARAMBOOL,*c,*t); + //b->BVTypeCheck(o); + nodestar output = new node(o); + //if(cinterface_exprdelete_on) created_exprs.push_back(output); + return output; +} + + ///////////////////////////////////////////////////////////////////////////// // BITVECTOR EXPR Creation methods // ///////////////////////////////////////////////////////////////////////////// diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h index 89ede24..863d043 100644 --- a/src/c_interface/c_interface.h +++ b/src/c_interface/c_interface.h @@ -103,6 +103,9 @@ extern "C" { //Boolean to single bit BV Expression Expr vc_boolToBVExpr(VC vc, Expr form); + //Parameterized Boolean Expression (PARAMBOOL, Boolean_Var, parameter) + Expr vc_paramBoolExpr(VC vc, Expr var, Expr param); + // Arrays //! Create an expression for the value of array at the given index @@ -166,7 +169,7 @@ extern "C" { //! Assert a new formula in the current context. /*! The formula must have Boolean type. */ - void vc_assertFormula(VC vc, Expr e); + void vc_assertFormula(VC vc, Expr e, int absrefine_num=0); //! Simplify e with respect to the current context Expr vc_simplify(VC vc, Expr e); @@ -214,6 +217,7 @@ extern "C" { Expr vc_bvConcatExpr(VC vc, Expr left, Expr right); Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right); + Expr vc_bvPlusExprN(VC vc, int n_bits, Expr* children, int numOfChildNodes); Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right); Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right); Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right); diff --git a/src/main/main.cpp b/src/main/main.cpp index ffe6e70..f7bcfa9 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -114,9 +114,6 @@ int main(int argc, char ** argv) { case 'p': print_counterexample_flag = true; break; - case 'y': - print_binary_flag = true; - break; case 'q': print_arrayval_declaredorder_flag = true; break; @@ -141,6 +138,9 @@ int main(int argc, char ** argv) { case 'x': xor_flatten_flag = true; break; + case 'y': + print_binary_flag = true; + break; case 'z': print_sat_varorder_flag = true; break; -- 2.47.3