diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-12-24 01:15:40 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-24 01:15:40 -0300 |
commit | e0dfc0a343dfd330f9c8d2a5c1ebd21146366ca9 (patch) | |
tree | 4602faa1f16a2548fe27ad1e7ea6a6a28bec4ee7 /src/preprocessing/passes/miplib_trick.cpp | |
parent | a539b63c369544ed08a1fa7fa4c8e3d437be3766 (diff) |
[proof-new] Only use old proofs for unsat cores if no proof new (#5725)
Now the old proofs are used for unsat cores only if proofNew is disabled. Later commits will generate unsat cores from the new proofs when requested. Eventually we will compare them and when we confirm the new unsat core generation is better we will delete the old one.
This also does some minor refactoring in some preprocessing. No behavior is changed.
Diffstat (limited to 'src/preprocessing/passes/miplib_trick.cpp')
-rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 4ed2aede9..0bb386697 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -180,6 +180,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( Assert(assertionsToPreprocess->getRealAssertionsEnd() == assertionsToPreprocess->size()); Assert(!options::incrementalSolving()); + Assert(!options::unsatCores()); context::Context fakeContext; TheoryEngine* te = d_preprocContext->getTheoryEngine(); @@ -527,10 +528,6 @@ PreprocessingPassResult MipLibTrick::applyInternal( Node n = Rewriter::rewrite(geq.andNode(leq)); assertionsToPreprocess->push_back(n); - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(n, Node::null()); - } TrustSubstitutionMap tnullMap(&fakeContext, nullptr); CVC4_UNUSED SubstitutionMap& nullMap = tnullMap.get(); Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions @@ -599,11 +596,6 @@ PreprocessingPassResult MipLibTrick::applyInternal( Debug("miplib") << " " << newAssertion << endl; assertionsToPreprocess->push_back(newAssertion); - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(newAssertion, - Node::null()); - } Debug("miplib") << " assertions to remove: " << endl; for (vector<TNode>::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); |