summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/attribute.h17
-rw-r--r--src/expr/node.h17
-rw-r--r--src/expr/node_builder.h13
-rw-r--r--src/theory/theory.cpp15
-rw-r--r--src/theory/theory.h13
-rw-r--r--src/theory/uf/ecdata.h22
-rw-r--r--src/theory/uf/theory_uf.cpp126
-rw-r--r--src/theory/uf/theory_uf.h67
8 files changed, 234 insertions, 56 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 95433688e..5620d7795 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -86,10 +86,10 @@ struct KindValueToTableValueMapping<bool> {
template <class T>
struct KindValueToTableValueMapping<T*> {
typedef void* table_value_type;
- inline static void* convert(const T*& t) {
- return reinterpret_cast<void*>(t);
+ inline static void* convert(const T* const& t) {
+ return reinterpret_cast<void*>(const_cast<T*>(t));
}
- inline static T* convertBack(void*& t) {
+ inline static T* convertBack(void* const& t) {
return reinterpret_cast<T*>(t);
}
};
@@ -455,6 +455,17 @@ struct getTable<const T*> {
}
};
+template <class T>
+struct getTable<T*> {
+ typedef AttrHash<void*> table_type;
+ static inline table_type& get(AttributeManager& am) {
+ return am.d_ptrs;
+ }
+ static inline const table_type& get(const AttributeManager& am) {
+ return am.d_ptrs;
+ }
+};
+
// ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
template <class AttrKind>
diff --git a/src/expr/node.h b/src/expr/node.h
index e1085a32a..03f3e9da3 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -325,6 +325,15 @@ template<bool ref_count>
NodeTemplate uMinusNode() const;
NodeTemplate multNode(const NodeTemplate& right) const;
+ /**
+ * Sets the given attribute of this node to the given value.
+ * @param attKind the kind of the atribute
+ * @param value the value to set the attribute to
+ */
+ template<class AttrKind>
+ inline void setAttribute(const AttrKind& attKind,
+ const typename AttrKind::value_type& value);
+
private:
/**
@@ -334,14 +343,6 @@ template<bool ref_count>
*/
void debugPrint();
- /**
- * Sets the given attribute of this node to the given value.
- * @param attKind the kind of the atribute
- * @param value the value to set the attribute to
- */
- template<class AttrKind>
- inline void setAttribute(const AttrKind& attKind,
- const typename AttrKind::value_type& value);
/**
* Indents the given stream a given amount of spaces.
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 61b048a5b..d79d5ad54 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -47,6 +47,7 @@ class MultNodeBuilder;
template <unsigned nchild_thresh>
class NodeBuilder {
+
unsigned d_size;
uint64_t d_hash;
@@ -129,14 +130,17 @@ public:
}
Kind getKind() const {
+ Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
return d_nv->getKind();
}
unsigned getNumChildren() const {
+ Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
return d_nv->getNumChildren();
}
Node operator[](int i) const {
+ Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
Assert(i >= 0 && i < d_nv->getNumChildren());
return Node(d_nv->d_children[i]);
}
@@ -225,6 +229,11 @@ public:
friend class PlusNodeBuilder;
friend class MultNodeBuilder;
*/
+
+ //Yet 1 more example of how terrifying C++ is as a language
+ //This is needed for copy constructors of different sizes to access private fields
+ template <unsigned N> friend class NodeBuilder;
+
};/* class NodeBuilder */
#if 0
@@ -439,9 +448,9 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) :
if(nb.d_nv->d_nchildren > nchild_thresh) {
realloc(nb.d_size, false);
- std::copy(nb.d_nv->ev_begin(), nb.d_nv->end(), d_nv->nv_begin());
+ std::copy(nb.d_nv->ev_begin(), nb.d_nv->ev_end(), d_nv->nv_begin());
} else {
- std::copy(nb.d_nv->ev_begin(), nb.d_nv->end(), d_inlineNv.nv_begin());
+ std::copy(nb.d_nv->ev_begin(), nb.d_nv->ev_end(), d_inlineNv.nv_begin());
}
d_nv->d_kind = nb.d_nv->d_kind;
d_nv->d_nchildren = nb.d_nv->d_nchildren;
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 61b2fdfa3..cf52de75e 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -18,5 +18,20 @@
namespace CVC4 {
namespace theory {
+bool Theory::done() {
+ return d_nextAssertion >= d_assertions.size();
+}
+
+
+Node Theory::get() {
+ Node n = d_assertions[d_nextAssertion];
+ d_nextAssertion = d_nextAssertion + 1;
+ return n;
+}
+
+void Theory::assertFact(const Node& n){
+ d_assertions.push_back(n);
+}
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 831a185f8..76b9697dc 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -60,8 +60,7 @@ public:
/**
* Construct a Theory.
*/
- Theory() {
- }
+ Theory(context::Context* c) : d_assertions(c), d_nextAssertion(c, 0){}
/**
* Destructs a Theory. This implementation does nothing, but we
@@ -82,7 +81,10 @@ public:
* setup() MUST NOT MODIFY context-dependent objects that it hasn't
* itself just created.
*/
- virtual void setup(const Node& n) = 0;
+
+ /*virtual void setup(const Node& n) = 0;*/
+
+ virtual void registerTerm(TNode n) = 0;
/**
* Assert a fact in the current context.
@@ -109,6 +111,9 @@ public:
virtual void explain(OutputChannel& out,
const Node& n,
Effort level = FULL_EFFORT) = 0;
+private:
+ context::CDList<Node> d_assertions;
+ context::CDO<unsigned> d_nextAssertion;
protected:
/**
@@ -121,7 +126,7 @@ protected:
/**
* Returns true if the assertFactQueue is empty
*/
- bool done() { return true; }
+ bool done();
};/* class Theory */
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h
index c8303a245..221512669 100644
--- a/src/theory/uf/ecdata.h
+++ b/src/theory/uf/ecdata.h
@@ -26,10 +26,13 @@ namespace theory {
struct Link {
context::CDO< Link* > next;
-
- //TODO soft reference
+
+ /**
+ * As I have not yet succeeded in justifying to myself that soft references are safe
+ * I am leaving this a hard refernce for now.
+ */
Node data;
-
+
Link(context::Context* context, Node n, Link * l = NULL):
next(context, l), data(n)
{}
@@ -37,20 +40,23 @@ struct Link {
static void* operator new(size_t size, context::ContextMemoryManager* pCMM) {
return pCMM->newData(size);
}
-
+
};
class ECData : public context::ContextObj {
private:
- ECData * find;
+ ECData* find;
+ /**
+ * Is it safe to make this a soft link? Why or why not?
+ */
Node rep;
-
+
unsigned watchListSize;
- Link * first;
- Link * last;
+ Link* first;
+ Link* last;
context::ContextObj* save(context::ContextMemoryManager* pCMM);
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 6f9171f36..652eb4a55 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -23,29 +23,94 @@ using namespace theory;
using namespace context;
-/* Temporaries to facilitate compiling. */
-enum TmpEnum {EC};
-void setAttribute(Node n, TmpEnum te, ECData * ec){}
-ECData* getAttribute(Node n, TmpEnum te) { return NULL; }
Node getOperator(Node x) { return Node::null(); }
-void TheoryUF::setup(const Node& n){
- ECData * ecN = new (true) ECData(d_context, n);
- //TODO Make sure attribute manager owns the pointer
- setAttribute(n, EC, ecN);
+TheoryUF::TheoryUF(Context* c) :
+ Theory(c), d_pending(c), d_currentPendingIdx(c,0), d_disequality(c)
+{}
+
+TheoryUF::~TheoryUF(){}
+
+void TheoryUF::registerTerm(TNode n){
+
+ ECData* ecN;
+
+ if(n.hasAttribute(ECAttr(),&ecN)){
+ /* registerTerm(n) is only called when a node has not been seen in the
+ * current context. ECAttr() is not a context-dependent attribute.
+ * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call,
+ * then it must be the case that this attribute was created in a previous
+ * and no longer valid context. Because of this we have to reregister the
+ * predecessors lists.
+ * Also we do not have to worry about duplicates because all of the Link*
+ * setup before are removed when the context n was setup in was popped out
+ * of. All we are going to do here are sanity checks.*/
+
+ /*
+ * Consider the following chain of events:
+ * 1) registerTerm(n) is called on node n where n : f(m) in context level X,
+ * 2) A new ECData is created on the heap, ecN,
+ * 3) n is added to the predessecor list of m in context level X,
+ * 4) We pop out of X,
+ * 5) n is removed from the predessecor list of m because this is context
+ * dependent, the Link* will be destroyed and pointers to the Link
+ * structs in the ECData objects will be updated.
+ * 6) registerTerm(n) is called on node n in context level Y,
+ * 7) If n.hasAttribute(ECAttr(), &ecN), then ecN is still around,
+ * but the predecessor list is not
+ *
+ * The above assumes that the code is working correctly.
+ */
+ Assert(ecN->getFirst() == NULL,
+ "Equivalence class data exists for the node being registered. "
+ "Expected getFirst() == NULL. "
+ "This data is either already in use or was not properly maintained "
+ "during backtracking");
+ /*Assert(ecN->getLast() == NULL,
+ "Equivalence class data exists for the node being registered. "
+ "Expected getLast() == NULL. "
+ "This data is either already in use or was not properly maintained "
+ "during backtracking.");*/
+ Assert(ecN->isClassRep(),
+ "Equivalence class data exists for the node being registered. "
+ "Expected isClassRep() to be true. "
+ "This data is either already in use or was not properly maintained "
+ "during backtracking");
+ Assert(ecN->getWatchListSize() == 0,
+ "Equivalence class data exists for the node being registered. "
+ "Expected getWatchListSize() == 0. "
+ "This data is either already in use or was not properly maintained "
+ "during backtracking");
+ }else{
+ ecN = new (true) ECData(d_context, n);
+ n.setAttribute(ECAttr(), ecN);
+ }
if(n.getKind() == APPLY){
- for(Node::iterator cIter = n.begin(); cIter != n.end(); ++cIter){
- Node child = *cIter;
-
- ECData * ecChild = getAttribute(child, EC);
+ for(TNode::iterator cIter = n.begin(); cIter != n.end(); ++cIter){
+ TNode child = *cIter;
+
+ ECData* ecChild = child.getAttribute(ECAttr());
ecChild = ccFind(ecChild);
+ for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->next ){
+ if(equiv(n, Px->data)){
+ d_pending.push_back(n.eqNode(Px->data));
+ }
+ }
+
ecChild->addPredecessor(n, d_context);
}
}
+
+}
+
+bool TheoryUF::sameCongruenceClass(TNode x, TNode y){
+ return
+ ccFind(x.getAttribute(ECAttr())) ==
+ ccFind(y.getAttribute(ECAttr()));
}
bool TheoryUF::equiv(Node x, Node y){
@@ -59,10 +124,10 @@ bool TheoryUF::equiv(Node x, Node y){
Node::iterator yIter = y.begin();
while(xIter != x.end()){
-
- if(ccFind(getAttribute(*xIter, EC)) !=
- ccFind(getAttribute(*yIter, EC)))
+
+ if(!sameCongruenceClass(*xIter, *yIter)){
return false;
+ }
++xIter;
++yIter;
@@ -106,18 +171,17 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){
//TODO make parameters soft references
void TheoryUF::merge(){
do{
- Node assertion = d_pending[d_currentPendingIdx];
+ TNode assertion = d_pending[d_currentPendingIdx];
d_currentPendingIdx = d_currentPendingIdx + 1;
-
- Node x = assertion[0];
- Node y = assertion[1];
-
- ECData* ecX = ccFind(getAttribute(x, EC));
- ECData* ecY = ccFind(getAttribute(y, EC));
-
+
+ TNode x = assertion[0];
+ TNode y = assertion[1];
+
+ ECData* ecX = ccFind(x.getAttribute(ECAttr()));
+ ECData* ecY = ccFind(y.getAttribute(ECAttr()));
if(ecX == ecY)
continue;
-
+
ccUnion(ecX, ecY);
}while( d_currentPendingIdx < d_pending.size() );
}
@@ -125,7 +189,6 @@ void TheoryUF::merge(){
void TheoryUF::check(OutputChannel& out, Effort level){
while(!done()){
Node assertion = get();
-
switch(assertion.getKind()){
case EQUAL:
@@ -139,13 +202,20 @@ void TheoryUF::check(OutputChannel& out, Effort level){
Unreachable();
}
}
+
+ //Make sure all outstanding merges are completed.
+ if(d_currentPendingIdx < d_pending.size()){
+ merge();
+ }
+
if(fullEffort(level)){
for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
diseqIter != d_disequality.end();
++diseqIter){
-
- if(ccFind(getAttribute((*diseqIter)[0], EC)) ==
- ccFind(getAttribute((*diseqIter)[1], EC))){
+
+ TNode left = (*diseqIter)[0];
+ TNode right = (*diseqIter)[1];
+ if(sameCongruenceClass(left, right)){
out.conflict(*diseqIter, true);
}
}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 0ab51ca2c..6a1dfb886 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -18,23 +18,44 @@
#define __CVC4__THEORY__THEORY_UF_H
#include "expr/node.h"
+#include "expr/attribute.h"
+
#include "theory/theory.h"
#include "theory/output_channel.h"
+
#include "context/context.h"
#include "theory/uf/ecdata.h"
namespace CVC4 {
namespace theory {
+
class TheoryUF : public Theory {
private:
+
+ /**
+ * The associated context. Needed for allocating context dependent objects
+ * and objects in context dependent memory.
+ */
context::Context* d_context;
+
+ /** List of pending equivalence class merges. */
context::CDList<Node> d_pending;
- context::CDList<Node> d_disequality;
+
+ /** Index of the next pending equality to merge. */
context::CDO<unsigned> d_currentPendingIdx;
+ /** List of all disequalities this theory has seen. */
+ context::CDList<Node> d_disequality;
+
+
public:
- void setup(const Node& n);
+
+ TheoryUF(context::Context* c);
+ ~TheoryUF();
+
+ void registerTerm(TNode n);
+
void check(OutputChannel& out, Effort level= FULL_EFFORT);
@@ -45,16 +66,56 @@ public:
Effort level = FULL_EFFORT){}
private:
+ /**
+ * Checks whether 2 nodes are already in the same equivalence class tree.
+ * This should only be used internally, and it should only be done when
+ * the only thing done with the equivalence classes is an equality check.
+ *
+ * @returns true iff ccFind(x) == ccFind(y);
+ */
+ bool sameCongruenceClass(TNode x, TNode y);
+
+ /**
+ * Checks whether Node x and Node y are currently congruent
+ * using the equivalence class data structures.
+ * @returns true iff
+ * |x| = n = |y| and
+ * x.getOperator() == y.getOperator() and
+ * forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i])
+ */
bool equiv(Node x, Node y);
+
+ /**
+ * Merges 2 equivalence classes, checks wether any predecessors need to
+ * be set equal to complete congruence closure.
+ * The class with the smaller class size will be merged.
+ * @pre ecX->isClassRep()
+ * @pre ecY->isClassRep()
+ */
void ccUnion(ECData* ecX, ECData* ecY);
+
+ /**
+ * Returns the representative of the equivalence class.
+ * May modify the find pointers associated with equivalence classes.
+ */
ECData* ccFind(ECData* x);
+ /* Performs Congruence Closure to reflect the new additions to d_pending. */
void merge();
- //TODO put back in theory
+
+};
+
+struct ECCleanupFcn{
+ static void cleanup(ECData* & ec){
+ ec->deleteSelf();
+ }
};
+struct EquivClass;
+typedef expr::Attribute<EquivClass, ECData* /*, ECCleanupFcn*/> ECAttr;
+
} /* CVC4::theory namespace */
} /* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback