summaryrefslogtreecommitdiff
path: root/src/theory/evaluator.cpp
AgeCommit message (Collapse)Author
2018-09-18Fix issue with str.idof in evaluator (#2493)Andres Noetzli
2018-08-27Remove dead code in evaluator (#2389)Andres Noetzli
This should fix Coverity issue 1470214.
2018-08-01Fix wrong evaluation of STRING_STOI (#2252)Andres Noetzli
2018-07-26 Fix a few issues in the sygus sampler related to evaluation (#2215)Andrew Reynolds
2018-06-26sygusComp2018: Add evaluator (#2090)Andres Noetzli
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback