diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-09 13:02:14 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-09 13:02:14 -0600 |
| commit | b384526f32eab67bce49c26e38d9bd7d8b1baca0 (patch) | |
| tree | 1c35fc83c23f11928ef6be32cb493237730568ea | |
| parent | 1b180f87266ffa206da1d5b772816b80e7f97c14 (diff) | |
(proof-new) Minor fix and allow proof option (#6085)
This is in preparation for enabling CI / proofs on master.
This does not throw an option exception when proofs are enabled, it also makes a fix that was missing on master and needed for regressions to pass on master.
This is partially taken from #5980.
| -rw-r--r-- | src/smt/set_defaults.cpp | 11 | ||||
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 3 |
2 files changed, 6 insertions, 8 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index a79d79e19..91910da47 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -72,8 +72,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Notice() << "SmtEngine: setting unsatCores" << std::endl; options::unsatCores.set(true); } - if (options::checkUnsatCoresNew()) + if (options::checkProofs() || options::checkUnsatCoresNew()) { + Notice() << "SmtEngine: setting proof" << std::endl; options::proof.set(true); } if (options::bitvectorAigSimplifications.wasSetByUser()) @@ -310,7 +311,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || options::produceAbducts() || options::produceInterpols() != options::ProduceInterpols::NONE || options::modelCoresMode() != options::ModelCoresMode::NONE - || options::blockModelsMode() != options::BlockModelsMode::NONE) + || options::blockModelsMode() != options::BlockModelsMode::NONE + || options::proof()) && !options::produceAssertions()) { Notice() << "SmtEngine: turning on produce-assertions to support " @@ -1375,11 +1377,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) "division. " "Try --bv-div-zero-const to interpret division by zero as a constant."); } - // !!!!!!!!!!!!!!!! temporary, until proofs are functional - if (options::proof()) - { - throw OptionException("--proof is not yet supported."); - } if (logic == LogicInfo("QF_UFNRA")) { diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 206b47348..75f93af47 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -422,7 +422,8 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, || id == PfRule::THEORY_PREPROCESS_LEMMA || id == PfRule::THEORY_EXPAND_DEF || id == PfRule::WITNESS_AXIOM || id == PfRule::THEORY_LEMMA || id == PfRule::THEORY_REWRITE - || id == PfRule::TRUST_SUBS || id == PfRule::TRUST_SUBS_MAP) + || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS + || id == PfRule::TRUST_SUBS_MAP) { // "trusted" rules Assert(children.empty()); |