diff options
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/uf/kinds | 10 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 141 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 11 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 49 | ||||
-rw-r--r-- | src/theory/uf/tim/theory_uf_tim.cpp | 16 | ||||
-rw-r--r-- | src/theory/uf/tim/theory_uf_tim.h | 18 |
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. |