diff options
Diffstat (limited to 'src/bindings/compat/c')
-rw-r--r-- | src/bindings/compat/c/Makefile | 4 | ||||
-rw-r--r-- | src/bindings/compat/c/Makefile.am | 36 | ||||
-rw-r--r-- | src/bindings/compat/c/c_interface.cpp | 2881 | ||||
-rw-r--r-- | src/bindings/compat/c/c_interface.h | 702 | ||||
-rw-r--r-- | src/bindings/compat/c/c_interface_defs.h | 53 |
5 files changed, 0 insertions, 3676 deletions
diff --git a/src/bindings/compat/c/Makefile b/src/bindings/compat/c/Makefile deleted file mode 100644 index f7b224652..000000000 --- a/src/bindings/compat/c/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../../.. -srcdir = src/bindings/compat/c - -include $(topdir)/Makefile.subdir diff --git a/src/bindings/compat/c/Makefile.am b/src/bindings/compat/c/Makefile.am deleted file mode 100644 index 4ec4626c6..000000000 --- a/src/bindings/compat/c/Makefile.am +++ /dev/null @@ -1,36 +0,0 @@ -# LIBCVC4BINDINGS_VERSION (-version-info) is in the form current:revision:age -# -# current - -# increment if interfaces have been added, removed or changed -# revision - -# increment if source code has changed -# set to zero if current is incremented -# age - -# increment if interfaces have been added -# set to zero if interfaces have been removed -# or changed -# -LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ - -AM_CPPFLAGS = \ - -D__BUILDING_CVC4BINDINGSLIB \ - -I@builddir@/../../.. -I@srcdir@/../../../include -I@srcdir@/../../.. -AM_CXXFLAGS = -Wall -Wno-return-type - -lib_LTLIBRARIES = - -if CVC4_LANGUAGE_BINDING_C - -lib_LTLIBRARIES += libcvc4bindings_c_compat.la -libcvc4bindings_c_compat_la_LDFLAGS = \ - -version-info $(LIBCVC4BINDINGS_VERSION) -libcvc4bindings_c_compat_la_LIBADD = \ - @builddir@/../../../compat/libcvc4compat.la \ - @builddir@/../../../libcvc4.la - -endif - -libcvc4bindings_c_compat_la_SOURCES = \ - c_interface_defs.h \ - c_interface.h \ - c_interface.cpp diff --git a/src/bindings/compat/c/c_interface.cpp b/src/bindings/compat/c/c_interface.cpp deleted file mode 100644 index 8219d5169..000000000 --- a/src/bindings/compat/c/c_interface.cpp +++ /dev/null @@ -1,2881 +0,0 @@ -/*****************************************************************************/ -/*! - * \file c_interface.cpp - * - * 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> - * - */ -/*****************************************************************************/ - - -#include <strings.h> -#include "bindings/compat/c/c_interface_defs.h" -#include "compat/cvc3_compat.h" -//#include "vc.h" -//#include "command_line_flags.h" -//#include "parser.h" -//#include "vc_cmd.h" -//#include "theory_bitvector.h" -//#include "fdstream.h" -#include <string> -#include <cassert> -#include <cerrno> -#include <unistd.h> - -#ifdef CVC4_DEBUG -# define DebugAssert(cond, str) assert(cond) -# define IF_DEBUG(x) x -#else -# define DebugAssert(...) -# define IF_DEBUG(x) -#endif - -using namespace std; - - -// ------------------------------------------------------------------------- -// Debugging -// ------------------------------------------------------------------------- - -// + will mean OK -// - will mean error -int c_interface_error_flag = 1; -const int error_int = -100; -const char* c_interface_error_message = "An Exception Occured: System in a compromised state."; -string c_interface_error_string; -// Used to return char* values. Note that the value is only good until -// the next call to a function returning char* -static string tmpString; - -void signal_error(const char* message,int flag_val,CVC3::Exception ex){ - ostringstream ss; - ss << c_interface_error_message << endl; - ss << "Message: " << message << endl; - ss << "Exception: " << ex << endl; - IF_DEBUG(cerr << ss.str();) - c_interface_error_string = ss.str(); - c_interface_error_flag = flag_val; -} - -extern "C" int vc_get_error_status(){ - return c_interface_error_flag; -} - -extern "C" void vc_reset_error_status(){ - c_interface_error_flag = 1; - c_interface_error_string = ""; -} - -extern "C" char* vc_get_error_string() { - return (char*) (c_interface_error_string.c_str()); -} - - -// Private to implementation - -class CInterface { -public: - static CVC3::Type fromType(Type t); - static Type toType(const CVC3::Type& t); - static CVC3::Expr fromExpr(Expr e); - static Expr toExpr(const CVC3::Expr& e); - static CVC3::Op fromOp(Op op); - static Op toOp(VC vc, const CVC3::Op& op); - // static CVC3::Proof fromProof(Proof proof); - // static Proof toProof(const CVC3::Proof& proof); - static void deleteExpr(Expr e); - static void deleteType(Type t); - static void deleteVector(Expr* vec); -}; - - -CVC3::Type CInterface::fromType(Type t) -{ - return *(CVC3::Type*)t; -} - - -Type CInterface::toType(const CVC3::Type& t) -{ - if(t.isNull()) return NULL; - return Type(new CVC3::Type(t)); -} - - -CVC3::Expr CInterface::fromExpr(Expr e) -{ - return *(CVC3::Expr*)e; -} - - -Expr CInterface::toExpr(const CVC3::Expr& e) -{ - if(e.isNull()) return NULL; - return Expr(new CVC3::Expr(e)); -} - - -CVC3::Op CInterface::fromOp(Op op) -{ - return *(CVC3::Op*)op; -} - - -Op CInterface::toOp(VC vc, const CVC3::Op& op) -{ - if (op.isNull()) return NULL; - return Op(new CVC3::Op(op)); -} - - -// CVC3::Proof CInterface::fromProof(Proof proof) -// { -// return CVC3::Proof(fromExpr(proof)); -// } - - -// Proof CInterface::toProof(const CVC3::Proof& proof) -// { -// return toExpr(proof.getExpr()); -// } - - -void CInterface::deleteExpr(Expr e) -{ - if (e) delete (CVC3::Expr*)e; -} - -void CInterface::deleteType(Type t) -{ - if (t) delete (CVC3::Type*)t; -} - -void CInterface::deleteVector(Expr* e) -{ - if (e) delete [] e; -} - - -static CVC3::Type fromType(Type t) { return CInterface::fromType(t); } -static Type toType(const CVC3::Type& t) { return CInterface::toType(t); } -static CVC3::Expr fromExpr(Expr e) { return CInterface::fromExpr(e); } -static Expr toExpr(const CVC3::Expr& e) { return CInterface::toExpr(e); } -static CVC3::Op fromOp(Op op) { return CInterface::fromOp(op); } -static Op toOp(VC vc, const CVC3::Op& op) { return CInterface::toOp(vc, op); } -// static CVC3::Proof fromProof(Proof proof) { return CInterface::fromProof(proof); } -// static Proof toProof(const CVC3::Proof& proof) { return CInterface::toProof(proof); } - - -static char *val_to_binary_str(unsigned nbits, unsigned long val) { - char s[65]; - - assert(nbits < sizeof s); - strcpy(s, ""); - while(nbits-- > 0) { - if((val >> nbits) & 1) - strcat(s, "1"); - else - strcat(s, "0"); - } - return strdup(s); -} - - -/////////////////////////////////////////////////////////////////////////// -// Begin implementation of C interface // -/////////////////////////////////////////////////////////////////////////// - - -extern "C" VC vc_createValidityChecker(Flags flags) { - try{ - CVC3::CLFlags f = (flags==NULL)? CVC3::ValidityChecker::createFlags() - : *((CVC3::CLFlags*)flags); - return (VC)CVC3::ValidityChecker::create(f); - } catch (CVC3::Exception ex){ - signal_error("vc_createValidityChecker",error_int,ex); - return NULL; - } -} - - -extern "C" Flags vc_createFlags() { - try{ - return new CVC3::CLFlags(CVC3::ValidityChecker::createFlags()); - } catch (CVC3::Exception ex){ - signal_error("vc_createFlags",error_int,ex); - return NULL; - } -} - - -extern "C" void vc_destroyValidityChecker(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - delete cvc; - } catch (CVC3::Exception ex){ - signal_error("vc_destroyVelidityChecker",error_int,ex); - } -} - - -extern "C" void vc_deleteFlags(Flags flags) { - try{ - delete ((CVC3::CLFlags*)flags); - } catch (CVC3::Exception ex){ - signal_error("vc_deleteFlags",error_int,ex); - } -} - - -extern "C" void vc_deleteExpr(Expr e) -{ - try{ - CInterface::deleteExpr(e); - } catch (CVC3::Exception ex){ - signal_error("vc_deleteExpr",error_int,ex); - } -} - - -extern "C" void vc_deleteType(Type t) -{ - try{ - CInterface::deleteType(t); - } catch (CVC3::Exception ex){ - signal_error("vc_deleteType",error_int,ex); - } -} - - -extern "C" void vc_deleteOp(Op op) -{ - vc_deleteExpr(op); -} - - -extern "C" void vc_deleteVector(Expr* e) -{ - try{ - CInterface::deleteVector(e); - } catch (CVC3::Exception ex){ - signal_error("vc_deleteVector",error_int,ex); - } -} - - -extern "C" void vc_deleteTypeVector(Type* e) -{ - vc_deleteVector(e); -} - - -extern "C" void vc_setBoolFlag(Flags flags, char* name, int val) { - try{ - CVC3::CLFlags& f = *((CVC3::CLFlags*)flags); - f.setFlag(name, (val!=0)); - } catch (CVC3::Exception ex){ - signal_error("vc_setBoolFlag",error_int,ex); - } -} - - -extern "C" void vc_setIntFlag(Flags flags, char* name, int val) { - try{ - CVC3::CLFlags& f = *((CVC3::CLFlags*)flags); - f.setFlag(name, val); - } catch (CVC3::Exception ex){ - signal_error("vc_setIntFlag",error_int,ex); - } -} - - -extern "C" void vc_setStringFlag(Flags flags, char* name, char* val) { - try{ - CVC3::CLFlags& f = *((CVC3::CLFlags*)flags); - f.setFlag(name, string(val)); - } catch (CVC3::Exception ex){ - signal_error("vc_setStringFlag",error_int,ex); - } -} - - -extern "C" void vc_setStrSeqFlag(Flags flags, char* name, char* str, int val) { - try{ - CVC3::CLFlags& f = *((CVC3::CLFlags*)flags); - f.setFlag(name, pair<string,bool>(string(str), val!=0)); - } catch (CVC3::Exception ex){ - signal_error("vc_setStrSeqFlag",error_int,ex); - } -} - - -extern "C" Type vc_boolType(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->boolType()); - } catch (CVC3::Exception ex){ - signal_error("vc_boolType",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_realType(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->realType()); - }catch (CVC3::Exception ex){ - signal_error("vc_realType",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_intType(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->intType()); - }catch (CVC3::Exception ex){ - signal_error("vc_intType",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_subRangeType(VC vc, int lowerEnd, int upperEnd) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->subrangeType(cvc->ratExpr(lowerEnd), - cvc->ratExpr(upperEnd))); - }catch (CVC3::Exception &ex){ - signal_error("vc_subRangeType",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_subtypeType(VC vc, Expr pred, Expr witness) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->subtypeType(fromExpr(pred), fromExpr(witness))); - }catch (CVC3::Exception &ex){ - signal_error("vc_subtypeType",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_tupleType2(VC vc, Type type0, Type type1) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->tupleType(fromType(type0), fromType(type1))); - }catch (CVC3::Exception ex){ - signal_error("vc_tupleType2",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_tupleType3(VC vc, Type type0, Type type1, Type type2) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->tupleType(fromType(type0), fromType(type1), - fromType(type2))); - }catch (CVC3::Exception ex){ - signal_error("vc_tupleType3",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_tupleTypeN(VC vc, Type* types, int numTypes) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Type> cvcTypes; - for (int i = 0; i < numTypes; ++i) { - cvcTypes.push_back(fromType(types[i])); - } - return toType(cvc->tupleType(cvcTypes)); - }catch(CVC3::Exception ex){ - signal_error("vc_tupleTypeN",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_recordType1(VC vc, char* field, Type type) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->recordType(field, fromType(type))); - }catch(CVC3::Exception ex){ - signal_error("vc_recordType1",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_recordType2(VC vc, char* field0, Type type0, - char* field1, Type type1) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->recordType(field0, fromType(type0), - field1, fromType(type1))); - }catch(CVC3::Exception ex){ - signal_error("vc_recordType2",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_recordType3(VC vc, char* field0, Type type0, - char* field1, Type type1, - char* field2, Type type2) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->recordType(field0, fromType(type0), - field1, fromType(type1), - field2, fromType(type2))); - }catch(CVC3::Exception ex){ - signal_error("vc_recordType3",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_recordTypeN(VC vc, char** fields, Type* types, - int numFields) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<std::string> cvcFields; - vector<CVC3::Type> cvcTypes; - for (int i = 0; i < numFields; ++i) { - cvcFields.push_back(fields[i]); - cvcTypes.push_back(fromType(types[i])); - } - return toType(cvc->recordType(cvcFields, cvcTypes)); - }catch(CVC3::Exception ex){ - signal_error("vc_recordTypeN",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_dataType1(VC vc, char* name, char* constructor, int arity, - char** selectors, Expr* types) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - string cvcName(name); - string cvcConstructor(constructor); - vector<string> cvcSelectors; - vector<CVC3::Expr> cvcTypes; - for (int i = 0; i < arity; ++i) { - cvcSelectors.push_back(selectors[i]); - cvcTypes.push_back(fromExpr(types[i])); - } - return toType(cvc->dataType(cvcName, cvcConstructor, cvcSelectors, cvcTypes)); - }catch(CVC3::Exception ex){ - signal_error("vc_dataType1",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_dataTypeN(VC vc, char* name, int numCons, char** constructors, - int* arities, char*** selectors, Expr** types) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - string cvcName(name); - vector<string> cvcConstructors; - vector<vector<string> > cvcSelectors(numCons); - vector<vector<CVC3::Expr> > cvcTypes(numCons); - for (int i = 0; i < numCons; ++i) { - cvcConstructors.push_back(constructors[i]); - for (int j = 0; j < arities[i]; ++j) { - cvcSelectors[i].push_back(selectors[i][j]); - cvcTypes[i].push_back(fromExpr(types[i][j])); - } - } - return toType(cvc->dataType(cvcName, cvcConstructors, - cvcSelectors, cvcTypes)); - }catch(CVC3::Exception ex){ - signal_error("vc_dataTypeN",error_int,ex); - return NULL; - } -} - - -extern "C" Type* vc_dataTypeMN(VC vc, int numTypes, char** names, - int* numCons, char*** constructors, - int** arities, char**** selectors, - Expr*** types) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<string> cvcNames; - vector<vector<string> > cvcConstructors(numTypes); - vector<vector<vector<string> > > cvcSelectors(numTypes); - vector<vector<vector<CVC3::Expr> > > cvcTypes(numTypes); - int i; - for (i = 0; i < numTypes; ++i) { - cvcNames.push_back(names[i]); - cvcSelectors[i].resize(numCons[i]); - cvcTypes[i].resize(numCons[i]); - for (int j = 0; i < numCons[i]; ++j) { - cvcConstructors[i].push_back(constructors[i][j]); - for (int k = 0; k < arities[i][j]; ++k) { - cvcSelectors[i][j].push_back(selectors[i][j][k]); - cvcTypes[i][j].push_back(fromExpr(types[i][j][k])); - } - } - } - vector<CVC3::Type> cvcReturnTypes; - cvc->dataType(cvcNames, cvcConstructors, - cvcSelectors, cvcTypes, cvcReturnTypes); - Type* returnTypes = new Type[numTypes]; - for (i = 0; i < numTypes; ++i) { - returnTypes[i] = toType(cvcReturnTypes[i]); - } - return returnTypes; - }catch(CVC3::Exception ex){ - signal_error("vc_dataTypeN",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_arrayType(VC vc, Type typeIndex, Type typeData) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->arrayType(fromType(typeIndex), fromType(typeData))); - }catch(CVC3::Exception ex){ - signal_error("vc_arrayType",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_bvType(VC vc, int n) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->bitvecType(n)); - }catch (CVC3::Exception ex){ - signal_error("vc_bvType",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_funType1(VC vc, Type typeDom, Type typeRan) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->funType(fromType(typeDom), fromType(typeRan))); - }catch(CVC3::Exception ex){ - signal_error("vc_funType1",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_funType2(VC vc, Type a1, Type a2, Type typeRan) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Type> args; - args.push_back(fromType(a1)); - args.push_back(fromType(a2)); - return toType(cvc->funType(args, fromType(typeRan))); - }catch(CVC3::Exception ex){ - signal_error("vc_funType2",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_funType3(VC vc, Type a1, Type a2, Type a3, Type typeRan) -{ - try { - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Type> args; - args.push_back(fromType(a1)); - args.push_back(fromType(a2)); - args.push_back(fromType(a3)); - return toType(cvc->funType(args, fromType(typeRan))); - } catch(CVC3::Exception ex){ - signal_error("vc_funType3",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_funTypeN(VC vc, Type* a, Type typeRan, int numArgs) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Type> args; - for(int i=0; i<numArgs; ++i) - args.push_back(fromType(*(a+i))); - return toType(cvc->funType(args, fromType(typeRan))); - }catch(CVC3::Exception ex){ - signal_error("vc_funTypeN",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_createType(VC vc, char* typeName) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->createType(typeName)); - }catch(CVC3::Exception ex){ - signal_error("vc_createType",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_lookupType(VC vc, char* typeName) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->lookupType(typeName)); - }catch(CVC3::Exception ex){ - signal_error("vc_lookupType",error_int,ex); - return NULL; - } -} - - -///////////////////////////////////////////////////////////////////////////// -// Expr manipulation methods // -///////////////////////////////////////////////////////////////////////////// - - -extern "C" ExprManager vc_getEM(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return (ExprManager)cvc->getEM(); - }catch(CVC3::Exception ex){ - signal_error("vc_getEM",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_varExpr(VC vc, char* name, Type type) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->varExpr(name, fromType(type))); - }catch(CVC3::Exception ex){ - signal_error("vc_varExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_varExprDef(VC vc, char* name, Type type, Expr def) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->varExpr(name, fromType(type), fromExpr(def))); - }catch(CVC3::Exception ex){ - signal_error("vc_varExprDef",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_lookupVar(VC vc, char* name, Type* type) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - CVC3::Type t; - Expr e = toExpr(cvc->lookupVar(name, &t)); - *type = toType(t); - return e; - }catch(CVC3::Exception ex){ - signal_error("vc_lookupVar",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_getType(VC vc, Expr e) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->getType(fromExpr(e))); - }catch(CVC3::Exception ex){ - signal_error("vc_getType",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_getBaseType(VC vc, Expr e) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->getBaseType(fromExpr(e))); - }catch(CVC3::Exception ex){ - signal_error("vc_getBaseType",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_getBaseTypeOfType(VC vc, Type t) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->getBaseType(fromType(t))); - }catch(CVC3::Exception ex){ - signal_error("vc_getBaseTypeOfType",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_getTypePred(VC vc, Type t, Expr e) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->getTypePred(fromType(t), fromExpr(e))); - }catch(CVC3::Exception ex){ - signal_error("vc_getTypePred",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_stringExpr(VC vc, char* str) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->stringExpr(str)); - }catch(CVC3::Exception ex){ - signal_error("vc_stringExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_idExpr(VC vc, char* str) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->idExpr(str)); - }catch(CVC3::Exception ex){ - signal_error("vc_idExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_listExpr(VC vc, int numKids, Expr* kids) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> args; - for(int i=0; i<numKids; ++i) - args.push_back(fromExpr(kids[i])); - return toExpr(cvc->listExpr(args)); - }catch(CVC3::Exception ex){ - signal_error("vc_listExpr",error_int,ex); - return NULL; - } -} - - -extern "C" void vc_printExpr(VC vc, Expr e) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - cvc->printExpr(fromExpr(e)); - }catch(CVC3::Exception ex){ - signal_error("vc_printExpr",error_int,ex); - } -} - - -extern "C" char* vc_printExprString(VC vc, Expr e) -{ - try{ - ostringstream os; - string aa; - char* result; - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - cvc->printExpr(fromExpr(e), os); - os.flush(); - aa=os.str(); - result=new char[aa.length()+1]; - strcpy(result,aa.c_str()); - return result; - } catch(CVC3::Exception ex) { - signal_error("vc_printExprString",error_int,ex); - return NULL; - } -} - - -extern "C" void vc_deleteString(char* str) -{ - if (str) delete [] str; -} - - -extern "C" void vc_printExprFile(VC vc, Expr e, int fd) -{ - try { - stringstream ss; - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - cvc->printExpr(fromExpr(e), ss); - string s = ss.str(); - ssize_t e = write(fd, s.c_str(), s.size()); - if(e < 0) { - IF_DEBUG(cerr << "write() failed, errno == " << errno << endl;) - c_interface_error_string = "write() failed"; - c_interface_error_flag = errno; - } - } catch(CVC3::Exception ex) { - signal_error("vc_printExpr",error_int,ex); - } -} - - -extern "C" Expr vc_importExpr(VC vc, Expr e) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->importExpr(fromExpr(e))); - }catch(CVC3::Exception ex){ - signal_error("vc_importExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_importType(VC vc, Type e) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toType(cvc->importType(fromType(e))); - }catch(CVC3::Exception ex){ - signal_error("vc_importType",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_eqExpr(VC vc, Expr child0, Expr child1) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->eqExpr(fromExpr(child0), fromExpr(child1))); - }catch(CVC3::Exception ex){ - signal_error("vc_eqExpr",error_int,ex); - return NULL; - } -} - -extern "C" Expr vc_distinctExpr(VC vc, Expr* children, int numChildren) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcExprs; - for (int i = 0; i < numChildren; ++i) { - cvcExprs.push_back(fromExpr(children[i])); - } - return toExpr(cvc->distinctExpr(cvcExprs)); - }catch(CVC3::Exception ex){ - signal_error("vc_distinctExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_trueExpr(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->trueExpr()); - }catch(CVC3::Exception ex){ - signal_error("vc_trueExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_falseExpr(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->falseExpr()); - }catch(CVC3::Exception ex){ - signal_error("vc_falseExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_notExpr(VC vc, Expr child) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->notExpr(fromExpr(child))); - }catch(CVC3::Exception ex){ - signal_error("vc_notExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_andExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->andExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_andExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_andExprN(VC vc, Expr* children, int numChildren) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcExprs; - for (int i = 0; i < numChildren; ++i) { - cvcExprs.push_back(fromExpr(children[i])); - } - return toExpr(cvc->andExpr(cvcExprs)); - }catch(CVC3::Exception ex){ - signal_error("vc_andExprN",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_orExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->orExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_orExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_orExprN(VC vc, Expr* children, int numChildren) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcExprs; - for (int i = 0; i < numChildren; ++i) { - cvcExprs.push_back(fromExpr(children[i])); - } - return toExpr(cvc->orExpr(cvcExprs)); - }catch(CVC3::Exception ex){ - signal_error("vc_orExprN",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->impliesExpr(fromExpr(hyp), fromExpr(conc))); - }catch(CVC3::Exception ex){ - signal_error("vc_impliesExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_iffExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->iffExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_iffExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_iteExpr(VC vc, Expr ifpart, Expr thenpart, Expr elsepart) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->iteExpr(fromExpr(ifpart), fromExpr(thenpart), - fromExpr(elsepart))); - }catch(CVC3::Exception ex){ - signal_error("vc_iteExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_substExpr(VC vc, Expr e, - Expr* oldTerms, int numOldTerms, - Expr* newTerms, int numNewTerms) -{ - try{ - vector<CVC3::Expr> oldExprs, newExprs; - CVC3::Expr ex = fromExpr(e); - //CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - for (int i = 0; i < numOldTerms; ++i) { - oldExprs.push_back(fromExpr(oldTerms[i])); - } - for (int i = 0; i < numNewTerms; ++i) { - newExprs.push_back(fromExpr(newTerms[i])); - } - return toExpr(ex.substExpr(oldExprs, newExprs)); - }catch(CVC3::Exception ex){ - signal_error("vc_substExpr",error_int,ex); - return NULL; - } -} - - - -extern "C" Op vc_createOp(VC vc, char* name, Type type) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toOp(vc, cvc->createOp(name, fromType(type))); - }catch(CVC3::Exception ex){ - signal_error("vc_createOp",error_int,ex); - return NULL; - } -} - - -extern "C" Op vc_createOpDef(VC vc, char* name, Type type, Expr def) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toOp(vc, cvc->createOp(name, fromType(type), fromExpr(def))); - }catch(CVC3::Exception ex){ - signal_error("vc_createOpDef",error_int,ex); - return NULL; - } -} - - -extern "C" Op vc_lookupOp(VC vc, char* name, Type* type) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - CVC3::Type t; - Op op = toOp(vc, cvc->lookupOp(name, &t)); - *type = toType(t); - return op; - } catch(CVC3::Exception ex){ - signal_error("vc_lookupOp",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_funExpr1(VC vc, Op op, Expr child) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->funExpr(fromOp(op), fromExpr(child))); - }catch(CVC3::Exception ex){ - signal_error("vc_funExpr1",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_funExpr2(VC vc, Op op, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->funExpr(fromOp(op), fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_funExpr2",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_funExpr3(VC vc, Op op, Expr child0, Expr child1, - Expr child2) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->funExpr(fromOp(op), fromExpr(child0), fromExpr(child1), - fromExpr(child2))); - }catch(CVC3::Exception ex){ - signal_error("vc_funExpr3",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_funExprN(VC vc, Op op, Expr* children, int numChildren) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcExprs; - for (int i = 0; i < numChildren; ++i) { - cvcExprs.push_back(fromExpr(children[i])); - } - return toExpr(cvc->funExpr(fromOp(op), cvcExprs)); - }catch(CVC3::Exception ex){ - signal_error("vc_funExprN",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_ratExpr(VC vc, int n, int d) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->ratExpr(n, d)); - }catch(CVC3::Exception ex){ - signal_error("vc_ratExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_ratExprFromStr(VC vc, char* n, char* d, int base) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->ratExpr(n, d, base)); - }catch(CVC3::Exception ex){ - signal_error("vc_ratExprFromStr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_ratExprFromStr1(VC vc, char* n, int base) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->ratExpr(n, base)); - }catch(CVC3::Exception ex){ - signal_error("vc_ratExprFromStr1",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_uminusExpr(VC vc, Expr child) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->uminusExpr(fromExpr(child))); - }catch(CVC3::Exception ex){ - signal_error("vc_uminusExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_plusExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->plusExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_plusExpr",error_int,ex); - return NULL; - } -} - -extern "C" Expr vc_plusExprN(VC vc, Expr* children, int numChildren) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcExprs; - for (int i = 0; i < numChildren; ++i) { - cvcExprs.push_back(fromExpr(children[i])); - } - return toExpr(cvc->plusExpr(cvcExprs)); - }catch(CVC3::Exception ex){ - signal_error("vc_plusExprN",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_minusExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->minusExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_minusExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_multExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->multExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_multExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_powExpr(VC vc, Expr pow, Expr base) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->powExpr(fromExpr(pow), fromExpr(base))); - }catch(CVC3::Exception ex){ - signal_error("vc_powExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_divideExpr(VC vc, Expr numerator, Expr denominator) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->divideExpr(fromExpr(numerator), fromExpr(denominator))); - }catch(CVC3::Exception ex){ - signal_error("vc_divideExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_ltExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->ltExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_ltExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_leExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->leExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_leExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_gtExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->gtExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_gtExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_geExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->geExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_geExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_recordExpr1(VC vc, char* field, Expr expr) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->recordExpr(field, fromExpr(expr))); - }catch(CVC3::Exception ex){ - signal_error("vc_recordExpr1",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_recordExpr2(VC vc, char* field0, Expr expr0, - char* field1, Expr expr1) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->recordExpr(field0, fromExpr(expr0), - field1, fromExpr(expr1))); - }catch(CVC3::Exception ex){ - signal_error("vc_recordExpr2",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_recordExpr3(VC vc, char* field0, Expr expr0, - char* field1, Expr expr1, - char* field2, Expr expr2) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->recordExpr(field0, fromExpr(expr0), - field1, fromExpr(expr1), - field2, fromExpr(expr2))); - }catch(CVC3::Exception ex){ - signal_error("vc_recordExpr3",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_recordExprN(VC vc, char** fields, Expr* exprs, - int numFields) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<std::string> cvcFields; - vector<CVC3::Expr> cvcExprs; - for (int i = 0; i < numFields; ++i) { - cvcFields.push_back(fields[i]); - cvcExprs.push_back(fromExpr(exprs[i])); - } - return toExpr(cvc->recordExpr(cvcFields, cvcExprs)); - }catch(CVC3::Exception ex){ - signal_error("vc_recordExprN",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_recSelectExpr(VC vc, Expr record, char* field) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->recSelectExpr(fromExpr(record), field)); - }catch(CVC3::Exception ex){ - signal_error("vc_recSelectExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_recUpdateExpr(VC vc, Expr record, char* field, - Expr newValue) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->recUpdateExpr(fromExpr(record), field, - fromExpr(newValue))); - }catch(CVC3::Exception ex){ - signal_error("vc_recUpdateExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_readExpr(VC vc, Expr array, Expr index) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->readExpr(fromExpr(array), fromExpr(index))); - }catch(CVC3::Exception ex){ - signal_error("vc_readExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->writeExpr(fromExpr(array), fromExpr(index), - fromExpr(newValue))); - }catch(CVC3::Exception ex){ - signal_error("vc_writeExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_bv32Type(VC vc) -{ - return vc_bvType(vc, 32); -} - - -extern "C" Expr vc_bvConstExprFromStr(VC vc, char* binary_repr) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->parseExpr(cvc->listExpr("_BVCONST", cvc->stringExpr(binary_repr)))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvConstExpr",error_int, ex); - return NULL; - } -} - - -extern "C" Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value) -{ - char* s = val_to_binary_str(n_bits, value); - return vc_bvConstExprFromStr(vc, s); -} - - -extern "C" Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value) -{ - return vc_bvConstExprFromInt(vc, 32, value); -} - - -extern "C" Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long value) -{ - char* s = val_to_binary_str(n_bits, value); - return vc_bvConstExprFromStr(vc, s); -} - - -extern "C" Expr vc_bvConcatExpr(VC vc, Expr left, Expr right) { - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newConcatExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception &ex){ - signal_error("vc_bvConcatExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvConcatExprN(VC vc, Expr* children, int numChildren) { - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcExprs; - for (int i = 0; i < numChildren; ++i) { - cvcExprs.push_back(fromExpr(children[i])); - } - return toExpr(cvc->newConcatExpr(cvcExprs)); - }catch(CVC3::Exception &ex){ - signal_error("vc_concatExprN",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, int low_bit_no) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVExtractExpr(fromExpr(child), high_bit_no, low_bit_no)); - }catch(CVC3::Exception ex){ - signal_error("vc_bvExtract",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvBoolExtract(VC vc, Expr child, int bit_no) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - CVC3::Expr lExpr = cvc->listExpr("_BOOLEXTRACT", fromExpr(child), cvc->ratExpr(bit_no)); - return toExpr(cvc->parseExpr(lExpr)); - - }catch(CVC3::Exception ex){ - signal_error("vc_bvBoolExtract",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvNotExpr(VC vc, Expr child) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVNegExpr(fromExpr(child))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvNotExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvAndExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVAndExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvAndExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvOrExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVOrExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvOrExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvXorExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVXorExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvXorExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvLtExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVLTExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvLtExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvLeExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVLEExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvLeExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvGtExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - CVC3::Expr lExpr = cvc->listExpr("_BVGT", fromExpr(left), fromExpr(right)); - return toExpr(cvc->parseExpr(lExpr)); - - }catch(CVC3::Exception ex){ - signal_error("vc_bvGtExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvGeExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - CVC3::Expr lExpr = cvc->listExpr("_BVGE", fromExpr(left), fromExpr(right)); - return toExpr(cvc->parseExpr(lExpr)); - - }catch(CVC3::Exception ex){ - signal_error("vc_bvGeExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvSLtExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVSLTExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvSLtExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvSLeExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVSLEExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvSLeExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvSGtExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - CVC3::Expr lExpr = cvc->listExpr("_BVSGT", fromExpr(left), fromExpr(right)); - return toExpr(cvc->parseExpr(lExpr)); - - }catch(CVC3::Exception ex){ - signal_error("vc_bvSGtExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvSGeExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - CVC3::Expr lExpr = cvc->listExpr("_BVSGE", fromExpr(left), fromExpr(right)); - return toExpr(cvc->parseExpr(lExpr)); - - }catch(CVC3::Exception ex){ - signal_error("vc_bvSGeExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvSignExtend(VC vc, Expr child, int nbits) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newSXExpr(fromExpr(child), nbits)); - }catch(CVC3::Exception ex){ - signal_error("vc_bvSignExtend",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvUMinusExpr(VC vc, Expr child) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVUminusExpr(fromExpr(child))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvUMinusExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> args; - args.push_back(fromExpr(left)); - args.push_back(fromExpr(right)); - return toExpr(cvc->newBVPlusExpr(n_bits, args)); - }catch(CVC3::Exception ex){ - signal_error("vc_bvPlusExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right) -{ - return vc_bvPlusExpr(vc, 32, left, right); -} - - -extern "C" Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - CVC3::Expr lExpr = cvc->listExpr("_BVSUB", cvc->ratExpr(n_bits), fromExpr(left), fromExpr(right)); - return toExpr(cvc->parseExpr(lExpr)); - }catch(CVC3::Exception ex){ - signal_error("vc_bvMinusExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right) -{ - return vc_bvMinusExpr(vc, 32, left, right); -} - - -extern "C" Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVMultExpr(n_bits, fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvMultExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bv32MultExpr(VC vc, Expr left, Expr right) -{ - return vc_bvMultExpr(vc, 32, left, right); -} - - -extern "C" Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newFixedLeftShiftExpr(fromExpr(child), sh_amt)); - }catch(CVC3::Exception ex){ - signal_error("vc_bvLeftShiftExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newFixedRightShiftExpr(fromExpr(child), sh_amt)); - }catch(CVC3::Exception ex){ - signal_error("vc_bvRightShiftExpr",error_int,ex); - return NULL; - } -} - -extern "C" Expr vc_bvUDivExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVUDivExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvUDivExpr",error_int,ex); - return NULL; - } -} - -extern "C" Expr vc_bvURemExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVURemExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvURemExpr",error_int,ex); - return NULL; - } -} - -extern "C" Expr vc_bvSDivExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVSDivExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvSDivExpr",error_int,ex); - return NULL; - } -} - -extern "C" Expr vc_bvSRemExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVSRemExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvSRemExpr",error_int,ex); - return NULL; - } -} - -extern "C" Expr vc_bvSModExpr(VC vc, Expr left, Expr right) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->newBVSModExpr(fromExpr(left), fromExpr(right))); - }catch(CVC3::Exception ex){ - signal_error("vc_bvSModExpr",error_int,ex); - return NULL; - } -} - - -/* Same as vc_bvLeftShift only that the answer in 32 bits long */ -extern "C" Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child) { - return vc_bvExtract(vc, vc_bvLeftShiftExpr(vc, sh_amt, child), 31, 0); -} - - -/* Same as vc_bvRightShift only that the answer in 32 bits long */ -extern "C" Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child) { - return vc_bvExtract(vc, vc_bvRightShiftExpr(vc, sh_amt, child), 31, 0); -} - -extern "C" Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child) { - try{ - Expr ifpart; - Expr thenpart; - Expr elsepart = vc_trueExpr(vc); - Expr ite = vc_trueExpr(vc); - - for(int count=32; count >= 0; count--){ - if(count != 32) { - ifpart = vc_eqExpr(vc, sh_amt, - vc_bvConstExprFromInt(vc, 32, count)); - thenpart = vc_bvExtract(vc, - vc_bvLeftShiftExpr(vc, count, child), - 31, 0); - - ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); - elsepart = ite; - } else { - elsepart = vc_bvConstExprFromInt(vc,32, 0); - } - } - return ite; - }catch(CVC3::Exception ex){ - signal_error("vc_bvVar32LeftShiftExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs) { - try{ - Expr ifpart; - Expr thenpart; - Expr elsepart = vc_trueExpr(vc); - Expr ite = vc_trueExpr(vc); - - for(int count=32; count >= 0; count--){ - if(count != 32) { - ifpart = vc_eqExpr(vc, rhs, - vc_bvConstExprFromInt(vc, 32, 1 << count)); - thenpart = vc_bvRightShiftExpr(vc, count, child); - ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); - elsepart = ite; - } else { - elsepart = vc_bvConstExprFromInt(vc,32, 0); - } - } - return ite; - }catch(CVC3::Exception ex){ - signal_error("vc_bvVar32DivByPowOfTwoExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child) -{ - try{ - Expr ifpart; - Expr thenpart; - Expr elsepart = vc_trueExpr(vc); - Expr ite = vc_trueExpr(vc); - - for(int count=32; count >= 0; count--){ - if(count != 32) { - ifpart = vc_eqExpr(vc, sh_amt, - vc_bvConstExprFromInt(vc, 32, count)); - thenpart = vc_bvRightShiftExpr(vc, count, child); - ite = vc_iteExpr(vc,ifpart,thenpart,elsepart); - elsepart = ite; - } else { - elsepart = vc_bvConstExprFromInt(vc,32, 0); - } - } - return ite; - }catch(CVC3::Exception ex){ - signal_error("vc_bvVar32LeftShiftExpr",error_int,ex); - return NULL; - } -} - - -/* C pointer support: C interface to support C memory arrays in CVC3 */ -extern "C" Expr vc_bvCreateMemoryArray(VC vc, char * arrayName) { - Type bv8 = vc_bvType(vc,8); - Type bv32 = vc_bvType(vc,32); - - Type malloced_mem0 = vc_arrayType(vc,bv32,bv8); - return vc_varExpr(vc, arrayName, malloced_mem0); -} - -/*OLD VERSIONS C pointer theory functions. DO NOT DELETE */ - -// //Warning: Type checking needed to ensure that the function is run -// //correctly is not being done. it is assumed that the function -// //recieves inputs of the correct types -// extern "C" Expr vc_bvReadMemoryArray(VC vc, -// Expr array, -// Expr byteIndex, int newBitsPerElem) { -// DebugAssert(newBitsPerElem%8 == 0, -// "new bits per element must be a multiple of 8\n"); - -// Expr numerator = vc_bvMultExpr(vc,32, -// vc_bvConstExprFromInt(vc,32,newBitsPerElem), -// byteIndex); -// int numOfBytes = newBitsPerElem/8; -// DebugAssert(numOfBytes > 0, -// "numOfBytes must be greater than 0"); - -// if(numOfBytes == 1) -// return vc_readExpr(vc,array,numerator); -// else { -// int count = 1; -// Expr a = vc_readExpr(vc,array,numerator); -// while(--numOfBytes > 0) { -// Expr b = vc_readExpr(vc,array, -// vc_bvPlusExpr(vc,32,numerator,vc_bvConstExprFromInt(vc,32,count))); -// a = vc_bvConcatExpr(vc,a,b); -// count++; -// } -// return a; -// } -// } - -// extern "C" Expr vc_bvWriteToMemoryArray(VC vc, -// Expr array, Expr byteIndex, -// Expr element, int newBitsPerElem) { -// DebugAssert(newBitsPerElem%8 == 0, -// "new bits per element must be a multiple of 8\n"); - -// Expr numerator = vc_bvMultExpr(vc,32, -// vc_bvConstExprFromInt(vc,32,newBitsPerElem), -// byteIndex); -// int numOfBytes = newBitsPerElem/8; -// DebugAssert(numOfBytes > 0, -// "numOfBytes must be greater than 0"); - -// if(numOfBytes == 1) -// return vc_writeExpr(vc,array,numerator, element); -// else { -// int count = 1; -// int hi = newBitsPerElem - 1; -// int low = newBitsPerElem - 8; -// Expr c = vc_bvExtract(vc,element,hi,low); -// Expr newarray = vc_writeExpr(vc,array,numerator,c); -// while(--numOfBytes > 0) { -// hi = low-1; -// low = low-8; -// c = vc_bvExtract(vc,element,hi,low); -// newarray = vc_writeExpr(vc,newarray,numerator,c); -// count++; -// } -// return newarray; -// } -// } - - -extern "C" Expr vc_bvReadMemoryArray(VC vc, - Expr array, - Expr byteIndex, int numOfBytes) { - - DebugAssert(0 < numOfBytes, - "number of Bytes must be greater than 0\n"); - - if(numOfBytes == 1) - return vc_readExpr(vc,array,byteIndex); - else { - int count = 1; - Expr a = vc_readExpr(vc,array,byteIndex); - while(--numOfBytes > 0) { - Expr b = vc_readExpr(vc,array, - /*vc_simplify(vc, */ - vc_bvPlusExpr(vc, 32, - byteIndex, - vc_bvConstExprFromInt(vc,32,count)))/*)*/; - a = vc_bvConcatExpr(vc,b,a); - count++; - } - return a; - } -} - - -extern "C" Expr vc_bvWriteToMemoryArray(VC vc, - Expr array, Expr byteIndex, - Expr element, int numOfBytes) { - DebugAssert(numOfBytes > 0, - "numOfBytes must be greater than 0"); - - //int newBitsPerElem = numOfBytes*8; - if(numOfBytes == 1) - return vc_writeExpr(vc, array, byteIndex, element); - else { - int count = 1; - //int hi = newBitsPerElem - 1; - //int low = newBitsPerElem - 8; - int low_elem = 0; - int hi_elem = low_elem + 7; - Expr c = vc_bvExtract(vc, element, hi_elem, low_elem); - Expr newarray = vc_writeExpr(vc, array, byteIndex, c); - while(--numOfBytes > 0) { - //hi = low-1; - //low = low-8; - - low_elem = low_elem + 8; - hi_elem = low_elem + 7; - - c = vc_bvExtract(vc, element, hi_elem, low_elem); - newarray = - vc_writeExpr(vc, newarray, - vc_bvPlusExpr(vc, 32, byteIndex, vc_bvConstExprFromInt(vc,32,count)), - c); - count++; - } - return newarray; - } -} - -extern "C" Expr vc_tupleExprN(VC vc, Expr* children, int numChildren) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcExprs; - for (int i = 0; i < numChildren; ++i) { - cvcExprs.push_back(fromExpr(children[i])); - } - return toExpr(cvc->tupleExpr(cvcExprs)); - }catch(CVC3::Exception ex){ - signal_error("vc_tupleExprN",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_tupleSelectExpr(VC vc, Expr tuple, int index) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->tupleSelectExpr(fromExpr(tuple), index)); - }catch(CVC3::Exception ex){ - signal_error("vc_tupleSelectExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_tupleUpdateExpr(VC vc, Expr tuple, int index, Expr newValue) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->tupleUpdateExpr(fromExpr(tuple), index, - fromExpr(newValue))); - }catch(CVC3::Exception ex){ - signal_error("vc_tupleUpdateExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_datatypeConsExpr(VC vc, char* constructor, - int numArgs, Expr* args) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcArgs; - for (int i = 0; i < numArgs; ++i) { - cvcArgs.push_back(fromExpr(args[i])); - } - return toExpr(cvc->datatypeConsExpr(constructor, cvcArgs)); - }catch(CVC3::Exception ex){ - signal_error("vc_datatypeConsExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_datatypeSelExpr(VC vc, char* selector, Expr arg) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->datatypeSelExpr(selector, fromExpr(arg))); - }catch(CVC3::Exception ex){ - signal_error("vc_datatypeSelExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_datatypeTestExpr(VC vc, char* constructor, Expr arg) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->datatypeTestExpr(constructor, fromExpr(arg))); - }catch(CVC3::Exception ex){ - signal_error("vc_datatypeTestExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_boundVarExpr(VC vc, char* name, char *uid, Type type) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->boundVarExpr(name, uid, fromType(type))); - }catch(CVC3::Exception ex){ - signal_error("vc_getEM",error_int,ex); - return NULL; - } -} - - -extern "C" Type vc_forallExpr(VC vc, Expr* Bvars, int numBvars, Expr f) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcBvars; - for (int i = 0; i < numBvars; ++i) { - cvcBvars.push_back(fromExpr(Bvars[i])); - } - return toExpr(cvc->forallExpr(cvcBvars,fromExpr(f))); - }catch(CVC3::Exception ex){ - signal_error("vc_forallExpr",error_int,ex); - return NULL; - } -} - -// triggers must be an array of listExpr -// each listExpr represent a trigger -// if a listExpr contains more than one Expr, then it is a multi-trigger -extern "C" void vc_setTriggers(VC vc, Expr e, int numTrigs, Expr* triggers) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<vector<CVC3::Expr> >cvcTriggers; - for (int i = 0; i < numTrigs; ++i) { - vector<CVC3::Expr> curTrig; - CVC3::Expr trigExpr = fromExpr(triggers[i]); - if(trigExpr.isRawList()){ - for(int j = 0 ; j < trigExpr.arity(); j++){ - curTrig.push_back(trigExpr[j]); - } - } - else{ - curTrig.push_back(trigExpr); - } - cvcTriggers.push_back(curTrig); - } - - cvc->setTriggers(fromExpr(e), cvcTriggers); - }catch(CVC3::Exception ex){ - signal_error("vc_setTriggers",error_int,ex); - } -} - - -extern "C" Expr vc_existsExpr(VC vc, Expr* Bvars, int numBvars, Expr f) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcBvars; - for (int i = 0; i < numBvars; ++i) { - cvcBvars.push_back(fromExpr(Bvars[i])); - } - return toExpr(cvc->existsExpr(cvcBvars,fromExpr(f))); - }catch(CVC3::Exception ex){ - signal_error("vc_existsExpr",error_int,ex); - return NULL; - } -} - - -extern "C" Op vc_lambdaExpr(VC vc, int numVars, Expr* vars, Expr body) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcVars; - for (int i = 0; i < numVars; ++i) { - cvcVars.push_back(fromExpr(vars[i])); - } - return toOp(vc, cvc->lambdaExpr(cvcVars, fromExpr(body))); - }catch(CVC3::Exception ex){ - signal_error("vc_lambdaExpr",error_int,ex); - return NULL; - } -} - - -///////////////////////////////////////////////////////////////////////////// -// Context-related methods // -///////////////////////////////////////////////////////////////////////////// - - -extern "C" void vc_setResourceLimit(VC vc, unsigned limit) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - cvc->setResourceLimit(limit); - }catch(CVC3::Exception ex){ - signal_error("vc_setResourceLimit",error_int,ex); - } -} - - -extern "C" void vc_assertFormula(VC vc, Expr e) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - cvc->assertFormula(fromExpr(e)); - }catch(CVC3::Exception ex){ - signal_error("vc_assertFormula",error_int,ex); - } -} - - -extern "C" void vc_registerAtom(VC vc, Expr e) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - cvc->registerAtom(fromExpr(e)); - }catch(CVC3::Exception ex){ - signal_error("vc_registerAtom",error_int,ex); - } -} - - -extern "C" Expr vc_getImpliedLiteral(VC vc) -{ - try { - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->getImpliedLiteral()); - } catch(CVC3::Exception ex){ - signal_error("vc_getImpliedLiteral",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_simplify(VC vc, Expr e) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->simplify(fromExpr(e))); - }catch(CVC3::Exception ex){ - signal_error("vc_simplify",error_int,ex); - return NULL; - } -} - - -extern "C" int vc_query(VC vc, Expr e) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return (int)cvc->query(fromExpr(e)); - }catch(CVC3::Exception ex){ - signal_error("vc_query",error_int,ex); - return error_int; - } -} - - -extern "C" int vc_checkContinue(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return (int)cvc->checkContinue(); - }catch(CVC3::Exception ex){ - signal_error("vc_checkContinue",error_int,ex); - return error_int; - } -} - - -extern "C" int vc_restart(VC vc, Expr e) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return (int)cvc->restart(fromExpr(e)); - }catch(CVC3::Exception ex){ - signal_error("vc_restart",error_int,ex); - return error_int; - } -} - - -extern "C" void vc_returnFromCheck(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - cvc->returnFromCheck(); - }catch(CVC3::Exception ex){ - signal_error("vc_returnFromCheck",error_int,ex); - } -} - - -extern "C" Expr* vc_getUserAssumptions(VC vc, int* size) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcAssumptions; - cvc->getUserAssumptions(cvcAssumptions); - Expr* assumptions = new Expr[cvcAssumptions.size()]; - unsigned n = 0; - for (; n < cvcAssumptions.size(); ++n) { - assumptions[n] = toExpr(cvcAssumptions[n]); - } - *size = int(n); - return assumptions; - }catch(CVC3::Exception ex){ - signal_error("vc_getUserAssumptions",error_int,ex); - return NULL; - } -} - - -extern "C" Expr* vc_getInternalAssumptions(VC vc, int* size) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcAssumptions; - cvc->getInternalAssumptions(cvcAssumptions); - Expr* assumptions = new Expr[cvcAssumptions.size()]; - unsigned n = 0; - for (; n < cvcAssumptions.size(); ++n) { - assumptions[n] = toExpr(cvcAssumptions[n]); - } - *size = int(n); - return assumptions; - }catch(CVC3::Exception ex){ - signal_error("vc_getInternalAssumptions",error_int,ex); - return NULL; - } -} - - -extern "C" Expr* vc_getAssumptions(VC vc, int* size) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcAssumptions; - cvc->getAssumptions(cvcAssumptions); - Expr* assumptions = new Expr[cvcAssumptions.size()]; - unsigned n = 0; - for (; n < cvcAssumptions.size(); ++n) { - assumptions[n] = toExpr(cvcAssumptions[n]); - } - *size = int(n); - return assumptions; - }catch(CVC3::Exception ex){ - signal_error("vc_getAssumptions",error_int,ex); - return NULL; - } -} - -//yeting, this is for proof translation, -extern "C" Expr vc_getProofAssumptions(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcAssumptions; - cvc->getUserAssumptions(cvcAssumptions); - return toExpr(cvc->listExpr(cvcAssumptions)); - }catch(CVC3::Exception ex){ - signal_error("vc_getProofAssumptions",error_int,ex); - return NULL; - } -} - -//yeting, this is for proof translation -extern "C" Expr vc_getProofQuery(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->getProofQuery()); - }catch(CVC3::Exception ex){ - signal_error("vc_getProofQuery",error_int,ex); - return NULL; - } -} - - -extern "C" Expr* vc_getAssumptionsUsed(VC vc, int* size) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcAssumptions; - cvc->getAssumptionsUsed(cvcAssumptions); - Expr* assumptions = new Expr[cvcAssumptions.size()]; - unsigned n = 0; - for (; n < cvcAssumptions.size(); ++n) { - assumptions[n] = toExpr(cvcAssumptions[n]); - } - *size = int(n); - return assumptions; - }catch(CVC3::Exception ex){ - signal_error("vc_getAssumptionsUsed",error_int,ex); - return NULL; - } -} - - -extern "C" Expr* vc_getCounterExample(VC vc, int* size) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcAssumptions; - cvc->getCounterExample(cvcAssumptions); - Expr* assumptions = new Expr[cvcAssumptions.size()]; - unsigned n = 0; - for (; n < cvcAssumptions.size(); ++n) { - assumptions[n] = toExpr(cvcAssumptions[n]); - } - *size = int(n); - return assumptions; - }catch(CVC3::Exception ex){ - signal_error("vc_getCounterExample",error_int,ex); - return NULL; - } -} - - -extern "C" Expr* vc_getConcreteModel(VC vc, int* size) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - CVC3::ExprMap<CVC3::Expr> assertions; - cvc->getConcreteModel(assertions); - Expr* locAssumptions = new Expr[assertions.size()]; - int n = 0; - CVC3::ExprMap<CVC3::Expr>::iterator it = assertions.begin(), end = assertions.end(); - for (; it != end; it++) { - locAssumptions[n] = toExpr(cvc->eqExpr(it->first, it->second)); - n++; - } - *size = n; - return locAssumptions; - }catch(CVC3::Exception ex){ - signal_error("vc_getConcreteModel",error_int,ex); - return NULL; - } -} - - -extern "C" int vc_inconsistent(VC vc, Expr** assumptions, int* size) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> assertions; - bool ret = cvc->inconsistent(assertions); - Expr* locAssumptions = new Expr[assertions.size()]; - for (unsigned i = 0; i < assertions.size(); ++i) { - locAssumptions[i] = toExpr(assertions[i]); - } - *assumptions = locAssumptions; - *size = assertions.size(); - return (int)ret; - }catch(CVC3::Exception ex){ - signal_error("vc_inconsistent",error_int,ex); - return 0; - } -} - - -extern "C" char* vc_incomplete(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<string> reasons; - bool ret = cvc->incomplete(reasons); - if (!ret) return NULL; - string allReasons = ""; - for (unsigned i = 0; i < reasons.size(); ++i) { - allReasons += '\n'; - allReasons += reasons[i]; - } - char* retStr = new char[allReasons.length()+1]; - allReasons.copy(retStr, allReasons.length()); - retStr[allReasons.length()] = '\0'; - return retStr; - }catch(CVC3::Exception ex){ - signal_error("vc_incomplete",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_getProof(VC vc) -{ - signal_error("vc_getProofTCC",error_int,CVC3::Exception("Unimplemented")); - return NULL; -} - - -extern "C" Expr vc_getProofOfFile(VC vc, char* fileName){ - signal_error("vc_getProofTCC",error_int,CVC3::Exception("Unimplemented")); - return NULL; -} - - -extern "C" Expr vc_getTCC(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->getTCC()); - }catch(CVC3::Exception ex){ - signal_error("vc_getTCC",error_int,ex); - return NULL; - } -} - - -extern "C" Expr* vc_getAssumptionsTCC(VC vc, int* size) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - vector<CVC3::Expr> cvcAssumptions; - cvc->getAssumptionsTCC(cvcAssumptions); - Expr* assumptions = new Expr[cvcAssumptions.size()]; - unsigned n = 0; - for (; n < cvcAssumptions.size(); ++n) { - assumptions[n] = toExpr(cvcAssumptions[n]); - } - *size = int(n); - return assumptions; - }catch(CVC3::Exception ex){ - signal_error("vc_getAssumptionsTCC",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_getProofTCC(VC vc) -{ - signal_error("vc_getProofTCC",error_int,CVC3::Exception("Unimplemented")); - return NULL; -} - - -extern "C" Expr vc_getClosure(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return toExpr(cvc->getClosure()); - }catch(CVC3::Exception ex){ - signal_error("vc_getClosure",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_getProofClosure(VC vc) -{ - signal_error("vc_getProofTCC",error_int,CVC3::Exception("Unimplemented")); - return NULL; -} - - -extern "C" int vc_stackLevel(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return cvc->stackLevel(); - }catch(CVC3::Exception ex){ - signal_error("vc_stackLevel",error_int,ex); - return 0; - } -} - - -extern "C" void vc_push(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - cvc->push(); - }catch(CVC3::Exception ex){ - signal_error("vc_push",error_int,ex); - } -} - - -extern "C" void vc_pop(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - cvc->pop(); - }catch(CVC3::Exception ex){ - signal_error("vc_pop",error_int,ex); - } -} - - -extern "C" void vc_popto(VC vc, int stackLevel) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - cvc->popto(stackLevel); - }catch(CVC3::Exception ex){ - signal_error("vc_popto",error_int,ex); - } -} - - -extern "C" Context vc_getCurrentContext(VC vc) -{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return (Context)cvc->getCurrentContext(); -} - - -// ------------------------------------------------------------------------- -// Util -// ------------------------------------------------------------------------- - - -extern "C" int vc_compare_exprs(Expr e1,Expr e2){ - try{ - return (compare(fromExpr(e1),fromExpr(e2))); - } catch (CVC3::Exception ex){ - signal_error("vc_compare_exprs",error_int,ex); - return error_int; - } -} - - -extern "C" const char* vc_exprString(Expr e){ - try{ - tmpString =(fromExpr(e)).toString(); - return tmpString.c_str(); - } catch (CVC3::Exception ex){ - signal_error("vc_exprString",error_int,ex); - return "ERROR"; - } -} - - -extern "C" const char* vc_typeString(Type t){ - try{ - tmpString = (fromExpr(t)).toString(); - return tmpString.c_str(); - } catch (CVC3::Exception ex){ - signal_error("vc_typeString",error_int,ex); - return "ERROR"; - } -} - - -extern "C" bool vc_isClosure(Expr e){ - signal_error("vc_isClosure",error_int,CVC3::Exception("Unimplemented")); - return false; -} - - -extern "C" bool vc_isQuantifier(Expr e){ - signal_error("vc_isQuantifier",error_int,CVC3::Exception("Unimplemented")); - return false; -} - - -extern "C" bool vc_isLambda(Expr e){ - signal_error("vc_isLambda",error_int,CVC3::Exception("Unimplemented")); - return false; -} - - -extern "C" bool vc_isVar(Expr e){ - try{ - return (fromExpr(e)).isVar(); - } catch (CVC3::Exception ex){ - signal_error("vc_isVar",error_int,ex); - return false; - } -} - - -extern "C" int vc_arity(Expr e){ - try{ - return (fromExpr(e)).arity(); - } catch (CVC3::Exception ex){ - signal_error("vc_arity",error_int,ex); - return error_int; - } -} - - -extern "C" int vc_getKind(Expr e){ - try{ - return (fromExpr(e)).getKind(); - } catch (CVC3::Exception ex){ - signal_error("vc_getKind",error_int,ex); - return error_int; - } -} - - -extern "C" Expr vc_getChild(Expr e, int i){ - try{ - return toExpr(((fromExpr(e))[i])); - } catch (CVC3::Exception ex){ - signal_error("vc_getChild",error_int,ex); - return NULL; - } -} - - -extern "C" int vc_getNumVars(Expr e){ - signal_error("vc_getNumVars",error_int,CVC3::Exception("Unimplemented")); - return 0; -} - - -extern "C" Expr vc_getVar(Expr e, int i){ - signal_error("vc_getVar",error_int,CVC3::Exception("Unimplemented")); - return 0; -} - - -extern "C" Expr vc_getBody(Expr e){ - signal_error("vc_getBody",error_int,CVC3::Exception("Unimplemented")); - return 0; -} - -extern "C" Expr vc_getExistential(Expr e){ - signal_error("vc_getExistential",error_int,CVC3::Exception("Unimplemented")); - return 0; -} - - -extern "C" Expr vc_getFun(VC vc, Expr e) -{ - try{ - return toExpr((fromExpr(e)).getOp().getExpr()); - }catch(CVC3::Exception ex){ - signal_error("vc_getFun",error_int,ex); - return NULL; - } -} - - -extern "C" Expr vc_toExpr(Type t){ - try{ - return toExpr(fromExpr(t)); - } catch (CVC3::Exception ex){ - signal_error("vc_toExpr",error_int,ex); - return NULL; - } -} - - -extern "C" const char* vc_getKindString(VC vc,int kind) -{ - try{ - tmpString = CVC4::kind::kindToString(CVC4::Kind(kind)); - return tmpString.c_str(); - } catch (CVC3::Exception ex){ - signal_error("vc_getKindString",error_int,ex); - return NULL; - } -} - - -extern "C" int vc_getKindInt(VC vc,char* kind_name) -{ - signal_error("vc_getKindInt",error_int,CVC3::Exception("Unimplemented")); - return 0; -} - - -extern "C" int vc_getInt(Expr e){ - try{ - CVC3::Expr ex = fromExpr(e); - return int(ex.getConst<CVC3::Rational>().getNumerator().getLong()); - } catch (CVC3::Exception ex){ - signal_error("vc_getInt",error_int,ex); - return error_int; - } -} - - -extern "C" int vc_getBVInt(VC vc, Expr e){ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return int(cvc->computeBVConst(fromExpr(e)).getNumerator().getLong()); - } catch (CVC3::Exception ex){ - signal_error("vc_getBVInt",error_int,ex); - return 0; - } -} - - -extern "C" unsigned int vc_getBVUnsigned(VC vc, Expr e){ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - return unsigned(cvc->computeBVConst(fromExpr(e)).getNumerator().getUnsignedLong()); - } catch (CVC3::Exception ex){ - signal_error("vc_getBVUnsigned",error_int,ex); - return 0; - } -} - - -extern "C" void vc_print_statistics(VC vc) -{ - try{ - CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; - cvc->printStatistics(); - } catch (CVC3::Exception ex){ - signal_error("vc_print_statistics",error_int,ex); - } -} diff --git a/src/bindings/compat/c/c_interface.h b/src/bindings/compat/c/c_interface.h deleted file mode 100644 index 379097c27..000000000 --- a/src/bindings/compat/c/c_interface.h +++ /dev/null @@ -1,702 +0,0 @@ -/*****************************************************************************/ -/*! - * \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 - * COPYING file provided with this distribution. - * - * <hr> - * - */ -/*****************************************************************************/ - -#include "cvc4_public.h" - -#ifndef _cvc3__include__c_interface_h_ -#define _cvc3__include__c_interface_h_ - -#include "bindings/compat/c/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 vc the validity checker - * - * \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 vc the validity checker - \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 vc the validity checker - * \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 - - diff --git a/src/bindings/compat/c/c_interface_defs.h b/src/bindings/compat/c/c_interface_defs.h deleted file mode 100644 index 0f0155324..000000000 --- a/src/bindings/compat/c/c_interface_defs.h +++ /dev/null @@ -1,53 +0,0 @@ -/*****************************************************************************/ -/*! - * \file c_interface_defs.h - * - * Author: Clark Barrett - * - * Created: Thu Jun 5 13:16:26 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 - * COPYING file provided with this distribution. - * - * <hr> - * - */ -/*****************************************************************************/ - -#include "cvc4_public.h" - -#ifndef _cvc3__include__c_interface_defs_h_ -#define _cvc3__include__c_interface_defs_h_ - -//#include "kinds.h" - -#ifdef CVC3_STRONG_TYPING - - typedef struct _cvc_VC *VC; - typedef struct _cvc_Context *Context; - typedef struct _cvc_ExprManager *ExprManager; - typedef struct _cvc_Flags *Flags; - - typedef struct _cvc_Expr * Expr; - typedef struct _cvc_Op * Op; - typedef struct _cvc_Type* Type; -#else - - //This gives absolutely no static pointer typing. - typedef void* VC; - typedef void* Context; - typedef void* ExprManager; - typedef void* Flags; - - typedef void* Expr; - typedef void* Op; - typedef void* Type; - typedef void* Proof; - -#endif -#endif - |