This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:
the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.
{
CVC5_API_TRY_CATCH_BEGIN;
NodeManagerScope scope(getNodeManager());
- CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]
- || d_smtEngine->getOptions()[options::unsatCoresNew])
+ CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores])
<< "Cannot get unsat core unless explicitly enabled "
"(try --produce-unsat-cores)";
CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
help = "turn on unsat core generation"
[[option]]
- name = "checkUnsatCores"
- category = "regular"
- long = "check-unsat-cores"
- 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"
+ name = "unsatCoresMode"
+ smt_name = "unsat-cores-mode"
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."
+ long = "unsat-cores-mode=MODE"
+ type = "UnsatCoresMode"
+ default = "OFF"
+ help = "choose unsat core mode, see --unsat-cores-mode=help"
+ help_mode = "unsat cores modes."
+[[option.mode.OFF]]
+ name = "off"
+ help = "Do not produce unsat cores."
+[[option.mode.OLD_PROOF]]
+ name = "old-proof"
+ help = "Produce unsat cores from old proof infrastructure."
+[[option.mode.SAT_PROOF]]
+ name = "sat-proof"
+ help = "Produce unsat cores from SAT and preprocessing proofs."
+[[option.mode.FULL_PROOF]]
+ name = "full-proof"
+ help = "Produce unsat cores from full proofs."
+[[option.mode.ASSUMPTIONS]]
+ name = "assumptions"
+ help = "Produce unsat cores using solving under assumptions and preprocessing proofs."
-# Temporary option until old unsat cores are removed and this becomes the standard
[[option]]
- name = "checkUnsatCoresNew"
+ name = "checkUnsatCores"
category = "regular"
- long = "check-unsat-cores-new"
+ long = "check-unsat-cores"
type = "bool"
- 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."
+ help = "after UNSAT/VALID, produce and check an unsat core (expensive)"
[[option]]
name = "dumpUnsatCores"
{
d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
}
- else if (options::unsatCores())
+ else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::currentPM()->addDependence(n, d_nodes[i]);
}
d_pppg->notifyNewAssert(newConjr, lcp);
}
}
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
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())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
assertion);
bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
{
- Assert(!options::unsatCores());
+ Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF);
bool result = true;
bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
if (simpDidALotOfWork)
Assert(assertionsToPreprocess->getRealAssertionsEnd()
== assertionsToPreprocess->size());
Assert(!options::incrementalSolving());
- Assert(!options::unsatCores());
+ Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF);
context::Context fakeContext;
TheoryEngine* te = d_preprocContext->getTheoryEngine();
PreprocessingPassResult NonClausalSimp::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- Assert(!options::unsatCores() || isProofEnabled())
- << "Unsat cores with non-clausal simp only supported with new proofs";
+ Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
+ || isProofEnabled())
+ << "Unsat cores with non-clausal simp only supported with new proofs. "
+ "Cores mode is "
+ << options::unsatCoresMode() << "\n";
d_preprocContext->spendResource(Resource::PreprocessStep);
imap[assertions->size()] = newSkolems[j];
assertions->pushBackTrusted(newAsserts[j]);
// new assertions have a dependence on the node (old pf architecture)
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
assertion);
}
void ProofManager::traceUnsatCore() {
- Assert(options::unsatCores());
+ Assert(options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF);
d_satProof->refreshProof();
IdToSatClause used_lemmas;
IdToSatClause used_inputs;
void ProofManager::getLemmasInUnsatCore(std::vector<Node>& lemmas)
{
- Assert(options::unsatCores())
+ Assert(options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
<< "Cannot compute unsat core when proofs are off";
Assert(unsatCoreAvailable())
<< "Cannot get unsat core at this time. Mabye the input is SAT?";
d_pfManager.reset(
new SatProofManager(this, proxy->getCnfStream(), userContext, pnm));
}
- else if (options::unsatCores())
+ else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::currentPM()->initSatProof(this);
}
uncheckedEnqueue(mkLit(varTrue, false));
uncheckedEnqueue(mkLit(varFalse, true));
// FIXME: these should be axioms I believe
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
// came from (ie. the theory/sharing)
Trace("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)"
<< std::endl;
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ClauseId id = ProofManager::getSatProof()->registerClause(real_reason,
THEORY_LEMMA);
lemmas.push();
ps.copyTo(lemmas.last());
lemmas_removable.push(removable);
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
// 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())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ClauseKind ck =
ProofManager::getCnfProof()->getCurrentAssertionKind()
if (options::unsatCores() || isProofEnabled())
{
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ClauseKind ck =
ProofManager::getCnfProof()->getCurrentAssertionKind()
}
if (ps.size() == falseLiteralsCount)
{
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getSatProof()->finalizeProof(cr);
}
<< std::endl;
if (ps.size() == 1)
{
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ClauseKind ck =
ProofManager::getCnfProof()->getCurrentAssertionKind()
}
CRef confl = propagate(CHECK_WITHOUT_THEORY);
if(! (ok = (confl == CRef_Undef)) ) {
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
if (ca[confl].size() == 1)
{
}
return ok;
} else {
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
id = ClauseIdUndef;
}
Debug("minisat") << "\n";
}
Assert(c.size() > 1);
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getSatProof()->markDeleted(cr);
}
int max_resolution_level = 0; // Maximal level of the resolved clauses
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getSatProof()->startResChain(confl);
}
// FIXME: can we do it lazily if we actually need the proof?
if (level(var(q)) == 0)
{
- if (options::unsatCores())
+ if (options::unsatCoresMode()
+ == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getSatProof()->resolveOutUnit(q);
}
if (pathC > 0 && confl != CRef_Undef)
{
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
}
// Literal is not redundant
out_learnt[j++] = out_learnt[i];
} else {
- if (options::unsatCores())
+ if (options::unsatCoresMode()
+ == options::UnsatCoresMode::OLD_PROOF)
{
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())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getCnfProof()->popCurrentAssertion();
}
for (i = j = 0; i < cs.size(); i++){
Clause& c = ca[cs[i]];
if (satisfied(c)) {
- if (options::unsatCores() && locked(c))
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+ && locked(c))
{
// store a resolution of the literal c propagated
ProofManager::getSatProof()->storeUnitResolution(c[0]);
if (decisionLevel() == 0)
{
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getSatProof()->finalizeProof(confl);
}
if (learnt_clause.size() == 1)
{
uncheckedEnqueue(learnt_clause[0]);
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getSatProof()->endResChain(learnt_clause[0]);
}
attachClause(cr);
claBumpActivity(ca[cr]);
uncheckedEnqueue(learnt_clause[0], cr);
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
ProofManager::getSatProof()->endResChain(id);
{
ca.reloc(ws[j].cref,
to,
- options::unsatCores() ? ProofManager::getSatProof()
- : nullptr);
+ options::unsatCoresMode()
+ == options::UnsatCoresMode::OLD_PROOF
+ ? ProofManager::getSatProof()
+ : nullptr);
}
}
ca.reloc(
vardata[v].d_reason,
to,
- options::unsatCores() ? ProofManager::getSatProof() : nullptr);
+ options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+ ? ProofManager::getSatProof()
+ : nullptr);
}
}
// All learnt:
{
ca.reloc(clauses_removable[i],
to,
- options::unsatCores() ? ProofManager::getSatProof() : nullptr);
+ options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+ ? ProofManager::getSatProof()
+ : nullptr);
}
// All original:
//
{
ca.reloc(clauses_persistent[i],
to,
- options::unsatCores() ? ProofManager::getSatProof() : nullptr);
+ options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+ ? ProofManager::getSatProof()
+ : nullptr);
}
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getSatProof()->finishUpdateCRef();
}
}
lemma_ref = ca.alloc(clauseLevel, lemma, removable);
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
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() && lemma.size() == 1)
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF
+ && 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())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
}
d_ppm.reset(
new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get()));
}
- else if (options::unsatCores())
+ else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
}
Node node = trn.getNode();
Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl;
bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
- Assert(!isProofEnabled() || trn.getGenerator() != nullptr
- || options::unsatCores() || options::unsatCoresNew());
+ Assert(
+ !isProofEnabled() || trn.getGenerator() != nullptr
+ || options::unsatCores()
+ || (options::unsatCores()
+ && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF));
assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
}
Node theoryExplanation = tte.getNode();
if (options::produceProofs())
{
- Assert(options::unsatCoresNew() || tte.getGenerator());
+ Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF
+ || tte.getGenerator());
d_propEngine->getProofCnfStream()->convertPropagation(tte);
}
- else if (options::unsatCores())
+ else if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
}
}
// Give it to the old proof manager
- if (options::unsatCores())
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
if (inInput)
{ // n is an input assertion
// 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());
+ d_finalProof = d_pnm->mkScope(pfn, assertions, !options::unsatCores());
Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
}
* 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.
+ * SmtEngine will have proofs using this proof manager, according to the unsat
+ * core mode:
+ *
+ * - assumption mode: proofs only for preprocessing, not in sat solver or
+ * theory engine, and level of granularity set to off (unless otherwise
+ * specified by the user)
+ *
+ * - sat-proof mode: proofs for preprocessing + sat solver, not in theory
+ * engine and level of granularity set to off (unless otherwise specified by
+ * the user)
+ *
+ * - full-proof mode: proofs for the whole solver as normal
+ *
+ * Note that if --produce-proofs is set then full-proof mode of unsat cores is
+ * forced.
*
* - If we are not producing unsat cores then the SmtEngine will have proofs as
- * long as --produce-proofs was given.
+ * long as --produce-proofs is on.
*
* - If SmtEngine has been configured in a way that is incompatible with proofs
* then unsat core production will be disabled.
// implied options
if (options::debugCheckModels())
{
- Notice() << "SmtEngine: setting checkModel" << std::endl;
options::checkModels.set(true);
}
if (options::checkModels() || options::dumpModels())
{
- Notice() << "SmtEngine: setting produceModels" << std::endl;
options::produceModels.set(true);
}
if (options::checkModels())
{
- Notice() << "SmtEngine: setting produceAssignments" << std::endl;
options::produceAssignments.set(true);
}
+ // unsat cores and proofs shenanigans
if (options::dumpUnsatCoresFull())
{
- Notice() << "SmtEngine: setting dumpUnsatCores" << std::endl;
options::dumpUnsatCores.set(true);
}
- if ((options::unsatCores() && options::unsatCoresNew())
- || (options::checkUnsatCores() && options::checkUnsatCoresNew()))
+ if (options::checkUnsatCores() || options::dumpUnsatCores()
+ || options::unsatAssumptions())
{
- AlwaysAssert(false) << "Can't have both unsat cores modes, pick one.\n";
+ options::unsatCores.set(true);
}
- if (options::checkUnsatCores())
+
+ if (options::unsatCores()
+ && options::unsatCoresMode() == options::UnsatCoresMode::OFF)
{
- options::unsatCores.set(true);
+ if (options::unsatCoresMode.wasSetByUser())
+ {
+ Notice()
+ << "Overriding OFF unsat-core mode since cores were requested..\n";
+ }
+ options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF);
}
- if (options::checkUnsatCoresNew())
+
+ if (options::checkProofs() || options::dumpProofs())
{
- options::unsatCoresNew.set(true);
+ options::produceProofs.set(true);
}
- if (options::dumpUnsatCores() || options::unsatAssumptions())
+
+ if (options::produceProofs()
+ && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
{
- if (!options::unsatCoresNew())
+ if (options::unsatCoresMode.wasSetByUser())
{
- Notice() << "SmtEngine: setting unsatCores" << std::endl;
- options::unsatCores.set(true);
+ Notice() << "Forcing full-proof mode for unsat cores mode since proofs "
+ "were requested.\n";
}
+ options::unsatCoresMode.set(options::UnsatCoresMode::FULL_PROOF);
}
- if (options::unsatCoresNew()
- && ((options::produceProofs() && options::produceProofs.wasSetByUser())
- || (options::checkProofs() && options::checkProofs.wasSetByUser())
- || (options::dumpProofs() && options::dumpProofs.wasSetByUser())))
+
+ // set proofs on if not yet set
+ if (options::unsatCores() && !options::produceProofs()
+ && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF)
{
- AlwaysAssert(false) << "Can't properly produce proofs and have the new "
- "unsat cores simultaneously.\n";
+ if (options::produceProofs.wasSetByUser())
+ {
+ Notice()
+ << "Forcing proof production since new unsat cores were requested.\n";
+ }
+ options::produceProofs.set(true);
}
- if (options::checkProofs() || options::unsatCoresNew()
- || options::dumpProofs())
+
+ // guarantee that if unsat cores mode is not OFF, then they are activated
+ if (!options::unsatCores())
{
- Notice() << "SmtEngine: setting proof" << std::endl;
- options::produceProofs.set(true);
+ if (options::unsatCoresMode.wasSetByUser())
+ {
+ Notice() << "Overriding unsat-core mode for OFF since cores were not "
+ "requested.\n";
+ }
+ options::unsatCoresMode.set(options::UnsatCoresMode::OFF);
}
+
+ // whether we want to force safe unsat cores, i.e., if we are in the OLD_PROOF
+ // unsat core mode, since new ones are experimental
+ bool safeUnsatCores =
+ options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF;
+
if (options::bitvectorAigSimplifications.wasSetByUser())
{
Notice() << "SmtEngine: setting bitvectorAig" << std::endl;
// formulas is unsat. Thus, proofs do not apply.
disableProofs = true;
}
- // !!! must disable proofs if using the old unsat core infrastructure
- // TODO (#project 37) remove this
- if (options::unsatCores())
- {
- disableProofs = true;
- }
// new unsat core specific restrictions for proofs
- if (options::unsatCoresNew())
+ if (options::unsatCores()
+ && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
+ && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
{
// no fine-graininess
if (!options::proofGranularityMode.wasSetByUser())
// if we requiring disabling proofs, disable them now
if (disableProofs && options::produceProofs())
{
- if (options::unsatCoresNew())
+ if (options::unsatCoresMode() != options::UnsatCoresMode::OFF
+ && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF)
{
- Notice() << "SmtEngine: turning off new unsat cores." << std::endl;
+ Notice() << "SmtEngine: reverting to old unsat cores since proofs are "
+ "disabled.\n";
+ options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF);
}
- options::unsatCoresNew.set(false);
- options::checkUnsatCoresNew.set(false);
if (options::produceProofs())
{
Notice() << "SmtEngine: turning off produce-proofs." << std::endl;
if (options::sygusCoreConnective())
{
options::unsatCores.set(true);
+ if (options::unsatCoresMode() == options::UnsatCoresMode::OFF)
+ {
+ options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF);
+ }
}
if ((options::checkModels() || options::checkSynthSol()
// 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()
- || options::unsatCoresNew())
+ if (options::incrementalSolving() || safeUnsatCores)
{
if (options::unconstrainedSimp())
{
if (options::unconstrainedSimp.wasSetByUser())
{
throw OptionException(
- "unconstrained simplification not supported with unsat "
+ "unconstrained simplification not supported with old unsat "
"cores/incremental solving");
}
Notice() << "SmtEngine: turning off unconstrained simplification to "
- "support unsat cores/incremental solving"
+ "support old unsat cores/incremental solving"
<< std::endl;
options::unconstrainedSimp.set(false);
}
// Disable options incompatible with unsat cores or output an error if enabled
// explicitly
- if (options::unsatCores() || options::unsatCoresNew())
+ if (safeUnsatCores)
{
if (options::simplificationMode() != options::SimplificationMode::NONE)
{
if (options::simplificationMode.wasSetByUser())
{
- throw OptionException("simplification not supported with unsat cores");
+ throw OptionException(
+ "simplification not supported with old unsat cores");
}
Notice() << "SmtEngine: turning off simplification to support unsat "
"cores"
if (options::pbRewrites.wasSetByUser())
{
throw OptionException(
- "pseudoboolean rewrites not supported with unsat cores");
+ "pseudoboolean rewrites not supported with old unsat cores");
}
Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
- "unsat cores"
- << std::endl;
+ "old unsat cores\n";
options::pbRewrites.set(false);
}
{
if (options::sortInference.wasSetByUser())
{
- throw OptionException("sort inference not supported with unsat cores");
+ throw OptionException(
+ "sort inference not supported with old unsat cores");
}
- Notice() << "SmtEngine: turning off sort inference to support unsat "
- "cores"
- << std::endl;
+ Notice() << "SmtEngine: turning off sort inference to support old unsat "
+ "cores\n";
options::sortInference.set(false);
}
if (options::preSkolemQuant.wasSetByUser())
{
throw OptionException(
- "pre-skolemization not supported with unsat cores");
+ "pre-skolemization not supported with old unsat cores");
}
- Notice() << "SmtEngine: turning off pre-skolemization to support unsat "
- "cores"
- << std::endl;
+ Notice() << "SmtEngine: turning off pre-skolemization to support old "
+ "unsat cores\n";
options::preSkolemQuant.set(false);
}
-
if (options::bitvectorToBool())
{
if (options::bitvectorToBool.wasSetByUser())
{
- throw OptionException("bv-to-bool not supported with unsat cores");
+ throw OptionException("bv-to-bool not supported with old unsat cores");
}
- Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat "
- "cores"
- << std::endl;
+ Notice() << "SmtEngine: turning off bitvector-to-bool to support old "
+ "unsat cores\n";
options::bitvectorToBool.set(false);
}
if (options::boolToBitvector.wasSetByUser())
{
throw OptionException(
- "bool-to-bv != off not supported with unsat cores");
+ "bool-to-bv != off not supported with old unsat cores");
}
- Notice() << "SmtEngine: turning off bool-to-bv to support unsat "
- "cores"
- << std::endl;
+ Notice()
+ << "SmtEngine: turning off bool-to-bv to support old unsat cores\n";
options::boolToBitvector.set(options::BoolToBVMode::OFF);
}
{
if (options::bvIntroducePow2.wasSetByUser())
{
- throw OptionException("bv-intro-pow2 not supported with unsat cores");
+ throw OptionException(
+ "bv-intro-pow2 not supported with old unsat cores");
}
- Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
- "unsat-cores"
- << std::endl;
+ Notice()
+ << "SmtEngine: turning off bv-intro-pow2 to support old unsat cores";
options::bvIntroducePow2.set(false);
}
{
if (options::repeatSimp.wasSetByUser())
{
- throw OptionException("repeat-simp not supported with unsat cores");
+ throw OptionException("repeat-simp not supported with old unsat cores");
}
- Notice() << "SmtEngine: turning off repeat-simp to support unsat "
- "cores"
- << std::endl;
+ Notice()
+ << "SmtEngine: turning off repeat-simp to support old unsat cores\n";
options::repeatSimp.set(false);
}
{
if (options::globalNegate.wasSetByUser())
{
- throw OptionException("global-negate not supported with unsat cores");
+ throw OptionException(
+ "global-negate not supported with old unsat cores");
}
- Notice() << "SmtEngine: turning off global-negate to support unsat "
- "cores"
- << std::endl;
+ Notice() << "SmtEngine: turning off global-negate to support old unsat "
+ "cores\n";
options::globalNegate.set(false);
}
if (options::bitvectorAig())
{
- throw OptionException("bitblast-aig not supported with unsat cores");
+ throw OptionException("bitblast-aig not supported with old unsat cores");
}
if (options::doITESimp())
{
- throw OptionException("ITE simp not supported with unsat cores");
+ throw OptionException("ITE simp not supported with old unsat cores");
}
}
else
if (!options::ufSymmetryBreaker.wasSetByUser())
{
bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
- && !options::incrementalSolving()
- && !options::unsatCores() && !options::unsatCoresNew();
+ && !options::incrementalSolving() && !safeUnsatCores;
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::unsatCoresNew();
+ && !safeUnsatCores;
Trace("smt") << "setting repeat simplification to " << repeatSimp
<< std::endl;
options::repeatSimp.set(repeatSimp);
}
Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
- // 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());
+ d_smtSolver->finishInit(logic);
// now can construct the SMT-level model object
TheoryEngine* te = d_smtSolver->getTheoryEngine();
}
}
// Check that UNSAT results generate an unsat core correctly.
- if (options::checkUnsatCores() || options::checkUnsatCoresNew())
+ if (options::checkUnsatCores())
{
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
{
UnsatCore SmtEngine::getUnsatCoreInternal()
{
- if (!options::unsatCores() && !options::unsatCoresNew())
+ if (!options::unsatCores())
{
throw ModalException(
- "Cannot get an unsat core when produce-unsat-cores[-new] option is "
- "off.");
+ "Cannot get an unsat core when produce-unsat-cores[-new] or "
+ "produce-proofs option is off.");
}
if (d_state->getMode() != SmtMode::UNSAT)
{
}
void SmtEngine::checkUnsatCore() {
- Assert(options::unsatCores() || options::unsatCoresNew())
+ Assert(options::unsatCores())
<< "cannot check unsat core if unsat cores are turned off";
Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
// 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
{
SmtScope smts(this);
finishInit();
- if (options::produceProofs() && !options::unsatCoresNew()
+ if (options::produceProofs()
+ && (!options::unsatCores()
+ || options::unsatCoresMode() == options::UnsatCoresMode::FULL_PROOF)
&& getSmtMode() == SmtMode::UNSAT)
{
// minimize instantiations based on proof manager
SmtSolver::~SmtSolver() {}
-void SmtSolver::finishInit(const LogicInfo& logicInfo,
- bool proofForUnsatCoreMode)
+void SmtSolver::finishInit(const LogicInfo& logicInfo)
{
// 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(),
- proofForUnsatCoreMode ? nullptr : d_pnm));
+ d_theoryEngine.reset(new TheoryEngine(
+ d_smt.getContext(),
+ d_smt.getUserContext(),
+ d_rm,
+ logicInfo,
+ d_smt.getOutputManager(),
+ // Other than whether d_pm is set, theory engine proofs are conditioned on
+ // the relationshup between proofs and unsat cores: the unsat cores are in
+ // FULL_PROOF mode, no proofs are generated on theory engine.
+ (options::unsatCores()
+ && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
+ ? nullptr
+ : d_pnm));
// Add the theories
for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
* 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,
- bool proofForUnsatCoreMode = false);
+ void finishInit(const LogicInfo& logicInfo);
/** Reset all assertions, global declarations, etc. */
void resetAssertions();
/**
(declare-fun f () Int)
(declare-fun g () String)
(declare-fun h () String)
-(assert (or
- (not (= ( str.replace "B" ( str.at "A" f) "") "B"))
- (not (= ( str.replace "B" ( str.replace "B" g "") "")
+(assert (or
+ (not (= ( str.replace "B" ( str.at "A" f) "") "B"))
+ (not (= ( str.replace "B" ( str.replace "B" g "") "")
( str.at ( str.replace ( str.replace a d "") "C" "") ( str.indexof "B" ( str.replace ( str.replace a d "") "C" "") 0))))))
(assert (= a (str.++ (str.++ d "C") g)))
(assert (= b (str.++ e g)))
projects / cvc5.git / commitdiff