summaryrefslogtreecommitdiff
path: root/src/smt/quant_elim_solver.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/quant_elim_solver.h')
-rw-r--r--src/smt/quant_elim_solver.h7
1 files changed, 2 insertions, 5 deletions
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;
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback