diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-09-03 23:46:43 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-09-03 23:46:43 -0700 |
commit | ed21776f3fdf079ebedaee6882cf6d86c9159dd1 (patch) | |
tree | cc0399535673536fd1376f647e2c38778066a2e5 /src/theory/theory_engine.cpp | |
parent | c9e23f66383a4d490aca6d082d40117fe799ee4b (diff) |
Remove unused postsolve infrastructurermPostsolve
The theory property `postsolve` was not used by any of the theories.
This commit removes the property and associated infrastructure.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 28 |
1 files changed, 0 insertions, 28 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ac06d266d..a834ca300 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -749,34 +749,6 @@ bool TheoryEngine::presolve() { return false; }/* TheoryEngine::presolve() */ -void TheoryEngine::postsolve() { - // no longer in SAT mode - d_inSatMode = false; - // Reset the interrupt flag - d_interrupted = false; - bool CVC4_UNUSED wasInConflict = d_inConflict; - - try { - // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT -#endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPostsolve) \ - { \ - theoryOf(THEORY)->postsolve(); \ - Assert(!d_inConflict || wasInConflict) \ - << "conflict raised during postsolve()"; \ - } - - // Postsolve for each theory using the statement above - CVC4_FOR_EACH_THEORY; - } catch(const theory::Interrupted&) { - Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl; - } -}/* TheoryEngine::postsolve() */ - - void TheoryEngine::notifyRestart() { // Reset the interrupt flag d_interrupted = false; |