diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-09-01 19:57:21 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-02 02:57:21 +0000 |
| commit | fb4a3021359059c82f9a01ad4a9d78d1c126a64c (patch) | |
| tree | 97e228ace63c39f6fce72004c1ef1adbe61a2afd /src/theory/builtin/proof_checker.cpp | |
| parent | 9f48eb94a7a72338283492169a0d494fcdc57034 (diff) | |
rewriter: Make rewriteEqualityExt non-static. (#7110)
More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
Diffstat (limited to 'src/theory/builtin/proof_checker.cpp')
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 54d1779ec..bb0f9a413 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -16,6 +16,7 @@ #include "theory/builtin/proof_checker.h" #include "expr/skolem_manager.h" +#include "smt/env.h" #include "smt/term_formula_removal.h" #include "theory/evaluator.h" #include "theory/rewriter.h" @@ -28,6 +29,8 @@ namespace cvc5 { namespace theory { namespace builtin { +BuiltinProofRuleChecker::BuiltinProofRuleChecker(Env& env) : d_env(env) {} + void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) { pc->registerChecker(PfRule::ASSUME, this); @@ -81,7 +84,7 @@ Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr) } if (idr == MethodId::RW_REWRITE_EQ_EXT) { - return Rewriter::rewriteEqualityExt(n); + return d_env.getRewriter()->rewriteEqualityExt(n); } if (idr == MethodId::RW_EVALUATE) { |