From 663a6edef6b65d400e2d97dc9c8276da3d3cb0b1 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 19 Nov 2010 01:37:55 +0000 Subject: Merge from ufprop branch, including: * Theory::staticLearning() for statically adding new T-stuff before normal preprocessing. UF's staticLearning() does transitivity of equality/iff, solving the diamonds. * more aggressive T-propagation for UF * new KEEP_STATISTIC macro to hide Theories from having to register/deregister statistics (and also has the advantage of keeping the statistic type, field name, and the 'tag' used to output the statistic in the same place---instead of scattered in the theory definition and constructor initializer list. See documentation for KEEP_STATISTIC in src/util/stats.h for more of an explanation). * more statistics for UF * restart notifications from SAT (through TheoryEngine) via Theory::notifyRestart() * StackingMap and UnionFind unit tests * build fixes/adjustments * code cleanup; minor other improvements --- src/theory/theory_engine.h | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) (limited to 'src/theory/theory_engine.h') diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 8ee5c91d7..3176b9698 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -309,12 +309,23 @@ public: return d_theoryOut.d_conflictNode.get().isNull(); } + /** + * Calls staticLearning() on all active theories, accumulating their + * combined contributions in the "learned" builder. + */ + void staticLearning(TNode in, NodeBuilder<>& learned); + /** * Calls presolve() on all active theories and returns true * if one of the theories discovers a conflict. */ bool presolve(); + /** + * Calls notifyRestart() on all active theories. + */ + void notifyRestart(); + inline const std::vector& getPropagatedLiterals() const { return d_theoryOut.d_propagatedLiterals; } @@ -365,9 +376,9 @@ private: public: IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanation; Statistics(): - d_statConflicts("theory::conflicts",0), - d_statPropagate("theory::propagate",0), - d_statLemma("theory::lemma",0), + d_statConflicts("theory::conflicts", 0), + d_statPropagate("theory::propagate", 0), + d_statLemma("theory::lemma", 0), d_statAugLemma("theory::aug_lemma", 0), d_statExplanation("theory::explanation", 0) { -- cgit v1.2.3