diff options
-rw-r--r-- | src/api/cpp/cvc5.cpp | 3 | ||||
-rw-r--r-- | src/options/smt_options.toml | 11 | ||||
-rw-r--r-- | src/preprocessing/assertion_pipeline.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/quantifier_macros.cpp | 4 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 69 | ||||
-rw-r--r-- | src/prop/proof_cnf_stream.cpp | 68 | ||||
-rw-r--r-- | src/prop/proof_cnf_stream.h | 10 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 3 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 3 | ||||
-rw-r--r-- | src/smt/assertions.cpp | 2 | ||||
-rw-r--r-- | src/smt/proof_manager.cpp | 7 | ||||
-rw-r--r-- | src/smt/proof_manager.h | 18 | ||||
-rw-r--r-- | src/smt/set_defaults.cpp | 58 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 18 | ||||
-rw-r--r-- | src/smt/smt_solver.cpp | 16 | ||||
-rw-r--r-- | src/smt/smt_solver.h | 8 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 |
18 files changed, 200 insertions, 104 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 435597bc7..1c62bd4f0 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -6256,7 +6256,8 @@ std::vector<Term> Solver::getUnsatCore(void) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]) + CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores] + || d_smtEngine->getOptions()[options::unsatCoresNew]) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index c8a1a8fb4..c6e42477b 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -207,12 +207,21 @@ header = "options/smt_options.h" type = "bool" help = "after UNSAT/VALID, produce and check an unsat core (expensive)" +# Temporary option until old unsat cores are removed and this becomes the standard +[[option]] + name = "unsatCoresNew" + category = "regular" + long = "produce-unsat-cores-new" + type = "bool" + help = "turn on unsat core generation using the new proof infrastructure. Note this option is incompatible with the regular unsat cores and with producing proofs." + +# Temporary option until old unsat cores are removed and this becomes the standard [[option]] name = "checkUnsatCoresNew" category = "regular" long = "check-unsat-cores-new" type = "bool" - help = "after UNSAT/VALID, produce and check an unsat core (expensive) using the new proof infrastructure" + help = "after UNSAT/VALID, produce and check an unsat core (expensive) using the new proof infrastructure. Note this option is incompatible with the regular unsat cores and with producing proofs." [[option]] name = "dumpUnsatCores" diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 7d21066d8..43f245656 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -204,7 +204,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg) d_pppg->notifyNewAssert(newConjr, lcp); } } - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]); } diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 068e47f13..a03ac21a3 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -62,7 +62,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) imap[assertions->size()] = newSkolems[j]; assertions->pushBackTrusted(newAsserts[j]); // new assertions have a dependence on the node (old pf architecture) - if (options::unsatCores() && !options::produceProofs()) + if (options::unsatCores()) { ProofManager::currentPM()->addDependence(newAsserts[j].getProven(), assertion); diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 66837267a..952ced4d5 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -86,7 +86,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap) 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() && !options::produceProofs() + if (options::unsatCores() && std::find(macro_assertions.begin(), macro_assertions.end(), assertions[i]) @@ -116,7 +116,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap) // 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() && !options::produceProofs()) + if (options::unsatCores()) { ProofManager::currentPM()->addDependence(curr, assertions[i]); for (unsigned j = 0; j < macro_assertions.size(); j++) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 7a7809eef..8f59ec13b 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -241,7 +241,7 @@ Solver::Solver(cvc5::prop::TheoryProxy* proxy, uncheckedEnqueue(mkLit(varTrue, false)); uncheckedEnqueue(mkLit(varFalse, true)); // FIXME: these should be axioms I believe - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false)); ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true)); @@ -344,7 +344,6 @@ CRef Solver::reason(Var x) { } return vardata[x].d_reason; } - // What's the literal we are trying to explain Lit l = mkLit(x, value(x) != l_True); @@ -428,7 +427,7 @@ CRef Solver::reason(Var x) { // came from (ie. the theory/sharing) Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl; - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); @@ -515,7 +514,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) lemmas.push(); ps.copyTo(lemmas.last()); lemmas_removable.push(removable); - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { // Store the expression being converted to CNF until // the clause is actually created @@ -534,7 +533,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) // construct the clause below to give to the proof manager // as the final conflict. if(falseLiteralsCount == 1) { - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ClauseKind ck = ProofManager::getCnfProof()->getCurrentAssertionKind() @@ -577,7 +576,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) if (options::unsatCores() || isProofEnabled()) { - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ClauseKind ck = ProofManager::getCnfProof()->getCurrentAssertionKind() @@ -593,7 +592,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) } if (ps.size() == falseLiteralsCount) { - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getSatProof()->finalizeProof(cr); } @@ -615,7 +614,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) << std::endl; if (ps.size() == 1) { - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ClauseKind ck = ProofManager::getCnfProof()->getCurrentAssertionKind() @@ -641,7 +640,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) } CRef confl = propagate(CHECK_WITHOUT_THEORY); if(! (ok = (confl == CRef_Undef)) ) { - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { if (ca[confl].size() == 1) { @@ -669,7 +668,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) } return ok; } else { - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { id = ClauseIdUndef; } @@ -716,7 +715,7 @@ void Solver::detachClause(CRef cr, bool strict) { Debug("minisat") << "\n"; } Assert(c.size() > 1); - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getSatProof()->markDeleted(cr); } @@ -998,7 +997,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) int max_resolution_level = 0; // Maximal level of the resolved clauses - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getSatProof()->startResChain(confl); } @@ -1062,7 +1061,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) // FIXME: can we do it lazily if we actually need the proof? if (level(var(q)) == 0) { - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getSatProof()->resolveOutUnit(q); } @@ -1084,7 +1083,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) if (pathC > 0 && confl != CRef_Undef) { - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); } @@ -1124,7 +1123,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) // Literal is not redundant out_learnt[j++] = out_learnt[i]; } else { - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); } @@ -1420,7 +1419,7 @@ void Solver::propagateTheory() { addClause(explanation, true, id); // explainPropagation() pushes the explanation on the assertion // stack in CnfProof, so we need to pop it here. - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getCnfProof()->popCurrentAssertion(); } @@ -1564,7 +1563,7 @@ void Solver::removeSatisfied(vec<CRef>& cs) for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; if (satisfied(c)) { - if (options::unsatCores() && !isProofEnabled() && locked(c)) + if (options::unsatCores() && locked(c)) { // store a resolution of the literal c propagated ProofManager::getSatProof()->storeUnitResolution(c[0]); @@ -1671,7 +1670,7 @@ lbool Solver::search(int nof_conflicts) if (decisionLevel() == 0) { - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getSatProof()->finalizeProof(confl); } @@ -1698,7 +1697,7 @@ lbool Solver::search(int nof_conflicts) if (learnt_clause.size() == 1) { uncheckedEnqueue(learnt_clause[0]); - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getSatProof()->endResChain(learnt_clause[0]); } @@ -1716,7 +1715,7 @@ lbool Solver::search(int nof_conflicts) attachClause(cr); claBumpActivity(ca[cr]); uncheckedEnqueue(learnt_clause[0], cr); - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT); ProofManager::getSatProof()->endResChain(id); @@ -2059,9 +2058,8 @@ void Solver::relocAll(ClauseAllocator& to) { ca.reloc(ws[j].cref, to, - (options::unsatCores() && !isProofEnabled()) - ? ProofManager::getSatProof() - : nullptr); + options::unsatCores() ? ProofManager::getSatProof() + : nullptr); } } @@ -2073,11 +2071,10 @@ void Solver::relocAll(ClauseAllocator& to) if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) { - ca.reloc(vardata[v].d_reason, - to, - (options::unsatCores() && !isProofEnabled()) - ? ProofManager::getSatProof() - : nullptr); + ca.reloc( + vardata[v].d_reason, + to, + options::unsatCores() ? ProofManager::getSatProof() : nullptr); } } // All learnt: @@ -2086,9 +2083,7 @@ void Solver::relocAll(ClauseAllocator& to) { ca.reloc(clauses_removable[i], to, - (options::unsatCores() && !isProofEnabled()) - ? ProofManager::getSatProof() - : nullptr); + options::unsatCores() ? ProofManager::getSatProof() : nullptr); } // All original: // @@ -2096,11 +2091,9 @@ void Solver::relocAll(ClauseAllocator& to) { ca.reloc(clauses_persistent[i], to, - (options::unsatCores() && !isProofEnabled()) - ? ProofManager::getSatProof() - : nullptr); + options::unsatCores() ? ProofManager::getSatProof() : nullptr); } - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getSatProof()->finishUpdateCRef(); } @@ -2270,7 +2263,7 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { TNode cnf_assertion = lemmas_cnf_assertion[j]; @@ -2291,7 +2284,7 @@ CRef Solver::updateLemmas() { // If the lemma is propagating enqueue its literal (or set the conflict) if (conflict == CRef_Undef && value(lemma[0]) != l_True) { if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) { - if (options::unsatCores() && !isProofEnabled() && lemma.size() == 1) + if (options::unsatCores() && lemma.size() == 1) { Node cnf_assertion = lemmas_cnf_assertion[j]; @@ -2311,7 +2304,7 @@ CRef Solver::updateLemmas() { } else { Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl; conflict = CRef_Lazy; - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); } diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index b7d80da76..a15864ad3 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -519,23 +519,33 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn) Node proven = trn.getProven(); Trace("cnf") << "ProofCnfStream::convertPropagation: proven explanation" << proven << "\n"; - Assert(trn.getGenerator()); - Assert(trn.getGenerator()->getProofFor(proven)->isClosed()); - Trace("cnf-steps") << proven << " by explainPropagation " - << trn.identifyGenerator() << std::endl; - d_proof.addLazyStep(proven, - trn.getGenerator(), - PfRule::ASSUME, - true, - "ProofCnfStream::convertPropagation"); + // If we are not producing proofs in the theory engine there is no need to + // keep track in d_proof of the clausification. We still need however to let + // the SAT proof manager know that this clause is an assumption. + bool proofLogging = trn.getGenerator() != nullptr; + if (proofLogging) + { + Assert(trn.getGenerator()->getProofFor(proven)->isClosed()); + Trace("cnf-steps") << proven << " by explainPropagation " + << trn.identifyGenerator() << std::endl; + d_proof.addLazyStep(proven, + trn.getGenerator(), + PfRule::ASSUME, + true, + "ProofCnfStream::convertPropagation"); + } // since the propagation is added directly to the SAT solver via theoryProxy, // do the transformation of the lemma E1 ^ ... ^ En => P into CNF here NodeManager* nm = NodeManager::currentNM(); - Node clauseImpliesElim = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]); - Trace("cnf") << "ProofCnfStream::convertPropagation: adding " - << PfRule::IMPLIES_ELIM << " rule to conclude " - << clauseImpliesElim << "\n"; - d_proof.addStep(clauseImpliesElim, PfRule::IMPLIES_ELIM, {proven}, {}); + Node clauseImpliesElim; + if (proofLogging) + { + clauseImpliesElim = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]); + Trace("cnf") << "ProofCnfStream::convertPropagation: adding " + << PfRule::IMPLIES_ELIM << " rule to conclude " + << clauseImpliesElim << "\n"; + d_proof.addStep(clauseImpliesElim, PfRule::IMPLIES_ELIM, {proven}, {}); + } Node clauseExp; // need to eliminate AND if (proven[0].getKind() == kind::AND) @@ -548,27 +558,33 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn) disjunctsRes.push_back(proven[0][i].notNode()); } disjunctsRes.push_back(proven[1]); - Node clauseAndNeg = nm->mkNode(kind::OR, disjunctsAndNeg); - // add proof steps to convert into clause - d_proof.addStep(clauseAndNeg, PfRule::CNF_AND_NEG, {}, {proven[0]}); clauseExp = nm->mkNode(kind::OR, disjunctsRes); - d_proof.addStep(clauseExp, - PfRule::RESOLUTION, - {clauseAndNeg, clauseImpliesElim}, - {nm->mkConst(true), proven[0]}); + if (proofLogging) + { + // add proof steps to convert into clause + Node clauseAndNeg = nm->mkNode(kind::OR, disjunctsAndNeg); + d_proof.addStep(clauseAndNeg, PfRule::CNF_AND_NEG, {}, {proven[0]}); + d_proof.addStep(clauseExp, + PfRule::RESOLUTION, + {clauseAndNeg, clauseImpliesElim}, + {nm->mkConst(true), proven[0]}); + } } else { - clauseExp = clauseImpliesElim; + clauseExp = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]); } normalizeAndRegister(clauseExp); // consume steps - const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps(); - for (const std::pair<Node, ProofStep>& step : steps) + if (proofLogging) { - d_proof.addStep(step.first, step.second); + const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps(); + for (const std::pair<Node, ProofStep>& step : steps) + { + d_proof.addStep(step.first, step.second); + } + d_psb.clear(); } - d_psb.clear(); } void ProofCnfStream::ensureLiteral(TNode n) diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index d696db580..6299471dd 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -79,12 +79,11 @@ class ProofCnfStream : public ProofGenerator ProofGenerator* pg); /** - * Clausifies the given propagation lemma *without* registering the - * resoluting clause in the SAT solver, as this is handled internally by the - * SAT solver. The clausification steps and the generator within the trust - * node are saved in d_proof. */ + * Clausifies the given propagation lemma *without* registering the resoluting + * clause in the SAT solver, as this is handled internally by the SAT + * solver. The clausification steps and the generator within the trust node + * are saved in d_proof if we are producing proofs in the theory engine. */ void convertPropagation(theory::TrustNode ttn); - /** * Ensure that the given node will have a designated SAT literal that is * definitionally equal to it. The result of this function is that the Node @@ -152,6 +151,7 @@ class ProofCnfStream : public ProofGenerator * above normalizations on all added clauses. */ void normalizeAndRegister(TNode clauseNode); + /** Reference to the underlying cnf stream. */ CnfStream& d_cnfStream; /** The proof manager of underlying SAT solver associated with this stream. */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 4af943537..2eaa3a812 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -246,7 +246,8 @@ void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn, Node node = trn.getNode(); Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl; bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; - Assert(!isProofEnabled() || trn.getGenerator() != nullptr); + Assert(!isProofEnabled() || trn.getGenerator() != nullptr + || options::unsatCores() || options::unsatCoresNew()); assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator()); } diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index bf386fc0e..6ff2af527 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -96,8 +96,9 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { theory::TrustNode tte = d_theoryEngine->getExplanation(lNode); Node theoryExplanation = tte.getNode(); - if (cvc5::options::produceProofs()) + if (options::produceProofs()) { + Assert(options::unsatCoresNew() || tte.getGenerator()); d_propEngine->getProofCnfStream()->convertPropagation(tte); } else if (options::unsatCores()) diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index d873f31bb..aee7a2a86 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -178,7 +178,7 @@ void Assertions::addFormula( } // Give it to the old proof manager - if (options::unsatCores() && !isProofEnabled()) + if (options::unsatCores()) { if (inInput) { // n is an input assertion diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index b06590918..f6c489055 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -131,9 +131,10 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn, Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n"; - // Now make the final scope, which ensures that the only open leaves - // of the proof are the assertions. - d_finalProof = d_pnm->mkScope(pfn, assertions); + // Now make the final scope, which ensures that the only open leaves of the + // proof are the assertions, unless we are doing proofs to generate unsat + // cores, in which case we do not care. + d_finalProof = d_pnm->mkScope(pfn, assertions, !options::unsatCoresNew()); Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n"; } diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index 0345991d2..253dbecaf 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -38,6 +38,24 @@ class ProofPostproccess; /** * This class is responsible for managing the proof output of SmtEngine, as * well as setting up the global proof checker and proof node manager. + * + * The proof production of an SmtEngine is directly impacted by whether, and + * how, we are producing unsat cores: + * + * - If we are producing unsat cores using the old proof infrastructure, then + * SmtEngine will not have proofs in the sense of this proof manager. + * + * - If we are producing unsat cores using this proof infrastructure, then the + * SmtEngine will have proofs using this proof manager (if --produce-proofs + * was not passed by the user it will be activated), but these proofs will + * only cover preprocessing and the prop engine, i.e., the theory engine will + * not have proofs. + * + * - If we are not producing unsat cores then the SmtEngine will have proofs as + * long as --produce-proofs was given. + * + * - If SmtEngine has been configured in a way that is incompatible with proofs + * then unsat core production will be disabled. */ class PfManager { diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 0a8819c4b..cf5fc267b 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -70,13 +70,36 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Notice() << "SmtEngine: setting dumpUnsatCores" << std::endl; options::dumpUnsatCores.set(true); } - if (options::checkUnsatCores() || options::checkUnsatCoresNew() - || options::dumpUnsatCores() || options::unsatAssumptions()) + if ((options::unsatCores() && options::unsatCoresNew()) + || (options::checkUnsatCores() && options::checkUnsatCoresNew())) + { + AlwaysAssert(false) << "Can't have both unsat cores modes, pick one.\n"; + } + if (options::checkUnsatCores()) { - Notice() << "SmtEngine: setting unsatCores" << std::endl; options::unsatCores.set(true); } - if (options::checkProofs() || options::checkUnsatCoresNew() + if (options::checkUnsatCoresNew()) + { + options::unsatCoresNew.set(true); + } + if (options::dumpUnsatCores() || options::unsatAssumptions()) + { + if (!options::unsatCoresNew()) + { + Notice() << "SmtEngine: setting unsatCores" << std::endl; + options::unsatCores.set(true); + } + } + if (options::unsatCoresNew() + && ((options::produceProofs() && options::produceProofs.wasSetByUser()) + || (options::checkProofs() && options::checkProofs.wasSetByUser()) + || (options::dumpProofs() && options::dumpProofs.wasSetByUser()))) + { + AlwaysAssert(false) << "Can't properly produce proofs and have the new " + "unsat cores simultaneously.\n"; + } + if (options::checkProofs() || options::unsatCoresNew() || options::dumpProofs()) { Notice() << "SmtEngine: setting proof" << std::endl; @@ -278,11 +301,21 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // !!! must disable proofs if using the old unsat core infrastructure // TODO (#project 37) remove this - if (options::unsatCores() && !options::checkUnsatCoresNew()) + if (options::unsatCores()) { disableProofs = true; } + // new unsat core specific restrictions for proofs + if (options::unsatCoresNew()) + { + // no fine-graininess + if (!options::proofGranularityMode.wasSetByUser()) + { + options::proofGranularityMode.set(options::ProofGranularityMode::OFF); + } + } + if (options::arraysExp()) { if (!logic.isQuantified()) @@ -335,6 +368,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // if we requiring disabling proofs, disable them now if (disableProofs && options::produceProofs()) { + if (options::unsatCoresNew()) + { + Notice() << "SmtEngine: turning off new unsat cores." << std::endl; + } + options::unsatCoresNew.set(false); + options::checkUnsatCoresNew.set(false); if (options::produceProofs()) { Notice() << "SmtEngine: turning off produce-proofs." << std::endl; @@ -366,7 +405,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // Disable options incompatible with incremental solving, unsat cores or // output an error if enabled explicitly. It is also currently incompatible // with arithmetic, force the option off. - if (options::incrementalSolving() || options::unsatCores()) + if (options::incrementalSolving() || options::unsatCores() + || options::unsatCoresNew()) { if (options::unconstrainedSimp()) { @@ -428,7 +468,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // Disable options incompatible with unsat cores or output an error if enabled // explicitly - if (options::unsatCores()) + if (options::unsatCores() || options::unsatCoresNew()) { if (options::simplificationMode() != options::SimplificationMode::NONE) { @@ -707,7 +747,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified() && !options::incrementalSolving() - && !options::unsatCores(); + && !options::unsatCores() && !options::unsatCoresNew(); Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc << std::endl; options::ufSymmetryBreaker.set(qf_uf_noinc); @@ -756,7 +796,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) && (logic.isTheoryEnabled(THEORY_ARRAYS) && logic.isTheoryEnabled(THEORY_UF) && logic.isTheoryEnabled(THEORY_BV)) - && !options::unsatCores(); + && !options::unsatCores() && !options::unsatCoresNew(); Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl; options::repeatSimp.set(repeatSimp); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3eedfdf53..3d38ba37b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -236,7 +236,10 @@ void SmtEngine::finishInit() } Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; - d_smtSolver->finishInit(logic); + // if proofs and unsat cores, proofs are used solely for unsat core + // production, so we don't generate proofs in the theory engine, which is + // communicated via the second argument + d_smtSolver->finishInit(logic, options::unsatCoresNew()); // now can construct the SMT-level model object TheoryEngine* te = d_smtSolver->getTheoryEngine(); @@ -1408,10 +1411,11 @@ StatisticsRegistry& SmtEngine::getStatisticsRegistry() UnsatCore SmtEngine::getUnsatCoreInternal() { - if (!options::unsatCores()) + if (!options::unsatCores() && !options::unsatCoresNew()) { throw ModalException( - "Cannot get an unsat core when produce-unsat-cores option is off."); + "Cannot get an unsat core when produce-unsat-cores[-new] option is " + "off."); } if (d_state->getMode() != SmtMode::UNSAT) { @@ -1437,7 +1441,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal() } void SmtEngine::checkUnsatCore() { - Assert(options::unsatCores()) + Assert(options::unsatCores() || options::unsatCoresNew()) << "cannot check unsat core if unsat cores are turned off"; Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; @@ -1449,7 +1453,10 @@ void SmtEngine::checkUnsatCore() { coreChecker->getOptions().set(options::checkUnsatCores, false); // disable all proof options coreChecker->getOptions().set(options::produceProofs, false); + coreChecker->getOptions().set(options::checkProofs, false); coreChecker->getOptions().set(options::checkUnsatCoresNew, false); + coreChecker->getOptions().set(options::proofEagerChecking, false); + // set up separation logic heap if necessary TypeNode sepLocType, sepDataType; if (getSepHeapTypes(sepLocType, sepDataType)) @@ -1633,7 +1640,8 @@ void SmtEngine::getInstantiationTermVectors( { SmtScope smts(this); finishInit(); - if (options::produceProofs() && getSmtMode() == SmtMode::UNSAT) + if (options::produceProofs() && !options::unsatCoresNew() + && getSmtMode() == SmtMode::UNSAT) { // minimize instantiations based on proof manager getRelevantInstantiationTermVectors(insts); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index ceec0619b..2847e5ee9 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -49,16 +49,18 @@ SmtSolver::SmtSolver(SmtEngine& smt, SmtSolver::~SmtSolver() {} -void SmtSolver::finishInit(const LogicInfo& logicInfo) +void SmtSolver::finishInit(const LogicInfo& logicInfo, + bool proofForUnsatCoreMode) { // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) - d_theoryEngine.reset(new TheoryEngine(d_smt.getContext(), - d_smt.getUserContext(), - d_rm, - logicInfo, - d_smt.getOutputManager(), - d_pnm)); + d_theoryEngine.reset( + new TheoryEngine(d_smt.getContext(), + d_smt.getUserContext(), + d_rm, + logicInfo, + d_smt.getOutputManager(), + proofForUnsatCoreMode ? nullptr : d_pnm)); // Add the theories for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index e4493eedf..ae1cc2e40 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -71,8 +71,13 @@ class SmtSolver ~SmtSolver(); /** * Create theory engine, prop engine based on the logic info. + * + * @param logicInfo the logic information + * @param proofForUnsatCoreMode whether this SmtSolver will operate in unsat + * core mode. If true, proofs will not be produced in the theory engine. */ - void finishInit(const LogicInfo& logicInfo); + void finishInit(const LogicInfo& logicInfo, + bool proofForUnsatCoreMode = false); /** Reset all assertions, global declarations, etc. */ void resetAssertions(); /** @@ -129,6 +134,7 @@ class SmtSolver /** Get a pointer to the preprocessor */ Preprocessor* getPreprocessor(); //------------------------------------------ end access methods + private: /** Reference to the parent SMT engine */ SmtEngine& d_smt; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9f0e3eb82..79f9c660f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1784,7 +1784,7 @@ theory::TrustNode TheoryEngine::getExplanation( return trn; } - return theory::TrustNode::mkTrustLemma(expNode, nullptr); + return theory::TrustNode::mkTrustPropExp(conclusion, expNode, nullptr); } bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; } |