diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-22 15:05:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-22 20:05:44 +0000 |
| commit | ba259d66be877de3cc77e4f62083905ace942c82 (patch) | |
| tree | 864bd79d72e52516bd9427a9f3d6907843f14b01 /src/smt/env_obj.h | |
| parent | f9fd2f7a1e37540c0ac6a9ef33f9da91f69a8368 (diff) | |
Towards standard usage of evaluator (#7189)
This makes the evaluator accessible via EnvObj through the Rewriter. It furthermore removes Rewriter::rewrite from inside the evaluator itself.
Construction of Evaluator utilities is now discouraged.
The include dependencies were cleaned slightly in this PR, leading to more precise includes throughout.
This is work towards having a configurable cardinality for strings, as well as eliminating SmtEngineScope.
Diffstat (limited to 'src/smt/env_obj.h')
| -rw-r--r-- | src/smt/env_obj.h | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h index ef9a82b17..75b97fda9 100644 --- a/src/smt/env_obj.h +++ b/src/smt/env_obj.h @@ -55,6 +55,20 @@ class EnvObj * This is a wrapper around theory::Rewriter::extendedRewrite via Env. */ Node extendedRewrite(TNode node, bool aggr = true) const; + /** + * Evaluate node n under the substitution args -> vals. + * This is a wrapper about theory::Rewriter::evaluate via Env. + */ + Node evaluate(TNode n, + const std::vector<Node>& args, + const std::vector<Node>& vals, + bool useRewriter = true) const; + /** Same as above, with a visited cache. */ + Node evaluate(TNode n, + const std::vector<Node>& args, + const std::vector<Node>& vals, + const std::unordered_map<Node, Node>& visited, + bool useRewriter = true) const; /** Get the current logic information. */ const LogicInfo& logicInfo() const; |