From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 9 Mar 2021 19:02:14 +0000 (-0600)
Subject: (proof-new) Minor fix and allow proof option (#6085)
X-Git-Tag: cvc5-1.0.0~2128
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b384526f32eab67bce49c26e38d9bd7d8b1baca0;p=cvc5.git

(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.
---

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());