summaryrefslogtreecommitdiff
path: root/src/options/quantifiers_options.toml
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/quantifiers_options.toml')
-rw-r--r--src/options/quantifiers_options.toml18
1 files changed, 18 insertions, 0 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 2a5faf9f7..d29052042 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -2023,3 +2023,21 @@ header = "options/quantifiers_options.h"
[[option.mode.BOTH]]
name = "both"
help = "combines minimal and maximal ."
+
+[[option]]
+ name = "sygusInstMode"
+ category = "regular"
+ long = "sygus-inst-mode=MODE"
+ type = "SygusInstMode"
+ default = "PRIORITY_INST"
+ help = "select instantiation lemma mode"
+ help_mode = "SyGuS instantiation lemma modes."
+[[option.mode.PRIORITY_INST]]
+ name = "priority-inst"
+ help = "add instantiation lemmas first, add evaluation unfolding if instantiation fails."
+[[option.mode.PRIORITY_EVAL]]
+ name = "priority-eval"
+ help = "add evaluation unfolding lemma first, add instantiation lemma if unfolding lemmas already added."
+[[option.mode.INTERLEAVE]]
+ name = "interleave"
+ help = "add instantiation and evaluation unfolding lemmas in the same step."
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback