projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5ee3c8d) | patch
Fix evaluator for non-evaluatable nodes (#3575)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 16 Dec 2019 17:23:54 +0000 (11:23 -0600)
committerAndres Noetzli <andres.noetzli@gmail.com>
Mon, 16 Dec 2019 17:23:54 +0000 (09:23 -0800)
commitd15d44b3c91b5be2c19adac292f137d2a67eb848
tree67f8cac1485c833970929ab10e216a1d69e8b48dtree
parent5ee3c8d02e21b1c20bfe56538c4cbe4fed0481ebcommit | diff
Fix evaluator for non-evaluatable nodes (#3575)

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.
src/theory/evaluator.cpp diff | blob | history
src/theory/evaluator.h diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.cpp diff | blob | history