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.cpp | |
parent | 964b40905c6daed1ac4612fde034264222f6bb67 (diff) |
more interface work; adding legacy C interface
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 64 |
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 */ |