summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/Makefile.am3
-rw-r--r--src/theory/uf/kinds10
-rw-r--r--src/theory/uf/morgan/theory_uf_morgan.cpp141
-rw-r--r--src/theory/uf/morgan/theory_uf_morgan.h11
-rw-r--r--src/theory/uf/theory_uf.h4
-rw-r--r--src/theory/uf/theory_uf_rewriter.h49
-rw-r--r--src/theory/uf/tim/theory_uf_tim.cpp16
-rw-r--r--src/theory/uf/tim/theory_uf_tim.h18
8 files changed, 130 insertions, 122 deletions
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 04fe533ae..e4647b442 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -11,7 +11,8 @@ nodist_EXTRA_libuf_la_SOURCES = \
libuf_la_SOURCES = \
theory_uf.h \
- theory_uf_type_rules.h
+ theory_uf_type_rules.h \
+ theory_uf_rewriter.h
libuf_la_LIBADD = \
@builddir@/tim/libuftim.la \
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 8cd6aec70..a1fcac1df 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -4,9 +4,17 @@
# src/theory/builtin/kinds.
#
-theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"
+theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h"
+
+properties stable-infinite check propagate staticLearning presolve
+
+rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
+
+sort KIND_TYPE "Uninterpreted Sort"
parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
variable SORT_TAG "sort tag"
parameterized SORT_TYPE SORT_TAG 0: "sort type"
+
+endtheory \ No newline at end of file
diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index cd9ee79c3..33c8bc7b6 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -31,8 +31,8 @@ using namespace CVC4::theory;
using namespace CVC4::theory::uf;
using namespace CVC4::theory::uf::morgan;
-TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) :
- TheoryUF(id, ctxt, out),
+TheoryUFMorgan::TheoryUFMorgan(Context* ctxt, OutputChannel& out) :
+ TheoryUF(ctxt, out),
d_assertions(ctxt),
d_ccChannel(this),
d_cc(ctxt, &d_ccChannel),
@@ -70,23 +70,6 @@ TheoryUFMorgan::~TheoryUFMorgan() {
StatisticsRegistry::unregisterStat(&d_ccNewSkolemVars);
}
-RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) {
- if(topLevel) {
- Debug("uf") << "uf: begin rewrite(" << n << ")" << endl;
- Node ret(n);
- if(n.getKind() == kind::EQUAL ||
- n.getKind() == kind::IFF) {
- if(n[0] == n[1]) {
- ret = NodeManager::currentNM()->mkConst(true);
- }
- }
- Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << endl;
- return RewriteComplete(ret);
- } else {
- return RewriteComplete(n);
- }
-}
-
void TheoryUFMorgan::preRegisterTerm(TNode n) {
Debug("uf") << "uf: preRegisterTerm(" << n << ")" << endl;
if(n.getKind() == kind::EQUAL || n.getKind() == kind::IFF) {
@@ -258,63 +241,63 @@ void TheoryUFMorgan::merge(TNode a, TNode b) {
// disequal to, and the attendant disequality
// FIXME these could be "remembered" and then done in propagation (?)
- EqLists::iterator eq_i = d_equalities.find(a);
- if(eq_i != d_equalities.end()) {
- EqList* eq = (*eq_i).second;
- if(Debug.isOn("uf")) {
- Debug("uf") << "a == " << a << endl;
- Debug("uf") << "size of eq(a) is " << eq->size() << endl;
- }
- for(EqList::const_iterator j = eq->begin(); j != eq->end(); ++j) {
- Debug("uf") << " eq(a) ==> " << *j << endl;
- TNode eqn = *j;
- Assert(eqn.getKind() == kind::EQUAL ||
- eqn.getKind() == kind::IFF);
- TNode s = eqn[0];
- TNode t = eqn[1];
- if(Debug.isOn("uf")) {
- Debug("uf") << " s ==> " << s << endl
- << " t ==> " << t << endl
- << " find(s) ==> " << debugFind(s) << endl
- << " find(t) ==> " << debugFind(t) << endl;
- }
- TNode sp = find(s);
- TNode tp = find(t);
- if(sp == tp) {
- // propagation of equality
- Debug("uf:prop") << " uf-propagating " << eqn << endl;
- ++d_propagations;
- d_out->propagate(eqn);
- } else {
- Assert(sp == b || tp == b);
- appendToEqList(b, eqn);
- if(sp == b) {
- map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(tp);
- if(k != alreadyDiseqs.end()) {
- // propagation of disequality
- // FIXME: this will propagate the same disequality on every
- // subsequent merge, won't it??
- Node deqn = (*k).second.notNode();
- Debug("uf:prop") << " uf-propagating " << deqn << endl;
- ++d_propagations;
- d_out->propagate(deqn);
- }
- } else {
- map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(sp);
- if(k != alreadyDiseqs.end()) {
- // propagation of disequality
- // FIXME: this will propagate the same disequality on every
- // subsequent merge, won't it??
- Node deqn = (*k).second.notNode();
- Debug("uf:prop") << " uf-propagating " << deqn << endl;
- ++d_propagations;
- d_out->propagate(deqn);
- }
- }
- }
- }
- Debug("uf") << "end eq-list." << endl;
- }
+// EqLists::iterator eq_i = d_equalities.find(a);
+// if(eq_i != d_equalities.end()) {
+// EqList* eq = (*eq_i).second;
+// if(Debug.isOn("uf")) {
+// Debug("uf") << "a == " << a << endl;
+// Debug("uf") << "size of eq(a) is " << eq->size() << endl;
+// }
+// for(EqList::const_iterator j = eq->begin(); j != eq->end(); ++j) {
+// Debug("uf") << " eq(a) ==> " << *j << endl;
+// TNode eqn = *j;
+// Assert(eqn.getKind() == kind::EQUAL ||
+// eqn.getKind() == kind::IFF);
+// TNode s = eqn[0];
+// TNode t = eqn[1];
+// if(Debug.isOn("uf")) {
+// Debug("uf") << " s ==> " << s << endl
+// << " t ==> " << t << endl
+// << " find(s) ==> " << debugFind(s) << endl
+// << " find(t) ==> " << debugFind(t) << endl;
+// }
+// TNode sp = find(s);
+// TNode tp = find(t);
+// if(sp == tp) {
+// // propagation of equality
+// Debug("uf:prop") << " uf-propagating " << eqn << endl;
+// ++d_propagations;
+// d_out->propagate(eqn);
+// } else {
+// Assert(sp == b || tp == b);
+// appendToEqList(b, eqn);
+// if(sp == b) {
+// map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(tp);
+// if(k != alreadyDiseqs.end()) {
+// // propagation of disequality
+// // FIXME: this will propagate the same disequality on every
+// // subsequent merge, won't it??
+// Node deqn = (*k).second.notNode();
+// Debug("uf:prop") << " uf-propagating " << deqn << endl;
+// ++d_propagations;
+// d_out->propagate(deqn);
+// }
+// } else {
+// map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(sp);
+// if(k != alreadyDiseqs.end()) {
+// // propagation of disequality
+// // FIXME: this will propagate the same disequality on every
+// // subsequent merge, won't it??
+// Node deqn = (*k).second.notNode();
+// Debug("uf:prop") << " uf-propagating " << deqn << endl;
+// ++d_propagations;
+// d_out->propagate(deqn);
+// }
+// }
+// }
+// }
+// Debug("uf") << "end eq-list." << endl;
+// }
}
void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) {
@@ -564,12 +547,12 @@ void TheoryUFMorgan::propagate(Effort level) {
Debug("uf") << "uf: end propagate(" << level << ")" << endl;
}
-void TheoryUFMorgan::explain(TNode n, Effort level) {
+void TheoryUFMorgan::explain(TNode n) {
TimerStat::CodeTimer codeTimer(d_explainTimer);
- Debug("uf") << "uf: begin explain([" << n << "], " << level << ")" << endl;
+ Debug("uf") << "uf: begin explain([" << n << "])" << endl;
Unimplemented();
- Debug("uf") << "uf: end explain([" << n << "], " << level << ")" << endl;
+ Debug("uf") << "uf: end explain([" << n << "])" << endl;
}
void TheoryUFMorgan::presolve() {
diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
index cbc5f1eab..2a079603b 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.h
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -132,7 +132,7 @@ private:
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUFMorgan(int id, context::Context* ctxt, OutputChannel& out);
+ TheoryUFMorgan(context::Context* ctxt, OutputChannel& out);
/** Destructor for UF theory, cleans up memory and statistics. */
~TheoryUFMorgan();
@@ -170,13 +170,6 @@ public:
void check(Effort level);
/**
- * Rewrites a node in the theory of uninterpreted functions.
- * This is fairly basic and only ensures that atoms that are
- * unsatisfiable or a valid are rewritten to false or true respectively.
- */
- RewriteResponse postRewrite(TNode n, bool topLevel);
-
- /**
* Propagates theory literals.
*
* Overloads void propagate(Effort level); from theory.h.
@@ -190,7 +183,7 @@ public:
* Overloads void explain(TNode n, Effort level); from theory.h.
* See theory/theory.h for more information about this method.
*/
- void explain(TNode n, Effort level);
+ void explain(TNode n);
/**
* The theory should only add (via .operator<< or .append()) to the
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index f745cf402..be3d7ac69 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -37,8 +37,8 @@ class TheoryUF : public Theory {
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUF(int id, context::Context* ctxt, OutputChannel& out)
- : Theory(id, ctxt, out) {}
+ TheoryUF(context::Context* ctxt, OutputChannel& out)
+ : Theory(THEORY_UF, ctxt, out) {}
};/* class TheoryUF */
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
new file mode 100644
index 000000000..e71f74fea
--- /dev/null
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -0,0 +1,49 @@
+/*
+ * theory_uf_rewriter.h
+ *
+ * Created on: Dec 21, 2010
+ * Author: dejan
+ */
+
+#pragma once
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+class TheoryUfRewriter {
+
+public:
+
+ static RewriteResponse postRewrite(TNode node) {
+ if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) {
+ if(node[0] == node[1]) {
+ return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+ }
+ if (node[0] > node[1]) {
+ Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
+ // If we've switched theories, we need to rewrite again (TODO: THIS IS HACK, once theories accept eq, change)
+ if (Theory::theoryOf(newNode[0]) != Theory::theoryOf(newNode[1])) {
+ return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+ } else {
+ return RewriteResponse(REWRITE_DONE, newNode);
+ }
+ }
+ }
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+
+ static RewriteResponse preRewrite(TNode node) {
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+
+ static inline void init() {}
+ static inline void shutdown() {}
+
+};
+
+}
+}
+}
diff --git a/src/theory/uf/tim/theory_uf_tim.cpp b/src/theory/uf/tim/theory_uf_tim.cpp
index ccc37a24b..db0574d4f 100644
--- a/src/theory/uf/tim/theory_uf_tim.cpp
+++ b/src/theory/uf/tim/theory_uf_tim.cpp
@@ -27,8 +27,8 @@ using namespace CVC4::theory;
using namespace CVC4::theory::uf;
using namespace CVC4::theory::uf::tim;
-TheoryUFTim::TheoryUFTim(int id, Context* c, OutputChannel& out) :
- TheoryUF(id, c, out),
+TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out) :
+ TheoryUF(c, out),
d_assertions(c),
d_pending(c),
d_currentPendingIdx(c,0),
@@ -39,18 +39,6 @@ TheoryUFTim::TheoryUFTim(int id, Context* c, OutputChannel& out) :
TheoryUFTim::~TheoryUFTim() {
}
-Node TheoryUFTim::rewrite(TNode n){
- Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
- Node ret(n);
- if(n.getKind() == EQUAL){
- Assert(n.getNumChildren() == 2);
- if(n[0] == n[1]) {
- ret = NodeManager::currentNM()->mkConst(true);
- }
- }
- Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl;
- return ret;
-}
void TheoryUFTim::preRegisterTerm(TNode n) {
Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl;
Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl;
diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h
index 73033f387..cdaa7975c 100644
--- a/src/theory/uf/tim/theory_uf_tim.h
+++ b/src/theory/uf/tim/theory_uf_tim.h
@@ -86,7 +86,7 @@ private:
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUFTim(int id, context::Context* c, OutputChannel& out);
+ TheoryUFTim(context::Context* c, OutputChannel& out);
/** Destructor for the TheoryUF object. */
~TheoryUFTim();
@@ -130,20 +130,6 @@ public:
}
/**
- * Rewrites a node in the theory of uninterpreted functions.
- * This is fairly basic and only ensures that atoms that are
- * unsatisfiable or a valid are rewritten to false or true respectively.
- */
- Node rewrite(TNode n);
-
- /**
- * Plug in old rewrite to the new (pre,post)rewrite interface.
- */
- RewriteResponse postRewrite(TNode n, bool topLevel) {
- return RewriteComplete(topLevel ? rewrite(n) : Node(n));
- }
-
- /**
* Propagates theory literals. Currently does nothing.
*
* Overloads void propagate(Effort level); from theory.h.
@@ -157,7 +143,7 @@ public:
* Overloads void explain(TNode n, Effort level); from theory.h.
* See theory/theory.h for more information about this method.
*/
- void explain(TNode n, Effort level) {}
+ void explain(TNode n) {}
/**
* Get a theory value.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback