diff options
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index e6a2e2336..af891e3a3 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -535,6 +535,18 @@ public: virtual void presolve() { } /** + * A Theory is called with postsolve exactly one time per user + * check-sat. postsolve() is called after the query has completed + * (regardless of whether sat, unsat, or unknown), and after any + * model-querying related to the query has been performed. + * After this call, the theory will not get another check() or + * propagate() call until presolve() is called again. A Theory + * cannot raise conflicts, add lemmas, or propagate literals during + * postsolve(). + */ + virtual void postsolve() { } + + /** * Notification sent to the theory wheneven the search restarts. * Serves as a good time to do some clean-up work, and you can * assume you're at DL 0 for the purposes of Contexts. This function |