24 #ifndef _cvc3__include__c_interface_h_
25 #define _cvc3__include__c_interface_h_
90 char* field1,
Type type1);
92 char* field1,
Type type1,
93 char* field2,
Type type2);
105 char** selectors,
Expr* types);
112 int* arities,
char*** selectors,
Expr** types);
122 int* numCons,
char*** constructors,
123 int** arities,
char**** selectors,
265 Expr* oldTerms,
int numOldTerms,
266 Expr* newTerms,
int numNewTerms);
334 char* field1,
Expr expr1);
336 char* field1,
Expr expr1,
337 char* field2,
Expr expr2);
417 Expr array,
Expr byteIndex,
int numOfBytes);
420 Expr element,
int numOfBytes);
Expr vc_simplify(VC vc, Expr e)
Simplify e with respect to the current context.
Expr vc_tupleExprN(VC vc, Expr *children, int numChildren)
Create a tuple expression.
Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right)
Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right)
Expr vc_importExpr(VC vc, Expr e)
Import the Expr from another instance of VC.
Expr vc_getChild(Expr e, int i)
Type vc_dataType1(VC vc, char *name, char *constructor, int arity, char **selectors, Expr *types)
Single datatype, single constructor.
char * vc_exprString(Expr e)
Convert Expr to string.
void vc_deleteExpr(Expr e)
Delete expression.
Type vc_getBaseTypeOfType(VC vc, Type t)
Get the largest supertype of the Type.
Expr vc_bvConcatExpr(VC vc, Expr left, Expr right)
Op vc_createOpDef(VC vc, char *name, Type type, Expr def)
Create a named user-defined function with a given type.
Expr vc_bvReadMemoryArray(VC vc, Expr array, Expr byteIndex, int numOfBytes)
Expr vc_getClosure(VC vc)
After successful query, return its closure |- Gamma => phi.
Expr vc_orExprN(VC vc, Expr *children, int numChildren)
void vc_returnFromCheck(VC vc)
Returns to context immediately before last invalid query.
Expr vc_ratExprFromStr(VC vc, char *n, char *d, int base)
Create a rational number n/d; n and d are given as strings.
void vc_pop(VC vc)
Restore the current context to its state at the last checkpoint.
Expr vc_bvSLtExpr(VC vc, Expr left, Expr right)
int vc_getKindInt(VC vc, char *kind_name)
Translate a kind string to an int.
Type vc_funTypeN(VC vc, Type *args, Type typeRan, int numArgs)
Create a function type with N arguments.
void vc_setStringFlag(Flags flags, char *name, char *val)
Set a string flag to the given value.
Expr vc_bvSDivExpr(VC vc, Expr left, Expr right)
Flags vc_createFlags()
Create validity checker's flags.
Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, int low_bit_no)
Expr vc_getProof(VC vc)
Returns the proof for the last proven query.
Expr vc_bvSGtExpr(VC vc, Expr left, Expr right)
Expr vc_getProofClosure(VC vc)
Construct a proof of the query closure |- Gamma => phi.
Expr vc_bvConcatExprN(VC vc, Expr *children, int numChildren)
void vc_deleteVector(Expr *e)
Delete vector of expressions.
Type vc_createType(VC vc, char *typeName)
Create an uninterpreted named type.
void vc_destroyValidityChecker(VC vc)
Destroy the validity checker.
void vc_printExpr(VC vc, Expr e)
Expr vc_parseExpr(VC vc, char* s);.
Expr vc_bvLeExpr(VC vc, Expr left, Expr right)
Expr vc_ratExpr(VC vc, int n, int d)
Create a rational number with numerator n and denominator d.
void vc_popto(VC vc, int stackLevel)
Restore the current context to the given stackLevel.
Expr vc_datatypeConsExpr(VC vc, char *constructor, int numArgs, Expr *args)
Datatype constructor expression.
Expr vc_recSelectExpr(VC vc, Expr record, char *field)
Create an expression representing the selection of a field from a record.
char * vc_printExprString(VC vc, Expr e)
Print e into a char*.
Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc)
void vc_setTriggers(VC vc, Expr e, int numTrigs, Expr *triggers)
Set triggers for a forallExpr.
Expr vc_bvAndExpr(VC vc, Expr left, Expr right)
int vc_query(VC vc, Expr e)
Check validity of e in the current context.
Expr vc_varExprDef(VC vc, char *name, Type type, Expr def)
Create a variable with a given name, type, and value.
void vc_deleteFlags(Flags flags)
Delete the flags.
Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right)
unsigned int vc_getBVUnsigned(VC vc, Expr e)
Return an unsigned int from a constant bitvector expression.
Expr * vc_getInternalAssumptions(VC vc, int *size)
Get assumptions made internally in this and all previous contexts.
Expr vc_bvNotExpr(VC vc, Expr child)
Type vc_subtypeType(VC vc, Expr pred, Expr witness)
Creates a subtype defined by the given predicate.
Expr vc_funExpr3(VC vc, Op op, Expr child0, Expr child1, Expr child2)
Expr vc_funExprN(VC vc, Op op, Expr *children, int numChildren)
Expr vc_plusExprN(VC vc, Expr *children, int numChildren)
void vc_reset_error_status()
Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value)
Expr * vc_getAssumptions(VC vc, int *size)
Get all assumptions made in this and all previous contexts.
int vc_getNumVars(Expr e)
int vc_getBVInt(VC vc, Expr e)
Return an int from a constant bitvector expression.
Type vc_forallExpr(VC vc, Expr *Bvars, int numBvars, Expr f)
Create a FORALL quantifier.
Op vc_lambdaExpr(VC vc, int numVars, Expr *vars, Expr body)
Lambda-expression.
const char * vc_getKindString(VC vc, int kind)
Translate a kind int to a string.
Type vc_bvType(VC vc, int n)
Create a bitvector type of length n.
Expr vc_plusExpr(VC vc, Expr left, Expr right)
Type vc_recordType3(VC vc, char *field0, Type type0, char *field1, Type type1, char *field2, Type type2)
Expr vc_gtExpr(VC vc, Expr left, Expr right)
Expr vc_existsExpr(VC vc, Expr *Bvars, int numBvars, Expr f)
Create an EXISTS quantifier.
Type vc_subRangeType(VC vc, int lowerEnd, int upperEnd)
Create a subrange type.
int vc_isQuantifier(Expr e)
Expr vc_notExpr(VC vc, Expr child)
Expr vc_funExpr1(VC vc, Op op, Expr child)
Create expressions with a user-defined operator.
Expr vc_getTCC(VC vc)
Returns the TCC of the last assumption or query.
Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child)
Op vc_lookupOp(VC vc, char *name, Type *type)
Lookup an operator by name.
Type vc_funType3(VC vc, Type a1, Type a2, Type a3, Type typeRan)
Create a function type with 3 arguments.
VC vc_createValidityChecker(Flags flags)
Flags can be NULL.
Expr vc_getProofTCC(VC vc)
Returns the proof of TCC of the last assumption or query.
Expr vc_ltExpr(VC vc, Expr left, Expr right)
void vc_printExprFile(VC vc, Expr e, int fd)
Print 'e' into an open file descriptor.
Expr vc_getFun(VC vc, Expr e)
Expr vc_geExpr(VC vc, Expr left, Expr right)
Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right)
Expr vc_datatypeTestExpr(VC vc, char *constructor, Expr arg)
Datatype tester expression.
ExprManager * vc_getEM(VC vc)
Return the ExprManager.
Expr vc_bv32MultExpr(VC vc, Expr left, Expr right)
Type vc_tupleTypeN(VC vc, Type *types, int numTypes)
Create a tuple type. 'types' is an array of types of length numTypes.
void vc_setStrSeqFlag(Flags flags, char *name, char *str, int val)
Add a (string, bool) pair to the multy-string flag.
int vc_inconsistent(VC vc, Expr **assumptions, int *size)
Expr vc_bvGeExpr(VC vc, Expr left, Expr right)
Expr vc_getVar(Expr e, int i)
Expr vc_tupleSelectExpr(VC vc, Expr tuple, int index)
Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5)
Expr vc_substExpr(VC vc, Expr e, Expr *oldTerms, int numOldTerms, Expr *newTerms, int numNewTerms)
Type vc_recordTypeN(VC vc, char **fields, Type *types, int numFields)
Create a record type.
Expr vc_bvConstExprFromStr(VC vc, char *binary_repr)
Expr vc_lookupVar(VC vc, char *name, Type *type)
Get the expression and type associated with a name.
Expr vc_powExpr(VC vc, Expr pow, Expr base)
Expr vc_multExpr(VC vc, Expr left, Expr right)
void vc_deleteOp(Op op)
Delete operator.
Expr * vc_getAssumptionsUsed(VC vc, int *size)
Returns the set of assumptions used in the proof of queried formula.
Expr vc_readExpr(VC vc, Expr array, Expr index)
Create an expression for the value of array at the given index.
Expr vc_bvSignExtend(VC vc, Expr child, int nbits)
Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child)
Expr vc_bvUMinusExpr(VC vc, Expr child)
Expr vc_uminusExpr(VC vc, Expr child)
Unary minus. Child must have a numeric type.
Expr vc_bvSLeExpr(VC vc, Expr left, Expr right)
Type * vc_dataTypeMN(VC vc, int numTypes, char **names, int *numCons, char ***constructors, int **arities, char ****selectors, Expr ***types)
Multiple datatypes.
Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child)
int vc_getInt(Expr e)
Return an int from a rational expression.
Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child)
void vc_print_statistics(VC vc)
Print statistics.
int vc_stackLevel(VC vc)
Returns the current stack level. Initial level is 0.
Expr * vc_getConcreteModel(VC vc, int *size)
Will assign concrete values to all user created variables.
Expr vc_funExpr2(VC vc, Op op, Expr left, Expr right)
Expr * vc_getAssumptionsTCC(VC vc, int *size)
Return the set of assumptions used in the proof of the last TCC.
void vc_deleteTypeVector(Type *e)
Delete vector of types.
Expr vc_ratExprFromStr1(VC vc, char *n, int base)
Create a rational from a single string.
Expr vc_bvSGeExpr(VC vc, Expr left, Expr right)
void vc_deleteType(Type t)
Delete type.
Macros that should be defined everywhere during the building of the libraries and driver binary...
Expr vc_eqExpr(VC vc, Expr child0, Expr child1)
Create an equality expression. The two children must have the same type.
void vc_setIntFlag(Flags flags, char *name, int val)
Set an integer flag to the given value.
Expr vc_bvSRemExpr(VC vc, Expr left, Expr right)
Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long value)
Type vc_arrayType(VC vc, Type typeIndex, Type typeData)
Create an array type.
Type vc_funType2(VC vc, Type a1, Type a2, Type typeRan)
Create a function type with 2 arguments.
Expr vc_bvCreateMemoryArray(VC vc, char *arrayName)
Expr vc_andExprN(VC vc, Expr *children, int numChildren)
Expr * vc_getCounterExample(VC vc, int *size)
Return the counterexample after a failed query.
Expr vc_getExistential(Expr e)
Expr vc_bvURemExpr(VC vc, Expr left, Expr right)
Expr vc_getProofOfFile(VC vc, char *filename)
Returns the proof of a .cvc file, if it is valid.
Expr vc_bvWriteToMemoryArray(VC vc, Expr array, Expr byteIndex, Expr element, int numOfBytes)
Expr vc_getTypePred(VC vc, Type t, Expr e)
Get the subtype predicate.
Expr vc_getImpliedLiteral(VC vc)
Return next literal implied by last assertion. Null if none.
char * vc_incomplete(VC vc)
Returns non-NULL if the invalid result from last query() is imprecise.
Expr vc_bvSModExpr(VC vc, Expr left, Expr right)
void vc_setBoolFlag(Flags flags, char *name, int val)
Set a boolean flag to true or false.
int vc_compare_exprs(Expr e1, Expr e2)
Compares two expressions.
Expr vc_bvGtExpr(VC vc, Expr left, Expr right)
Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value)
Expr vc_listExpr(VC vc, int numKids, Expr *kids)
Create a list Expr.
Expr vc_getProofQuery(VC vc)
Expr vc_bvUDivExpr(VC vc, Expr left, Expr right)
Expr vc_recordExprN(VC vc, char **fields, Expr *exprs, int numFields)
Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child)
void vc_assertFormula(VC vc, Expr e)
Assert a new formula in the current context.
Expr vc_getProofAssumptions(VC vc)
Expr vc_recUpdateExpr(VC vc, Expr record, char *field, Expr newValue)
Record update; equivalent to "record WITH .field := newValue".
int vc_checkContinue(VC vc)
Get the next model.
Context * vc_getCurrentContext(VC vc)
Get the current context.
Expr vc_recordExpr1(VC vc, char *field, Expr expr)
void vc_registerAtom(VC vc, Expr e)
Register an atomic formula of interest.
int vc_get_error_status()
Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs)
Type vc_getType(VC vc, Expr e)
Get the type of the Expr.
Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child)
Op vc_createOp(VC vc, char *name, Type type)
Create an operator from a function with a given name and type.
Expr vc_iffExpr(VC vc, Expr left, Expr right)
Type vc_tupleType2(VC vc, Type type0, Type type1)
Expr vc_recordExpr2(VC vc, char *field0, Expr expr0, char *field1, Expr expr1)
Expr * vc_getUserAssumptions(VC vc, int *size)
Get assumptions made by the user in this and all previous contexts.
Type vc_getBaseType(VC vc, Expr e)
Get the largest supertype of the Expr.
Expr vc_idExpr(VC vc, char *name)
Create an ID Expr.
Expr vc_varExpr(VC vc, char *name, Type type)
Create a variable with a given name and type.
Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right)
Expr vc_distinctExpr(VC vc, Expr *children, int numChildren)
Create an all distinct expression. All children must ahve the same type.
Expr vc_tupleUpdateExpr(VC vc, Expr tuple, int index, Expr newValue)
Tuple update; equivalent to "tuple WITH index := newValue".
Type vc_recordType1(VC vc, char *field, Type type)
int vc_restart(VC vc, Expr e)
Restart the most recent query with e as an additional assertion.
Expr vc_bvXorExpr(VC vc, Expr left, Expr right)
Expr vc_bvOrExpr(VC vc, Expr left, Expr right)
Expr vc_andExpr(VC vc, Expr left, Expr right)
Type vc_tupleType3(VC vc, Type type0, Type type1, Type type2)
Expr vc_recordExpr3(VC vc, char *field0, Expr expr0, char *field1, Expr expr1, char *field2, Expr expr2)
Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue)
Array update; equivalent to "array WITH [index] := newValue".
Type vc_funType1(VC vc, Type a1, Type typeRan)
Create a function type with 1 argument.
char * vc_typeString(Type t)
Convert Type to string.
char * vc_get_error_string()
Expr vc_divideExpr(VC vc, Expr numerator, Expr denominator)
Expr vc_boundVarExpr(VC vc, char *name, char *uid, Type type)
Create a bound variable.
Type vc_dataTypeN(VC vc, char *name, int numCons, char **constructors, int *arities, char ***selectors, Expr **types)
Single datatype, multiple constructors.
Type vc_importType(Type t)
Import the Type from another instance of VC.
Expr vc_leExpr(VC vc, Expr left, Expr right)
Expr vc_iteExpr(VC vc, Expr ifpart, Expr thenpart, Expr elsepart)
Type vc_lookupType(VC vc, char *typeName)
Lookup a user-defined (uninterpreted) type by name.
Type vc_recordType2(VC vc, char *field0, Type type0, char *field1, Type type1)
Expr vc_minusExpr(VC vc, Expr left, Expr right)
void vc_deleteString(char *str)
Delete char* returned by previous function.
Expr vc_datatypeSelExpr(VC vc, char *selector, Expr arg)
Datatype selector expression.
Expr vc_orExpr(VC vc, Expr left, Expr right)
Expr vc_bvLtExpr(VC vc, Expr left, Expr right)
Expr vc_stringExpr(VC vc, char *str)
Create a string Expr.
void vc_push(VC vc)
Checkpoint the current context and increase the scope level.
void vc_setResourceLimit(VC vc, unsigned limit)
Set the resource limit (0==unlimited, 1==exhausted).
Expr vc_bvBoolExtract(VC vc, Expr child, int bit_no)