diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-09-10 20:51:03 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-10 18:51:03 -0700 |
| commit | 1a695dcbe3036ab0f1922c5655c082ec1f14db97 (patch) | |
| tree | 96444e8dedeb0b98ba01a7f7b1a7a0c5b2349410 /src/options/quantifiers_options.toml | |
| parent | f5746ca4a24c1b9f05f5528bc66016668d9a7863 (diff) | |
Using a single condition enumerator in sygus-unif (#2440)
This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).
In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:
- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.
A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.
There is also small improvements for trace messages.
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index c9d1aefa1..01cf41518 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -741,7 +741,7 @@ header = "options/quantifiers_options.h" read_only = true help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas" -### Rewrite rules options +### Rewrite rules options [[option]] name = "quantRewriteRules" @@ -761,7 +761,7 @@ header = "options/quantifiers_options.h" read_only = true help = "add one instance of rewrite rule per round" -### Induction options +### Induction options [[option]] name = "quantInduction" @@ -976,6 +976,22 @@ header = "options/quantifiers_options.h" help = "Unification-based function synthesis" [[option]] + name = "sygusUnifCondIndependent" + category = "regular" + long = "sygus-unif-cond-independent" + type = "bool" + default = "false" + help = "Synthesize conditions indepedently from return values (may generate bigger solutions)" + +[[option]] + name = "sygusUnifCondIndNoRepeatSol" + category = "regular" + long = "sygus-unif-cond-indpendent-no-repeat-sol" + type = "bool" + default = "true" + help = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis" + +[[option]] name = "sygusBoolIteReturnConst" category = "regular" long = "sygus-bool-ite-return-const" @@ -1164,7 +1180,7 @@ header = "options/quantifiers_options.h" type = "bool" default = "true" help = "Minimize synthesis solutions" - + [[option]] name = "sygusEvalOpt" category = "regular" @@ -1180,7 +1196,7 @@ header = "options/quantifiers_options.h" type = "bool" default = "false" help = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant" - + # Internal uses of sygus [[option]] |