diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/Makefile.am | 2 | ||||
-rw-r--r-- | src/theory/arith/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 4 | ||||
-rw-r--r-- | src/theory/arrays/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 4 | ||||
-rw-r--r-- | src/theory/booleans/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 4 | ||||
-rw-r--r-- | src/theory/bv/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 4 | ||||
-rw-r--r-- | src/theory/theory.cpp | 77 | ||||
-rw-r--r-- | src/theory/theory.h | 183 | ||||
-rw-r--r-- | src/theory/uf/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 87 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 21 |
14 files changed, 177 insertions, 224 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 2891e64cf..6b1854bfc 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libtheory.la diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 226d5af12..cb838f497 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -1,12 +1,11 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libarith.la libarith_la_SOURCES = \ - theory_def.h \ theory_arith.h EXTRA_DIST = kinds diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 973651f7a..d211cd37d 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -25,10 +25,10 @@ namespace CVC4 { namespace theory { namespace arith { -class TheoryArith : public TheoryImpl<TheoryArith> { +class TheoryArith : public Theory { public: TheoryArith(context::Context* c, OutputChannel& out) : - TheoryImpl<TheoryArith>(c, out) { + Theory(c, out) { } void preRegisterTerm(TNode n) { Unimplemented(); } diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index af3a28b3b..5d3514dda 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -1,12 +1,11 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libarrays.la libarrays_la_SOURCES = \ - theory_def.h \ theory_arrays.h EXTRA_DIST = kinds diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index ec3b88ccd..2f62aacd7 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -25,10 +25,10 @@ namespace CVC4 { namespace theory { namespace arrays { -class TheoryArrays : public TheoryImpl<TheoryArrays> { +class TheoryArrays : public Theory { public: TheoryArrays(context::Context* c, OutputChannel& out) : - TheoryImpl<TheoryArrays>(c, out) { + Theory(c, out) { } void preRegisterTerm(TNode n) { Unimplemented(); } diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index cbdf13add..690299630 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -1,12 +1,11 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libbooleans.la libbooleans_la_SOURCES = \ - theory_def.h \ theory_bool.h EXTRA_DIST = kinds diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 5196bb018..eb6e84c39 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -25,10 +25,10 @@ namespace CVC4 { namespace theory { namespace booleans { -class TheoryBool : public TheoryImpl<TheoryBool> { +class TheoryBool : public Theory { public: TheoryBool(context::Context* c, OutputChannel& out) : - TheoryImpl<TheoryBool>(c, out) { + Theory(c, out) { } void preRegisterTerm(TNode n) { Unimplemented(); } diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index 54622bf9a..d90472fd3 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -1,12 +1,11 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libbv.la libbv_la_SOURCES = \ - theory_def.h \ theory_bv.h EXTRA_DIST = kinds diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index fbb62545d..a859291a7 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -25,10 +25,10 @@ namespace CVC4 { namespace theory { namespace bv { -class TheoryBV : public TheoryImpl<TheoryBV> { +class TheoryBV : public Theory { public: TheoryBV(context::Context* c, OutputChannel& out) : - TheoryImpl<TheoryBV>(c, out) { + Theory(c, out) { } void preRegisterTerm(TNode n) { Unimplemented(); } diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 17a35f2ed..d4bd717be 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -23,5 +23,82 @@ using namespace std; namespace CVC4 { namespace theory { +Node Theory::get() { + Assert( !d_facts.empty(), + "Theory::get() called with assertion queue empty!" ); + + Node fact = d_facts.front(); + d_facts.pop_front(); + + Debug("theory") << "Theory::get() => " << fact + << "(" << d_facts.size() << " left)" << std::endl; + + if(! fact.getAttribute(RegisteredAttr())) { + std::list<TNode> toReg; + toReg.push_back(fact); + + Debug("theory") << "Theory::get(): registering new atom" << std::endl; + + /* Essentially this is doing a breadth-first numbering of + * non-registered subterms with children. Any non-registered + * leaves are immediately registered. */ + for(std::list<TNode>::iterator workp = toReg.begin(); + workp != toReg.end(); + ++workp) { + + TNode n = *workp; + + if(n.hasOperator()) { + TNode c = n.getOperator(); + + if(! c.getAttribute(RegisteredAttr())) { + if(c.getNumChildren() == 0) { + c.setAttribute(RegisteredAttr(), true); + registerTerm(c); + } else { + toReg.push_back(c); + } + } + } + + for(TNode::iterator i = n.begin(); i != n.end(); ++i) { + TNode c = *i; + + if(! c.getAttribute(RegisteredAttr())) { + if(c.getNumChildren() == 0) { + c.setAttribute(RegisteredAttr(), true); + registerTerm(c); + } else { + toReg.push_back(c); + } + } + } + } + + /* Now register the list of terms in reverse order. Between this + * and the above registration of leaves, this should ensure that + * all subterms in the entire tree were registered in + * reverse-topological order. */ + for(std::list<TNode>::reverse_iterator i = toReg.rbegin(); + i != toReg.rend(); + ++i) { + + TNode n = *i; + + /* Note that a shared TNode in the DAG rooted at "fact" could + * appear twice on the list, so we have to avoid hitting it + * twice. */ + // FIXME when ExprSets are online, use one of those to avoid + // duplicates in the above? + if(! n.getAttribute(RegisteredAttr())) { + n.setAttribute(RegisteredAttr(), true); + registerTerm(n); + } + } + } + + return fact; +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 4c3a43061..2fcac86b0 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -38,36 +38,22 @@ namespace theory { struct RewriteCacheTag {}; typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache; -template <class T> -class TheoryImpl; - /** * Base class for T-solvers. Abstract DPLL(T). * * This is essentially an interface class. The TheoryEngine has - * pointers to Theory. But each individual theory implementation T - * should inherit from TheoryImpl<T>, which specializes a few things - * for that theory. + * pointers to Theory. Note that only one specific Theory type (e.g., + * TheoryUF) can exist per NodeManager, because of how the + * RegisteredAttr works. (If you need multiple instances of the same + * theory, you'll have to write a multiplexed theory that dispatches + * all calls to them.) */ class Theory { private: - template <class T> - friend class ::CVC4::theory::TheoryImpl; - friend class ::CVC4::TheoryEngine; /** - * Construct a Theory. - */ - Theory(context::Context* ctxt, OutputChannel& out) throw() : - d_context(ctxt), - d_facts(), - d_factsResetter(*this), - d_out(&out) { - } - - /** * Disallow default construction. */ Theory(); @@ -110,13 +96,23 @@ private: protected: /** + * Construct a Theory. + */ + Theory(context::Context* ctxt, OutputChannel& out) throw() : + d_context(ctxt), + d_facts(), + d_factsResetter(*this), + d_out(&out) { + } + + /** * This is called at shutdown time by the TheoryEngine, just before * destruction. It is important because there are destruction * ordering issues between PropEngine and Theory (based on what * hard-links to Nodes are outstanding). As the fact queue might be * nonempty, we ensure here that it's clear. If you overload this, - * you must make an explicit call here to the Theory implementation - * of this function too. + * you must make an explicit call here to this->Theory::shutdown() + * too. */ virtual void shutdown() { d_facts.clear(); @@ -158,6 +154,24 @@ protected: return n.getAttribute(RewriteCache()); } + /** Tag for the "registerTerm()-has-been-called" flag on Nodes */ + struct Registered {}; + /** The "registerTerm()-has-been-called" flag on Nodes */ + typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr; + + /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */ + struct PreRegistered {}; + /** The "preRegisterTerm()-has-been-called" flag on Nodes */ + typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr; + + /** + * Returns the next atom in the assertFact() queue. Guarantees that + * registerTerm() has been called on the theory specific subterms. + * + * @return the next atom in the assertFact() queue. + */ + Node get(); + public: /** @@ -308,133 +322,6 @@ protected: };/* class Theory */ - -/** - * Base class for T-solver implementations. Each individual - * implementation T of the Theory interface should inherit from - * TheoryImpl<T>. This class specializes some things for a particular - * theory implementation. - * - * The problem with this is that Theory implementations cannot be - * further subclassed without designing all non-children in the type - * DAG to play the same trick as here (be template-polymorphic in their - * most-derived child), linearizing the inheritance hierarchy (viewing - * each instantiation separately). - */ -template <class T> -class TheoryImpl : public Theory { - -protected: - - /** - * Construct a Theory. - */ - TheoryImpl(context::Context* ctxt, OutputChannel& out) : - Theory(ctxt, out) { - /* FIXME: assert here that a TheoryImpl<T> doesn't already exist - * for this NodeManager?? If it does, we're hosed because they'll - * share per-theory node attributes. */ - } - - /** Tag for the "registerTerm()-has-been-called" flag on Nodes */ - struct Registered {}; - /** The "registerTerm()-has-been-called" flag on Nodes */ - typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr; - - /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */ - struct PreRegistered {}; - /** The "preRegisterTerm()-has-been-called" flag on Nodes */ - typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr; - - /** - * Returns the next atom in the assertFact() queue. Guarantees that - * registerTerm() has been called on the theory specific subterms. - * - * @return the next atom in the assertFact() queue. - */ - Node get(); -};/* class TheoryImpl<T> */ - -template <class T> -Node TheoryImpl<T>::get() { - Assert(typeid(*this) == typeid(T), - "Improper Theory inheritance chain detected."); - - Assert( !d_facts.empty(), - "Theory::get() called with assertion queue empty!" ); - - Node fact = d_facts.front(); - d_facts.pop_front(); - - Debug("theory") << "Theory::get() => " << fact << "(" << d_facts.size() << " left)" << std::endl; - - if(! fact.getAttribute(RegisteredAttr())) { - std::list<TNode> toReg; - toReg.push_back(fact); - - Debug("theory") << "Theory::get(): registering new atom" << std::endl; - - /* Essentially this is doing a breadth-first numbering of - * non-registered subterms with children. Any non-registered - * leaves are immediately registered. */ - for(std::list<TNode>::iterator workp = toReg.begin(); - workp != toReg.end(); - ++workp) { - - TNode n = *workp; - - if(n.hasOperator()) { - TNode c = n.getOperator(); - - if(! c.getAttribute(RegisteredAttr())) { - if(c.getNumChildren() == 0) { - c.setAttribute(RegisteredAttr(), true); - registerTerm(c); - } else { - toReg.push_back(c); - } - } - } - - for(TNode::iterator i = n.begin(); i != n.end(); ++i) { - TNode c = *i; - - if(! c.getAttribute(RegisteredAttr())) { - if(c.getNumChildren() == 0) { - c.setAttribute(RegisteredAttr(), true); - registerTerm(c); - } else { - toReg.push_back(c); - } - } - } - } - - /* Now register the list of terms in reverse order. Between this - * and the above registration of leaves, this should ensure that - * all subterms in the entire tree were registered in - * reverse-topological order. */ - for(std::list<TNode>::reverse_iterator i = toReg.rbegin(); - i != toReg.rend(); - ++i) { - - TNode n = *i; - - /* Note that a shared TNode in the DAG rooted at "fact" could - * appear twice on the list, so we have to avoid hitting it - * twice. */ - // FIXME when ExprSets are online, use one of those to avoid - // duplicates in the above? - if(! n.getAttribute(RegisteredAttr())) { - n.setAttribute(RegisteredAttr(), true); - registerTerm(n); - } - } - } - - return fact; -} - }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 156733c5b..e0aa3a1df 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -1,12 +1,11 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libuf.la libuf_la_SOURCES = \ - theory_def.h \ ecdata.h \ ecdata.cpp \ theory_uf.h \ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 3fe82b16c..f0d8b47e0 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -10,10 +10,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** + ** Implementation of the theory of uninterpreted functions. **/ - #include "theory/uf/theory_uf.h" #include "theory/uf/ecdata.h" #include "expr/kind.h" @@ -24,37 +23,32 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::uf; - - TheoryUF::TheoryUF(Context* c, OutputChannel& out) : - TheoryImpl<TheoryUF>(c, out), + Theory(c, out), d_assertions(c), d_pending(c), d_currentPendingIdx(c,0), d_disequality(c), - d_registered(c) -{} + d_registered(c) { +} -TheoryUF::~TheoryUF(){} +TheoryUF::~TheoryUF() { +} -void TheoryUF::preRegisterTerm(TNode n){ +void TheoryUF::preRegisterTerm(TNode n) { Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl; Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl; } -void TheoryUF::registerTerm(TNode n){ +void TheoryUF::registerTerm(TNode n) { Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl; - d_registered.push_back(n); - - - ECData* ecN; - if(n.getAttribute(ECAttr(), 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, @@ -101,7 +95,7 @@ void TheoryUF::registerTerm(TNode n){ "Expected getWatchListSize() == 0. " "This data is either already in use or was not properly maintained " "during backtracking"); - }else{ + } else { //The attribute does not exist, so it is created and set ecN = new (true) ECData(getContext(), n); n.setAttribute(ECAttr(), ecN); @@ -110,10 +104,10 @@ void TheoryUF::registerTerm(TNode n){ /* If the node is an APPLY_UF, we need to add it to the predecessor list * of its children. */ - if(n.getKind() == APPLY_UF){ + if(n.getKind() == APPLY_UF) { TNode::iterator cIter = n.begin(); - for(; cIter != n.end(); ++cIter){ + for(; cIter != n.end(); ++cIter) { TNode child = *cIter; /* Because this can be called after nodes have been merged, we need @@ -124,8 +118,8 @@ void TheoryUF::registerTerm(TNode n){ /* 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)){ + 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); } @@ -138,30 +132,32 @@ void TheoryUF::registerTerm(TNode n){ } -bool TheoryUF::sameCongruenceClass(TNode x, TNode y){ +bool TheoryUF::sameCongruenceClass(TNode x, TNode y) { return ccFind(x.getAttribute(ECAttr())) == ccFind(y.getAttribute(ECAttr())); } -bool TheoryUF::equiv(TNode x, TNode y){ +bool TheoryUF::equiv(TNode x, TNode y) { Assert(x.getKind() == kind::APPLY_UF); Assert(y.getKind() == kind::APPLY_UF); - if(x.getNumChildren() != y.getNumChildren()) + if(x.getNumChildren() != y.getNumChildren()) { return false; + } - if(x.getOperator() != y.getOperator()) + 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()){ + while(xIter != x.end()) { - if(!sameCongruenceClass(*xIter, *yIter)){ + if(!sameCongruenceClass(*xIter, *yIter)) { return false; } @@ -178,10 +174,10 @@ bool TheoryUF::equiv(TNode x, TNode y){ * many better algorithms use eager path compression. * 2) Elminate recursion. */ -ECData* TheoryUF::ccFind(ECData * x){ - if( x->getFind() == x) +ECData* TheoryUF::ccFind(ECData * x) { + if(x->getFind() == x) { return x; - else{ + } else { return ccFind(x->getFind()); } /* Slightly better Find w/ path compression and no recursion*/ @@ -189,7 +185,7 @@ ECData* TheoryUF::ccFind(ECData * x){ ECData* start; ECData* next = x; while(x != x->getFind()) x=x->getRep(); - while( (start = next) != x){ + while( (start = next) != x) { next = start->getFind(); start->setFind(x); } @@ -197,23 +193,23 @@ ECData* TheoryUF::ccFind(ECData * x){ */ } -void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){ +void TheoryUF::ccUnion(ECData* ecX, ECData* ecY) { ECData* nslave; ECData* nmaster; - if(ecX->getWatchListSize() <= ecY->getWatchListSize()){ + if(ecX->getWatchListSize() <= ecY->getWatchListSize()) { nslave = ecX; nmaster = ecY; - }else{ + } 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)){ + 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); } @@ -223,7 +219,7 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){ ECData::takeOverDescendantWatchList(nslave, nmaster); } -void TheoryUF::merge(){ +void TheoryUF::merge() { while(d_currentPendingIdx < d_pending.size() ) { Node assertion = d_pending[d_currentPendingIdx]; d_currentPendingIdx = d_currentPendingIdx + 1; @@ -248,7 +244,7 @@ void TheoryUF::merge(){ } } -Node TheoryUF::constructConflict(TNode diseq){ +Node TheoryUF::constructConflict(TNode diseq) { Debug("uf") << "uf: begin constructConflict()" << std::endl; NodeBuilder<> nb(kind::AND); @@ -267,15 +263,15 @@ Node TheoryUF::constructConflict(TNode diseq){ return conflict; } -void TheoryUF::check(Effort level){ +void TheoryUF::check(Effort level) { Debug("uf") << "uf: begin check(" << level << ")" << std::endl; - while(!done()){ + while(!done()) { Node assertion = get(); Debug("uf") << "TheoryUF::check(): " << assertion << std::endl; - switch(assertion.getKind()){ + switch(assertion.getKind()) { case EQUAL: d_assertions.push_back(assertion); d_pending.push_back(assertion); @@ -292,18 +288,18 @@ void TheoryUF::check(Effort level){ } //Make sure all outstanding merges are completed. - if(d_currentPendingIdx < d_pending.size()){ + if(d_currentPendingIdx < d_pending.size()) { merge(); } - if(fullEffort(level)){ + if(fullEffort(level)) { for(CDList<Node>::const_iterator diseqIter = d_disequality.begin(); diseqIter != d_disequality.end(); - ++diseqIter){ + ++diseqIter) { TNode left = (*diseqIter)[0]; TNode right = (*diseqIter)[1]; - if(sameCongruenceClass(left, right)){ + if(sameCongruenceClass(left, right)) { Node remakeNeq = (*diseqIter).notNode(); Node conflict = constructConflict(remakeNeq); d_out->conflict(conflict, false); @@ -313,5 +309,4 @@ void TheoryUF::check(Effort level){ } Debug("uf") << "uf: end check(" << level << ")" << std::endl; - } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 8495e6c9c..5863a31fc 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -38,7 +38,7 @@ namespace CVC4 { namespace theory { namespace uf { -class TheoryUF : public TheoryImpl<TheoryUF> { +class TheoryUF : public Theory { private: @@ -176,31 +176,30 @@ private: /** Constructs a conflict from an inconsistent disequality. */ Node constructConflict(TNode diseq); -}; +};/* class TheoryUF */ /** * Cleanup function for ECData. This will be used for called whenever * a ECAttr is being destructed. */ -struct ECCleanupStrategy{ - static void cleanup(ECData* ec){ +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 EquivClass; +struct ECAttrTag {}; /** * ECAttr is the attribute that maps a node to an equivalence class. */ -typedef expr::Attribute<EquivClass, ECData*, ECCleanupStrategy > ECAttr; - -} /* CVC4::theory::uf namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr; +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__THEORY__UF__THEORY_UF_H */ |