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 8eb2fd783e613f3f82602c61ad3f05df339ef5d7..c63f9953490a0572893648d3955d2e7306d639e8 100644 (file)
--- 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 798f7dd57eb68446d7d5ee9ce7909bf6108e94c6..5f628219ba7986ef031d3fdcbeea57b05e2878cd 100644 (file)
--- 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 1942903994908dab72ddb145f3eb4241d08d564e..bce73046f01a57f4f0d20ef2d9fc411ab8c371ae 100644 (file)
--- 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)
   {