diff options
author | Tim King <taking@cs.nyu.edu> | 2010-11-16 21:11:11 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-11-16 21:11:11 +0000 |
commit | bb2a0e0e12f39a1b4dea8fb0c990decba4708a1c (patch) | |
tree | 6e5824f8cf1b0f1cb32e6cae5cbd214b1b48d965 /src/theory/theory.h | |
parent | e66924cb0f425ca70969058532340e68c9c17a54 (diff) |
Added Theory::presolve().
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 10 |
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..) */ |