1 files changed, 62 insertions, 2 deletions
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 */