diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-02-20 14:48:22 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-02-20 14:48:22 +0000 |
| commit | a426d4b7795a173d6a50418a38a3b41bbfaf880d (patch) | |
| tree | 0687d074dd73c5b474538814e1c5f29207f48ab1 /src/theory/theory_engine.h | |
| parent | 96240c3cbc2a25e2d9ab14d1048ffda82a83ded2 (diff) | |
Added Theory::postsolve() infrastructure as Clark requested.
(Though currently unused.)
For theories that request presolve and postsolve (in their kinds file),
they will get a presolve() notification before the first check(). After
the final check during the current search, they get a postsolve().
presolve() and postsolve() notifications always come in pairs, bracketing
all check()/propagate()/getValue() calls related to a single query. In
the case of incremental benchmarks, theories may get additional
presolve()/postsolve() pairs, but again, they always come in pairs.
Expected performance impact: none (for theories that don't use it)
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3598&reference_id=3581&p=5
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 387468b14..147fb868e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -519,6 +519,11 @@ public: */ bool presolve(); + /** + * Calls postsolve() on all active theories. + */ + void postsolve(); + /** * Calls notifyRestart() on all active theories. */ |