This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly.
This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.
{
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)
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"
d_pppg->notifyNewAssert(newConjr, lcp);
}
}
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]);
}
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);
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])
// 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++)
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));
}
return vardata[x].d_reason;
}
-
// What's the literal we are trying to explain
Lit l = mkLit(x, value(x) != l_True);
// 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);
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
// 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()
if (options::unsatCores() || isProofEnabled())
{
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
ClauseKind ck =
ProofManager::getCnfProof()->getCurrentAssertionKind()
}
if (ps.size() == falseLiteralsCount)
{
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
ProofManager::getSatProof()->finalizeProof(cr);
}
<< std::endl;
if (ps.size() == 1)
{
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
ClauseKind ck =
ProofManager::getCnfProof()->getCurrentAssertionKind()
}
CRef confl = propagate(CHECK_WITHOUT_THEORY);
if(! (ok = (confl == CRef_Undef)) ) {
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
if (ca[confl].size() == 1)
{
}
return ok;
} else {
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
id = ClauseIdUndef;
}
Debug("minisat") << "\n";
}
Assert(c.size() > 1);
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
ProofManager::getSatProof()->markDeleted(cr);
}
int max_resolution_level = 0; // Maximal level of the resolved clauses
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
ProofManager::getSatProof()->startResChain(confl);
}
// 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);
}
if (pathC > 0 && confl != CRef_Undef)
{
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
}
// Literal is not redundant
out_learnt[j++] = out_learnt[i];
} else {
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
}
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();
}
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]);
if (decisionLevel() == 0)
{
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
ProofManager::getSatProof()->finalizeProof(confl);
}
if (learnt_clause.size() == 1)
{
uncheckedEnqueue(learnt_clause[0]);
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
ProofManager::getSatProof()->endResChain(learnt_clause[0]);
}
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);
{
ca.reloc(ws[j].cref,
to,
- (options::unsatCores() && !isProofEnabled())
- ? ProofManager::getSatProof()
- : nullptr);
+ options::unsatCores() ? ProofManager::getSatProof()
+ : nullptr);
}
}
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:
{
ca.reloc(clauses_removable[i],
to,
- (options::unsatCores() && !isProofEnabled())
- ? ProofManager::getSatProof()
- : nullptr);
+ options::unsatCores() ? ProofManager::getSatProof() : nullptr);
}
// All original:
//
{
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();
}
}
lemma_ref = ca.alloc(clauseLevel, lemma, removable);
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
TNode cnf_assertion = lemmas_cnf_assertion[j];
// 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];
} 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);
}
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)
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)
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
* 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. */
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());
}
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())
}
// Give it to the old proof manager
- if (options::unsatCores() && !isProofEnabled())
+ if (options::unsatCores())
{
if (inInput)
{ // n is an input assertion
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";
}
/**
* 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
{
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;
}
// !!! 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())
// 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;
// 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())
{
// 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)
{
{
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);
&& (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);
}
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();
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)
{
}
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;
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))
{
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);
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;
~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();
/**
/** Get a pointer to the preprocessor */
Preprocessor* getPreprocessor();
//------------------------------------------ end access methods
+
private:
/** Reference to the parent SMT engine */
SmtEngine& d_smt;
return trn;
}
- return theory::TrustNode::mkTrustLemma(expNode, nullptr);
+ return theory::TrustNode::mkTrustPropExp(conclusion, expNode, nullptr);
}
bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }
projects / cvc5.git / commitdiff