Split SygusSolver from SmtEngine (#4891)

This is the solver for standard SyGuS queries. Notice it now depends only on SmtSolver and not SmtEngine.

This PR updates Expr -> Node for the sygus interface in SmtEngine.

SmtEnginePrivate is no longer needed and is deleted with this PR.

1 files changed, 3 insertions, 4 deletions

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 01e2a4f0f..2a6346c18 100644
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -89,16 +89,15 @@ bool AbductionSolver::getAbductInternal(Node& abd)
   if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
   {
     // get the synthesis solution
-    std::map<Expr, Expr> sols;
+    std::map<Node, Node> sols;
     d_subsolver->getSynthSolutions(sols);
     Assert(sols.size() == 1);
-    Expr essf = d_sssf.toExpr();
-    std::map<Expr, Expr>::iterator its = sols.find(essf);
+    std::map<Node, Node>::iterator its = sols.find(d_sssf);
     if (its != sols.end())
     {
       Trace("sygus-abduct")
           << "SmtEngine::getAbduct: solution is " << its->second << std::endl;
-      abd = Node::fromExpr(its->second);
+      abd = its->second;
       if (abd.getKind() == kind::LAMBDA)
       {
         abd = abd[1];