From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 4 Jan 2022 21:22:20 +0000 (-0600)
Subject: Change default granularity of proofs to macro (#7855)
X-Git-Tag: cvc5-1.0.0~602
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=306ca2f784980ace13aa5c9149bf067b0a1c54fe;p=cvc5.git

Change default granularity of proofs to macro (#7855)

Also changes the name "off" to "macro" to be more consistent.
---

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index 8eb2fd783..c63f99534 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -75,12 +75,12 @@ name   = "Proof"
   category   = "regular"
   long       = "proof-granularity=MODE"
   type       = "ProofGranularityMode"
-  default    = "THEORY_REWRITE"
+  default    = "MACRO"
   help       = "modes for proof granularity"
   help_mode  = "Modes for proof granularity."
-[[option.mode.OFF]]
-  name = "off"
-  help = "Do not improve the granularity of proofs."
+[[option.mode.MACRO]]
+  name = "macro"
+  help = "Allow macros. Do not improve the granularity of proofs."
 [[option.mode.REWRITE]]
   name = "rewrite"
   help = "Allow rewrite or substitution steps, expand macros."
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 798f7dd57..5f628219b 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -77,7 +77,7 @@ PfManager::PfManager(Env& env)
 
   // add rules to eliminate here
   if (options().proof.proofGranularityMode
-      != options::ProofGranularityMode::OFF)
+      != options::ProofGranularityMode::MACRO)
   {
     d_pfpp->setEliminateRule(PfRule::MACRO_SR_EQ_INTRO);
     d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_INTRO);
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 194290399..bce73046f 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -86,7 +86,6 @@ void SetDefaults::setDefaultsPre(Options& opts)
     {
       opts.smt.unsatCoresMode = options::UnsatCoresMode::PP_ONLY;
     }
-    opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF;
   }
   if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores
       || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores
@@ -138,17 +137,6 @@ void SetDefaults::setDefaultsPre(Options& opts)
   Assert(opts.smt.unsatCores
          == (opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF));
 
-  // new unsat core specific restrictions for proofs
-  if (opts.smt.unsatCores
-      && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF)
-  {
-    // no fine-graininess
-    if (!opts.proof.proofGranularityModeWasSetByUser)
-    {
-      opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF;
-    }
-  }
-
   // if we requiring disabling proofs, disable them now
   if (opts.smt.produceProofs)
   {