From: Morgan Deters Date: Tue, 27 Sep 2011 00:34:30 +0000 (+0000) Subject: more interface work; adding legacy C interface X-Git-Tag: cvc5-1.0.0~8457 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d529e4c065d880f5fdf6e10cb0996a45e739bb51;p=cvc5.git more interface work; adding legacy C interface --- diff --git a/config/bindings.m4 b/config/bindings.m4 index 5758518ef..f47490fec 100644 --- a/config/bindings.m4 +++ b/config/bindings.m4 @@ -2,7 +2,7 @@ # ----------------------- # Supported language bindings for CVC4. AC_DEFUN([CVC4_SUPPORTED_BINDINGS], -[java,csharp,perl,php,python,ruby,tcl,ocaml]) +[c,java,csharp,perl,php,python,ruby,tcl,ocaml]) # CVC4_CHECK_BINDINGS(DEFAULT_BINDINGS_LIST) # ------------------------------------------ @@ -33,7 +33,7 @@ if test "$noswig" = yes; then fi else if test -z "$SWIG"; then - AC_CHECK_PROGS(SWIG, swig, swig, []) + AC_CHECK_PROGS(SWIG, [swig swig2.0], swig, []) else AC_CHECK_PROG(SWIG, "$SWIG", "$SWIG", []) fi @@ -54,7 +54,11 @@ else binding_error=no AC_MSG_CHECKING([for availability of $binding binding]) case "$binding" in - c++) AC_MSG_RESULT([C++ is built by default]);; + c++) + AC_MSG_RESULT([C++ is built by default]);; + c) + cvc4_build_c_bindings=yes + AC_MSG_RESULT([C support will be built]);; java) cvc4_build_java_bindings=yes AC_MSG_RESULT([Java support will be built]);; diff --git a/src/bindings/compat/Makefile.am b/src/bindings/compat/Makefile.am index bd20da5b8..e5ea3b399 100644 --- a/src/bindings/compat/Makefile.am +++ b/src/bindings/compat/Makefile.am @@ -4,6 +4,6 @@ AM_CPPFLAGS = \ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) if CVC4_BUILD_LIBCOMPAT -SUBDIRS = java +SUBDIRS = c java endif diff --git a/src/bindings/compat/c/Makefile b/src/bindings/compat/c/Makefile new file mode 100644 index 000000000..f7b224652 --- /dev/null +++ b/src/bindings/compat/c/Makefile @@ -0,0 +1,4 @@ +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 new file mode 100644 index 000000000..ceabe16db --- /dev/null +++ b/src/bindings/compat/c/Makefile.am @@ -0,0 +1,35 @@ +# 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@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. +AM_CXXFLAGS = -Wall -Wno-return-type $(FLAG_VISIBILITY_HIDDEN) + +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 = \ + -L@builddir@/../../../compat -lcvc4compat + +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 new file mode 100644 index 000000000..58fb70dcb --- /dev/null +++ b/src/bindings/compat/c/c_interface.cpp @@ -0,0 +1,2870 @@ +/*****************************************************************************/ +/*! + * \file c_interface.cpp + * + * Authors: Clark Barrett + * Cristian Cadar + * + * Created: Thu Jun 5 10:34:02 2003 + * + *
+ * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + *
+ * + */ +/*****************************************************************************/ + + +#include +#include "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 + + +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(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 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 cvcFields; + vector 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 cvcSelectors; + vector 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 cvcConstructors; + vector > cvcSelectors(numCons); + vector > 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 cvcNames; + vector > cvcConstructors(numTypes); + vector > > cvcSelectors(numTypes); + vector > > 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 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 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 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 args; + for(int i=0; ifunType(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 args; + for(int i=0; ilistExpr(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(); + write(fd, s.c_str(), s.size()); + } 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 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 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 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 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 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 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 cvcFields; + vector 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 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 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 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 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 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 >cvcTriggers; + for (int i = 0; i < numTrigs; ++i) { + vector 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 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 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 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 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 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 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 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 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 assertions; + cvc->getConcreteModel(assertions); + Expr* locAssumptions = new Expr[assertions.size()]; + int n = 0; + CVC3::ExprMap::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 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 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 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); + if(ex.getKind() == CVC4::kind::CONST_INTEGER) { + return int(ex.getConst().getLong()); + } else { + return int(ex.getConst().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 new file mode 100644 index 000000000..a836e8bca --- /dev/null +++ b/src/bindings/compat/c/c_interface.h @@ -0,0 +1,696 @@ +/*****************************************************************************/ +/*! + * \file c_interface.h + * + * Authors: Clark Barrett + * Cristian Cadar + * + * Created: Thu Jun 5 10:34:02 2003 + * + *
+ * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + *
+ * + */ +/*****************************************************************************/ + +#ifndef _cvc3__include__c_interface_h_ +#define _cvc3__include__c_interface_h_ + +#include "c_interface_defs.h" + +//! Flags can be NULL +VC vc_createValidityChecker(Flags flags); +//! Create validity checker's flags +Flags vc_createFlags(); +//! Destroy the validity checker. +/*! Must be called after all other objects are deleted, except the flags */ +void vc_destroyValidityChecker(VC vc); +//! Delete the flags +void vc_deleteFlags(Flags flags); +//! Delete type +void vc_deleteType(Type t); +//! Delete expression +void vc_deleteExpr(Expr e); +//! Delete operator +void vc_deleteOp(Op op); +//! Delete vector of expressions +void vc_deleteVector(Expr* e); +//! Delete vector of types +void vc_deleteTypeVector(Type* e); + +// Setting the flags +//! Set a boolean flag to true or false +void vc_setBoolFlag(Flags flags, char* name, int val); +//! Set an integer flag to the given value +void vc_setIntFlag(Flags flags, char* name, int val); +//! Set a string flag to the given value +void vc_setStringFlag(Flags flags, char* name, char* val); +//! Add a (string, bool) pair to the multy-string flag +void vc_setStrSeqFlag(Flags flags, char* name, char* str, int val); + +// Basic types +Type vc_boolType(VC vc); +Type vc_realType(VC vc); +Type vc_intType(VC vc); + +//! Create a subrange type +Type vc_subRangeType(VC vc, int lowerEnd, int upperEnd); + +//! Creates a subtype defined by the given predicate +/*! + * \param pred is a predicate taking one argument of type T and returning + * Boolean. The resulting type is a subtype of T whose elements x are those + * satisfying the predicate pred(x). + * + * \param witness is an expression of type T for which pred holds (if a Null + * expression is passed as a witness, cvc will try to prove \f$\exists x. pred(x))\f$. + * if the witness check fails, a TypecheckException is thrown. + */ +Type vc_subtypeType(VC vc, Expr pred, Expr witness); + +// Tuple types +Type vc_tupleType2(VC vc, Type type0, Type type1); +Type vc_tupleType3(VC vc, Type type0, Type type1, Type type2); +//! Create a tuple type. 'types' is an array of types of length numTypes. +Type vc_tupleTypeN(VC vc, Type* types, int numTypes); + +// Record types +Type vc_recordType1(VC vc, char* field, Type type); +Type vc_recordType2(VC vc, char* field0, Type type0, + char* field1, Type type1); +Type vc_recordType3(VC vc, char* field0, Type type0, + char* field1, Type type1, + char* field2, Type type2); +//! Create a record type. +/*! 'fields' and 'types' are arrays of length numFields. */ +Type vc_recordTypeN(VC vc, char** fields, Type* types, int numFields); + +// Datatypes + +//! Single datatype, single constructor +/*! The types are either type exressions (obtained from a type with + * getExpr()) or string expressions containing the name of (one of) the + * dataType(s) being defined. */ +Type vc_dataType1(VC vc, char* name, char* constructor, int arity, + char** selectors, Expr* types); + +//! Single datatype, multiple constructors +/*! The types are either type exressions (obtained from a type with + * getExpr()) or string expressions containing the name of (one of) the + * dataType(s) being defined. */ +Type vc_dataTypeN(VC vc, char* name, int numCons, char** constructors, + int* arities, char*** selectors, Expr** types); + +//! Multiple datatypes +/*! The types are either type exressions (obtained from a type with + * getExpr()) or string expressions containing the name of (one of) the + * dataType(s) being defined. + * Returns an array of size numTypes which must be freed by calling + * vc_deleteTypeVector. + */ +Type* vc_dataTypeMN(VC vc, int numTypes, char** names, + int* numCons, char*** constructors, + int** arities, char**** selectors, + Expr*** types); + +//! Create an array type +Type vc_arrayType(VC vc, Type typeIndex, Type typeData); + +//! Create a bitvector type of length n +Type vc_bvType(VC vc, int n); + +//! Create a function type with 1 argument +Type vc_funType1(VC vc, Type a1, Type typeRan); +//! Create a function type with 2 arguments +Type vc_funType2(VC vc, Type a1, Type a2, Type typeRan); +//! Create a function type with 3 arguments +Type vc_funType3(VC vc, Type a1, Type a2, Type a3, Type typeRan); +//! Create a function type with N arguments +Type vc_funTypeN(VC vc, Type* args, Type typeRan, int numArgs); + +// User-defined types + +//! Create an uninterpreted named type +Type vc_createType(VC vc, char* typeName); +//! Lookup a user-defined (uninterpreted) type by name +Type vc_lookupType(VC vc, char* typeName); + +///////////////////////////////////////////////////////////////////////////// +// Expr manipulation methods // +///////////////////////////////////////////////////////////////////////////// + +//! Return the ExprManager +ExprManager* vc_getEM(VC vc); + +//! Create a variable with a given name and type +/*! The type cannot be a function type. */ +Expr vc_varExpr(VC vc, char* name, Type type); + +//! Create a variable with a given name, type, and value +Expr vc_varExprDef(VC vc, char* name, Type type, + Expr def); + +//! Get the expression and type associated with a name. +/*! If there is no such Expr, a NULL Expr is returned. */ +Expr vc_lookupVar(VC vc, char* name, Type* type); + +//! Get the type of the Expr. +Type vc_getType(VC vc, Expr e); + +//! Get the largest supertype of the Expr. +Type vc_getBaseType(VC vc, Expr e); + +//! Get the largest supertype of the Type. +Type vc_getBaseTypeOfType(VC vc, Type t); + +//! Get the subtype predicate +Expr vc_getTypePred(VC vc, Type t, Expr e); + +//! Create a string Expr +Expr vc_stringExpr(VC vc, char* str); + +//! Create an ID Expr +Expr vc_idExpr(VC vc, char* name); + +//! Create a list Expr +/*! Intermediate representation for DP-specific expressions. + * Normally, the first element of the list is a string Expr + * representing an operator, and the rest of the list are the + * arguments. For example, + * + * kids.push_back(vc->stringExpr("PLUS")); + * kids.push_back(x); // x and y are previously created Exprs + * kids.push_back(y); + * Expr lst = vc->listExpr(kids); + * + * Or, alternatively (using its overloaded version): + * + * Expr lst = vc->listExpr("PLUS", x, y); + * + * or + * + * vector summands; + * summands.push_back(x); summands.push_back(y); ... + * Expr lst = vc->listExpr("PLUS", summands); + */ +Expr vc_listExpr(VC vc, int numKids, Expr* kids); + +// Expr I/O +//! Expr vc_parseExpr(VC vc, char* s); +void vc_printExpr(VC vc, Expr e); +//! Print e into a char* +/*! Note that the ownership of the char* is given to the caller + which should free the memory when it is done with it. This + can be done by calling vc_deleteString. */ +char* vc_printExprString(VC vc, Expr e); +//! Delete char* returned by previous function +void vc_deleteString(char* str); +//! Print 'e' into an open file descriptor +void vc_printExprFile(VC vc, Expr e, int fd); + +//! Import the Expr from another instance of VC +/*! When expressions need to be passed among several instances of + * VC, they need to be explicitly imported into the + * corresponding instance using this method. The return result is + * an identical expression that belongs to the current instance of + * VC, and can be safely used as part of more complex + * expressions from the same instance. + \param vc is the instance to be imported into + \param e is the expression created using a different (not vc) instance + */ +Expr vc_importExpr(VC vc, Expr e); + +//! Import the Type from another instance of VC +/*! \sa vc_importExpr() */ +Type vc_importType(Type t); + +//! Create an equality expression. The two children must have the same type. +Expr vc_eqExpr(VC vc, Expr child0, Expr child1); + +//! Create an all distinct expression. All children must ahve the same type. +Expr vc_distinctExpr(VC vc, Expr* children, int numChildren); + +// Boolean expressions + +// The following functions create Boolean expressions. The children provided +// as arguments must be of type Boolean. +Expr vc_trueExpr(VC vc); +Expr vc_falseExpr(VC vc); +Expr vc_notExpr(VC vc, Expr child); +Expr vc_andExpr(VC vc, Expr left, Expr right); +Expr vc_andExprN(VC vc, Expr* children, int numChildren); +Expr vc_orExpr(VC vc, Expr left, Expr right); +Expr vc_orExprN(VC vc, Expr* children, int numChildren); +Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc); +Expr vc_iffExpr(VC vc, Expr left, Expr right); +Expr vc_iteExpr(VC vc, Expr ifpart, Expr thenpart, Expr elsepart); + +// Substitution + +// Substitutes oldTerms for newTerms in e. +// This function doesn't actually exist in ValidityChecker interface, +// but it does in Expr, and its functionality is needed in the C interface. +// For consistency, it is represented here as if it were in ValidityChecker. +Expr vc_substExpr(VC vc, Expr e, + Expr* oldTerms, int numOldTerms, + Expr* newTerms, int numNewTerms); + +// User-defined (uninterpreted) functions. + +//! Create an operator from a function with a given name and type. +/*! Name is given as an ID Expr, and the type must be a function type. */ +Op vc_createOp(VC vc, char* name, Type type); + +//! Create a named user-defined function with a given type +Op vc_createOpDef(VC vc, char* name, Type type, Expr def); + +//! Lookup an operator by name. +/*! Returns the operator and the type if the operator exists. + * Returns NULL otherwise + */ +Op vc_lookupOp(VC vc, char* name, Type* type); + +//! Create expressions with a user-defined operator. +/*! op must have a function type. */ +Expr vc_funExpr1(VC vc, Op op, Expr child); +Expr vc_funExpr2(VC vc, Op op, Expr left, Expr right); +Expr vc_funExpr3(VC vc, Op op, Expr child0, Expr child1, Expr child2); +Expr vc_funExprN(VC vc, Op op, Expr* children, int numChildren); + +// Arithmetic + +//! Create a rational number with numerator n and denominator d. +/*! d cannot be 0. */ +Expr vc_ratExpr(VC vc, int n, int d); + +//! Create a rational number n/d; n and d are given as strings +/*! n and d are converted to arbitrary-precision integers according to + * the given base. d cannot be 0. */ +Expr vc_ratExprFromStr(VC vc, char* n, char* d, int base); + +//! Create a rational from a single string. +/*! + \param n can be a string containing an integer, a pair of integers + "nnn/ddd", or a number in the fixed or floating point format. + \param base is the base in which to interpret the string. +*/ +Expr vc_ratExprFromStr1(VC vc, char* n, int base); + +//! Unary minus. Child must have a numeric type. +Expr vc_uminusExpr(VC vc, Expr child); + +// plus, minus, mult. Children must have numeric types. +Expr vc_plusExpr(VC vc, Expr left, Expr right); +Expr vc_plusExprN(VC vc, Expr* children, int numChildren); +Expr vc_minusExpr(VC vc, Expr left, Expr right); +Expr vc_multExpr(VC vc, Expr left, Expr right); +Expr vc_powExpr(VC vc, Expr pow, Expr base); +Expr vc_divideExpr(VC vc, Expr numerator, Expr denominator); + +// The following functions create less-than, less-than or equal, +// greater-than, and greater-than or equal expressions of type Boolean. +// Their arguments must be of numeric types. +Expr vc_ltExpr(VC vc, Expr left, Expr right); +Expr vc_leExpr(VC vc, Expr left, Expr right); +Expr vc_gtExpr(VC vc, Expr left, Expr right); +Expr vc_geExpr(VC vc, Expr left, Expr right); + +// Records + +// Create record literals; +Expr vc_recordExpr1(VC vc, char* field, Expr expr); +Expr vc_recordExpr2(VC vc, char* field0, Expr expr0, + char* field1, Expr expr1); +Expr vc_recordExpr3(VC vc, char* field0, Expr expr0, + char* field1, Expr expr1, + char* field2, Expr expr2); +Expr vc_recordExprN(VC vc, char** fields, Expr* exprs, int numFields); + +//! Create an expression representing the selection of a field from a record. +Expr vc_recSelectExpr(VC vc, Expr record, char* field); + +//! Record update; equivalent to "record WITH .field := newValue" +Expr vc_recUpdateExpr(VC vc, Expr record, char* field, Expr newValue); + +// Arrays + +//! Create an expression for the value of array at the given index +Expr vc_readExpr(VC vc, Expr array, Expr index); + +//! Array update; equivalent to "array WITH [index] := newValue" +Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue); + +// Bitvectors +// Additional type constructor +Type vc_bv32Type(VC vc); + +// Bitvector constants +Expr vc_bvConstExprFromStr(VC vc, char* binary_repr); +Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value); +Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value); +Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long value); + +// Concat and extract +Expr vc_bvConcatExpr(VC vc, Expr left, Expr right); +Expr vc_bvConcatExprN(VC vc, Expr* children, int numChildren); +Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, int low_bit_no); +Expr vc_bvBoolExtract(VC vc, Expr child, int bit_no); + +// Bitwise Boolean operators: Negation, And, Or, Xor +Expr vc_bvNotExpr(VC vc, Expr child); +Expr vc_bvAndExpr(VC vc, Expr left, Expr right); +Expr vc_bvOrExpr(VC vc, Expr left, Expr right); +Expr vc_bvXorExpr(VC vc, Expr left, Expr right); + +// Unsigned bitvector inequalities +Expr vc_bvLtExpr(VC vc, Expr left, Expr right); +Expr vc_bvLeExpr(VC vc, Expr left, Expr right); +Expr vc_bvGtExpr(VC vc, Expr left, Expr right); +Expr vc_bvGeExpr(VC vc, Expr left, Expr right); + +// Signed bitvector inequalities +Expr vc_bvSLtExpr(VC vc, Expr left, Expr right); +Expr vc_bvSLeExpr(VC vc, Expr left, Expr right); +Expr vc_bvSGtExpr(VC vc, Expr left, Expr right); +Expr vc_bvSGeExpr(VC vc, Expr left, Expr right); + +// Sign-extend child to a total of nbits bits +Expr vc_bvSignExtend(VC vc, Expr child, int nbits); + +// Bitvector arithmetic: unary minus, plus, subtract, multiply +Expr vc_bvUMinusExpr(VC vc, Expr child); +Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right); +Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right); +Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right); +Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right); +Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right); +Expr vc_bv32MultExpr(VC vc, Expr left, Expr right); +Expr vc_bvUDivExpr(VC vc, Expr left, Expr right); +Expr vc_bvURemExpr(VC vc, Expr left, Expr right); +Expr vc_bvSDivExpr(VC vc, Expr left, Expr right); +Expr vc_bvSRemExpr(VC vc, Expr left, Expr right); +Expr vc_bvSModExpr(VC vc, Expr left, Expr right); + +// Shift operators +Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child); +Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child); +Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child); +Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child); +Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child); +Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child); +Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs); + +/*C pointer support: C interface to support C memory arrays in CVC3 */ +Expr vc_bvCreateMemoryArray(VC vc, char * arrayName); +Expr vc_bvReadMemoryArray(VC vc, + Expr array, Expr byteIndex, int numOfBytes); +Expr vc_bvWriteToMemoryArray(VC vc, + Expr array, Expr byteIndex, + Expr element, int numOfBytes); + +// Tuples + +//! Create a tuple expression +/*! 'children' is an array of elements of length numChildren */ +Expr vc_tupleExprN(VC vc, Expr* children, int numChildren); + +//! Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5) +Expr vc_tupleSelectExpr(VC vc, Expr tuple, int index); + +//! Tuple update; equivalent to "tuple WITH index := newValue" +Expr vc_tupleUpdateExpr(VC vc, Expr tuple, int index, Expr newValue); + +// Datatypes + +//! Datatype constructor expression +Expr vc_datatypeConsExpr(VC vc, char* constructor, int numArgs, Expr* args); + +//! Datatype selector expression +Expr vc_datatypeSelExpr(VC vc, char* selector, Expr arg); + +//! Datatype tester expression +Expr vc_datatypeTestExpr(VC vc, char* constructor, Expr arg); + +// Quantifiers + +//! Create a bound variable. +/*! \param name + * \param uid is a fresh unique string to distinguish this variable + * from other bound variables with the same name + * \param type + */ +Expr vc_boundVarExpr(VC vc, char* name, char *uid, Type type); + +//! Create a FORALL quantifier. +/*! Bvars is an array of bound variables of length numBvars. */ +Type vc_forallExpr(VC vc, Expr* Bvars, int numBvars, Expr f); + +//! Set triggers for a forallExpr +void vc_setTriggers(VC vc, Expr e, int numTrigs, Expr* triggers); + +//! Create an EXISTS quantifier. +/*! Bvars is an array of bound variables of length numBvars. */ +Expr vc_existsExpr(VC vc, Expr* Bvars, int numBvars, Expr f); + +//! Lambda-expression +Op vc_lambdaExpr(VC vc, int numVars, Expr* vars, Expr body); + +///////////////////////////////////////////////////////////////////////////// +// Context-related methods // +///////////////////////////////////////////////////////////////////////////// + +//! Set the resource limit (0==unlimited, 1==exhausted). +/*! Currently, the limit is the total number of processed facts. */ +void vc_setResourceLimit(VC vc, unsigned limit); + +//! Assert a new formula in the current context. +/*! The formula must have Boolean type. */ +void vc_assertFormula(VC vc, Expr e); + +//! Register an atomic formula of interest. +/*! Registered atoms are tracked by the decision procedures. If one of them + is deduced to be true or false, it is added to a list of implied literals. + Implied literals can be retrieved with the getImpliedLiteral function */ +void vc_registerAtom(VC vc, Expr e); + +//! Return next literal implied by last assertion. Null if none. +/*! Returned literals are either registered atomic formulas or their negation + */ +Expr vc_getImpliedLiteral(VC vc); + +//! Simplify e with respect to the current context +Expr vc_simplify(VC vc, Expr e); + +//! Check validity of e in the current context. +/*! Possible results are: 0 = invalid, 1 = valid, 2 = abort, 3 = unknown, + * -100 = exception (type error, internal error, etc). + * If the result is 1, then the resulting context is the same as + * the starting context. If the result is 0 or 3, then the resulting + * context is a context in which e is false (though the context may be + * inconsistent in the case of an unknown result). e must have Boolean + * type. In the case of a result of -100, refer to vc_get_error_string() + * to see what went wrong. */ +int vc_query(VC vc, Expr e); + +//! Get the next model +/*! This method should only be called after a query which returns + 0. Its return values are as for vc_query(). */ +int vc_checkContinue(VC vc); + +//! Restart the most recent query with e as an additional assertion. +/*! This method should only be called after a query which returns + 0. Its return values are as for vc_query(). */ +int vc_restart(VC vc, Expr e); + +//! Returns to context immediately before last invalid query. +/*! This method should only be called after a query which returns 0. + */ +void vc_returnFromCheck(VC vc); + +//! Get assumptions made by the user in this and all previous contexts. +/*! User assumptions are created either by calls to assertFormula or by a + * call to query. In the latter case, the negated query is added as an + * assumption. The caller is responsible for freeing the array when + * finished with it. + */ +Expr* vc_getUserAssumptions(VC vc, int* size); + +//! Get assumptions made internally in this and all previous contexts. +/*! Internal assumptions are literals assumed by the sat solver. + * The caller is responsible for freeing the array when finished with it by + * calling vc_deleteVector. + */ +Expr* vc_getInternalAssumptions(VC vc, int* size); + +//! Get all assumptions made in this and all previous contexts. +/*! + * The caller is responsible for freeing the array when finished with it by + * calling vc_deleteVector. + */ +Expr* vc_getAssumptions(VC vc, int* size); + +//yeting, for proof translation, get the assumptions used. +//the assumptions used are different from the user assumptions. +//the assumptions used are preprocessed if 'preprocess' is ena +Expr vc_getProofAssumptions(VC vc); + +//yeting, for proof translation, +Expr vc_getProofQuery(VC vc); + +//! Returns the set of assumptions used in the proof of queried formula. +/*! It returns a subset of getAssumptions(). If the last query was false + * or there has not yet been a query, it does nothing. + * The caller is responsible for freeing the array when finished with it by + * calling vc_deleteVector. + */ +Expr* vc_getAssumptionsUsed(VC vc, int* size); + +//! Return the counterexample after a failed query. +/*! This method should only be called after a query which returns + * false. It will try to return the simplest possible set of + * assertions which are sufficient to make the queried expression + * false. The caller is responsible for freeing the array when finished with + * it by calling vc_deleteVector. + */ +Expr* vc_getCounterExample(VC vc, int* size); + +//! Will assign concrete values to all user created variables +/*! This function should only be called after a query which return false. + * Returns an array of Exprs with size *size. + * The caller is responsible for freeing the array when finished with it by + * calling vc_deleteVector. + */ +Expr* vc_getConcreteModel(VC vc, int* size); + +// Returns true if the current context is inconsistent. +/*! Also returns a minimal set of assertions used to determine the + * inconsistency. The caller is responsible for freeing the array when finished + * with it by calling vc_deleteVector. + */ +int vc_inconsistent(VC vc, Expr** assumptions, int* size); + +//! Returns non-NULL if the invalid result from last query() is imprecise +/*! + * The return value is filled with the reasons for incompleteness (it + * is intended to be shown to the end user). The caller is responsible for + * freeing the string returned by calling vc_deleteString. + */ +char* vc_incomplete(VC vc); + +//! Returns the proof for the last proven query +Expr vc_getProof(VC vc); + +//! Returns the proof of a .cvc file, if it is valid. +Expr vc_getProofOfFile(VC vc, char * filename); + +//! Returns the TCC of the last assumption or query +/*! Returns Null Expr if no assumptions or queries were performed. */ +Expr vc_getTCC(VC vc); + +//! Return the set of assumptions used in the proof of the last TCC +/*! The caller is responsible for freeing the array when finished with it by + * calling vc_deleteVector. + */ +Expr* vc_getAssumptionsTCC(VC vc, int* size); + +//! Returns the proof of TCC of the last assumption or query +/*! Returns Null Expr if no assumptions or queries were performed. */ +Expr vc_getProofTCC(VC vc); + +//! After successful query, return its closure |- Gamma => phi +/*! Turn a valid query Gamma |- phi into an implication + * |- Gamma => phi. + * + * Returns Null Expr if last query was invalid. + */ +Expr vc_getClosure(VC vc); + +//! Construct a proof of the query closure |- Gamma => phi +/*! Returns Null if last query was Invalid. */ +Expr vc_getProofClosure(VC vc); + +//! Returns the current stack level. Initial level is 0. +int vc_stackLevel(VC vc); + +//! Checkpoint the current context and increase the scope level +void vc_push(VC vc); + +//! Restore the current context to its state at the last checkpoint +void vc_pop(VC vc); + +//! Restore the current context to the given stackLevel. +/*! stackLevel must be less than or equal to the current stack level. + */ +void vc_popto(VC vc, int stackLevel); + +//! Get the current context +Context* vc_getCurrentContext(VC vc); + +/* ---------------------------------------------------------------------- */ +/* Util */ +/* ---------------------------------------------------------------------- */ + +// Order + +//! Compares two expressions +/*! If e1 < e2, e1==e2, and e1 > e2, it returns -1, 0, 1 + * respectively. A return value of -100 signals an error (refer to + * vc_get_error_string() for details). + * + * Can't be 'compare' because already defined in ocaml */ +int vc_compare_exprs(Expr e1,Expr e2); + +// Printing + +//! Convert Expr to string +char* vc_exprString(Expr e); +//! Convert Type to string +char* vc_typeString(Type t); + +// What kind of Expr? +int vc_isClosure(Expr e); +int vc_isQuantifier(Expr e); +int vc_isLambda(Expr e); +Expr vc_isVar(Expr e); + +int vc_arity(Expr e); +int vc_getKind(Expr e); +Expr vc_getChild(Expr e, int i); +int vc_getNumVars(Expr e); +Expr vc_getVar(Expr e, int i); +Expr vc_getBody(Expr e); +Expr vc_getExistential(Expr e); +Expr vc_getFun(VC vc, Expr e); +Expr vc_toExpr(Type t); + +//! Translate a kind int to a string +const char* vc_getKindString(VC vc,int kind); + +//! Translate a kind string to an int +int vc_getKindInt(VC vc,char* kind_name); + +//! Return an int from a rational expression +int vc_getInt(Expr e); + +//! Return an int from a constant bitvector expression +int vc_getBVInt(VC vc, Expr e); +//! Return an unsigned int from a constant bitvector expression +unsigned int vc_getBVUnsigned(VC vc, Expr e); + +// Debug +int vc_get_error_status(); +void vc_reset_error_status(); +char* vc_get_error_string(); + +//! Print statistics +void vc_print_statistics(VC vc); + +#endif + + diff --git a/src/bindings/compat/c/c_interface_defs.h b/src/bindings/compat/c/c_interface_defs.h new file mode 100644 index 000000000..9b59fce56 --- /dev/null +++ b/src/bindings/compat/c/c_interface_defs.h @@ -0,0 +1,51 @@ +/*****************************************************************************/ +/*! + * \file c_interface_defs.h + * + * Author: Clark Barrett + * + * Created: Thu Jun 5 13:16:26 2003 + * + *
+ * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + *
+ * + */ +/*****************************************************************************/ + +#ifndef _cvc3__include__c_interface_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 + diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am index 9dd6ab947..d958eccf0 100644 --- a/src/bindings/compat/java/Makefile.am +++ b/src/bindings/compat/java/Makefile.am @@ -27,7 +27,7 @@ data_DATA += cvc4compat.jar libcvc4bindings_java_compat_la_LDFLAGS = \ -version-info $(LIBCVC4BINDINGS_VERSION) libcvc4bindings_java_compat_la_LIBADD = \ - -L@builddir@/../compat -lcvc4compat + -L@builddir@/../../../compat -lcvc4compat endif @@ -68,7 +68,7 @@ SRC_CPP_FILES = JniUtils.cpp # all cpp files (to compile) CPP_FILES = $(SRC_CPP_FILES) $(JNI_CPP_FILES) -nodist_libcvc4bindings_java_compat_la_SOURCES = $(CPP_FILES) +libcvc4bindings_java_compat_la_SOURCES = $(CPP_FILES) HEADER_FILES = JniUtils.h PYTHON_FILES = run_all.py run_tests.py create_impl.py diff --git a/src/bindings/compat/java/src/cvc3/JniUtils.cpp b/src/bindings/compat/java/src/cvc3/JniUtils.cpp index c8e3f5e9b..f291b221b 100644 --- a/src/bindings/compat/java/src/cvc3/JniUtils.cpp +++ b/src/bindings/compat/java/src/cvc3/JniUtils.cpp @@ -19,7 +19,7 @@ namespace Java_cvc3_JniUtils { /// Embedding of c++ objects in java objects - Embedded* unembed(JNIEnv* env, jobject jobj) { + /*Embedded* unembed(JNIEnv* env, jobject jobj) { Embedded* embedded = (Embedded*) env->GetDirectBufferAddress(jobj); DebugAssert(embedded != NULL, "JniUtils::unembed: embedded object is NULL"); return embedded; @@ -29,7 +29,7 @@ namespace Java_cvc3_JniUtils { Embedded* embedded = unembed(env, jobj); DebugAssert(embedded != NULL, "JniUtils::deleteEmbedded: embedded object is NULL"); delete embedded; - } + }*/ @@ -73,16 +73,20 @@ namespace Java_cvc3_JniUtils { } DebugAssert(false, "JniUtils::toJava(FormulaValue): unreachable"); + return toJava(env, "UNDEFINED"); } jstring toJava(JNIEnv* env, CVC3::InputLanguage lang) { switch (lang) { case PRESENTATION_LANG: return toJava(env, "PRESENTATION"); case SMTLIB_LANG: return toJava(env, "SMTLIB"); - case LISP_LANG: return toJava(env, "LISP"); + case SMTLIB_V2_LANG: return toJava(env, "SMTLIB_V2"); + //case LISP_LANG: return toJava(env, "LISP"); + default: /* fall through */; } DebugAssert(false, "JniUtils::toJava(InputLanguage): unreachable"); + return toJava(env, "UNDEFINED"); } InputLanguage toCppInputLanguage(JNIEnv* env, const string& lang) { @@ -90,11 +94,16 @@ namespace Java_cvc3_JniUtils { return PRESENTATION_LANG; } else if (lang.compare("SMTLIB") == 0) { return SMTLIB_LANG; + } else if (lang.compare("SMTLIB_V2") == 0) { + return SMTLIB_V2_LANG; + /* } else if (lang.compare("LISP") == 0) { return LISP_LANG; + */ } DebugAssert(false, "JniUtils::toCpp(InputLanguage): unreachable"); + return CVC4::language::input::LANG_MAX; } void toJava(JNIEnv* env, const Exception& e) { @@ -161,7 +170,7 @@ namespace Java_cvc3_JniUtils { env->FindClass("java/lang/String"), env->NewStringUTF("")); - for(int i = 0; i < v.size(); ++i) { + for(unsigned i = 0; i < v.size(); ++i) { env->SetObjectArrayElement(jarray, i, toJava(env, v[i])); } diff --git a/src/compat/Makefile.am b/src/compat/Makefile.am index 1e64a61bb..936a63559 100644 --- a/src/compat/Makefile.am +++ b/src/compat/Makefile.am @@ -21,7 +21,7 @@ if CVC4_BUILD_LIBCOMPAT lib_LTLIBRARIES = libcvc4compat.la if HAVE_CXXTESTGEN -noinst_LTLIBRARIES = libcvc4compat_noinst.la +check_LTLIBRARIES = libcvc4compat_noinst.la endif libcvc4compat_la_LDFLAGS = \ @@ -48,6 +48,7 @@ libcvc4compat_noinst_la_SOURCES = \ else EXTRA_DIST = \ + cvc3_kinds.h \ cvc3_compat.h \ cvc3_compat.cpp diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 766cc300d..896a13681 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -265,11 +265,11 @@ size_t Expr::hash() const { } bool Expr::isFalse() const { - return getKind() == CVC4::kind::CONST_BOOLEAN && !getConst(); + return getKind() == CVC4::kind::CONST_BOOLEAN && getConst() == false; } bool Expr::isTrue() const { - return getKind() == CVC4::kind::CONST_BOOLEAN && getConst(); + return getKind() == CVC4::kind::CONST_BOOLEAN && getConst() == true; } bool Expr::isBoolConst() const { @@ -280,6 +280,26 @@ bool Expr::isVar() const { return isVariable(); } +bool Expr::isString() const { + return false; +} + +bool Expr::isApply() const { + return hasOperator(); +} + +bool Expr::isTheorem() const { + return false; +} + +bool Expr::isConstant() const { + return isConst(); +} + +bool Expr::isRawList() const { + return false; +} + bool Expr::isEq() const { return getKind() == CVC4::kind::EQUAL; } @@ -320,6 +340,28 @@ bool Expr::isSkolem() const { return getKind() == CVC4::kind::SKOLEM; } +Op Expr::mkOp() const { + return *this; +} + +Op Expr::getOp() const { + return getOperator(); +} + +Expr Expr::getOpExpr() const { + return getOperator(); +} + +int Expr::getOpKind() const { + Expr op = getOperator(); + int k = op.getKind(); + return k == BUILTIN ? getKind() : k; +} + +Expr Expr::getExpr() const { + return *this; +} + std::vector< std::vector > Expr::getTriggers() const { return vector< vector >(); } @@ -1889,4 +1931,22 @@ void ValidityChecker::printStatistics() { Message() << d_smt->getStatisticsRegistry(); } +int compare(const Expr& e1, const Expr& e2) { + // Quick equality check (operator== is implemented independently + // and more efficiently) + if(e1 == e2) return 0; + + if(e1.isNull()) return -1; + if(e2.isNull()) return 1; + + // Both are non-Null. Check for constant + bool e1c = e1.isConstant(); + if (e1c != e2.isConstant()) { + return e1c ? -1 : 1; + } + + // Compare the indices + return (e1.getIndex() < e2.getIndex())? -1 : 1; +} + }/* CVC3 namespace */ diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index fbb54a46c..81ac3a6aa 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -228,8 +228,8 @@ class Proof {}; using CVC4::ExprManager; using CVC4::InputLanguage; -using CVC4::Rational; using CVC4::Integer; +using CVC4::Rational; using CVC4::Exception; using CVC4::Cardinality; using namespace CVC4::kind; @@ -299,6 +299,9 @@ public: };/* class CVC3::Type */ +class Expr; +typedef Expr Op; + /** * Expr class for CVC3 compatibility layer. * @@ -341,6 +344,11 @@ public: bool isTrue() const; bool isBoolConst() const; bool isVar() const; + bool isString() const; + bool isApply() const; + bool isTheorem() const; + bool isConstant() const; + bool isRawList() const; bool isEq() const; bool isNot() const; @@ -354,6 +362,14 @@ public: bool isRational() const; bool isSkolem() const; + Rational getRational() const; + + Op mkOp() const; + Op getOp() const; + Expr getOpExpr() const; + int getOpKind() const; + Expr getExpr() const;// since people are used to doing getOp().getExpr() in CVC3 + //! Get the manual triggers of the closure Expr std::vector< std::vector > getTriggers() const; @@ -389,7 +405,6 @@ public: };/* class CVC3::Expr */ -typedef Expr Op; typedef CVC4::StatisticsRegistry Statistics; #define PRESENTATION_LANG ::CVC4::language::input::LANG_CVC4 @@ -1460,6 +1475,9 @@ void ExprHashMap::insert(Expr a, Expr b) { (*this)[a] = b; } +// Comparison (the way that CVC3 does it) +int compare(const Expr& e1, const Expr& e2); + }/* CVC3 namespace */ #endif /* _cvc3__include__vc_h_ */