summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/care_graph.h62
-rw-r--r--src/theory/theory.cpp16
-rw-r--r--src/theory/theory.h78
-rw-r--r--src/theory/theory_engine.cpp3
4 files changed, 101 insertions, 58 deletions
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 <set>
+
+#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<CarePair> 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<bool, Node> 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<CarePair> 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<Node>& 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<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
- theoryOf(THEORY)->getCareGraph(careGraph); \
+ theoryOf(THEORY)->getCareGraph(&careGraph); \
}
// Call on each parametric theory to give us its care graph
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback