summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-08-08 17:09:18 -0500
committerGitHub <noreply@github.com>2018-08-08 17:09:18 -0500
commitece17ee2c38fa5769ae3ab7fa3607c0e88c0021f (patch)
treea3b68f05ce57ba255ef1647efd66b60ccf3fb3e9 /src/options
parentc7489b25e3e50437785e7b739288475e4cdc8626 (diff)
Disable argument relevance for sygus by default (#2288)
Diffstat (limited to 'src/options')
-rw-r--r--src/options/quantifiers_options.toml8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index aac84e92c..5f6638dce 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1175,6 +1175,14 @@ header = "options/quantifiers_options.h"
default = "true"
help = "use optimized approach for evaluation in sygus"
+[[option]]
+ name = "sygusArgRelevant"
+ category = "regular"
+ long = "sygus-arg-relevant"
+ type = "bool"
+ default = "false"
+ help = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant"
+
# Internal uses of sygus
[[option]]
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback