diff options
Diffstat (limited to 'src/bindings/compat/c/c_interface.h')
| -rw-r--r-- | src/bindings/compat/c/c_interface.h | 696 |
1 files changed, 696 insertions, 0 deletions
diff --git a/src/bindings/compat/c/c_interface.h b/src/bindings/compat/c/c_interface.h new file mode 100644 index 000000000..a836e8bca --- /dev/null +++ b/src/bindings/compat/c/c_interface.h @@ -0,0 +1,696 @@ +/*****************************************************************************/ +/*! + * \file c_interface.h + * + * Authors: Clark Barrett + * Cristian Cadar + * + * Created: Thu Jun 5 10:34:02 2003 + * + * <hr> + * + * 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 \ref + * LICENSE file provided with this distribution. + * + * <hr> + * + */ +/*****************************************************************************/ + +#ifndef _cvc3__include__c_interface_h_ +#define _cvc3__include__c_interface_h_ + +#include "c_interface_defs.h" + +//! Flags can be NULL +VC vc_createValidityChecker(Flags flags); +//! Create validity checker's flags +Flags vc_createFlags(); +//! Destroy the validity checker. +/*! Must be called after all other objects are deleted, except the flags */ +void vc_destroyValidityChecker(VC vc); +//! Delete the flags +void vc_deleteFlags(Flags flags); +//! Delete type +void vc_deleteType(Type t); +//! Delete expression +void vc_deleteExpr(Expr e); +//! Delete operator +void vc_deleteOp(Op op); +//! Delete vector of expressions +void vc_deleteVector(Expr* e); +//! Delete vector of types +void vc_deleteTypeVector(Type* e); + +// Setting the flags +//! Set a boolean flag to true or false +void vc_setBoolFlag(Flags flags, char* name, int val); +//! Set an integer flag to the given value +void vc_setIntFlag(Flags flags, char* name, int val); +//! Set a string flag to the given value +void vc_setStringFlag(Flags flags, char* name, char* val); +//! Add a (string, bool) pair to the multy-string flag +void vc_setStrSeqFlag(Flags flags, char* name, char* str, int val); + +// Basic types +Type vc_boolType(VC vc); +Type vc_realType(VC vc); +Type vc_intType(VC vc); + +//! Create a subrange type +Type vc_subRangeType(VC vc, int lowerEnd, int upperEnd); + +//! Creates a subtype defined by the given predicate +/*! + * \param 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). + * + * \param 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 \f$\exists x. pred(x))\f$. + * if the witness check fails, a TypecheckException is thrown. + */ +Type vc_subtypeType(VC vc, Expr pred, Expr witness); + +// Tuple types +Type vc_tupleType2(VC vc, Type type0, Type type1); +Type vc_tupleType3(VC vc, Type type0, Type type1, Type type2); +//! Create a tuple type. 'types' is an array of types of length numTypes. +Type vc_tupleTypeN(VC vc, Type* types, int numTypes); + +// Record types +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); +//! Create a record type. +/*! 'fields' and 'types' are arrays of length numFields. */ +Type vc_recordTypeN(VC vc, char** fields, Type* types, int numFields); + +// Datatypes + +//! 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. */ +Type vc_dataType1(VC vc, char* name, char* constructor, int arity, + 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. */ +Type vc_dataTypeN(VC vc, char* name, 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_dataTypeMN(VC vc, int numTypes, char** names, + int* numCons, char*** constructors, + int** arities, char**** selectors, + Expr*** types); + +//! Create an array type +Type vc_arrayType(VC vc, Type typeIndex, Type typeData); + +//! Create a bitvector type of length n +Type vc_bvType(VC vc, int n); + +//! Create a function type with 1 argument +Type vc_funType1(VC vc, Type a1, Type typeRan); +//! Create a function type with 2 arguments +Type vc_funType2(VC vc, Type a1, Type a2, Type typeRan); +//! Create a function type with 3 arguments +Type vc_funType3(VC vc, Type a1, Type a2, Type a3, Type typeRan); +//! Create a function type with N arguments +Type vc_funTypeN(VC vc, Type* args, Type typeRan, int numArgs); + +// User-defined types + +//! Create an uninterpreted named type +Type vc_createType(VC vc, char* typeName); +//! Lookup a user-defined (uninterpreted) type by name +Type vc_lookupType(VC vc, char* typeName); + +///////////////////////////////////////////////////////////////////////////// +// Expr manipulation methods // +///////////////////////////////////////////////////////////////////////////// + +//! Return the ExprManager +ExprManager* vc_getEM(VC vc); + +//! Create a variable with a given name and type +/*! The type cannot be a function type. */ +Expr vc_varExpr(VC vc, char* name, Type type); + +//! Create a variable with a given name, type, and value +Expr vc_varExprDef(VC vc, char* name, Type type, + Expr def); + +//! 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); + +//! Get the largest supertype of the Expr. +Type vc_getBaseType(VC vc, Expr e); + +//! Get the largest supertype of the Type. +Type vc_getBaseTypeOfType(VC vc, Type t); + +//! Get the subtype predicate +Expr vc_getTypePred(VC vc, Type t, Expr e); + +//! Create a string Expr +Expr vc_stringExpr(VC vc, char* str); + +//! Create an ID Expr +Expr vc_idExpr(VC vc, char* name); + +//! 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); + */ +Expr vc_listExpr(VC vc, int numKids, Expr* kids); + +// Expr I/O +//! Expr vc_parseExpr(VC vc, char* s); +void vc_printExpr(VC vc, Expr e); +//! 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. */ +char* vc_printExprString(VC vc, Expr e); +//! Delete char* returned by previous function +void vc_deleteString(char* str); +//! Print 'e' into an open file descriptor +void vc_printExprFile(VC vc, Expr e, int fd); + +//! 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. + \param vc is the instance to be imported into + \param e is the expression created using a different (not vc) instance + */ +Expr vc_importExpr(VC vc, Expr e); + +//! Import the Type from another instance of VC +/*! \sa vc_importExpr() */ +Type vc_importType(Type t); + +//! Create an equality expression. The two children must have the same type. +Expr vc_eqExpr(VC vc, Expr child0, Expr child1); + +//! Create an all distinct expression. All children must ahve the same type. +Expr vc_distinctExpr(VC vc, Expr* children, int numChildren); + +// Boolean expressions + +// The following functions create Boolean expressions. The children provided +// as arguments must be of type Boolean. +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); + +// Substitution + +// Substitutes oldTerms for newTerms in e. +// This function doesn't actually exist in ValidityChecker interface, +// but it does in Expr, and its functionality is needed in the C interface. +// For consistency, it is represented here as if it were in ValidityChecker. +Expr vc_substExpr(VC vc, Expr e, + Expr* oldTerms, int numOldTerms, + Expr* newTerms, int numNewTerms); + +// User-defined (uninterpreted) functions. + +//! 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. */ +Op vc_createOp(VC vc, char* name, Type type); + +//! Create a named user-defined function with a given type +Op vc_createOpDef(VC vc, char* name, Type type, Expr def); + +//! Lookup an operator by name. +/*! Returns the operator and the type if the operator exists. + * Returns NULL otherwise + */ +Op vc_lookupOp(VC vc, char* name, Type* type); + +//! Create expressions with a user-defined operator. +/*! op must have a function type. */ +Expr vc_funExpr1(VC vc, Op op, Expr child); +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); + +// Arithmetic + +//! Create a rational number with numerator n and denominator d. +/*! d cannot be 0. */ +Expr vc_ratExpr(VC vc, int n, int d); + +//! 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. */ +Expr vc_ratExprFromStr(VC vc, char* n, char* d, int base); + +//! Create a rational from a single string. +/*! + \param n can be a string containing an integer, a pair of integers + "nnn/ddd", or a number in the fixed or floating point format. + \param base is the base in which to interpret the string. +*/ +Expr vc_ratExprFromStr1(VC vc, char* n, int base); + +//! Unary minus. Child must have a numeric type. +Expr vc_uminusExpr(VC vc, Expr child); + +// plus, minus, mult. Children must have numeric types. +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); + +// The following functions create less-than, less-than or equal, +// greater-than, and greater-than or equal expressions of type Boolean. +// Their arguments must be of numeric types. +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); + +// Records + +// Create record literals; +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); + +//! Create an expression representing the selection of a field from a record. +Expr vc_recSelectExpr(VC vc, Expr record, char* field); + +//! Record update; equivalent to "record WITH .field := newValue" +Expr vc_recUpdateExpr(VC vc, Expr record, char* field, Expr newValue); + +// 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); + +// Bitvectors +// Additional type constructor +Type vc_bv32Type(VC vc); + +// Bitvector constants +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); + +// Concat and extract +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); + +// Bitwise Boolean operators: Negation, And, Or, Xor +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); + +// Unsigned bitvector inequalities +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); + +// Signed bitvector inequalities +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); + +// Sign-extend child to a total of nbits bits +Expr vc_bvSignExtend(VC vc, Expr child, int nbits); + +// Bitvector arithmetic: unary minus, plus, subtract, multiply +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); + +// Shift operators +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); + +/*C pointer support: C interface to support C memory arrays in CVC3 */ +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); + +// Tuples + +//! Create a tuple expression +/*! 'children' is an array of elements of length numChildren */ +Expr vc_tupleExprN(VC vc, Expr* children, int numChildren); + +//! Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5) +Expr vc_tupleSelectExpr(VC vc, Expr tuple, int index); + +//! Tuple update; equivalent to "tuple WITH index := newValue" +Expr vc_tupleUpdateExpr(VC vc, Expr tuple, int index, Expr newValue); + +// Datatypes + +//! Datatype constructor expression +Expr vc_datatypeConsExpr(VC vc, char* constructor, int numArgs, Expr* args); + +//! Datatype selector expression +Expr vc_datatypeSelExpr(VC vc, char* selector, Expr arg); + +//! Datatype tester expression +Expr vc_datatypeTestExpr(VC vc, char* constructor, Expr arg); + +// Quantifiers + +//! Create a bound variable. +/*! \param name + * \param uid is a fresh unique string to distinguish this variable + * from other bound variables with the same name + * \param type + */ +Expr vc_boundVarExpr(VC vc, char* name, char *uid, Type type); + +//! Create a FORALL quantifier. +/*! Bvars is an array of bound variables of length numBvars. */ +Type vc_forallExpr(VC vc, Expr* Bvars, int numBvars, Expr f); + +//! Set triggers for a forallExpr +void vc_setTriggers(VC vc, Expr e, int numTrigs, Expr* triggers); + +//! Create an EXISTS quantifier. +/*! Bvars is an array of bound variables of length numBvars. */ +Expr vc_existsExpr(VC vc, Expr* Bvars, int numBvars, Expr f); + +//! Lambda-expression +Op vc_lambdaExpr(VC vc, int numVars, Expr* vars, Expr body); + +///////////////////////////////////////////////////////////////////////////// +// Context-related methods // +///////////////////////////////////////////////////////////////////////////// + +//! Set the resource limit (0==unlimited, 1==exhausted). +/*! Currently, the limit is the total number of processed facts. */ +void vc_setResourceLimit(VC vc, unsigned limit); + +//! Assert a new formula in the current context. +/*! The formula must have Boolean type. */ +void vc_assertFormula(VC vc, Expr e); + +//! 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_registerAtom(VC vc, Expr e); + +//! Return next literal implied by last assertion. Null if none. +/*! Returned literals are either registered atomic formulas or their negation + */ +Expr vc_getImpliedLiteral(VC vc); + +//! Simplify e with respect to the current context +Expr vc_simplify(VC vc, Expr e); + +//! 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. */ +int vc_query(VC vc, Expr e); + +//! Get the next model +/*! This method should only be called after a query which returns + 0. Its return values are as for vc_query(). */ +int vc_checkContinue(VC vc); + +//! 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(). */ +int vc_restart(VC vc, Expr e); + +//! Returns to context immediately before last invalid query. +/*! This method should only be called after a query which returns 0. + */ +void vc_returnFromCheck(VC vc); + +//! 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. + */ +Expr* vc_getUserAssumptions(VC vc, int* size); + +//! 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. + */ +Expr* vc_getInternalAssumptions(VC vc, int* size); + +//! 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. + */ +Expr* vc_getAssumptions(VC vc, int* size); + +//yeting, for proof translation, get the assumptions used. +//the assumptions used are different from the user assumptions. +//the assumptions used are preprocessed if 'preprocess' is ena +Expr vc_getProofAssumptions(VC vc); + +//yeting, for proof translation, +Expr vc_getProofQuery(VC vc); + +//! 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. + */ +Expr* vc_getAssumptionsUsed(VC vc, int* size); + +//! 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. + */ +Expr* vc_getCounterExample(VC vc, int* size); + +//! 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. + */ +Expr* vc_getConcreteModel(VC vc, int* size); + +// Returns true if the current context is inconsistent. +/*! 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_inconsistent(VC vc, Expr** assumptions, int* size); + +//! 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. + */ +char* vc_incomplete(VC vc); + +//! Returns the proof for the last proven query +Expr vc_getProof(VC vc); + +//! Returns the proof of a .cvc file, if it is valid. +Expr vc_getProofOfFile(VC vc, char * filename); + +//! Returns the TCC of the last assumption or query +/*! Returns Null Expr if no assumptions or queries were performed. */ +Expr vc_getTCC(VC vc); + +//! 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. + */ +Expr* vc_getAssumptionsTCC(VC vc, int* size); + +//! Returns the proof of TCC of the last assumption or query +/*! Returns Null Expr if no assumptions or queries were performed. */ +Expr vc_getProofTCC(VC vc); + +//! 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. + */ +Expr vc_getClosure(VC vc); + +//! Construct a proof of the query closure |- Gamma => phi +/*! Returns Null if last query was Invalid. */ +Expr vc_getProofClosure(VC vc); + +//! Returns the current stack level. Initial level is 0. +int vc_stackLevel(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); + +//! Restore the current context to the given stackLevel. +/*! stackLevel must be less than or equal to the current stack level. + */ +void vc_popto(VC vc, int stackLevel); + +//! Get the current context +Context* vc_getCurrentContext(VC vc); + +/* ---------------------------------------------------------------------- */ +/* Util */ +/* ---------------------------------------------------------------------- */ + +// Order + +//! 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 */ +int vc_compare_exprs(Expr e1,Expr e2); + +// Printing + +//! Convert Expr to string +char* vc_exprString(Expr e); +//! Convert Type to string +char* vc_typeString(Type t); + +// What kind of Expr? +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); + +//! Translate a kind int to a string +const char* vc_getKindString(VC vc,int kind); + +//! Translate a kind string to an int +int vc_getKindInt(VC vc,char* kind_name); + +//! Return an int from a rational expression +int vc_getInt(Expr e); + +//! Return an int from a constant bitvector expression +int vc_getBVInt(VC vc, Expr e); +//! Return an unsigned int from a constant bitvector expression +unsigned int vc_getBVUnsigned(VC vc, Expr e); + +// Debug +int vc_get_error_status(); +void vc_reset_error_status(); +char* vc_get_error_string(); + +//! Print statistics +void vc_print_statistics(VC vc); + +#endif + + |