diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-26 16:09:03 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-26 16:09:03 -0700 |
| commit | 81bb4147ad681641dc99a62fc1a8605f99c05f2d (patch) | |
| tree | 18bf2c6a4cbe000f401bc72ff76eba9e0f452933 /src/options/quantifiers_options.toml | |
| parent | 1fd8d68067fcc7470682de09a9391d7140682c48 (diff) | |
sygusComp2018: Add evaluator (#2090)
This commit adds the Evaluator class that can be used to quickly
evaluate terms under a given substitution without going through the
rewriter. This has been shown to lead to significant performance
improvements on SyGuS PBE problems with a large number of inputs because
candidate solutions are evaluated on those inputs. With this commit, the
evaluator only gets called from the SyGuS solver but there are
potentially other places in the code that could profit from it.
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 69868ad8d..be4c66b27 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1118,6 +1118,14 @@ header = "options/quantifiers_options.h" includes = ["options/quantifiers_modes.h"] help = "mode for using samples in the counterexample-guided inductive synthesis loop" +[[option]] + name = "sygusEvalOpt" + category = "regular" + long = "sygus-eval-opt" + type = "bool" + default = "true" + help = "use optimized approach for evaluation in sygus" + # Internal uses of sygus [[option]] |