diff options
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/proof_options.toml | 38 | ||||
| -rw-r--r-- | src/options/smt_options.toml | 57 |
2 files changed, 47 insertions, 48 deletions
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index c744b237b..631a27604 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -10,3 +10,41 @@ header = "options/proof_options.h" default = "false" read_only = true help = "Print conclusion of proof steps when printing AST" + +[[option]] + name = "proofPedantic" + category = "regular" + long = "proof-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" + +[[option]] + name = "proofEagerChecking" + category = "regular" + long = "proof-eager-checking" + type = "bool" + default = "false" + help = "check proofs eagerly with proof 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." 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" |