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/theory/theory.h | |
parent | f40ec39fe48f83e1cc1a31f9e18635687bd63c76 (diff) |
some improvements to the sharing mechanism/interface
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 72 |
1 files changed, 64 insertions, 8 deletions
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 |