From: vijay_ganesh Date: Wed, 14 Oct 2009 20:27:36 +0000 (+0000) Subject: formatted using gnu style X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=d4ba96235be210e9366441fbf0f542ee42a81d7f;p=francis%2Fstp.git formatted using gnu style git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@304 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp index 0576d0e..9fe8a37 100644 --- a/src/absrefine_counterexample/AbstractionRefinement.cpp +++ b/src/absrefine_counterexample/AbstractionRefinement.cpp @@ -42,8 +42,8 @@ namespace BEEV SOLVER_RETURN_TYPE AbsRefine_CounterExample:: SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, - const ASTNode& inputAlreadyInSAT, - const ASTNode& original_input) { + const ASTNode& inputAlreadyInSAT, + const ASTNode& original_input) { //printf("doing array read refinement\n"); if (!bm->UserFlags.arrayread_refinement_flag) FatalError("SATBased_ArrayReadRefinement: Control should not reach here"); diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index 46a5309..91e088d 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -858,7 +858,7 @@ namespace BEEV // print functions should print unconditionally. Put a // conditional around the call if you don't want them to print if (!(bm->UserFlags.stats_flag - && bm->UserFlags.print_nodes_flag)) + && bm->UserFlags.print_nodes_flag)) return; int num_vars = newS.nVars(); @@ -927,7 +927,7 @@ namespace BEEV CounterExampleMap.clear(); ConstructCounterExample(SatSolver); if (bm->UserFlags.stats_flag - && bm->UserFlags.print_nodes_flag) + && bm->UserFlags.print_nodes_flag) { PrintSATModel(SatSolver); } @@ -954,7 +954,7 @@ namespace BEEV else { if (bm->UserFlags.stats_flag - && bm->UserFlags.print_nodes_flag) + && bm->UserFlags.print_nodes_flag) { cout << "Supposedly bogus one: \n"; bool tmp = bm->UserFlags.print_counterexample_flag; diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index e6a3065..3e816c8 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -34,8 +34,9 @@ extern int cvcparse(void*); void vc_setFlags(VC vc, char c) { bmstar b = (bmstar)(((stpstar)vc)->bm); - - std::string helpstring = "Usage: stp [-option] [infile]\n\n"; + + std::string helpstring = + "Usage: stp [-option] [infile]\n\n"; helpstring += "STP version: " + BEEV::version + "\n\n"; helpstring += @@ -66,7 +67,7 @@ void vc_setFlags(VC vc, char c) { "-x : flatten nested XORs\n"; helpstring += "-y : print counterexample in binary\n"; - + switch(c) { case 'a' : b->UserFlags.optimize_flag = false; @@ -129,7 +130,9 @@ void vc_setFlags(VC vc, char c) { b->UserFlags.print_sat_varorder_flag = true; break; default: - std::string s = "C_interface: vc_setFlags: Unrecognized commandline flag:\n"; + std::string s = + "C_interface: " \ + "vc_setFlags: Unrecognized commandline flag:\n"; s += helpstring; BEEV::FatalError(s.c_str()); break; @@ -151,7 +154,10 @@ VC vc_createValidityChecker(void) { BEEV::ArrayTransformer * arrayTransformer = new BEEV::ArrayTransformer(bm, simp); BEEV::AbsRefine_CounterExample * Ctr_Example = - new BEEV::AbsRefine_CounterExample(bm, simp, arrayTransformer, tosat); + new BEEV::AbsRefine_CounterExample(bm, + simp, + arrayTransformer, + tosat); BEEV::ParserBM = bm; stpstar stp = @@ -196,13 +202,15 @@ void vc_printExprCCode(VC vc, Expr e) { BEEV::ASTVec declsFromParser = (nodelist)b->ListOfDeclaredVars; for(BEEV::ASTVec::iterator it=declsFromParser.begin(), - itend=declsFromParser.end(); it!=itend;it++) { + itend=declsFromParser.end(); it!=itend;it++) { if(BEEV::BITVECTOR_TYPE == it->GetType()) { const char* name = it->GetName(); unsigned int bitWidth = it->GetValueWidth(); assert(bitWidth % 8 == 0); unsigned int byteWidth = bitWidth / 8; - cout << "unsigned char " << name << "[" << byteWidth << "];" << endl; + cout << "unsigned char " + << name + << "[" << byteWidth << "];" << endl; } else { // vc_printExprCCode: unsupported decl. type @@ -225,17 +233,25 @@ void vc_printExprFile(VC vc, Expr e, int fd) { static void vc_printVarDeclsToStream(VC vc, ostream &os) { for(BEEV::ASTVec::iterator i = decls->begin(), - iend=decls->end();i!=iend;i++) { + iend=decls->end();i!=iend;i++) { node a = *i; switch(a.GetType()) { case BEEV::BITVECTOR_TYPE: a.PL_Print(os); - os << " : BITVECTOR(" << a.GetValueWidth() << ");" << endl; + os << " : BITVECTOR(" + << a.GetValueWidth() + << ");" << endl; break; case BEEV::ARRAY_TYPE: a.PL_Print(os); - os << " : ARRAY " << "BITVECTOR(" << a.GetIndexWidth() << ") OF "; - os << "BITVECTOR(" << a.GetValueWidth() << ");" << endl; + os << " : ARRAY " + << "BITVECTOR(" + << a.GetIndexWidth() + << ") OF "; + os << "BITVECTOR(" + << a.GetValueWidth() + << ");" + << endl; break; case BEEV::BOOLEAN_TYPE: a.PL_Print(os); @@ -276,8 +292,8 @@ void vc_printAsserts(VC vc, int simplify_print) { } void vc_printQueryStateToBuffer(VC vc, Expr e, - char **buf, - unsigned long *len, int simplify_print){ + char **buf, + unsigned long *len, int simplify_print){ assert(vc); assert(e); assert(buf); @@ -380,10 +396,18 @@ Type vc_arrayType(VC vc, Type typeIndex, Type typeData) { nodestar ti = (nodestar)typeIndex; nodestar td = (nodestar)typeData; - if(!(ti->GetKind() == BEEV::BITVECTOR && (*ti)[0].GetKind() == BEEV::BVCONST)) - BEEV::FatalError("Tyring to build array whose indextype i is not a BITVECTOR, where i = ",*ti); - if(!(td->GetKind() == BEEV::BITVECTOR && (*td)[0].GetKind() == BEEV::BVCONST)) - BEEV::FatalError("Trying to build an array whose valuetype v is not a BITVECTOR. where a = ",*td); + if(!(ti->GetKind() == BEEV::BITVECTOR + && (*ti)[0].GetKind() == BEEV::BVCONST)) + { + BEEV::FatalError("Tyring to build array whose"\ + "indextype i is not a BITVECTOR, where i = ",*ti); + } + if(!(td->GetKind() == BEEV::BITVECTOR + && (*td)[0].GetKind() == BEEV::BVCONST)) + { + BEEV::FatalError("Trying to build an array whose"\ + "valuetype v is not a BITVECTOR. where a = ",*td); + } nodestar output = new node(b->CreateNode(BEEV::ARRAY,(*ti)[0],(*td)[0])); //if(cinterface_exprdelete_on) created_exprs.push_back(output); return (Type)output; @@ -459,9 +483,10 @@ int vc_query(VC vc, Expr e) { stpstar stp = ((stpstar)vc); bmstar b = (bmstar)(stp->bm); - if(!BEEV::is_Form_kind(a->GetKind())) - BEEV::FatalError("CInterface: Trying to QUERY a NON formula: ",*a); - + if(!BEEV::is_Form_kind(a->GetKind())) + { + BEEV::FatalError("CInterface: Trying to QUERY a NON formula: ",*a); + } //a->LispPrint(cout, 0); //printf("##################################################\n"); BVTypeCheck(*a); @@ -470,17 +495,21 @@ int vc_query(VC vc, Expr e) { const BEEV::ASTVec v = b->GetAsserts(); node o; int output; - if(!v.empty()) { - if(v.size()==1) { - output = stp->TopLevelSTP(v[0],*a); + if(!v.empty()) + { + if(v.size()==1) + { + output = stp->TopLevelSTP(v[0],*a); + } + else + { + output = stp->TopLevelSTP(b->CreateNode(BEEV::AND,v),*a); + } } - else { - output = stp->TopLevelSTP(b->CreateNode(BEEV::AND,v),*a); + else + { + output = stp->TopLevelSTP(b->CreateNode(BEEV::TRUE),*a); } - } - else { - output = stp->TopLevelSTP(b->CreateNode(BEEV::TRUE),*a); - } return output; } //end of vc_query @@ -562,7 +591,8 @@ WholeCounterExample vc_getWholeCounterExample(VC vc) { ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); CompleteCEStar c = - new BEEV::CompleteCounterExample(ce->GetCompleteCounterExample(), b); + new BEEV::CompleteCounterExample(ce->GetCompleteCounterExample(), + b); return c; } @@ -578,10 +608,11 @@ Expr vc_getTermFromCounterExample(VC vc, Expr e, CompleteCEStar cc) { int vc_getBVLength(VC vc, Expr ex) { nodestar e = (nodestar)ex; - if(BEEV::BITVECTOR_TYPE != e->GetType()) { - BEEV::FatalError("c_interface: vc_GetBVLength: Input expression must be a bit-vector"); - } - + if(BEEV::BITVECTOR_TYPE != e->GetType()) + { + BEEV::FatalError("c_interface: vc_GetBVLength: " \ + "Input expression must be a bit-vector"); + } return e->GetValueWidth(); } // end of vc_getBVLength @@ -835,7 +866,10 @@ Expr vc_boolToBVExpr(VC vc, Expr form) { BVTypeCheck(*c); if(!is_Form_kind(c->GetKind())) - BEEV::FatalError("CInterface: vc_BoolToBVExpr: You have input a NON formula:",*c); + { + BEEV::FatalError("CInterface: vc_BoolToBVExpr: "\ + "You have input a NON formula:",*c); + } node o; node one = b->CreateOneConst(1); @@ -872,8 +906,11 @@ Type vc_bvType(VC vc, int num_bits) { bmstar b = (bmstar)(((stpstar)vc)->bm); if(!(0 < num_bits)) - BEEV::FatalError("CInterface: number of bits in a bvtype must be a positive integer:", - b->CreateNode(BEEV::UNDEFINED)); + { + BEEV::FatalError("CInterface: number of bits in a bvtype"\ + " must be a positive integer:", + b->CreateNode(BEEV::UNDEFINED)); + } node e = b->CreateBVConst(32, num_bits); nodestar output = new node(b->CreateNode(BEEV::BITVECTOR,e)); @@ -885,11 +922,15 @@ Type vc_bv32Type(VC vc) { return vc_bvType(vc,32); } -Expr vc_bvConstExprFromDecStr(VC vc, const size_t width, const char* decimalInput ) { +Expr vc_bvConstExprFromDecStr(VC vc, + const size_t width, + const char* decimalInput ) +{ bmstar b = (bmstar)(((stpstar)vc)->bm); string *param = new string(decimalInput); - // funny type to get it to compile. fix later when I understand what this does. + // funny type to get it to compile. fix later when I + // understand what this does. node n = b->CreateBVConst((string*&)param, (int)10,(int)width); BVTypeCheck(n); nodestar output = new node(n); @@ -917,8 +958,8 @@ Expr vc_bvConstExprFromInt(VC vc, unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> 64-n_bits; //printf("%ull", max_n_bits); if(v > max_n_bits) { - printf("CInterface: vc_bvConstExprFromInt: "\ - "You are trying to construct a constant %llu >= %d,\n", v, max_n_bits); + printf("CInterface: vc_bvConstExprFromInt: " \ + "Cannot construct a constant %llu >= %d,\n", v, max_n_bits); BEEV::FatalError("FatalError"); } node n = b->CreateBVConst(n_bits, v); @@ -1260,7 +1301,9 @@ Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr ccc) { //convert leftshift to bvconcat if(0 != sh_amt) { node len = b->CreateBVConst(sh_amt, 0); - node o = b->CreateTerm(BEEV::BVCONCAT, a->GetValueWidth() + sh_amt, *a, len); + node o = + b->CreateTerm(BEEV::BVCONCAT, + a->GetValueWidth() + sh_amt, *a, len); BVTypeCheck(o); nodestar output = new node(o); //if(cinterface_exprdelete_on) created_exprs.push_back(output); @@ -1300,7 +1343,10 @@ Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr ccc) { return a; else { if(0== w) - BEEV::FatalError("CInterface: vc_bvRightShiftExpr: cannot have a bitvector of length 0:",*a); + { + BEEV::FatalError("CInterface: vc_bvRightShiftExpr: "\ + "cannot have a bitvector of length 0:",*a); + } nodestar output = new node(b->CreateBVConst(w,0)); //if(cinterface_exprdelete_on) created_exprs.push_back(output); return output; @@ -1327,20 +1373,24 @@ Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child) { assert(child_width>0); - for(int count=32; count >= 0; count--){ - if(count != 32) { - ifpart = vc_eqExpr(vc, sh_amt, - vc_bvConstExprFromInt(vc, shift_width, count)); - thenpart = vc_bvExtract(vc, - vc_bvLeftShiftExpr(vc, count, child), - child_width-1, 0); - - ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); - elsepart = ite; + for(int count=32; count >= 0; count--) + { + if(count != 32) + { + ifpart = vc_eqExpr(vc, sh_amt, + vc_bvConstExprFromInt(vc, shift_width, count)); + thenpart = vc_bvExtract(vc, + vc_bvLeftShiftExpr(vc, count, child), + child_width-1, 0); + + ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); + elsepart = ite; + } + else + { + elsepart = vc_bvConstExprFromInt(vc,child_width, 0); + } } - else - elsepart = vc_bvConstExprFromInt(vc,child_width, 0); - } return ite; } @@ -1350,17 +1400,21 @@ Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs) { Expr elsepart = vc_trueExpr(vc); Expr ite = vc_trueExpr(vc); - for(int count=32; count >= 0; count--){ - if(count != 32) { - ifpart = vc_eqExpr(vc, rhs, - vc_bvConstExprFromInt(vc, 32, 1 << count)); - thenpart = vc_bvRightShiftExpr(vc, count, child); - ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); - elsepart = ite; - } else { - elsepart = vc_bvConstExprFromInt(vc,32, 0); + for(int count=32; count >= 0; count--) + { + if(count != 32) + { + ifpart = vc_eqExpr(vc, rhs, + vc_bvConstExprFromInt(vc, 32, 1 << count)); + thenpart = vc_bvRightShiftExpr(vc, count, child); + ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); + elsepart = ite; + } + else + { + elsepart = vc_bvConstExprFromInt(vc,32, 0); + } } - } return ite; } @@ -1375,17 +1429,21 @@ Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child) { assert(child_width>0); - for(int count=32; count >= 0; count--){ - if(count != 32) { - ifpart = vc_eqExpr(vc, sh_amt, - vc_bvConstExprFromInt(vc, shift_width, count)); - thenpart = vc_bvRightShiftExpr(vc, count, child); - ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); - elsepart = ite; - } else { - elsepart = vc_bvConstExprFromInt(vc,child_width, 0); + for(int count=32; count >= 0; count--) + { + if(count != 32) + { + ifpart = vc_eqExpr(vc, sh_amt, + vc_bvConstExprFromInt(vc, shift_width, count)); + thenpart = vc_bvRightShiftExpr(vc, count, child); + ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); + elsepart = ite; + } + else + { + elsepart = vc_bvConstExprFromInt(vc,child_width, 0); + } } - } return ite; } @@ -1487,7 +1545,11 @@ int getBVInt(Expr e) { nodestar a = (nodestar)e; if(BEEV::BVCONST != a->GetKind()) - BEEV::FatalError("CInterface: getBVInt: Attempting to extract int value from a NON-constant BITVECTOR: ",*a); + { + BEEV::FatalError("CInterface: getBVInt: Attempting to "\ + "extract int value from a NON-constant BITVECTOR: ", + *a); + } return (int)GetUnsignedConst(*a); } @@ -1497,7 +1559,11 @@ unsigned int getBVUnsigned(Expr e) { nodestar a = (nodestar)e; if(BEEV::BVCONST != a->GetKind()) - BEEV::FatalError("getBVUnsigned: Attempting to extract int value from a NON-constant BITVECTOR: ",*a); + { + BEEV::FatalError("getBVUnsigned: Attempting to extract int "\ + "value from a NON-constant BITVECTOR: ", + *a); + } return (unsigned int)GetUnsignedConst(*a); } @@ -1523,24 +1589,28 @@ Expr vc_simplify(VC vc, Expr e) { nodestar a = (nodestar)e; simpstar simp = (simpstar)(((stpstar)vc)->simp); - if(BEEV::BOOLEAN_TYPE == a->GetType()) { - nodestar round1 = new node(simp->SimplifyFormula_TopLevel(*a,false)); - b->Begin_RemoveWrites = true; - nodestar output = new node(simp->SimplifyFormula_TopLevel(*round1,false)); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - b->Begin_RemoveWrites = false; - delete round1; - return output; - } - else { - nodestar round1 = new node(simp->SimplifyTerm(*a)); - b->Begin_RemoveWrites = true; - nodestar output = new node(simp->SimplifyTerm(*round1)); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - b->Begin_RemoveWrites = false; - delete round1; - return output; - } + if(BEEV::BOOLEAN_TYPE == a->GetType()) + { + nodestar round1 = + new node(simp->SimplifyFormula_TopLevel(*a,false)); + b->Begin_RemoveWrites = true; + nodestar output = + new node(simp->SimplifyFormula_TopLevel(*round1,false)); + //if(cinterface_exprdelete_on) created_exprs.push_back(output); + b->Begin_RemoveWrites = false; + delete round1; + return output; + } + else + { + nodestar round1 = new node(simp->SimplifyTerm(*a)); + b->Begin_RemoveWrites = true; + nodestar output = new node(simp->SimplifyTerm(*round1)); + //if(cinterface_exprdelete_on) created_exprs.push_back(output); + b->Begin_RemoveWrites = false; + delete round1; + return output; + } } /* C pointer support: C interface to support C memory arrays in CVCL */ @@ -1560,20 +1630,23 @@ Expr vc_bvReadMemoryArray(VC vc, if(numOfBytes == 1) return vc_readExpr(vc,array,byteIndex); - else { - int count = 1; - Expr a = vc_readExpr(vc,array,byteIndex); - while(--numOfBytes > 0) { - Expr b = vc_readExpr(vc,array, - /*vc_simplify(vc, */ - vc_bvPlusExpr(vc, 32, - byteIndex, - vc_bvConstExprFromInt(vc,32,count)))/*)*/; - a = vc_bvConcatExpr(vc,b,a); - count++; + else + { + int count = 1; + Expr a = vc_readExpr(vc,array,byteIndex); + while(--numOfBytes > 0) + { + Expr b = vc_readExpr(vc,array, + /*vc_simplify(vc, */ + vc_bvPlusExpr(vc, 32, + byteIndex, + vc_bvConstExprFromInt(vc,32, + count))); + a = vc_bvConcatExpr(vc,b,a); + count++; + } + return a; } - return a; - } } Expr vc_bvWriteToMemoryArray(VC vc, @@ -1596,14 +1669,16 @@ Expr vc_bvWriteToMemoryArray(VC vc, while(--numOfBytes > 0) { hi = low-1; low = low-8; - + low_elem = low_elem + 8; hi_elem = low_elem + 7; - + c = vc_bvExtract(vc, element, hi_elem, low_elem); newarray = vc_writeExpr(vc, newarray, - vc_bvPlusExpr(vc, 32, byteIndex, vc_bvConstExprFromInt(vc,32,count)), + vc_bvPlusExpr(vc, 32, + byteIndex, + vc_bvConstExprFromInt(vc,32,count)), c); count++; } @@ -1683,14 +1758,18 @@ Expr getChild(Expr e, int i){ nodestar a = (nodestar)e; BEEV::ASTVec c = a->GetChildren(); - if(0 <= i && (unsigned)i < c.size()) { - BEEV::ASTNode o = c[i]; - nodestar output = new node(o); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return output; - } + if(0 <= i && (unsigned)i < c.size()) + { + BEEV::ASTNode o = c[i]; + nodestar output = new node(o); + //if(cinterface_exprdelete_on) created_exprs.push_back(output); + return output; + } else - BEEV::FatalError("getChild: Error accessing childNode in expression: ",*a); + { + BEEV::FatalError("getChild: Error accessing childNode " \ + "in expression: ",*a); + } return a; } @@ -1711,7 +1790,7 @@ int vc_getHashQueryStateToBuffer(VC vc, Expr query) { Type vc_getType(VC vc, Expr ex) { nodestar e = (nodestar)ex; - + switch(e->GetType()) { case BEEV::BOOLEAN_TYPE: return vc_boolType(vc); @@ -1726,7 +1805,9 @@ Type vc_getType(VC vc, Expr ex) { break; } default: - BEEV::FatalError("c_interface: vc_GetType: expression with bad typing: please check your expression construction"); + BEEV::FatalError("c_interface: vc_GetType: "\ + "expression with bad typing: "\ + "please check your expression construction"); return vc_boolType(vc); break; } @@ -1776,29 +1857,28 @@ int getDegree (Expr e) { int getBVLength(Expr ex) { nodestar e = (nodestar)ex; - - if(BEEV::BITVECTOR_TYPE != e->GetType()) { - BEEV::FatalError("c_interface: vc_GetBVLength: Input expression must be a bit-vector"); - } - + + if(BEEV::BITVECTOR_TYPE != e->GetType()) + { + BEEV::FatalError("c_interface: vc_GetBVLength: "\ + "Input expression must be a bit-vector"); + } + return e->GetValueWidth(); } type_t getType (Expr ex) { - nodestar e = (nodestar)ex; - + nodestar e = (nodestar)ex; return (type_t)(e->GetType()); } int getVWidth (Expr ex) { nodestar e = (nodestar)ex; - return e->GetValueWidth(); } int getIWidth (Expr ex) { nodestar e = (nodestar)ex; - return e->GetIndexWidth(); } @@ -1806,7 +1886,7 @@ void vc_printCounterExampleFile(VC vc, int fd) { fdostream os(fd); bmstar b = (bmstar)(((stpstar)vc)->bm); ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); - + b->UserFlags.print_counterexample_flag = true; os << "COUNTEREXAMPLE BEGIN: \n"; ce->PrintCounterExample(true, os); @@ -1818,7 +1898,6 @@ const char* exprName(Expr e){ } int getExprID (Expr ex) { - BEEV::ASTNode q = (*(nodestar)ex); - + BEEV::ASTNode q = (*(nodestar)ex); return q.GetNodeNum(); } diff --git a/src/main/main.cpp b/src/main/main.cpp index 32a0212..6b97060 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -95,7 +95,7 @@ int main(int argc, char ** argv) { switch(argv[i][1]) { case 'a' : - bm->UserFlags.optimize_flag = false; + bm->UserFlags.optimize_flag = false; break; case 'b': bm->UserFlags.print_STPinput_back_flag = true; diff --git a/src/parser/CVC.y b/src/parser/CVC.y index c658cc2..790a4f5 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -32,11 +32,11 @@ return YY_EXIT_FAILURE; }; -%} + %} %union { - unsigned int uintval; /* for numerals in types. */ + unsigned int uintval; /* for numerals in types. */ struct { //stores the indexwidth and valuewidth //indexwidth is 0 iff type is bitvector. positive iff type is @@ -57,24 +57,24 @@ %start cmd -%token AND_TOK "AND" -%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" -%token IMPLIES_TOK "=>" -%token IFF_TOK "<=>" - -%token IF_TOK "IF" -%token THEN_TOK "THEN" -%token ELSE_TOK "ELSE" -%token ELSIF_TOK "ELSIF" -%token END_TOK "END" -%token ENDIF_TOK "ENDIF" -%token NEQ_TOK "/=" +%token AND_TOK "AND" +%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" +%token IMPLIES_TOK "=>" +%token IFF_TOK "<=>" + +%token IF_TOK "IF" +%token THEN_TOK "THEN" +%token ELSE_TOK "ELSE" +%token ELSIF_TOK "ELSIF" +%token END_TOK "END" +%token ENDIF_TOK "ENDIF" +%token NEQ_TOK "/=" %token ASSIGN_TOK ":=" %token BV_TOK "BV" @@ -125,7 +125,7 @@ %token IN_TOK "IN" %token LET_TOK "LET" -//%token COUNTEREXAMPLE_TOK "COUNTEREXAMPLE" + //%token COUNTEREXAMPLE_TOK "COUNTEREXAMPLE" %token PUSH_TOK "PUSH" %token POP_TOK "POP" @@ -170,931 +170,931 @@ %% cmd : other_cmd - | other_cmd counterexample - ; +| other_cmd counterexample +; counterexample : COUNTEREXAMPLE_TOK ';' - { - ParserBM->UserFlags.print_counterexample_flag = true; - (GlobalSTP->Ctr_Example)->PrintCounterExample(true); - } - ; +{ + ParserBM->UserFlags.print_counterexample_flag = true; + (GlobalSTP->Ctr_Example)->PrintCounterExample(true); +} +; other_cmd : other_cmd1 - | Query - { - ((ASTVec*)AssertsQuery)->push_back(ParserBM->CreateNode(TRUE)); - ((ASTVec*)AssertsQuery)->push_back(*$1); - delete $1; - } - | VarDecls Query - { - ((ASTVec*)AssertsQuery)->push_back(ParserBM->CreateNode(TRUE)); - ((ASTVec*)AssertsQuery)->push_back(*$2); - delete $2; - } - | other_cmd1 Query - { - ASTVec aaa = ParserBM->GetAsserts(); - if(aaa.size() == 0) - { - yyerror("Fatal Error: parsing: GetAsserts() call: no assertions: "); - } - - ASTNode asserts = - aaa.size() == 1 ? - aaa[0] : - ParserBM->CreateNode(AND, aaa); - ((ASTVec*)AssertsQuery)->push_back(asserts); - ((ASTVec*)AssertsQuery)->push_back(*$2); - delete $2; - } - ; +| Query +{ + ((ASTVec*)AssertsQuery)->push_back(ParserBM->CreateNode(TRUE)); + ((ASTVec*)AssertsQuery)->push_back(*$1); + delete $1; +} +| VarDecls Query +{ + ((ASTVec*)AssertsQuery)->push_back(ParserBM->CreateNode(TRUE)); + ((ASTVec*)AssertsQuery)->push_back(*$2); + delete $2; +} +| other_cmd1 Query +{ + ASTVec aaa = ParserBM->GetAsserts(); + if(aaa.size() == 0) + { + yyerror("Fatal Error: parsing: GetAsserts() call: no assertions: "); + } + + ASTNode asserts = + aaa.size() == 1 ? + aaa[0] : + ParserBM->CreateNode(AND, aaa); + ((ASTVec*)AssertsQuery)->push_back(asserts); + ((ASTVec*)AssertsQuery)->push_back(*$2); + delete $2; +} +; other_cmd1 : VarDecls Asserts - { - delete $2; - } - | Asserts - { - delete $1; - } - | other_cmd1 VarDecls Asserts - { - delete $3; - } - ; +{ + delete $2; +} +| Asserts +{ + delete $1; +} +| other_cmd1 VarDecls Asserts +{ + delete $3; +} +; /* push : PUSH_TOK */ /* { */ -/* ParserBM->Push(); */ +/* ParserBM->Push(); */ /* } */ /* | */ /* ; */ /* pop : POP_TOK */ /* { */ -/* ParserBM->Pop(); */ +/* ParserBM->Pop(); */ /* } */ /* | */ /* ; */ Asserts : Assert - { - $$ = new ASTVec; - $$->push_back(*$1); - ParserBM->AddAssert(*$1); - delete $1; - } - | Asserts Assert - { - $1->push_back(*$2); - ParserBM->AddAssert(*$2); - $$ = $1; - delete $2; - } - ; +{ + $$ = new ASTVec; + $$->push_back(*$1); + ParserBM->AddAssert(*$1); + delete $1; +} +| Asserts Assert +{ + $1->push_back(*$2); + ParserBM->AddAssert(*$2); + $$ = $1; + delete $2; +} +; Assert : ASSERT_TOK Formula ';' { $$ = $2; } - ; +; Query : QUERY_TOK Formula ';' { ParserBM->AddQuery(*$2); $$ = $2;} - ; +; /* Grammar for Variable Declaration */ -VarDecls : VarDecl ';' - { - } - | VarDecls VarDecl ';' - { - } - ; - -VarDecl : FORM_IDs ':' Type - { - for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { - _parser_symbol_table.insert(*i); - i->SetIndexWidth($3.indexwidth); - i->SetValueWidth($3.valuewidth); - ParserBM->ListOfDeclaredVars.push_back(*i); - } - delete $1; - } - | FORM_IDs ':' Type '=' Expr - { - //do type checking. if doesn't pass then abort - BVTypeCheck(*$5); - if($3.indexwidth != $5->GetIndexWidth()) - yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); - if($3.valuewidth != $5->GetValueWidth()) - yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); - - for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { - //set the valuewidth of the identifier - i->SetValueWidth($5->GetValueWidth()); - i->SetIndexWidth($5->GetIndexWidth()); - - ParserBM->GetLetMgr()->LetExprMgr(*i,*$5); - delete $5; - } - } - | FORM_IDs ':' Type '=' Formula - { - //do type checking. if doesn't pass then abort - BVTypeCheck(*$5); - if($3.indexwidth != $5->GetIndexWidth()) - yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); - if($3.valuewidth != $5->GetValueWidth()) - yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); - - for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { - //set the valuewidth of the identifier - i->SetValueWidth($5->GetValueWidth()); - i->SetIndexWidth($5->GetIndexWidth()); - - ParserBM->GetLetMgr()->LetExprMgr(*i,*$5); - delete $5; - } - } - ; +VarDecls : VarDecl ';' +{ +} +| VarDecls VarDecl ';' +{ +} +; + +VarDecl : FORM_IDs ':' Type +{ + for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { + _parser_symbol_table.insert(*i); + i->SetIndexWidth($3.indexwidth); + i->SetValueWidth($3.valuewidth); + ParserBM->ListOfDeclaredVars.push_back(*i); + } + delete $1; +} +| FORM_IDs ':' Type '=' Expr +{ + //do type checking. if doesn't pass then abort + BVTypeCheck(*$5); + if($3.indexwidth != $5->GetIndexWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + if($3.valuewidth != $5->GetValueWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + + for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { + //set the valuewidth of the identifier + i->SetValueWidth($5->GetValueWidth()); + i->SetIndexWidth($5->GetIndexWidth()); + + ParserBM->GetLetMgr()->LetExprMgr(*i,*$5); + delete $5; + } +} +| FORM_IDs ':' Type '=' Formula +{ + //do type checking. if doesn't pass then abort + BVTypeCheck(*$5); + if($3.indexwidth != $5->GetIndexWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + if($3.valuewidth != $5->GetValueWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + + for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { + //set the valuewidth of the identifier + i->SetValueWidth($5->GetValueWidth()); + i->SetIndexWidth($5->GetIndexWidth()); + + ParserBM->GetLetMgr()->LetExprMgr(*i,*$5); + delete $5; + } +} +; reverseFORM_IDs : FORMID_TOK - { - $$ = new ASTVec; - $$->push_back(*$1); - delete $1; - } - | FORMID_TOK ',' reverseFORM_IDs - { - $3->push_back(*$1); - $$ = $3; - delete $1; - } - ; +{ + $$ = new ASTVec; + $$->push_back(*$1); + delete $1; +} +| FORMID_TOK ',' reverseFORM_IDs +{ + $3->push_back(*$1); + $$ = $3; + delete $1; +} +; FORM_IDs : reverseFORM_IDs - { - $$ = new ASTVec($1->rbegin(),$1->rend()); - delete $1; - } - ; +{ + $$ = new ASTVec($1->rbegin(),$1->rend()); + delete $1; +} +; ForDecl : FORMID_TOK ':' Type - { - $1->SetIndexWidth($3.indexwidth); - $1->SetValueWidth($3.valuewidth); - _parser_symbol_table.insert(*$1); - $$ = $1; - } +{ + $1->SetIndexWidth($3.indexwidth); + $1->SetValueWidth($3.valuewidth); + _parser_symbol_table.insert(*$1); + $$ = $1; +} /* Grammar for Types */ -Type : BvType { $$ = $1; } - | BoolType { $$ = $1; } - | ArrayType { $$ = $1; } - ; +Type : BvType { $$ = $1; } +| BoolType { $$ = $1; } +| ArrayType { $$ = $1; } +; BvType : BV_TOK '(' NUMERAL_TOK ')' - { - /*((indexwidth is 0) && (valuewidth>0)) iff type is BV*/ - $$.indexwidth = 0; - unsigned int length = $3; - if(length > 0) { - $$.valuewidth = length; - } - else - FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); - } - ; +{ + /*((indexwidth is 0) && (valuewidth>0)) iff type is BV*/ + $$.indexwidth = 0; + unsigned int length = $3; + if(length > 0) { + $$.valuewidth = length; + } + else + FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); +} +; BoolType : BOOLEAN_TOK - { - $$.indexwidth = 0; - $$.valuewidth = 0; - } - ; +{ + $$.indexwidth = 0; + $$.valuewidth = 0; +} +; ArrayType : ARRAY_TOK BvType OF_TOK BvType - { - $$.indexwidth = $2.valuewidth; - $$.valuewidth = $4.valuewidth; - } - ; +{ + $$.indexwidth = $2.valuewidth; + $$.valuewidth = $4.valuewidth; +} +; /*Grammar for ITEs which are a type of Term*/ -IfExpr : IF_TOK Formula THEN_TOK Expr ElseRestExpr - { - unsigned int width = $4->GetValueWidth(); - if (width != $5->GetValueWidth()) - yyerror("Width mismatch in IF-THEN-ELSE"); - if($4->GetIndexWidth() != $5->GetIndexWidth()) - yyerror("Width mismatch in IF-THEN-ELSE"); - - BVTypeCheck(*$2); - BVTypeCheck(*$4); - BVTypeCheck(*$5); - $$ = new ASTNode(ParserBM->CreateTerm(ITE, width, *$2, *$4, *$5)); - $$->SetIndexWidth($5->GetIndexWidth()); - BVTypeCheck(*$$); - delete $2; - delete $4; - delete $5; - } - ; - -ElseRestExpr : ELSE_TOK Expr ENDIF_TOK { $$ = $2; } - | ELSIF_TOK Expr THEN_TOK Expr ElseRestExpr - { - unsigned int width = $2->GetValueWidth(); - if (width != $4->GetValueWidth() || width != $5->GetValueWidth()) - yyerror("Width mismatch in IF-THEN-ELSE"); - if ($2->GetIndexWidth() != $4->GetValueWidth() || $2->GetIndexWidth() != $5->GetValueWidth()) - yyerror("Width mismatch in IF-THEN-ELSE"); - - BVTypeCheck(*$2); - BVTypeCheck(*$4); - BVTypeCheck(*$5); - $$ = new ASTNode(ParserBM->CreateTerm(ITE, width, *$2, *$4, *$5)); - $$->SetIndexWidth($5->GetIndexWidth()); - BVTypeCheck(*$$); - delete $2; - delete $4; - delete $5; - } - ; +IfExpr : IF_TOK Formula THEN_TOK Expr ElseRestExpr +{ + unsigned int width = $4->GetValueWidth(); + if (width != $5->GetValueWidth()) + yyerror("Width mismatch in IF-THEN-ELSE"); + if($4->GetIndexWidth() != $5->GetIndexWidth()) + yyerror("Width mismatch in IF-THEN-ELSE"); + + BVTypeCheck(*$2); + BVTypeCheck(*$4); + BVTypeCheck(*$5); + $$ = new ASTNode(ParserBM->CreateTerm(ITE, width, *$2, *$4, *$5)); + $$->SetIndexWidth($5->GetIndexWidth()); + BVTypeCheck(*$$); + delete $2; + delete $4; + delete $5; +} +; + +ElseRestExpr : ELSE_TOK Expr ENDIF_TOK { $$ = $2; } +| ELSIF_TOK Expr THEN_TOK Expr ElseRestExpr +{ + unsigned int width = $2->GetValueWidth(); + if (width != $4->GetValueWidth() || width != $5->GetValueWidth()) + yyerror("Width mismatch in IF-THEN-ELSE"); + if ($2->GetIndexWidth() != $4->GetValueWidth() || $2->GetIndexWidth() != $5->GetValueWidth()) + yyerror("Width mismatch in IF-THEN-ELSE"); + + BVTypeCheck(*$2); + BVTypeCheck(*$4); + BVTypeCheck(*$5); + $$ = new ASTNode(ParserBM->CreateTerm(ITE, width, *$2, *$4, *$5)); + $$->SetIndexWidth($5->GetIndexWidth()); + BVTypeCheck(*$$); + delete $2; + delete $4; + delete $5; +} +; /* Grammar for formulas */ -Formula : '(' Formula ')' - { - $$ = $2; - } - | FORMID_TOK - { - $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); delete $1; - } - | FORMID_TOK '(' Expr ')' - { - $$ = new ASTNode(ParserBM->CreateNode(PARAMBOOL,*$1,*$3)); - delete $1; - delete $3; - } - | BOOLEXTRACT_TOK '(' Expr ',' NUMERAL_TOK ')' - { - unsigned int width = $3->GetValueWidth(); - if(width <= (unsigned)$5) - yyerror("Fatal Error: BOOLEXTRACT: trying to boolextract a bit which beyond range"); - - ASTNode hi = ParserBM->CreateBVConst(32, $5); - ASTNode low = ParserBM->CreateBVConst(32, $5); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVEXTRACT,1,*$3,hi,low)); - BVTypeCheck(*n); - ASTNode zero = ParserBM->CreateBVConst(1,0); - ASTNode * out = new ASTNode(ParserBM->CreateNode(EQ,*n,zero)); - BVTypeCheck(*out); - - $$ = out; - delete $3; - } - | Expr '=' Expr - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(EQ, *$1, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $1; - delete $3; - } - | Expr NEQ_TOK Expr - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(NOT, ParserBM->CreateNode(EQ, *$1, *$3))); - BVTypeCheck(*n); - $$ = n; - delete $1; - delete $3; - } - | FOR_TOK '(' ForDecl ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ';' EXCEPT_TOK Formula ')' '{' 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(*$12); - vec.push_back(*$15); - ASTNode * n = new ASTNode(ParserBM->CreateNode(FOR,vec)); - 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(ParserBM->CreateNode(FALSE)); - vec.push_back(*$12); - ASTNode * n = new ASTNode(ParserBM->CreateNode(FOR,vec)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $5; - delete $7; - delete $9; - delete $12; - } - | NOT_TOK Formula - { - $$ = new ASTNode(ParserBM->CreateNode(NOT, *$2)); - delete $2; - } - | Formula OR_TOK Formula %prec OR_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(OR, *$1, *$3)); - delete $1; - delete $3; - } - | Formula NOR_TOK Formula - { - $$ = new ASTNode(ParserBM->CreateNode(NOR, *$1, *$3)); - delete $1; - delete $3; - } - | Formula AND_TOK Formula %prec AND_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(AND, *$1, *$3)); - delete $1; - delete $3; - } - | Formula NAND_TOK Formula - { - $$ = new ASTNode(ParserBM->CreateNode(NAND, *$1, *$3)); - delete $1; - delete $3; - } - | Formula IMPLIES_TOK Formula - { - $$ = new ASTNode(ParserBM->CreateNode(IMPLIES, *$1, *$3)); - delete $1; - delete $3; - } - | Formula IFF_TOK Formula - { - $$ = new ASTNode(ParserBM->CreateNode(IFF, *$1, *$3)); - delete $1; - delete $3; - } - | Formula XOR_TOK Formula - { - $$ = new ASTNode(ParserBM->CreateNode(XOR, *$1, *$3)); - delete $1; - delete $3; - } - | BVLT_TOK '(' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVLT, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $5; - } - | BVGT_TOK '(' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVGT, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $5; - } - | BVLE_TOK '(' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVLE, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $5; - } - | BVGE_TOK '(' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVGE, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $5; - } - | BVSLT_TOK '(' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSLT, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $5; - } - | BVSGT_TOK '(' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSGT, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $5; - } - | BVSLE_TOK '(' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSLE, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $5; - } - | BVSGE_TOK '(' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSGE, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $5; - } - | IfForm - | TRUELIT_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(TRUE)); - $$->SetIndexWidth(0); - $$->SetValueWidth(0); - } - | FALSELIT_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(FALSE)); - $$->SetIndexWidth(0); - $$->SetValueWidth(0); - } - - | LET_TOK LetDecls IN_TOK Formula - { - $$ = $4; - //Cleanup the LetIDToExprMap - ParserBM->GetLetMgr()->CleanupLetIDMap(); - } - ; +Formula : '(' Formula ')' +{ + $$ = $2; +} +| FORMID_TOK +{ + $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); delete $1; +} +| FORMID_TOK '(' Expr ')' +{ + $$ = new ASTNode(ParserBM->CreateNode(PARAMBOOL,*$1,*$3)); + delete $1; + delete $3; +} +| BOOLEXTRACT_TOK '(' Expr ',' NUMERAL_TOK ')' +{ + unsigned int width = $3->GetValueWidth(); + if(width <= (unsigned)$5) + yyerror("Fatal Error: BOOLEXTRACT: trying to boolextract a bit which beyond range"); + + ASTNode hi = ParserBM->CreateBVConst(32, $5); + ASTNode low = ParserBM->CreateBVConst(32, $5); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVEXTRACT,1,*$3,hi,low)); + BVTypeCheck(*n); + ASTNode zero = ParserBM->CreateBVConst(1,0); + ASTNode * out = new ASTNode(ParserBM->CreateNode(EQ,*n,zero)); + BVTypeCheck(*out); + + $$ = out; + delete $3; +} +| Expr '=' Expr +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(EQ, *$1, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $1; + delete $3; +} +| Expr NEQ_TOK Expr +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(NOT, ParserBM->CreateNode(EQ, *$1, *$3))); + BVTypeCheck(*n); + $$ = n; + delete $1; + delete $3; +} +| FOR_TOK '(' ForDecl ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ';' EXCEPT_TOK Formula ')' '{' 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(*$12); + vec.push_back(*$15); + ASTNode * n = new ASTNode(ParserBM->CreateNode(FOR,vec)); + 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(ParserBM->CreateNode(FALSE)); + vec.push_back(*$12); + ASTNode * n = new ASTNode(ParserBM->CreateNode(FOR,vec)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + delete $7; + delete $9; + delete $12; +} +| NOT_TOK Formula +{ + $$ = new ASTNode(ParserBM->CreateNode(NOT, *$2)); + delete $2; +} +| Formula OR_TOK Formula %prec OR_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(OR, *$1, *$3)); + delete $1; + delete $3; +} +| Formula NOR_TOK Formula +{ + $$ = new ASTNode(ParserBM->CreateNode(NOR, *$1, *$3)); + delete $1; + delete $3; +} +| Formula AND_TOK Formula %prec AND_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(AND, *$1, *$3)); + delete $1; + delete $3; +} +| Formula NAND_TOK Formula +{ + $$ = new ASTNode(ParserBM->CreateNode(NAND, *$1, *$3)); + delete $1; + delete $3; +} +| Formula IMPLIES_TOK Formula +{ + $$ = new ASTNode(ParserBM->CreateNode(IMPLIES, *$1, *$3)); + delete $1; + delete $3; +} +| Formula IFF_TOK Formula +{ + $$ = new ASTNode(ParserBM->CreateNode(IFF, *$1, *$3)); + delete $1; + delete $3; +} +| Formula XOR_TOK Formula +{ + $$ = new ASTNode(ParserBM->CreateNode(XOR, *$1, *$3)); + delete $1; + delete $3; +} +| BVLT_TOK '(' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVLT, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; +} +| BVGT_TOK '(' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVGT, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; +} +| BVLE_TOK '(' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVLE, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; +} +| BVGE_TOK '(' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVGE, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; +} +| BVSLT_TOK '(' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSLT, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; +} +| BVSGT_TOK '(' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSGT, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; +} +| BVSLE_TOK '(' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSLE, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; +} +| BVSGE_TOK '(' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSGE, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; +} +| IfForm +| TRUELIT_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(TRUE)); + $$->SetIndexWidth(0); + $$->SetValueWidth(0); +} +| FALSELIT_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(FALSE)); + $$->SetIndexWidth(0); + $$->SetValueWidth(0); +} + +| LET_TOK LetDecls IN_TOK Formula +{ + $$ = $4; + //Cleanup the LetIDToExprMap + ParserBM->GetLetMgr()->CleanupLetIDMap(); +} +; /*Grammar for ITEs which are Formulas */ -IfForm : IF_TOK Formula THEN_TOK Formula ElseRestForm - { - $$ = new ASTNode(ParserBM->CreateNode(ITE, *$2, *$4, *$5)); - delete $2; - delete $4; - delete $5; - } - ; - -ElseRestForm : ELSE_TOK Formula ENDIF_TOK { $$ = $2; } - | ELSIF_TOK Formula THEN_TOK Formula ElseRestForm - { - $$ = new ASTNode(ParserBM->CreateNode(ITE, *$2, *$4, *$5)); - delete $2; - delete $4; - delete $5; - } - ; +IfForm : IF_TOK Formula THEN_TOK Formula ElseRestForm +{ + $$ = new ASTNode(ParserBM->CreateNode(ITE, *$2, *$4, *$5)); + delete $2; + delete $4; + delete $5; +} +; + +ElseRestForm : ELSE_TOK Formula ENDIF_TOK { $$ = $2; } +| ELSIF_TOK Formula THEN_TOK Formula ElseRestForm +{ + $$ = new ASTNode(ParserBM->CreateNode(ITE, *$2, *$4, *$5)); + delete $2; + delete $4; + delete $5; +} +; /*Grammar for a list of expressions*/ -Exprs : Expr - { - $$ = new ASTVec; - BVTypeCheck(*$1); - $$->push_back(*$1); - delete $1; - } - | Exprs ',' Expr - { - $1->push_back(*$3); - BVTypeCheck(*$3); - $$ = $1; - delete $3; - } - ; +Exprs : Expr +{ + $$ = new ASTVec; + BVTypeCheck(*$1); + $$->push_back(*$1); + delete $1; +} +| Exprs ',' Expr +{ + $1->push_back(*$3); + BVTypeCheck(*$3); + $$ = $1; + delete $3; +} +; /* Grammar for Expr */ -Expr : TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); delete $1;} - | '(' Expr ')' { $$ = $2; } - | BVCONST_TOK { $$ = $1; } - | BOOL_TO_BV_TOK '(' Formula ')' - { - BVTypeCheck(*$3); - ASTNode one = ParserBM->CreateBVConst(1,1); - ASTNode zero = ParserBM->CreateBVConst(1,0); - - //return ITE(*$3, length(1), 0bin1, 0bin0) - $$ = new ASTNode(ParserBM->CreateTerm(ITE,1,*$3,one,zero)); - delete $3; - } - | Expr '[' Expr ']' - { - // valuewidth is same as array, indexwidth is 0. - unsigned int width = $1->GetValueWidth(); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(READ, width, *$1, *$3)); - BVTypeCheck(*n); - $$ = n; - - delete $1; - delete $3; - } - | Expr '(' Expr ')' //array read but in the form of a uninterpreted function application - { - // valuewidth is same as array, indexwidth is 0. - unsigned int width = $1->GetValueWidth(); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(READ, width, *$1, *$3)); - BVTypeCheck(*n); - $$ = n; - - delete $1; - delete $3; - } - | Expr '[' NUMERAL_TOK ':' NUMERAL_TOK ']' - { - int width = $3 - $5 + 1; - if (width < 0) - yyerror("Negative width in extract"); - - if((unsigned)$3 >= $1->GetValueWidth()) - yyerror("Parsing: Wrong width in BVEXTRACT\n"); - - ASTNode hi = ParserBM->CreateBVConst(32, $3); - ASTNode low = ParserBM->CreateBVConst(32, $5); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVEXTRACT, width, *$1,hi,low)); - BVTypeCheck(*n); - $$ = n; - delete $1; - } - | BVNEG_TOK Expr - { - unsigned int width = $2->GetValueWidth(); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNEG, width, *$2)); - BVTypeCheck(*n); - $$ = n; - delete $2; - } - | Expr BVAND_TOK Expr - { - unsigned int width = $1->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in AND"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVAND, width, *$1, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $1; - delete $3; - } - | Expr BVOR_TOK Expr - { - unsigned int width = $1->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in OR"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVOR, width, *$1, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $1; - delete $3; - } - | BVXOR_TOK '(' Expr ',' Expr ')' - { - unsigned int width = $3->GetValueWidth(); - if (width != $5->GetValueWidth()) { - yyerror("Width mismatch in XOR"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVXOR, width, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $5; - } - | BVNAND_TOK '(' Expr ',' Expr ')' - { - unsigned int width = $3->GetValueWidth(); - if (width != $5->GetValueWidth()) { - yyerror("Width mismatch in NAND"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNAND, width, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - - delete $3; - delete $5; - } - | BVNOR_TOK '(' Expr ',' Expr ')' - { - unsigned int width = $3->GetValueWidth(); - if (width != $5->GetValueWidth()) { - yyerror("Width mismatch in NOR"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNOR, width, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - - delete $3; - delete $5; - } - | BVXNOR_TOK '(' Expr ',' Expr ')' - { - unsigned int width = $3->GetValueWidth(); - if (width != $5->GetValueWidth()) { - yyerror("Width mismatch in NOR"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVXNOR, width, *$3, *$5)); - BVTypeCheck(*n); - $$ = n; - - delete $3; - delete $5; - } - | BVSX_TOK '(' Expr ',' NUMERAL_TOK ')' - { - //width of the expr which is being sign - //extended. $5 is the resulting length of the - //signextended expr - BVTypeCheck(*$3); - if($3->GetValueWidth() == $5) { - $$ = $3; - } - else { - ASTNode width = ParserBM->CreateBVConst(32,$5); - ASTNode *n = - new ASTNode(ParserBM->CreateTerm(BVSX, $5,*$3,width)); - BVTypeCheck(*n); - $$ = n; - delete $3; - } - } - | Expr BVCONCAT_TOK Expr - { - unsigned int width = $1->GetValueWidth() + $3->GetValueWidth(); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVCONCAT, width, *$1, *$3)); - BVTypeCheck(*n); - $$ = n; - - delete $1; - delete $3; - } - | Expr BVLEFTSHIFT_TOK NUMERAL_TOK - { - ASTNode zero_bits = ParserBM->CreateZeroConst($3); - ASTNode * n = - new ASTNode(ParserBM->CreateTerm(BVCONCAT, - $1->GetValueWidth() + $3, *$1, zero_bits)); - BVTypeCheck(*n); - $$ = n; - delete $1; - } - | Expr BVRIGHTSHIFT_TOK NUMERAL_TOK - { - ASTNode len = ParserBM->CreateZeroConst($3); - unsigned int w = $1->GetValueWidth(); - - //the amount by which you are rightshifting - //is less-than/equal-to the length of input - //bitvector - if((unsigned)$3 < w) { - ASTNode hi = ParserBM->CreateBVConst(32,w-1); - ASTNode low = ParserBM->CreateBVConst(32,$3); - ASTNode extract = ParserBM->CreateTerm(BVEXTRACT,w-$3,*$1,hi,low); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVCONCAT, w,len, extract)); - BVTypeCheck(*n); - $$ = n; - } - else - $$ = new ASTNode(ParserBM->CreateZeroConst(w)); - - delete $1; - } - | BVPLUS_TOK '(' NUMERAL_TOK ',' Exprs ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVPLUS, $3, *$5)); - BVTypeCheck(*n); - $$ = n; - - delete $5; - } - | BVSUB_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVSUB, $3, *$5, *$7)); - BVTypeCheck(*n); - $$ = n; - - delete $5; - delete $7; - } - | BVUMINUS_TOK '(' Expr ')' - { - unsigned width = $3->GetValueWidth(); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVUMINUS,width,*$3)); - BVTypeCheck(*n); - $$ = n; - delete $3; - } - | BVMULT_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVMULT, $3, *$5, *$7)); - BVTypeCheck(*n); - $$ = n; - - delete $5; - delete $7; - } - | BVDIV_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVDIV, $3, *$5, *$7)); - BVTypeCheck(*n); - $$ = n; - - delete $5; - delete $7; - } - | BVMOD_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVMOD, $3, *$5, *$7)); - BVTypeCheck(*n); - $$ = n; - - delete $5; - delete $7; - } - | SBVDIV_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVDIV, $3, *$5, *$7)); - BVTypeCheck(*n); - $$ = n; - - delete $5; - delete $7; - } - | SBVREM_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' - { - ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVREM, $3, *$5, *$7)); - BVTypeCheck(*n); - $$ = n; - delete $5; - delete $7; - } - | IfExpr { $$ = $1; } - | ArrayUpdateExpr - | LET_TOK LetDecls IN_TOK Expr - { - $$ = $4; - //Cleanup the LetIDToExprMap - //ParserBM->CleanupLetIDMap(); - } - ; +Expr : TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); delete $1;} +| '(' Expr ')' { $$ = $2; } +| BVCONST_TOK { $$ = $1; } +| BOOL_TO_BV_TOK '(' Formula ')' +{ + BVTypeCheck(*$3); + ASTNode one = ParserBM->CreateBVConst(1,1); + ASTNode zero = ParserBM->CreateBVConst(1,0); + + //return ITE(*$3, length(1), 0bin1, 0bin0) + $$ = new ASTNode(ParserBM->CreateTerm(ITE,1,*$3,one,zero)); + delete $3; +} +| Expr '[' Expr ']' +{ + // valuewidth is same as array, indexwidth is 0. + unsigned int width = $1->GetValueWidth(); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(READ, width, *$1, *$3)); + BVTypeCheck(*n); + $$ = n; + + delete $1; + delete $3; +} +| Expr '(' Expr ')' //array read but in the form of a uninterpreted function application +{ + // valuewidth is same as array, indexwidth is 0. + unsigned int width = $1->GetValueWidth(); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(READ, width, *$1, *$3)); + BVTypeCheck(*n); + $$ = n; + + delete $1; + delete $3; +} +| Expr '[' NUMERAL_TOK ':' NUMERAL_TOK ']' +{ + int width = $3 - $5 + 1; + if (width < 0) + yyerror("Negative width in extract"); + + if((unsigned)$3 >= $1->GetValueWidth()) + yyerror("Parsing: Wrong width in BVEXTRACT\n"); + + ASTNode hi = ParserBM->CreateBVConst(32, $3); + ASTNode low = ParserBM->CreateBVConst(32, $5); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVEXTRACT, width, *$1,hi,low)); + BVTypeCheck(*n); + $$ = n; + delete $1; +} +| BVNEG_TOK Expr +{ + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNEG, width, *$2)); + BVTypeCheck(*n); + $$ = n; + delete $2; +} +| Expr BVAND_TOK Expr +{ + unsigned int width = $1->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in AND"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVAND, width, *$1, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $1; + delete $3; +} +| Expr BVOR_TOK Expr +{ + unsigned int width = $1->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in OR"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVOR, width, *$1, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $1; + delete $3; +} +| BVXOR_TOK '(' Expr ',' Expr ')' +{ + unsigned int width = $3->GetValueWidth(); + if (width != $5->GetValueWidth()) { + yyerror("Width mismatch in XOR"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVXOR, width, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; +} +| BVNAND_TOK '(' Expr ',' Expr ')' +{ + unsigned int width = $3->GetValueWidth(); + if (width != $5->GetValueWidth()) { + yyerror("Width mismatch in NAND"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNAND, width, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + + delete $3; + delete $5; +} +| BVNOR_TOK '(' Expr ',' Expr ')' +{ + unsigned int width = $3->GetValueWidth(); + if (width != $5->GetValueWidth()) { + yyerror("Width mismatch in NOR"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNOR, width, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + + delete $3; + delete $5; +} +| BVXNOR_TOK '(' Expr ',' Expr ')' +{ + unsigned int width = $3->GetValueWidth(); + if (width != $5->GetValueWidth()) { + yyerror("Width mismatch in NOR"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVXNOR, width, *$3, *$5)); + BVTypeCheck(*n); + $$ = n; + + delete $3; + delete $5; +} +| BVSX_TOK '(' Expr ',' NUMERAL_TOK ')' +{ + //width of the expr which is being sign + //extended. $5 is the resulting length of the + //signextended expr + BVTypeCheck(*$3); + if($3->GetValueWidth() == $5) { + $$ = $3; + } + else { + ASTNode width = ParserBM->CreateBVConst(32,$5); + ASTNode *n = + new ASTNode(ParserBM->CreateTerm(BVSX, $5,*$3,width)); + BVTypeCheck(*n); + $$ = n; + delete $3; + } +} +| Expr BVCONCAT_TOK Expr +{ + unsigned int width = $1->GetValueWidth() + $3->GetValueWidth(); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVCONCAT, width, *$1, *$3)); + BVTypeCheck(*n); + $$ = n; + + delete $1; + delete $3; +} +| Expr BVLEFTSHIFT_TOK NUMERAL_TOK +{ + ASTNode zero_bits = ParserBM->CreateZeroConst($3); + ASTNode * n = + new ASTNode(ParserBM->CreateTerm(BVCONCAT, + $1->GetValueWidth() + $3, *$1, zero_bits)); + BVTypeCheck(*n); + $$ = n; + delete $1; +} +| Expr BVRIGHTSHIFT_TOK NUMERAL_TOK +{ + ASTNode len = ParserBM->CreateZeroConst($3); + unsigned int w = $1->GetValueWidth(); + + //the amount by which you are rightshifting + //is less-than/equal-to the length of input + //bitvector + if((unsigned)$3 < w) { + ASTNode hi = ParserBM->CreateBVConst(32,w-1); + ASTNode low = ParserBM->CreateBVConst(32,$3); + ASTNode extract = ParserBM->CreateTerm(BVEXTRACT,w-$3,*$1,hi,low); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVCONCAT, w,len, extract)); + BVTypeCheck(*n); + $$ = n; + } + else + $$ = new ASTNode(ParserBM->CreateZeroConst(w)); + + delete $1; +} +| BVPLUS_TOK '(' NUMERAL_TOK ',' Exprs ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVPLUS, $3, *$5)); + BVTypeCheck(*n); + $$ = n; + + delete $5; +} +| BVSUB_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVSUB, $3, *$5, *$7)); + BVTypeCheck(*n); + $$ = n; + + delete $5; + delete $7; +} +| BVUMINUS_TOK '(' Expr ')' +{ + unsigned width = $3->GetValueWidth(); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVUMINUS,width,*$3)); + BVTypeCheck(*n); + $$ = n; + delete $3; +} +| BVMULT_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVMULT, $3, *$5, *$7)); + BVTypeCheck(*n); + $$ = n; + + delete $5; + delete $7; +} +| BVDIV_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVDIV, $3, *$5, *$7)); + BVTypeCheck(*n); + $$ = n; + + delete $5; + delete $7; +} +| BVMOD_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVMOD, $3, *$5, *$7)); + BVTypeCheck(*n); + $$ = n; + + delete $5; + delete $7; +} +| SBVDIV_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVDIV, $3, *$5, *$7)); + BVTypeCheck(*n); + $$ = n; + + delete $5; + delete $7; +} +| SBVREM_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' +{ + ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVREM, $3, *$5, *$7)); + BVTypeCheck(*n); + $$ = n; + delete $5; + delete $7; +} +| IfExpr { $$ = $1; } +| ArrayUpdateExpr +| LET_TOK LetDecls IN_TOK Expr +{ + $$ = $4; + //Cleanup the LetIDToExprMap + //ParserBM->CleanupLetIDMap(); +} +; /*Grammar for Array Update Expr*/ ArrayUpdateExpr : Expr WITH_TOK Updates - { - ASTNode * result; - unsigned int width = $1->GetValueWidth(); - - ASTNodeMap::iterator it = $3->begin(); - ASTNodeMap::iterator itend = $3->end(); - result = new ASTNode(ParserBM->CreateTerm(WRITE, - width, - *$1, - (*it).first, - (*it).second)); - result->SetIndexWidth($1->GetIndexWidth()); - BVTypeCheck(*result); - for(it++;it!=itend;it++) { - result = new ASTNode(ParserBM->CreateTerm(WRITE, - width, - *result, - (*it).first, - (*it).second)); - result->SetIndexWidth($1->GetIndexWidth()); - BVTypeCheck(*result); - } - BVTypeCheck(*result); - $$ = result; - delete $3; - } - ; +{ + ASTNode * result; + unsigned int width = $1->GetValueWidth(); + + ASTNodeMap::iterator it = $3->begin(); + ASTNodeMap::iterator itend = $3->end(); + result = new ASTNode(ParserBM->CreateTerm(WRITE, + width, + *$1, + (*it).first, + (*it).second)); + result->SetIndexWidth($1->GetIndexWidth()); + BVTypeCheck(*result); + for(it++;it!=itend;it++) { + result = new ASTNode(ParserBM->CreateTerm(WRITE, + width, + *result, + (*it).first, + (*it).second)); + result->SetIndexWidth($1->GetIndexWidth()); + BVTypeCheck(*result); + } + BVTypeCheck(*result); + $$ = result; + delete $3; +} +; Updates : '[' Expr ']' ASSIGN_TOK Expr - { - $$ = new ASTNodeMap(); - (*$$)[*$2] = *$5; - } - | Updates WITH_TOK '[' Expr ']' ASSIGN_TOK Expr - { - (*$1)[*$4] = *$7; - } - ; +{ + $$ = new ASTNodeMap(); + (*$$)[*$2] = *$5; +} +| Updates WITH_TOK '[' Expr ']' ASSIGN_TOK Expr +{ + (*$1)[*$4] = *$7; +} +; /*Grammar for LET Expr*/ -LetDecls : LetDecl - | LetDecls ',' LetDecl - ; - -LetDecl : FORMID_TOK '=' Expr - { - //Expr must typecheck - BVTypeCheck(*$3); - - //set the valuewidth of the identifier - $1->SetValueWidth($3->GetValueWidth()); - $1->SetIndexWidth($3->GetIndexWidth()); - - //populate the hashtable from LET-var --> - //LET-exprs and then process them: - // - //1. ensure that LET variables do not clash - //1. with declared variables. - // - //2. Ensure that LET variables are not - //2. defined more than once - ParserBM->GetLetMgr()->LetExprMgr(*$1,*$3); - delete $1; - delete $3; - } - | FORMID_TOK ':' Type '=' Expr - { - //do type checking. if doesn't pass then abort - BVTypeCheck(*$5); - - if($3.indexwidth != $5->GetIndexWidth()) - yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); - if($3.valuewidth != $5->GetValueWidth()) - yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); - - //set the valuewidth of the identifier - $1->SetValueWidth($5->GetValueWidth()); - $1->SetIndexWidth($5->GetIndexWidth()); - - ParserBM->GetLetMgr()->LetExprMgr(*$1,*$5); - delete $1; - delete $5; - } - | FORMID_TOK '=' Formula - { - //Expr must typecheck - BVTypeCheck(*$3); - - //set the valuewidth of the identifier - $1->SetValueWidth($3->GetValueWidth()); - $1->SetIndexWidth($3->GetIndexWidth()); - - //Do LET-expr management - ParserBM->GetLetMgr()->LetExprMgr(*$1,*$3); - delete $1; - delete $3; - } - | FORMID_TOK ':' Type '=' Formula - { - //do type checking. if doesn't pass then abort - BVTypeCheck(*$5); - - if($3.indexwidth != $5->GetIndexWidth()) - yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); - if($3.valuewidth != $5->GetValueWidth()) - yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); - - //set the valuewidth of the identifier - $1->SetValueWidth($5->GetValueWidth()); - $1->SetIndexWidth($5->GetIndexWidth()); - - //Do LET-expr management - ParserBM->GetLetMgr()->LetExprMgr(*$1,*$5); - delete $1; - delete $5; - } - ; +LetDecls : LetDecl +| LetDecls ',' LetDecl +; + +LetDecl : FORMID_TOK '=' Expr +{ + //Expr must typecheck + BVTypeCheck(*$3); + + //set the valuewidth of the identifier + $1->SetValueWidth($3->GetValueWidth()); + $1->SetIndexWidth($3->GetIndexWidth()); + + //populate the hashtable from LET-var --> + //LET-exprs and then process them: + // + //1. ensure that LET variables do not clash + //1. with declared variables. + // + //2. Ensure that LET variables are not + //2. defined more than once + ParserBM->GetLetMgr()->LetExprMgr(*$1,*$3); + delete $1; + delete $3; +} +| FORMID_TOK ':' Type '=' Expr +{ + //do type checking. if doesn't pass then abort + BVTypeCheck(*$5); + + if($3.indexwidth != $5->GetIndexWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + if($3.valuewidth != $5->GetValueWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + + //set the valuewidth of the identifier + $1->SetValueWidth($5->GetValueWidth()); + $1->SetIndexWidth($5->GetIndexWidth()); + + ParserBM->GetLetMgr()->LetExprMgr(*$1,*$5); + delete $1; + delete $5; +} +| FORMID_TOK '=' Formula +{ + //Expr must typecheck + BVTypeCheck(*$3); + + //set the valuewidth of the identifier + $1->SetValueWidth($3->GetValueWidth()); + $1->SetIndexWidth($3->GetIndexWidth()); + + //Do LET-expr management + ParserBM->GetLetMgr()->LetExprMgr(*$1,*$3); + delete $1; + delete $3; +} +| FORMID_TOK ':' Type '=' Formula +{ + //do type checking. if doesn't pass then abort + BVTypeCheck(*$5); + + if($3.indexwidth != $5->GetIndexWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + if($3.valuewidth != $5->GetValueWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + + //set the valuewidth of the identifier + $1->SetValueWidth($5->GetValueWidth()); + $1->SetIndexWidth($5->GetIndexWidth()); + + //Do LET-expr management + ParserBM->GetLetMgr()->LetExprMgr(*$1,*$5); + delete $1; + delete $5; +} +; %% diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y index a63fdff..74e8ba4 100644 --- a/src/parser/smtlib.y +++ b/src/parser/smtlib.y @@ -63,11 +63,11 @@ #define YYERROR_VERBOSE 1 #define YY_EXIT_FAILURE -1 #define YYPARSE_PARAM AssertsQuery -%} + %} %union { // FIXME: Why is this not an UNSIGNED int? - int uintval; /* for numerals in types. */ + int uintval; /* for numerals in types. */ // for BV32 BVCONST unsigned long long ullval; @@ -156,7 +156,7 @@ %token SEMICOLON_TOK %token EOF_TOK %token EQ_TOK -/*BV SPECIFIC TOKENS*/ + /*BV SPECIFIC TOKENS*/ %token NAND_TOK %token NOR_TOK %token NEQ_TOK @@ -204,147 +204,147 @@ %% cmd: - benchmark +benchmark +{ + ASTNode assumptions; + if($1 == NULL) + { + assumptions = ParserBM->CreateNode(TRUE); + } + else { - ASTNode assumptions; - if($1 == NULL) - { - assumptions = ParserBM->CreateNode(TRUE); - } - else - { - assumptions = *$1; - } + assumptions = *$1; + } - if(query.IsNull()) - { - query = ParserBM->CreateNode(FALSE); - } - - ((ASTVec*)AssertsQuery)->push_back(assumptions); - ((ASTVec*)AssertsQuery)->push_back(query); - delete $1; - YYACCEPT; + if(query.IsNull()) + { + query = ParserBM->CreateNode(FALSE); } + + ((ASTVec*)AssertsQuery)->push_back(assumptions); + ((ASTVec*)AssertsQuery)->push_back(query); + delete $1; + YYACCEPT; +} ; benchmark: - LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK - { - if($4 != NULL){ - if($4->size() > 1) - $$ = new ASTNode(ParserBM->CreateNode(AND,*$4)); - else - $$ = new ASTNode((*$4)[0]); - delete $4; - } - else { - $$ = NULL; - } - } +LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK +{ + if($4 != NULL){ + if($4->size() > 1) + $$ = new ASTNode(ParserBM->CreateNode(AND,*$4)); + else + $$ = new ASTNode((*$4)[0]); + delete $4; + } + else { + $$ = NULL; + } +} /* | EOF_TOK */ /* { */ /* } */ ; bench_name: - FORMID_TOK - { - } +FORMID_TOK +{ +} ; bench_attributes: - bench_attribute - { - $$ = new ASTVec; - if ($1 != NULL) { - $$->push_back(*$1); - ParserBM->AddAssert(*$1); - delete $1; - } - } - | bench_attributes bench_attribute - { - if ($1 != NULL && $2 != NULL) { - $1->push_back(*$2); - ParserBM->AddAssert(*$2); - $$ = $1; - delete $2; - } - } +bench_attribute +{ + $$ = new ASTVec; + if ($1 != NULL) { + $$->push_back(*$1); + ParserBM->AddAssert(*$1); + delete $1; + } +} +| bench_attributes bench_attribute +{ + if ($1 != NULL && $2 != NULL) { + $1->push_back(*$2); + ParserBM->AddAssert(*$2); + $$ = $1; + delete $2; + } +} ; bench_attribute: - COLON_TOK ASSUMPTION_TOK an_formula - { - //assumptions are like asserts - $$ = $3; - } - | COLON_TOK FORMULA_TOK an_formula - { - // Previously this would call AddQuery() on the negation. - // But if multiple formula were (eroneously) present - // it discarded all but the last formula. Allowing multiple - // formula and taking the conjunction of them along with all - // the assumptions is what the other solvers do. +COLON_TOK ASSUMPTION_TOK an_formula +{ + //assumptions are like asserts + $$ = $3; +} +| COLON_TOK FORMULA_TOK an_formula +{ + // Previously this would call AddQuery() on the negation. + // But if multiple formula were (eroneously) present + // it discarded all but the last formula. Allowing multiple + // formula and taking the conjunction of them along with all + // the assumptions is what the other solvers do. - //assumptions are like asserts - $$ = $3; - } - | COLON_TOK STATUS_TOK status - { - $$ = NULL; - } - | COLON_TOK LOGIC_TOK logic_name - { - if (!(0 == strcmp($3->GetName(),"QF_UFBV") || - 0 == strcmp($3->GetName(),"QF_BV") || - //0 == strcmp($3->GetName(),"QF_UF") || - 0 == strcmp($3->GetName(),"QF_AUFBV"))) { - yyerror("Wrong input logic:"); - } - $$ = NULL; - } - | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK var_decls RPAREN_TOK - { - $$ = NULL; - } - | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK var_decls RPAREN_TOK - { - $$ = NULL; - } - | annotation - { - $$ = NULL; - } + //assumptions are like asserts + $$ = $3; +} +| COLON_TOK STATUS_TOK status +{ + $$ = NULL; +} +| COLON_TOK LOGIC_TOK logic_name +{ + if (!(0 == strcmp($3->GetName(),"QF_UFBV") || + 0 == strcmp($3->GetName(),"QF_BV") || + //0 == strcmp($3->GetName(),"QF_UF") || + 0 == strcmp($3->GetName(),"QF_AUFBV"))) { + yyerror("Wrong input logic:"); + } + $$ = NULL; +} +| COLON_TOK EXTRAFUNS_TOK LPAREN_TOK var_decls RPAREN_TOK +{ + $$ = NULL; +} +| COLON_TOK EXTRAPREDS_TOK LPAREN_TOK var_decls RPAREN_TOK +{ + $$ = NULL; +} +| annotation +{ + $$ = NULL; +} ; logic_name: - FORMID_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - $$ = $1; - } - | FORMID_TOK - { - $$ = $1; - } +FORMID_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK +{ + $$ = $1; +} +| FORMID_TOK +{ + $$ = $1; +} ; status: - SAT_TOK { - input_status = TO_BE_SATISFIABLE; - $$ = NULL; - } - | UNSAT_TOK { - input_status = TO_BE_UNSATISFIABLE; - $$ = NULL; - } - | UNKNOWN_TOK - { - input_status = TO_BE_UNKNOWN; - $$ = NULL; +SAT_TOK { + input_status = TO_BE_SATISFIABLE; + $$ = NULL; +} +| UNSAT_TOK { + input_status = TO_BE_UNSATISFIABLE; + $$ = NULL; } - ; +| UNKNOWN_TOK +{ + input_status = TO_BE_UNKNOWN; + $$ = NULL; +} +; /* annotations: */ @@ -357,809 +357,809 @@ status: /* ; */ annotation: - attribute - { - } - | attribute user_value - { - } +attribute +{ +} +| attribute user_value +{ +} ; user_value: - USER_VAL_TOK - { - //cerr << "Printing user_value: " << *$1 << endl; - } +USER_VAL_TOK +{ + //cerr << "Printing user_value: " << *$1 << endl; +} ; attribute: - COLON_TOK SOURCE_TOK - { - } - | COLON_TOK CATEGORY_TOK - { - } - | COLON_TOK DIFFICULTY_TOK +COLON_TOK SOURCE_TOK +{ +} +| COLON_TOK CATEGORY_TOK +{ +} +| COLON_TOK DIFFICULTY_TOK ; sort_symbs: - sort_symb - { - //a single sort symbol here means either a BitVec or a Boolean - $$.indexwidth = $1.indexwidth; - $$.valuewidth = $1.valuewidth; - } - | sort_symb sort_symb - { - //two sort symbols mean f: type --> type - $$.indexwidth = $1.valuewidth; - $$.valuewidth = $2.valuewidth; - } +sort_symb +{ + //a single sort symbol here means either a BitVec or a Boolean + $$.indexwidth = $1.indexwidth; + $$.valuewidth = $1.valuewidth; +} +| sort_symb sort_symb +{ + //two sort symbols mean f: type --> type + $$.indexwidth = $1.valuewidth; + $$.valuewidth = $2.valuewidth; +} ; var_decls: - var_decl - { - } +var_decl +{ +} // | LPAREN_TOK var_decl RPAREN_TOK - | - var_decls var_decl - { - } +| +var_decls var_decl +{ +} ; var_decl: - LPAREN_TOK FORMID_TOK sort_symbs RPAREN_TOK - { - _parser_symbol_table.insert(*$2); - //Sort_symbs has the indexwidth/valuewidth. Set those fields in - //var - $2->SetIndexWidth($3.indexwidth); - $2->SetValueWidth($3.valuewidth); - if(ParserBM->UserFlags.print_STPinput_back_flag) - ParserBM->ListOfDeclaredVars.push_back(*$2); - } - | LPAREN_TOK FORMID_TOK RPAREN_TOK - { - _parser_symbol_table.insert(*$2); - //Sort_symbs has the indexwidth/valuewidth. Set those fields in - //var - $2->SetIndexWidth(0); - $2->SetValueWidth(0); - if(ParserBM->UserFlags.print_STPinput_back_flag) - ParserBM->ListOfDeclaredVars.push_back(*$2); - } +LPAREN_TOK FORMID_TOK sort_symbs RPAREN_TOK +{ + _parser_symbol_table.insert(*$2); + //Sort_symbs has the indexwidth/valuewidth. Set those fields in + //var + $2->SetIndexWidth($3.indexwidth); + $2->SetValueWidth($3.valuewidth); + if(ParserBM->UserFlags.print_STPinput_back_flag) + ParserBM->ListOfDeclaredVars.push_back(*$2); +} +| LPAREN_TOK FORMID_TOK RPAREN_TOK +{ + _parser_symbol_table.insert(*$2); + //Sort_symbs has the indexwidth/valuewidth. Set those fields in + //var + $2->SetIndexWidth(0); + $2->SetValueWidth(0); + if(ParserBM->UserFlags.print_STPinput_back_flag) + ParserBM->ListOfDeclaredVars.push_back(*$2); +} ; an_formulas: - an_formula - { - $$ = new ASTVec; - if ($1 != NULL) { - $$->push_back(*$1); - delete $1; - } - } - | - an_formulas an_formula - { - if ($1 != NULL && $2 != NULL) { - $1->push_back(*$2); - $$ = $1; - delete $2; - } - } +an_formula +{ + $$ = new ASTVec; + if ($1 != NULL) { + $$->push_back(*$1); + delete $1; + } +} +| +an_formulas an_formula +{ + if ($1 != NULL && $2 != NULL) { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +} ; an_formula: - TRUE_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(TRUE)); - $$->SetIndexWidth(0); - $$->SetValueWidth(0); - } - | FALSE_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(FALSE)); - $$->SetIndexWidth(0); - $$->SetValueWidth(0); - } - | fvar - { - $$ = $1; - } - | LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK +TRUE_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(TRUE)); + $$->SetIndexWidth(0); + $$->SetValueWidth(0); +} +| FALSE_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(FALSE)); + $$->SetIndexWidth(0); + $$->SetValueWidth(0); +} +| fvar +{ + $$ = $1; +} +| LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK //| LPAREN_TOK EQ_TOK an_term an_term annotations RPAREN_TOK - { - ASTNode * n = new ASTNode((GlobalSTP->simp)->CreateSimplifiedEQ(*$3, *$4)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK - { - using namespace BEEV; +{ + ASTNode * n = new ASTNode((GlobalSTP->simp)->CreateSimplifiedEQ(*$3, *$4)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK +{ + using namespace BEEV; - ASTVec terms = *$3; - ASTVec forms; + ASTVec terms = *$3; + ASTVec forms; - for(ASTVec::const_iterator it=terms.begin(),itend=terms.end(); - it!=itend; it++) { - for(ASTVec::const_iterator it2=it+1; it2!=itend; it2++) { - ASTNode * n = new ASTNode(ParserBM->CreateNode(NOT, ParserBM->CreateNode(EQ, *it, *it2))); + for(ASTVec::const_iterator it=terms.begin(),itend=terms.end(); + it!=itend; it++) { + for(ASTVec::const_iterator it2=it+1; it2!=itend; it2++) { + ASTNode * n = new ASTNode(ParserBM->CreateNode(NOT, ParserBM->CreateNode(EQ, *it, *it2))); - BVTypeCheck(*n); + BVTypeCheck(*n); - forms.push_back(*n); - } - } + forms.push_back(*n); + } + } - if(forms.size() == 0) - FatalError("empty distinct"); + if(forms.size() == 0) + FatalError("empty distinct"); - $$ = (forms.size() == 1) ? - new ASTNode(forms[0]) : - new ASTNode(ParserBM->CreateNode(AND, forms)); + $$ = (forms.size() == 1) ? + new ASTNode(forms[0]) : + new ASTNode(ParserBM->CreateNode(AND, forms)); - delete $3; - } + delete $3; +} - | LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK +| LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK //| LPAREN_TOK BVSLT_TOK an_term an_term annotations RPAREN_TOK - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSLT, *$3, *$4)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVSLE_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSLT, *$3, *$4)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVSLE_TOK an_term an_term RPAREN_TOK //| LPAREN_TOK BVSLE_TOK an_term an_term annotations RPAREN_TOK - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSLE, *$3, *$4)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVSGT_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSLE, *$3, *$4)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVSGT_TOK an_term an_term RPAREN_TOK //| LPAREN_TOK BVSGT_TOK an_term an_term annotations RPAREN_TOK - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSGT, *$3, *$4)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVSGE_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSGT, *$3, *$4)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVSGE_TOK an_term an_term RPAREN_TOK //| LPAREN_TOK BVSGE_TOK an_term an_term annotations RPAREN_TOK - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSGE, *$3, *$4)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVLT_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVSGE, *$3, *$4)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVLT_TOK an_term an_term RPAREN_TOK //| LPAREN_TOK BVLT_TOK an_term an_term annotations RPAREN_TOK - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVLT, *$3, *$4)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVLE_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVLT, *$3, *$4)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVLE_TOK an_term an_term RPAREN_TOK //| LPAREN_TOK BVLE_TOK an_term an_term annotations RPAREN_TOK - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVLE, *$3, *$4)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVGT_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVLE, *$3, *$4)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVGT_TOK an_term an_term RPAREN_TOK //| LPAREN_TOK BVGT_TOK an_term an_term annotations RPAREN_TOK - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVGT, *$3, *$4)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK BVGE_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVGT, *$3, *$4)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVGE_TOK an_term an_term RPAREN_TOK //| LPAREN_TOK BVGE_TOK an_term an_term annotations RPAREN_TOK - { - ASTNode * n = new ASTNode(ParserBM->CreateNode(BVGE, *$3, *$4)); - BVTypeCheck(*n); - $$ = n; - delete $3; - delete $4; - } - | LPAREN_TOK an_formula RPAREN_TOK - { - $$ = $2; - } - | LPAREN_TOK NOT_TOK an_formula RPAREN_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(NOT, *$3)); - delete $3; - } - | LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(IMPLIES, *$3, *$4)); - delete $3; - delete $4; - } - | LPAREN_TOK ITE_TOK an_formula an_formula an_formula RPAREN_TOK - { - $$ = new ASTNode((GlobalSTP->simp)->CreateSimplifiedFormulaITE(*$3, *$4, *$5)); - delete $3; - delete $4; - delete $5; - } - | LPAREN_TOK AND_TOK an_formulas RPAREN_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(AND, *$3)); - delete $3; - } - | LPAREN_TOK OR_TOK an_formulas RPAREN_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(OR, *$3)); - delete $3; - } - | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(XOR, *$3, *$4)); - delete $3; - delete $4; - } - | LPAREN_TOK IFF_TOK an_formula an_formula RPAREN_TOK - { - $$ = new ASTNode(ParserBM->CreateNode(IFF, *$3, *$4)); - delete $3; - delete $4; - } - | letexpr_mgmt an_formula RPAREN_TOK +{ + ASTNode * n = new ASTNode(ParserBM->CreateNode(BVGE, *$3, *$4)); + BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK an_formula RPAREN_TOK +{ + $$ = $2; +} +| LPAREN_TOK NOT_TOK an_formula RPAREN_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(NOT, *$3)); + delete $3; +} +| LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(IMPLIES, *$3, *$4)); + delete $3; + delete $4; +} +| LPAREN_TOK ITE_TOK an_formula an_formula an_formula RPAREN_TOK +{ + $$ = new ASTNode((GlobalSTP->simp)->CreateSimplifiedFormulaITE(*$3, *$4, *$5)); + delete $3; + delete $4; + delete $5; +} +| LPAREN_TOK AND_TOK an_formulas RPAREN_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(AND, *$3)); + delete $3; +} +| LPAREN_TOK OR_TOK an_formulas RPAREN_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(OR, *$3)); + delete $3; +} +| LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(XOR, *$3, *$4)); + delete $3; + delete $4; +} +| LPAREN_TOK IFF_TOK an_formula an_formula RPAREN_TOK +{ + $$ = new ASTNode(ParserBM->CreateNode(IFF, *$3, *$4)); + delete $3; + delete $4; +} +| letexpr_mgmt an_formula RPAREN_TOK //| letexpr_mgmt an_formula annotations RPAREN_TOK - { - $$ = $2; - //Cleanup the LetIDToExprMap - ParserBM->GetLetMgr()->CleanupLetIDMap(); - } +{ + $$ = $2; + //Cleanup the LetIDToExprMap + ParserBM->GetLetMgr()->CleanupLetIDMap(); +} ; letexpr_mgmt: - LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK - { - //Expr must typecheck - BVTypeCheck(*$6); +LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK +{ + //Expr must typecheck + BVTypeCheck(*$6); - //set the valuewidth of the identifier - $5->SetValueWidth($6->GetValueWidth()); - $5->SetIndexWidth($6->GetIndexWidth()); + //set the valuewidth of the identifier + $5->SetValueWidth($6->GetValueWidth()); + $5->SetIndexWidth($6->GetIndexWidth()); - //populate the hashtable from LET-var --> - //LET-exprs and then process them: - // - //1. ensure that LET variables do not clash - //1. with declared variables. - // - //2. Ensure that LET variables are not - //2. defined more than once - ParserBM->GetLetMgr()->LetExprMgr(*$5,*$6); - delete $5; - delete $6; - } - | LPAREN_TOK FLET_TOK LPAREN_TOK DOLLAR_TOK FORMID_TOK an_formula RPAREN_TOK - { - //Expr must typecheck - BVTypeCheck(*$6); + //populate the hashtable from LET-var --> + //LET-exprs and then process them: + // + //1. ensure that LET variables do not clash + //1. with declared variables. + // + //2. Ensure that LET variables are not + //2. defined more than once + ParserBM->GetLetMgr()->LetExprMgr(*$5,*$6); + delete $5; + delete $6; +} +| LPAREN_TOK FLET_TOK LPAREN_TOK DOLLAR_TOK FORMID_TOK an_formula RPAREN_TOK +{ + //Expr must typecheck + BVTypeCheck(*$6); - //set the valuewidth of the identifier - $5->SetValueWidth($6->GetValueWidth()); - $5->SetIndexWidth($6->GetIndexWidth()); + //set the valuewidth of the identifier + $5->SetValueWidth($6->GetValueWidth()); + $5->SetIndexWidth($6->GetIndexWidth()); - //Do LET-expr management - ParserBM->GetLetMgr()->LetExprMgr(*$5,*$6); - delete $5; - delete $6; - } + //Do LET-expr management + ParserBM->GetLetMgr()->LetExprMgr(*$5,*$6); + delete $5; + delete $6; +} an_terms: - an_term - { - $$ = new ASTVec; - if ($1 != NULL) { - $$->push_back(*$1); - delete $1; - } - } - | - an_terms an_term - { - if ($1 != NULL && $2 != NULL) { - $1->push_back(*$2); - $$ = $1; - delete $2; - } - } +an_term +{ + $$ = new ASTVec; + if ($1 != NULL) { + $$->push_back(*$1); + delete $1; + } +} +| +an_terms an_term +{ + if ($1 != NULL && $2 != NULL) { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +} ; an_term: - BVCONST_TOK - { - $$ = new ASTNode(ParserBM->CreateBVConst($1, 10, 32)); - } - | BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - $$ = new ASTNode(ParserBM->CreateBVConst($1,10,$3)); - delete $1; - } - | an_nonbvconst_term - ; +BVCONST_TOK +{ + $$ = new ASTNode(ParserBM->CreateBVConst($1, 10, 32)); +} +| BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK +{ + $$ = new ASTNode(ParserBM->CreateBVConst($1,10,$3)); + delete $1; +} +| an_nonbvconst_term +; an_nonbvconst_term: - BITCONST_TOK { $$ = $1; } - | var - { - $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); - delete $1; - } - | LPAREN_TOK an_term RPAREN_TOK +BITCONST_TOK { $$ = $1; } +| var +{ + $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); + delete $1; +} +| LPAREN_TOK an_term RPAREN_TOK //| LPAREN_TOK an_term annotations RPAREN_TOK - { - $$ = $2; - //$$ = new ASTNode(ParserBM->SimplifyTerm(*$2)); - //delete $2; - } - | SELECT_TOK an_term an_term - { - //ARRAY READ - // valuewidth is same as array, indexwidth is 0. - ASTNode array = *$2; - ASTNode index = *$3; - unsigned int width = array.GetValueWidth(); - ASTNode * n = - new ASTNode(ParserBM->CreateTerm(READ, width, array, index)); - BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | STORE_TOK an_term an_term an_term - { - //ARRAY WRITE - unsigned int width = $4->GetValueWidth(); - ASTNode array = *$2; - ASTNode index = *$3; - ASTNode writeval = *$4; - ASTNode write_term = ParserBM->CreateTerm(WRITE,width,array,index,writeval); - write_term.SetIndexWidth($2->GetIndexWidth()); - BVTypeCheck(write_term); - ASTNode * n = new ASTNode(write_term); - $$ = n; - delete $2; - delete $3; - delete $4; - } - | BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term - { - int width = $3 - $5 + 1; - if (width < 0) - yyerror("Negative width in extract"); +{ + $$ = $2; + //$$ = new ASTNode(ParserBM->SimplifyTerm(*$2)); + //delete $2; +} +| SELECT_TOK an_term an_term +{ + //ARRAY READ + // valuewidth is same as array, indexwidth is 0. + ASTNode array = *$2; + ASTNode index = *$3; + unsigned int width = array.GetValueWidth(); + ASTNode * n = + new ASTNode(ParserBM->CreateTerm(READ, width, array, index)); + BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; +} +| STORE_TOK an_term an_term an_term +{ + //ARRAY WRITE + unsigned int width = $4->GetValueWidth(); + ASTNode array = *$2; + ASTNode index = *$3; + ASTNode writeval = *$4; + ASTNode write_term = ParserBM->CreateTerm(WRITE,width,array,index,writeval); + write_term.SetIndexWidth($2->GetIndexWidth()); + BVTypeCheck(write_term); + ASTNode * n = new ASTNode(write_term); + $$ = n; + delete $2; + delete $3; + delete $4; +} +| BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term +{ + int width = $3 - $5 + 1; + if (width < 0) + yyerror("Negative width in extract"); - if((unsigned)$3 >= $7->GetValueWidth()) - yyerror("Parsing: Wrong width in BVEXTRACT\n"); + if((unsigned)$3 >= $7->GetValueWidth()) + yyerror("Parsing: Wrong width in BVEXTRACT\n"); - ASTNode hi = ParserBM->CreateBVConst(32, $3); - ASTNode low = ParserBM->CreateBVConst(32, $5); - ASTNode output = ParserBM->CreateTerm(BVEXTRACT, width, *$7,hi,low); - ASTNode * n = new ASTNode(output); - BVTypeCheck(*n); - $$ = n; - delete $7; - } - | ITE_TOK an_formula an_term an_term - { - unsigned int width = $3->GetValueWidth(); - if (width != $4->GetValueWidth()) { - cerr << *$3; - cerr << *$4; - yyerror("Width mismatch in IF-THEN-ELSE"); - } - if($3->GetIndexWidth() != $4->GetIndexWidth()) - yyerror("Width mismatch in IF-THEN-ELSE"); + ASTNode hi = ParserBM->CreateBVConst(32, $3); + ASTNode low = ParserBM->CreateBVConst(32, $5); + ASTNode output = ParserBM->CreateTerm(BVEXTRACT, width, *$7,hi,low); + ASTNode * n = new ASTNode(output); + BVTypeCheck(*n); + $$ = n; + delete $7; +} +| ITE_TOK an_formula an_term an_term +{ + unsigned int width = $3->GetValueWidth(); + if (width != $4->GetValueWidth()) { + cerr << *$3; + cerr << *$4; + yyerror("Width mismatch in IF-THEN-ELSE"); + } + if($3->GetIndexWidth() != $4->GetIndexWidth()) + yyerror("Width mismatch in IF-THEN-ELSE"); - BVTypeCheck(*$2); - BVTypeCheck(*$3); - BVTypeCheck(*$4); - $$ = new ASTNode((GlobalSTP->simp)->CreateSimplifiedTermITE(*$2, *$3, *$4)); - //$$ = new ASTNode(ParserBM->CreateTerm(ITE,width,*$2, *$3, *$4)); - $$->SetIndexWidth($4->GetIndexWidth()); - BVTypeCheck(*$$); - delete $2; - delete $3; - delete $4; - } - | BVCONCAT_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth() + $3->GetValueWidth(); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVCONCAT, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; + BVTypeCheck(*$2); + BVTypeCheck(*$3); + BVTypeCheck(*$4); + $$ = new ASTNode((GlobalSTP->simp)->CreateSimplifiedTermITE(*$2, *$3, *$4)); + //$$ = new ASTNode(ParserBM->CreateTerm(ITE,width,*$2, *$3, *$4)); + $$->SetIndexWidth($4->GetIndexWidth()); + BVTypeCheck(*$$); + delete $2; + delete $3; + delete $4; +} +| BVCONCAT_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth() + $3->GetValueWidth(); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVCONCAT, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; - delete $2; - delete $3; - } - | BVNOT_TOK an_term - { - //this is the BVNEG (term) in the CVCL language - unsigned int width = $2->GetValueWidth(); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNEG, width, *$2)); - BVTypeCheck(*n); - $$ = n; - delete $2; - } - | BVNEG_TOK an_term - { - //this is the BVUMINUS term in CVCL langauge - unsigned width = $2->GetValueWidth(); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVUMINUS,width,*$2)); - BVTypeCheck(*n); - $$ = n; - delete $2; - } - | BVAND_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in AND"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVAND, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVOR_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in OR"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVOR, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVXOR_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in XOR"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVXOR, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVSUB_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVSUB"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVSUB, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVPLUS_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVPLUS"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVPLUS, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; + delete $2; + delete $3; +} +| BVNOT_TOK an_term +{ + //this is the BVNEG (term) in the CVCL language + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNEG, width, *$2)); + BVTypeCheck(*n); + $$ = n; + delete $2; +} +| BVNEG_TOK an_term +{ + //this is the BVUMINUS term in CVCL langauge + unsigned width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVUMINUS,width,*$2)); + BVTypeCheck(*n); + $$ = n; + delete $2; +} +| BVAND_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in AND"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVAND, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; +} +| BVOR_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in OR"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVOR, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; +} +| BVXOR_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in XOR"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVXOR, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; +} +| BVSUB_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVSUB"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVSUB, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; +} +| BVPLUS_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVPLUS"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVPLUS, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; - } - | BVMULT_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVMULT"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVMULT, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } +} +| BVMULT_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVMULT"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVMULT, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; +} | BVDIV_TOK an_term an_term { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVDIV"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVDIV, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVDIV"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVDIV, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; - delete $2; - delete $3; + delete $2; + delete $3; } | BVMOD_TOK an_term an_term { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVMOD"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVMOD, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVMOD"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVMOD, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; - delete $2; - delete $3; + delete $2; + delete $3; } | SBVDIV_TOK an_term an_term { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in SBVDIV"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVDIV, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in SBVDIV"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVDIV, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; - delete $2; - delete $3; + delete $2; + delete $3; } | SBVREM_TOK an_term an_term { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in SBVREM"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVREM, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in SBVREM"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVREM, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; } | SBVMOD_TOK an_term an_term { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in SBVMOD"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVMOD, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in SBVMOD"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(SBVMOD, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; } - | BVNAND_TOK an_term an_term - { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVNAND"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNAND, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; - } - | BVNOR_TOK an_term an_term +| BVNAND_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVNAND"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNAND, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; +} +| BVNOR_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVNOR"); + } + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNOR, width, *$2, *$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; +} +| BVLEFTSHIFT_1_TOK an_term an_term +{ + // shifting left by who know how much? + unsigned int w = $2->GetValueWidth(); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVLEFTSHIFT,w,*$2,*$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; +} +| BVRIGHTSHIFT_1_TOK an_term an_term +{ + // shifting right by who know how much? + unsigned int w = $2->GetValueWidth(); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVRIGHTSHIFT,w,*$2,*$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; +} +| BVARITHRIGHTSHIFT_TOK an_term an_term +{ + // shifting arithmetic right by who know how much? + unsigned int w = $2->GetValueWidth(); + ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVSRSHIFT,w,*$2,*$3)); + BVTypeCheck(*n); + $$ = n; + delete $2; +} +| BVROTATE_LEFT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term +{ + BVTypeCheck(*$5); + + ASTNode *n; + unsigned width = $5->GetValueWidth(); + unsigned rotate = $3; + if (0 == rotate) { - unsigned int width = $2->GetValueWidth(); - if (width != $3->GetValueWidth()) { - yyerror("Width mismatch in BVNOR"); - } - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVNOR, width, *$2, *$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; - delete $3; + n = $5; } - | BVLEFTSHIFT_1_TOK an_term an_term -{ - // shifting left by who know how much? - unsigned int w = $2->GetValueWidth(); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVLEFTSHIFT,w,*$2,*$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; - } - | BVRIGHTSHIFT_1_TOK an_term an_term + else if (rotate < width) { - // shifting right by who know how much? - unsigned int w = $2->GetValueWidth(); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVRIGHTSHIFT,w,*$2,*$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; + ASTNode high = ParserBM->CreateBVConst(32,width-1); + ASTNode zero = ParserBM->CreateBVConst(32,0); + ASTNode cut = ParserBM->CreateBVConst(32,width-rotate); + ASTNode cutMinusOne = ParserBM->CreateBVConst(32,width-rotate-1); + + ASTNode top = ParserBM->CreateTerm(BVEXTRACT,rotate,*$5,high, cut); + ASTNode bottom = ParserBM->CreateTerm(BVEXTRACT,width-rotate,*$5,cutMinusOne,zero); + n = new ASTNode(ParserBM->CreateTerm(BVCONCAT,width,bottom,top)); + delete $5; } - | BVARITHRIGHTSHIFT_TOK an_term an_term + else { - // shifting arithmetic right by who know how much? - unsigned int w = $2->GetValueWidth(); - ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVSRSHIFT,w,*$2,*$3)); - BVTypeCheck(*n); - $$ = n; - delete $2; + n = NULL; // remove gcc warning. + yyerror("Rotate must be strictly less than the width."); } - | BVROTATE_LEFT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term - { - BVTypeCheck(*$5); - ASTNode *n; - unsigned width = $5->GetValueWidth(); - unsigned rotate = $3; - if (0 == rotate) - { - n = $5; - } - else if (rotate < width) - { - ASTNode high = ParserBM->CreateBVConst(32,width-1); - ASTNode zero = ParserBM->CreateBVConst(32,0); - ASTNode cut = ParserBM->CreateBVConst(32,width-rotate); - ASTNode cutMinusOne = ParserBM->CreateBVConst(32,width-rotate-1); - - ASTNode top = ParserBM->CreateTerm(BVEXTRACT,rotate,*$5,high, cut); - ASTNode bottom = ParserBM->CreateTerm(BVEXTRACT,width-rotate,*$5,cutMinusOne,zero); - n = new ASTNode(ParserBM->CreateTerm(BVCONCAT,width,bottom,top)); - delete $5; - } - else - { - n = NULL; // remove gcc warning. - yyerror("Rotate must be strictly less than the width."); - } + BVTypeCheck(*n); + $$ = n; - BVTypeCheck(*n); - $$ = n; +} +| BVROTATE_RIGHT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term +{ + BVTypeCheck(*$5); + ASTNode *n; + unsigned width = $5->GetValueWidth(); + unsigned rotate = $3; + if (0 == rotate) + { + n = $5; } - | BVROTATE_RIGHT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term + else if (rotate < width) { - BVTypeCheck(*$5); - - ASTNode *n; - unsigned width = $5->GetValueWidth(); - unsigned rotate = $3; - if (0 == rotate) - { - n = $5; - } - else if (rotate < width) - { - ASTNode high = ParserBM->CreateBVConst(32,width-1); - ASTNode zero = ParserBM->CreateBVConst(32,0); - ASTNode cut = ParserBM->CreateBVConst(32,rotate); - ASTNode cutMinusOne = ParserBM->CreateBVConst(32,rotate-1); + ASTNode high = ParserBM->CreateBVConst(32,width-1); + ASTNode zero = ParserBM->CreateBVConst(32,0); + ASTNode cut = ParserBM->CreateBVConst(32,rotate); + ASTNode cutMinusOne = ParserBM->CreateBVConst(32,rotate-1); - ASTNode bottom = ParserBM->CreateTerm(BVEXTRACT,rotate,*$5,cutMinusOne, zero); - ASTNode top = ParserBM->CreateTerm(BVEXTRACT,width-rotate,*$5,high,cut); - n = new ASTNode(ParserBM->CreateTerm(BVCONCAT,width,bottom,top)); - delete $5; - } - else - { - n = NULL; // remove gcc warning. - yyerror("Rotate must be strictly less than the width."); - } - - BVTypeCheck(*n); - $$ = n; - + ASTNode bottom = ParserBM->CreateTerm(BVEXTRACT,rotate,*$5,cutMinusOne, zero); + ASTNode top = ParserBM->CreateTerm(BVEXTRACT,width-rotate,*$5,high,cut); + n = new ASTNode(ParserBM->CreateTerm(BVCONCAT,width,bottom,top)); + delete $5; } - | BVSX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term + else { - BVTypeCheck(*$5); - unsigned w = $5->GetValueWidth() + $3; - ASTNode width = ParserBM->CreateBVConst(32,w); - ASTNode *n = new ASTNode(ParserBM->CreateTerm(BVSX,w,*$5,width)); - BVTypeCheck(*n); - $$ = n; - delete $5; + n = NULL; // remove gcc warning. + yyerror("Rotate must be strictly less than the width."); } + + BVTypeCheck(*n); + $$ = n; + +} +| BVSX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term +{ + BVTypeCheck(*$5); + unsigned w = $5->GetValueWidth() + $3; + ASTNode width = ParserBM->CreateBVConst(32,w); + ASTNode *n = new ASTNode(ParserBM->CreateTerm(BVSX,w,*$5,width)); + BVTypeCheck(*n); + $$ = n; + delete $5; +} | BVZX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term +{ + BVTypeCheck(*$5); + if (0 != $3) { - BVTypeCheck(*$5); - if (0 != $3) - { unsigned w = $5->GetValueWidth() + $3; - ASTNode leading_zeroes = ParserBM->CreateZeroConst($3); + ASTNode leading_zeroes = ParserBM->CreateZeroConst($3); ASTNode *n = new ASTNode(ParserBM->CreateTerm(BVCONCAT,w,leading_zeroes,*$5)); BVTypeCheck(*n); $$ = n; delete $5; } - else - $$ = $5; + else + $$ = $5; - } +} ; sort_symb: - BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - // Just return BV width. If sort is BOOL, width is 0. - // Otherwise, BITVEC[w] returns w. - // - //((indexwidth is 0) && (valuewidth>0)) iff type is BV - $$.indexwidth = 0; - unsigned int length = $3; - if(length > 0) { - $$.valuewidth = length; - } - else { - FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); - } - } - | ARRAY_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK - { - unsigned int index_len = $3; - unsigned int value_len = $5; - if(index_len > 0) { - $$.indexwidth = $3; - } - else { - FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); - } +BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK +{ + // Just return BV width. If sort is BOOL, width is 0. + // Otherwise, BITVEC[w] returns w. + // + //((indexwidth is 0) && (valuewidth>0)) iff type is BV + $$.indexwidth = 0; + unsigned int length = $3; + if(length > 0) { + $$.valuewidth = length; + } + else { + FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + } +} +| ARRAY_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK +{ + unsigned int index_len = $3; + unsigned int value_len = $5; + if(index_len > 0) { + $$.indexwidth = $3; + } + else { + FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + } - if(value_len > 0) { - $$.valuewidth = $5; - } - else { - FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); - } - } + if(value_len > 0) { + $$.valuewidth = $5; + } + else { + FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + } +} ; var: - FORMID_TOK - { - $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); - delete $1; - } - | TERMID_TOK - { - $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); - delete $1; - } - | QUESTION_TOK TERMID_TOK - { - $$ = $2; - } +FORMID_TOK +{ + $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); + delete $1; +} +| TERMID_TOK +{ + $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); + delete $1; +} +| QUESTION_TOK TERMID_TOK +{ + $$ = $2; +} ; fvar: - DOLLAR_TOK FORMID_TOK - { - $$ = $2; - } - | FORMID_TOK - { - $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); - delete $1; - } +DOLLAR_TOK FORMID_TOK +{ + $$ = $2; +} +| FORMID_TOK +{ + $$ = new ASTNode(ParserBM->GetLetMgr()->ResolveID(*$1)); + delete $1; +} ; %% diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index e9bde34..cf2dd40 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -747,7 +747,7 @@ namespace BEEV }//end of inner for loop } //end of outer for loop - //get the exponent + //get the exponent power_of_2 = power_of_2_lowest; //if control is here, we are gauranteed that we have chosen a diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp index bd09bce..d809785 100644 --- a/src/simplifier/consteval.cpp +++ b/src/simplifier/consteval.cpp @@ -248,8 +248,8 @@ namespace BEEV // SBVREM : Result of rounding the quotient towards // zero. i.e. (-10)/3, has a remainder of -1 - // - // SBVMOD : Result of rounding the quotient towards + // + // SBVMOD : Result of rounding the quotient towards // -infinity. i.e. (-10)/3, has a modulus of 2. EXCEPT THAT // if it divides exactly and the signs are different, then // it's equal to the dividend. @@ -260,7 +260,7 @@ namespace BEEV CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true); if (_bm->UserFlags.division_by_zero_returns_one_flag - && CONSTANTBV::BitVector_is_empty(tmp1)) + && CONSTANTBV::BitVector_is_empty(tmp1)) { // Expecting a division by zero. Just return one. OutputNode = _bm->CreateOneConst(outputwidth); @@ -268,7 +268,7 @@ namespace BEEV else { CONSTANTBV::ErrCode e = - CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder); + CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder); if (e != 0) { @@ -317,7 +317,7 @@ namespace BEEV tmp1 = CONSTANTBV::BitVector_Clone(tmp1); if (_bm->UserFlags.division_by_zero_returns_one_flag - && CONSTANTBV::BitVector_is_empty(tmp1)) + && CONSTANTBV::BitVector_is_empty(tmp1)) { // Expecting a division by zero. Just return one. OutputNode = _bm->CreateOneConst(outputwidth); @@ -416,7 +416,7 @@ namespace BEEV CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true); if (_bm->UserFlags.division_by_zero_returns_one_flag - && CONSTANTBV::BitVector_is_empty(tmp1)) + && CONSTANTBV::BitVector_is_empty(tmp1)) { // Expecting a division by zero. Just return one. OutputNode = _bm->CreateOneConst(outputwidth); diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 249eb47..e3304ab 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -801,7 +801,7 @@ namespace BEEV ASTNode Simplifier:: CreateSimplifiedFormulaITE(const ASTNode& in0, - const ASTNode& in1, const ASTNode& in2) + const ASTNode& in1, const ASTNode& in2) { ASTNode t0 = in0; ASTNode t1 = in1; @@ -2311,9 +2311,9 @@ namespace BEEV vars_to_consts[aaa].push_back(one); } //end of for loop - //go over the map from variables to vector of values. combine the - //vector of values, multiply to the variable, and put the - //resultant monomial in the output BVPLUS. + //go over the map from variables to vector of values. combine the + //vector of values, multiply to the variable, and put the + //resultant monomial in the output BVPLUS. for (ASTNodeToVecMap::iterator it = vars_to_consts.begin(), itend = vars_to_consts.end(); it != itend; it++) { ASTVec ccc = it->second; @@ -2811,7 +2811,7 @@ namespace BEEV output = newVar; } //end of start_abstracting if condition - //memoize + //memoize UpdateSimplifyMap(input, output, false); return output; } //end of RemoveWrites() diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp index 60bb670..4df074a 100644 --- a/src/to-sat/CallSAT.cpp +++ b/src/to-sat/CallSAT.cpp @@ -56,13 +56,13 @@ namespace BEEV (input_status == TO_BE_SATISFIABLE)) { cerr << "Warning. Expected satisfiable,"\ - " FOUND unsatisfiable" << endl; + " FOUND unsatisfiable" << endl; } else if (!true_iff_valid && (input_status == TO_BE_UNSATISFIABLE)) { cerr << "Warning. Expected unsatisfiable,"\ - " FOUND satisfiable" << endl; + " FOUND satisfiable" << endl; } } } diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp index dbcfb72..3eb9dbf 100644 --- a/src/to-sat/SimpBool.cpp +++ b/src/to-sat/SimpBool.cpp @@ -89,7 +89,7 @@ namespace BEEV } ASTNode STPMgr::CreateSimpForm(Kind kind, - const ASTNode& child0, const ASTNode& child1) + const ASTNode& child0, const ASTNode& child1) { ASTVec children; //child_stack.clear(); // could just reset top pointer. @@ -102,8 +102,8 @@ namespace BEEV } ASTNode STPMgr::CreateSimpForm(Kind kind, - const ASTNode& child0, - const ASTNode& child1, const ASTNode& child2) + const ASTNode& child0, + const ASTNode& child1, const ASTNode& child2) { ASTVec children; //child_stack.clear(); // could just reset top pointer. @@ -185,7 +185,7 @@ namespace BEEV fflag = 1; // For selective debug printing (below). // append grandchildren to children flat_children.insert(flat_children.end(), - gchildren.begin(), gchildren.end()); + gchildren.begin(), gchildren.end()); } else { @@ -209,7 +209,7 @@ namespace BEEV } ASTNode STPMgr::CreateSimpAndOr(bool IsAnd, - const ASTNode& form1, const ASTNode& form2) + const ASTNode& form1, const ASTNode& form2) { ASTVec children; children.push_back(form1); @@ -254,7 +254,7 @@ namespace BEEV ASTVec::const_iterator it_end = flat_children.end(); ASTVec::const_iterator next_it; for (ASTVec::const_iterator it = flat_children.begin(); - it != it_end; it = next_it) + it != it_end; it = next_it) { next_it = it + 1; bool nextexists = (next_it < it_end); @@ -278,7 +278,7 @@ namespace BEEV // cout << "Dropping [" << it->GetNodeNum() << "]" << endl; } else if (nextexists && (next_it->GetKind() == NOT) - && ((*next_it)[0] == *it)) + && ((*next_it)[0] == *it)) { // form and negation -- return FALSE for AND, TRUE for OR. retval = annihilator; @@ -379,7 +379,7 @@ namespace BEEV *next_it = ASTFalse; } else if (nextexists && (next_it->GetKind() == NOT) - && ((*next_it)[0] == *it)) + && ((*next_it)[0] == *it)) { // x XOR NOT x = TRUE. Skip current, write "true" into next_it // so that it gets tossed, too. @@ -447,8 +447,8 @@ namespace BEEV // FIXME: How do I know whether ITE is a formula or not? ASTNode STPMgr::CreateSimpFormITE(const ASTNode& child0, - const ASTNode& child1, - const ASTNode& child2) + const ASTNode& child1, + const ASTNode& child2) { ASTNode retval; @@ -456,8 +456,8 @@ namespace BEEV if (_trace_simpbool) { cout << "========" << endl - << "CreateSimpFormITE " - << child0 << child1 << child2 << endl; + << "CreateSimpFormITE " + << child0 << child1 << child2 << endl; } if (ASTTrue == child0) diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index afcf25f..a26775f 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -243,9 +243,9 @@ namespace BEEV return result; } //End of onChildDoNeg() - //######################################## - //######################################## - //utilities for control bits. + //######################################## + //######################################## + //utilities for control bits. void CNFMgr::initializeCNFInfo(CNFInfo& x) { @@ -448,9 +448,9 @@ namespace BEEV return psi; } //End of Product - //######################################## - //######################################## - //prep. for cnf conversion + //######################################## + //######################################## + //prep. for cnf conversion void CNFMgr::scanFormula(const ASTNode& varphi, bool isPos) { @@ -689,9 +689,9 @@ namespace BEEV } } //End of convertTermForCNF() - //######################################## - //######################################## - // functions for renaming nodes during cnf conversion + //######################################## + //######################################## + // functions for renaming nodes during cnf conversion ASTNode* CNFMgr::doRenameITE(const ASTNode& varphi, ClauseList* defs) { @@ -803,9 +803,9 @@ namespace BEEV setWasRenamedNeg(*x); } //End of doRenamingNeg() - //######################################## - //######################################## - //main switch for individual cnf conversion cases + //######################################## + //######################################## + //main switch for individual cnf conversion cases void CNFMgr::convertFormulaToCNFPosCases(const ASTNode& varphi, ClauseList* defs) { @@ -966,9 +966,9 @@ namespace BEEV } } //convertFormulaToCNFNegCases() - //######################################## - //######################################## - // individual cnf conversion cases + //######################################## + //######################################## + // individual cnf conversion cases void CNFMgr::convertFormulaToCNFPosPred(const ASTNode& varphi, ClauseList* defs) { @@ -1564,9 +1564,9 @@ namespace BEEV return psi; } //End of convertFormulaToCNFNegXORAux() - //######################################## - //######################################## - // utilities for reclaiming memory. + //######################################## + //######################################## + // utilities for reclaiming memory. void CNFMgr::reduceMemoryFootprintPos(const ASTNode& varphi) { @@ -1598,8 +1598,8 @@ namespace BEEV } } //End of reduceMemoryFootprintNeg() - //######################################## - //######################################## + //######################################## + //######################################## ASTNode* CNFMgr::ASTNodeToASTNodePtr(const ASTNode& varphi) { @@ -1618,8 +1618,8 @@ namespace BEEV return psi; } //End of ASTNodeToASTNodePtr() - //######################################## - //######################################## + //######################################## + //######################################## void CNFMgr::cleanup(const ASTNode& varphi) { @@ -1650,9 +1650,9 @@ namespace BEEV info.clear(); } //End of cleanup() - //######################################## - //######################################## - // constructor + //######################################## + //######################################## + // constructor CNFMgr::CNFMgr(STPMgr *bmgr) {