1 files changed, 12 insertions, 17 deletions
diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h
index 19bb54c61..03c899ead 100644
--- a/src/smt/interpolation_solver.h
+++ b/src/smt/interpolation_solver.h
@@ -20,12 +20,9 @@
 
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
-
-class Env;
-class SmtEngine;
-
 namespace smt {
 
 /**
@@ -35,28 +32,30 @@ namespace smt {
  * a subsolver SmtEngine for a sygus conjecture that captures the interpolation
  * query, and implements supporting utility methods such as checkInterpol.
  */
-class InterpolationSolver
+class InterpolationSolver : protected EnvObj
 {
  public:
-  InterpolationSolver(Env& env, SmtEngine* parent);
+  InterpolationSolver(Env& env);
   ~InterpolationSolver();
 
   /**
-   * This method asks this SMT engine to find an interpolant with respect to
+   * This method asks this solver to find an interpolant with respect to
    * the current assertion stack (call it A) and the conjecture (call it B). If
    * this method returns true, then interpolant is set to a formula I such that
    * A ^ ~I and I ^ ~B are both unsatisfiable.
    *
-   * @param conj The conjecture of the interpolation problem.
+   * @param axioms The expanded assertions A of the parent SMT engine
+   * @param conj The conjecture B of the interpolation problem.
    * @param grammarType A sygus datatype type that encodes the syntax
    * restrictions on the shape of possible solutions.
-   * @param interpol This argument is updated to contain the solution to the
+   * @param interpol This argument is updated to contain the solution I to the
    * interpolation problem.
    *
    * This method invokes a separate copy of the SMT engine for solving the
    * corresponding sygus problem for generating such a solution.
    */
-  bool getInterpol(const Node& conj,
+  bool getInterpol(const std::vector<Node>& axioms,
+                   const Node& conj,
                    const TypeNode& grammarType,
                    Node& interpol);
 
@@ -64,7 +63,9 @@ class InterpolationSolver
    * Same as above, but without user-provided grammar restrictions. A default
    * grammar is chosen internally using the sygus grammar constructor utility.
    */
-  bool getInterpol(const Node& conj, Node& interpol);
+  bool getInterpol(const std::vector<Node>& axioms,
+                   const Node& conj,
+                   Node& interpol);
 
   /**
    * Check that a solution to an interpolation problem is indeed a solution.
@@ -76,12 +77,6 @@ class InterpolationSolver
   void checkInterpol(Node interpol,
                      const std::vector<Node>& easserts,
                      const Node& conj);
-
- private:
-  /** Reference to the env */
-  Env& d_env;
-  /** The parent SMT engine */
-  SmtEngine* d_parent;
 };
 
 }  // namespace smt