Use the evaluator utility in the function definition evaluator (#3576)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 16 Dec 2019 21:02:28 +0000 (15:02 -0600)
committerAndres Noetzli <andres.noetzli@gmail.com>
Mon, 16 Dec 2019 21:02:28 +0000 (13:02 -0800)
commite1074c87769d079936b52a8e8ea33cc03f8b4638
tree4b962b255603e66ebca84e2607cb1def1b800326
parent0db2265511cf553c793cfb150079c524bb1e6449
Use the evaluator utility in the function definition evaluator (#3576)

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.
src/theory/evaluator.cpp
src/theory/evaluator.h
src/theory/quantifiers/fun_def_evaluator.cpp
src/theory/quantifiers/fun_def_evaluator.h