more interface work; adding legacy C interface

11 files changed, 3756 insertions, 12 deletions

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
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ *
+ * <hr>
+ *
+ */
+/*****************************************************************************/
+
+
+#include <strings.h>
+#include "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 <assert.h>
+
+
+using namespace std;
+
+
+// -------------------------------------------------------------------------
+//  Debugging
+// -------------------------------------------------------------------------
+
+// + will mean OK
+// - will mean error
+int c_interface_error_flag = 1;
+const int error_int = -100;
+const char* c_interface_error_message = "An Exception Occured: System in a compromised state.";
+string c_interface_error_string;
+// Used to return char* values.  Note that the value is only good until
+// the next call to a function returning char*
+static string tmpString;
+
+void signal_error(const char* message,int flag_val,CVC3::Exception ex){
+  ostringstream ss;
+  ss << c_interface_error_message << endl;
+  ss << "Message: " << message << endl;
+  ss << "Exception: " << ex << endl;
+  IF_DEBUG(cerr << ss.str();)
+  c_interface_error_string = ss.str();
+  c_interface_error_flag = flag_val;
+}
+
+extern "C" int vc_get_error_status(){
+  return c_interface_error_flag;
+}
+
+extern "C" void vc_reset_error_status(){
+  c_interface_error_flag = 1;
+  c_interface_error_string = "";
+}
+
+extern "C" char* vc_get_error_string() {
+  return (char*) (c_interface_error_string.c_str());
+}
+
+
+// Private to implementation
+
+class CInterface {
+public:
+  static CVC3::Type fromType(Type t);
+  static Type toType(const CVC3::Type& t);
+  static CVC3::Expr fromExpr(Expr e);
+  static Expr toExpr(const CVC3::Expr& e);
+  static CVC3::Op fromOp(Op op);
+  static Op toOp(VC vc, const CVC3::Op& op);
+  //  static CVC3::Proof fromProof(Proof proof);
+  //  static Proof toProof(const CVC3::Proof& proof);
+  static void deleteExpr(Expr e);
+  static void deleteType(Type t);
+  static void deleteVector(Expr* vec);
+};
+
+
+CVC3::Type CInterface::fromType(Type t)
+{
+  return *(CVC3::Type*)t;
+}
+
+
+Type CInterface::toType(const CVC3::Type& t)
+{
+  if(t.isNull()) return NULL;
+  return Type(new CVC3::Type(t));
+}
+
+
+CVC3::Expr CInterface::fromExpr(Expr e)
+{
+  return *(CVC3::Expr*)e;
+}
+
+
+Expr CInterface::toExpr(const CVC3::Expr& e)
+{
+  if(e.isNull()) return NULL;
+  return Expr(new CVC3::Expr(e));
+}
+
+
+CVC3::Op CInterface::fromOp(Op op)
+{
+  return *(CVC3::Op*)op;
+}
+
+
+Op CInterface::toOp(VC vc, const CVC3::Op& op)
+{
+  if (op.isNull()) return NULL;
+  return Op(new CVC3::Op(op));
+}
+
+
+// CVC3::Proof CInterface::fromProof(Proof proof)
+// {
+//   return CVC3::Proof(fromExpr(proof));
+// }
+
+
+// Proof CInterface::toProof(const CVC3::Proof& proof)
+// {
+//   return toExpr(proof.getExpr());
+// }
+
+
+void CInterface::deleteExpr(Expr e)
+{
+  if (e) delete (CVC3::Expr*)e;
+}
+
+void CInterface::deleteType(Type t)
+{
+  if (t) delete (CVC3::Type*)t;
+}
+
+void CInterface::deleteVector(Expr* e)
+{
+  if (e) delete [] e;
+}
+
+
+static CVC3::Type fromType(Type t) { return CInterface::fromType(t); }
+static Type toType(const CVC3::Type& t) { return CInterface::toType(t); }
+static CVC3::Expr fromExpr(Expr e) { return CInterface::fromExpr(e); }
+static Expr toExpr(const CVC3::Expr& e) { return CInterface::toExpr(e); }
+static CVC3::Op fromOp(Op op) { return CInterface::fromOp(op); }
+static Op toOp(VC vc, const CVC3::Op& op) { return CInterface::toOp(vc, op); }
+// static CVC3::Proof fromProof(Proof proof) { return CInterface::fromProof(proof); }
+// static Proof toProof(const CVC3::Proof& proof) { return CInterface::toProof(proof); }
+
+
+static char *val_to_binary_str(unsigned nbits, unsigned long val) {
+        char s[65];
+
+	assert(nbits < sizeof s);
+        strcpy(s, "");
+        while(nbits-- > 0) {
+                if((val >> nbits) & 1)
+                        strcat(s, "1");
+                else
+                        strcat(s, "0");
+        }
+        return strdup(s);
+}
+
+
+///////////////////////////////////////////////////////////////////////////
+// Begin implementation of C interface                                   //
+///////////////////////////////////////////////////////////////////////////
+
+
+extern "C" VC vc_createValidityChecker(Flags flags) {
+  try{
+    CVC3::CLFlags f = (flags==NULL)? CVC3::ValidityChecker::createFlags()
+      : *((CVC3::CLFlags*)flags);
+    return (VC)CVC3::ValidityChecker::create(f);
+  } catch (CVC3::Exception ex){
+    signal_error("vc_createValidityChecker",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Flags vc_createFlags() {
+  try{
+  return new CVC3::CLFlags(CVC3::ValidityChecker::createFlags());
+  } catch (CVC3::Exception ex){
+    signal_error("vc_createFlags",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" void vc_destroyValidityChecker(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  delete cvc;
+  } catch (CVC3::Exception ex){
+    signal_error("vc_destroyVelidityChecker",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_deleteFlags(Flags flags) {
+  try{
+  delete ((CVC3::CLFlags*)flags);
+  } catch (CVC3::Exception ex){
+    signal_error("vc_deleteFlags",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_deleteExpr(Expr e)
+{
+  try{
+  CInterface::deleteExpr(e);
+  } catch (CVC3::Exception ex){
+    signal_error("vc_deleteExpr",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_deleteType(Type t)
+{
+  try{
+  CInterface::deleteType(t);
+  } catch (CVC3::Exception ex){
+    signal_error("vc_deleteType",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_deleteOp(Op op)
+{
+  vc_deleteExpr(op);
+}
+
+
+extern "C" void vc_deleteVector(Expr* e)
+{
+  try{
+  CInterface::deleteVector(e);
+  } catch (CVC3::Exception ex){
+    signal_error("vc_deleteVector",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_deleteTypeVector(Type* e)
+{
+  vc_deleteVector(e);
+}
+
+
+extern "C" void vc_setBoolFlag(Flags flags, char* name, int val) {
+  try{
+  CVC3::CLFlags& f = *((CVC3::CLFlags*)flags);
+  f.setFlag(name, (val!=0));
+  } catch (CVC3::Exception ex){
+    signal_error("vc_setBoolFlag",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_setIntFlag(Flags flags, char* name, int val) {
+  try{
+  CVC3::CLFlags& f = *((CVC3::CLFlags*)flags);
+  f.setFlag(name, val);
+  } catch (CVC3::Exception ex){
+    signal_error("vc_setIntFlag",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_setStringFlag(Flags flags, char* name, char* val) {
+  try{
+  CVC3::CLFlags& f = *((CVC3::CLFlags*)flags);
+  f.setFlag(name, string(val));
+  } catch (CVC3::Exception ex){
+    signal_error("vc_setStringFlag",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_setStrSeqFlag(Flags flags, char* name, char* str, int val) {
+  try{
+  CVC3::CLFlags& f = *((CVC3::CLFlags*)flags);
+  f.setFlag(name, pair<string,bool>(string(str), val!=0));
+  } catch (CVC3::Exception ex){
+    signal_error("vc_setStrSeqFlag",error_int,ex);
+  }
+}
+
+
+extern "C" Type vc_boolType(VC vc)
+{
+  try{
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    return toType(cvc->boolType());
+  } catch (CVC3::Exception ex){
+    signal_error("vc_boolType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_realType(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->realType());
+  }catch (CVC3::Exception ex){
+    signal_error("vc_realType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_intType(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->intType());
+  }catch (CVC3::Exception ex){
+    signal_error("vc_intType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_subRangeType(VC vc, int lowerEnd, int upperEnd)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->subrangeType(cvc->ratExpr(lowerEnd),
+                                  cvc->ratExpr(upperEnd)));
+  }catch (CVC3::Exception &ex){
+    signal_error("vc_subRangeType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_subtypeType(VC vc, Expr pred, Expr witness)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->subtypeType(fromExpr(pred), fromExpr(witness)));
+  }catch (CVC3::Exception &ex){
+    signal_error("vc_subtypeType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_tupleType2(VC vc, Type type0, Type type1)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->tupleType(fromType(type0), fromType(type1)));
+  }catch (CVC3::Exception ex){
+    signal_error("vc_tupleType2",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_tupleType3(VC vc, Type type0, Type type1, Type type2)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->tupleType(fromType(type0), fromType(type1),
+			       fromType(type2)));
+  }catch (CVC3::Exception ex){
+    signal_error("vc_tupleType3",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_tupleTypeN(VC vc, Type* types, int numTypes)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Type> cvcTypes;
+  for (int i = 0; i < numTypes; ++i) {
+    cvcTypes.push_back(fromType(types[i]));
+  }
+  return toType(cvc->tupleType(cvcTypes));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_tupleTypeN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_recordType1(VC vc, char* field, Type type)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->recordType(field, fromType(type)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_recordType1",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_recordType2(VC vc, char* field0, Type type0,
+                                      char* field1, Type type1)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->recordType(field0, fromType(type0),
+				field1, fromType(type1)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_recordType2",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_recordType3(VC vc, char* field0, Type type0,
+			              char* field1, Type type1,
+                                      char* field2, Type type2)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->recordType(field0, fromType(type0),
+				field1, fromType(type1),
+				field2, fromType(type2)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_recordType3",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_recordTypeN(VC vc, char** fields, Type* types,
+			       int numFields)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<std::string> cvcFields;
+  vector<CVC3::Type> cvcTypes;
+  for (int i = 0; i < numFields; ++i) {
+    cvcFields.push_back(fields[i]);
+    cvcTypes.push_back(fromType(types[i]));
+  }
+  return toType(cvc->recordType(cvcFields, cvcTypes));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_recordTypeN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_dataType1(VC vc, char* name, char* constructor, int arity,
+                             char** selectors, Expr* types)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  string cvcName(name);
+  string cvcConstructor(constructor);
+  vector<string> cvcSelectors;
+  vector<CVC3::Expr> cvcTypes;
+  for (int i = 0; i < arity; ++i) {
+    cvcSelectors.push_back(selectors[i]);
+    cvcTypes.push_back(fromExpr(types[i]));
+  }
+  return toType(cvc->dataType(cvcName, cvcConstructor, cvcSelectors, cvcTypes));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_dataType1",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_dataTypeN(VC vc, char* name, int numCons, char** constructors,
+                             int* arities, char*** selectors, Expr** types)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  string cvcName(name);
+  vector<string> cvcConstructors;
+  vector<vector<string> > cvcSelectors(numCons);
+  vector<vector<CVC3::Expr> > cvcTypes(numCons);
+  for (int i = 0; i < numCons; ++i) {
+    cvcConstructors.push_back(constructors[i]);
+    for (int j = 0; j < arities[i]; ++j) {
+      cvcSelectors[i].push_back(selectors[i][j]);
+      cvcTypes[i].push_back(fromExpr(types[i][j]));
+    }
+  }
+  return toType(cvc->dataType(cvcName, cvcConstructors,
+                              cvcSelectors, cvcTypes));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_dataTypeN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type* vc_dataTypeMN(VC vc, int numTypes, char** names,
+                               int* numCons, char*** constructors,
+                               int** arities, char**** selectors,
+                               Expr*** types)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<string> cvcNames;
+  vector<vector<string> > cvcConstructors(numTypes);
+  vector<vector<vector<string> > > cvcSelectors(numTypes);
+  vector<vector<vector<CVC3::Expr> > > cvcTypes(numTypes);
+  int i;
+  for (i = 0; i < numTypes; ++i) {
+    cvcNames.push_back(names[i]);
+    cvcSelectors[i].resize(numCons[i]);
+    cvcTypes[i].resize(numCons[i]);
+    for (int j = 0; i < numCons[i]; ++j) {
+      cvcConstructors[i].push_back(constructors[i][j]);
+      for (int k = 0; k < arities[i][j]; ++k) {
+        cvcSelectors[i][j].push_back(selectors[i][j][k]);
+        cvcTypes[i][j].push_back(fromExpr(types[i][j][k]));
+      }
+    }
+  }
+  vector<CVC3::Type> cvcReturnTypes;
+  cvc->dataType(cvcNames, cvcConstructors,
+                cvcSelectors, cvcTypes, cvcReturnTypes);
+  Type* returnTypes = new Type[numTypes];
+  for (i = 0; i < numTypes; ++i) {
+    returnTypes[i] = toType(cvcReturnTypes[i]);
+  }
+  return returnTypes;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_dataTypeN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_arrayType(VC vc, Type typeIndex, Type typeData)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->arrayType(fromType(typeIndex), fromType(typeData)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_arrayType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_bvType(VC vc, int n)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->bitvecType(n));
+  }catch (CVC3::Exception ex){
+    signal_error("vc_bvType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_funType1(VC vc, Type typeDom, Type typeRan)
+{
+  try{
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    return toType(cvc->funType(fromType(typeDom), fromType(typeRan)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_funType1",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_funType2(VC vc, Type a1, Type a2, Type typeRan)
+{
+  try{
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    vector<CVC3::Type> args;
+    args.push_back(fromType(a1));
+    args.push_back(fromType(a2));
+    return toType(cvc->funType(args, fromType(typeRan)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_funType2",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_funType3(VC vc, Type a1, Type a2, Type a3, Type typeRan)
+{
+  try {
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    vector<CVC3::Type> args;
+    args.push_back(fromType(a1));
+    args.push_back(fromType(a2));
+    args.push_back(fromType(a3));
+    return toType(cvc->funType(args, fromType(typeRan)));
+  } catch(CVC3::Exception ex){
+    signal_error("vc_funType3",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_funTypeN(VC vc, Type* a, Type typeRan, int numArgs)
+{
+  try{
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    vector<CVC3::Type> args;
+    for(int i=0; i<numArgs; ++i)
+      args.push_back(fromType(*(a+i)));
+    return toType(cvc->funType(args, fromType(typeRan)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_funTypeN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_createType(VC vc, char* typeName)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->createType(typeName));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_createType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_lookupType(VC vc, char* typeName)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->lookupType(typeName));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_lookupType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+/////////////////////////////////////////////////////////////////////////////
+// Expr manipulation methods                                               //
+/////////////////////////////////////////////////////////////////////////////
+
+
+extern "C" ExprManager vc_getEM(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return (ExprManager)cvc->getEM();
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getEM",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_varExpr(VC vc, char* name, Type type)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->varExpr(name, fromType(type)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_varExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_varExprDef(VC vc, char* name, Type type, Expr def)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->varExpr(name, fromType(type), fromExpr(def)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_varExprDef",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_lookupVar(VC vc, char* name, Type* type)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  CVC3::Type t;
+  Expr e = toExpr(cvc->lookupVar(name, &t));
+  *type = toType(t);
+  return e;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_lookupVar",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_getType(VC vc, Expr e)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->getType(fromExpr(e)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_getBaseType(VC vc, Expr e)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->getBaseType(fromExpr(e)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getBaseType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_getBaseTypeOfType(VC vc, Type t)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toType(cvc->getBaseType(fromType(t)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getBaseTypeOfType",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_getTypePred(VC vc, Type t, Expr e)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->getTypePred(fromType(t), fromExpr(e)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getTypePred",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_stringExpr(VC vc, char* str)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->stringExpr(str));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_stringExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_idExpr(VC vc, char* str)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->idExpr(str));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_idExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_listExpr(VC vc, int numKids, Expr* kids)
+{
+  try{
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    vector<CVC3::Expr> args;
+    for(int i=0; i<numKids; ++i)
+      args.push_back(fromExpr(kids[i]));
+    return toExpr(cvc->listExpr(args));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_listExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" void vc_printExpr(VC vc, Expr e)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  cvc->printExpr(fromExpr(e));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_printExpr",error_int,ex);
+  }
+}
+
+
+extern "C" char* vc_printExprString(VC vc, Expr e)
+{
+  try{
+    ostringstream os;
+    string aa;
+    char*  result;
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    cvc->printExpr(fromExpr(e), os);
+    os.flush();
+    aa=os.str();
+    result=new char[aa.length()+1];
+    strcpy(result,aa.c_str());
+    return result;
+  } catch(CVC3::Exception ex) {
+    signal_error("vc_printExprString",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" void vc_deleteString(char* str)
+{
+  if (str) delete [] str;
+}
+
+
+extern "C" void vc_printExprFile(VC vc, Expr e, int fd)
+{
+  try {
+    stringstream ss;
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    cvc->printExpr(fromExpr(e), ss);
+    string s = ss.str();
+    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<CVC3::Expr> cvcExprs;
+  for (int i = 0; i < numChildren; ++i) {
+    cvcExprs.push_back(fromExpr(children[i]));
+  }
+  return toExpr(cvc->distinctExpr(cvcExprs));
+  }catch(CVC3::Exception ex){
+  signal_error("vc_distinctExpr",error_int,ex);
+  return NULL;
+  }
+}
+
+
+extern "C" Expr vc_trueExpr(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->trueExpr());
+  }catch(CVC3::Exception ex){
+    signal_error("vc_trueExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_falseExpr(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->falseExpr());
+  }catch(CVC3::Exception ex){
+    signal_error("vc_falseExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_notExpr(VC vc, Expr child)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->notExpr(fromExpr(child)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_notExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_andExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->andExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_andExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_andExprN(VC vc, Expr* children, int numChildren)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcExprs;
+  for (int i = 0; i < numChildren; ++i) {
+    cvcExprs.push_back(fromExpr(children[i]));
+  }
+  return toExpr(cvc->andExpr(cvcExprs));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_andExprN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_orExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->orExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_orExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_orExprN(VC vc, Expr* children, int numChildren)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcExprs;
+  for (int i = 0; i < numChildren; ++i) {
+    cvcExprs.push_back(fromExpr(children[i]));
+  }
+  return toExpr(cvc->orExpr(cvcExprs));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_orExprN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->impliesExpr(fromExpr(hyp), fromExpr(conc)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_impliesExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_iffExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->iffExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_iffExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_iteExpr(VC vc, Expr ifpart, Expr thenpart, Expr elsepart)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->iteExpr(fromExpr(ifpart), fromExpr(thenpart),
+			     fromExpr(elsepart)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_iteExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_substExpr(VC vc, Expr e,
+                             Expr* oldTerms, int numOldTerms,
+                             Expr* newTerms, int numNewTerms)
+{
+  try{
+  vector<CVC3::Expr> oldExprs, newExprs;
+  CVC3::Expr ex = fromExpr(e);
+  //CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  for (int i = 0; i < numOldTerms; ++i) {
+    oldExprs.push_back(fromExpr(oldTerms[i]));
+  }
+  for (int i = 0; i < numNewTerms; ++i) {
+    newExprs.push_back(fromExpr(newTerms[i]));
+  }
+  return toExpr(ex.substExpr(oldExprs, newExprs));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_substExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+
+extern "C" Op vc_createOp(VC vc, char* name, Type type)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toOp(vc, cvc->createOp(name, fromType(type)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_createOp",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Op vc_createOpDef(VC vc, char* name, Type type, Expr def)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toOp(vc, cvc->createOp(name, fromType(type), fromExpr(def)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_createOpDef",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Op vc_lookupOp(VC vc, char* name, Type* type)
+{
+  try{
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    CVC3::Type t;
+    Op op = toOp(vc, cvc->lookupOp(name, &t));
+    *type = toType(t);
+    return op;
+  } catch(CVC3::Exception ex){
+    signal_error("vc_lookupOp",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_funExpr1(VC vc, Op op, Expr child)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->funExpr(fromOp(op), fromExpr(child)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_funExpr1",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_funExpr2(VC vc, Op op, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->funExpr(fromOp(op), fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_funExpr2",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_funExpr3(VC vc, Op op, Expr child0, Expr child1,
+			    Expr child2)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->funExpr(fromOp(op), fromExpr(child0), fromExpr(child1),
+			     fromExpr(child2)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_funExpr3",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_funExprN(VC vc, Op op, Expr* children, int numChildren)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcExprs;
+  for (int i = 0; i < numChildren; ++i) {
+    cvcExprs.push_back(fromExpr(children[i]));
+  }
+  return toExpr(cvc->funExpr(fromOp(op), cvcExprs));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_funExprN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_ratExpr(VC vc, int n, int d)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->ratExpr(n, d));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_ratExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_ratExprFromStr(VC vc, char* n, char* d, int base)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->ratExpr(n, d, base));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_ratExprFromStr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_ratExprFromStr1(VC vc, char* n, int base)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->ratExpr(n, base));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_ratExprFromStr1",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_uminusExpr(VC vc, Expr child)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->uminusExpr(fromExpr(child)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_uminusExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_plusExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->plusExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_plusExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+extern "C" Expr vc_plusExprN(VC vc, Expr* children, int numChildren)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcExprs;
+  for (int i = 0; i < numChildren; ++i) {
+    cvcExprs.push_back(fromExpr(children[i]));
+  }
+  return toExpr(cvc->plusExpr(cvcExprs));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_plusExprN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_minusExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->minusExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_minusExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_multExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->multExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_multExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_powExpr(VC vc, Expr pow, Expr base)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->powExpr(fromExpr(pow), fromExpr(base)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_powExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_divideExpr(VC vc, Expr numerator, Expr denominator)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->divideExpr(fromExpr(numerator), fromExpr(denominator)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_divideExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_ltExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->ltExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_ltExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_leExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->leExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_leExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_gtExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->gtExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_gtExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_geExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->geExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_geExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_recordExpr1(VC vc, char* field, Expr expr)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->recordExpr(field, fromExpr(expr)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_recordExpr1",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_recordExpr2(VC vc, char* field0, Expr expr0,
+			              char* field1, Expr expr1)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->recordExpr(field0, fromExpr(expr0),
+				field1, fromExpr(expr1)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_recordExpr2",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_recordExpr3(VC vc, char* field0, Expr expr0,
+			              char* field1, Expr expr1,
+			              char* field2, Expr expr2)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->recordExpr(field0, fromExpr(expr0),
+				field1, fromExpr(expr1),
+				field2, fromExpr(expr2)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_recordExpr3",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_recordExprN(VC vc, char** fields, Expr* exprs,
+			       int numFields)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<std::string> cvcFields;
+  vector<CVC3::Expr> cvcExprs;
+  for (int i = 0; i < numFields; ++i) {
+    cvcFields.push_back(fields[i]);
+    cvcExprs.push_back(fromExpr(exprs[i]));
+  }
+  return toExpr(cvc->recordExpr(cvcFields, cvcExprs));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_recordExprN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_recSelectExpr(VC vc, Expr record, char* field)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->recSelectExpr(fromExpr(record), field));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_recSelectExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_recUpdateExpr(VC vc, Expr record, char* field,
+				 Expr newValue)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->recUpdateExpr(fromExpr(record), field,
+				   fromExpr(newValue)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_recUpdateExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_readExpr(VC vc, Expr array, Expr index)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->readExpr(fromExpr(array), fromExpr(index)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_readExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->writeExpr(fromExpr(array), fromExpr(index),
+			       fromExpr(newValue)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_writeExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_bv32Type(VC vc)
+{
+  return vc_bvType(vc, 32);
+}
+
+
+extern "C" Expr vc_bvConstExprFromStr(VC vc, char* binary_repr)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->parseExpr(cvc->listExpr("_BVCONST", cvc->stringExpr(binary_repr))));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvConstExpr",error_int, ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value)
+{
+  char* s = val_to_binary_str(n_bits, value);
+  return vc_bvConstExprFromStr(vc, s);
+}
+
+
+extern "C" Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value)
+{
+  return vc_bvConstExprFromInt(vc, 32, value);
+}
+
+
+extern "C" Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long value)
+{
+  char* s = val_to_binary_str(n_bits, value);
+  return vc_bvConstExprFromStr(vc, s);
+}
+
+
+extern "C" Expr vc_bvConcatExpr(VC vc, Expr left, Expr right) {
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newConcatExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception &ex){
+    signal_error("vc_bvConcatExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvConcatExprN(VC vc, Expr* children, int numChildren) {
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcExprs;
+  for (int i = 0; i < numChildren; ++i) {
+    cvcExprs.push_back(fromExpr(children[i]));
+  }
+  return toExpr(cvc->newConcatExpr(cvcExprs));
+  }catch(CVC3::Exception &ex){
+    signal_error("vc_concatExprN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, int low_bit_no)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVExtractExpr(fromExpr(child), high_bit_no, low_bit_no));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvExtract",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvBoolExtract(VC vc, Expr child, int bit_no)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  CVC3::Expr lExpr = cvc->listExpr("_BOOLEXTRACT", fromExpr(child), cvc->ratExpr(bit_no));
+  return toExpr(cvc->parseExpr(lExpr));
+
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvBoolExtract",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvNotExpr(VC vc, Expr child)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVNegExpr(fromExpr(child)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvNotExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvAndExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVAndExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvAndExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvOrExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVOrExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvOrExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvXorExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVXorExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvXorExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvLtExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVLTExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvLtExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvLeExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVLEExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvLeExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvGtExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  CVC3::Expr lExpr = cvc->listExpr("_BVGT", fromExpr(left), fromExpr(right));
+  return toExpr(cvc->parseExpr(lExpr));
+
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvGtExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvGeExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  CVC3::Expr lExpr = cvc->listExpr("_BVGE", fromExpr(left), fromExpr(right));
+  return toExpr(cvc->parseExpr(lExpr));
+
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvGeExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvSLtExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVSLTExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvSLtExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvSLeExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVSLEExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvSLeExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvSGtExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  CVC3::Expr lExpr = cvc->listExpr("_BVSGT", fromExpr(left), fromExpr(right));
+  return toExpr(cvc->parseExpr(lExpr));
+
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvSGtExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvSGeExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  CVC3::Expr lExpr = cvc->listExpr("_BVSGE", fromExpr(left), fromExpr(right));
+  return toExpr(cvc->parseExpr(lExpr));
+
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvSGeExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvSignExtend(VC vc, Expr child, int nbits)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newSXExpr(fromExpr(child), nbits));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvSignExtend",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvUMinusExpr(VC vc, Expr child)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVUminusExpr(fromExpr(child)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvUMinusExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> args;
+  args.push_back(fromExpr(left));
+  args.push_back(fromExpr(right));
+  return toExpr(cvc->newBVPlusExpr(n_bits, args));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvPlusExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right)
+{
+  return vc_bvPlusExpr(vc, 32, left, right);
+}
+
+
+extern "C" Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  CVC3::Expr lExpr = cvc->listExpr("_BVSUB", cvc->ratExpr(n_bits), fromExpr(left), fromExpr(right));
+   return toExpr(cvc->parseExpr(lExpr));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvMinusExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right)
+{
+  return vc_bvMinusExpr(vc, 32, left, right);
+}
+
+
+extern "C" Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVMultExpr(n_bits, fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvMultExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bv32MultExpr(VC vc, Expr left, Expr right)
+{
+  return vc_bvMultExpr(vc, 32, left, right);
+}
+
+
+extern "C" Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newFixedLeftShiftExpr(fromExpr(child), sh_amt));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvLeftShiftExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newFixedRightShiftExpr(fromExpr(child), sh_amt));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvRightShiftExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+extern "C" Expr vc_bvUDivExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVUDivExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvUDivExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+extern "C" Expr vc_bvURemExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVURemExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvURemExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+extern "C" Expr vc_bvSDivExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVSDivExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvSDivExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+extern "C" Expr vc_bvSRemExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVSRemExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvSRemExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+extern "C" Expr vc_bvSModExpr(VC vc, Expr left, Expr right)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->newBVSModExpr(fromExpr(left), fromExpr(right)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvSModExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+/* Same as vc_bvLeftShift only that the answer in 32 bits long */
+extern "C" Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child) {
+  return vc_bvExtract(vc, vc_bvLeftShiftExpr(vc, sh_amt, child), 31, 0);
+}
+
+
+/* Same as vc_bvRightShift only that the answer in 32 bits long */
+extern "C" Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child) {
+  return vc_bvExtract(vc, vc_bvRightShiftExpr(vc, sh_amt, child), 31, 0);
+}
+
+extern "C" Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child) {
+  try{
+  Expr ifpart;
+  Expr thenpart;
+  Expr elsepart = vc_trueExpr(vc);
+  Expr ite = vc_trueExpr(vc);
+
+  for(int count=32; count >= 0; count--){
+    if(count != 32) {
+      ifpart = vc_eqExpr(vc, sh_amt,
+			 vc_bvConstExprFromInt(vc, 32, count));
+      thenpart = vc_bvExtract(vc,
+			      vc_bvLeftShiftExpr(vc, count, child),
+			      31, 0);
+
+      ite = vc_iteExpr(vc,ifpart,thenpart,elsepart);
+      elsepart = ite;
+    } else {
+      elsepart = vc_bvConstExprFromInt(vc,32, 0);
+    }
+  }
+  return ite;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvVar32LeftShiftExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs) {
+  try{
+  Expr ifpart;
+  Expr thenpart;
+  Expr elsepart = vc_trueExpr(vc);
+  Expr ite = vc_trueExpr(vc);
+
+  for(int count=32; count >= 0; count--){
+    if(count != 32) {
+      ifpart = vc_eqExpr(vc, rhs,
+			 vc_bvConstExprFromInt(vc, 32, 1 << count));
+      thenpart = vc_bvRightShiftExpr(vc, count, child);
+      ite = vc_iteExpr(vc,ifpart,thenpart,elsepart);
+      elsepart = ite;
+    } else {
+      elsepart = vc_bvConstExprFromInt(vc,32, 0);
+    }
+  }
+  return ite;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvVar32DivByPowOfTwoExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child)
+{
+  try{
+  Expr ifpart;
+  Expr thenpart;
+  Expr elsepart = vc_trueExpr(vc);
+  Expr ite = vc_trueExpr(vc);
+
+  for(int count=32; count >= 0; count--){
+    if(count != 32) {
+      ifpart = vc_eqExpr(vc, sh_amt,
+			 vc_bvConstExprFromInt(vc, 32, count));
+      thenpart = vc_bvRightShiftExpr(vc, count, child);
+      ite = vc_iteExpr(vc,ifpart,thenpart,elsepart);
+      elsepart = ite;
+    } else {
+      elsepart = vc_bvConstExprFromInt(vc,32, 0);
+    }
+  }
+  return ite;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_bvVar32LeftShiftExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+/* C pointer support: C interface to support C memory arrays in CVC3 */
+extern "C" Expr vc_bvCreateMemoryArray(VC vc, char * arrayName) {
+  Type bv8  = vc_bvType(vc,8);
+  Type bv32 = vc_bvType(vc,32);
+
+  Type malloced_mem0 = vc_arrayType(vc,bv32,bv8);
+  return vc_varExpr(vc, arrayName, malloced_mem0);
+}
+
+/*OLD VERSIONS C pointer theory functions. DO NOT DELETE */
+
+// //Warning: Type checking needed to ensure that the function is run
+// //correctly is not being done. it is assumed that the function
+// //recieves inputs of the correct types
+// extern "C" Expr vc_bvReadMemoryArray(VC vc,
+// 				     Expr array,
+// 				     Expr byteIndex, int newBitsPerElem) {
+//   DebugAssert(newBitsPerElem%8 == 0,
+// 	      "new bits per element must be a multiple of 8\n");
+
+//   Expr numerator = vc_bvMultExpr(vc,32,
+// 				 vc_bvConstExprFromInt(vc,32,newBitsPerElem),
+// 				 byteIndex);
+//   int numOfBytes = newBitsPerElem/8;
+//   DebugAssert(numOfBytes > 0,
+// 	      "numOfBytes must be greater than 0");
+
+//   if(numOfBytes == 1)
+//     return vc_readExpr(vc,array,numerator);
+//   else {
+//     int count = 1;
+//     Expr a = vc_readExpr(vc,array,numerator);
+//     while(--numOfBytes > 0) {
+//       Expr b = vc_readExpr(vc,array,
+// 			   vc_bvPlusExpr(vc,32,numerator,vc_bvConstExprFromInt(vc,32,count)));
+//       a = vc_bvConcatExpr(vc,a,b);
+//       count++;
+//     }
+//     return a;
+//   }
+// }
+
+// extern "C" Expr vc_bvWriteToMemoryArray(VC vc,
+// 					Expr array, Expr byteIndex,
+// 					Expr element, int newBitsPerElem) {
+//   DebugAssert(newBitsPerElem%8 == 0,
+// 	      "new bits per element must be a multiple of 8\n");
+
+//   Expr numerator = vc_bvMultExpr(vc,32,
+// 				 vc_bvConstExprFromInt(vc,32,newBitsPerElem),
+// 				 byteIndex);
+//   int numOfBytes = newBitsPerElem/8;
+//   DebugAssert(numOfBytes > 0,
+// 	      "numOfBytes must be greater than 0");
+
+//   if(numOfBytes == 1)
+//     return vc_writeExpr(vc,array,numerator, element);
+//   else {
+//     int count = 1;
+//     int hi = newBitsPerElem - 1;
+//     int low = newBitsPerElem - 8;
+//     Expr c = vc_bvExtract(vc,element,hi,low);
+//     Expr newarray = vc_writeExpr(vc,array,numerator,c);
+//     while(--numOfBytes > 0) {
+//       hi = low-1;
+//       low = low-8;
+//       c = vc_bvExtract(vc,element,hi,low);
+//       newarray = vc_writeExpr(vc,newarray,numerator,c);
+//       count++;
+//     }
+//     return newarray;
+//   }
+// }
+
+
+extern "C" Expr vc_bvReadMemoryArray(VC vc,
+				     Expr array,
+				     Expr byteIndex, int numOfBytes) {
+
+  DebugAssert(0 < numOfBytes,
+	      "number of Bytes must be greater than 0\n");
+
+  if(numOfBytes == 1)
+    return vc_readExpr(vc,array,byteIndex);
+  else {
+    int count = 1;
+    Expr a = vc_readExpr(vc,array,byteIndex);
+    while(--numOfBytes > 0) {
+      Expr b = vc_readExpr(vc,array,
+			   /*vc_simplify(vc, */
+				       vc_bvPlusExpr(vc, 32,
+						     byteIndex,
+						     vc_bvConstExprFromInt(vc,32,count)))/*)*/;
+      a = vc_bvConcatExpr(vc,b,a);
+      count++;
+    }
+    return a;
+  }
+}
+
+
+extern "C" Expr vc_bvWriteToMemoryArray(VC vc,
+					Expr array, Expr byteIndex,
+					Expr element, int numOfBytes) {
+  DebugAssert(numOfBytes > 0,
+	      "numOfBytes must be greater than 0");
+
+  int newBitsPerElem = numOfBytes*8;
+  if(numOfBytes == 1)
+    return vc_writeExpr(vc, array, byteIndex, element);
+  else {
+    int count = 1;
+    int hi = newBitsPerElem - 1;
+    int low = newBitsPerElem - 8;
+    int low_elem = 0;
+    int hi_elem = low_elem + 7;
+    Expr c = vc_bvExtract(vc, element, hi_elem, low_elem);
+    Expr newarray = vc_writeExpr(vc, array, byteIndex, c);
+    while(--numOfBytes > 0) {
+      hi = low-1;
+      low = low-8;
+
+      low_elem = low_elem + 8;
+      hi_elem = low_elem + 7;
+
+      c = vc_bvExtract(vc, element, hi_elem, low_elem);
+      newarray =
+	vc_writeExpr(vc, newarray,
+		     vc_bvPlusExpr(vc, 32, byteIndex, vc_bvConstExprFromInt(vc,32,count)),
+		     c);
+      count++;
+    }
+    return newarray;
+  }
+}
+
+extern "C" Expr vc_tupleExprN(VC vc, Expr* children, int numChildren)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcExprs;
+  for (int i = 0; i < numChildren; ++i) {
+    cvcExprs.push_back(fromExpr(children[i]));
+  }
+  return toExpr(cvc->tupleExpr(cvcExprs));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_tupleExprN",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_tupleSelectExpr(VC vc, Expr tuple, int index)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->tupleSelectExpr(fromExpr(tuple), index));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_tupleSelectExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_tupleUpdateExpr(VC vc, Expr tuple, int index, Expr newValue)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->tupleUpdateExpr(fromExpr(tuple), index,
+                                     fromExpr(newValue)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_tupleUpdateExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_datatypeConsExpr(VC vc, char* constructor,
+                                    int numArgs, Expr* args)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcArgs;
+  for (int i = 0; i < numArgs; ++i) {
+    cvcArgs.push_back(fromExpr(args[i]));
+  }
+  return toExpr(cvc->datatypeConsExpr(constructor, cvcArgs));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_datatypeConsExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_datatypeSelExpr(VC vc, char* selector, Expr arg)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->datatypeSelExpr(selector, fromExpr(arg)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_datatypeSelExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_datatypeTestExpr(VC vc, char* constructor, Expr arg)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->datatypeTestExpr(constructor, fromExpr(arg)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_datatypeTestExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_boundVarExpr(VC vc, char* name, char *uid, Type type)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->boundVarExpr(name, uid, fromType(type)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getEM",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Type vc_forallExpr(VC vc, Expr* Bvars, int numBvars, Expr f)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcBvars;
+  for (int i = 0; i < numBvars; ++i) {
+    cvcBvars.push_back(fromExpr(Bvars[i]));
+  }
+  return toExpr(cvc->forallExpr(cvcBvars,fromExpr(f)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_forallExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+// triggers must be an array of listExpr
+// each listExpr represent a trigger
+// if a listExpr contains more than one Expr, then it is a multi-trigger
+extern "C" void vc_setTriggers(VC vc, Expr e, int numTrigs, Expr* triggers)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<vector<CVC3::Expr> >cvcTriggers;
+  for (int i = 0; i < numTrigs; ++i) {
+    vector<CVC3::Expr> curTrig;
+    CVC3::Expr trigExpr = fromExpr(triggers[i]);
+    if(trigExpr.isRawList()){
+      for(int j = 0 ; j < trigExpr.arity(); j++){
+       curTrig.push_back(trigExpr[j]);
+      }
+    }
+    else{
+      curTrig.push_back(trigExpr);
+    }
+    cvcTriggers.push_back(curTrig);
+  } 
+  
+  cvc->setTriggers(fromExpr(e), cvcTriggers);
+  }catch(CVC3::Exception ex){
+    signal_error("vc_setTriggers",error_int,ex);
+  }
+}
+
+
+extern "C" Expr vc_existsExpr(VC vc, Expr* Bvars, int numBvars, Expr f)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcBvars;
+  for (int i = 0; i < numBvars; ++i) {
+    cvcBvars.push_back(fromExpr(Bvars[i]));
+  }
+  return toExpr(cvc->existsExpr(cvcBvars,fromExpr(f)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_existsExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Op vc_lambdaExpr(VC vc, int numVars, Expr* vars, Expr body)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcVars;
+  for (int i = 0; i < numVars; ++i) {
+    cvcVars.push_back(fromExpr(vars[i]));
+  }
+  return toOp(vc, cvc->lambdaExpr(cvcVars, fromExpr(body)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_lambdaExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+/////////////////////////////////////////////////////////////////////////////
+// Context-related methods                                                 //
+/////////////////////////////////////////////////////////////////////////////
+
+
+extern "C" void vc_setResourceLimit(VC vc, unsigned limit)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  cvc->setResourceLimit(limit);
+  }catch(CVC3::Exception ex){
+    signal_error("vc_setResourceLimit",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_assertFormula(VC vc, Expr e)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  cvc->assertFormula(fromExpr(e));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_assertFormula",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_registerAtom(VC vc, Expr e)
+{
+  try{
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    cvc->registerAtom(fromExpr(e));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_registerAtom",error_int,ex);
+  }
+}
+
+
+extern "C" Expr vc_getImpliedLiteral(VC vc)
+{
+  try {
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    return toExpr(cvc->getImpliedLiteral());
+  } catch(CVC3::Exception ex){
+    signal_error("vc_getImpliedLiteral",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_simplify(VC vc, Expr e)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->simplify(fromExpr(e)));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_simplify",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" int vc_query(VC vc, Expr e)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return (int)cvc->query(fromExpr(e));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_query",error_int,ex);
+    return error_int;
+  }
+}
+
+
+extern "C" int vc_checkContinue(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return (int)cvc->checkContinue();
+  }catch(CVC3::Exception ex){
+    signal_error("vc_checkContinue",error_int,ex);
+    return error_int;
+  }
+}
+
+
+extern "C" int vc_restart(VC vc, Expr e)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return (int)cvc->restart(fromExpr(e));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_restart",error_int,ex);
+    return error_int;
+  }
+}
+
+
+extern "C" void vc_returnFromCheck(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  cvc->returnFromCheck();
+  }catch(CVC3::Exception ex){
+    signal_error("vc_returnFromCheck",error_int,ex);
+  }
+}
+
+
+extern "C" Expr* vc_getUserAssumptions(VC vc, int* size)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcAssumptions;
+  cvc->getUserAssumptions(cvcAssumptions);
+  Expr* assumptions = new Expr[cvcAssumptions.size()];
+  unsigned n = 0;
+  for (; n < cvcAssumptions.size(); ++n) {
+    assumptions[n] = toExpr(cvcAssumptions[n]);
+  }
+  *size = int(n);
+  return assumptions;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getUserAssumptions",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr* vc_getInternalAssumptions(VC vc, int* size)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcAssumptions;
+  cvc->getInternalAssumptions(cvcAssumptions);
+  Expr* assumptions = new Expr[cvcAssumptions.size()];
+  unsigned n = 0;
+  for (; n < cvcAssumptions.size(); ++n) {
+    assumptions[n] = toExpr(cvcAssumptions[n]);
+  }
+  *size = int(n);
+  return assumptions;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getInternalAssumptions",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr* vc_getAssumptions(VC vc, int* size)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcAssumptions;
+  cvc->getAssumptions(cvcAssumptions);
+  Expr* assumptions = new Expr[cvcAssumptions.size()];
+  unsigned n = 0;
+  for (; n < cvcAssumptions.size(); ++n) {
+    assumptions[n] = toExpr(cvcAssumptions[n]);
+  }
+  *size = int(n);
+  return assumptions;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getAssumptions",error_int,ex);
+    return NULL;
+  }
+}
+
+//yeting, this is for proof translation,
+extern "C" Expr vc_getProofAssumptions(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcAssumptions;
+  cvc->getUserAssumptions(cvcAssumptions);
+  return toExpr(cvc->listExpr(cvcAssumptions));
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getProofAssumptions",error_int,ex);
+    return NULL;
+  }
+}
+
+//yeting, this is for proof translation
+extern "C" Expr vc_getProofQuery(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->getProofQuery());
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getProofQuery",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr* vc_getAssumptionsUsed(VC vc, int* size)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcAssumptions;
+  cvc->getAssumptionsUsed(cvcAssumptions);
+  Expr* assumptions = new Expr[cvcAssumptions.size()];
+  unsigned n = 0;
+  for (; n < cvcAssumptions.size(); ++n) {
+    assumptions[n] = toExpr(cvcAssumptions[n]);
+  }
+  *size = int(n);
+  return assumptions;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getAssumptionsUsed",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr* vc_getCounterExample(VC vc, int* size)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcAssumptions;
+  cvc->getCounterExample(cvcAssumptions);
+  Expr* assumptions = new Expr[cvcAssumptions.size()];
+  unsigned n = 0;
+  for (; n < cvcAssumptions.size(); ++n) {
+    assumptions[n] = toExpr(cvcAssumptions[n]);
+  }
+  *size = int(n);
+  return assumptions;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getCounterExample",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr* vc_getConcreteModel(VC vc, int* size)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  CVC3::ExprMap<CVC3::Expr> assertions;
+  cvc->getConcreteModel(assertions);
+  Expr* locAssumptions = new Expr[assertions.size()];
+  int n = 0;
+  CVC3::ExprMap<CVC3::Expr>::iterator it = assertions.begin(), end = assertions.end();
+  for (; it != end; it++) {
+    locAssumptions[n] = toExpr(cvc->eqExpr(it->first, it->second));
+    n++;
+  }
+  *size = n;
+  return locAssumptions;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getConcreteModel",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" int vc_inconsistent(VC vc, Expr** assumptions, int* size)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> assertions;
+  bool ret = cvc->inconsistent(assertions);
+  Expr* locAssumptions = new Expr[assertions.size()];
+  for (unsigned i = 0; i < assertions.size(); ++i) {
+    locAssumptions[i] = toExpr(assertions[i]);
+  }
+  *assumptions = locAssumptions;
+  *size = assertions.size();
+  return (int)ret;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_inconsistent",error_int,ex);
+    return 0;
+  }
+}
+
+
+extern "C" char* vc_incomplete(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<string> reasons;
+  bool ret = cvc->incomplete(reasons);
+  if (!ret) return NULL;
+  string allReasons = "";
+  for (unsigned i = 0; i < reasons.size(); ++i) {
+    allReasons += '\n';
+    allReasons += reasons[i];
+  }
+  char* retStr = new char[allReasons.length()+1];
+  allReasons.copy(retStr, allReasons.length());
+  retStr[allReasons.length()] = '\0';
+  return retStr;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_incomplete",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_getProof(VC vc)
+{
+  signal_error("vc_getProofTCC",error_int,CVC3::Exception("Unimplemented"));
+  return NULL;
+}
+
+
+extern "C" Expr vc_getProofOfFile(VC vc, char* fileName){
+  signal_error("vc_getProofTCC",error_int,CVC3::Exception("Unimplemented"));
+  return NULL;
+}
+
+
+extern "C" Expr vc_getTCC(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->getTCC());
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getTCC",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr* vc_getAssumptionsTCC(VC vc, int* size)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  vector<CVC3::Expr> cvcAssumptions;
+  cvc->getAssumptionsTCC(cvcAssumptions);
+  Expr* assumptions = new Expr[cvcAssumptions.size()];
+  unsigned n = 0;
+  for (; n < cvcAssumptions.size(); ++n) {
+    assumptions[n] = toExpr(cvcAssumptions[n]);
+  }
+  *size = int(n);
+  return assumptions;
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getAssumptionsTCC",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_getProofTCC(VC vc)
+{
+  signal_error("vc_getProofTCC",error_int,CVC3::Exception("Unimplemented"));
+  return NULL;
+}
+
+
+extern "C" Expr vc_getClosure(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return toExpr(cvc->getClosure());
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getClosure",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_getProofClosure(VC vc)
+{
+  signal_error("vc_getProofTCC",error_int,CVC3::Exception("Unimplemented"));
+  return NULL;
+}
+
+
+extern "C" int vc_stackLevel(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return cvc->stackLevel();
+  }catch(CVC3::Exception ex){
+    signal_error("vc_stackLevel",error_int,ex);
+    return 0;
+  }
+}
+
+
+extern "C" void vc_push(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  cvc->push();
+  }catch(CVC3::Exception ex){
+    signal_error("vc_push",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_pop(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  cvc->pop();
+  }catch(CVC3::Exception ex){
+    signal_error("vc_pop",error_int,ex);
+  }
+}
+
+
+extern "C" void vc_popto(VC vc, int stackLevel)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  cvc->popto(stackLevel);
+  }catch(CVC3::Exception ex){
+    signal_error("vc_popto",error_int,ex);
+  }
+}
+
+
+extern "C" Context vc_getCurrentContext(VC vc)
+{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  return (Context)cvc->getCurrentContext();
+}
+
+
+// -------------------------------------------------------------------------
+//  Util
+// -------------------------------------------------------------------------
+
+
+extern "C" int vc_compare_exprs(Expr e1,Expr e2){
+  try{
+    return (compare(fromExpr(e1),fromExpr(e2)));
+  } catch (CVC3::Exception ex){
+    signal_error("vc_compare_exprs",error_int,ex);
+    return error_int;
+  }
+}
+
+
+extern "C" const char* vc_exprString(Expr e){
+  try{
+    tmpString =(fromExpr(e)).toString();
+    return tmpString.c_str();
+  } catch (CVC3::Exception ex){
+    signal_error("vc_exprString",error_int,ex);
+    return "ERROR";
+  }
+}
+
+
+extern "C" const char* vc_typeString(Type t){
+  try{
+    tmpString = (fromExpr(t)).toString();
+    return tmpString.c_str();
+  } catch (CVC3::Exception ex){
+    signal_error("vc_typeString",error_int,ex);
+    return "ERROR";
+  }
+}
+
+
+extern "C" bool vc_isClosure(Expr e){
+  signal_error("vc_isClosure",error_int,CVC3::Exception("Unimplemented"));
+  return false;
+}
+
+
+extern "C" bool vc_isQuantifier(Expr e){
+  signal_error("vc_isQuantifier",error_int,CVC3::Exception("Unimplemented"));
+  return false;
+}
+
+
+extern "C" bool vc_isLambda(Expr e){
+  signal_error("vc_isLambda",error_int,CVC3::Exception("Unimplemented"));
+  return false;
+}
+
+
+extern "C" bool vc_isVar(Expr e){
+  try{
+    return (fromExpr(e)).isVar();
+  } catch (CVC3::Exception ex){
+    signal_error("vc_isVar",error_int,ex);
+    return false;
+  }
+}
+
+
+extern "C" int vc_arity(Expr e){
+  try{
+    return (fromExpr(e)).arity();
+  } catch (CVC3::Exception ex){
+    signal_error("vc_arity",error_int,ex);
+    return error_int;
+  }
+}
+
+
+extern "C" int vc_getKind(Expr e){
+  try{
+    return (fromExpr(e)).getKind();
+  } catch (CVC3::Exception ex){
+    signal_error("vc_getKind",error_int,ex);
+    return error_int;
+  }
+}
+
+
+extern "C" Expr vc_getChild(Expr e, int i){
+  try{
+    return toExpr(((fromExpr(e))[i]));
+  } catch (CVC3::Exception ex){
+    signal_error("vc_getChild",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" int vc_getNumVars(Expr e){
+  signal_error("vc_getNumVars",error_int,CVC3::Exception("Unimplemented"));
+  return 0;
+}
+
+
+extern "C" Expr vc_getVar(Expr e, int i){
+  signal_error("vc_getVar",error_int,CVC3::Exception("Unimplemented"));
+  return 0;
+}
+
+
+extern "C" Expr vc_getBody(Expr e){
+  signal_error("vc_getBody",error_int,CVC3::Exception("Unimplemented"));
+  return 0;
+}
+
+extern "C" Expr vc_getExistential(Expr e){
+  signal_error("vc_getExistential",error_int,CVC3::Exception("Unimplemented"));
+  return 0;
+}
+
+
+extern "C" Expr vc_getFun(VC vc, Expr e)
+{
+  try{
+    return toExpr((fromExpr(e)).getOp().getExpr());
+  }catch(CVC3::Exception ex){
+    signal_error("vc_getFun",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" Expr vc_toExpr(Type t){
+  try{
+    return toExpr(fromExpr(t));
+  } catch (CVC3::Exception ex){
+    signal_error("vc_toExpr",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" const char* vc_getKindString(VC vc,int kind)
+{
+  try{
+  tmpString = CVC4::kind::kindToString(CVC4::Kind(kind));
+  return tmpString.c_str();
+  } catch (CVC3::Exception ex){
+    signal_error("vc_getKindString",error_int,ex);
+    return NULL;
+  }
+}
+
+
+extern "C" int vc_getKindInt(VC vc,char* kind_name)
+{
+  signal_error("vc_getKindInt",error_int,CVC3::Exception("Unimplemented"));
+  return 0;
+}
+
+
+extern "C" int vc_getInt(Expr e){
+  try{
+    CVC3::Expr ex = fromExpr(e);
+    if(ex.getKind() == CVC4::kind::CONST_INTEGER) {
+      return int(ex.getConst<CVC3::Integer>().getLong());
+    } else {
+      return int(ex.getConst<CVC3::Rational>().getNumerator().getLong());
+    }
+  } catch (CVC3::Exception ex){
+    signal_error("vc_getInt",error_int,ex);
+    return error_int;
+  }
+}
+
+
+extern "C" int vc_getBVInt(VC vc, Expr e){
+  try{
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    return int(cvc->computeBVConst(fromExpr(e)).getNumerator().getLong());
+  } catch (CVC3::Exception ex){
+    signal_error("vc_getBVInt",error_int,ex);
+    return 0;
+  }
+}
+
+
+extern "C" unsigned int vc_getBVUnsigned(VC vc, Expr e){
+  try{
+    CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+    return unsigned(cvc->computeBVConst(fromExpr(e)).getNumerator().getUnsignedLong());
+  } catch (CVC3::Exception ex){
+    signal_error("vc_getBVUnsigned",error_int,ex);
+    return 0;
+  }
+}
+
+
+extern "C" void vc_print_statistics(VC vc)
+{
+  try{
+  CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
+  cvc->printStatistics();
+  } catch (CVC3::Exception ex){
+    signal_error("vc_print_statistics",error_int,ex);
+  }
+}
diff --git a/src/bindings/compat/c/c_interface.h b/src/bindings/compat/c/c_interface.h
new file mode 100644
index 000000000..a836e8bca
--- /dev/null
+++ b/src/bindings/compat/c/c_interface.h
@@ -0,0 +1,696 @@
+/*****************************************************************************/
+/*!
+ * \file c_interface.h
+ *
+ * Authors: Clark Barrett
+ *          Cristian Cadar
+ *
+ * Created: Thu Jun  5 10:34:02 2003
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ *
+ * <hr>
+ *
+ */
+/*****************************************************************************/
+
+#ifndef _cvc3__include__c_interface_h_
+#define _cvc3__include__c_interface_h_
+
+#include "c_interface_defs.h"
+
+//! Flags can be NULL
+VC vc_createValidityChecker(Flags flags);
+//! Create validity checker's flags
+Flags vc_createFlags();
+//! Destroy the validity checker.
+/*! Must be called after all other objects are deleted, except the flags */
+void vc_destroyValidityChecker(VC vc);
+//! Delete the flags
+void vc_deleteFlags(Flags flags);
+//! Delete type
+void vc_deleteType(Type t);
+//! Delete expression
+void vc_deleteExpr(Expr e);
+//! Delete operator
+void vc_deleteOp(Op op);
+//! Delete vector of expressions
+void vc_deleteVector(Expr* e);
+//! Delete vector of types
+void vc_deleteTypeVector(Type* e);
+
+// Setting the flags
+//! Set a boolean flag to true or false
+void vc_setBoolFlag(Flags flags, char* name, int val);
+//! Set an integer flag to the given value
+void vc_setIntFlag(Flags flags, char* name, int val);
+//! Set a string flag to the given value
+void vc_setStringFlag(Flags flags, char* name, char* val);
+//! Add a (string, bool) pair to the multy-string flag
+void vc_setStrSeqFlag(Flags flags, char* name, char* str, int val);
+
+// Basic types
+Type vc_boolType(VC vc);
+Type vc_realType(VC vc);
+Type vc_intType(VC vc);
+
+//! Create a subrange type
+Type vc_subRangeType(VC vc, int lowerEnd, int upperEnd);
+
+//! Creates a subtype defined by the given predicate
+/*!
+ * \param pred is a predicate taking one argument of type T and returning
+ * Boolean.  The resulting type is a subtype of T whose elements x are those
+ * satisfying the predicate pred(x).
+ *
+ * \param witness is an expression of type T for which pred holds (if a Null
+ *  expression is passed as a witness, cvc will try to prove \f$\exists x. pred(x))\f$.
+ *  if the witness check fails, a TypecheckException is thrown.
+ */
+Type vc_subtypeType(VC vc, Expr pred, Expr witness);
+
+// Tuple types
+Type vc_tupleType2(VC vc, Type type0, Type type1);
+Type vc_tupleType3(VC vc, Type type0, Type type1, Type type2);
+//! Create a tuple type.  'types' is an array of types of length numTypes.
+Type vc_tupleTypeN(VC vc, Type* types, int numTypes);
+
+// Record types
+Type vc_recordType1(VC vc, char* field, Type type);
+Type vc_recordType2(VC vc, char* field0, Type type0,
+                           char* field1, Type type1);
+Type vc_recordType3(VC vc, char* field0, Type type0,
+	                   char* field1, Type type1,
+	                   char* field2, Type type2);
+//! Create a record type.
+/*! 'fields' and 'types' are arrays of length numFields. */
+Type vc_recordTypeN(VC vc, char** fields, Type* types, int numFields);
+
+// Datatypes
+
+//! Single datatype, single constructor
+/*! The types are either type exressions (obtained from a type with
+ *  getExpr()) or string expressions containing the name of (one of) the
+ *  dataType(s) being defined. */
+Type vc_dataType1(VC vc, char* name, char* constructor, int arity,
+                  char** selectors, Expr* types);
+
+//! Single datatype, multiple constructors
+/*! The types are either type exressions (obtained from a type with
+ *  getExpr()) or string expressions containing the name of (one of) the
+ *  dataType(s) being defined. */
+Type vc_dataTypeN(VC vc, char* name, int numCons, char** constructors,
+                  int* arities, char*** selectors, Expr** types);
+
+//! Multiple datatypes
+/*! The types are either type exressions (obtained from a type with
+ *  getExpr()) or string expressions containing the name of (one of) the
+ *  dataType(s) being defined.
+ *  Returns an array of size numTypes which must be freed by calling
+ *  vc_deleteTypeVector.
+ */
+Type* vc_dataTypeMN(VC vc, int numTypes, char** names,
+                    int* numCons, char*** constructors,
+                    int** arities, char**** selectors,
+                    Expr*** types);
+
+//! Create an array type
+Type vc_arrayType(VC vc, Type typeIndex, Type typeData);
+
+//! Create a bitvector type of length n
+Type vc_bvType(VC vc, int n);
+
+//! Create a function type with 1 argument
+Type vc_funType1(VC vc, Type a1, Type typeRan);
+//! Create a function type with 2 arguments
+Type vc_funType2(VC vc, Type a1, Type a2, Type typeRan);
+//! Create a function type with 3 arguments
+Type vc_funType3(VC vc, Type a1, Type a2, Type a3, Type typeRan);
+//! Create a function type with N arguments
+Type vc_funTypeN(VC vc, Type* args, Type typeRan, int numArgs);
+
+// User-defined types
+
+//! Create an uninterpreted named type
+Type vc_createType(VC vc, char* typeName);
+//! Lookup a user-defined (uninterpreted) type by name
+Type vc_lookupType(VC vc, char* typeName);
+
+/////////////////////////////////////////////////////////////////////////////
+// Expr manipulation methods                                               //
+/////////////////////////////////////////////////////////////////////////////
+
+//! Return the ExprManager
+ExprManager* vc_getEM(VC vc);
+
+//! Create a variable with a given name and type
+/*! The type cannot be a function type. */
+Expr vc_varExpr(VC vc, char* name, Type type);
+
+//! Create a variable with a given name, type, and value
+Expr vc_varExprDef(VC vc, char* name, Type type,
+                   Expr def);
+
+//! Get the expression and type associated with a name.
+/*!  If there is no such Expr, a NULL Expr is returned. */
+Expr vc_lookupVar(VC vc, char* name, Type* type);
+
+//! Get the type of the Expr.
+Type vc_getType(VC vc, Expr e);
+
+//! Get the largest supertype of the Expr.
+Type vc_getBaseType(VC vc, Expr e);
+
+//! Get the largest supertype of the Type.
+Type vc_getBaseTypeOfType(VC vc, Type t);
+
+//! Get the subtype predicate
+Expr vc_getTypePred(VC vc, Type t, Expr e);
+
+//! Create a string Expr
+Expr vc_stringExpr(VC vc, char* str);
+
+//! Create an ID Expr
+Expr vc_idExpr(VC vc, char* name);
+
+//! Create a list Expr
+/*! Intermediate representation for DP-specific expressions.
+ *  Normally, the first element of the list is a string Expr
+ *  representing an operator, and the rest of the list are the
+ *  arguments.  For example,
+ *
+ *  kids.push_back(vc->stringExpr("PLUS"));
+ *  kids.push_back(x); // x and y are previously created Exprs
+ *  kids.push_back(y);
+ *  Expr lst = vc->listExpr(kids);
+ *
+ * Or, alternatively (using its overloaded version):
+ *
+ * Expr lst = vc->listExpr("PLUS", x, y);
+ *
+ * or
+ *
+ * vector<Expr> summands;
+ * summands.push_back(x); summands.push_back(y); ...
+ * Expr lst = vc->listExpr("PLUS", summands);
+ */
+Expr vc_listExpr(VC vc, int numKids, Expr* kids);
+
+// Expr I/O
+//! Expr vc_parseExpr(VC vc, char* s);
+void vc_printExpr(VC vc, Expr e);
+//! Print e into a char*
+/*! Note that the ownership of the char* is given to the caller
+  which should free the memory when it is done with it.  This
+  can be done by calling vc_deleteString. */
+char* vc_printExprString(VC vc, Expr e);
+//! Delete char* returned by previous function
+void vc_deleteString(char* str);
+//! Print 'e' into an open file descriptor
+void vc_printExprFile(VC vc, Expr e, int fd);
+
+//! Import the Expr from another instance of VC
+/*! When expressions need to be passed among several instances of
+ *  VC, they need to be explicitly imported into the
+ *  corresponding instance using this method.  The return result is
+ *  an identical expression that belongs to the current instance of
+ *  VC, and can be safely used as part of more complex
+ *  expressions from the same instance.
+ \param vc is the instance to be imported into
+ \param e is the expression created using a different (not vc) instance
+ */
+Expr vc_importExpr(VC vc, Expr e);
+
+//! Import the Type from another instance of VC
+/*! \sa vc_importExpr() */
+Type vc_importType(Type t);
+
+//! Create an equality expression.  The two children must have the same type.
+Expr vc_eqExpr(VC vc, Expr child0, Expr child1);
+
+//! Create an all distinct expression. All children must ahve the same type.
+Expr vc_distinctExpr(VC vc, Expr* children, int numChildren);
+
+// Boolean expressions
+
+// The following functions create Boolean expressions.  The children provided
+// as arguments must be of type Boolean.
+Expr vc_trueExpr(VC vc);
+Expr vc_falseExpr(VC vc);
+Expr vc_notExpr(VC vc, Expr child);
+Expr vc_andExpr(VC vc, Expr left, Expr right);
+Expr vc_andExprN(VC vc, Expr* children, int numChildren);
+Expr vc_orExpr(VC vc, Expr left, Expr right);
+Expr vc_orExprN(VC vc, Expr* children, int numChildren);
+Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc);
+Expr vc_iffExpr(VC vc, Expr left, Expr right);
+Expr vc_iteExpr(VC vc, Expr ifpart, Expr thenpart, Expr elsepart);
+
+// Substitution
+
+// Substitutes oldTerms for newTerms in e.
+// This function doesn't actually exist in ValidityChecker interface,
+// but it does in Expr, and its functionality is needed in the C interface.
+// For consistency, it is represented here as if it were in ValidityChecker.
+Expr vc_substExpr(VC vc, Expr e,
+                  Expr* oldTerms, int numOldTerms,
+                  Expr* newTerms, int numNewTerms);
+
+// User-defined (uninterpreted) functions.
+
+//! Create an operator from a function with a given name and type.
+/*! Name is given as an ID Expr, and the type must be a function type. */
+Op vc_createOp(VC vc, char* name, Type type);
+
+//! Create a named user-defined function with a given type
+Op vc_createOpDef(VC vc, char* name, Type type, Expr def);
+
+//! Lookup an operator by name.
+/*! Returns the operator and the type if the operator exists.
+ * Returns NULL otherwise
+ */
+Op vc_lookupOp(VC vc, char* name, Type* type);
+
+//! Create expressions with a user-defined operator.
+/*!  op must have a function type. */
+Expr vc_funExpr1(VC vc, Op op, Expr child);
+Expr vc_funExpr2(VC vc, Op op, Expr left, Expr right);
+Expr vc_funExpr3(VC vc, Op op, Expr child0, Expr child1, Expr child2);
+Expr vc_funExprN(VC vc, Op op, Expr* children, int numChildren);
+
+// Arithmetic
+
+//! Create a rational number with numerator n and denominator d.
+/*! d cannot be 0. */
+Expr vc_ratExpr(VC vc, int n, int d);
+
+//! Create a rational number n/d; n and d are given as strings
+/*! n and d are converted to arbitrary-precision integers according to
+ *  the given base.  d cannot be 0.  */
+Expr vc_ratExprFromStr(VC vc, char* n, char* d, int base);
+
+//! Create a rational from a single string.
+/*!
+  \param n can be a string containing an integer, a pair of integers
+  "nnn/ddd", or a number in the fixed or floating point format.
+  \param base is the base in which to interpret the string.
+*/
+Expr vc_ratExprFromStr1(VC vc, char* n, int base);
+
+//! Unary minus.  Child must have a numeric type.
+Expr vc_uminusExpr(VC vc, Expr child);
+
+// plus, minus, mult.  Children must have numeric types.
+Expr vc_plusExpr(VC vc, Expr left, Expr right);
+Expr vc_plusExprN(VC vc, Expr* children, int numChildren);
+Expr vc_minusExpr(VC vc, Expr left, Expr right);
+Expr vc_multExpr(VC vc, Expr left, Expr right);
+Expr vc_powExpr(VC vc, Expr pow, Expr base);
+Expr vc_divideExpr(VC vc, Expr numerator, Expr denominator);
+
+// The following functions create less-than, less-than or equal,
+// greater-than, and greater-than or equal expressions of type Boolean.
+// Their arguments must be of numeric types.
+Expr vc_ltExpr(VC vc, Expr left, Expr right);
+Expr vc_leExpr(VC vc, Expr left, Expr right);
+Expr vc_gtExpr(VC vc, Expr left, Expr right);
+Expr vc_geExpr(VC vc, Expr left, Expr right);
+
+// Records
+
+// Create record literals;
+Expr vc_recordExpr1(VC vc, char* field, Expr expr);
+Expr vc_recordExpr2(VC vc, char* field0, Expr expr0,
+		                   char* field1, Expr expr1);
+Expr vc_recordExpr3(VC vc, char* field0, Expr expr0,
+                                   char* field1, Expr expr1,
+		                   char* field2, Expr expr2);
+Expr vc_recordExprN(VC vc, char** fields, Expr* exprs, int numFields);
+
+//! Create an expression representing the selection of a field from a record.
+Expr vc_recSelectExpr(VC vc, Expr record, char* field);
+
+//! Record update; equivalent to "record WITH .field := newValue"
+Expr vc_recUpdateExpr(VC vc, Expr record, char* field, Expr newValue);
+
+// Arrays
+
+//! Create an expression for the value of array at the given index
+Expr vc_readExpr(VC vc, Expr array, Expr index);
+
+//! Array update; equivalent to "array WITH [index] := newValue"
+Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue);
+
+// Bitvectors
+// Additional type constructor
+Type vc_bv32Type(VC vc);
+
+// Bitvector constants
+Expr vc_bvConstExprFromStr(VC vc, char* binary_repr);
+Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value);
+Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value);
+Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long value);
+
+// Concat and extract
+Expr vc_bvConcatExpr(VC vc, Expr left, Expr right);
+Expr vc_bvConcatExprN(VC vc, Expr* children, int numChildren);
+Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, int low_bit_no);
+Expr vc_bvBoolExtract(VC vc, Expr child, int bit_no);
+
+// Bitwise Boolean operators: Negation, And, Or, Xor
+Expr vc_bvNotExpr(VC vc, Expr child);
+Expr vc_bvAndExpr(VC vc, Expr left, Expr right);
+Expr vc_bvOrExpr(VC vc, Expr left, Expr right);
+Expr vc_bvXorExpr(VC vc, Expr left, Expr right);
+
+// Unsigned bitvector inequalities
+Expr vc_bvLtExpr(VC vc, Expr left, Expr right);
+Expr vc_bvLeExpr(VC vc, Expr left, Expr right);
+Expr vc_bvGtExpr(VC vc, Expr left, Expr right);
+Expr vc_bvGeExpr(VC vc, Expr left, Expr right);
+
+// Signed bitvector inequalities
+Expr vc_bvSLtExpr(VC vc, Expr left, Expr right);
+Expr vc_bvSLeExpr(VC vc, Expr left, Expr right);
+Expr vc_bvSGtExpr(VC vc, Expr left, Expr right);
+Expr vc_bvSGeExpr(VC vc, Expr left, Expr right);
+
+// Sign-extend child to a total of nbits bits
+Expr vc_bvSignExtend(VC vc, Expr child, int nbits);
+
+// Bitvector arithmetic: unary minus, plus, subtract, multiply
+Expr vc_bvUMinusExpr(VC vc, Expr child);
+Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right);
+Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right);
+Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right);
+Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right);
+Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right);
+Expr vc_bv32MultExpr(VC vc, Expr left, Expr right);
+Expr vc_bvUDivExpr(VC vc, Expr left, Expr right);
+Expr vc_bvURemExpr(VC vc, Expr left, Expr right);
+Expr vc_bvSDivExpr(VC vc, Expr left, Expr right);
+Expr vc_bvSRemExpr(VC vc, Expr left, Expr right);
+Expr vc_bvSModExpr(VC vc, Expr left, Expr right);
+
+// Shift operators
+Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child);
+Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child);
+Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child);
+Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child);
+Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child);
+Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child);
+Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs);
+
+/*C pointer support:  C interface to support C memory arrays in CVC3 */
+Expr vc_bvCreateMemoryArray(VC vc, char * arrayName);
+Expr vc_bvReadMemoryArray(VC vc,
+			  Expr array, Expr byteIndex, int numOfBytes);
+Expr vc_bvWriteToMemoryArray(VC vc,
+			     Expr array, Expr  byteIndex,
+			     Expr element, int numOfBytes);
+
+// Tuples
+
+//! Create a tuple expression
+/*! 'children' is an array of elements of length numChildren */
+Expr vc_tupleExprN(VC vc, Expr* children, int numChildren);
+
+//! Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5)
+Expr vc_tupleSelectExpr(VC vc, Expr tuple, int index);
+
+//! Tuple update; equivalent to "tuple WITH index := newValue"
+Expr vc_tupleUpdateExpr(VC vc, Expr tuple, int index, Expr newValue);
+
+// Datatypes
+
+//! Datatype constructor expression
+Expr vc_datatypeConsExpr(VC vc, char* constructor, int numArgs, Expr* args);
+
+//! Datatype selector expression
+Expr vc_datatypeSelExpr(VC vc, char* selector, Expr arg);
+
+//! Datatype tester expression
+Expr vc_datatypeTestExpr(VC vc, char* constructor, Expr arg);
+
+// Quantifiers
+
+//! Create a bound variable.
+/*! \param name
+ * \param uid is a fresh unique string to distinguish this variable
+ * from other bound variables with the same name
+ * \param type
+ */
+Expr vc_boundVarExpr(VC vc, char* name, char *uid, Type type);
+
+//! Create a FORALL quantifier.
+/*! Bvars is an array of bound variables of length numBvars. */
+Type vc_forallExpr(VC vc, Expr* Bvars, int numBvars, Expr f);
+
+//! Set triggers for a forallExpr
+void vc_setTriggers(VC vc, Expr e, int numTrigs, Expr* triggers);
+
+//! Create an EXISTS quantifier.
+/*! Bvars is an array of bound variables of length numBvars. */
+Expr vc_existsExpr(VC vc, Expr* Bvars, int numBvars, Expr f);
+
+//! Lambda-expression
+Op vc_lambdaExpr(VC vc, int numVars, Expr* vars, Expr body);
+
+/////////////////////////////////////////////////////////////////////////////
+// Context-related methods                                                 //
+/////////////////////////////////////////////////////////////////////////////
+
+//! Set the resource limit (0==unlimited, 1==exhausted).
+/*! Currently, the limit is the total number of processed facts. */
+void vc_setResourceLimit(VC vc, unsigned limit);
+
+//! Assert a new formula in the current context.
+/*! The formula must have Boolean type. */
+void vc_assertFormula(VC vc, Expr e);
+
+//! Register an atomic formula of interest.
+/*! Registered atoms are tracked by the decision procedures.  If one of them
+    is deduced to be true or false, it is added to a list of implied literals.
+    Implied literals can be retrieved with the getImpliedLiteral function */
+void vc_registerAtom(VC vc, Expr e);
+
+//! Return next literal implied by last assertion.  Null if none.
+/*! Returned literals are either registered atomic formulas or their negation
+ */
+Expr vc_getImpliedLiteral(VC vc);
+
+//! Simplify e with respect to the current context
+Expr vc_simplify(VC vc, Expr e);
+
+//! Check validity of e in the current context.
+/*! Possible results are: 0 = invalid, 1 = valid, 2 = abort, 3 = unknown,
+ * -100 = exception (type error, internal error, etc).
+ * If the result is 1, then the resulting context is the same as
+ * the starting context.  If the result is 0 or 3, then the resulting
+ * context is a context in which e is false (though the context may be
+ * inconsistent in the case of an unknown result).  e must have Boolean
+ * type.  In the case of a result of -100, refer to vc_get_error_string()
+ * to see what went wrong. */
+int vc_query(VC vc, Expr e);
+
+//! Get the next model
+/*! This method should only be called after a query which returns
+  0.  Its return values are as for vc_query(). */
+int vc_checkContinue(VC vc);
+
+//! Restart the most recent query with e as an additional assertion.
+/*! This method should only be called after a query which returns
+  0.  Its return values are as for vc_query(). */
+int vc_restart(VC vc, Expr e);
+
+//! Returns to context immediately before last invalid query.
+/*! This method should only be called after a query which returns 0.
+ */
+void vc_returnFromCheck(VC vc);
+
+//! Get assumptions made by the user in this and all previous contexts.
+/*! User assumptions are created either by calls to assertFormula or by a
+ * call to query.  In the latter case, the negated query is added as an
+ * assumption.  The caller is responsible for freeing the array when
+ * finished with it.
+ */
+Expr* vc_getUserAssumptions(VC vc, int* size);
+
+//! Get assumptions made internally in this and all previous contexts.
+/*! Internal assumptions are literals assumed by the sat solver.
+ * The caller is responsible for freeing the array when finished with it by
+ * calling vc_deleteVector.
+ */
+Expr* vc_getInternalAssumptions(VC vc, int* size);
+
+//! Get all assumptions made in this and all previous contexts.
+/*!
+ * The caller is responsible for freeing the array when finished with it by
+ * calling vc_deleteVector.
+ */
+Expr* vc_getAssumptions(VC vc, int* size);
+
+//yeting, for proof translation, get the assumptions used.
+//the assumptions used are different from the user assumptions.
+//the assumptions used are preprocessed if 'preprocess' is ena
+Expr vc_getProofAssumptions(VC vc);
+
+//yeting, for proof translation,
+Expr vc_getProofQuery(VC vc);
+
+//! Returns the set of assumptions used in the proof of queried formula.
+/*! It returns a subset of getAssumptions().  If the last query was false
+ *  or there has not yet been a query, it does nothing.
+ * The caller is responsible for freeing the array when finished with it by
+ * calling vc_deleteVector.
+ */
+Expr* vc_getAssumptionsUsed(VC vc, int* size);
+
+//! Return the counterexample after a failed query.
+/*! This method should only be called after a query which returns
+ * false.  It will try to return the simplest possible set of
+ * assertions which are sufficient to make the queried expression
+ * false.  The caller is responsible for freeing the array when finished with
+ * it by calling vc_deleteVector.
+ */
+Expr* vc_getCounterExample(VC vc, int* size);
+
+//! Will assign concrete values to all user created variables
+/*! This function should only be called after a query which return false.
+ * Returns an array of Exprs with size *size.
+ * The caller is responsible for freeing the array when finished with it by
+ * calling vc_deleteVector.
+ */
+Expr* vc_getConcreteModel(VC vc, int* size);
+
+// Returns true if the current context is inconsistent.
+/*! Also returns a minimal set of assertions used to determine the
+ * inconsistency. The caller is responsible for freeing the array when finished
+ * with it by calling vc_deleteVector.
+ */
+int vc_inconsistent(VC vc, Expr** assumptions, int* size);
+
+//! Returns non-NULL if the invalid result from last query() is imprecise
+/*!
+ * The return value is filled with the reasons for incompleteness (it
+ * is intended to be shown to the end user).  The caller is responsible for
+ * freeing the string returned by calling vc_deleteString.
+ */
+char* vc_incomplete(VC vc);
+
+//! Returns the proof for the last proven query
+Expr vc_getProof(VC vc);
+
+//! Returns the proof of a .cvc file, if it is valid.
+Expr vc_getProofOfFile(VC vc, char * filename);
+
+//! Returns the TCC of the last assumption or query
+/*! Returns Null Expr if no assumptions or queries were performed. */
+Expr vc_getTCC(VC vc);
+
+//! Return the set of assumptions used in the proof of the last TCC
+/*! The caller is responsible for freeing the array when finished with it by
+ * calling vc_deleteVector.
+ */
+Expr* vc_getAssumptionsTCC(VC vc, int* size);
+
+//! Returns the proof of TCC of the last assumption or query
+/*! Returns Null Expr if no assumptions or queries were performed. */
+Expr vc_getProofTCC(VC vc);
+
+//! After successful query, return its closure |- Gamma => phi
+/*! Turn a valid query Gamma |- phi into an implication
+ * |- Gamma => phi.
+ *
+ * Returns Null Expr if last query was invalid.
+ */
+Expr vc_getClosure(VC vc);
+
+//! Construct a proof of the query closure |- Gamma => phi
+/*! Returns Null if last query was Invalid. */
+Expr vc_getProofClosure(VC vc);
+
+//! Returns the current stack level.  Initial level is 0.
+int vc_stackLevel(VC vc);
+
+//! Checkpoint the current context and increase the scope level
+void vc_push(VC vc);
+
+//! Restore the current context to its state at the last checkpoint
+void vc_pop(VC vc);
+
+//! Restore the current context to the given stackLevel.
+/*! stackLevel must be less than or equal to the current stack level.
+ */
+void vc_popto(VC vc, int stackLevel);
+
+//! Get the current context
+Context* vc_getCurrentContext(VC vc);
+
+/* ---------------------------------------------------------------------- */
+/*  Util                                                                  */
+/* ---------------------------------------------------------------------- */
+
+// Order
+
+//! Compares two expressions
+/*! If e1 < e2, e1==e2, and e1 > e2, it returns -1, 0, 1
+ * respectively.  A return value of -100 signals an error (refer to
+ * vc_get_error_string() for details).
+ *
+ * Can't be 'compare' because already defined in ocaml */
+int vc_compare_exprs(Expr e1,Expr e2);
+
+// Printing
+
+//! Convert Expr to string
+char* vc_exprString(Expr e);
+//! Convert Type to string
+char* vc_typeString(Type t);
+
+// What kind of Expr?
+int vc_isClosure(Expr e);
+int vc_isQuantifier(Expr e);
+int vc_isLambda(Expr e);
+Expr vc_isVar(Expr e);
+
+int vc_arity(Expr e);
+int vc_getKind(Expr e);
+Expr vc_getChild(Expr e, int i);
+int vc_getNumVars(Expr e);
+Expr vc_getVar(Expr e, int i);
+Expr vc_getBody(Expr e);
+Expr vc_getExistential(Expr e);
+Expr vc_getFun(VC vc, Expr e);
+Expr vc_toExpr(Type t);
+
+//! Translate a kind int to a string
+const char* vc_getKindString(VC vc,int kind);
+
+//! Translate a kind string to an int
+int vc_getKindInt(VC vc,char* kind_name);
+
+//! Return an int from a rational expression
+int vc_getInt(Expr e);
+
+//! Return an int from a constant bitvector expression
+int vc_getBVInt(VC vc, Expr e);
+//! Return an unsigned int from a constant bitvector expression
+unsigned int vc_getBVUnsigned(VC vc, Expr e);
+
+// Debug
+int vc_get_error_status();
+void vc_reset_error_status();
+char* vc_get_error_string();
+
+//! Print statistics
+void vc_print_statistics(VC vc);
+
+#endif
+
+
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
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ * 
+ * <hr>
+ * 
+ */
+/*****************************************************************************/
+
+#ifndef _cvc3__include__c_interface_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<bool>();
+  return getKind() == CVC4::kind::CONST_BOOLEAN && getConst<bool>() == false;
 }
 
 bool Expr::isTrue() const {
-  return getKind() == CVC4::kind::CONST_BOOLEAN && getConst<bool>();
+  return getKind() == CVC4::kind::CONST_BOOLEAN && getConst<bool>() == 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> > Expr::getTriggers() const {
   return vector< vector<Expr> >();
 }
@@ -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<Expr> > 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<T>::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_ */