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.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 64f9dbd358014d4f0c54f5b902dab7eb150de3dd..eef2b7052aaef32a9a7fdd7c40417706816bfc5d 100644 (file)
--- 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 91ff522b5ee21d46a3254bed2c825cfe9a8998c0..e5b95d6566eb76cc9dff8e8fd67e90fa8228cbe9 100644 (file)
--- 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 f51b6759bb05a385bf0874c08bdcb8dca5644acc..5a8c41652cce5a65db406d33aa3d3c5293f79bf4 100644 (file)
--- 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