diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-09 16:07:30 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-09 22:07:30 +0000 |
| commit | 6808152d40b0b4293816c18a8ddf83df2afc39f7 (patch) | |
| tree | 429c816c274bf825f9ba765941991c0a2d1b14d0 /src/preprocessing/passes | |
| parent | dd92b4235e0a74b08ba02c0af11833bad27335ad (diff) | |
Remove logic request (#6089)
This removes use of the logic request utility.
It generally bad practice to change the logic dynamically, e.g. during preprocessing, since it makes it so that CVC4 does not properly initialize. We now insist that logic is changed upfront in set_defaults.
This is in preparation for the smt::Env class, which will change the ownership of logic.
Diffstat (limited to 'src/preprocessing/passes')
| -rw-r--r-- | src/preprocessing/passes/bv_abstraction.cpp | 8 | ||||
| -rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 1 |
2 files changed, 1 insertions, 8 deletions
diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp index e9197754b..539cc3b36 100644 --- a/src/preprocessing/passes/bv_abstraction.cpp +++ b/src/preprocessing/passes/bv_abstraction.cpp @@ -49,17 +49,11 @@ PreprocessingPassResult BvAbstraction::applyInternal( assertionsToPreprocess->end()); TheoryEngine* te = d_preprocContext->getTheoryEngine(); bv::TheoryBV* bv_theory = static_cast<bv::TheoryBV*>(te->theoryOf(THEORY_BV)); - bool changed = bv_theory->applyAbstraction(assertions, new_assertions); + bv_theory->applyAbstraction(assertions, new_assertions); for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i])); } - // If we are using the lazy solver and the abstraction applies, then UF - // symbols were introduced. - if (options::bitblastMode() == options::BitblastMode::LAZY && changed) - { - d_preprocContext->widenLogic(theory::THEORY_UF); - } return PreprocessingPassResult::NO_CONFLICT; } diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 56a4448da..f6ae77bc2 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -555,7 +555,6 @@ PreprocessingPassResult MipLibTrick::applyInternal( { newVars.push_back(varRef); } - d_preprocContext->enableIntegers(); } Node sum; if (pos.getKind() == kind::AND) |