From 64a8b1b205ccc793865bacf2b4388c534dc2f16d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 4 Aug 2020 18:27:27 -0500
Subject: [PATCH] Fixes for getInterpolant and getAbduct API methods (#4846)

This fixes three issues in the getInterpolant method in the API, which was also copied to the getAbduct method:
(1) Use Node not Expr
(2) Must set up ExprManager scope
(3) The wrong solver pointer was passed to the returned term, which was causing segfaults on all abduction regressions.

We should also consider changing the interface of this method to return the term instead of a Boolean. This could be done as future work.

This fixes regress1.
---
 src/api/cvc4cpp.cpp    | 20 ++++++++++++--------
 src/smt/smt_engine.cpp | 10 +++++-----
 src/smt/smt_engine.h   |  6 ++++--
 3 files changed, 21 insertions(+), 15 deletions(-)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 64f9dbd35..eef2b7052 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -5055,11 +5055,12 @@ void Solver::pop(uint32_t nscopes) const
 bool Solver::getInterpolant(Term conj, Term& output) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  Expr result;
-  bool success = d_smtEngine->getInterpol(conj.d_node->toExpr(), result);
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  Node result;
+  bool success = d_smtEngine->getInterpol(*conj.d_node, result);
   if (success)
   {
-    output = Term(output.d_solver, result);
+    output = Term(this, result);
   }
   return success;
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -5068,12 +5069,13 @@ bool Solver::getInterpolant(Term conj, Term& output) const
 bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  Expr result;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  Node result;
   bool success = d_smtEngine->getInterpol(
-      conj.d_node->toExpr(), *g.resolve().d_type, result);
+      *conj.d_node, TypeNode::fromType(*g.resolve().d_type), result);
   if (success)
   {
-    output = Term(output.d_solver, result);
+    output = Term(this, result);
   }
   return success;
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -5082,11 +5084,12 @@ bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const
 bool Solver::getAbduct(Term conj, Term& output) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
   Node result;
   bool success = d_smtEngine->getAbduct(*conj.d_node, result);
   if (success)
   {
-    output = Term(output.d_solver, result);
+    output = Term(this, result);
   }
   return success;
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -5095,12 +5098,13 @@ bool Solver::getAbduct(Term conj, Term& output) const
 bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
   Node result;
   bool success = d_smtEngine->getAbduct(
       *conj.d_node, TypeNode::fromType(*g.resolve().d_type), result);
   if (success)
   {
-    output = Term(output.d_solver, result);
+    output = Term(this, result);
   }
   return success;
   CVC4_API_SOLVER_TRY_CATCH_END;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 91ff522b5..e5b95d656 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2766,16 +2766,16 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
   }
 }
 
-bool SmtEngine::getInterpol(const Expr& conj,
-                            const Type& grammarType,
-                            Expr& interpol)
+bool SmtEngine::getInterpol(const Node& conj,
+                            const TypeNode& grammarType,
+                            Node& interpol)
 {
   return false;
 }
 
-bool SmtEngine::getInterpol(const Expr& conj, Expr& interpol)
+bool SmtEngine::getInterpol(const Node& conj, Node& interpol)
 {
-  Type grammarType;
+  TypeNode grammarType;
   return getInterpol(conj, grammarType, interpol);
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f51b6759b..5a8c41652 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -648,10 +648,12 @@ 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 getInterpol(const Expr& conj, const Type& grammarType, Expr& interpol);
+  bool getInterpol(const Node& conj,
+                   const TypeNode& grammarType,
+                   Node& interpol);
 
   /** Same as above, but without user-provided grammar restrictions */
-  bool getInterpol(const Expr& conj, Expr& interpol);
+  bool getInterpol(const Node& conj, Node& interpol);
 
   /**
    * This method asks this SMT engine to find an abduct with respect to the
-- 
2.30.2