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/proof_post_processor.cpp | |
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/proof_post_processor.cpp')
-rw-r--r-- | src/smt/proof_post_processor.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 3866c1e0e..f5db349e1 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -478,8 +478,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, rargs.push_back(args[3]); } } - Rewriter* rr = d_env.getRewriter(); - Node tr = rr->rewriteViaMethod(ts, idr); + Node tr = d_env.rewriteViaMethod(ts, idr); Trace("smt-proof-pp-debug") << "...eq intro rewrite equality is " << ts << " == " << tr << ", from " << idr << std::endl; @@ -954,7 +953,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, getMethodId(args[1], idr); } Rewriter* rr = d_env.getRewriter(); - Node ret = rr->rewriteViaMethod(args[0], idr); + Node ret = d_env.rewriteViaMethod(args[0], idr); Node eq = args[0].eqNode(ret); if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT) { |