From 306ca2f784980ace13aa5c9149bf067b0a1c54fe Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 4 Jan 2022 15:22:20 -0600 Subject: [PATCH] Change default granularity of proofs to macro (#7855) Also changes the name "off" to "macro" to be more consistent. --- src/options/proof_options.toml | 8 ++++---- src/smt/proof_manager.cpp | 2 +- src/smt/set_defaults.cpp | 12 ------------ 3 files changed, 5 insertions(+), 17 deletions(-) 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) { -- 2.30.2