cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2020-01-30	External cache argument for evaluator (#3672)	Andrew Reynolds

2019-12-16	Use the evaluator utility in the function definition evaluator (#3576)	Andrew Reynolds
	Improves performance on ground conjectures with recursive functions. We use the evalutator to (partially) evaluate bodies of recursive functions, instead of relying on substitution+rewriting.
2019-12-16	Fix evaluator for non-evaluatable nodes (#3575)	Andrew Reynolds
	This ensures that the Evaluator always returns the result of substitution + rewriting for constant substitutions. This requires a few further extensions to the code, namely: (1) Applying substutitions to operators, (2) Reconstructing all nodes that fail to evaluate by taking into account evaluation of their children.
2019-12-16	Revert evaluate as node. (#3574)	Andrew Reynolds

2019-12-15	Minor improvement to evaluator (#3570)	Andrew Reynolds
	Fixes a bug where we don't return the partially evaluated version (for unevaluatable nodes). Also adds `NONLINEAR_MULT` whose semantics is identical to `MULT`.
2019-12-10	Incorporate rewriting on demand in the evaluator (#3549)	Andrew Reynolds

2019-07-31	Add some missing cases in evaluator (#3133)	Andrew Reynolds

2019-03-26	Update copyright headers.	Aina Niemetz

2018-11-07	Evaluator: add support for str.code (#2696)	Andres Noetzli

2018-09-18	Fix issue with str.idof in evaluator (#2493)	Andres Noetzli

2018-08-27	Remove dead code in evaluator (#2389)	Andres Noetzli
	This should fix Coverity issue 1470214.
2018-08-01	Fix 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-26	sygusComp2018: 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.