more interface work; adding legacy C interface

3 files changed, 84 insertions, 5 deletions

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_ */