diff options
Diffstat (limited to 'src/expr/expr.cpp')
-rw-r--r-- | src/expr/expr.cpp | 47 |
1 files changed, 30 insertions, 17 deletions
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index e88189bcc..fa273dfa5 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -13,6 +13,7 @@ #include "expr/expr.h" #include "expr_value.h" #include "expr_builder.h" +#include "util/Assert.h" using namespace CVC4::expr; @@ -33,70 +34,82 @@ Expr::Expr() : Expr::Expr(ExprValue* ev) : d_ev(ev) { - if(d_ev != 0) - d_ev->inc(); + Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); + d_ev->inc(); } Expr::Expr(const Expr& e) { - if((d_ev = e.d_ev) && d_ev != 0) - d_ev->inc(); + Assert(e.d_ev != NULL, "Expecting a non-NULL evpression value!"); + d_ev = e.d_ev; + d_ev->inc(); } Expr::~Expr() { - if(d_ev) - d_ev->dec(); + Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); + d_ev->dec(); +} + +void Expr::assignExprValue(ExprValue* ev) { + d_ev = ev; + d_ev->inc(); } Expr& Expr::operator=(const Expr& e) { - if(d_ev) + Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); + if(this != &e && d_ev != e.d_ev) { d_ev->dec(); - if((d_ev = e.d_ev)) + d_ev = e.d_ev; d_ev->inc(); + } return *this; } -ExprValue* Expr::operator->() const { +ExprValue const* Expr::operator->() const { + Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); return d_ev; } uint64_t Expr::hash() const { + Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); return d_ev->hash(); } Expr Expr::eqExpr(const Expr& right) const { - return ExprBuilder(*this).eqExpr(right); + return ExprManager::currentEM()->mkExpr(EQUAL, *this, right); } Expr Expr::notExpr() const { - return ExprBuilder(*this).notExpr(); + return ExprManager::currentEM()->mkExpr(NOT, *this); } +// FIXME: What does this do and why? Expr Expr::negate() const { // avoid double-negatives return ExprBuilder(*this).negate(); } + Expr Expr::andExpr(const Expr& right) const { - return ExprBuilder(*this).andExpr(right); + return ExprManager::currentEM()->mkExpr(AND, *this, right); } Expr Expr::orExpr(const Expr& right) const { - return ExprBuilder(*this).orExpr(right); + return ExprManager::currentEM()->mkExpr(OR, *this, right); } Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const { - return ExprBuilder(*this).iteExpr(thenpart, elsepart); + return ExprManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart); } Expr Expr::iffExpr(const Expr& right) const { - return ExprBuilder(*this).iffExpr(right); + return ExprManager::currentEM()->mkExpr(IFF, *this, right); } Expr Expr::impExpr(const Expr& right) const { - return ExprBuilder(*this).impExpr(right); + return ExprManager::currentEM()->mkExpr(IMPLIES, *this, right); } Expr Expr::xorExpr(const Expr& right) const { - return ExprBuilder(*this).xorExpr(right); + return ExprManager::currentEM()->mkExpr(XOR, *this, right); } }/* CVC4 namespace */ |