diff options
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/Makefile.am | 10 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.h | 2 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine_impl.h | 2 | ||||
| -rw-r--r-- | src/theory/uf/kinds | 5 | ||||
| -rw-r--r-- | src/theory/uf/morgan/Makefile | 4 | ||||
| -rw-r--r-- | src/theory/uf/morgan/Makefile.am | 16 | ||||
| -rw-r--r-- | src/theory/uf/morgan/stacking_map.cpp | 83 | ||||
| -rw-r--r-- | src/theory/uf/morgan/stacking_map.h | 91 | ||||
| -rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 751 | ||||
| -rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 267 | ||||
| -rw-r--r-- | src/theory/uf/morgan/union_find.cpp | 61 | ||||
| -rw-r--r-- | src/theory/uf/morgan/union_find.h | 148 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 4 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.h | 6 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 2 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 2 | ||||
| -rw-r--r-- | src/theory/uf/tim/Makefile | 4 | ||||
| -rw-r--r-- | src/theory/uf/tim/Makefile.am | 14 | ||||
| -rw-r--r-- | src/theory/uf/tim/ecdata.cpp | 105 | ||||
| -rw-r--r-- | src/theory/uf/tim/ecdata.h | 261 | ||||
| -rw-r--r-- | src/theory/uf/tim/theory_uf_tim.cpp | 325 | ||||
| -rw-r--r-- | src/theory/uf/tim/theory_uf_tim.h | 225 |
22 files changed, 13 insertions, 2375 deletions
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index fc0f32927..f25e50ec9 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -5,10 +5,6 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libuf.la -# force automake to link using g++ -nodist_EXTRA_libuf_la_SOURCES = \ - dummy.cpp - libuf_la_SOURCES = \ theory_uf.h \ theory_uf.cpp \ @@ -19,10 +15,4 @@ libuf_la_SOURCES = \ symmetry_breaker.h \ symmetry_breaker.cpp -libuf_la_LIBADD = \ - @builddir@/tim/libuftim.la \ - @builddir@/morgan/libufmorgan.la - -SUBDIRS = tim morgan - EXTRA_DIST = kinds diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 4f3879560..ba607526f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h index 1dd9963f7..bea6ff9a9 100644 --- a/src/theory/uf/equality_engine_impl.h +++ b/src/theory/uf/equality_engine_impl.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 6cec23385..1f8643330 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -5,11 +5,14 @@ # theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" +typechecker "theory/uf/theory_uf_type_rules.h" properties stable-infinite -properties check propagate staticLearning presolve notifyRestart +properties check propagate staticLearning presolve rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" +typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule + endtheory diff --git a/src/theory/uf/morgan/Makefile b/src/theory/uf/morgan/Makefile deleted file mode 100644 index 4f6767bdd..000000000 --- a/src/theory/uf/morgan/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../../.. -srcdir = src/theory/uf/morgan - -include $(topdir)/Makefile.subdir diff --git a/src/theory/uf/morgan/Makefile.am b/src/theory/uf/morgan/Makefile.am deleted file mode 100644 index 886178a6f..000000000 --- a/src/theory/uf/morgan/Makefile.am +++ /dev/null @@ -1,16 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libufmorgan.la - -libufmorgan_la_SOURCES = \ - theory_uf_morgan.h \ - theory_uf_morgan.cpp \ - union_find.h \ - union_find.cpp \ - stacking_map.h \ - stacking_map.cpp - -EXTRA_DIST = diff --git a/src/theory/uf/morgan/stacking_map.cpp b/src/theory/uf/morgan/stacking_map.cpp deleted file mode 100644 index 16a85e71b..000000000 --- a/src/theory/uf/morgan/stacking_map.cpp +++ /dev/null @@ -1,83 +0,0 @@ -/********************* */ -/*! \file stacking_map.cpp - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Backtrackable map using an undo stack - ** - ** Backtrackable map using an undo stack rather than storing items in - ** a CDMap<>. - **/ - -#include <iostream> - -#include "theory/uf/morgan/stacking_map.h" -#include "util/Assert.h" -#include "expr/node.h" - -using namespace std; - -namespace CVC4 { -namespace theory { -namespace uf { -namespace morgan { - -template <class NodeType, class NodeHash> -TNode StackingMap<NodeType, NodeHash>::find(TNode n) const { - typename MapType::const_iterator i = d_map.find(n); - if(i == d_map.end()) { - return TNode(); - } else { - return (*i).second; - } -} - -template <class NodeType, class NodeHash> -void StackingMap<NodeType, NodeHash>::set(TNode n, TNode newValue) { - Trace("ufsm") << "UFSM setting " << n << " : " << newValue << " @ " << d_trace.size() << endl; - NodeType& ref = d_map[n]; - d_trace.push_back(make_pair(n, TNode(ref))); - d_offset = d_trace.size(); - ref = newValue; -} - -template <class NodeType, class NodeHash> -void StackingMap<NodeType, NodeHash>::notify() { - Trace("ufsm") << "UFSM cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; - while(d_offset < d_trace.size()) { - pair<TNode, TNode> p = d_trace.back(); - if(p.second.isNull()) { - d_map.erase(p.first); - Trace("ufsm") << "UFSM " << d_trace.size() << " erasing " << p.first << endl; - } else { - d_map[p.first] = p.second; - Trace("ufsm") << "UFSM " << d_trace.size() << " replacing " << p << endl; - } - d_trace.pop_back(); - } - Trace("ufufsm") << "UFSM cancelling finished." << endl; -} - -// The following declarations allow us to put functions in the .cpp file -// instead of the header, since we know which instantiations are needed. - -template TNode StackingMap<Node, NodeHashFunction>::find(TNode n) const; -template void StackingMap<Node, NodeHashFunction>::set(TNode n, TNode newValue); -template void StackingMap<Node, NodeHashFunction>::notify(); - -template TNode StackingMap<TNode, TNodeHashFunction>::find(TNode n) const; -template void StackingMap<TNode, TNodeHashFunction>::set(TNode n, TNode newValue); -template void StackingMap<TNode, TNodeHashFunction>::notify(); - -}/* CVC4::theory::uf::morgan namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/theory/uf/morgan/stacking_map.h b/src/theory/uf/morgan/stacking_map.h deleted file mode 100644 index c54acc363..000000000 --- a/src/theory/uf/morgan/stacking_map.h +++ /dev/null @@ -1,91 +0,0 @@ -/********************* */ -/*! \file stacking_map.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Backtrackable map using an undo stack - ** - ** Backtrackable map using an undo stack rather than storing items in - ** a CDMap<>. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__UF__MORGAN__STACKING_MAP_H -#define __CVC4__THEORY__UF__MORGAN__STACKING_MAP_H - -#include <utility> -#include <vector> -#include <ext/hash_map> - -#include "expr/node.h" -#include "context/cdo.h" - -namespace CVC4 { - -namespace context { - class Context; -}/* CVC4::context namespace */ - -namespace theory { -namespace uf { -namespace morgan { - -// NodeType \in { Node, TNode } -template <class NodeType, class NodeHash> -class StackingMap : context::ContextNotifyObj { - /** Our underlying map type. */ - typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType; - - /** - * Our map of Nodes to their values. - */ - MapType d_map; - - /** Our undo stack for changes made to d_map. */ - std::vector<std::pair<TNode, TNode> > d_trace; - - /** Our current offset in the d_trace stack (context-dependent). */ - context::CDO<size_t> d_offset; - -public: - StackingMap(context::Context* ctxt) : - context::ContextNotifyObj(ctxt), - d_offset(ctxt, 0) { - } - - ~StackingMap() throw() { } - - /** - * Return a Node's value in the key-value map. If n is not a key in - * the map, this function returns TNode::null(). - */ - TNode find(TNode n) const; - - /** - * Set the value in the key-value map for Node n to newValue. - */ - void set(TNode n, TNode newValue); - - /** - * Called by the Context when a pop occurs. Cancels everything to the - * current context level. Overrides ContextNotifyObj::notify(). - */ - void notify(); - -};/* class StackingMap<> */ - -}/* CVC4::theory::uf::morgan namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /*__CVC4__THEORY__UF__MORGAN__STACKING_MAP_H */ diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp deleted file mode 100644 index 01bab53ac..000000000 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ /dev/null @@ -1,751 +0,0 @@ -/********************* */ -/*! \file theory_uf_morgan.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of the theory of uninterpreted functions. - ** - ** Implementation of the theory of uninterpreted functions. - **/ - -#include "theory/uf/morgan/theory_uf_morgan.h" -#include "theory/valuation.h" -#include "expr/kind.h" -#include "util/congruence_closure.h" -#include "theory/uf/symmetry_breaker.h" - -#include <map> - -using namespace std; - -using namespace CVC4; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; -using namespace CVC4::theory::uf::morgan; - -TheoryUFMorgan::TheoryUFMorgan(Context* ctxt, OutputChannel& out, Valuation valuation) : - TheoryUF(ctxt, out, valuation), - d_assertions(ctxt), - d_ccChannel(this), - d_cc(ctxt, &d_ccChannel), - d_unionFind(ctxt), - d_disequalities(ctxt), - d_equalities(ctxt), - d_conflict(), - d_trueNode(), - d_falseNode(), - d_trueEqFalseNode(), - d_ccExplanationLength("theory::uf::morgan::cc::averageExplanationLength", - d_cc.getExplanationLength()), - d_ccNewSkolemVars("theory::uf::morgan::cc::newSkolemVariables", - d_cc.getNewSkolemVars()) { - - StatisticsRegistry::registerStat(&d_ccExplanationLength); - StatisticsRegistry::registerStat(&d_ccNewSkolemVars); - - NodeManager* nm = NodeManager::currentNM(); - TypeNode boolType = nm->booleanType(); - d_trueNode = nm->mkVar("TRUE_UF", boolType); - d_falseNode = nm->mkVar("FALSE_UF", boolType); - d_trueEqFalseNode = nm->mkNode(kind::IFF, d_trueNode, d_falseNode); - addDisequality(d_trueEqFalseNode); - d_cc.addTerm(d_trueNode); - d_cc.addTerm(d_falseNode); -} - -TheoryUFMorgan::~TheoryUFMorgan() { - d_trueNode = Node::null(); - d_falseNode = Node::null(); - d_trueEqFalseNode = Node::null(); - - StatisticsRegistry::unregisterStat(&d_ccExplanationLength); - StatisticsRegistry::unregisterStat(&d_ccNewSkolemVars); -} - -void TheoryUFMorgan::preRegisterTerm(TNode n) { - Debug("uf") << "uf: preRegisterTerm(" << n << ")" << endl; - if(n.getKind() == kind::EQUAL || n.getKind() == kind::IFF) { - registerEqualityForPropagation(n); - } -} - -void TheoryUFMorgan::registerTerm(TNode n) { - Debug("uf") << "uf: registerTerm(" << n << ")" << endl; -} - -Node TheoryUFMorgan::constructConflict(TNode diseq) { - Debug("uf") << "uf: begin constructConflict()" << endl; - Debug("uf") << "uf: using diseq == " << diseq << endl; - - Node explanation = d_cc.explain(diseq[0], diseq[1]); - - NodeBuilder<> nb(kind::AND); - if(explanation.getKind() == kind::AND) { - for(TNode::iterator i = TNode(explanation).begin(); - i != TNode(explanation).end(); - ++i) { - TNode n = *i; - Assert(n.getKind() == kind::EQUAL || - n.getKind() == kind::IFF); - Assert(n[0] != d_trueNode && - n[0] != d_falseNode); - if(n[1] == d_trueNode) { - nb << n[0]; - } else if(n[1] == d_falseNode) { - nb << n[0].notNode(); - } else { - nb << n; - } - } - } else { - Assert(explanation.getKind() == kind::EQUAL || - explanation.getKind() == kind::IFF); - Assert(explanation[0] != d_trueNode && - explanation[0] != d_falseNode); - if(explanation[1] == d_trueNode) { - nb << explanation[0]; - } else if(explanation[1] == d_falseNode) { - nb << explanation[0].notNode(); - } else { - nb << explanation; - } - } - if(diseq != d_trueEqFalseNode) { - nb << diseq.notNode(); - } - - // by construction this should be true - Assert(nb.getNumChildren() > 1); - - Node conflict = nb; - Debug("uf") << "conflict constructed : " << conflict << endl; - - Debug("uf") << "uf: ending constructConflict()" << endl; - - return conflict; -} - -void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) { - Debug("uf") << "uf: notified of merge " << a << endl - << " and " << b << endl; - if(!d_conflict.isNull()) { - // if already a conflict, we don't care - return; - } - - merge(a, b); -} - -void TheoryUFMorgan::merge(TNode a, TNode b) { - Assert(d_conflict.isNull()); - - // make "a" the one with shorter diseqList - EqLists::iterator deq_ia = d_disequalities.find(a); - EqLists::iterator deq_ib = d_disequalities.find(b); - if(deq_ia != d_disequalities.end()) { - if(deq_ib == d_disequalities.end() || - (*deq_ia).second->size() > (*deq_ib).second->size()) { - TNode tmp = a; - a = b; - b = tmp; - Debug("uf") << " swapping to make a shorter diseqList" << endl; - } - } - a = find(a); - b = find(b); - Debug("uf") << "uf: uf reps are " << a << endl - << " and " << b << endl; - - if(a == b) { - return; - } - - // should have already found such a conflict - Assert(find(d_trueNode) != find(d_falseNode)); - - d_unionFind.setCanon(a, b); - - EqLists::iterator deq_i = d_disequalities.find(a); - // a set of other trees we are already disequal to, and their - // (TNode) equalities (for optimizations below) - map<TNode, TNode> alreadyDiseqs; - if(deq_i != d_disequalities.end()) { - EqLists::iterator deq_ib = d_disequalities.find(b); - if(deq_ib != d_disequalities.end()) { - EqList* deq = (*deq_ib).second; - for(EqList::const_iterator j = deq->begin(); j != deq->end(); ++j) { - TNode deqn = *j; - TNode s = deqn[0]; - TNode t = deqn[1]; - TNode sp = find(s); - TNode tp = find(t); - Assert(sp == b || tp == b); - if(sp == b) { - alreadyDiseqs[tp] = deqn; - } else { - alreadyDiseqs[sp] = deqn; - } - } - } - - EqList* deq = (*deq_i).second; - if(Debug.isOn("uf")) { - Debug("uf") << "a == " << a << endl; - Debug("uf") << "size of deq(a) is " << deq->size() << endl; - } - for(EqList::const_iterator j = deq->begin(); j != deq->end(); ++j) { - Debug("uf") << " deq(a) ==> " << *j << endl; - TNode deqn = *j; - Assert(deqn.getKind() == kind::EQUAL || - deqn.getKind() == kind::IFF); - TNode s = deqn[0]; - TNode t = deqn[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) { - d_conflict = deqn; - return; - } - Assert(sp == b || tp == b); - // optimization: don't put redundant diseq's in the list - if(sp == b) { - if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) { - appendToDiseqList(b, deqn); - alreadyDiseqs[tp] = deqn; - } - } else { - if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) { - appendToDiseqList(b, deqn); - alreadyDiseqs[sp] = deqn; - } - } - } - Debug("uf") << "end diseq-list." << endl; - } - - // Note that at this point, alreadyDiseqs contains everything we're - // 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; -// } -} - -void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) { - Debug("uf") << "appending " << eq << endl - << " to diseq list of " << of << endl; - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - Assert(of == debugFind(of)); - EqLists::iterator deq_i = d_disequalities.find(of); - EqList* deq; - if(deq_i == d_disequalities.end()) { - deq = new(getContext()->getCMM()) EqList(true, getContext(), false, - ContextMemoryAllocator<TNode>(getContext()->getCMM())); - d_disequalities.insertDataFromContextMemory(of, deq); - } else { - deq = (*deq_i).second; - } - deq->push_back(eq); - if(Debug.isOn("uf")) { - Debug("uf") << " size is now " << deq->size() << endl; - } -} - -void TheoryUFMorgan::appendToEqList(TNode of, TNode eq) { - Debug("uf") << "appending " << eq << endl - << " to eq list of " << of << endl; - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - Assert(of == debugFind(of)); - EqLists::iterator eq_i = d_equalities.find(of); - EqList* eql; - if(eq_i == d_equalities.end()) { - eql = new(getContext()->getCMM()) EqList(true, getContext(), false, - ContextMemoryAllocator<TNode>(getContext()->getCMM())); - d_equalities.insertDataFromContextMemory(of, eql); - } else { - eql = (*eq_i).second; - } - eql->push_back(eq); - if(Debug.isOn("uf")) { - Debug("uf") << " size is now " << eql->size() << endl; - } -} - -void TheoryUFMorgan::addDisequality(TNode eq) { - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - - TNode a = eq[0]; - TNode b = eq[1]; - - appendToDiseqList(find(a), eq); - appendToDiseqList(find(b), eq); -} - -void TheoryUFMorgan::registerEqualityForPropagation(TNode eq) { - // should NOT be in search at this point, this must be called during - // preregistration - - // FIXME with lemmas on demand, this could miss future propagations, - // since we are not necessarily at context level 0, but are updating - // context-sensitive structures. - - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - - TNode a = eq[0]; - TNode b = eq[1]; - - appendToEqList(find(a), eq); - appendToEqList(find(b), eq); -} - -void TheoryUFMorgan::check(Effort level) { - TimerStat::CodeTimer codeTimer(d_checkTimer); - - Debug("uf") << "uf: begin check(" << level << ")" << endl; - - while(!done()) { - Assert(d_conflict.isNull()); - - Node assertion = get(); - - //d_activeAssertions.push_back(assertion); - - Debug("uf") << "uf check(): " << assertion << endl; - - switch(assertion.getKind()) { - case kind::EQUAL: - case kind::IFF: - d_cc.addEquality(assertion); - if(!d_conflict.isNull()) { - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - ++d_conflicts; - d_out->conflict(conflict, false); - return; - } - merge(assertion[0], assertion[1]); - break; - case kind::APPLY_UF: - { // predicate - - // assert it's a predicate - Assert(assertion.getOperator().getType().getRangeType().isBoolean()); - - Node eq = NodeManager::currentNM()->mkNode(kind::IFF, - assertion, d_trueNode); - d_cc.addTerm(assertion); - d_cc.addEquality(eq); - - if(!d_conflict.isNull()) { - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - ++d_conflicts; - d_out->conflict(conflict, false); - return; - } - - if(Debug.isOn("uf")) { - Debug("uf") << "true == false ? " - << (find(d_trueNode) == find(d_falseNode)) << endl; - } - - Assert(find(d_trueNode) != find(d_falseNode)); - - merge(eq[0], eq[1]); - } - break; - case kind::NOT: - if(assertion[0].getKind() == kind::EQUAL || - assertion[0].getKind() == kind::IFF) { - Node a = assertion[0][0]; - Node b = assertion[0][1]; - - addDisequality(assertion[0]); - - d_cc.addTerm(a); - d_cc.addTerm(b); - - if(Debug.isOn("uf")) { - Debug("uf") << " a ==> " << a << endl - << " b ==> " << b << endl - << " find(a) ==> " << debugFind(a) << endl - << " find(b) ==> " << debugFind(b) << endl; - } - - // There are two ways to get a conflict here. - if(!d_conflict.isNull()) { - // We get a conflict this way if we weren't watching a, b - // before and we were just now notified (via - // notifyCongruent()) when we called addTerm() above that - // they are congruent. We make this a separate case (even - // though the check in the "else if.." below would also - // catch it, so that we can clear out d_conflict. - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - ++d_conflicts; - d_out->conflict(conflict, false); - return; - } else if(find(a) == find(b)) { - // We get a conflict this way if we WERE previously watching - // a, b and were notified previously (via notifyCongruent()) - // that they were congruent. - Node conflict = constructConflict(assertion[0]); - ++d_conflicts; - d_out->conflict(conflict, false); - return; - } - - // If we get this far, there should be nothing conflicting due - // to this disequality. - Assert(!d_cc.areCongruent(a, b)); - } else { - // negation of a predicate - Assert(assertion[0].getKind() == kind::APPLY_UF); - - // assert it's a predicate - Assert(assertion[0].getOperator().getType().getRangeType().isBoolean()); - - Node eq = NodeManager::currentNM()->mkNode(kind::IFF, - assertion[0], d_falseNode); - d_cc.addTerm(assertion[0]); - d_cc.addEquality(eq); - - if(!d_conflict.isNull()) { - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - ++d_conflicts; - d_out->conflict(conflict, false); - return; - } - - if(Debug.isOn("uf")) { - Debug("uf") << "true == false ? " - << (find(d_trueNode) == find(d_falseNode)) << endl; - } - - Assert(find(d_trueNode) != find(d_falseNode)); - - merge(eq[0], eq[1]); - } - break; - default: - Unhandled(assertion.getKind()); - } - - /* - if(Debug.isOn("uf")) { - dump(); - } - */ - } - Assert(d_conflict.isNull()); - Debug("uf") << "uf check() done = " << (done() ? "true" : "false") - << endl; - - /* - for(CDList<Node>::const_iterator diseqIter = d_disequality.begin(); - diseqIter != d_disequality.end(); - ++diseqIter) { - - TNode left = (*diseqIter)[0]; - TNode right = (*diseqIter)[1]; - if(Debug.isOn("uf")) { - Debug("uf") << "testing left: " << left << endl - << " right: " << right << endl - << " find(L): " << debugFind(left) << endl - << " find(R): " << debugFind(right) << endl - << " areCong: " << d_cc.areCongruent(left, right) - << endl; - } - Assert((debugFind(left) == debugFind(right)) == - d_cc.areCongruent(left, right)); - } - */ - - Debug("uf") << "uf: end check(" << level << ")" << endl; -} - -void TheoryUFMorgan::propagate(Effort level) { - TimerStat::CodeTimer codeTimer(d_propagateTimer); - - Debug("uf") << "uf: begin propagate(" << level << ")" << endl; - // propagation is done in check(), for now - // FIXME need to find a slick way to propagate predicates - Debug("uf") << "uf: end propagate(" << level << ")" << endl; -} - -void TheoryUFMorgan::explain(TNode n) { - TimerStat::CodeTimer codeTimer(d_explainTimer); - - Debug("uf") << "uf: begin explain([" << n << "])" << endl; - Unimplemented(); - Debug("uf") << "uf: end explain([" << n << "])" << endl; -} - -void TheoryUFMorgan::presolve() { - TimerStat::CodeTimer codeTimer(d_presolveTimer); - - Debug("uf") << "uf: begin presolve()" << endl; - if(Options::current()->ufSymmetryBreaker) { - vector<Node> newClauses; - d_symb.apply(newClauses); - for(vector<Node>::const_iterator i = newClauses.begin(); - i != newClauses.end(); - ++i) { - d_out->lemma(*i); - } - } - Debug("uf") << "uf: end presolve()" << endl; -} - -void TheoryUFMorgan::notifyRestart() { - Debug("uf") << "uf: begin notifyDecisionLevelZero()" << endl; - Debug("uf") << "uf: end notifyDecisionLevelZero()" << endl; -} - -Node TheoryUFMorgan::getValue(TNode n) { - NodeManager* nodeManager = NodeManager::currentNM(); - - switch(n.getKind()) { - - case kind::VARIABLE: - case kind::APPLY_UF: - if(n.getType().isBoolean()) { - if(d_cc.areCongruent(d_trueNode, n)) { - return nodeManager->mkConst(true); - } else if(d_cc.areCongruent(d_falseNode, n)) { - return nodeManager->mkConst(false); - } - } - return d_cc.normalize(n); - - case kind::EQUAL: // 2 args - return nodeManager-> - mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); - - default: - Unhandled(n.getKind()); - } -} - -void TheoryUFMorgan::staticLearning(TNode n, NodeBuilder<>& learned) { - TimerStat::CodeTimer codeTimer(d_staticLearningTimer); - - vector<TNode> workList; - workList.push_back(n); - __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed; - - while(!workList.empty()) { - n = workList.back(); - - bool unprocessedChildren = false; - for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { - if(processed.find(*i) == processed.end()) { - // unprocessed child - workList.push_back(*i); - unprocessedChildren = true; - } - } - - if(unprocessedChildren) { - continue; - } - - workList.pop_back(); - // has node n been processed in the meantime ? - if(processed.find(n) != processed.end()) { - continue; - } - processed.insert(n); - - // == DIAMONDS == - - Debug("diamonds") << "===================== looking at" << endl - << n << endl; - - // binary OR of binary ANDs of EQUALities - if(n.getKind() == kind::OR && n.getNumChildren() == 2 && - n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 && - n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 && - (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) && - (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) && - (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) && - (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) { - // now we have (a = b && c = d) || (e = f && g = h) - - Debug("diamonds") << "has form of a diamond!" << endl; - - TNode - a = n[0][0][0], b = n[0][0][1], - c = n[0][1][0], d = n[0][1][1], - e = n[1][0][0], f = n[1][0][1], - g = n[1][1][0], h = n[1][1][1]; - - // test that one of {a, b} = one of {c, d}, and make "b" the - // shared node (i.e. put in the form (a = b && b = d)) - // note we don't actually care about the shared ones, so the - // "swaps" below are one-sided, ignoring b and c - if(a == c) { - a = b; - } else if(a == d) { - a = b; - d = c; - } else if(b == c) { - // nothing to do - } else if(b == d) { - d = c; - } else { - // condition not satisfied - Debug("diamonds") << "+ A fails" << endl; - continue; - } - - Debug("diamonds") << "+ A holds" << endl; - - // same: one of {e, f} = one of {g, h}, and make "f" the - // shared node (i.e. put in the form (e = f && f = h)) - if(e == g) { - e = f; - } else if(e == h) { - e = f; - h = g; - } else if(f == g) { - // nothing to do - } else if(f == h) { - h = g; - } else { - // condition not satisfied - Debug("diamonds") << "+ B fails" << endl; - continue; - } - - Debug("diamonds") << "+ B holds" << endl; - - // now we have (a = b && b = d) || (e = f && f = h) - // test that {a, d} == {e, h} - if( (a == e && d == h) || - (a == h && d == e) ) { - // learn: n implies a == d - Debug("diamonds") << "+ C holds" << endl; - Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d); - Debug("diamonds") << " ==> " << newEquality << endl; - learned << n.impNode(newEquality); - } else { - Debug("diamonds") << "+ C fails" << endl; - } - } - } - - if(Options::current()->ufSymmetryBreaker) { - d_symb.assertFormula(n); - } -} - -/* -void TheoryUFMorgan::dump() { - if(!Debug.isOn("uf")) { - return; - } - Debug("uf") << "============== THEORY_UF ==============" << endl; - Debug("uf") << "Active assertions list:" << endl; - for(context::CDList<Node>::const_iterator i = d_activeAssertions.begin(); - i != d_activeAssertions.end(); - ++i) { - Debug("uf") << " " << *i << endl; - } - Debug("uf") << "Congruence union-find:" << endl; - for(UnionFind::const_iterator i = d_unionFind.begin(); - i != d_unionFind.end(); - ++i) { - Debug("uf") << " " << (*i).first << " ==> " << (*i).second - << endl; - } - Debug("uf") << "Disequality lists:" << endl; - for(EqLists::const_iterator i = d_disequalities.begin(); - i != d_disequalities.end(); - ++i) { - Debug("uf") << " " << (*i).first << ":" << endl; - EqList* dl = (*i).second; - for(EqList::const_iterator j = dl->begin(); - j != dl->end(); - ++j) { - Debug("uf") << " " << *j << endl; - } - } - Debug("uf") << "=======================================" << endl; -} -*/ diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h deleted file mode 100644 index e801f383e..000000000 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ /dev/null @@ -1,267 +0,0 @@ -/********************* */ -/*! \file theory_uf_morgan.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of the theory of uninterpreted functions with - ** equality - ** - ** Implementation of the theory of uninterpreted functions with equality, - ** based on CVC4's congruence closure module (which is in turn based on - ** the Nieuwenhuis and Oliveras paper, Fast Congruence Closure and - ** Extensions. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H -#define __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H - -#include "expr/node.h" -#include "expr/attribute.h" - -#include "theory/theory.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/morgan/union_find.h" -#include "theory/uf/symmetry_breaker.h" - -#include "context/context.h" -#include "context/context_mm.h" -#include "context/cdlist.h" -#include "util/congruence_closure.h" - -namespace CVC4 { -namespace theory { -namespace uf { -namespace morgan { - -class TheoryUFMorgan : public TheoryUF { - -private: - - class CongruenceChannel { - TheoryUFMorgan* d_uf; - - public: - CongruenceChannel(TheoryUFMorgan* uf) : d_uf(uf) {} - void notifyCongruent(TNode a, TNode b) { - d_uf->notifyCongruent(a, b); - } - };/* class CongruenceChannel */ - friend class CongruenceChannel; - - /** - * List of all of the non-negated literals from the assertion queue. - * This is used only for conflict generation. - * This differs from pending as the program generates new equalities that - * are not in this list. - * This will probably be phased out in future version. - */ - context::CDList<Node> d_assertions; - - SymmetryBreaker d_symb; - - /** - * Our channel connected to the congruence closure module. - */ - CongruenceChannel d_ccChannel; - - /** - * Instance of the congruence closure module. - */ - CongruenceClosure<CongruenceChannel, CongruenceOperator<kind::APPLY_UF> > d_cc; - - /** - * Our union find for equalities. - */ - UnionFind<TNode, TNodeHashFunction> d_unionFind; - - typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > EqList; - typedef context::CDMap<Node, EqList*, NodeHashFunction> EqLists; - - /** List of all disequalities this theory has seen. */ - EqLists d_disequalities; - - /** List of all (potential) equalities to be propagated. */ - EqLists d_equalities; - - Node d_conflict; - - Node d_trueNode, d_falseNode, d_trueEqFalseNode; - - // === STATISTICS === - /** time spent in check() */ - KEEP_STATISTIC(TimerStat, - d_checkTimer, - "theory::uf::morgan::checkTime"); - /** time spent in propagate() */ - KEEP_STATISTIC(TimerStat, - d_propagateTimer, - "theory::uf::morgan::propagateTime"); - - /** time spent in explain() */ - KEEP_STATISTIC(TimerStat, - d_explainTimer, - "theory::uf::morgan::explainTime"); - /** time spent in staticLearning() */ - KEEP_STATISTIC(TimerStat, - d_staticLearningTimer, - "theory::uf::morgan::staticLearningTime"); - /** time spent in presolve() */ - KEEP_STATISTIC(TimerStat, - d_presolveTimer, - "theory::uf::morgan::presolveTime"); - /** number of UF conflicts */ - KEEP_STATISTIC(IntStat, - d_conflicts, - "theory::uf::morgan::conflicts", 0); - /** number of UF propagations */ - KEEP_STATISTIC(IntStat, - d_propagations, - "theory::uf::morgan::propagations", 0); - /** CC module expl length */ - WrappedStat<AverageStat> d_ccExplanationLength; - /** CC module # skolem vars */ - WrappedStat<IntStat> d_ccNewSkolemVars; - -public: - - /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFMorgan(context::Context* ctxt, OutputChannel& out, Valuation valuation); - - /** Destructor for UF theory, cleans up memory and statistics. */ - ~TheoryUFMorgan(); - - /** - * Registers a previously unseen [in this context] node n. - * For TheoryUF, this sets up and maintains invaraints about - * equivalence class data-structures. - * - * Overloads a void registerTerm(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - void registerTerm(TNode n); - - /** - * Currently this does nothing. - * - * Overloads a void preRegisterTerm(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - void preRegisterTerm(TNode n); - - /** - * Checks whether the set of literals provided to the theory is consistent. - * - * If this is called at any effort level, it computes the congruence closure - * of all of the positive literals in the context. - * - * If this is called at full effort it checks if any of the negative literals - * are inconsistent with the congruence closure. - * - * Overloads void check(Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void check(Effort level); - - /** - * Propagates theory literals. - * - * Overloads void propagate(Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void propagate(Effort level); - - /** - * Explains a previously theory-propagated literal. - * - * Overloads void explain(TNode n, Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void explain(TNode n); - - /** - * The theory should only add (via .operator<< or .append()) to the - * "learned" builder. It is a conjunction to add to the formula at - * the top-level and may contain other theories' contributions. - */ - void staticLearning(TNode in, NodeBuilder<>& learned); - - /** - * A Theory is called with presolve exactly one time per user - * check-sat. presolve() is called after preregistration, - * rewriting, and Boolean propagation, (other theories' - * propagation?), but the notified Theory has not yet had its - * check() or propagate() method called. A Theory may empty its - * assertFact() queue using get(). A Theory can raise conflicts, - * add lemmas, and propagate literals during presolve(). - */ - void presolve(); - - /** - * Notification sent to the Theory when the search restarts. - */ - void notifyRestart(); - - /** - * Gets a theory value. - * - * Overloads Node getValue(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - Node getValue(TNode n); - - std::string identify() const { return std::string("TheoryUFMorgan"); } - -private: - - /** Constructs a conflict from an inconsistent disequality. */ - Node constructConflict(TNode diseq); - - inline TNode find(TNode a); - inline TNode debugFind(TNode a) const; - - void appendToDiseqList(TNode of, TNode eq); - void appendToEqList(TNode of, TNode eq); - void addDisequality(TNode eq); - void registerEqualityForPropagation(TNode eq); - - /** - * Receives a notification from the congruence closure module that - * two nodes have been merged into the same congruence class. - */ - void notifyCongruent(TNode a, TNode b); - - /** - * Internally handle a congruence, whether generated by the CC - * module or from a theory check(). Merges the classes from a and b - * and looks for a conflict. If there is one, sets d_conflict. - */ - void merge(TNode a, TNode b); - - void dump(); - -};/* class TheoryUFMorgan */ - -inline TNode TheoryUFMorgan::find(TNode a) { - return d_unionFind.find(a); -} - -inline TNode TheoryUFMorgan::debugFind(TNode a) const { - return d_unionFind.debugFind(a); -} - -}/* CVC4::theory::uf::morgan namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H */ diff --git a/src/theory/uf/morgan/union_find.cpp b/src/theory/uf/morgan/union_find.cpp deleted file mode 100644 index 135320707..000000000 --- a/src/theory/uf/morgan/union_find.cpp +++ /dev/null @@ -1,61 +0,0 @@ -/********************* */ -/*! \file union_find.cpp - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Path-compressing, backtrackable union-find using an undo - ** stack - ** - ** Path-compressing, backtrackable union-find using an undo stack - ** rather than storing items in a CDMap<>. - **/ - -#include <iostream> - -#include "theory/uf/morgan/union_find.h" -#include "util/Assert.h" -#include "expr/node.h" - -using namespace std; - -namespace CVC4 { -namespace theory { -namespace uf { -namespace morgan { - -template <class NodeType, class NodeHash> -void UnionFind<NodeType, NodeHash>::notify() { - Trace("ufuf") << "UFUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; - while(d_offset < d_trace.size()) { - pair<TNode, TNode> p = d_trace.back(); - if(p.second.isNull()) { - d_map.erase(p.first); - Trace("ufuf") << "UFUF " << d_trace.size() << " erasing " << p.first << endl; - } else { - d_map[p.first] = p.second; - Trace("ufuf") << "UFUF " << d_trace.size() << " replacing " << p << endl; - } - d_trace.pop_back(); - } - Trace("ufuf") << "UFUF cancelling finished." << endl; -} - -// The following declarations allow us to put functions in the .cpp file -// instead of the header, since we know which instantiations are needed. - -template void UnionFind<Node, NodeHashFunction>::notify(); - -template void UnionFind<TNode, TNodeHashFunction>::notify(); - -}/* CVC4::theory::uf::morgan namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/theory/uf/morgan/union_find.h b/src/theory/uf/morgan/union_find.h deleted file mode 100644 index 794d7452c..000000000 --- a/src/theory/uf/morgan/union_find.h +++ /dev/null @@ -1,148 +0,0 @@ -/********************* */ -/*! \file union_find.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Path-compressing, backtrackable union-find using an undo - ** stack - ** - ** Path-compressing, backtrackable union-find using an undo stack - ** rather than storing items in a CDMap<>. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__UF__MORGAN__UNION_FIND_H -#define __CVC4__THEORY__UF__MORGAN__UNION_FIND_H - -#include <utility> -#include <vector> -#include <ext/hash_map> - -#include "expr/node.h" -#include "context/cdo.h" - -namespace CVC4 { - -namespace context { - class Context; -}/* CVC4::context namespace */ - -namespace theory { -namespace uf { -namespace morgan { - -// NodeType \in { Node, TNode } -template <class NodeType, class NodeHash> -class UnionFind : context::ContextNotifyObj { - /** Our underlying map type. */ - typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType; - - /** - * Our map of Nodes to their canonical representatives. - * If a Node is not present in the map, it is its own - * representative. - */ - MapType d_map; - - /** Our undo stack for changes made to d_map. */ - std::vector<std::pair<TNode, TNode> > d_trace; - - /** Our current offset in the d_trace stack (context-dependent). */ - context::CDO<size_t> d_offset; - -public: - UnionFind(context::Context* ctxt) : - context::ContextNotifyObj(ctxt), - d_offset(ctxt, 0) { - } - - ~UnionFind() throw() { } - - /** - * Return a Node's union-find representative, doing path compression. - */ - inline TNode find(TNode n); - - /** - * Return a Node's union-find representative, NOT doing path compression. - * This is useful for Assert() statements, debug checking, and similar - * things that you do NOT want to mutate the structure. - */ - inline TNode debugFind(TNode n) const; - - /** - * Set the canonical representative of n to newParent. They should BOTH - * be their own canonical representatives on entry to this funciton. - */ - inline void setCanon(TNode n, TNode newParent); - - /** - * Called by the Context when a pop occurs. Cancels everything to the - * current context level. Overrides ContextNotifyObj::notify(). - */ - void notify(); - -};/* class UnionFind<> */ - -template <class NodeType, class NodeHash> -inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const { - typename MapType::const_iterator i = d_map.find(n); - if(i == d_map.end()) { - return n; - } else { - return debugFind((*i).second); - } -} - -template <class NodeType, class NodeHash> -inline TNode UnionFind<NodeType, NodeHash>::find(TNode n) { - Trace("ufuf") << "UFUF find of " << n << std::endl; - typename MapType::iterator i = d_map.find(n); - if(i == d_map.end()) { - Trace("ufuf") << "UFUF it is rep" << std::endl; - return n; - } else { - Trace("ufuf") << "UFUF not rep: par is " << (*i).second << std::endl; - std::pair<TNode, TNode> pr = *i; - // our iterator is invalidated by the recursive call to find(), - // since it mutates the map - TNode p = find(pr.second); - if(p == pr.second) { - return p; - } - d_trace.push_back(std::make_pair(n, pr.second)); - d_offset = d_trace.size(); - Trace("ufuf") << "UFUF setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl; - pr.second = p; - d_map.insert(pr); - return p; - } -} - -template <class NodeType, class NodeHash> -inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) { - Assert(d_map.find(n) == d_map.end()); - Assert(d_map.find(newParent) == d_map.end()); - if(n != newParent) { - Trace("ufuf") << "UFUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl; - d_map[n] = newParent; - d_trace.push_back(std::make_pair(n, TNode::null())); - d_offset = d_trace.size(); - } -} - -}/* CVC4::theory::uf::morgan namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /*__CVC4__THEORY__UF__MORGAN__UNION_FIND_H */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 3c8d59d08..401c18203 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -2,10 +2,10 @@ /*! \file theory_uf.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index de8e70a49..1f4c2372f 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf.h ** \verbatim - ** Original author: dejan - ** Major contributors: none + ** Original author: mdeters + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index ee88df126..e1aba2c95 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -2,7 +2,7 @@ /*! \file theory_uf_rewriter.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 7a4bf721f..927a31e01 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -5,7 +5,7 @@ ** Major contributors: cconway, mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/uf/tim/Makefile b/src/theory/uf/tim/Makefile deleted file mode 100644 index e1db2cbf9..000000000 --- a/src/theory/uf/tim/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../../.. -srcdir = src/theory/uf/tim - -include $(topdir)/Makefile.subdir diff --git a/src/theory/uf/tim/Makefile.am b/src/theory/uf/tim/Makefile.am deleted file mode 100644 index 647783885..000000000 --- a/src/theory/uf/tim/Makefile.am +++ /dev/null @@ -1,14 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libuftim.la - -libuftim_la_SOURCES = \ - ecdata.h \ - ecdata.cpp \ - theory_uf_tim.h \ - theory_uf_tim.cpp - -EXTRA_DIST = diff --git a/src/theory/uf/tim/ecdata.cpp b/src/theory/uf/tim/ecdata.cpp deleted file mode 100644 index 52a110ff2..000000000 --- a/src/theory/uf/tim/ecdata.cpp +++ /dev/null @@ -1,105 +0,0 @@ -/********************* */ -/*! \file ecdata.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of equivalence class data for UF theory. - ** - ** Implementation of equivalence class data for UF theory. This is a - ** context-dependent object. - **/ - -#include "theory/uf/tim/ecdata.h" - -using namespace CVC4; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; -using namespace CVC4::theory::uf::tim; - -ECData::ECData(Context * context, TNode n) : - ContextObj(context), - d_find(this), - d_rep(n), - d_watchListSize(0), - d_first(NULL), - d_last(NULL) { -} - -bool ECData::isClassRep() { - return this == this->d_find; -} - -void ECData::addPredecessor(TNode n) { - Assert(isClassRep()); - - makeCurrent(); - - Link * newPred = new(getCMM()) Link(getContext(), n, d_first); - d_first = newPred; - if(d_last == NULL) { - d_last = newPred; - } - - ++d_watchListSize; -} - -ContextObj* ECData::save(ContextMemoryManager* pCMM) { - return new(pCMM) ECData(*this); -} - -void ECData::restore(ContextObj* pContextObj) { - ECData* data = (ECData*)pContextObj; - d_find = data->d_find; - d_first = data->d_first; - d_last = data->d_last; - d_rep = data->d_rep; - d_watchListSize = data->d_watchListSize; -} - -Node ECData::getRep() { - return d_rep; -} - -unsigned ECData::getWatchListSize() { - return d_watchListSize; -} - -void ECData::setFind(ECData * ec) { - makeCurrent(); - d_find = ec; -} - -ECData* ECData::getFind() { - return d_find; -} - -Link* ECData::getFirst() { - return d_first; -} - -void ECData::takeOverDescendantWatchList(ECData* nslave, ECData* nmaster) { - Assert(nslave != nmaster); - Assert(nslave->getFind() == nmaster); - - nmaster->makeCurrent(); - - nmaster->d_watchListSize += nslave->d_watchListSize; - - if(nmaster->d_first == NULL) { - nmaster->d_first = nslave->d_first; - nmaster->d_last = nslave->d_last; - } else if(nslave->d_first != NULL) { - Link* currLast = nmaster->d_last; - currLast->d_next = nslave->d_first; - nmaster->d_last = nslave->d_last; - } -} diff --git a/src/theory/uf/tim/ecdata.h b/src/theory/uf/tim/ecdata.h deleted file mode 100644 index 5e72f0042..000000000 --- a/src/theory/uf/tim/ecdata.h +++ /dev/null @@ -1,261 +0,0 @@ -/********************* */ -/*! \file ecdata.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Context dependent equivalence class datastructure for nodes. - ** - ** Context dependent equivalence class datastructure for nodes. - ** Currently keeps a context dependent watch list. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__UF__TIM__ECDATA_H -#define __CVC4__THEORY__UF__TIM__ECDATA_H - -#include "expr/node.h" -#include "context/context.h" -#include "context/cdo.h" -#include "context/context_mm.h" - -namespace CVC4 { -namespace theory { -namespace uf { -namespace tim { - -/** - * Link is a context dependent linked list of nodes. - * Link is intended to be allocated in a Context's memory manager. - * The next pointer of the list is context dependent, but the node being - * pointed to is fixed for the life of the Link. - * - * Clients of Link are intended not to modify the node that is being pointed - * to in good faith. This may change in the future. - */ -struct Link { - /** - * Pointer to the next element in linked list. - * This is context dependent. - */ - context::CDO<Link*> d_next; - - /** - * Link is supposed to be allocated in a region of a - * ContextMemoryManager. In order to avoid having to decrement the - * ref count at deletion time, it is preferrable for the user of - * Link to maintain the invariant that data will survival for the - * entire scope of the TNode. - */ - TNode d_data; - - /** - * Creates a new Link w.r.t. a context for the node n. - * An optional parameter is to specify the next element in the link. - */ - Link(context::Context* context, TNode n, Link* l = NULL) : - d_next(true, context, l), - d_data(n) { - Debug("context") << "Link: " << this - << " so cdo is " << &d_next << std::endl; - } - - /** - * Allocates a new Link in the region for the provided ContextMemoryManager. - * This allows for cheap cleanup on pop. - */ - static void* operator new(size_t size, context::ContextMemoryManager* pCMM) { - return pCMM->newData(size); - } - -private: - - /** - * The destructor isn't actually defined. This declaration keeps - * the compiler from creating (wastefully) a default definition, and - * ensures that we get a link error if someone uses Link in a way - * that requires destruction. Objects of class Link should always - * be allocated in a ContextMemoryManager, which doesn't call - * destructors. - */ - ~Link() throw(); - - /** - * Just like the destructor, this is not defined. This ensures no - * one tries to create a Link on the heap. - */ - static void* operator new(size_t size); - -};/* struct Link */ - - -/** - * ECData is a equivalence class object that is context dependent. - * It is developed in order to support the congruence closure algorithm - * in TheoryUF, and is not intended to be used outside of that package. - * - * ECData maintains: - * - find pointer for the equivalence class (disjoint set forest) - * - the node that represents the equivalence class. - * - maintains a predecessorlist/watchlist - * - * ECData does not have support for the canonical find and union operators - * for disjoint set forests. Instead it only provides access to the find - * pointer. The implementation of find is ccFind in TheoryUF. - * union is broken into 2 phases: - * 1) setting the find point with setFind - * 2) taking over the watch list of the other node. - * This is a technical requirement for the implementation of TheoryUF. - * (See ccUnion in TheoryUF for more information.) - * - * The intended paradigm for iterating over the watch list of ec is: - * for(Link* i = ec->getFirst(); i != NULL; i = i->next ); - * - * See also ECAttr() in theory_uf.h, and theory_uf.cpp where the codde that uses - * ECData lives. - */ -class ECData : public context::ContextObj { -private: - /** - * This is the standard disjoint set forest find pointer. - * - * Why an ECData pointer instead of a node? - * This was chosen to be a ECData pointer in order to shortcut at least one - * table every time the find pointer is examined. - */ - ECData* d_find; - - /** - * This is pointer back to the node that represents this equivalence class. - * - * The following invariant should be maintained: - * (n.getAttribute(ECAttr()))->rep == n - * i.e. rep is equal to the node that maps to the ECData using ECAttr. - * - * Tricky part: This needs to be a TNode, not a Node. - * Suppose that rep were a hard link. - * When a node n maps to an ECData via the ECAttr() there will be a hard - * link back to n in the ECData. The attribute does not do garbage collection - * until the node gets garbage collected, which does not happen until its - * ref count drops to 0. So because of this cycle neither the node and - * the ECData will never get garbage collected. - * So this needs to be a soft link. - */ - TNode d_rep; - - // Watch list data structures follow - - /** - * Maintains watch list size for more efficient merging. - */ - unsigned d_watchListSize; - - /** - * Pointer to the beginning of the watchlist. - * This value is NULL iff the watch list is empty. - */ - Link* d_first; - - /** - * Pointer to the end of the watch-list. - * This is maintained in order to constant time list merging. - * (This does not give any asymptotic improve as this is currently always - * preceeded by an O(|watchlist|) operation.) - * This value is NULL iff the watch list is empty. - */ - Link* d_last; - - /** Context-dependent operation: save this ECData */ - context::ContextObj* save(context::ContextMemoryManager* pCMM); - - /** Context-dependent operation: restore this ECData */ - void restore(context::ContextObj* pContextObj); - -public: - /** - * Returns true if this ECData object is the current representative of - * the equivalence class. - */ - bool isClassRep(); - - /** - * Adds a node to the watch list of the equivalence class. Does - * context-dependent memory allocation in the Context with which - * this ECData was created. - * - * @param n the node to be added. - * @pre isClassRep() == true - */ - void addPredecessor(TNode n); - - /** - * Creates a EQ with the representative n - * @param context the context to associate with this ecdata. - * This is required as ECData is context dependent - * @param n the node that corresponds to this ECData - */ - ECData(context::Context* context, TNode n); - - /** Destructor for ECDatas */ - ~ECData() { - Debug("ufgc") << "Calling ECData destructor" << std::endl; - destroy(); - } - - /** - * An ECData takes over the watch list of another ECData. - * This is the second step in the union operator for ECData. - * This should be called after nslave->setFind(nmaster); - * After this is done nslave's watch list should never be accessed by - * getLast() or getFirst() - */ - static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster); - - /** - * Returns the representative of this ECData. - */ - Node getRep(); - - /** - * Returns the size of the equivalence class. - */ - unsigned getWatchListSize(); - - /** - * Returns a pointer the first member of the watch list. - */ - Link* getFirst(); - - - /** - * Returns the find pointer of the ECData. - * If isClassRep(), then getFind() == this - */ - ECData* getFind(); - - /** - * Sets the find pointer of the equivalence class to be another ECData object. - * - * @pre isClassRep() == true - * @pre ec->isClassRep() == true - * @post isClassRep() == false - * @post ec->isClassRep() == true - */ - void setFind(ECData * ec); - -};/* class ECData */ - -}/* CVC4::theory::uf::tim namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */ diff --git a/src/theory/uf/tim/theory_uf_tim.cpp b/src/theory/uf/tim/theory_uf_tim.cpp deleted file mode 100644 index ae37dfe99..000000000 --- a/src/theory/uf/tim/theory_uf_tim.cpp +++ /dev/null @@ -1,325 +0,0 @@ -/********************* */ -/*! \file theory_uf_tim.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of the theory of uninterpreted functions. - ** - ** Implementation of the theory of uninterpreted functions. - **/ - -#include "theory/uf/tim/theory_uf_tim.h" -#include "theory/uf/tim/ecdata.h" -#include "expr/kind.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; -using namespace CVC4::theory::uf::tim; - -TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out, Valuation valuation) : - TheoryUF(c, out, valuation), - d_assertions(c), - d_pending(c), - d_currentPendingIdx(c,0), - d_disequality(c), - d_registered(c) { - Warning() << "NOTE:" << std::endl - << "NOTE: currently the 'Tim' UF solver is broken," << std::endl - << "NOTE: since its registerTerm() function is never" << std::endl - << "NOTE: called." << std::endl - << "NOTE:" << std::endl; -} - -TheoryUFTim::~TheoryUFTim() { -} - -void TheoryUFTim::preRegisterTerm(TNode n) { - Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl; - Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl; -} - -void TheoryUFTim::registerTerm(TNode n) { - - Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl; - - d_registered.push_back(n); - - ECData* ecN; - - if(n.getAttribute(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 { - //The attribute does not exist, so it is created and set - ecN = new (true) ECData(getContext(), n); - n.setAttribute(ECAttr(), ecN); - } - - /* If the node is an APPLY_UF, we need to add it to the predecessor list - * of its children. - */ - if(n.getKind() == APPLY_UF) { - TNode::iterator cIter = n.begin(); - - for(; cIter != n.end(); ++cIter) { - TNode child = *cIter; - - /* Because this can be called after nodes have been merged, we need - * to lookup the representative in the UnionFind datastructure. - */ - ECData* ecChild = ccFind(child.getAttribute(ECAttr())); - - /* Because this can be called after nodes have been merged we may need - * to be merged with other predecessors of the equivalence class. - */ - for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ) { - if(equiv(n, Px->d_data)) { - Node pend = n.eqNode(Px->d_data); - d_pending.push_back(pend); - } - } - - ecChild->addPredecessor(n); - } - } - Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl; - -} - -bool TheoryUFTim::sameCongruenceClass(TNode x, TNode y) { - return - ccFind(x.getAttribute(ECAttr())) == - ccFind(y.getAttribute(ECAttr())); -} - -bool TheoryUFTim::equiv(TNode x, TNode y) { - Assert(x.getKind() == kind::APPLY_UF); - Assert(y.getKind() == kind::APPLY_UF); - - if(x.getNumChildren() != y.getNumChildren()) { - return false; - } - - if(x.getOperator() != y.getOperator()) { - return false; - } - - // intentionally don't look at operator - - TNode::iterator xIter = x.begin(); - TNode::iterator yIter = y.begin(); - - while(xIter != x.end()) { - - if(!sameCongruenceClass(*xIter, *yIter)) { - return false; - } - - ++xIter; - ++yIter; - } - return true; -} - -/* This is a very basic, but *obviously correct* find implementation - * of the classic find algorithm. - * TODO after we have done some more testing: - * 1) Add path compression. This is dependent on changes to ccUnion as - * many better algorithms use eager path compression. - * 2) Elminate recursion. - */ -ECData* TheoryUFTim::ccFind(ECData * x) { - if(x->getFind() == x) { - return x; - } else { - return ccFind(x->getFind()); - } - /* Slightly better Find w/ path compression and no recursion*/ - /* - ECData* start; - ECData* next = x; - while(x != x->getFind()) x=x->getRep(); - while( (start = next) != x) { - next = start->getFind(); - start->setFind(x); - } - return x; - */ -} - -void TheoryUFTim::ccUnion(ECData* ecX, ECData* ecY) { - ECData* nslave; - ECData* nmaster; - - if(ecX->getWatchListSize() <= ecY->getWatchListSize()) { - nslave = ecX; - nmaster = ecY; - } else { - nslave = ecY; - nmaster = ecX; - } - - nslave->setFind(nmaster); - - for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->d_next ) { - for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ) { - if(equiv(Px->d_data,Py->d_data)) { - Node pendingEq = (Px->d_data).eqNode(Py->d_data); - d_pending.push_back(pendingEq); - } - } - } - - ECData::takeOverDescendantWatchList(nslave, nmaster); -} - -void TheoryUFTim::merge() { - while(d_currentPendingIdx < d_pending.size() ) { - Node assertion = d_pending[d_currentPendingIdx]; - d_currentPendingIdx = d_currentPendingIdx + 1; - - TNode x = assertion[0]; - TNode y = assertion[1]; - - ECData* tmpX = x.getAttribute(ECAttr()); - ECData* tmpY = y.getAttribute(ECAttr()); - - ECData* ecX = ccFind(tmpX); - ECData* ecY = ccFind(tmpY); - if(ecX == ecY) - continue; - - Debug("uf") << "merging equivalence classes for " << std::endl; - Debug("uf") << "left equivalence class :" << (ecX->getRep()) << std::endl; - Debug("uf") << "right equivalence class :" << (ecY->getRep()) << std::endl; - Debug("uf") << std::endl; - - ccUnion(ecX, ecY); - } -} - -Node TheoryUFTim::constructConflict(TNode diseq) { - Debug("uf") << "uf: begin constructConflict()" << std::endl; - - NodeBuilder<> nb(kind::AND); - nb << diseq; - for(unsigned i = 0; i < d_assertions.size(); ++i) { - nb << d_assertions[i]; - } - - Assert(nb.getNumChildren() > 0); - Node conflict = nb.getNumChildren() == 1 ? nb[0] : nb; - - Debug("uf") << "conflict constructed : " << conflict << std::endl; - - Debug("uf") << "uf: ending constructConflict()" << std::endl; - - return conflict; -} - -void TheoryUFTim::check(Effort level) { - - Debug("uf") << "uf: begin check(" << level << ")" << std::endl; - - while(!done()) { - Node assertion = get(); - Debug("uf") << "TheoryUFTim::check(): " << assertion << std::endl; - - switch(assertion.getKind()) { - case EQUAL: - d_assertions.push_back(assertion); - d_pending.push_back(assertion); - merge(); - break; - case NOT: - Assert(assertion[0].getKind() == EQUAL, - "predicates not supported in this UF implementation"); - d_disequality.push_back(assertion[0]); - break; - case APPLY_UF: - Unhandled("predicates not supported in this UF implementation"); - default: - Unhandled(assertion.getKind()); - } - - Debug("uf") << "TheoryUFTim::check(): done = " << (done() ? "true" : "false") << std::endl; - } - - //Make sure all outstanding merges are completed. - if(d_currentPendingIdx < d_pending.size()) { - merge(); - } - - if(standardEffortOrMore(level)) { - for(CDList<Node>::const_iterator diseqIter = d_disequality.begin(); - diseqIter != d_disequality.end(); - ++diseqIter) { - - TNode left = (*diseqIter)[0]; - TNode right = (*diseqIter)[1]; - if(sameCongruenceClass(left, right)) { - Node remakeNeq = (*diseqIter).notNode(); - Node conflict = constructConflict(remakeNeq); - d_out->conflict(conflict, false); - return; - } - } - } - - Debug("uf") << "uf: end check(" << level << ")" << std::endl; -} diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h deleted file mode 100644 index 70c60728f..000000000 --- a/src/theory/uf/tim/theory_uf_tim.h +++ /dev/null @@ -1,225 +0,0 @@ -/********************* */ -/*! \file theory_uf_tim.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief This is a basic implementation of the Theory of Uninterpreted Functions - ** with Equality. - ** - ** This is a basic implementation of the Theory of Uninterpreted Functions - ** with Equality. It is based on the Nelson-Oppen algorithm given in - ** "Fast Decision Procedures Based on Congruence Closure" - ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf) - ** This has been extended to work in a context-dependent way. - ** This interacts heavily with the data-structures given in ecdata.h . - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H -#define __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H - -#include "expr/node.h" -#include "expr/attribute.h" - -#include "theory/theory.h" - -#include "context/context.h" -#include "context/cdo.h" -#include "context/cdlist.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/tim/ecdata.h" - -namespace CVC4 { -namespace theory { -namespace uf { -namespace tim { - -class TheoryUFTim : public TheoryUF { - -private: - - /** - * List of all of the non-negated literals from the assertion queue. - * This is used only for conflict generation. - * This differs from pending as the program generates new equalities that - * are not in this list. - * This will probably be phased out in future version. - */ - context::CDList<Node> d_assertions; - - /** - * List of pending equivalence class merges. - * - * Tricky part: - * Must keep a hard link because new equality terms are created and appended - * to this list. - */ - context::CDList<Node> d_pending; - - /** 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; - - /** - * List of all of the terms that are registered in the current context. - * When registerTerm is called on a term we want to guarentee that there - * is a hard link to the term for the duration of the context in which - * register term is called. - * This invariant is enough for us to use soft links where we want is the - * current implementation as well as making ECAttr() not context dependent. - * Soft links used both in ECData, and Link. - */ - context::CDList<Node> d_registered; - -public: - - /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFTim(context::Context* c, OutputChannel& out, Valuation valuation); - - /** Destructor for the TheoryUF object. */ - ~TheoryUFTim(); - - /** - * Registers a previously unseen [in this context] node n. - * For TheoryUF, this sets up and maintains invaraints about - * equivalence class data-structures. - * - * Overloads a void registerTerm(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - void registerTerm(TNode n); - - /** - * Currently this does nothing. - * - * Overloads a void preRegisterTerm(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - void preRegisterTerm(TNode n); - - /** - * Checks whether the set of literals provided to the theory is consistent. - * - * If this is called at any effort level, it computes the congruence closure - * of all of the positive literals in the context. - * - * If this is called at full effort it checks if any of the negative literals - * are inconsistent with the congruence closure. - * - * Overloads void check(Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void check(Effort level); - - void presolve() { - // do nothing - } - - /** - * Propagates theory literals. Currently does nothing. - * - * Overloads void propagate(Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void propagate(Effort level) {} - - /** - * Explains a previously reported conflict. Currently does nothing. - * - * Overloads void explain(TNode n, Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void explain(TNode n) {} - - /** - * Get a theory value. - * - * Overloads Node getValue(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - Node getValue(TNode n) { - Unimplemented("TheoryUFTim doesn't support model generation"); - } - - std::string identify() const { return std::string("TheoryUFTim"); } - -private: - /** - * Checks whether 2 nodes are already in the same equivalence class tree. - * This should only be used internally, and it should only be called 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(TNode x, TNode 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(); - - /** Constructs a conflict from an inconsistent disequality. */ - Node constructConflict(TNode diseq); - -};/* class TheoryUFTim */ - - -/** - * Cleanup function for ECData. This will be used for called whenever - * a ECAttr is being destructed. - */ -struct ECCleanupStrategy { - static void cleanup(ECData* ec) { - Debug("ufgc") << "cleaning up ECData " << ec << "\n"; - ec->deleteSelf(); - } -};/* struct ECCleanupStrategy */ - -/** Unique name to use for constructing ECAttr. */ -struct ECAttrTag {}; - -/** - * ECAttr is the attribute that maps a node to an equivalence class. - */ -typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr; - -}/* CVC4::theory::uf::tim namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */ |