From d6b3329e3f2b6e29e5f4af6cf09fd32e26c47e15 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Sep 2021 12:30:31 -0500 Subject: Towards standard usage of ExtendedRewriter (#7145) This PR: Adds extendedRewrite to EnvObj and Rewriter. Eliminates static calls to Rewriter::rewrite from within the extended rewriter. Instead, the use of extended rewriter is always through Rewriter, which passes itself to the ExtendedRewriter. Make most uses of extended rewriter non-static. I've added a placeholder method Rewriter::callExtendedRewrite for places in the code that call the extended rewriter are currently difficult to eliminate. --- src/smt/quant_elim_solver.h | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'src/smt/quant_elim_solver.h') diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index f890deba0..a0b43d09d 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -20,10 +20,9 @@ #include "expr/node.h" #include "smt/assertions.h" +#include "smt/env_obj.h" namespace cvc5 { -class Env; - namespace smt { class SmtSolver; @@ -36,7 +35,7 @@ class SmtSolver; * quantifier instantiations used for unsat which are in turn used for * constructing the solution for the quantifier elimination query. */ -class QuantElimSolver +class QuantElimSolver : protected EnvObj { public: QuantElimSolver(Env& env, SmtSolver& sms); @@ -97,8 +96,6 @@ class QuantElimSolver bool isInternalSubsolver); private: - /** Reference to the env */ - Env& d_env; /** The SMT solver, which is used during doQuantifierElimination. */ SmtSolver& d_smtSolver; }; -- cgit v1.2.3