src/core/expr.cpp

   1 /*********************                                           -*- C++ -*-  */
   2 /** expr.cpp
   3  ** This file is part of the CVC4 prototype.
   4  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
   5  ** Courant Institute of Mathematical Sciences
   6  ** New York University
   7  ** See the file COPYING in the top-level source directory for licensing
   8  ** information.
   9  **
  10  ** Reference-counted encapsulation of a pointer to an expression.
  11  **/
  12
  13 #include "cvc4_expr.h"
  14 #include "core/expr_value.h"
  15 #include "core/expr_builder.h"
  16
  17 namespace CVC4 {
  18
  19 Expr Expr::s_null(0);
  20
  21 Expr::Expr(ExprValue* ev)
  22   : d_ev(ev) {
  23   // FIXME: thread-safety
  24   ++d_ev->d_rc;
  25 }
  26
  27 Expr::Expr(const Expr& e) {
  28   // FIXME: thread-safety
  29   if((d_ev = e.d_ev))
  30     ++d_ev->d_rc;
  31 }
  32
  33 Expr::~Expr() {
  34   // FIXME: thread-safety
  35   --d_ev->d_rc;
  36 }
  37
  38 Expr& Expr::operator=(const Expr& e) {
  39   // FIXME: thread-safety
  40   if(d_ev)
  41     --d_ev->d_rc;
  42   if((d_ev = e.d_ev))
  43     ++d_ev->d_rc;
  44   return *this;
  45 }
  46
  47 ExprValue* Expr::operator->() {
  48   return d_ev;
  49 }
  50
  51 const ExprValue* Expr::operator->() const {
  52   return d_ev;
  53 }
  54
  55 uint64_t Expr::hash() const {
  56   return d_ev->hash();
  57 }
  58
  59 Expr Expr::eqExpr(const Expr& right) const {
  60   return ExprBuilder(*this).eqExpr(right);
  61 }
  62
  63 Expr Expr::notExpr() const {
  64   return ExprBuilder(*this).notExpr();
  65 }
  66
  67 Expr Expr::negate() const { // avoid double-negatives
  68   return ExprBuilder(*this).negate();
  69 }
  70
  71 Expr Expr::andExpr(const Expr& right) const {
  72   return ExprBuilder(*this).andExpr(right);
  73 }
  74
  75 Expr Expr::orExpr(const Expr& right) const {
  76   return ExprBuilder(*this).orExpr(right);
  77 }
  78
  79 Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
  80   return ExprBuilder(*this).iteExpr(thenpart, elsepart);
  81 }
  82
  83 Expr Expr::iffExpr(const Expr& right) const {
  84   return ExprBuilder(*this).iffExpr(right);
  85 }
  86
  87 Expr Expr::impExpr(const Expr& right) const {
  88   return ExprBuilder(*this).impExpr(right);
  89 }
  90
  91 Expr Expr::xorExpr(const Expr& right) const {
  92   return ExprBuilder(*this).xorExpr(right);
  93 }
  94
  95 Expr Expr::skolemExpr(int i) const {
  96   return ExprBuilder(*this).skolemExpr(i);
  97 }
  98
  99 Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
 100                      const std::vector<Expr>& newTerms) const {
 101   return ExprBuilder(*this).substExpr(oldTerms, newTerms);
 102 }
 103
 104 } /* CVC4 namespace */