/*****************************************************************************/
/*!
* \file c_interface.h
*
* 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 \ref
* LICENSE file provided with this distribution.
*
*
*
*/
/*****************************************************************************/
#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 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