diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-22 16:07:16 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-22 16:07:16 -0600 |
commit | 71d72df0437607723256bbd7b4f28cd6c89fe40f (patch) | |
tree | 1021b9e166290db4637a0be447da359d0aed4752 /src/options/smt_options.toml | |
parent | 580f3e93c2cc4564e6fa87d07426dc1ff87224e4 (diff) |
(proof-new) Change proof-new option to proof (#5955)
Also moves several proof-specific options to proof_options.
Diffstat (limited to 'src/options/smt_options.toml')
-rw-r--r-- | src/options/smt_options.toml | 57 |
1 files changed, 9 insertions, 48 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index ed056ac9f..c29fe5e50 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -131,67 +131,28 @@ header = "options/smt_options.h" help = "Block models based on the concrete model values for the free variables." [[option]] - name = "dumpProofs" - category = "regular" - long = "dump-proofs" - type = "bool" - default = "false" - read_only = true - help = "output proofs after every UNSAT/VALID response" - -[[option]] - name = "proofNew" + name = "proof" category = "regular" - long = "proof-new" + long = "proof" type = "bool" default = "false" - help = "do proof production using the new infrastructure" + help = "produce proofs, support check-proofs and get-proof" [[option]] - name = "proofNewPedantic" - category = "regular" - long = "proof-new-pedantic=N" - type = "uint32_t" - default = "0" - read_only = true - help = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof-new" - -[[option]] - name = "proofNewEagerChecking" + name = "dumpProofs" category = "regular" - long = "proof-new-eager-checking" + long = "dump-proofs" type = "bool" default = "false" read_only = true - 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." + help = "output proofs after every UNSAT/VALID response" [[option]] - name = "checkProofsNew" + name = "checkProofs" category = "regular" - long = "check-proofs-new" + long = "check-proofs" type = "bool" - help = "after UNSAT/VALID, check the generated proof (with proof-new)" + help = "after UNSAT/VALID, check the generated proof (with proof)" [[option]] name = "dumpInstantiations" |