From 09d14ac7f81111882327cb168f100e9f998611ac Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 27 Mar 2017 10:02:11 -0700 Subject: [PATCH] Moving the CareGraph into its own file. --- src/Makefile.am | 1 + src/theory/care_graph.h | 62 ++++++++++++++++++++++++++++ src/theory/theory.cpp | 16 ++++++++ src/theory/theory.h | 78 ++++++++++-------------------------- src/theory/theory_engine.cpp | 3 +- 5 files changed, 102 insertions(+), 58 deletions(-) create mode 100644 src/theory/care_graph.h diff --git a/src/Makefile.am b/src/Makefile.am index 1d43b4ec2..5caed7b14 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -146,6 +146,7 @@ libcvc4_la_SOURCES = \ theory/assertion.h \ theory/atom_requests.cpp \ theory/atom_requests.h \ + theory/care_graph.h \ theory/interrupted.h \ theory/ite_utilities.cpp \ theory/ite_utilities.h \ diff --git a/src/theory/care_graph.h b/src/theory/care_graph.h new file mode 100644 index 000000000..870d3f4be --- /dev/null +++ b/src/theory/care_graph.h @@ -0,0 +1,62 @@ +/********************* */ +/*! \file care_graph.h + ** \verbatim + ** Top contributors (to current version): + ** Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The care graph datastructure. + ** + ** The care graph datastructure. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__CARE_GRAPH_H +#define __CVC4__THEORY__CARE_GRAPH_H + +#include + +#include "expr/kind.h" // For TheoryId. +#include "expr/node.h" + +namespace CVC4 { +namespace theory { + +/** + * A (ordered) pair of terms a theory cares about. + */ +struct CarePair { + const TNode a, b; + const TheoryId theory; + + CarePair(TNode a, TNode b, TheoryId 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; + } + +}; /* struct CarePair */ + +/** + * A set of care pairs. + */ +typedef std::set CareGraph; + +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__CARE_GRAPH_H */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 340ab2373..ab72bf55f 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -296,6 +296,22 @@ std::pair Theory::entailmentCheck( return make_pair(false, Node::null()); } +void Theory::addCarePair(TNode t1, TNode t2) { + if (d_careGraph) { + d_careGraph->insert(CarePair(t1, t2, d_id)); + } +} + +void Theory::getCareGraph(CareGraph* careGraph) { + Assert(careGraph != NULL); + + Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl; + TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime); + d_careGraph = careGraph; + computeCareGraph(); + d_careGraph = NULL; +} + EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid) : d_tid(tid) { } diff --git a/src/theory/theory.h b/src/theory/theory.h index 0bea566b1..5701f0a7b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -36,6 +36,7 @@ #include "smt/dump.h" #include "smt/logic_request.h" #include "theory/assertion.h" +#include "theory/care_graph.h" #include "theory/logic_info.h" #include "theory/output_channel.h" #include "theory/valuation.h" @@ -63,37 +64,6 @@ namespace eq { class EqualityEngine; }/* CVC4::theory::eq namespace */ - -/** - * A (ordered) pair of terms a theory cares about. - */ -struct CarePair { - public: - const TNode a, b; - const TheoryId theory; - - CarePair(TNode a, TNode b, TheoryId 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; - } - -}; /* struct CarePair */ - -/** - * A set of care pairs. - */ -typedef std::set CareGraph; - /** * Base class for T-solvers. Abstract DPLL(T). * @@ -186,11 +156,7 @@ 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)); - } - } + void addCarePair(TNode t1, TNode t2); /** * The function should compute the care graph over the shared terms. @@ -207,6 +173,7 @@ protected: * Helper function for computeRelevantTerms */ void collectTerms(TNode n, std::set& termSet) const; + /** * Scans the current set of assertions and shared terms top-down * until a theory-leaf is reached, and adds all terms found to @@ -486,7 +453,9 @@ public: * Assert a fact in the current context. */ void assertFact(TNode assertion, bool isPreregistered) { - Trace("theory") << "Theory<" << getId() << ">::assertFact[" << d_satContext->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl; + Trace("theory") << "Theory<" << getId() << ">::assertFact[" + << d_satContext->getLevel() << "](" << assertion << ", " + << (isPreregistered ? "true" : "false") << ")" << std::endl; d_facts.push_back(Assertion(assertion, isPreregistered)); } @@ -509,22 +478,19 @@ public: } /** - * 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. + * 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. */ - void getCareGraph(CareGraph& careGraph) { - Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl; - TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime); - d_careGraph = &careGraph; - computeCareGraph(); - d_careGraph = NULL; - } + void getCareGraph(CareGraph* careGraph); /** - * Return the status of two terms in the current context. Should be implemented in - * sub-theories to enable more efficient theory-combination. + * Return the status of two terms in the current context. Should be + * implemented in sub-theories to enable more efficient theory-combination. */ - virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } + virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { + return EQUALITY_UNKNOWN; + } /** * Return the model value of the give shared term (or null if not available). @@ -541,14 +507,11 @@ public: * - or call get() until done() is true. */ virtual void check(Effort level = EFFORT_FULL) { } - - /** - * Needs last effort check? - */ + + /** Needs last effort check? */ virtual bool needsCheckLastEffort() { return false; } - /** - * T-propagate new literal assignments in the current context. - */ + + /** T-propagate new literal assignments in the current context. */ virtual void propagate(Effort level = EFFORT_FULL) { } /** @@ -569,9 +532,10 @@ public: * class. */ virtual void collectModelInfo( TheoryModel* m, bool fullModel ){ } + /** if theories want to do something with model after building, do it here */ virtual void postProcessModel( TheoryModel* m ){ } - + /** * Return a decision request, if the theory has one, or the NULL node * otherwise. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 8014a8f22..a68625da8 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -37,6 +37,7 @@ #include "smt_util/node_visitor.h" #include "theory/arith/arith_ite_utils.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/care_graph.h" #include "theory/ite_utilities.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/model_engine.h" @@ -662,7 +663,7 @@ void TheoryEngine::combineTheories() { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \ - theoryOf(THEORY)->getCareGraph(careGraph); \ + theoryOf(THEORY)->getCareGraph(&careGraph); \ } // Call on each parametric theory to give us its care graph -- 2.30.2