src/core/expr_builder.cpp

   1 /*********************                                           -*- C++ -*-  */
   2 /** expr_builder.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  **/
  11
  12 #include "core/expr_builder.h"
  13 #include "core/expr_manager.h"
  14 #include "core/expr_value.h"
  15
  16 using namespace std;
  17
  18 namespace CVC4 {
  19
  20 ExprBuilder::ExprBuilder() : d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {}
  21
  22 ExprBuilder::ExprBuilder(Kind k) : d_em(ExprManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) {}
  23
  24 ExprBuilder::ExprBuilder(const Expr& e) : d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
  25   ExprValue *v = e->inc();
  26   d_children.u_arr[0] = v;
  27 }
  28
  29 ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), d_nchildren(eb.d_nchildren) {
  30   cvc4assert(!d_used);
  31
  32   if(d_nchildren > nchild_thresh) {
  33     d_children.u_vec = new vector<Expr>();
  34     d_children.u_vec->reserve(d_nchildren + 5);
  35     copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), back_inserter(*d_children.u_vec));
  36   } else {
  37     iterator j = d_children.u_arr;
  38     for(iterator i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j)
  39       *j = i->inc();
  40   }
  41 }
  42
  43 ExprBuilder::ExprBuilder(ExprManager* em) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {
  44 }
  45
  46 ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) {
  47 }
  48
  49 ExprBuilder::ExprBuilder(ExprManager* em, const Expr&) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
  50   ExprValue *v = e->inc();
  51   d_children.u_arr[0] = v;
  52 }
  53
  54 ExprBuilder::~ExprBuilder() {
  55   if(d_nchildren > nchild_thresh) {
  56     delete d_children.u_vec;
  57   } else {
  58     for(iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) {
  59       *i
  60     }
  61   }
  62 }
  63
  64 // Compound expression constructors
  65 ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
  66   if(d_kind != UNDEFINED_KIND && d_kind != EQUAL)
  67     collapse();
  68   d_kind = EQUAL;
  69   return *this;
  70 }
  71
  72 ExprBuilder& ExprBuilder::notExpr() {
  73 }
  74
  75 // avoid double-negatives
  76 ExprBuilder& ExprBuilder::negate() {
  77 }
  78
  79 ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
  80 }
  81
  82 ExprBuilder& ExprBuilder::orExpr(const Expr& right) {
  83 }
  84
  85 ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) {
  86 }
  87
  88 ExprBuilder& ExprBuilder::iffExpr(const Expr& right) {
  89 }
  90
  91 ExprBuilder& ExprBuilder::impExpr(const Expr& right) {
  92 }
  93
  94 ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
  95 }
  96
  97 ExprBuilder& ExprBuilder::skolemExpr(int i) {
  98 }
  99
 100 ExprBuilder& ExprBuilder::substExpr(const std::vector<Expr>& oldTerms,
 101                                     const std::vector<Expr>& newTerms) {
 102 }
 103
 104 // "Stream" expression constructor syntax
 105 ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
 106 }
 107
 108 ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
 109 }
 110
 111 template <class Iterator>
 112 ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
 113 }
 114
 115 void ExprBuilder::addChild(const Expr& e) {
 116   if(d_nchildren == nchild_thresh) {
 117     vector<Expr>* v = new vector<Expr>();
 118     v->reserve(nchild_thresh + 5);
 119
 120   }
 121   return *this;
 122 }
 123
 124 void ExprBuilder::collapse() {
 125   if(d_nchildren == nchild_thresh) {
 126     vector<Expr>* v = new vector<Expr>();
 127     v->reserve(nchild_thresh + 5);
 128
 129   }
 130   return *this;
 131 }
 132
 133 // not const
 134 ExprBuilder::operator Expr() {
 135 }
 136
 137 AndExprBuilder   ExprBuilder::operator&&(Expr) {
 138 }
 139
 140 OrExprBuilder    ExprBuilder::operator||(Expr) {
 141 }
 142
 143 PlusExprBuilder  ExprBuilder::operator+ (Expr) {
 144 }
 145
 146 PlusExprBuilder  ExprBuilder::operator- (Expr) {
 147 }
 148
 149 MultExprBuilder  ExprBuilder::operator* (Expr) {
 150 }
 151
 152 } /* CVC4 namespace */