cvc4-1.4
|
Go to the source code of this file.
Functions | |
VC | vc_createValidityChecker (Flags flags) |
Flags can be NULL. More... | |
Flags | vc_createFlags () |
Create validity checker's flags. More... | |
void | vc_destroyValidityChecker (VC vc) |
Destroy the validity checker. More... | |
void | vc_deleteFlags (Flags flags) |
Delete the flags. More... | |
void | vc_deleteType (Type t) |
Delete type. More... | |
void | vc_deleteExpr (Expr e) |
Delete expression. More... | |
void | vc_deleteOp (Op op) |
Delete operator. More... | |
void | vc_deleteVector (Expr *e) |
Delete vector of expressions. More... | |
void | vc_deleteTypeVector (Type *e) |
Delete vector of types. More... | |
void | vc_setBoolFlag (Flags flags, char *name, int val) |
Set a boolean flag to true or false. More... | |
void | vc_setIntFlag (Flags flags, char *name, int val) |
Set an integer flag to the given value. More... | |
void | vc_setStringFlag (Flags flags, char *name, char *val) |
Set a string flag to the given value. More... | |
void | vc_setStrSeqFlag (Flags flags, char *name, char *str, int val) |
Add a (string, bool) pair to the multy-string flag. More... | |
Type | vc_boolType (VC vc) |
Type | vc_realType (VC vc) |
Type | vc_intType (VC vc) |
Type | vc_subRangeType (VC vc, int lowerEnd, int upperEnd) |
Create a subrange type. More... | |
Type | vc_subtypeType (VC vc, Expr pred, Expr witness) |
Creates a subtype defined by the given predicate. More... | |
Type | vc_tupleType2 (VC vc, Type type0, Type type1) |
Type | vc_tupleType3 (VC vc, Type type0, Type type1, Type type2) |
Type | vc_tupleTypeN (VC vc, Type *types, int numTypes) |
Create a tuple type. 'types' is an array of types of length numTypes. More... | |
Type | vc_recordType1 (VC vc, char *field, Type type) |
Type | vc_recordType2 (VC vc, char *field0, Type type0, char *field1, Type type1) |
Type | vc_recordType3 (VC vc, char *field0, Type type0, char *field1, Type type1, char *field2, Type type2) |
Type | vc_recordTypeN (VC vc, char **fields, Type *types, int numFields) |
Create a record type. More... | |
Type | vc_dataType1 (VC vc, char *name, char *constructor, int arity, char **selectors, Expr *types) |
Single datatype, single constructor. More... | |
Type | vc_dataTypeN (VC vc, char *name, int numCons, char **constructors, int *arities, char ***selectors, Expr **types) |
Single datatype, multiple constructors. More... | |
Type * | vc_dataTypeMN (VC vc, int numTypes, char **names, int *numCons, char ***constructors, int **arities, char ****selectors, Expr ***types) |
Multiple datatypes. More... | |
Type | vc_arrayType (VC vc, Type typeIndex, Type typeData) |
Create an array type. More... | |
Type | vc_bvType (VC vc, int n) |
Create a bitvector type of length n. More... | |
Type | vc_funType1 (VC vc, Type a1, Type typeRan) |
Create a function type with 1 argument. More... | |
Type | vc_funType2 (VC vc, Type a1, Type a2, Type typeRan) |
Create a function type with 2 arguments. More... | |
Type | vc_funType3 (VC vc, Type a1, Type a2, Type a3, Type typeRan) |
Create a function type with 3 arguments. More... | |
Type | vc_funTypeN (VC vc, Type *args, Type typeRan, int numArgs) |
Create a function type with N arguments. More... | |
Type | vc_createType (VC vc, char *typeName) |
Create an uninterpreted named type. More... | |
Type | vc_lookupType (VC vc, char *typeName) |
Lookup a user-defined (uninterpreted) type by name. More... | |
ExprManager * | vc_getEM (VC vc) |
Return the ExprManager. More... | |
Expr | vc_varExpr (VC vc, char *name, Type type) |
Create a variable with a given name and type. More... | |
Expr | vc_varExprDef (VC vc, char *name, Type type, Expr def) |
Create a variable with a given name, type, and value. More... | |
Expr | vc_lookupVar (VC vc, char *name, Type *type) |
Get the expression and type associated with a name. More... | |
Type | vc_getType (VC vc, Expr e) |
Get the type of the Expr. More... | |
Type | vc_getBaseType (VC vc, Expr e) |
Get the largest supertype of the Expr. More... | |
Type | vc_getBaseTypeOfType (VC vc, Type t) |
Get the largest supertype of the Type. More... | |
Expr | vc_getTypePred (VC vc, Type t, Expr e) |
Get the subtype predicate. More... | |
Expr | vc_stringExpr (VC vc, char *str) |
Create a string Expr. More... | |
Expr | vc_idExpr (VC vc, char *name) |
Create an ID Expr. More... | |
Expr | vc_listExpr (VC vc, int numKids, Expr *kids) |
Create a list Expr. More... | |
void | vc_printExpr (VC vc, Expr e) |
Expr vc_parseExpr(VC vc, char* s);. More... | |
char * | vc_printExprString (VC vc, Expr e) |
Print e into a char*. More... | |
void | vc_deleteString (char *str) |
Delete char* returned by previous function. More... | |
void | vc_printExprFile (VC vc, Expr e, int fd) |
Print 'e' into an open file descriptor. More... | |
Expr | vc_importExpr (VC vc, Expr e) |
Import the Expr from another instance of VC. More... | |
Type | vc_importType (Type t) |
Import the Type from another instance of VC. More... | |
Expr | vc_eqExpr (VC vc, Expr child0, Expr child1) |
Create an equality expression. The two children must have the same type. More... | |
Expr | vc_distinctExpr (VC vc, Expr *children, int numChildren) |
Create an all distinct expression. All children must ahve the same type. More... | |
Expr | vc_trueExpr (VC vc) |
Expr | vc_falseExpr (VC vc) |
Expr | vc_notExpr (VC vc, Expr child) |
Expr | vc_andExpr (VC vc, Expr left, Expr right) |
Expr | vc_andExprN (VC vc, Expr *children, int numChildren) |
Expr | vc_orExpr (VC vc, Expr left, Expr right) |
Expr | vc_orExprN (VC vc, Expr *children, int numChildren) |
Expr | vc_impliesExpr (VC vc, Expr hyp, Expr conc) |
Expr | vc_iffExpr (VC vc, Expr left, Expr right) |
Expr | vc_iteExpr (VC vc, Expr ifpart, Expr thenpart, Expr elsepart) |
Expr | vc_substExpr (VC vc, Expr e, Expr *oldTerms, int numOldTerms, Expr *newTerms, int numNewTerms) |
Op | vc_createOp (VC vc, char *name, Type type) |
Create an operator from a function with a given name and type. More... | |
Op | vc_createOpDef (VC vc, char *name, Type type, Expr def) |
Create a named user-defined function with a given type. More... | |
Op | vc_lookupOp (VC vc, char *name, Type *type) |
Lookup an operator by name. More... | |
Expr | vc_funExpr1 (VC vc, Op op, Expr child) |
Create expressions with a user-defined operator. More... | |
Expr | vc_funExpr2 (VC vc, Op op, Expr left, Expr right) |
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_ratExpr (VC vc, int n, int d) |
Create a rational number with numerator n and denominator d. More... | |
Expr | vc_ratExprFromStr (VC vc, char *n, char *d, int base) |
Create a rational number n/d; n and d are given as strings. More... | |
Expr | vc_ratExprFromStr1 (VC vc, char *n, int base) |
Create a rational from a single string. More... | |
Expr | vc_uminusExpr (VC vc, Expr child) |
Unary minus. Child must have a numeric type. More... | |
Expr | vc_plusExpr (VC vc, Expr left, Expr right) |
Expr | vc_plusExprN (VC vc, Expr *children, int numChildren) |
Expr | vc_minusExpr (VC vc, Expr left, Expr right) |
Expr | vc_multExpr (VC vc, Expr left, Expr right) |
Expr | vc_powExpr (VC vc, Expr pow, Expr base) |
Expr | vc_divideExpr (VC vc, Expr numerator, Expr denominator) |
Expr | vc_ltExpr (VC vc, Expr left, Expr right) |
Expr | vc_leExpr (VC vc, Expr left, Expr right) |
Expr | vc_gtExpr (VC vc, Expr left, Expr right) |
Expr | vc_geExpr (VC vc, Expr left, Expr right) |
Expr | vc_recordExpr1 (VC vc, char *field, Expr expr) |
Expr | vc_recordExpr2 (VC vc, char *field0, Expr expr0, char *field1, Expr expr1) |
Expr | vc_recordExpr3 (VC vc, char *field0, Expr expr0, char *field1, Expr expr1, char *field2, Expr expr2) |
Expr | vc_recordExprN (VC vc, char **fields, Expr *exprs, int numFields) |
Expr | vc_recSelectExpr (VC vc, Expr record, char *field) |
Create an expression representing the selection of a field from a record. More... | |
Expr | vc_recUpdateExpr (VC vc, Expr record, char *field, Expr newValue) |
Record update; equivalent to "record WITH .field := newValue". More... | |
Expr | vc_readExpr (VC vc, Expr array, Expr index) |
Create an expression for the value of array at the given index. More... | |
Expr | vc_writeExpr (VC vc, Expr array, Expr index, Expr newValue) |
Array update; equivalent to "array WITH [index] := newValue". More... | |
Type | vc_bv32Type (VC vc) |
Expr | vc_bvConstExprFromStr (VC vc, char *binary_repr) |
Expr | vc_bvConstExprFromInt (VC vc, int n_bits, unsigned int value) |
Expr | vc_bv32ConstExprFromInt (VC vc, unsigned int value) |
Expr | vc_bvConstExprFromLL (VC vc, int n_bits, unsigned long value) |
Expr | vc_bvConcatExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvConcatExprN (VC vc, Expr *children, int numChildren) |
Expr | vc_bvExtract (VC vc, Expr child, int high_bit_no, int low_bit_no) |
Expr | vc_bvBoolExtract (VC vc, Expr child, int bit_no) |
Expr | vc_bvNotExpr (VC vc, Expr child) |
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_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_bvSLtExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvSLeExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvSGtExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvSGeExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvSignExtend (VC vc, Expr child, int nbits) |
Expr | vc_bvUMinusExpr (VC vc, Expr child) |
Expr | vc_bvPlusExpr (VC vc, int n_bits, Expr left, Expr right) |
Expr | vc_bv32PlusExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvMinusExpr (VC vc, int n_bits, Expr left, Expr right) |
Expr | vc_bv32MinusExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvMultExpr (VC vc, int n_bits, Expr left, Expr right) |
Expr | vc_bv32MultExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvUDivExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvURemExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvSDivExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvSRemExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvSModExpr (VC vc, Expr left, Expr right) |
Expr | vc_bvLeftShiftExpr (VC vc, int sh_amt, Expr child) |
Expr | vc_bvRightShiftExpr (VC vc, int sh_amt, Expr child) |
Expr | vc_bv32LeftShiftExpr (VC vc, int sh_amt, Expr child) |
Expr | vc_bv32RightShiftExpr (VC vc, int sh_amt, Expr child) |
Expr | vc_bvVar32LeftShiftExpr (VC vc, Expr sh_amt, Expr child) |
Expr | vc_bvVar32RightShiftExpr (VC vc, Expr sh_amt, Expr child) |
Expr | vc_bvVar32DivByPowOfTwoExpr (VC vc, Expr child, Expr rhs) |
Expr | vc_bvCreateMemoryArray (VC vc, char *arrayName) |
Expr | vc_bvReadMemoryArray (VC vc, Expr array, Expr byteIndex, int numOfBytes) |
Expr | vc_bvWriteToMemoryArray (VC vc, Expr array, Expr byteIndex, Expr element, int numOfBytes) |
Expr | vc_tupleExprN (VC vc, Expr *children, int numChildren) |
Create a tuple expression. More... | |
Expr | vc_tupleSelectExpr (VC vc, Expr tuple, int index) |
Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5) More... | |
Expr | vc_tupleUpdateExpr (VC vc, Expr tuple, int index, Expr newValue) |
Tuple update; equivalent to "tuple WITH index := newValue". More... | |
Expr | vc_datatypeConsExpr (VC vc, char *constructor, int numArgs, Expr *args) |
Datatype constructor expression. More... | |
Expr | vc_datatypeSelExpr (VC vc, char *selector, Expr arg) |
Datatype selector expression. More... | |
Expr | vc_datatypeTestExpr (VC vc, char *constructor, Expr arg) |
Datatype tester expression. More... | |
Expr | vc_boundVarExpr (VC vc, char *name, char *uid, Type type) |
Create a bound variable. More... | |
Type | vc_forallExpr (VC vc, Expr *Bvars, int numBvars, Expr f) |
Create a FORALL quantifier. More... | |
void | vc_setTriggers (VC vc, Expr e, int numTrigs, Expr *triggers) |
Set triggers for a forallExpr. More... | |
Expr | vc_existsExpr (VC vc, Expr *Bvars, int numBvars, Expr f) |
Create an EXISTS quantifier. More... | |
Op | vc_lambdaExpr (VC vc, int numVars, Expr *vars, Expr body) |
Lambda-expression. More... | |
void | vc_setResourceLimit (VC vc, unsigned limit) |
Set the resource limit (0==unlimited, 1==exhausted). More... | |
void | vc_assertFormula (VC vc, Expr e) |
Assert a new formula in the current context. More... | |
void | vc_registerAtom (VC vc, Expr e) |
Register an atomic formula of interest. More... | |
Expr | vc_getImpliedLiteral (VC vc) |
Return next literal implied by last assertion. Null if none. More... | |
Expr | vc_simplify (VC vc, Expr e) |
Simplify e with respect to the current context. More... | |
int | vc_query (VC vc, Expr e) |
Check validity of e in the current context. More... | |
int | vc_checkContinue (VC vc) |
Get the next model. More... | |
int | vc_restart (VC vc, Expr e) |
Restart the most recent query with e as an additional assertion. More... | |
void | vc_returnFromCheck (VC vc) |
Returns to context immediately before last invalid query. More... | |
Expr * | vc_getUserAssumptions (VC vc, int *size) |
Get assumptions made by the user in this and all previous contexts. More... | |
Expr * | vc_getInternalAssumptions (VC vc, int *size) |
Get assumptions made internally in this and all previous contexts. More... | |
Expr * | vc_getAssumptions (VC vc, int *size) |
Get all assumptions made in this and all previous contexts. More... | |
Expr | vc_getProofAssumptions (VC vc) |
Expr | vc_getProofQuery (VC vc) |
Expr * | vc_getAssumptionsUsed (VC vc, int *size) |
Returns the set of assumptions used in the proof of queried formula. More... | |
Expr * | vc_getCounterExample (VC vc, int *size) |
Return the counterexample after a failed query. More... | |
Expr * | vc_getConcreteModel (VC vc, int *size) |
Will assign concrete values to all user created variables. More... | |
int | vc_inconsistent (VC vc, Expr **assumptions, int *size) |
char * | vc_incomplete (VC vc) |
Returns non-NULL if the invalid result from last query() is imprecise. More... | |
Expr | vc_getProof (VC vc) |
Returns the proof for the last proven query. More... | |
Expr | vc_getProofOfFile (VC vc, char *filename) |
Returns the proof of a .cvc file, if it is valid. More... | |
Expr | vc_getTCC (VC vc) |
Returns the TCC of the last assumption or query. More... | |
Expr * | vc_getAssumptionsTCC (VC vc, int *size) |
Return the set of assumptions used in the proof of the last TCC. More... | |
Expr | vc_getProofTCC (VC vc) |
Returns the proof of TCC of the last assumption or query. More... | |
Expr | vc_getClosure (VC vc) |
After successful query, return its closure |- Gamma => phi. More... | |
Expr | vc_getProofClosure (VC vc) |
Construct a proof of the query closure |- Gamma => phi. More... | |
int | vc_stackLevel (VC vc) |
Returns the current stack level. Initial level is 0. More... | |
void | vc_push (VC vc) |
Checkpoint the current context and increase the scope level. More... | |
void | vc_pop (VC vc) |
Restore the current context to its state at the last checkpoint. More... | |
void | vc_popto (VC vc, int stackLevel) |
Restore the current context to the given stackLevel. More... | |
Context * | vc_getCurrentContext (VC vc) |
Get the current context. More... | |
int | vc_compare_exprs (Expr e1, Expr e2) |
Compares two expressions. More... | |
char * | vc_exprString (Expr e) |
Convert Expr to string. More... | |
char * | vc_typeString (Type t) |
Convert Type to string. More... | |
int | vc_isClosure (Expr e) |
int | vc_isQuantifier (Expr e) |
int | vc_isLambda (Expr e) |
Expr | vc_isVar (Expr e) |
int | vc_arity (Expr e) |
int | vc_getKind (Expr e) |
Expr | vc_getChild (Expr e, int i) |
int | vc_getNumVars (Expr e) |
Expr | vc_getVar (Expr e, int i) |
Expr | vc_getBody (Expr e) |
Expr | vc_getExistential (Expr e) |
Expr | vc_getFun (VC vc, Expr e) |
Expr | vc_toExpr (Type t) |
const char * | vc_getKindString (VC vc, int kind) |
Translate a kind int to a string. More... | |
int | vc_getKindInt (VC vc, char *kind_name) |
Translate a kind string to an int. More... | |
int | vc_getInt (Expr e) |
Return an int from a rational expression. More... | |
int | vc_getBVInt (VC vc, Expr e) |
Return an int from a constant bitvector expression. More... | |
unsigned int | vc_getBVUnsigned (VC vc, Expr e) |
Return an unsigned int from a constant bitvector expression. More... | |
int | vc_get_error_status () |
void | vc_reset_error_status () |
char * | vc_get_error_string () |
void | vc_print_statistics (VC vc) |
Print statistics. More... | |
Authors: Clark Barrett Cristian Cadar
Created: Thu Jun 5 10:34:02 2003
License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the COPYING file provided with this distribution.
Definition in file c_interface.h.
int vc_arity | ( | Expr | e | ) |
Assert a new formula in the current context.
The formula must have Boolean type.
Create a bound variable.
vc | the validity checker |
name | |
uid | is a fresh unique string to distinguish this variable from other bound variables with the same name |
type |
int vc_checkContinue | ( | VC | vc | ) |
Get the next model.
This method should only be called after a query which returns 0. Its return values are as for vc_query().
Compares two expressions.
If e1 < e2, e1==e2, and e1 > e2, it returns -1, 0, 1 respectively. A return value of -100 signals an error (refer to vc_get_error_string() for details).
Can't be 'compare' because already defined in ocaml
Flags vc_createFlags | ( | ) |
Create validity checker's flags.
Create an operator from a function with a given name and type.
Name is given as an ID Expr, and the type must be a function type.
Create a named user-defined function with a given type.
Type vc_dataType1 | ( | VC | vc, |
char * | name, | ||
char * | constructor, | ||
int | arity, | ||
char ** | selectors, | ||
Expr * | types | ||
) |
Single datatype, single constructor.
The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined.
Datatype constructor expression.
Type* vc_dataTypeMN | ( | VC | vc, |
int | numTypes, | ||
char ** | names, | ||
int * | numCons, | ||
char *** | constructors, | ||
int ** | arities, | ||
char **** | selectors, | ||
Expr *** | types | ||
) |
Multiple datatypes.
The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined. Returns an array of size numTypes which must be freed by calling vc_deleteTypeVector.
Type vc_dataTypeN | ( | VC | vc, |
char * | name, | ||
int | numCons, | ||
char ** | constructors, | ||
int * | arities, | ||
char *** | selectors, | ||
Expr ** | types | ||
) |
Single datatype, multiple constructors.
The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined.
void vc_deleteExpr | ( | Expr | e | ) |
Delete expression.
void vc_deleteFlags | ( | Flags | flags | ) |
Delete the flags.
void vc_deleteOp | ( | Op | op | ) |
Delete operator.
void vc_deleteString | ( | char * | str | ) |
Delete char* returned by previous function.
void vc_deleteType | ( | Type | t | ) |
Delete type.
void vc_deleteTypeVector | ( | Type * | e | ) |
Delete vector of types.
void vc_deleteVector | ( | Expr * | e | ) |
Delete vector of expressions.
void vc_destroyValidityChecker | ( | VC | vc | ) |
Destroy the validity checker.
Must be called after all other objects are deleted, except the flags
Create an all distinct expression. All children must ahve the same type.
Create an equality expression. The two children must have the same type.
Create an EXISTS quantifier.
Bvars is an array of bound variables of length numBvars.
char* vc_exprString | ( | Expr | e | ) |
Convert Expr to string.
Create a FORALL quantifier.
Bvars is an array of bound variables of length numBvars.
Create expressions with a user-defined operator.
op must have a function type.
Create a function type with 3 arguments.
Create a function type with N arguments.
int vc_get_error_status | ( | ) |
char* vc_get_error_string | ( | ) |
Get all assumptions made in this and all previous contexts.
The caller is responsible for freeing the array when finished with it by calling vc_deleteVector.
Return the set of assumptions used in the proof of the last TCC.
The caller is responsible for freeing the array when finished with it by calling vc_deleteVector.
Returns the set of assumptions used in the proof of queried formula.
It returns a subset of getAssumptions(). If the last query was false or there has not yet been a query, it does nothing. The caller is responsible for freeing the array when finished with it by calling vc_deleteVector.
Return an unsigned int from a constant bitvector expression.
After successful query, return its closure |- Gamma => phi.
Turn a valid query Gamma |- phi into an implication |- Gamma => phi.
Returns Null Expr if last query was invalid.
Will assign concrete values to all user created variables.
This function should only be called after a query which return false. Returns an array of Exprs with size *size. The caller is responsible for freeing the array when finished with it by calling vc_deleteVector.
Return the counterexample after a failed query.
This method should only be called after a query which returns false. It will try to return the simplest possible set of assertions which are sufficient to make the queried expression false. The caller is responsible for freeing the array when finished with it by calling vc_deleteVector.
ExprManager* vc_getEM | ( | VC | vc | ) |
Return the ExprManager.
Return next literal implied by last assertion. Null if none.
Returned literals are either registered atomic formulas or their negation
int vc_getInt | ( | Expr | e | ) |
Return an int from a rational expression.
Get assumptions made internally in this and all previous contexts.
Internal assumptions are literals assumed by the sat solver. The caller is responsible for freeing the array when finished with it by calling vc_deleteVector.
int vc_getKind | ( | Expr | e | ) |
int vc_getKindInt | ( | VC | vc, |
char * | kind_name | ||
) |
Translate a kind string to an int.
const char* vc_getKindString | ( | VC | vc, |
int | kind | ||
) |
Translate a kind int to a string.
int vc_getNumVars | ( | Expr | e | ) |
Construct a proof of the query closure |- Gamma => phi.
Returns Null if last query was Invalid.
Returns the proof of TCC of the last assumption or query.
Returns Null Expr if no assumptions or queries were performed.
Returns the TCC of the last assumption or query.
Returns Null Expr if no assumptions or queries were performed.
Get assumptions made by the user in this and all previous contexts.
User assumptions are created either by calls to assertFormula or by a call to query. In the latter case, the negated query is added as an assumption. The caller is responsible for freeing the array when finished with it.
Import the Expr from another instance of VC.
When expressions need to be passed among several instances of VC, they need to be explicitly imported into the corresponding instance using this method. The return result is an identical expression that belongs to the current instance of VC, and can be safely used as part of more complex expressions from the same instance.
vc | is the instance to be imported into |
e | is the expression created using a different (not vc) instance |
Import the Type from another instance of VC.
char* vc_incomplete | ( | VC | vc | ) |
Returns non-NULL if the invalid result from last query() is imprecise.
The return value is filled with the reasons for incompleteness (it is intended to be shown to the end user). The caller is responsible for freeing the string returned by calling vc_deleteString.
Also returns a minimal set of assertions used to determine the inconsistency. The caller is responsible for freeing the array when finished with it by calling vc_deleteVector.
int vc_isClosure | ( | Expr | e | ) |
int vc_isLambda | ( | Expr | e | ) |
int vc_isQuantifier | ( | Expr | e | ) |
Create a list Expr.
Intermediate representation for DP-specific expressions. Normally, the first element of the list is a string Expr representing an operator, and the rest of the list are the arguments. For example,
kids.push_back(vc->stringExpr("PLUS")); kids.push_back(x); // x and y are previously created Exprs kids.push_back(y); Expr lst = vc->listExpr(kids);
Or, alternatively (using its overloaded version):
Expr lst = vc->listExpr("PLUS", x, y);
or
vector<Expr> summands; summands.push_back(x); summands.push_back(y); ... Expr lst = vc->listExpr("PLUS", summands);
Lookup an operator by name.
Returns the operator and the type if the operator exists. Returns NULL otherwise
Get the expression and type associated with a name.
If there is no such Expr, a NULL Expr is returned.
void vc_pop | ( | VC | vc | ) |
Restore the current context to its state at the last checkpoint.
void vc_popto | ( | VC | vc, |
int | stackLevel | ||
) |
Restore the current context to the given stackLevel.
stackLevel must be less than or equal to the current stack level.
void vc_print_statistics | ( | VC | vc | ) |
Print statistics.
Print e into a char*.
Note that the ownership of the char* is given to the caller which should free the memory when it is done with it. This can be done by calling vc_deleteString.
void vc_push | ( | VC | vc | ) |
Checkpoint the current context and increase the scope level.
Check validity of e in the current context.
Possible results are: 0 = invalid, 1 = valid, 2 = abort, 3 = unknown, -100 = exception (type error, internal error, etc). If the result is 1, then the resulting context is the same as the starting context. If the result is 0 or 3, then the resulting context is a context in which e is false (though the context may be inconsistent in the case of an unknown result). e must have Boolean type. In the case of a result of -100, refer to vc_get_error_string() to see what went wrong.
Create a rational number with numerator n and denominator d.
d cannot be 0.
Create a rational number n/d; n and d are given as strings.
n and d are converted to arbitrary-precision integers according to the given base. d cannot be 0.
Create a rational from a single string.
vc | the validity checker |
n | can be a string containing an integer, a pair of integers "nnn/ddd", or a number in the fixed or floating point format. |
base | is the base in which to interpret the string. |
Create an expression for the value of array at the given index.
Expr vc_recordExpr3 | ( | VC | vc, |
char * | field0, | ||
Expr | expr0, | ||
char * | field1, | ||
Expr | expr1, | ||
char * | field2, | ||
Expr | expr2 | ||
) |
Type vc_recordType3 | ( | VC | vc, |
char * | field0, | ||
Type | type0, | ||
char * | field1, | ||
Type | type1, | ||
char * | field2, | ||
Type | type2 | ||
) |
Create a record type.
'fields' and 'types' are arrays of length numFields.
Create an expression representing the selection of a field from a record.
Record update; equivalent to "record WITH .field := newValue".
Register an atomic formula of interest.
Registered atoms are tracked by the decision procedures. If one of them is deduced to be true or false, it is added to a list of implied literals. Implied literals can be retrieved with the getImpliedLiteral function
void vc_reset_error_status | ( | ) |
Restart the most recent query with e as an additional assertion.
This method should only be called after a query which returns 0. Its return values are as for vc_query().
void vc_returnFromCheck | ( | VC | vc | ) |
Returns to context immediately before last invalid query.
This method should only be called after a query which returns 0.
void vc_setBoolFlag | ( | Flags | flags, |
char * | name, | ||
int | val | ||
) |
Set a boolean flag to true or false.
void vc_setIntFlag | ( | Flags | flags, |
char * | name, | ||
int | val | ||
) |
Set an integer flag to the given value.
void vc_setResourceLimit | ( | VC | vc, |
unsigned | limit | ||
) |
Set the resource limit (0==unlimited, 1==exhausted).
Currently, the limit is the total number of processed facts.
void vc_setStringFlag | ( | Flags | flags, |
char * | name, | ||
char * | val | ||
) |
Set a string flag to the given value.
void vc_setStrSeqFlag | ( | Flags | flags, |
char * | name, | ||
char * | str, | ||
int | val | ||
) |
Add a (string, bool) pair to the multy-string flag.
int vc_stackLevel | ( | VC | vc | ) |
Returns the current stack level. Initial level is 0.
Expr vc_substExpr | ( | VC | vc, |
Expr | e, | ||
Expr * | oldTerms, | ||
int | numOldTerms, | ||
Expr * | newTerms, | ||
int | numNewTerms | ||
) |
Creates a subtype defined by the given predicate.
vc | the validity checker |
pred | is a predicate taking one argument of type T and returning Boolean. The resulting type is a subtype of T whose elements x are those satisfying the predicate pred(x). |
witness | is an expression of type T for which pred holds (if a Null expression is passed as a witness, cvc will try to prove ![]() |
Create a tuple expression.
'children' is an array of elements of length numChildren
Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5)
Create a tuple type. 'types' is an array of types of length numTypes.
Tuple update; equivalent to "tuple WITH index := newValue".
char* vc_typeString | ( | Type | t | ) |
Convert Type to string.
Create a variable with a given name and type.
The type cannot be a function type.
Create a variable with a given name, type, and value.