diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-16 11:23:54 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-16 09:23:54 -0800 |
commit | d15d44b3c91b5be2c19adac292f137d2a67eb848 (patch) | |
tree | 67f8cac1485c833970929ab10e216a1d69e8b48d /src/theory/evaluator.h | |
parent | 5ee3c8d02e21b1c20bfe56538c4cbe4fed0481eb (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.
Diffstat (limited to 'src/theory/evaluator.h')
-rw-r--r-- | src/theory/evaluator.h | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index a65ffdf19..94e6fc518 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -118,6 +118,19 @@ class Evaluator const std::vector<Node>& args, const std::vector<Node>& vals, std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode); + /** reconstruct + * + * This function reconstructs the result of evaluating n using a combination + * of evaluation results (eresults) and substitution+rewriting (evalAsNode). + * + * Arguments eresults and evalAsNode are built within the context of the + * above method for some args and vals. This method ensures that the return + * value is equivalent to the rewritten form of n * { args -> vals }. + */ + Node reconstruct( + TNode n, + std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults, + std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode); }; } // namespace theory |