summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cpp/cvc5.cpp3
-rw-r--r--src/options/smt_options.toml11
-rw-r--r--src/preprocessing/assertion_pipeline.cpp2
-rw-r--r--src/preprocessing/passes/ite_removal.cpp2
-rw-r--r--src/preprocessing/passes/quantifier_macros.cpp4
-rw-r--r--src/prop/minisat/core/Solver.cc69
-rw-r--r--src/prop/proof_cnf_stream.cpp68
-rw-r--r--src/prop/proof_cnf_stream.h10
-rw-r--r--src/prop/prop_engine.cpp3
-rw-r--r--src/prop/theory_proxy.cpp3
-rw-r--r--src/smt/assertions.cpp2
-rw-r--r--src/smt/proof_manager.cpp7
-rw-r--r--src/smt/proof_manager.h18
-rw-r--r--src/smt/set_defaults.cpp58
-rw-r--r--src/smt/smt_engine.cpp18
-rw-r--r--src/smt/smt_solver.cpp16
-rw-r--r--src/smt/smt_solver.h8
-rw-r--r--src/theory/theory_engine.cpp2
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; }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback