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");
// 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();
CounterExampleMap.clear();
ConstructCounterExample(SatSolver);
if (bm->UserFlags.stats_flag
- && bm->UserFlags.print_nodes_flag)
+ && bm->UserFlags.print_nodes_flag)
{
PrintSATModel(SatSolver);
}
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;
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 +=
"-x : flatten nested XORs\n";
helpstring +=
"-y : print counterexample in binary\n";
-
+
switch(c) {
case 'a' :
b->UserFlags.optimize_flag = false;
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;
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 =
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
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);
}
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);
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;
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);
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
ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);
CompleteCEStar c =
- new BEEV::CompleteCounterExample(ce->GetCompleteCounterExample(), b);
+ new BEEV::CompleteCounterExample(ce->GetCompleteCounterExample(),
+ b);
return c;
}
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
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);
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));
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);
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);
//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);
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;
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;
}
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;
}
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;
}
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);
}
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);
}
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 */
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,
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++;
}
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;
}
Type vc_getType(VC vc, Expr ex) {
nodestar e = (nodestar)ex;
-
+
switch(e->GetType()) {
case BEEV::BOOLEAN_TYPE:
return vc_boolType(vc);
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;
}
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();
}
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);
}
int getExprID (Expr ex) {
- BEEV::ASTNode q = (*(nodestar)ex);
-
+ BEEV::ASTNode q = (*(nodestar)ex);
return q.GetNodeNum();
}
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;
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
%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"
%token IN_TOK "IN"
%token LET_TOK "LET"
-//%token COUNTEREXAMPLE_TOK "COUNTEREXAMPLE"
+ //%token COUNTEREXAMPLE_TOK "COUNTEREXAMPLE"
%token PUSH_TOK "PUSH"
%token POP_TOK "POP"
%%
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;
+}
+;
%%
#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;
%token SEMICOLON_TOK
%token EOF_TOK
%token EQ_TOK
-/*BV SPECIFIC TOKENS*/
+ /*BV SPECIFIC TOKENS*/
%token NAND_TOK
%token NOR_TOK
%token NEQ_TOK
%%
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: */
/* ; */
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;
+}
;
%%
}//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
// 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.
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);
else
{
CONSTANTBV::ErrCode e =
- CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder);
+ CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder);
if (e != 0)
{
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);
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);
ASTNode
Simplifier::
CreateSimplifiedFormulaITE(const ASTNode& in0,
- const ASTNode& in1, const ASTNode& in2)
+ const ASTNode& in1, const ASTNode& in2)
{
ASTNode t0 = in0;
ASTNode t1 = in1;
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;
output = newVar;
} //end of start_abstracting if condition
- //memoize
+ //memoize
UpdateSimplifyMap(input, output, false);
return output;
} //end of RemoveWrites()
(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;
}
}
}
}
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.
}
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.
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
{
}
ASTNode STPMgr::CreateSimpAndOr(bool IsAnd,
- const ASTNode& form1, const ASTNode& form2)
+ const ASTNode& form1, const ASTNode& form2)
{
ASTVec children;
children.push_back(form1);
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);
// 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;
*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.
// 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;
if (_trace_simpbool)
{
cout << "========" << endl
- << "CreateSimpFormITE "
- << child0 << child1 << child2 << endl;
+ << "CreateSimpFormITE "
+ << child0 << child1 << child2 << endl;
}
if (ASTTrue == child0)
return result;
} //End of onChildDoNeg()
- //########################################
- //########################################
- //utilities for control bits.
+ //########################################
+ //########################################
+ //utilities for control bits.
void CNFMgr::initializeCNFInfo(CNFInfo& x)
{
return psi;
} //End of Product
- //########################################
- //########################################
- //prep. for cnf conversion
+ //########################################
+ //########################################
+ //prep. for cnf conversion
void CNFMgr::scanFormula(const ASTNode& varphi, bool isPos)
{
}
} //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)
{
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)
{
}
} //convertFormulaToCNFNegCases()
- //########################################
- //########################################
- // individual cnf conversion cases
+ //########################################
+ //########################################
+ // individual cnf conversion cases
void CNFMgr::convertFormulaToCNFPosPred(const ASTNode& varphi, ClauseList* defs)
{
return psi;
} //End of convertFormulaToCNFNegXORAux()
- //########################################
- //########################################
- // utilities for reclaiming memory.
+ //########################################
+ //########################################
+ // utilities for reclaiming memory.
void CNFMgr::reduceMemoryFootprintPos(const ASTNode& varphi)
{
}
} //End of reduceMemoryFootprintNeg()
- //########################################
- //########################################
+ //########################################
+ //########################################
ASTNode* CNFMgr::ASTNodeToASTNodePtr(const ASTNode& varphi)
{
return psi;
} //End of ASTNodeToASTNodePtr()
- //########################################
- //########################################
+ //########################################
+ //########################################
void CNFMgr::cleanup(const ASTNode& varphi)
{
info.clear();
} //End of cleanup()
- //########################################
- //########################################
- // constructor
+ //########################################
+ //########################################
+ // constructor
CNFMgr::CNFMgr(STPMgr *bmgr)
{
projects / francis / stp.git / commitdiff