diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-03 14:59:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-03 14:59:30 +0000 |
commit | 7fb54afe126e5045fc6c5553c1aff3c3f73509aa (patch) | |
tree | 37f4f23af0eccd6c9615a5af9b2d219e305d1f78 /src/expr | |
parent | bde1a14afc211c8f0f0521bb91feb562eaa9f9ea (diff) |
parsing/expr/command/result/various other fixes
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr.cpp | 8 | ||||
-rw-r--r-- | src/expr/expr.h | 57 | ||||
-rw-r--r-- | src/expr/expr_builder.h | 29 | ||||
-rw-r--r-- | src/expr/expr_manager.h | 49 | ||||
-rw-r--r-- | src/expr/expr_value.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr_value.h | 6 | ||||
-rw-r--r-- | src/expr/kind.h | 36 |
7 files changed, 178 insertions, 9 deletions
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index f94a3c438..2e3d7a7e2 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -22,16 +22,18 @@ Expr Expr::s_null(0); Expr::Expr(ExprValue* ev) : d_ev(ev) { - d_ev->inc(); + if(d_ev != 0) + d_ev->inc(); } Expr::Expr(const Expr& e) { - if((d_ev = e.d_ev)) + if((d_ev = e.d_ev) && d_ev != 0) d_ev->inc(); } Expr::~Expr() { - d_ev->dec(); + if(d_ev) + d_ev->dec(); } Expr& Expr::operator=(const Expr& e) { diff --git a/src/expr/expr.h b/src/expr/expr.h index 19f02650e..5a11e0fbd 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -14,12 +14,23 @@ #define __CVC4__EXPR_H #include <vector> +#include <iostream> #include <stdint.h> #include "cvc4_config.h" #include "expr/kind.h" namespace CVC4 { + class Expr; +}/* CVC4 namespace */ + +namespace std { +inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC; +} + +namespace CVC4 { + +class ExprManager; namespace expr { class ExprValue; @@ -45,10 +56,8 @@ class CVC4_PUBLIC Expr { * Increments the reference count. */ explicit Expr(ExprValue*); - typedef Expr* iterator; - typedef Expr const* const_iterator; - friend class ExprBuilder; + friend class ExprManager; public: CVC4_PUBLIC Expr(const Expr&); @@ -81,20 +90,62 @@ public: inline Kind getKind() const; + inline size_t numChildren() const; + static Expr null() { return s_null; } + typedef Expr* iterator; + typedef Expr const* const_iterator; + + inline iterator begin(); + inline iterator end(); + inline iterator begin() const; + inline iterator end() const; + + void toString(std::ostream&) const; };/* class Expr */ }/* CVC4 namespace */ #include "expr/expr_value.h" +inline std::ostream& std::operator<<(std::ostream& out, CVC4::Expr e) { + e.toString(out); + return out; +} + namespace CVC4 { inline Kind Expr::getKind() const { return Kind(d_ev->d_kind); } +inline void Expr::toString(std::ostream& out) const { + if(d_ev) + d_ev->toString(out); + else out << "null"; +} + +inline Expr::iterator Expr::begin() { + return d_ev->begin(); +} + +inline Expr::iterator Expr::end() { + return d_ev->end(); +} + +inline Expr::iterator Expr::begin() const { + return d_ev->begin(); +} + +inline Expr::iterator Expr::end() const { + return d_ev->end(); +} + +inline size_t Expr::numChildren() const { + return d_ev->d_nchildren; +} + }/* CVC4 namespace */ #endif /* __CVC4__EXPR_H */ diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index 13f196dd0..5c6019de1 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -13,6 +13,8 @@ #define __CVC4__EXPR_BUILDER_H #include <vector> +#include <cstdlib> + #include "expr_manager.h" #include "kind.h" @@ -48,6 +50,14 @@ class ExprBuilder { 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; + } + ExprBuilder& reset(const ExprValue*); public: @@ -188,8 +198,23 @@ inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& e // not const inline ExprBuilder::operator Expr() { - // FIXME - return Expr::s_null; + uint64_t hash = d_kind; + + for(ev_iterator i = ev_begin(); i != ev_end(); ++i) + hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash(); + + 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_rc = 0; + Expr e(ev); + + return d_em->lookup(hash, e); } inline AndExprBuilder ExprBuilder::operator&&(Expr e) { diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index e3fbd91bf..ee18ddc01 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -13,14 +13,61 @@ #define __CVC4__EXPR_MANAGER_H #include <vector> +#include <map> + #include "expr/expr.h" #include "kind.h" namespace CVC4 { -class ExprManager { +namespace expr { + class ExprBuilder; +}/* CVC4::expr namespace */ + +class CVC4_PUBLIC ExprManager { static __thread ExprManager* s_current; + friend class CVC4::ExprBuilder; + + 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; + } + } + public: static ExprManager* currentEM() { return s_current; } diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index fa5628e26..e24bb88b1 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -18,6 +18,8 @@ namespace CVC4 { +size_t ExprValue::next_id = 0; + uint64_t ExprValue::hash() const { uint64_t hash = d_kind; diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index 0b97dfdae..decd57045 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -63,6 +63,8 @@ class ExprValue { ExprValue* inc(); ExprValue* dec(); + static size_t next_id; + public: /** Hash this expression. * @return the hash value of this expression. */ @@ -82,6 +84,10 @@ public: const_iterator end() const; const_iterator rbegin() const; const_iterator rend() const; + + void toString(std::ostream& out) { + out << Kind(d_kind); + } }; }/* CVC4::expr namespace */ diff --git a/src/expr/kind.h b/src/expr/kind.h index db25d914e..790fd644d 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -12,6 +12,8 @@ #ifndef __CVC4__KIND_H #define __CVC4__KIND_H +#include <iostream> + namespace CVC4 { // TODO: create this file (?) from theory solver headers so that we @@ -49,4 +51,38 @@ 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) { + using namespace CVC4; + + switch(k) { + case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break; + case EQUAL: out << "EQUAL"; break; + case ITE: out << "ITE"; break; + case SKOLEM: out << "SKOLEM"; break; + case VARIABLE: out << "VARIABLE"; break; + + /* propositional connectives */ + case FALSE: out << "FALSE"; break; + case TRUE: out << "TRUE"; break; + + case NOT: out << "NOT"; break; + + case AND: out << "AND"; break; + case IFF: out << "IFF"; break; + case IMPLIES: out << "IMPLIES"; break; + case OR: out << "OR"; break; + case XOR: out << "XOR"; break; + + /* from arith */ + case PLUS: out << "PLUS"; break; + case MINUS: out << "MINUS"; break; + case MULT: out << "MULT"; break; + + default: out << "UNKNOWNKIND!"; break; + } + + return out; +} + #endif /* __CVC4__KIND_H */ |