summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-05-10 16:48:51 -0500
committerGitHub <noreply@github.com>2018-05-10 16:48:51 -0500
commitadcbee78823120baa47eb8ba868b614512a121a9 (patch)
treef019c19fa63cc06c8b4e93df2cbde7d61791368b /src/options
parentf29ced85757a85b6bd72b741d6ac7ff45ba29619 (diff)
Sygus repair constants (#1812)
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 4c771c143..10000bbb1 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -977,6 +977,14 @@ header = "options/quantifiers_options.h"
help = "use quantifier elimination as a preprocessing step for sygus"
[[option]]
+ name = "sygusRepairConst"
+ category = "regular"
+ long = "sygus-repair-const"
+ type = "bool"
+ default = "false"
+ help = "use approach to repair constants in sygus candidate solutions"
+
+[[option]]
name = "sygusMinGrammar"
category = "regular"
long = "sygus-min-grammar"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback