diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr.h | 14 | ||||
-rw-r--r-- | src/expr/expr_builder.cpp | 14 | ||||
-rw-r--r-- | src/expr/expr_builder.h | 45 | ||||
-rw-r--r-- | src/expr/expr_manager.cpp | 40 | ||||
-rw-r--r-- | src/expr/expr_manager.h | 39 | ||||
-rw-r--r-- | src/expr/expr_value.cpp | 18 | ||||
-rw-r--r-- | src/expr/expr_value.h | 6 | ||||
-rw-r--r-- | src/expr/kind.h | 11 |
8 files changed, 126 insertions, 61 deletions
diff --git a/src/expr/expr.h b/src/expr/expr.h index a16ffee13..013888baa 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -60,19 +60,23 @@ class CVC4_PUBLIC Expr { public: /** Default constructor, makes a null expression. */ - CVC4_PUBLIC Expr(); + Expr(); - CVC4_PUBLIC Expr(const Expr&); + Expr(const Expr&); /** Destructor. Decrements the reference count and, if zero, * collects the ExprValue. */ - CVC4_PUBLIC ~Expr(); + ~Expr(); - Expr& operator=(const Expr&) CVC4_PUBLIC; + bool operator==(const Expr& e) const { return d_ev == e.d_ev; } + bool operator!=(const Expr& e) const { return d_ev != e.d_ev; } + bool operator<(const Expr& e) const { return d_ev < e.d_ev; }// for map key + + Expr& operator=(const Expr&); /** Access to the encapsulated expression. * @return the encapsulated expression. */ - ExprValue* operator->() const CVC4_PUBLIC; + ExprValue* operator->() const; uint64_t hash() const; 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; } diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index 5c6019de1..d70acb1fb 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -96,7 +96,7 @@ public: // For pushing sequences of children ExprBuilder& append(const std::vector<Expr>& children) { return append(children.begin(), children.end()); } - ExprBuilder& append(Expr child) { return append(&child, &(child)+1); } + ExprBuilder& append(Expr child) { return append(&child, (&child) + 1); } template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end); operator Expr();// not const @@ -193,24 +193,47 @@ public: template <class Iterator> inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) { + for(Iterator i = begin; i != end; ++i) + addChild(*i); return *this; } // not const inline ExprBuilder::operator Expr() { - uint64_t hash = d_kind; - - for(ev_iterator i = ev_begin(); i != ev_end(); ++i) - hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash(); + ExprValue *ev; + uint64_t hash; + + // 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 { + hash = d_kind; + + if(d_nchildren <= nchild_thresh) { + for(ev_iterator i = ev_begin(); i != ev_end(); ++i) + hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash(); + + void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr)); + ev = new (space) ExprValue; + size_t nc = 0; + for(ev_iterator i = ev_begin(); i != ev_end(); ++i) + ev->d_children[nc++] = Expr(*i); + } else { + for(std::vector<Expr>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i) + hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash(); + + void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr)); + ev = new (space) ExprValue; + size_t nc = 0; + for(std::vector<Expr>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i) + ev->d_children[nc++] = Expr(*i); + } + } - void *space = std::malloc(sizeof(ExprValue) + d_nchildren * sizeof(Expr)); - ExprValue *ev = new (space) ExprValue; - size_t nc = 0; - for(ev_iterator i = ev_begin(); i != ev_end(); ++i) - ev->d_children[nc++] = Expr(*i); ev->d_nchildren = d_nchildren; ev->d_kind = d_kind; - ev->d_id = ExprValue::next_id++; + ev->d_id = ExprValue::next_id++;// FIXME multithreading ev->d_rc = 0; Expr e(ev); diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 3aeab8049..9b7697e4f 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -18,6 +18,42 @@ namespace CVC4 { __thread ExprManager* ExprManager::s_current = 0; +Expr ExprManager::lookup(uint64_t hash, const Expr& e) { + hash_t::iterator i = d_hash.find(hash); + if(i == d_hash.end()) { + // insert + std::vector<Expr> v; + v.push_back(e); + d_hash.insert(std::make_pair(hash, v)); + return e; + } else { + for(std::vector<Expr>::iterator j = i->second.begin(); j != i->second.end(); ++j) { + if(e.getKind() != j->getKind()) + continue; + + if(e.numChildren() != j->numChildren()) + continue; + + Expr::iterator c1 = e.begin(); + Expr::iterator c2 = j->begin(); + for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) { + if(c1->d_ev != c2->d_ev) + break; + } + + if(c1 != e.end() || c2 != j->end()) + continue; + + return *j; + } + // didn't find it, insert + std::vector<Expr> v; + v.push_back(e); + d_hash.insert(std::make_pair(hash, v)); + return e; + } +} + // general expression-builders Expr ExprManager::mkExpr(Kind kind) { @@ -49,4 +85,8 @@ Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) { return ExprBuilder(this, kind).append(children); } +Expr ExprManager::mkVar() { + return ExprBuilder(this, VARIABLE); +} + }/* CVC4 namespace */ diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index ee18ddc01..d311445f3 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -32,41 +32,7 @@ class CVC4_PUBLIC ExprManager { typedef std::map<uint64_t, std::vector<Expr> > hash_t; hash_t d_hash; - Expr lookup(uint64_t hash, const Expr& e) { - hash_t::iterator i = d_hash.find(hash); - if(i == d_hash.end()) { - // insert - std::vector<Expr> v; - v.push_back(e); - d_hash.insert(std::make_pair(hash, v)); - return e; - } else { - for(std::vector<Expr>::iterator j = i->second.begin(); j != i->second.end(); ++j) { - if(e.getKind() != j->getKind()) - continue; - - if(e.numChildren() != j->numChildren()) - continue; - - Expr::iterator c1 = e.begin(); - Expr::iterator c2 = j->begin(); - while(c1 != e.end() && c2 != j->end()) { - if(c1->d_ev != c2->d_ev) - break; - } - - if(c1 != e.end() || c2 != j->end()) - continue; - - return *j; - } - // didn't find it, insert - std::vector<Expr> v; - v.push_back(e); - d_hash.insert(std::make_pair(hash, v)); - return e; - } - } + Expr lookup(uint64_t hash, const Expr& e); public: static ExprManager* currentEM() { return s_current; } @@ -81,6 +47,9 @@ public: // N-ary version Expr mkExpr(Kind kind, std::vector<Expr> children); + // variables are special, because duplicates are permitted + Expr mkVar(); + // TODO: these use the current EM (but must be renamed) /* static Expr mkExpr(Kind kind) diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index c511c580a..250803281 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -18,12 +18,12 @@ namespace CVC4 { +size_t ExprValue::next_id = 1; + ExprValue::ExprValue() : d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) { } -size_t ExprValue::next_id = 1; - uint64_t ExprValue::hash() const { uint64_t hash = d_kind; @@ -82,4 +82,18 @@ ExprValue::const_iterator ExprValue::rend() const { return d_children - 1; } +void ExprValue::toString(std::ostream& out) const { + out << "(" << Kind(d_kind); + if(d_kind == VARIABLE) { + out << ":" << this; + } else { + for(const_iterator i = begin(); i != end(); ++i) { + if(i != end()) + out << " "; + out << *i; + } + } + out << ")"; +} + }/* CVC4 namespace */ diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index 6df7ad76f..18ad84073 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -21,7 +21,9 @@ #ifndef __CVC4__EXPR__EXPR_VALUE_H #define __CVC4__EXPR__EXPR_VALUE_H +#include "cvc4_config.h" #include <stdint.h> +#include "kind.h" namespace CVC4 { @@ -92,9 +94,7 @@ public: const_iterator rbegin() const; const_iterator rend() const; - void toString(std::ostream& out) { - out << Kind(d_kind); - } + void CVC4_PUBLIC toString(std::ostream& out) const; }; }/* CVC4::expr namespace */ diff --git a/src/expr/kind.h b/src/expr/kind.h index 49321b47f..5ac02ca7c 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -51,15 +51,16 @@ enum Kind { };/* enum Kind */ -}/* CVC4 namespace */ - -inline std::ostream& operator<<(std::ostream&, const CVC4::Kind&) CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream& out, const CVC4::Kind& k) { +inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) { using namespace CVC4; switch(k) { + + /* special cases */ case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break; case NULL_EXPR: out << "NULL"; break; + case EQUAL: out << "EQUAL"; break; case ITE: out << "ITE"; break; case SKOLEM: out << "SKOLEM"; break; @@ -88,4 +89,6 @@ inline std::ostream& operator<<(std::ostream& out, const CVC4::Kind& k) { return out; } +}/* CVC4 namespace */ + #endif /* __CVC4__KIND_H */ |