diff options
Diffstat (limited to 'src/options/smt_options.toml')
| -rw-r--r-- | src/options/smt_options.toml | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 2c87158de..4e1a89259 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -174,6 +174,34 @@ header = "options/smt_options.h" help = "check proofs eagerly with proof-new for local debugging" [[option]] + name = "proofGranularityMode" + category = "regular" + long = "proof-granularity=MODE" + type = "ProofGranularityMode" + default = "THEORY_REWRITE" + 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.REWRITE]] + name = "rewrite" + help = "allow rewrite or substitution steps, expand macros." +[[option.mode.THEORY_REWRITE]] + name = "theory-rewrite" + help = "allow theory rewrite steps, expand macros, rewrite and substitution steps." +[[option.mode.DSL_REWRITE]] + name = "dsl-rewrite" + help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps." + +[[option]] + name = "checkProofsNew" + category = "regular" + long = "check-proofs-new" + type = "bool" + help = "after UNSAT/VALID, check the generated proof (with proof-new)" + +[[option]] name = "dumpInstantiations" category = "regular" long = "dump-instantiations" |