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/cvc3_compat.h | |
parent | 964b40905c6daed1ac4612fde034264222f6bb67 (diff) |
more interface work; adding legacy C interface
Diffstat (limited to 'src/compat/cvc3_compat.h')
-rw-r--r-- | src/compat/cvc3_compat.h | 22 |
1 files changed, 20 insertions, 2 deletions
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_ */ |