case 'f':
BEEV::num_absrefine_flag = true;
//BEEV::num_absrefine = atoi(argv[++i]);
- break;
+ break;
case 'h':
BEEV::fprintf(stderr,BEEV::usage,BEEV::prog);
cout << helpstring;
break;
case 'z':
BEEV::print_sat_varorder_flag = true;
- break;
+ break;
default:
std::string s = "C_interface: vc_setFlags: Unrecognized commandline flag:\n";
s += helpstring;
break;
}
-
+
}
//Create a validity Checker. This is the global BeevMgr
VC vc_createValidityChecker(void) {
vc_setFlags('d');
- CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
+ CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
if(0 != c) {
cout << CONSTANTBV::BitVector_Error(c) << endl;
return 0;
BEEV::ASTNode q = (*(nodestar)e);
// b->Begin_RemoveWrites = true;
// BEEV::ASTNode q = b->SimplifyFormula_TopLevel(*((nodestar)e),false);
- // b->Begin_RemoveWrites = false;
+ // b->Begin_RemoveWrites = false;
q.PL_Print(cout);
}
-char * vc_printSMTLIB(VC vc, Expr e)
+char * vc_printSMTLIB(VC vc, Expr e)
{
stringstream ss;
printer::SMTLIB_Print(ss,*((nodestar)e), 0);
string s = ss.str();
char *copy = strdup(s.c_str());
return copy;
-
+
}
// prints Expr 'e' to stdout as C code
os << "QUERY( ";
b->Begin_RemoveWrites = true;
BEEV::ASTNode q = (simplify_print == 1) ? b->SimplifyFormula_TopLevel(*((nodestar)e),false) : *(nodestar)e;
- b->Begin_RemoveWrites = false;
+ b->Begin_RemoveWrites = false;
q.PL_Print(os);
os << " );" << endl;
BEEV::ASTNode q = *((nodestar)e);
// b->Begin_RemoveWrites = true;
// BEEV::ASTNode q = b->SimplifyFormula_TopLevel(*((nodestar)e),false);
- // b->Begin_RemoveWrites = false;
+ // b->Begin_RemoveWrites = false;
q.PL_Print(os);
//((nodestar)e)->PL_Print(os);
string s = os.str();
//b->Begin_RemoveWrites = true;
//BEEV::ASTNode q = b->SimplifyFormula_TopLevel(b->GetQuery(),false);
BEEV::ASTNode q = b->GetQuery();
- //b->Begin_RemoveWrites = false;
+ //b->Begin_RemoveWrites = false;
q.PL_Print(os);
// b->GetQuery().PL_Print(os);
os << ");" << endl;
bmstar b = (bmstar)vc;
nodestar a = (nodestar)array;
nodestar i = (nodestar)index;
-
+
b->BVTypeCheck(*a);
b->BVTypeCheck(*i);
node o = b->CreateTerm(BEEV::READ,a->GetValueWidth(),*a,*i);
/////////////////////////////////////////////////////////////////////////////
// Context-related methods //
/////////////////////////////////////////////////////////////////////////////
-//! Assert a new formula in the current context.
+//! Assert a new formula in the current context.
/*! The formula must have Boolean type. */
void vc_assertFormula(VC vc, Expr e, int absrefine_num) {
nodestar a = (nodestar)e;
b->BVTypeCheck(*a);
b->AddQuery(*a);
- const BEEV::ASTVec v = b->GetAsserts();
+ const BEEV::ASTVec v = b->GetAsserts();
node o;
if(!v.empty()) {
if(v.size()==1)
return b->TopLevelSAT(v[0],*a);
- else
+ else
return b->TopLevelSAT(b->CreateNode(BEEV::AND,v),*a);
}
else
void vc_printCounterExample(VC vc) {
bmstar b = (bmstar)vc;
- BEEV::print_counterexample_flag = true;
+ BEEV::print_counterexample_flag = true;
cout << "COUNTEREXAMPLE BEGIN: \n";
b->PrintCounterExample(true);
cout << "COUNTEREXAMPLE END: \n";
Expr vc_getCounterExample(VC vc, Expr e) {
nodestar a = (nodestar)e;
- bmstar b = (bmstar)vc;
+ bmstar b = (bmstar)vc;
bool t = false;
if(b->CounterExampleSize())
t = true;
- nodestar output = new node(b->GetCounterExample(t, *a));
+ nodestar output = new node(b->GetCounterExample(t, *a));
//if(cinterface_exprdelete_on) created_exprs.push_back(output);
return output;
}
WholeCounterExample vc_getWholeCounterExample(VC vc) {
bmstar b = (bmstar)vc;
- CompleteCEStar c =
+ CompleteCEStar c =
new BEEV::CompleteCounterExample(b->GetCompleteCounterExample(), b);
return c;
}
/////////////////////////////////////////////////////////////////////////////
// Expr Creation methods //
/////////////////////////////////////////////////////////////////////////////
-//! Create a variable with a given name and type
+//! Create a variable with a given name and type
/*! The type cannot be a function type. */
-Expr vc_varExpr1(VC vc, char* name,
+Expr vc_varExpr1(VC vc, const char* name,
int indexwidth, int valuewidth) {
bmstar b = (bmstar)vc;
node o = b->CreateSymbol(name);
o.SetIndexWidth(indexwidth);
o.SetValueWidth(valuewidth);
-
+
nodestar output = new node(o);
////if(cinterface_exprdelete_on) created_exprs.push_back(output);
b->BVTypeCheck(*output);
return output;
}
-Expr vc_varExpr(VC vc, char * name, Type type) {
+Expr vc_varExpr(VC vc, const char * name, Type type) {
bmstar b = (bmstar)vc;
nodestar a = (nodestar)type;
Expr vc_trueExpr(VC vc) {
bmstar b = (bmstar)vc;
node c = b->CreateNode(BEEV::TRUE);
-
+
nodestar d = new node(c);
//if(cinterface_exprdelete_on) created_exprs.push_back(d);
return d;
Expr vc_falseExpr(VC vc) {
bmstar b = (bmstar)vc;
node c = b->CreateNode(BEEV::FALSE);
-
+
nodestar d = new node(c);
//if(cinterface_exprdelete_on) created_exprs.push_back(d);
return d;
Expr vc_notExpr(VC vc, Expr ccc) {
bmstar b = (bmstar)vc;
nodestar a = (nodestar)ccc;
-
+
node o = b->CreateNode(BEEV::NOT,*a);
b->BVTypeCheck(o);
bmstar b = (bmstar)vc;
nodestar l = (nodestar)left;
nodestar r = (nodestar)right;
-
+
node o = b->CreateNode(BEEV::AND,*l,*r);
b->BVTypeCheck(o);
bmstar b = (bmstar)vc;
nodestar * c = (nodestar *)cc;
nodelist d;
-
+
for(int i =0; i < n; i++)
d.push_back(*c[i]);
-
+
node o = b->CreateNode(BEEV::AND,d);
b->BVTypeCheck(o);
bmstar b = (bmstar)vc;
nodestar * c = (nodestar *)cc;
nodelist d;
-
+
for(int i =0; i < n; i++)
d.push_back(*c[i]);
-
+
node o = b->CreateNode(BEEV::OR,d);
b->BVTypeCheck(o);
bmstar b = (bmstar)vc;
nodestar * c = (nodestar *)cc;
nodelist d;
-
+
for(int i =0; i < n; i++)
d.push_back(*c[i]);
-
+
node o = b->CreateTerm(BEEV::BVPLUS, n_bits, d);
b->BVTypeCheck(o);
nodestar c = (nodestar)cond;
nodestar t = (nodestar)thenpart;
nodestar e = (nodestar)elsepart;
-
+
b->BVTypeCheck(*c);
b->BVTypeCheck(*t);
b->BVTypeCheck(*e);
bmstar b = (bmstar)vc;
nodestar c = (nodestar)antecedent;
nodestar t = (nodestar)consequent;
-
+
b->BVTypeCheck(*c);
b->BVTypeCheck(*t);
node o;
bmstar b = (bmstar)vc;
nodestar c = (nodestar)e0;
nodestar t = (nodestar)e1;
-
+
b->BVTypeCheck(*c);
b->BVTypeCheck(*t);
node o;
Expr vc_boolToBVExpr(VC vc, Expr form) {
bmstar b = (bmstar)vc;
nodestar c = (nodestar)form;
-
+
b->BVTypeCheck(*c);
if(!is_Form_kind(c->GetKind()))
BEEV::FatalError("CInterface: vc_BoolToBVExpr: You have input a NON formula:",*c);
-
+
node o;
- node one = b->CreateOneConst(1);
- node zero = b->CreateZeroConst(1);
+ node one = b->CreateOneConst(1);
+ node zero = b->CreateZeroConst(1);
o = b->CreateTerm(BEEV::ITE,1,*c,one,zero);
b->BVTypeCheck(o);
bmstar b = (bmstar)vc;
nodestar c = (nodestar)boolvar;
nodestar t = (nodestar)parameter;
-
+
b->BVTypeCheck(*c);
b->BVTypeCheck(*t);
node o;
/////////////////////////////////////////////////////////////////////////////
Type vc_bvType(VC vc, int num_bits) {
bmstar b = (bmstar)vc;
-
+
if(!(0 < num_bits))
- BEEV::FatalError("CInterface: number of bits in a bvtype must be a positive integer:",
+ 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);
return vc_bvType(vc,32);
}
-Expr vc_bvConstExprFromDecStr(VC vc, const size_t width, char* decimalInput ) {
+Expr vc_bvConstExprFromDecStr(VC vc, const size_t width, const char* decimalInput ) {
bmstar b = (bmstar)vc;
string *param = new string(decimalInput);
}
-Expr vc_bvConstExprFromStr(VC vc, char* binary_repr) {
+Expr vc_bvConstExprFromStr(VC vc, const char* binary_repr) {
bmstar b = (bmstar)vc;
node n = b->CreateBVConst(binary_repr,2);
}
Expr vc_bvConstExprFromInt(VC vc,
- int n_bits,
+ int n_bits,
unsigned int value) {
bmstar b = (bmstar)vc;
}
Expr vc_bvConstExprFromLL(VC vc,
- int n_bits,
+ int n_bits,
unsigned long long value) {
bmstar b = (bmstar)vc;
-
+
node n = b->CreateBVConst(n_bits, value);
b->BVTypeCheck(n);
nodestar output = new node(n);
bmstar b = (bmstar)vc;
nodestar a = (nodestar)ccc;
b->BVTypeCheck(*a);
-
- unsigned int w = a->GetValueWidth();
+
+ unsigned int w = a->GetValueWidth();
//the amount by which you are rightshifting
//is less-than/equal-to the length of input
- //bitvector
+ //bitvector
if(0 < (unsigned)sh_amt && (unsigned)sh_amt < w) {
node len = b->CreateBVConst(sh_amt, 0);
node hi = b->CreateBVConst(32,w-1);
for(int count=32; count >= 0; count--){
if(count != 32) {
- ifpart = vc_eqExpr(vc, sh_amt,
+ ifpart = vc_eqExpr(vc, sh_amt,
vc_bvConstExprFromInt(vc, shift_width, count));
thenpart = vc_bvExtract(vc,
vc_bvLeftShiftExpr(vc, count, child),
ite = vc_iteExpr(vc,ifpart,thenpart,elsepart);
elsepart = ite;
- }
+ }
else
- elsepart = vc_bvConstExprFromInt(vc,child_width, 0);
- }
- return ite;
+ elsepart = vc_bvConstExprFromInt(vc,child_width, 0);
+ }
+ return ite;
}
Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs) {
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);
+ 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;
+ }
+ }
+ return ite;
}
Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child) {
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);
+ 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;
+ }
+ }
+ return ite;
}
Expr vc_bvExtract(VC vc, Expr ccc, int hi_num, int low_num) {
b->BVTypeCheck(*a);
node bit = b->CreateBVConst(32,bit_num);
- //node o = b->CreateNode(BEEV::BVGETBIT,*a,bit);
+ //node o = b->CreateNode(BEEV::BVGETBIT,*a,bit);
node zero = b->CreateBVConst(1,0);
node oo = b->CreateTerm(BEEV::BVEXTRACT,1,*a,bit,bit);
node o = b->CreateNode(BEEV::EQ,oo,zero);
b->BVTypeCheck(o);
nodestar output = new node(o);
//if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
+ return output;
}
Expr vc_bvBoolExtract_Zero(VC vc, Expr ccc, int bit_num) {
b->BVTypeCheck(*a);
node bit = b->CreateBVConst(32,bit_num);
- //node o = b->CreateNode(BEEV::BVGETBIT,*a,bit);
+ //node o = b->CreateNode(BEEV::BVGETBIT,*a,bit);
node zero = b->CreateBVConst(1,0);
node oo = b->CreateTerm(BEEV::BVEXTRACT,1,*a,bit,bit);
node o = b->CreateNode(BEEV::EQ,oo,zero);
b->BVTypeCheck(o);
nodestar output = new node(o);
//if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
+ return output;
}
Expr vc_bvBoolExtract_One(VC vc, Expr ccc, int bit_num) {
b->BVTypeCheck(*a);
node bit = b->CreateBVConst(32,bit_num);
- //node o = b->CreateNode(BEEV::BVGETBIT,*a,bit);
+ //node o = b->CreateNode(BEEV::BVGETBIT,*a,bit);
node one = b->CreateBVConst(1,1);
node oo = b->CreateTerm(BEEV::BVEXTRACT,1,*a,bit,bit);
node o = b->CreateNode(BEEV::EQ,oo,one);
b->BVTypeCheck(o);
nodestar output = new node(o);
//if(cinterface_exprdelete_on) created_exprs.push_back(output);
- return output;
+ return output;
}
Expr vc_bvSignExtend(VC vc, Expr ccc, int nbits) {
bmstar b = (bmstar)vc;
nodestar a = (nodestar)ccc;
-
+
//width of the expr which is being sign extended. nbits is the
//resulting length of the signextended expr
b->BVTypeCheck(*a);
-
+
unsigned exprlen = a->GetValueWidth();
unsigned outputlen = nbits;
node n;
//if(cinterface_exprdelete_on) created_exprs.push_back(output);
b->Begin_RemoveWrites = false;
delete round1;
- return output;
+ return output;
}
else {
nodestar round1 = new node(b->SimplifyTerm(*a));
}
/* C pointer support: C interface to support C memory arrays in CVCL */
-Expr vc_bvCreateMemoryArray(VC vc, char * arrayName) {
+Expr vc_bvCreateMemoryArray(VC vc, const char * arrayName) {
Type bv8 = vc_bvType(vc,8);
Type bv32 = vc_bvType(vc,32);
-
+
Type malloced_mem0 = vc_arrayType(vc,bv32,bv8);
return vc_varExpr(vc, arrayName, malloced_mem0);
}
-Expr vc_bvReadMemoryArray(VC vc,
- Expr array,
+Expr vc_bvReadMemoryArray(VC vc,
+ Expr array,
Expr byteIndex, int numOfBytes) {
if(!(numOfBytes > 0))
BEEV::FatalError("numOfBytes must be greater than 0");
while(--numOfBytes > 0) {
Expr b = vc_readExpr(vc,array,
/*vc_simplify(vc, */
- vc_bvPlusExpr(vc, 32,
+ vc_bvPlusExpr(vc, 32,
byteIndex,
vc_bvConstExprFromInt(vc,32,count)))/*)*/;
a = vc_bvConcatExpr(vc,b,a);
count++;
}
return a;
- }
+ }
}
-Expr vc_bvWriteToMemoryArray(VC vc,
- Expr array, Expr byteIndex,
+Expr vc_bvWriteToMemoryArray(VC vc,
+ Expr array, Expr byteIndex,
Expr element, int numOfBytes) {
if(!(numOfBytes > 0))
BEEV::FatalError("numOfBytes must be greater than 0");
-
+
int newBitsPerElem = numOfBytes*8;
if(numOfBytes == 1)
return vc_writeExpr(vc, array, byteIndex, element);
Expr newarray = vc_writeExpr(vc, array, byteIndex, c);
while(--numOfBytes > 0) {
hi = low-1;
- low = low-8;
+ low = low-8;
low_elem = low_elem + 8;
hi_elem = low_elem + 7;
c = vc_bvExtract(vc, element, hi_elem, low_elem);
- newarray =
+ newarray =
vc_writeExpr(vc, newarray,
vc_bvPlusExpr(vc, 32, byteIndex, vc_bvConstExprFromInt(vc,32,count)),
c);
count++;
}
return newarray;
- }
+ }
}
Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value){
// bmstar b = (bmstar)vc;
// extern FILE* cvcin;
// const char * prog = "stp";
-
+
// cvcin = fopen(infile,"r");
// if(cvcin == NULL) {
// fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
// BEEV::FatalError("");
// }
-
+
// BEEV::GlobalBeevMgr = b;
-// CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
+// CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
// if(0 != c) {
// cout << CONSTANTBV::BitVector_Error(c) << endl;
// return 0;
// nodelist aaa = b->GetAsserts();
// //Don't add the query. It gets added automatically if the input file
-// //has QUERY in it
+// //has QUERY in it
// //
// //node bbb = b->CreateNode(BEEV::NOT,b->GetQuery());
// node o = b->CreateNode(BEEV::AND,aaa);
// } //end of vc_parseExpr()
-Expr vc_parseExpr(VC vc, char* infile) {
+Expr vc_parseExpr(VC vc, const char* infile) {
bmstar b = (bmstar)vc;
extern FILE* cvcin;
const char * prog = "stp";
-
+
cvcin = fopen(infile,"r");
if(cvcin == NULL) {
fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
BEEV::FatalError("");
}
-
+
BEEV::GlobalBeevMgr = b;
- CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
+ CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
if(0 != c) {
cout << CONSTANTBV::BitVector_Error(c) << endl;
return 0;
BEEV::ASTNode asserts = (*(BEEV::ASTVec*)AssertsQuery)[0];
BEEV::ASTNode query = (*(BEEV::ASTVec*)AssertsQuery)[1];
//b->TopLevelSAT(asserts, query);
-
+
node oo = b->CreateNode(BEEV::NOT,query);
node o = b->CreateNode(BEEV::AND,asserts,oo);
nodestar output = new node(o);
//if(cinterface_exprdelete_on) created_exprs.push_back(output);
return output;
}
- else
+ else
BEEV::FatalError("getChild: Error accessing childNode in expression: ",*a);
return a;
}
assert(query);
bmstar b = (bmstar)vc;
nodestar qry = (nodestar)query;
- BEEV::ASTVec v = b->GetAsserts();
+ BEEV::ASTVec v = b->GetAsserts();
BEEV::ASTNode out = b->CreateNode(BEEV::AND,b->CreateNode(BEEV::NOT,*qry),v);
return out.Hash();
}
switch(e->GetType()) {
case BEEV::BOOLEAN_TYPE:
return vc_boolType(vc);
- break;
+ break;
case BEEV::BITVECTOR_TYPE:
return vc_bvType(vc,e->GetValueWidth());
break;
exprkind_t getExprKind(Expr e) {
nodestar input = (nodestar)e;
- return (exprkind_t)(input->GetKind());
+ return (exprkind_t)(input->GetKind());
}
int getDegree (Expr e) {
}
return e->GetValueWidth();
-}
+}
type_t getType (Expr ex) {
nodestar e = (nodestar)ex;
-
+
return (type_t)(e->GetType());
}
void vc_printCounterExampleFile(VC vc, int fd) {
fdostream os(fd);
bmstar b = (bmstar)vc;
- BEEV::print_counterexample_flag = true;
+ BEEV::print_counterexample_flag = true;
os << "COUNTEREXAMPLE BEGIN: \n";
b->PrintCounterExample(true, os);
os << "COUNTEREXAMPLE END: \n";
#endif
#include <stdio.h>
-
+
#ifdef STP_STRONG_TYPING
#else
//This gives absolutely no pointer typing at compile-time. Most C
// s : stats
// v : print nodes
void vc_setFlags(char c);
-
+
//! Flags can be NULL
VC vc_createValidityChecker(void);
-
+
// Basic types
Type vc_boolType(VC vc);
-
+
//! Create an array type
Type vc_arrayType(VC vc, Type typeIndex, Type typeData);
// Expr manipulation methods //
/////////////////////////////////////////////////////////////////////////////
- //! Create a variable with a given name and type
+ //! Create a variable with a given name and type
/*! The type cannot be a function type. The var name can contain
only variables, numerals and underscore. If you use any other
- symbol, you will get a segfault. */
- Expr vc_varExpr(VC vc, char * name, Type type);
+ symbol, you will get a segfault. */
+ Expr vc_varExpr(VC vc, const char * name, Type type);
//The var name can contain only variables, numerals and
//underscore. If you use any other symbol, you will get a segfault.
- Expr vc_varExpr1(VC vc, char* name,
+ Expr vc_varExpr1(VC vc, const char* name,
int indexwidth, int valuewidth);
//! Get the expression and type associated with a name.
/*! If there is no such Expr, a NULL Expr is returned. */
//Expr vc_lookupVar(VC vc, char* name, Type* type);
-
+
//! Get the type of the Expr.
Type vc_getType(VC vc, Expr e);
-
+
int vc_getBVLength(VC vc, Expr e);
//! Create an equality expression. The two children must have the same type.
Expr vc_eqExpr(VC vc, Expr child0, Expr child1);
-
+
// Boolean expressions
-
+
// The following functions create Boolean expressions. The children
// provided as arguments must be of type Boolean (except for the
// function vc_iteExpr(). In the case of vc_iteExpr() the
//The output type of vc_iteExpr can be Boolean (formula-level ite)
//or bit-vector (word-level ite)
Expr vc_iteExpr(VC vc, Expr conditional, Expr ifthenpart, Expr elsepart);
-
+
//Boolean to single bit BV Expression
Expr vc_boolToBVExpr(VC vc, Expr form);
Expr vc_paramBoolExpr(VC vc, Expr var, Expr param);
// Arrays
-
+
//! Create an expression for the value of array at the given index
Expr vc_readExpr(VC vc, Expr array, Expr index);
//! Array update; equivalent to "array WITH [index] := newValue"
Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue);
-
+
// Expr I/O: Parses directly from file in the c_interface. pretty cool!!
- Expr vc_parseExpr(VC vc, char* s);
+ Expr vc_parseExpr(VC vc, const char* s);
//! Prints 'e' to stdout.
void vc_printExpr(VC vc, Expr e);
//! Prints 'e' into an open file descriptor 'fd'
void vc_printExprFile(VC vc, Expr e, int fd);
- //! Prints state of 'vc' into malloc'd buffer '*buf' and stores the
- // length into '*len'. It is the responsibility of the caller to
+ //! Prints state of 'vc' into malloc'd buffer '*buf' and stores the
+ // length into '*len'. It is the responsibility of the caller to
// free the buffer.
//void vc_printStateToBuffer(VC vc, char **buf, unsigned long *len);
- //! Prints 'e' to malloc'd buffer '*buf'. Sets '*len' to the length of
+ //! Prints 'e' to malloc'd buffer '*buf'. Sets '*len' to the length of
// the buffer. It is the responsibility of the caller to free the buffer.
void vc_printExprToBuffer(VC vc, Expr e, char **buf, unsigned long * len);
//responsibility of the caller to free the buffer. The flag
//simplify_print must be set to "1" if you wish simplification to
//occur dring printing. It must be set to "0" otherwise
- void vc_printQueryStateToBuffer(VC vc, Expr e,
+ void vc_printQueryStateToBuffer(VC vc, Expr e,
char **buf, unsigned long *len, int simplify_print);
//! Similar to vc_printQueryStateToBuffer()
/////////////////////////////////////////////////////////////////////////////
// Context-related methods //
/////////////////////////////////////////////////////////////////////////////
-
- //! Assert a new formula in the current context.
+
+ //! Assert a new formula in the current context.
/*! The formula must have Boolean type. */
void vc_assertFormula(VC vc, Expr e, int absrefine_num=0);
-
+
//! Simplify e with respect to the current context
Expr vc_simplify(VC vc, Expr e);
//! Check validity of e in the current context. e must be a FORMULA
//
- //if returned 0 then input is INVALID.
+ //if returned 0 then input is INVALID.
//
//if returned 1 then input is VALID
//
//if returned 2 then ERROR
int vc_query(VC vc, Expr e);
-
+
//! Return the counterexample after a failed query.
Expr vc_getCounterExample(VC vc, Expr e);
//! get size of counterexample, i.e. the number of variables/array
//locations in the counterexample.
int vc_counterexample_size(VC vc);
-
+
//! Checkpoint the current context and increase the scope level
void vc_push(VC vc);
-
+
//! Restore the current context to its state at the last checkpoint
void vc_pop(VC vc);
-
+
//! Return an int from a constant bitvector expression
int getBVInt(Expr e);
//! Return an unsigned int from a constant bitvector expression
unsigned int getBVUnsigned(Expr e);
//! Return an unsigned long long int from a constant bitvector expressions
unsigned long long int getBVUnsignedLongLong(Expr e);
-
+
/**************************/
/* BIT VECTOR OPERATIONS */
/**************************/
Type vc_bvType(VC vc, int no_bits);
Type vc_bv32Type(VC vc);
-
- Expr vc_bvConstExprFromDecStr(VC vc, const size_t width, char* decimalInput );
- Expr vc_bvConstExprFromStr(VC vc, char* binary_repr);
+
+ Expr vc_bvConstExprFromDecStr(VC vc, const size_t width, const char* decimalInput );
+ Expr vc_bvConstExprFromStr(VC vc, const char* binary_repr);
Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value);
Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long long value);
Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value);
-
+
Expr vc_bvConcatExpr(VC vc, Expr left, Expr right);
Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right);
Expr vc_bvPlusExprN(VC vc, int n_bits, Expr* children, int numOfChildNodes);
Expr vc_sbvDivExpr(VC vc, int n_bits, Expr left, Expr right);
// signed left modulo right i.e. left%right
Expr vc_sbvModExpr(VC vc, int n_bits, Expr left, Expr right);
-
+
Expr vc_bvLtExpr(VC vc, Expr left, Expr right);
Expr vc_bvLeExpr(VC vc, Expr left, Expr right);
Expr vc_bvGtExpr(VC vc, Expr left, Expr right);
Expr vc_bvGeExpr(VC vc, Expr left, Expr right);
-
+
Expr vc_sbvLtExpr(VC vc, Expr left, Expr right);
Expr vc_sbvLeExpr(VC vc, Expr left, Expr right);
Expr vc_sbvGtExpr(VC vc, Expr left, Expr right);
Expr vc_sbvGeExpr(VC vc, Expr left, Expr right);
-
+
Expr vc_bvUMinusExpr(VC vc, Expr child);
- // bitwise operations: these are terms not formulas
+ // bitwise operations: these are terms not formulas
Expr vc_bvAndExpr(VC vc, Expr left, Expr right);
Expr vc_bvOrExpr(VC vc, Expr left, Expr right);
Expr vc_bvXorExpr(VC vc, Expr left, Expr right);
Expr vc_bvNotExpr(VC vc, Expr child);
-
+
Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child);
Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child);
/* Same as vc_bvLeftShift only that the answer in 32 bits long */
Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs);
Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, int low_bit_no);
-
+
//accepts a bitvector and position, and returns a boolean
//corresponding to that position. More precisely, it return the
//equation (x[bit_no:bit_no] == 0)
Expr vc_bvBoolExtract(VC vc, Expr x, int bit_no);
Expr vc_bvBoolExtract_Zero(VC vc, Expr x, int bit_no);
-
+
//accepts a bitvector and position, and returns a boolean
//corresponding to that position. More precisely, it return the
//equation (x[bit_no:bit_no] == 1)
- Expr vc_bvBoolExtract_One(VC vc, Expr x, int bit_no);
+ Expr vc_bvBoolExtract_One(VC vc, Expr x, int bit_no);
Expr vc_bvSignExtend(VC vc, Expr child, int nbits);
-
+
/*C pointer support: C interface to support C memory arrays in CVCL */
- Expr vc_bvCreateMemoryArray(VC vc, char * arrayName);
- Expr vc_bvReadMemoryArray(VC vc,
+ Expr vc_bvCreateMemoryArray(VC vc, const char * arrayName);
+ Expr vc_bvReadMemoryArray(VC vc,
Expr array, Expr byteIndex, int numOfBytes);
- Expr vc_bvWriteToMemoryArray(VC vc,
- Expr array, Expr byteIndex,
+ Expr vc_bvWriteToMemoryArray(VC vc,
+ Expr array, Expr byteIndex,
Expr element, int numOfBytes);
Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value);
-
+
// return a string representation of the Expr e. The caller is responsible
// for deallocating the string with free()
char* exprString(Expr e);
-
+
// return a string representation of the Type t. The caller is responsible
// for deallocating the string with free()
char* typeString(Type t);
// get name of expression. must be a variable.
const char* exprName(Expr e);
-
+
// get the node ID of an Expr.
int getExprID (Expr ex);
projects / francis / stp.git / commitdiff