Eliminate backwards ref to SmtEngine from abduction and interpol solvers (#7133)

5 files changed, 55 insertions, 55 deletions

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index b773d8d57..b66daefd3 100644
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -32,13 +32,11 @@ using namespace cvc5::theory;
 namespace cvc5 {
 namespace smt {
 
-AbductionSolver::AbductionSolver(Env& env, SmtEngine* parent)
-    : d_env(env), d_parent(parent)
-{
-}
+AbductionSolver::AbductionSolver(Env& env) : EnvObj(env) {}
 
 AbductionSolver::~AbductionSolver() {}
-bool AbductionSolver::getAbduct(const Node& goal,
+bool AbductionSolver::getAbduct(const std::vector<Node>& axioms,
+                                const Node& goal,
                                 const TypeNode& grammarType,
                                 Node& abd)
 {
@@ -48,7 +46,6 @@ bool AbductionSolver::getAbduct(const Node& goal,
     throw ModalException(msg);
   }
   Trace("sygus-abduct") << "SmtEngine::getAbduct: goal " << goal << std::endl;
-  std::vector<Node> axioms = d_parent->getExpandedAssertions();
   std::vector<Node> asserts(axioms.begin(), axioms.end());
   // must expand definitions
   Node conjn = d_env.getTopLevelSubstitutions().apply(goal);
@@ -74,16 +71,19 @@ bool AbductionSolver::getAbduct(const Node& goal,
   d_subsolver->setLogic(l);
   // assert the abduction query
   d_subsolver->assertFormula(aconj);
-  return getAbductInternal(abd);
+  return getAbductInternal(axioms, abd);
 }
 
-bool AbductionSolver::getAbduct(const Node& goal, Node& abd)
+bool AbductionSolver::getAbduct(const std::vector<Node>& axioms,
+                                const Node& goal,
+                                Node& abd)
 {
   TypeNode grammarType;
-  return getAbduct(goal, grammarType, abd);
+  return getAbduct(axioms, goal, grammarType, abd);
 }
 
-bool AbductionSolver::getAbductInternal(Node& abd)
+bool AbductionSolver::getAbductInternal(const std::vector<Node>& axioms,
+                                        Node& abd)
 {
   // should have initialized the subsolver by now
   Assert(d_subsolver != nullptr);
@@ -128,7 +128,7 @@ bool AbductionSolver::getAbductInternal(Node& abd)
       // if check abducts option is set, we check the correctness
       if (options::checkAbducts())
       {
-        checkAbduct(abd);
+        checkAbduct(axioms, abd);
       }
       return true;
     }
@@ -139,13 +139,13 @@ bool AbductionSolver::getAbductInternal(Node& abd)
   return false;
 }
 
-void AbductionSolver::checkAbduct(Node a)
+void AbductionSolver::checkAbduct(const std::vector<Node>& axioms, Node a)
 {
   Assert(a.getType().isBoolean());
   Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions"
                         << std::endl;
 
-  std::vector<Node> asserts = d_parent->getExpandedAssertions();
+  std::vector<Node> asserts(axioms.begin(), axioms.end());
   asserts.push_back(a);
 
   // two checks: first, consistent with assertions, second, implies negated goal
diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h
index b408fe060..3ea2755ae 100644
--- a/src/smt/abduction_solver.h
+++ b/src/smt/abduction_solver.h
@@ -20,10 +20,10 @@
 
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
-class Env;
 class SmtEngine;
 
 namespace smt {
@@ -35,10 +35,10 @@ namespace smt {
  * a subsolver SmtEngine for a sygus conjecture that captures the abduction
  * query, and implements supporting utility methods such as checkAbduct.
  */
-class AbductionSolver
+class AbductionSolver : protected EnvObj
 {
  public:
-  AbductionSolver(Env& env, SmtEngine* parent);
+  AbductionSolver(Env& env);
   ~AbductionSolver();
   /**
    * This method asks this SMT engine to find an abduct with respect to the
@@ -46,23 +46,27 @@ class AbductionSolver
    * If this method returns true, then abd is set to a formula C such that
    * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable.
    *
-   * @param goal The goal of the abduction problem.
+   * @param axioms The expanded assertions A of the parent SMT engine
+   * @param goal The goal B of the abduction problem.
    * @param grammarType A sygus datatype type that encodes the syntax
    * restrictions on the shape of possible solutions.
-   * @param abd This argument is updated to contain the solution to the
+   * @param abd This argument is updated to contain the solution C to the
    * abduction problem. Notice that this is a formula whose free symbols
    * are contained in goal + the parent's current assertion stack.
    *
    * This method invokes a separate copy of the SMT engine for solving the
    * corresponding sygus problem for generating such a solution.
    */
-  bool getAbduct(const Node& goal, const TypeNode& grammarType, Node& abd);
+  bool getAbduct(const std::vector<Node>& axioms,
+                 const Node& goal,
+                 const TypeNode& grammarType,
+                 Node& abd);
 
   /**
    * Same as above, but without user-provided grammar restrictions. A default
    * grammar is chosen internally using the sygus grammar constructor utility.
    */
-  bool getAbduct(const Node& goal, Node& abd);
+  bool getAbduct(const std::vector<Node>& axioms, const Node& goal, Node& abd);
 
   /**
    * Check that a solution to an abduction conjecture is indeed a solution.
@@ -71,8 +75,11 @@ class AbductionSolver
    * solution to the abduction problem (a) is SAT, and the assertions conjoined
    * with the abduct and the goal is UNSAT. If these criteria are not met, an
    * internal error is thrown.
+   *
+   * @param axioms The expanded assertions of the parent SMT engine
+   * @param a The abduct to check.
    */
-  void checkAbduct(Node a);
+  void checkAbduct(const std::vector<Node>& axioms, Node a);
 
  private:
   /**
@@ -84,11 +91,7 @@ class AbductionSolver
    * This method assumes d_subsolver has been initialized to do abduction
    * problems.
    */
-  bool getAbductInternal(Node& abd);
-  /** Reference to the env */
-  Env& d_env;
-  /** The parent SMT engine */
-  SmtEngine* d_parent;
+  bool getAbductInternal(const std::vector<Node>& axioms, Node& abd);
   /** The SMT engine subsolver
    *
    * This is a separate copy of the SMT engine which is used for making
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index ab7002205..3e227fa31 100644
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -32,14 +32,12 @@ using namespace cvc5::theory;
 namespace cvc5 {
 namespace smt {
 
-InterpolationSolver::InterpolationSolver(Env& env, SmtEngine* parent)
-    : d_env(env), d_parent(parent)
-{
-}
+InterpolationSolver::InterpolationSolver(Env& env) : EnvObj(env) {}
 
 InterpolationSolver::~InterpolationSolver() {}
 
-bool InterpolationSolver::getInterpol(const Node& conj,
+bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
+                                      const Node& conj,
                                       const TypeNode& grammarType,
                                       Node& interpol)
 {
@@ -51,7 +49,6 @@ bool InterpolationSolver::getInterpol(const Node& conj,
   }
   Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj
                           << std::endl;
-  std::vector<Node> axioms = d_parent->getExpandedAssertions();
   // must expand definitions
   Node conjn = d_env.getTopLevelSubstitutions().apply(conj);
   std::string name("A");
@@ -69,10 +66,12 @@ bool InterpolationSolver::getInterpol(const Node& conj,
   return false;
 }
 
-bool InterpolationSolver::getInterpol(const Node& conj, Node& interpol)
+bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
+                                      const Node& conj,
+                                      Node& interpol)
 {
   TypeNode grammarType;
-  return getInterpol(conj, grammarType, interpol);
+  return getInterpol(axioms, conj, grammarType, interpol);
 }
 
 void InterpolationSolver::checkInterpol(Node interpol,
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
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 72268aa03..582ca0c2c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -255,12 +255,12 @@ void SmtEngine::finishInit()
   // subsolvers
   if (d_env->getOptions().smt.produceAbducts)
   {
-    d_abductSolver.reset(new AbductionSolver(*d_env.get(), this));
+    d_abductSolver.reset(new AbductionSolver(*d_env.get()));
   }
   if (d_env->getOptions().smt.produceInterpols
       != options::ProduceInterpols::NONE)
   {
-    d_interpolSolver.reset(new InterpolationSolver(*d_env.get(), this));
+    d_interpolSolver.reset(new InterpolationSolver(*d_env.get()));
   }
 
   d_pp->finishInit();
@@ -1754,7 +1754,9 @@ bool SmtEngine::getInterpol(const Node& conj,
 {
   SmtScope smts(this);
   finishInit();
-  bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol);
+  std::vector<Node> axioms = getExpandedAssertions();
+  bool success =
+      d_interpolSolver->getInterpol(axioms, conj, grammarType, interpol);
   // notify the state of whether the get-interpol call was successfuly, which
   // impacts the SMT mode.
   d_state->notifyGetInterpol(success);
@@ -1773,7 +1775,8 @@ bool SmtEngine::getAbduct(const Node& conj,
 {
   SmtScope smts(this);
   finishInit();
-  bool success = d_abductSolver->getAbduct(conj, grammarType, abd);
+  std::vector<Node> axioms = getExpandedAssertions();
+  bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd);
   // notify the state of whether the get-abduct call was successfuly, which
   // impacts the SMT mode.
   d_state->notifyGetAbduct(success);