diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-18 22:02:11 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-18 22:02:11 +0000 |
commit | 394791604a62e19763a8a45328bc5177d91fabf9 (patch) | |
tree | 29027c84c0285da33bac6c5d1366635b9e4db1bc /src/expr | |
parent | 477e97cd81afe4b86eea47e9abe6311fc22299fc (diff) |
work on exprs, driver, util
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/attr_type.h | 2 | ||||
-rw-r--r-- | src/expr/expr.cpp | 10 | ||||
-rw-r--r-- | src/expr/expr_attribute.h | 6 | ||||
-rw-r--r-- | src/expr/expr_builder.cpp | 77 | ||||
-rw-r--r-- | src/expr/expr_builder.h | 12 | ||||
-rw-r--r-- | src/expr/expr_manager.cpp | 6 | ||||
-rw-r--r-- | src/expr/expr_manager.h | 2 | ||||
-rw-r--r-- | src/expr/expr_value.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr_value.h | 4 |
9 files changed, 92 insertions, 29 deletions
diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h index d76bd742d..d24385f8e 100644 --- a/src/expr/attr_type.h +++ b/src/expr/attr_type.h @@ -12,7 +12,7 @@ #ifndef __CVC4_ATTR_TYPE_H #define __CVC4_ATTR_TYPE_H -#include "core/expr_attribute.h" +#include "expr_attribute.h" namespace CVC4 { diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 5e422f349..b6484ef25 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -11,8 +11,8 @@ **/ #include "cvc4_expr.h" -#include "core/expr_value.h" -#include "core/expr_builder.h" +#include "expr_value.h" +#include "expr_builder.h" namespace CVC4 { @@ -44,11 +44,7 @@ Expr& Expr::operator=(const Expr& e) { return *this; } -ExprValue* Expr::operator->() { - return d_ev; -} - -const ExprValue* Expr::operator->() const { +ExprValue* Expr::operator->() const { return d_ev; } diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h index b00882478..3525a8370 100644 --- a/src/expr/expr_attribute.h +++ b/src/expr/expr_attribute.h @@ -15,9 +15,9 @@ // TODO WARNING this file needs work ! #include <stdint.h> -#include "core/config.h" -#include "core/context.h" -#include "core/cvc4_expr.h" +#include "config.h" +#include "context/context.h" +#include "cvc4_expr.h" namespace CVC4 { 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; } diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index fa08a3149..1104c17f5 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -13,8 +13,8 @@ #define __CVC4_EXPR_BUILDER_H #include <vector> -#include "core/expr_manager.h" -#include "core/kind.h" +#include "expr_manager.h" +#include "kind.h" namespace CVC4 { @@ -41,9 +41,15 @@ class ExprBuilder { std::vector<Expr>* u_vec; } d_children; - void addChild(); + void addChild(const Expr&); + void addChild(const ExprValue*); void collapse(); + typedef ExprValue** ev_iterator; + typedef ExprValue const** const_ev_iterator; + + void reset(const ExprValue*); + public: ExprBuilder(); diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 90f10d8f7..80091bef6 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -10,9 +10,9 @@ ** Expression manager implementation. **/ -#include "core/expr_builder.h" -#include "core/expr_manager.h" -#include "core/cvc4_expr.h" +#include "expr_builder.h" +#include "expr_manager.h" +#include "cvc4_expr.h" namespace CVC4 { diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 048250485..7e0da01c6 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -14,7 +14,7 @@ #include <vector> #include "cvc4_expr.h" -#include "core/kind.h" +#include "kind.h" namespace CVC4 { diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index ce4177a09..451538f3f 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -14,7 +14,7 @@ ** reference count on ExprValue instances and **/ -#include "core/expr_value.h" +#include "expr_value.h" namespace CVC4 { diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index 5f90533ed..4b4b4f612 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -48,6 +48,10 @@ class ExprValue { Expr d_children[0]; friend class Expr; + friend class ExprBuilder; + + ExprValue* inc() { /* FIXME thread safety */ ++d_rc; return this; } + ExprValue* dec() { /* FIXME thread safety */ --d_rc; return this; } public: /** Hash this expression. |