diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
commit | 2163539a8b839acf98bda0e1a65f1fcca5232fb2 (patch) | |
tree | 207a09896626f678172ec774459defa6690b0200 /src/expr/expr_builder.cpp | |
parent | abe5fb451ae66a4bedc88d870e99f76de4eb323c (diff) |
work on propositional layer, expression builder support for large expressions, output classes, and minisat
Diffstat (limited to 'src/expr/expr_builder.cpp')
-rw-r--r-- | src/expr/expr_builder.cpp | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp index be9c60199..4de22f987 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/expr_builder.cpp @@ -12,7 +12,8 @@ #include "expr_builder.h" #include "expr_manager.h" #include "expr_value.h" -#include "util/assert.h" +#include "util/Assert.h" +#include "util/output.h" using namespace std; @@ -159,15 +160,19 @@ ExprBuilder& ExprBuilder::xorExpr(const Expr& right) { // "Stream" expression constructor syntax ExprBuilder& ExprBuilder::operator<<(const Kind& op) { + d_kind = op; return *this; } ExprBuilder& ExprBuilder::operator<<(const Expr& child) { + addChild(child); return *this; } void ExprBuilder::addChild(const Expr& e) { + Debug("expr") << "adding child E " << e << endl; if(d_nchildren == nchild_thresh) { + Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl; 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) { @@ -178,9 +183,11 @@ void ExprBuilder::addChild(const Expr& e) { d_children.u_vec = v; ++d_nchildren; } else if(d_nchildren > nchild_thresh) { + Debug("expr") << "over thresh " << d_nchildren << " > " << nchild_thresh << endl; d_children.u_vec->push_back(e); ++d_nchildren; } else { + Debug("expr") << "under thresh " << d_nchildren << " < " << nchild_thresh << endl; ExprValue *ev = e.d_ev; d_children.u_arr[d_nchildren] = ev; ev->inc(); @@ -189,7 +196,9 @@ void ExprBuilder::addChild(const Expr& e) { } void ExprBuilder::addChild(ExprValue* ev) { + Debug("expr") << "adding child ev " << ev << endl; if(d_nchildren == nchild_thresh) { + Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl; 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) { @@ -200,9 +209,11 @@ void ExprBuilder::addChild(ExprValue* ev) { d_children.u_vec = v; ++d_nchildren; } else if(d_nchildren > nchild_thresh) { + Debug("expr") << "over thresh " << d_nchildren << " > " << nchild_thresh << endl; d_children.u_vec->push_back(Expr(ev)); ++d_nchildren; } else { + Debug("expr") << "under thresh " << d_nchildren << " < " << nchild_thresh << endl; d_children.u_arr[d_nchildren] = ev; ev->inc(); ++d_nchildren; @@ -214,6 +225,7 @@ ExprBuilder& ExprBuilder::collapse() { vector<Expr>* v = new vector<Expr>(); v->reserve(nchild_thresh + 5); // + Unreachable();// unimplemented } return *this; } |