diff options
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r-- | src/preprocessing/passes/apply_substs.cpp | 42 | ||||
-rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 4 | ||||
-rw-r--r-- | src/preprocessing/passes/ite_simp.cpp | 8 | ||||
-rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 10 | ||||
-rw-r--r-- | src/preprocessing/passes/non_clausal_simp.cpp | 18 | ||||
-rw-r--r-- | src/preprocessing/passes/quantifier_macros.cpp | 4 |
6 files changed, 27 insertions, 59 deletions
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 92f31b0b8..c93895e79 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -33,32 +33,28 @@ ApplySubsts::ApplySubsts(PreprocessingPassContext* preprocContext) PreprocessingPassResult ApplySubsts::applyInternal( AssertionPipeline* assertionsToPreprocess) { - if (!options::unsatCores()) - { - Chat() << "applying substitutions..." << std::endl; - Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): " - << "applying substitutions" << std::endl; - // TODO(#1255): Substitutions in incremental mode should be managed with a - // proper data structure. + Chat() << "applying substitutions..." << std::endl; + Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): " + << "applying substitutions" << std::endl; + // TODO(#1255): Substitutions in incremental mode should be managed with a + // proper data structure. - theory::TrustSubstitutionMap& tlsm = - d_preprocContext->getTopLevelSubstitutions(); - unsigned size = assertionsToPreprocess->size(); - for (unsigned i = 0; i < size; ++i) + theory::TrustSubstitutionMap& tlsm = + d_preprocContext->getTopLevelSubstitutions(); + unsigned size = assertionsToPreprocess->size(); + for (unsigned i = 0; i < size; ++i) + { + if (assertionsToPreprocess->isSubstsIndex(i)) { - if (assertionsToPreprocess->isSubstsIndex(i)) - { - continue; - } - Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i] - << std::endl; - d_preprocContext->spendResource( - ResourceManager::Resource::PreprocessStep); - assertionsToPreprocess->replaceTrusted( - i, tlsm.apply((*assertionsToPreprocess)[i])); - Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i] - << std::endl; + continue; } + Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i] + << std::endl; + d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + assertionsToPreprocess->replaceTrusted( + i, tlsm.apply((*assertionsToPreprocess)[i])); + Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i] + << std::endl; } return PreprocessingPassResult::NO_CONFLICT; } diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index d2f053379..91af2a5b8 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -50,7 +50,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) // process assertions->replaceTrusted(i, trn); // rewritten assertion has a dependence on the node (old pf architecture) - if (options::unsatCores()) + if (options::unsatCores() && !options::proofNew()) { ProofManager::currentPM()->addDependence(trn.getNode(), assertion); } @@ -61,7 +61,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) imap[newSkolems[j]] = assertions->size(); assertions->pushBackTrusted(newAsserts[j]); // new assertions have a dependence on the node (old pf architecture) - if (options::unsatCores()) + if (options::unsatCores() && !options::proofNew()) { ProofManager::currentPM()->addDependence(newAsserts[j].getProven(), assertion); diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 5568dcad0..746bf33bd 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -114,13 +114,7 @@ ITESimp::Statistics::~Statistics() bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) { - // This pass does not support dependency tracking yet - // (learns substitutions from all assertions so just - // adding addDependence is not enough) - if (options::unsatCores()) - { - return true; - } + Assert(!options::unsatCores()); bool result = true; bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic(); if (simpDidALotOfWork) 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(); diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 7ace55c0a..656822299 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -66,7 +66,8 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext) PreprocessingPassResult NonClausalSimp::applyInternal( AssertionPipeline* assertionsToPreprocess) { - Assert(!options::unsatCores()); + Assert(!options::unsatCores() || isProofEnabled()) + << "Unsat cores with non-clausal simp only supported with new proofs"; d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); @@ -111,13 +112,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal( // If in conflict, just return false Trace("non-clausal-simplify") << "conflict in non-clausal propagation" << std::endl; - Assert(!options::unsatCores()); assertionsToPreprocess->clear(); assertionsToPreprocess->pushBackTrusted(conf); - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(conf.getNode(), Node::null()); - } propagator->setNeedsFinish(true); return PreprocessingPassResult::CONFLICT; } @@ -177,14 +173,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal( // If the learned literal simplifies to false, we're in conflict Trace("non-clausal-simplify") << "conflict with " << learned_literals[i].getNode() << std::endl; - Assert(!options::unsatCores()); assertionsToPreprocess->clear(); Node n = NodeManager::currentNM()->mkConst<bool>(false); assertionsToPreprocess->push_back(n, false, false, d_llpg.get()); - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(n, Node::null()); - } propagator->setNeedsFinish(true); return PreprocessingPassResult::CONFLICT; } @@ -216,14 +207,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal( // If in conflict, we return false Trace("non-clausal-simplify") << "conflict while solving " << learnedLiteral << std::endl; - Assert(!options::unsatCores()); assertionsToPreprocess->clear(); Node n = NodeManager::currentNM()->mkConst<bool>(false); assertionsToPreprocess->push_back(n); - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(n, Node::null()); - } propagator->setNeedsFinish(true); return PreprocessingPassResult::CONFLICT; } diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 604f8719c..028bfede5 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -80,7 +80,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite) for( int i=0; i<(int)assertions.size(); i++ ){ Trace("macros-debug") << " process assertion " << assertions[i] << std::endl; if( processAssertion( assertions[i] ) ){ - if (options::unsatCores() + if (options::unsatCores() && !options::proofNew() && std::find(macro_assertions.begin(), macro_assertions.end(), assertions[i]) @@ -106,7 +106,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite) // is an over-approximation. a more fine-grained unsat core // computation would require caching dependencies for each subterm of // the formula, which is expensive. - if (options::unsatCores()) + if (options::unsatCores() && !options::proofNew()) { ProofManager::currentPM()->addDependence(curr, assertions[i]); for (unsigned j = 0; j < macro_assertions.size(); j++) |