diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-27 00:34:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-27 00:34:30 +0000 |
commit | d529e4c065d880f5fdf6e10cb0996a45e739bb51 (patch) | |
tree | 52aa084b73cb46870a8a544eeca36c0266948d9b /src/compat | |
parent | 964b40905c6daed1ac4612fde034264222f6bb67 (diff) |
more interface work; adding legacy C interface
Diffstat (limited to 'src/compat')
-rw-r--r-- | src/compat/Makefile.am | 3 | ||||
-rw-r--r-- | src/compat/cvc3_compat.cpp | 64 | ||||
-rw-r--r-- | src/compat/cvc3_compat.h | 22 |
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_ */ |