From b384526f32eab67bce49c26e38d9bd7d8b1baca0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 9 Mar 2021 13:02:14 -0600 Subject: [PATCH] (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. --- src/smt/set_defaults.cpp | 11 ++++------- 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()); -- 2.30.2