summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/expr.cpp8
-rw-r--r--src/expr/expr.h57
-rw-r--r--src/expr/expr_builder.h29
-rw-r--r--src/expr/expr_manager.h49
-rw-r--r--src/expr/expr_value.cpp2
-rw-r--r--src/expr/expr_value.h6
-rw-r--r--src/expr/kind.h36
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback