From bb2a0e0e12f39a1b4dea8fb0c990decba4708a1c Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 16 Nov 2010 21:11:11 +0000 Subject: Added Theory::presolve(). --- src/theory/theory.h | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/theory/theory.h') diff --git a/src/theory/theory.h b/src/theory/theory.h index df9dcafef..de260dd99 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -443,6 +443,16 @@ public: */ virtual Node getValue(TNode n, TheoryEngine* engine) = 0; + /** + * A Theory is called with presolve exactly one time per user check-sat. + * presolve() is called after preregistration, rewriting, and Boolean propagation, + * (other theories' propagation?), but the notified Theory has not yet had its check() + * or propagate() method called yet. + * A Theory may empty its assertFact() queue using get(). + * A Theory can raise conflicts, add lemmas, and propagate literals during presolve. + */ + virtual void presolve() = 0; + /** * Identify this theory (for debugging, dynamic configuration, * etc..) -- cgit v1.2.3