summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/expr.h14
-rw-r--r--src/expr/expr_builder.cpp14
-rw-r--r--src/expr/expr_builder.h45
-rw-r--r--src/expr/expr_manager.cpp40
-rw-r--r--src/expr/expr_manager.h39
-rw-r--r--src/expr/expr_value.cpp18
-rw-r--r--src/expr/expr_value.h6
-rw-r--r--src/expr/kind.h11
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback