Added Theory::presolve().

1 files changed, 10 insertions, 0 deletions

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
@@ -444,6 +444,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..)
    */