summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2018-09-13 15:06:50 -0500
committerGitHub <noreply@github.com>2018-09-13 15:06:50 -0500
commit6ac8972a11047d0d858055ea89aa2acf15e2cfa7 (patch)
tree66d8e8f744637c0a6a9fbe74f765d4b17a69eaac /src/options
parent466b45c52d83cf19caef2c1eee6e7c5fd2ecb1bc (diff)
Uses information gain heuristic for building better solutions from DTs (#2451)
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 01cf41518..a4fca6d3c 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -984,6 +984,14 @@ header = "options/quantifiers_options.h"
help = "Synthesize conditions indepedently from return values (may generate bigger solutions)"
[[option]]
+ name = "sygusUnifBooleanHeuristicDt"
+ category = "regular"
+ long = "sygus-unif-boolean-heuristic-dt"
+ type = "bool"
+ default = "false"
+ help = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)"
+
+[[option]]
name = "sygusUnifCondIndNoRepeatSol"
category = "regular"
long = "sygus-unif-cond-indpendent-no-repeat-sol"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback