sygusComp2018: Add evaluator (#2090)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 26 Jun 2018 23:09:03 +0000 (16:09 -0700)
committerGitHub <noreply@github.com>
Tue, 26 Jun 2018 23:09:03 +0000 (16:09 -0700)
commit81bb4147ad681641dc99a62fc1a8605f99c05f2d
tree18bf2c6a4cbe000f401bc72ff76eba9e0f452933
parent1fd8d68067fcc7470682de09a9391d7140682c48
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.
src/Makefile.am
src/options/quantifiers_options.toml
src/theory/evaluator.cpp [new file with mode: 0644]
src/theory/evaluator.h [new file with mode: 0644]
src/theory/quantifiers/sygus/term_database_sygus.cpp
src/theory/quantifiers/sygus/term_database_sygus.h
test/unit/Makefile.am
test/unit/theory/evaluator_white.h [new file with mode: 0644]