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 /contrib/cvc-devel.el | |
| 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 'contrib/cvc-devel.el')
0 files changed, 0 insertions, 0 deletions