diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-22 20:40:41 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-22 20:40:41 +0000 |
commit | 8c4495b18e40a406be35baceaf473878bcc375f1 (patch) | |
tree | 2c1e491cbb088e26775572160b31ae2cd250bad8 /src | |
parent | f40ec39fe48f83e1cc1a31f9e18635687bd63c76 (diff) |
some improvements to the sharing mechanism/interface
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory.h | 72 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 19 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 11 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 10 | ||||
-rw-r--r-- | src/theory/uf/equality_engine_impl.h | 35 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 39 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 2 |
8 files changed, 159 insertions, 33 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 0404bda3b..6460533e2 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -49,7 +49,7 @@ void Theory::addSharedTermInternal(TNode n) { addSharedTerm(n); } -void Theory::computeCareGraph(CareGraph& careGraph) { +void Theory::computeCareGraph() { Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << std::endl; for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) { TNode a = d_sharedTerms[i]; @@ -67,7 +67,7 @@ void Theory::computeCareGraph(CareGraph& careGraph) { break; default: // Let's split on it - careGraph.push_back(CarePair(a, b, getId())); + addCarePair(a, b); break; } } diff --git a/src/theory/theory.h b/src/theory/theory.h index c84d10ca1..a8d34eab3 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -31,6 +31,7 @@ #include "context/cdlist.h" #include "context/cdo.h" #include "util/options.h" +#include "util/stats.h" #include "util/dump.h" #include <string> @@ -71,19 +72,36 @@ struct Assertion { }; /** - * A pair of terms a theory cares about. + * A (oredered) pair of terms a theory cares about. */ struct CarePair { + TNode a, b; TheoryId theory; + +public: + CarePair(TNode a, TNode b, TheoryId theory) - : a(a), b(b), theory(theory) {} + : a(a < b ? a : b), b(a < b ? b : a), theory(theory) {} + + bool operator == (const CarePair& other) const { + return (theory == other.theory) && (a == other.a) && (b == other.b); + } + + bool operator < (const CarePair& other) const { + if (theory < other.theory) return true; + if (theory > other.theory) return false; + if (a < other.a) return true; + if (a > other.a) return false; + return b < other.b; + } + }; /** * A set of care pairs. */ -typedef std::vector<CarePair> CareGraph; +typedef std::set<CarePair> CareGraph; /** * Base class for T-solvers. Abstract DPLL(T). @@ -141,9 +159,39 @@ private: */ context::CDO<unsigned> d_sharedTermsIndex; + /** + * The care graph the theory will use during combination. + */ + CareGraph* d_careGraph; + + // === STATISTICS === + /** time spent in theory combination */ + TimerStat d_computeCareGraphTime; + + static std::string statName(TheoryId id, const char* statName) { + std::stringstream ss; + ss << "theory<" << id << ">::" << statName; + return ss.str(); + } + protected: /** + * The only method to add suff to the care graph. + */ + void addCarePair(TNode t1, TNode t2) { + if (d_careGraph) { + d_careGraph->insert(CarePair(t1, t2, d_id)); + } + } + + /** + * The function should compute the care graph over the shared terms. + * The default function returns all the pairs among the shared variables. + */ + virtual void computeCareGraph(); + + /** * A list of shared terms that the theory has. */ context::CDList<TNode> d_sharedTerms; @@ -159,10 +207,13 @@ protected: d_facts(context), d_factsHead(context, 0), d_sharedTermsIndex(context, 0), + d_careGraph(0), + d_computeCareGraphTime(statName(id, "computeCareGraphTime")), d_sharedTerms(context), d_out(&out), d_valuation(valuation) { + StatisticsRegistry::registerStat(&d_computeCareGraphTime); } /** @@ -213,14 +264,13 @@ protected: void printFacts(std::ostream& os) const; - public: /** * Return the ID of the theory responsible for the given type. */ static inline TheoryId theoryOf(TypeNode typeNode) { - Trace("theory") << "theoryOf(" << typeNode << ")" << std::endl; + Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl; TheoryId id; while (typeNode.isPredicateSubtype()) { typeNode = typeNode.getSubtypeBaseType(); @@ -289,6 +339,7 @@ public: * destructor. */ virtual ~Theory() { + StatisticsRegistry::unregisterStat(&d_computeCareGraphTime); } /** @@ -378,10 +429,15 @@ public: virtual void addSharedTerm(TNode n) { } /** - * The function should compute the care graph over the shared terms. - * The default function returns all the pairs among the shared variables. + * Return the current theory care graph. Theories should overload computeCareGraph to do + * the actual computation, and use addCarePair to add pairs to the care graph. */ - virtual void computeCareGraph(CareGraph& careGraph); + void getCareGraph(CareGraph& careGraph) { + TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime); + d_careGraph = &careGraph; + computeCareGraph(); + d_careGraph = NULL; + } /** * Return the status of two terms in the current context. Should be implemented in diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ebfc797a1..a3ff4d90b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -56,6 +56,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_propagatedLiteralsIndex(context, 0), d_decisionRequests(context), d_decisionRequestsIndex(context, 0), + d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms) { @@ -64,6 +65,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_theoryOut[theoryId] = NULL; } Rewriter::init(); + StatisticsRegistry::registerStat(&d_combineTheoriesTime); } TheoryEngine::~TheoryEngine() { @@ -75,6 +77,8 @@ TheoryEngine::~TheoryEngine() { delete d_theoryOut[theoryId]; } } + + StatisticsRegistry::unregisterStat(&d_combineTheoriesTime); } void TheoryEngine::preRegister(TNode preprocessed) { @@ -235,29 +239,30 @@ void TheoryEngine::combineTheories() { Debug("sharing") << "TheoryEngine::combineTheories()" << std::endl; + TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime); + CareGraph careGraph; #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::isParametric && isActive(THEORY)) { \ - CareGraph theoryGraph; \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->computeCareGraph(theoryGraph); \ - careGraph.insert(careGraph.end(), theoryGraph.begin(), theoryGraph.end()); \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->getCareGraph(careGraph); \ } CVC4_FOR_EACH_THEORY; // Now add splitters for the ones we are interested in - for (unsigned i = 0; i < careGraph.size(); ++ i) { - const CarePair& carePair = careGraph[i]; + CareGraph::const_iterator care_it = careGraph.begin(); + CareGraph::const_iterator care_it_end = careGraph.end(); + for (; care_it != care_it_end; ++ care_it) { + const CarePair& carePair = *care_it; Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl; Node equality = carePair.a.eqNode(carePair.b); Node normalizedEquality = Rewriter::rewrite(equality); - bool isTrivial = normalizedEquality.getKind() == kind::CONST_BOOLEAN; - + bool isTrivial = normalizedEquality.getKind() == kind::CONST_BOOLEAN; // If the node has a literal, it has been asserted so we should just check it bool value; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index a8aa62d35..5712b1502 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -194,28 +194,28 @@ class TheoryEngine { } void conflict(TNode conflictNode) throw(AssertionException) { - Trace("theory") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; + Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; ++ d_statistics.conflicts; d_engine->d_outputChannelUsed = true; d_engine->conflict(conflictNode, d_theory); } void propagate(TNode literal) throw(AssertionException) { - Trace("theory") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; + Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; ++ d_statistics.propagations; d_engine->d_outputChannelUsed = true; d_engine->propagate(literal, d_theory); } void propagateAsDecision(TNode literal) throw(AssertionException) { - Trace("theory") << "EngineOutputChannel<" << d_theory << ">::propagateAsDecision(" << literal << ")" << std::endl; + Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagateAsDecision(" << literal << ")" << std::endl; ++ d_statistics.propagationsAsDecisions; d_engine->d_outputChannelUsed = true; d_engine->propagateAsDecision(literal, d_theory); } theory::LemmaStatus lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { - Trace("theory") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; + Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; return d_engine->lemma(lemma, false, removable); @@ -419,6 +419,9 @@ class TheoryEngine { return theory::LemmaStatus(finalForm, d_userContext->getLevel()); } + /** Time spent in theory combination */ + TimerStat d_combineTheoriesTime; + public: /** Constructs a theory engine */ diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 7314b6552..d8757926a 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -632,6 +632,11 @@ public: TNode getRepresentative(TNode t) const; /** + * Add all the terms where the given term appears in (directly or implicitly). + */ + void getUseListTerms(TNode t, std::set<TNode>& output); + + /** * Returns true if the two nodes are in the same class. */ bool areEqual(TNode t1, TNode t2) const; @@ -663,6 +668,11 @@ public: bool isTriggerTerm(TNode t) const; /** + * Returns the representative trigger term (isTriggerTerm(t)) should be true. + */ + TNode getTriggerTermRepresentative(TNode t) const; + + /** * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with * trigger. */ diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h index 925410561..dd1bf0cbc 100644 --- a/src/theory/uf/equality_engine_impl.h +++ b/src/theory/uf/equality_engine_impl.h @@ -886,6 +886,14 @@ bool EqualityEngine<NotifyClass>::isTriggerTerm(TNode t) const { return d_nodeIndividualTrigger[classId] != +null_id; } + +template <typename NotifyClass> +TNode EqualityEngine<NotifyClass>::getTriggerTermRepresentative(TNode t) const { + Assert(isTriggerTerm(t)); + EqualityNodeId classId = getEqualityNode(t).getFind(); + return d_nodes[d_nodeIndividualTrigger[classId]]; +} + template <typename NotifyClass> void EqualityEngine<NotifyClass>::storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId) { Assert(d_applicationLookup.find(funNormalized) == d_applicationLookup.end()); @@ -897,6 +905,33 @@ void EqualityEngine<NotifyClass>::storeApplicationLookup(FunctionApplication& fu Assert(d_applicationLookupsCount == d_applicationLookups.size()); } +template <typename NotifyClass> +void EqualityEngine<NotifyClass>::getUseListTerms(TNode t, std::set<TNode>& output) { + if (hasTerm(t)) { + // Get the equivalence class + EqualityNodeId classId = getEqualityNode(t).getFind(); + // Go through the equivalence class and get where t is used in + EqualityNodeId currentId = classId; + do { + // Get the current node + EqualityNode& currentNode = getEqualityNode(currentId); + // Go through the use-list + UseListNodeId currentUseId = currentNode.getUseList(); + while (currentUseId != null_uselist_id) { + // Get the node of the use list + UseListNode& useNode = d_useListNodes[currentUseId]; + // Get the function application + EqualityNodeId funId = useNode.getApplicationId(); + output.insert(d_nodes[funId]); + // Go to the next one in the use list + currentUseId = useNode.getNext(); + } + // Move to the next node + currentId = currentNode.getNext(); + } while (currentId != classId); + } +} + } // Namespace uf } // Namespace theory } // Namespace CVC4 diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 7f5e11a64..f0694462d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -396,12 +396,21 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { }/* TheoryUF::ppStaticLearn() */ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) { + + Node equality = a.eqNode(b); + Node rewrittenEquality = Rewriter::rewrite(equality); + if (rewrittenEquality.isConst()) { + if (!rewrittenEquality.getConst<bool>()) { + return EQUALITY_FALSE; + } + } + if (d_equalityEngine.areEqual(a, b)) { // The terms are implied to be equal return EQUALITY_TRUE; } if (d_equalityEngine.areDisequal(a, b)) { - // The rems are implied to be dis-equal + // The terms are implied to be dis-equal return EQUALITY_FALSE; } // All other terms we interpret as dis-equal in the model @@ -413,17 +422,19 @@ void TheoryUF::addSharedTerm(TNode t) { d_equalityEngine.addTriggerTerm(t); } -void TheoryUF::computeCareGraph(CareGraph& careGraph) { +void TheoryUF::computeCareGraph() { if (d_sharedTerms.size() > 0) { - std::vector<CarePair> currentPairs; + vector< pair<TNode, TNode> > currentPairs; // Go through the function terms and see if there are any to split on unsigned functionTerms = d_functionsTerms.size(); for (unsigned i = 0; i < functionTerms; ++ i) { + TNode f1 = d_functionsTerms[i]; Node op = f1.getOperator(); + for (unsigned j = i + 1; j < functionTerms; ++ j) { TNode f2 = d_functionsTerms[j]; @@ -462,24 +473,30 @@ void TheoryUF::computeCareGraph(CareGraph& careGraph) { break; } - if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) { - // Not connected to shared terms, we don't care - continue; - } - if (eqStatusUf == EQUALITY_TRUE) { - // We don't neeed this one + // We don't need this one Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal" << std::endl; continue; } + if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) { + // Not connected to shared terms, we don't care + continue; + } + + // Get representative trigger terms + TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x); + TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y); + // Otherwise, we need to figure it out Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl; - currentPairs.push_back(CarePair(x, y, THEORY_UF)); + currentPairs.push_back(make_pair(x_shared, y_shared)); } if (!somePairIsDisequal) { - careGraph.insert(careGraph.end(), currentPairs.begin(), currentPairs.end()); + for (unsigned i = 0; i < currentPairs.size(); ++ i) { + addCarePair(currentPairs[i].first, currentPairs[i].second); + } } } } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index cb7674342..071883e1a 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -113,7 +113,7 @@ public: void presolve(); void addSharedTerm(TNode n); - void computeCareGraph(CareGraph& careGraph); + void computeCareGraph(); EqualityStatus getEqualityStatus(TNode a, TNode b); |