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.toml22
1 files changed, 19 insertions, 3 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 4a098f9fc..b8ddd6d31 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1132,12 +1132,28 @@ header = "options/quantifiers_options.h"
help = "use sygus to enumerate candidate rewrite rules via sampling"
[[option]]
- name = "sygusRewSynthFilter"
+ name = "sygusRewSynthFilterOrder"
category = "regular"
- long = "sygus-rr-synth-filter"
+ long = "sygus-rr-synth-filter-order"
type = "bool"
default = "true"
- help = "filter candidate rewrites based on techniques like matching"
+ help = "filter candidate rewrites based on variable ordering"
+
+[[option]]
+ name = "sygusRewSynthFilterMatch"
+ category = "regular"
+ long = "sygus-rr-synth-filter-match"
+ type = "bool"
+ default = "true"
+ help = "filter candidate rewrites based on matching"
+
+[[option]]
+ name = "sygusRewSynthFilterCong"
+ category = "regular"
+ long = "sygus-rr-synth-filter-cong"
+ type = "bool"
+ default = "true"
+ help = "filter candidate rewrites based on congruence"
[[option]]
name = "sygusRewVerify"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback