summaryrefslogtreecommitdiff
path: root/src/options/smt_options.toml
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-10-18 19:37:11 -0500
committerGitHub <noreply@github.com>2018-10-18 19:37:11 -0500
commit547bd91e189b28da9950e12037d1e88079157479 (patch)
tree7f225e6df081071028c9e6102c902a6224179edf /src/options/smt_options.toml
parent10707e3ec6f2cab793919f2d1a159e13cdd032a9 (diff)
Non-implied mode for model cores (#2653)
Diffstat (limited to 'src/options/smt_options.toml')
-rw-r--r--src/options/smt_options.toml15
1 files changed, 8 insertions, 7 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 8af1000ba..e0041774a 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -40,7 +40,7 @@ header = "options/smt_options.h"
type = "SimplificationMode"
default = "SIMPLIFICATION_MODE_BATCH"
handler = "stringToSimplificationMode"
- includes = ["options/simplification_mode.h"]
+ includes = ["options/smt_modes.h"]
help = "choose simplification mode, see --simplification=help"
[[alias]]
@@ -99,13 +99,14 @@ header = "options/smt_options.h"
help = "output models after every SAT/INVALID/UNKNOWN response"
[[option]]
- name = "produceModelCores"
+ name = "modelCoresMode"
category = "regular"
- long = "produce-model-cores"
- type = "bool"
- default = "false"
- read_only = true
- help = "when printing models, compute a minimal core of relevant definitions"
+ long = "model-cores=MODE"
+ type = "ModelCoresMode"
+ default = "MODEL_CORES_NONE"
+ handler = "stringToModelCoresMode"
+ includes = ["options/smt_modes.h"]
+ help = "mode for producing model cores"
[[option]]
name = "proof"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback