Split abduction solver from SmtEngine (#4733)

This splits everything related to abducts into its own standalone module, AbductionSolver.

It furthermore converts some of the interfaces of SmtEngine to make them take Node instead of Expr (this will be done for every method eventually).

The code for interpolation should follow a similar pattern, e.g. InterpolantSolver.

7 files changed, 391 insertions, 252 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 199c14330..28d943ced 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -219,6 +219,8 @@ libcvc4_add_sources(
   prop/sat_solver_types.h
   prop/theory_proxy.cpp
   prop/theory_proxy.h
+  smt/abduction_solver.cpp
+  smt/abduction_solver.h
   smt/command.cpp
   smt/command.h
   smt/command_list.cpp
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
new file mode 100644
index 000000000..adb80b719
--- /dev/null
+++ b/src/smt/abduction_solver.cpp
@@ -0,0 +1,202 @@
+/*********************                                                        */
+/*! \file abduction_solver.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for abduction queries
+ **/
+
+#include "smt/abduction_solver.h"
+
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/sygus/sygus_abduct.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/smt_engine_subsolver.h"
+
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace smt {
+
+AbductionSolver::AbductionSolver(SmtEngine* parent) : d_parent(parent) {}
+
+AbductionSolver::~AbductionSolver() {}
+bool AbductionSolver::getAbduct(const Node& goal,
+                                const TypeNode& grammarType,
+                                Node& abd)
+{
+  if (!options::produceAbducts())
+  {
+    const char* msg = "Cannot get abduct when produce-abducts options is off.";
+    throw ModalException(msg);
+  }
+  Trace("sygus-abduct") << "SmtEngine::getAbduct: goal " << goal << std::endl;
+  std::vector<Expr> easserts = d_parent->getExpandedAssertions();
+  std::vector<Node> axioms;
+  for (unsigned i = 0, size = easserts.size(); i < size; i++)
+  {
+    axioms.push_back(Node::fromExpr(easserts[i]));
+  }
+  std::vector<Node> asserts(axioms.begin(), axioms.end());
+  // must expand definitions
+  Node conjn = d_parent->expandDefinitions(goal);
+  // now negate
+  conjn = conjn.negate();
+  d_abdConj = conjn;
+  asserts.push_back(conjn);
+  std::string name("A");
+  Node aconj = quantifiers::SygusAbduct::mkAbductionConjecture(
+      name, asserts, axioms, grammarType);
+  // should be a quantified conjecture with one function-to-synthesize
+  Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1);
+  // remember the abduct-to-synthesize
+  d_sssf = aconj[0][0];
+  Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj
+                        << ", solving for " << d_sssf << std::endl;
+  // we generate a new smt engine to do the abduction query
+  initializeSubsolver(d_subsolver);
+  // get the logic
+  LogicInfo l = d_subsolver->getLogicInfo().getUnlockedCopy();
+  // enable everything needed for sygus
+  l.enableSygus();
+  d_subsolver->setLogic(l);
+  // assert the abduction query
+  d_subsolver->assertFormula(aconj.toExpr());
+  return getAbductInternal(abd);
+}
+
+bool AbductionSolver::getAbduct(const Node& goal, Node& abd)
+{
+  TypeNode grammarType;
+  return getAbduct(goal, grammarType, abd);
+}
+
+bool AbductionSolver::getAbductInternal(Node& abd)
+{
+  // should have initialized the subsolver by now
+  Assert(d_subsolver != nullptr);
+  Trace("sygus-abduct") << "  SmtEngine::getAbduct check sat..." << std::endl;
+  Result r = d_subsolver->checkSat();
+  Trace("sygus-abduct") << "  SmtEngine::getAbduct result: " << r << std::endl;
+  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+  {
+    // get the synthesis solution
+    std::map<Expr, Expr> sols;
+    d_subsolver->getSynthSolutions(sols);
+    Assert(sols.size() == 1);
+    Expr essf = d_sssf.toExpr();
+    std::map<Expr, Expr>::iterator its = sols.find(essf);
+    if (its != sols.end())
+    {
+      Trace("sygus-abduct")
+          << "SmtEngine::getAbduct: solution is " << its->second << std::endl;
+      abd = Node::fromExpr(its->second);
+      if (abd.getKind() == kind::LAMBDA)
+      {
+        abd = abd[1];
+      }
+      // get the grammar type for the abduct
+      Node agdtbv = d_sssf.getAttribute(SygusSynthFunVarListAttribute());
+      Assert(!agdtbv.isNull());
+      Assert(agdtbv.getKind() == kind::BOUND_VAR_LIST);
+      // convert back to original
+      // must replace formal arguments of abd with the free variables in the
+      // input problem that they correspond to.
+      std::vector<Node> vars;
+      std::vector<Node> syms;
+      SygusVarToTermAttribute sta;
+      for (const Node& bv : agdtbv)
+      {
+        vars.push_back(bv);
+        syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
+      }
+      abd = abd.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
+
+      // if check abducts option is set, we check the correctness
+      if (options::checkAbducts())
+      {
+        checkAbduct(abd);
+      }
+      return true;
+    }
+    Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!"
+                          << std::endl;
+    throw RecoverableModalException("Could not find solution for get-abduct.");
+  }
+  return false;
+}
+
+void AbductionSolver::checkAbduct(Node a)
+{
+  Assert(a.getType().isBoolean());
+  Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions"
+                        << std::endl;
+
+  std::vector<Expr> asserts = d_parent->getExpandedAssertions();
+  asserts.push_back(a.toExpr());
+
+  // two checks: first, consistent with assertions, second, implies negated goal
+  // is unsatisfiable.
+  for (unsigned j = 0; j < 2; j++)
+  {
+    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+                          << ": make new SMT engine" << std::endl;
+    // Start new SMT engine to check solution
+    std::unique_ptr<SmtEngine> abdChecker;
+    initializeSubsolver(abdChecker);
+    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+                          << ": asserting formulas" << std::endl;
+    for (const Expr& e : asserts)
+    {
+      abdChecker->assertFormula(e);
+    }
+    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+                          << ": check the assertions" << std::endl;
+    Result r = abdChecker->checkSat();
+    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+                          << ": result is " << r << std::endl;
+    std::stringstream serr;
+    bool isError = false;
+    if (j == 0)
+    {
+      if (r.asSatisfiabilityResult().isSat() != Result::SAT)
+      {
+        isError = true;
+        serr << "SmtEngine::checkAbduct(): produced solution cannot be shown "
+                "to be consisconsistenttent with assertions, result was "
+             << r;
+      }
+      Trace("check-abduct")
+          << "SmtEngine::checkAbduct: goal is " << d_abdConj << std::endl;
+      // add the goal to the set of assertions
+      Assert(!d_abdConj.isNull());
+      asserts.push_back(d_abdConj.toExpr());
+    }
+    else
+    {
+      if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+      {
+        isError = true;
+        serr << "SmtEngine::checkAbduct(): negated goal cannot be shown "
+                "unsatisfiable with produced solution, result was "
+             << r;
+      }
+    }
+    // did we get an unexpected result?
+    if (isError)
+    {
+      InternalError() << serr.str();
+    }
+  }
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h
new file mode 100644
index 000000000..2041b961d
--- /dev/null
+++ b/src/smt/abduction_solver.h
@@ -0,0 +1,120 @@
+/*********************                                                        */
+/*! \file abduction_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for abduction queries
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__ABDUCTION_SOLVER_H
+#define CVC4__SMT__ABDUCTION_SOLVER_H
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+/**
+ * A solver for abduction queries.
+ *
+ * This class is responsible for responding to get-abduct commands. It spawns
+ * a subsolver SmtEngine for a sygus conjecture that captures the abduction
+ * query, and implements supporting utility methods such as checkAbduct.
+ */
+class AbductionSolver
+{
+ public:
+  AbductionSolver(SmtEngine* parent);
+  ~AbductionSolver();
+  /**
+   * This method asks this SMT engine to find an abduct with respect to the
+   * current assertion stack (call it A) and the goal (call it B).
+   * 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 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
+   * 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);
+
+  /**
+   * 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);
+
+  /**
+   * Check that a solution to an abduction conjecture is indeed a solution.
+   *
+   * The check is made by determining that the assertions conjoined with the
+   * 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.
+   */
+  void checkAbduct(Node a);
+
+ private:
+  /**
+   * Get abduct internal.
+   *
+   * Get the next abduct from the internal subsolver d_subsolver. If
+   * successful, this method returns true and sets abd to that abduct.
+   *
+   * This method assumes d_subsolver has been initialized to do abduction
+   * problems.
+   */
+  bool getAbductInternal(Node& abd);
+  /** The parent SMT engine */
+  SmtEngine* d_parent;
+  /** The SMT engine subsolver
+   *
+   * This is a separate copy of the SMT engine which is used for making
+   * calls that cannot be answered by this copy of the SMT engine. An example
+   * of invoking this subsolver is the get-abduct command, where we wish to
+   * solve a sygus conjecture based on the current assertions. In particular,
+   * consider the input:
+   *   (assert A)
+   *   (get-abduct B)
+   * In the copy of the SMT engine where these commands are issued, we maintain
+   * A in the assertion stack. To solve the abduction problem, instead of
+   * modifying the assertion stack to remove A and add the sygus conjecture
+   * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the
+   * assertion stack unchaged. This copy of the SMT engine can be further
+   * queried for information regarding further solutions.
+   */
+  std::unique_ptr<SmtEngine> d_subsolver;
+  /**
+   * The conjecture of the current abduction problem. This expression is only
+   * valid while the parent SmtEngine is in mode SMT_MODE_ABDUCT.
+   */
+  Node d_abdConj;
+  /**
+   * If applicable, the function-to-synthesize that the subsolver is solving
+   * for. This is used for the get-abduct command.
+   */
+  Node d_sssf;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__ABDUCTION_SOLVER_H */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index e60f223b4..2e36190b4 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1555,7 +1555,8 @@ ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) : d_term(term) {}
 Expr ExpandDefinitionsCommand::getTerm() const { return d_term; }
 void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine)
 {
-  d_result = smtEngine->expandDefinitions(d_term);
+  Node t = Node::fromExpr(d_term);
+  d_result = smtEngine->expandDefinitions(t).toExpr();
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -1623,9 +1624,11 @@ void GetValueCommand::invoke(SmtEngine* smtEngine)
     for (int i = 0, size = d_terms.size(); i < size; i++)
     {
       Expr e = d_terms[i];
+      Node eNode = Node::fromExpr(e);
       Assert(nm == NodeManager::fromExprManager(e.getExprManager()));
-      Node request = Node::fromExpr(
-          options::expandDefinitions() ? smtEngine->expandDefinitions(e) : e);
+      Node request = options::expandDefinitions()
+                         ? smtEngine->expandDefinitions(eNode)
+                         : eNode;
       Node value = Node::fromExpr(result[i]);
       if (value.getType().isInteger() && request.getType() == nm->realType())
       {
@@ -2199,15 +2202,18 @@ void GetAbductCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
+    Node conjNode = Node::fromExpr(d_conj);
+    Node resn;
     if (d_sygus_grammar_type.isNull())
     {
-      d_resultStatus = smtEngine->getAbduct(d_conj, d_result);
+      d_resultStatus = smtEngine->getAbduct(conjNode, resn);
     }
     else
     {
-      d_resultStatus =
-          smtEngine->getAbduct(d_conj, d_sygus_grammar_type, d_result);
+      TypeNode gtype = TypeNode::fromType(d_sygus_grammar_type);
+      d_resultStatus = smtEngine->getAbduct(conjNode, gtype, resn);
     }
+    d_result = resn.toExpr();
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 12e0f443e..380878e41 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -81,6 +81,7 @@
 #include "proof/theory_proof.h"
 #include "proof/unsat_core.h"
 #include "prop/prop_engine.h"
+#include "smt/abduction_solver.h"
 #include "smt/command.h"
 #include "smt/command_list.h"
 #include "smt/defined_function.h"
@@ -101,7 +102,6 @@
 #include "theory/logic_info.h"
 #include "theory/quantifiers/fun_def_process.h"
 #include "theory/quantifiers/single_inv_partition.h"
-#include "theory/quantifiers/sygus/sygus_abduct.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -642,6 +642,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_proofManager(nullptr),
       d_rewriter(new theory::Rewriter()),
       d_definedFunctions(nullptr),
+      d_abductSolver(nullptr),
       d_assertionList(nullptr),
       d_assignments(nullptr),
       d_modelGlobalCommands(),
@@ -817,6 +818,12 @@ void SmtEngine::finishInit()
   }
   d_dumpCommands.clear();
 
+  // subsolvers
+  if (options::produceAbducts())
+  {
+    d_abductSolver.reset(new AbductionSolver(this));
+  }
+
   PROOF( ProofManager::currentPM()->setLogic(d_logic); );
   PROOF({
       for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
@@ -2161,18 +2168,17 @@ Expr SmtEngine::simplify(const Expr& ex)
   return n.toExpr();
 }
 
-Expr SmtEngine::expandDefinitions(const Expr& ex)
+Node SmtEngine::expandDefinitions(const Node& ex)
 {
   d_private->spendResource(ResourceManager::Resource::PreprocessStep);
 
-  Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
   Trace("smt") << "SMT expandDefinitions(" << ex << ")" << endl;
 
   // Substitute out any abstract values in ex.
-  Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
+  Node e = d_private->substituteAbstractValues(ex);
   if(options::typeChecking()) {
     // Ensure expr is type-checked at this point.
     e.getType(true);
@@ -2180,10 +2186,10 @@ Expr SmtEngine::expandDefinitions(const Expr& ex)
 
   unordered_map<Node, Node, NodeHashFunction> cache;
   Node n = d_private->getProcessAssertions()->expandDefinitions(
-      Node::fromExpr(e), cache, /* expandOnly = */ true);
-  n = postprocess(n, TypeNode::fromType(e.getType()));
+      e, cache, /* expandOnly = */ true);
+  n = postprocess(n, e.getType());
 
-  return n.toExpr();
+  return n;
 }
 
 // TODO(#1108): Simplify the error reporting of this method.
@@ -2985,69 +2991,11 @@ void SmtEngine::checkInterpol(Expr interpol,
 {
 }
 
-void SmtEngine::checkAbduct(Expr a)
+void SmtEngine::checkAbduct(Node a)
 {
   Assert(a.getType().isBoolean());
-  Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions"
-                        << std::endl;
-
-  std::vector<Expr> asserts = getExpandedAssertions();
-  asserts.push_back(a);
-
-  // two checks: first, consistent with assertions, second, implies negated goal
-  // is unsatisfiable.
-  for (unsigned j = 0; j < 2; j++)
-  {
-    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
-                          << ": make new SMT engine" << std::endl;
-    // Start new SMT engine to check solution
-    SmtEngine abdChecker(d_exprManager, &d_options);
-    abdChecker.setIsInternalSubsolver();
-    abdChecker.setLogic(getLogicInfo());
-    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
-                          << ": asserting formulas" << std::endl;
-    for (const Expr& e : asserts)
-    {
-      abdChecker.assertFormula(e);
-    }
-    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
-                          << ": check the assertions" << std::endl;
-    Result r = abdChecker.checkSat();
-    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
-                          << ": result is " << r << endl;
-    std::stringstream serr;
-    bool isError = false;
-    if (j == 0)
-    {
-      if (r.asSatisfiabilityResult().isSat() != Result::SAT)
-      {
-        isError = true;
-        serr << "SmtEngine::checkAbduct(): produced solution cannot be shown "
-                "to be consisconsistenttent with assertions, result was "
-             << r;
-      }
-      Trace("check-abduct")
-          << "SmtEngine::checkAbduct: goal is " << d_abdConj << std::endl;
-      // add the goal to the set of assertions
-      Assert(!d_abdConj.isNull());
-      asserts.push_back(d_abdConj);
-    }
-    else
-    {
-      if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
-      {
-        isError = true;
-        serr << "SmtEngine::checkAbduct(): negated goal cannot be shown "
-                "unsatisfiable with produced solution, result was "
-             << r;
-      }
-    }
-    // did we get an unexpected result?
-    if (isError)
-    {
-      InternalError() << serr.str();
-    }
-  }
+  // check it with the abduction solver
+  return d_abductSolver->checkAbduct(a);
 }
 
 // TODO(#1108): Simplify the error reporting of this method.
@@ -3217,54 +3165,11 @@ bool SmtEngine::getInterpol(const Expr& conj, Expr& interpol)
   return getInterpol(conj, grammarType, interpol);
 }
 
-bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
+bool SmtEngine::getAbduct(const Node& conj,
+                          const TypeNode& grammarType,
+                          Node& abd)
 {
-  SmtScope smts(this);
-
-  if (!options::produceAbducts())
-  {
-    const char* msg = "Cannot get abduct when produce-abducts options is off.";
-    throw ModalException(msg);
-  }
-  Trace("sygus-abduct") << "SmtEngine::getAbduct: conjecture " << conj
-                        << std::endl;
-  std::vector<Expr> easserts = getExpandedAssertions();
-  std::vector<Node> axioms;
-  for (unsigned i = 0, size = easserts.size(); i < size; i++)
-  {
-    axioms.push_back(Node::fromExpr(easserts[i]));
-  }
-  std::vector<Node> asserts(axioms.begin(), axioms.end());
-  // negate the conjecture
-  Node conjn = Node::fromExpr(conj);
-  // must expand definitions
-  std::unordered_map<Node, Node, NodeHashFunction> cache;
-  conjn = d_private->getProcessAssertions()->expandDefinitions(conjn, cache);
-  // now negate
-  conjn = conjn.negate();
-  d_abdConj = conjn.toExpr();
-  asserts.push_back(conjn);
-  std::string name("A");
-  Node aconj = theory::quantifiers::SygusAbduct::mkAbductionConjecture(
-      name, asserts, axioms, TypeNode::fromType(grammarType));
-  // should be a quantified conjecture with one function-to-synthesize
-  Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1);
-  // remember the abduct-to-synthesize
-  d_sssf = aconj[0][0].toExpr();
-  Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj
-                        << ", solving for " << d_sssf << std::endl;
-  // we generate a new smt engine to do the abduction query
-  d_subsolver.reset(
-      new SmtEngine(NodeManager::currentNM()->toExprManager(), &d_options));
-  d_subsolver->setIsInternalSubsolver();
-  // get the logic
-  LogicInfo l = d_logic.getUnlockedCopy();
-  // enable everything needed for sygus
-  l.enableSygus();
-  d_subsolver->setLogic(l);
-  // assert the abduction query
-  d_subsolver->assertFormula(aconj.toExpr());
-  if (getAbductInternal(abd))
+  if (d_abductSolver->getAbduct(conj, grammarType, abd))
   {
     // successfully generated an abduct, update to abduct state
     d_smtMode = SMT_MODE_ABDUCT;
@@ -3275,68 +3180,9 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
   return false;
 }
 
-bool SmtEngine::getAbductInternal(Expr& abd)
+bool SmtEngine::getAbduct(const Node& conj, Node& abd)
 {
-  // should have initialized the subsolver by now
-  Assert(d_subsolver != nullptr);
-  Trace("sygus-abduct") << "  SmtEngine::getAbduct check sat..." << std::endl;
-  Result r = d_subsolver->checkSat();
-  Trace("sygus-abduct") << "  SmtEngine::getAbduct result: " << r << std::endl;
-  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
-  {
-    // get the synthesis solution
-    std::map<Expr, Expr> sols;
-    d_subsolver->getSynthSolutions(sols);
-    Assert(sols.size() == 1);
-    std::map<Expr, Expr>::iterator its = sols.find(d_sssf);
-    if (its != sols.end())
-    {
-      Trace("sygus-abduct")
-          << "SmtEngine::getAbduct: solution is " << its->second << std::endl;
-      Node abdn = Node::fromExpr(its->second);
-      if (abdn.getKind() == kind::LAMBDA)
-      {
-        abdn = abdn[1];
-      }
-      // get the grammar type for the abduct
-      Node af = Node::fromExpr(d_sssf);
-      Node agdtbv = af.getAttribute(theory::SygusSynthFunVarListAttribute());
-      Assert(!agdtbv.isNull());
-      Assert(agdtbv.getKind() == kind::BOUND_VAR_LIST);
-      // convert back to original
-      // must replace formal arguments of abd with the free variables in the
-      // input problem that they correspond to.
-      std::vector<Node> vars;
-      std::vector<Node> syms;
-      SygusVarToTermAttribute sta;
-      for (const Node& bv : agdtbv)
-      {
-        vars.push_back(bv);
-        syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
-      }
-      abdn =
-          abdn.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
-
-      // convert to expression
-      abd = abdn.toExpr();
-
-      // if check abducts option is set, we check the correctness
-      if (options::checkAbducts())
-      {
-        checkAbduct(abd);
-      }
-      return true;
-    }
-    Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!"
-                          << std::endl;
-    throw RecoverableModalException("Could not find solution for get-abduct.");
-  }
-  return false;
-}
-
-bool SmtEngine::getAbduct(const Expr& conj, Expr& abd)
-{
-  Type grammarType;
+  TypeNode grammarType;
   return getAbduct(conj, grammarType, abd);
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 8db8eadd5..f6b1d08bf 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -91,23 +91,25 @@ namespace prop {
 /* -------------------------------------------------------------------------- */
 
 namespace smt {
-  /**
-   * Representation of a defined function.  We keep these around in
-   * SmtEngine to permit expanding definitions late (and lazily), to
-   * support getValue() over defined functions, to support user output
-   * in terms of defined functions, etc.
-   */
-  class DefinedFunction;
-
-  struct SmtEngineStatistics;
-  class SmtEnginePrivate;
-  class SmtScope;
-  class ProcessAssertions;
-
-  ProofManager* currentProofManager();
-
-  struct CommandCleanup;
-  typedef context::CDList<Command*, CommandCleanup> CommandList;
+/** Subsolvers */
+class AbductionSolver;
+/**
+ * Representation of a defined function.  We keep these around in
+ * SmtEngine to permit expanding definitions late (and lazily), to
+ * support getValue() over defined functions, to support user output
+ * in terms of defined functions, etc.
+ */
+class DefinedFunction;
+
+struct SmtEngineStatistics;
+class SmtEnginePrivate;
+class SmtScope;
+class ProcessAssertions;
+
+ProofManager* currentProofManager();
+
+struct CommandCleanup;
+typedef context::CDList<Command*, CommandCleanup> CommandList;
 }/* CVC4::smt namespace */
 
 /* -------------------------------------------------------------------------- */
@@ -508,7 +510,7 @@ class CVC4_PUBLIC SmtEngine
    *
    * @throw TypeCheckingException, LogicException, UnsafeInterruptException
    */
-  Expr expandDefinitions(const Expr& e);
+  Node expandDefinitions(const Node& e);
 
   /**
    * Get the assigned value of an expr (only if immediately preceded by a SAT
@@ -660,10 +662,10 @@ class CVC4_PUBLIC SmtEngine
    * This method invokes a separate copy of the SMT engine for solving the
    * corresponding sygus problem for generating such a solution.
    */
-  bool getAbduct(const Expr& conj, const Type& grammarType, Expr& abd);
+  bool getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd);
 
   /** Same as above, but without user-provided grammar restrictions */
-  bool getAbduct(const Expr& conj, Expr& abd);
+  bool getAbduct(const Node& conj, Node& abd);
 
   /**
    * Get list of quantified formulas that were instantiated on the last call
@@ -898,6 +900,13 @@ class CVC4_PUBLIC SmtEngine
 
   /** Get the resource manager of this SMT engine */
   ResourceManager* getResourceManager();
+
+  /**
+   * Get expanded assertions.
+   *
+   * Return the set of assertions, after expanding definitions.
+   */
+  std::vector<Expr> getExpandedAssertions();
   /* .......................................................................  */
  private:
   /* .......................................................................  */
@@ -994,7 +1003,7 @@ class CVC4_PUBLIC SmtEngine
    * with the abduct and the goal is UNSAT. If these criteria are not met, an
    * internal error is thrown.
    */
-  void checkAbduct(Expr a);
+  void checkAbduct(Node a);
 
   /**
    * Postprocess a value for output to the user.  Involves doing things
@@ -1111,30 +1120,12 @@ class CVC4_PUBLIC SmtEngine
                               Expr func);
 
   /**
-   * Get abduct internal.
-   *
-   * Get the next abduct from the internal subsolver d_subsolver. If
-   * successful, this method returns true and sets abd to that abduct.
-   *
-   * This method assumes d_subsolver has been initialized to do abduction
-   * problems.
-   */
-  bool getAbductInternal(Expr& abd);
-
-  /**
    * Helper method to obtain both the heap and nil from the solver. Returns a
    * std::pair where the first element is the heap expression and the second
    * element is the nil expression.
    */
   std::pair<Expr, Expr> getSepHeapAndNilExpr();
 
-  /**
-   * Get expanded assertions.
-   *
-   * Return the set of assertions, after expanding definitions.
-   */
-  std::vector<Expr> getExpandedAssertions();
-
   /* Members -------------------------------------------------------------- */
 
   /** Solver instance that owns this SmtEngine instance. */
@@ -1171,35 +1162,8 @@ class CVC4_PUBLIC SmtEngine
   /** An index of our defined functions */
   DefinedFunctionMap* d_definedFunctions;
 
-  /** The SMT engine subsolver
-   *
-   * This is a separate copy of the SMT engine which is used for making
-   * calls that cannot be answered by this copy of the SMT engine. An example
-   * of invoking this subsolver is the get-abduct command, where we wish to
-   * solve a sygus conjecture based on the current assertions. In particular,
-   * consider the input:
-   *   (assert A)
-   *   (get-abduct B)
-   * In the copy of the SMT engine where these commands are issued, we maintain
-   * A in the assertion stack. To solve the abduction problem, instead of
-   * modifying the assertion stack to remove A and add the sygus conjecture
-   * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the
-   * assertion stack unchaged. This copy of the SMT engine can be further
-   * queried for information regarding further solutions.
-   */
-  std::unique_ptr<SmtEngine> d_subsolver;
-
-  /**
-   * If applicable, the function-to-synthesize that the subsolver is solving
-   * for. This is used for the get-abduct command.
-   */
-  Expr d_sssf;
-
-  /**
-   * The conjecture of the current abduction problem. This expression is only
-   * valid while we are in mode SMT_MODE_ABDUCT.
-   */
-  Expr d_abdConj;
+  /** The solver for abduction queries */
+  std::unique_ptr<smt::AbductionSolver> d_abductSolver;
 
   /**
    * The assertion list (before any conversion) for supporting
diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index e95b66bd7..8ff0f8db2 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -232,8 +232,7 @@ Node mkSygusTerm(const DType& dt,
         // ensures we don't try to expand e.g. bitvector extract operators,
         // whose type is undefined, and thus should not be passed to
         // expandDefinitions.
-        opn = Node::fromExpr(
-            smt::currentSmtEngine()->expandDefinitions(op.toExpr()));
+        opn = smt::currentSmtEngine()->expandDefinitions(op);
         opn = Rewriter::rewrite(opn);
         opn = eliminatePartialOperators(opn);
         SygusOpRewrittenAttribute sora;