diff options
Diffstat (limited to 'src/expr/node_builder.h')
-rw-r--r-- | src/expr/node_builder.h | 313 |
1 files changed, 313 insertions, 0 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h new file mode 100644 index 000000000..be96c2e77 --- /dev/null +++ b/src/expr/node_builder.h @@ -0,0 +1,313 @@ +/********************* -*- C++ -*- */ +/** expr_builder.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + **/ + +#ifndef __CVC4__EXPR_BUILDER_H +#define __CVC4__EXPR_BUILDER_H + +#include <vector> +#include <cstdlib> + +#include "expr/node_manager.h" +#include "expr/kind.h" +#include "util/Assert.h" + +namespace CVC4 { + +class AndExprBuilder; +class OrExprBuilder; +class PlusExprBuilder; +class MinusExprBuilder; +class MultExprBuilder; + +class NodeBuilder { + NodeManager* d_em; + + Kind d_kind; + + // initially false, when you extract the Node this is set and you can't + // extract another + bool d_used; + + static const unsigned nchild_thresh = 10; + + unsigned d_nchildren; + union { + ExprValue* u_arr[nchild_thresh]; + std::vector<Node>* u_vec; + } d_children; + + void addChild(const Node& e) { addChild(e.d_ev); } + void addChild(ExprValue*); + NodeBuilder& collapse(); + + typedef ExprValue** ev_iterator; + typedef ExprValue const** const_ev_iterator; + + ev_iterator ev_begin() { + return d_children.u_arr; + } + + ev_iterator ev_end() { + return d_children.u_arr + d_nchildren; + } + + NodeBuilder& reset(const ExprValue*); + +public: + + NodeBuilder(); + NodeBuilder(Kind k); + NodeBuilder(const Node&); + NodeBuilder(const NodeBuilder&); + + NodeBuilder(NodeManager*); + NodeBuilder(NodeManager*, Kind k); + NodeBuilder(NodeManager*, const Node&); + NodeBuilder(NodeManager*, const NodeBuilder&); + + ~NodeBuilder(); + + // Compound expression constructors + NodeBuilder& eqExpr(const Node& right); + NodeBuilder& notExpr(); + NodeBuilder& negate(); // avoid double-negatives + NodeBuilder& andExpr(const Node& right); + NodeBuilder& orExpr(const Node& right); + NodeBuilder& iteExpr(const Node& thenpart, const Node& elsepart); + NodeBuilder& iffExpr(const Node& right); + NodeBuilder& impExpr(const Node& right); + NodeBuilder& xorExpr(const Node& right); + + /* TODO design: these modify NodeBuilder */ + NodeBuilder& operator!() { return notExpr(); } + NodeBuilder& operator&&(const Node& right) { return andExpr(right); } + NodeBuilder& operator||(const Node& right) { return orExpr(right); } + + // "Stream" expression constructor syntax + NodeBuilder& operator<<(const Kind& op); + NodeBuilder& operator<<(const Node& child); + + // For pushing sequences of children + NodeBuilder& append(const std::vector<Node>& children) { return append(children.begin(), children.end()); } + NodeBuilder& append(Node child) { return append(&child, (&child) + 1); } + template <class Iterator> NodeBuilder& append(const Iterator& begin, const Iterator& end); + + operator Node();// not const + + AndExprBuilder operator&&(Node); + OrExprBuilder operator||(Node); + PlusExprBuilder operator+ (Node); + PlusExprBuilder operator- (Node); + MultExprBuilder operator* (Node); + + friend class AndExprBuilder; + friend class OrExprBuilder; + friend class PlusExprBuilder; + friend class MultExprBuilder; +};/* class NodeBuilder */ + +class AndExprBuilder { + NodeBuilder d_eb; + +public: + + AndExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != AND) { + d_eb.collapse(); + d_eb.d_kind = AND; + } + } + + AndExprBuilder& operator&&(Node); + OrExprBuilder operator||(Node); + + operator NodeBuilder() { return d_eb; } + +};/* class AndExprBuilder */ + +class OrExprBuilder { + NodeBuilder d_eb; + +public: + + OrExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != OR) { + d_eb.collapse(); + d_eb.d_kind = OR; + } + } + + AndExprBuilder operator&&(Node); + OrExprBuilder& operator||(Node); + + operator NodeBuilder() { return d_eb; } + +};/* class OrExprBuilder */ + +class PlusExprBuilder { + NodeBuilder d_eb; + +public: + + PlusExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != PLUS) { + d_eb.collapse(); + d_eb.d_kind = PLUS; + } + } + + PlusExprBuilder& operator+(Node); + PlusExprBuilder& operator-(Node); + MultExprBuilder operator*(Node); + + operator NodeBuilder() { return d_eb; } + +};/* class PlusExprBuilder */ + +class MultExprBuilder { + NodeBuilder d_eb; + +public: + + MultExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != MULT) { + d_eb.collapse(); + d_eb.d_kind = MULT; + } + } + + PlusExprBuilder operator+(Node); + PlusExprBuilder operator-(Node); + MultExprBuilder& operator*(Node); + + operator NodeBuilder() { return d_eb; } + +};/* class MultExprBuilder */ + +template <class Iterator> +inline NodeBuilder& NodeBuilder::append(const Iterator& begin, const Iterator& end) { + for(Iterator i = begin; i != end; ++i) + addChild(*i); + return *this; +} + +// not const +inline NodeBuilder::operator Node() { + ExprValue *ev; + uint64_t hash; + + Assert(d_kind != UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); + + // variables are permitted to be duplicates (from POV of the expression manager) + if(d_kind == VARIABLE) { + ev = new ExprValue; + hash = reinterpret_cast<uint64_t>(ev); + } else { + if(d_nchildren <= nchild_thresh) { + hash = ExprValue::computeHash<ev_iterator>(d_kind, ev_begin(), ev_end()); + void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node)); + ev = new (space) ExprValue; + size_t nc = 0; + ev_iterator i = ev_begin(); + ev_iterator i_end = ev_end(); + for(; i != i_end; ++i) { + // The expressions in the allocated children are all 0, so we must + // construct it withouth using an assignment operator + ev->d_children[nc++].assignExprValue(*i); + } + } else { + hash = ExprValue::computeHash<std::vector<Node>::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end()); + void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node)); + ev = new (space) ExprValue; + size_t nc = 0; + for(std::vector<Node>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i) + ev->d_children[nc++] = Node(*i); + } + } + + ev->d_nchildren = d_nchildren; + ev->d_kind = d_kind; + ev->d_id = ExprValue::next_id++;// FIXME multithreading + ev->d_rc = 0; + Node e(ev); + + return d_em->lookup(hash, e); +} + +inline AndExprBuilder NodeBuilder::operator&&(Node e) { + return AndExprBuilder(*this) && e; +} + +inline OrExprBuilder NodeBuilder::operator||(Node e) { + return OrExprBuilder(*this) || e; +} + +inline PlusExprBuilder NodeBuilder::operator+ (Node e) { + return PlusExprBuilder(*this) + e; +} + +inline PlusExprBuilder NodeBuilder::operator- (Node e) { + return PlusExprBuilder(*this) - e; +} + +inline MultExprBuilder NodeBuilder::operator* (Node e) { + return MultExprBuilder(*this) * e; +} + +inline AndExprBuilder& AndExprBuilder::operator&&(Node e) { + d_eb.append(e); + return *this; +} + +inline OrExprBuilder AndExprBuilder::operator||(Node e) { + return OrExprBuilder(d_eb.collapse()) || e; +} + +inline AndExprBuilder OrExprBuilder::operator&&(Node e) { + return AndExprBuilder(d_eb.collapse()) && e; +} + +inline OrExprBuilder& OrExprBuilder::operator||(Node e) { + d_eb.append(e); + return *this; +} + +inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) { + d_eb.append(e); + return *this; +} + +inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) { + d_eb.append(e.negate()); + return *this; +} + +inline MultExprBuilder PlusExprBuilder::operator*(Node e) { + return MultExprBuilder(d_eb.collapse()) * e; +} + +inline PlusExprBuilder MultExprBuilder::operator+(Node e) { + return MultExprBuilder(d_eb.collapse()) + e; +} + +inline PlusExprBuilder MultExprBuilder::operator-(Node e) { + return MultExprBuilder(d_eb.collapse()) - e; +} + +inline MultExprBuilder& MultExprBuilder::operator*(Node e) { + d_eb.append(e); + return *this; +} + + +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR_BUILDER_H */ |