diff options
Diffstat (limited to 'src/expr/expr_builder.cpp')
-rw-r--r-- | src/expr/expr_builder.cpp | 77 |
1 files changed, 67 insertions, 10 deletions
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp index 6491b7d44..2f7114a9b 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/expr_builder.cpp @@ -9,9 +9,10 @@ ** **/ -#include "core/expr_builder.h" -#include "core/expr_manager.h" -#include "core/expr_value.h" +#include "expr_builder.h" +#include "expr_manager.h" +#include "expr_value.h" +#include "util/assert.h" using namespace std; @@ -26,6 +27,16 @@ ExprBuilder::ExprBuilder(const Expr& e) : d_em(ExprManager::currentEM()), d_kind d_children.u_arr[0] = v; } +ExprBuilder& ExprBuilder::reset(const ExprValue* ev) { + this->~ExprBuilder(); + d_kind = Kind(ev->d_kind); + d_used = false; + d_nchildren = ev->d_nchildren; + for(Expr::const_iterator i = ev->begin(); i != ev->end(); ++i) + addChild(i->d_ev); + return *this; +} + 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) { cvc4assert(!d_used); @@ -34,9 +45,9 @@ ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kin d_children.u_vec->reserve(d_nchildren + 5); copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), back_inserter(*d_children.u_vec)); } else { - iterator j = d_children.u_arr; - for(iterator i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j) - *j = i->inc(); + ev_iterator j = d_children.u_arr; + for(ExprValue* const* i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j) + *j = (*i)->inc(); } } @@ -46,7 +57,7 @@ ExprBuilder::ExprBuilder(ExprManager* em) : d_em(em), d_kind(UNDEFINED_KIND), d_ ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) { } -ExprBuilder::ExprBuilder(ExprManager* em, const Expr&) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { +ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { ExprValue *v = e->inc(); d_children.u_arr[0] = v; } @@ -55,8 +66,8 @@ ExprBuilder::~ExprBuilder() { if(d_nchildren > nchild_thresh) { delete d_children.u_vec; } else { - for(iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) { - *i + for(ev_iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) { + (*i)->dec(); } } } @@ -70,10 +81,20 @@ ExprBuilder& ExprBuilder::eqExpr(const Expr& right) { } ExprBuilder& ExprBuilder::notExpr() { + if(d_kind != UNDEFINED_KIND) + collapse(); + d_kind = NOT; + return *this; } // avoid double-negatives ExprBuilder& ExprBuilder::negate() { + if(d_kind == NOT) + return reset(d_children.u_arr[0]); + if(d_kind != UNDEFINED_KIND) + collapse(); + d_kind = NOT; + return *this; } ExprBuilder& ExprBuilder::andExpr(const Expr& right) { @@ -116,7 +137,43 @@ void ExprBuilder::addChild(const Expr& e) { if(d_nchildren == nchild_thresh) { vector<Expr>* v = new vector<Expr>(); v->reserve(nchild_thresh + 5); - + for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) { + v->push_back(Expr(*i)); + i->dec(); + } + v.push_back(e); + d_children.u_vec = v; + ++d_nchildren; + } else if(d_nchildren > nchild_thresh) { + d_children.u_vec.push_back(e); + ++d_nchildren; + } else { + ExprValue *ev = e->d_ev; + d_children.u_arr[d_nchildren] = ev; + ev->inc(); + ++d_nchildren; + } + return *this; +} + +void ExprBuilder::addChild(const ExprValue* ev) { + if(d_nchildren == nchild_thresh) { + vector<Expr>* v = new vector<Expr>(); + v->reserve(nchild_thresh + 5); + for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) { + v->push_back(Expr(*i)); + i->dec(); + } + v.push_back(Expr(ev)); + d_children.u_vec = v; + ++d_nchildren; + } else if(d_nchildren > nchild_thresh) { + d_children.u_vec.push_back(Expr(ev)); + ++d_nchildren; + } else { + d_children.u_arr[d_nchildren] = ev; + ev->inc(); + ++d_nchildren; } return *this; } |