Add support for incremental + interpolants (#7853)

Adds support for incrementality + get-interpol, including the get-interpol-next command.

22 files changed, 441 insertions, 58 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 4c43dbd5b..be5f1017d 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7579,9 +7579,14 @@ bool Solver::getInterpolant(const Term& conj, Term& output) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
+  CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols
+                 != options::ProduceInterpols::NONE)
+      << "Cannot get interpolant unless interpolants are enabled (try "
+         "--produce-interpols=mode)";
   //////// all checks before this line
   Node result;
-  bool success = d_slv->getInterpol(*conj.d_node, result);
+  TypeNode nullType;
+  bool success = d_slv->getInterpolant(*conj.d_node, nullType, result);
   if (success)
   {
     output = Term(this, result);
@@ -7597,10 +7602,36 @@ bool Solver::getInterpolant(const Term& conj,
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
+  CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols
+                 != options::ProduceInterpols::NONE)
+      << "Cannot get interpolant unless interpolants are enabled (try "
+         "--produce-interpols=mode)";
   //////// all checks before this line
   Node result;
   bool success =
-      d_slv->getInterpol(*conj.d_node, *grammar.resolve().d_type, result);
+      d_slv->getInterpolant(*conj.d_node, *grammar.resolve().d_type, result);
+  if (success)
+  {
+    output = Term(this, result);
+  }
+  return success;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+bool Solver::getInterpolantNext(Term& output) const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols
+                 != options::ProduceInterpols::NONE)
+      << "Cannot get interpolant unless interpolants are enabled (try "
+         "--produce-interpols=mode)";
+  CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving)
+      << "Cannot get next interpolant when not solving incrementally (try "
+         "--incremental)";
+  //////// all checks before this line
+  Node result;
+  bool success = d_slv->getInterpolantNext(result);
   if (success)
   {
     output = Term(this, result);
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 7e4dc3cc8..21f51a9c8 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4427,8 +4427,9 @@ class CVC5_EXPORT Solver
    *
    *     (get-interpol <conj>)
    *
-   * Requires to enable option
-   * :ref:`produce-interpols <lbl-option-produce-interpols>`.
+   * Requires option
+   * :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a
+   * mode different from `none`.
    * \endverbatim
    *
    * @param conj the conjecture term
@@ -4448,8 +4449,9 @@ class CVC5_EXPORT Solver
    *
    *     (get-interpol <conj> <grammar>)
    *
-   * Requires to enable option
-   * :ref:`produce-interpols <lbl-option-produce-interpols>`.
+   * Requires option
+   * :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a
+   * mode different from `none`.
    * \endverbatim
    *
    * @param conj the conjecture term
@@ -4461,6 +4463,31 @@ class CVC5_EXPORT Solver
   bool getInterpolant(const Term& conj, Grammar& grammar, Term& output) const;
 
   /**
+   * Get the next interpolant. Can only be called immediately after a successful
+   * call to get-interpol or get-interpol-next. Is guaranteed to produce a
+   * syntactically different interpolant wrt the last returned interpolant if
+   * successful.
+   *
+   * SMT-LIB:
+   *
+   * \verbatim embed:rst:leading-asterisk
+   * .. code:: smtlib
+   *
+   *     (get-interpol-next)
+   *
+   * Requires to enable incremental mode, and option
+   * :ref:`produce-interpols <lbl-option-produce-interpols>` to be set to a
+   * mode different from `none`.
+   * \endverbatim
+   *
+   * @param output a Term I such that A->I and I->B are valid, where A is the
+   *        current set of assertions and B is given in the input by conj
+   *        on the last call to getInterpolant.
+   * @return true if it gets interpolant @f$C@f$ successfully, false otherwise
+   */
+  bool getInterpolantNext(Term& output) const;
+
+  /**
    * Get an abduct.
    *
    * SMT-LIB:
diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 32ddf0691..5e2ac0972 100644
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -2183,7 +2183,7 @@ public class Solver implements IPointer, AutoCloseable
    * {@code
    * ( get-interpol <conj> )
    * }
-   * Requires to enable option 'produce-interpols'.
+   * Requires 'produce-interpols' to be set to a mode different from 'none'.
    * @param conj the conjecture term
    * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the
    *        current set of assertions and B is given in the input by conj.
@@ -2202,7 +2202,7 @@ public class Solver implements IPointer, AutoCloseable
    * {@code
    * ( get-interpol <conj> <g> )
    * }
-   * Requires to enable option 'produce-interpols'.
+   * Requires 'produce-interpols' to be set to a mode different from 'none'.
    * @param conj the conjecture term
    * @param grammar the grammar for the interpolant I
    * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the
@@ -2218,6 +2218,35 @@ public class Solver implements IPointer, AutoCloseable
       long pointer, long conjPointer, long grammarPointer, long outputPointer);
 
   /**
+   * Get the next interpolant. Can only be called immediately after a successful
+   * call to get-interpol or get-interpol-next. Is guaranteed to produce a
+   * syntactically different interpolant wrt the last returned interpolant if
+   * successful.
+   *
+   * SMT-LIB:
+   *
+   * \verbatim embed:rst:leading-asterisk
+   * .. code:: smtlib
+   *
+   *     (get-interpol-next)
+   *
+   * Requires to enable incremental mode, and option 'produce-interpols' to be
+   * set to a mode different from 'none'.
+   * \endverbatim
+   *
+   * @param output a Term I such that {@code A->I} and {@code I->B} are valid,
+   *        where A is the current set of assertions and B is given in the input
+   *        by conj on the last call to getInterpolant.
+   * @return true if it gets interpolant @f$C@f$ successfully, false otherwise
+   */
+  public boolean getInterpolantNext(Term output)
+  {
+    return getInterpolantNext(pointer, output.getPointer());
+  }
+
+  private native boolean getInterpolantNext(long pointer, long outputPointer);
+
+  /**
    * Get an abduct.
    * SMT-LIB:
    * {@code
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index 524c52796..705803c12 100644
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -2245,6 +2245,21 @@ Java_io_github_cvc5_api_Solver_getInterpolant__JJJJ(JNIEnv* env,
 
 /*
  * Class:     io_github_cvc5_api_Solver
+ * Method:    getInterpolantNext
+ * Signature: (JJ)Z
+ */
+JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getInterpolantNext(
+    JNIEnv* env, jobject, jlong pointer, jlong outputPointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Solver* solver = reinterpret_cast<Solver*>(pointer);
+  Term* output = reinterpret_cast<Term*>(outputPointer);
+  return (jboolean)solver->getInterpolantNext(*output);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     io_github_cvc5_api_Solver
  * Method:    getAbduct
  * Signature: (JJJ)Z
  */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 31171b278..fafda041a 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1022,6 +1022,10 @@ extendedCommand[std::unique_ptr<cvc5::Command>* cmd]
     {
       cmd->reset(new GetInterpolCommand(name, e, g));
     }
+  | GET_INTERPOL_NEXT_TOK {
+      PARSER_STATE->checkThatLogicIsSet();
+      cmd->reset(new GetInterpolNextCommand);
+    }
   | DECLARE_HEAP LPAREN_TOK
     sortSymbol[t, CHECK_DECLARED]
     sortSymbol[s, CHECK_DECLARED]
@@ -2244,6 +2248,7 @@ GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
 GET_ABDUCT_TOK : 'get-abduct';
 GET_ABDUCT_NEXT_TOK : 'get-abduct-next';
 GET_INTERPOL_TOK : 'get-interpol';
+GET_INTERPOL_NEXT_TOK : 'get-interpol-next';
 DECLARE_HEAP : 'declare-heap';
 DECLARE_POOL : 'declare-pool';
 
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index a4ff10014..12b52e284 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -405,6 +405,11 @@ void Printer::toStreamCmdGetInterpol(std::ostream& out,
   printUnknownCommand(out, "get-interpol");
 }
 
+void Printer::toStreamCmdGetInterpolNext(std::ostream& out) const
+{
+  printUnknownCommand(out, "get-interpol-next");
+}
+
 void Printer::toStreamCmdGetAbduct(std::ostream& out,
                                    const std::string& name,
                                    Node conj,
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 74eb8970b..2a9283001 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -200,6 +200,9 @@ class Printer
                                       Node conj,
                                       TypeNode sygusType) const;
 
+  /** Print get-interpol-next command */
+  virtual void toStreamCmdGetInterpolNext(std::ostream& out) const;
+
   /** Print get-abduct command */
   virtual void toStreamCmdGetAbduct(std::ostream& out,
                                     const std::string& name,
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index e6c99c707..69da5d03d 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1917,6 +1917,11 @@ void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out,
   out << ')' << std::endl;
 }
 
+void Smt2Printer::toStreamCmdGetInterpolNext(std::ostream& out) const
+{
+  out << "(get-interpol-next)" << std::endl;
+}
+
 void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
                                        const std::string& name,
                                        Node conj,
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index aad3948fe..bf6c20d40 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -174,6 +174,9 @@ class Smt2Printer : public cvc5::Printer
                               Node conj,
                               TypeNode sygusType) const override;
 
+  /** Print get-interpol-next command */
+  void toStreamCmdGetInterpolNext(std::ostream& out) const override;
+
   /** Print get-abduct command */
   void toStreamCmdGetAbduct(std::ostream& out,
                             const std::string& name,
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 8161dfb49..e22c39d0e 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2007,6 +2007,9 @@ void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
+    // we must remember the name of the interpolant, in case get-interpol-next
+    // is called later.
+    sm->setLastSynthName(d_name);
     if (d_sygus_grammar == nullptr)
     {
       d_resultStatus = solver->getInterpolant(d_conj, d_result);
@@ -2070,6 +2073,72 @@ void GetInterpolCommand::toStream(std::ostream& out,
 }
 
 /* -------------------------------------------------------------------------- */
+/* class GetInterpolNextCommand */
+/* -------------------------------------------------------------------------- */
+
+GetInterpolNextCommand::GetInterpolNextCommand() : d_resultStatus(false) {}
+
+api::Term GetInterpolNextCommand::getResult() const { return d_result; }
+
+void GetInterpolNextCommand::invoke(api::Solver* solver, SymbolManager* sm)
+{
+  try
+  {
+    // Get the name of the interpolant from the symbol manager
+    d_name = sm->getLastSynthName();
+    d_resultStatus = solver->getInterpolantNext(d_result);
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+void GetInterpolNextCommand::printResult(std::ostream& out) const
+{
+  if (!ok())
+  {
+    this->Command::printResult(out);
+  }
+  else
+  {
+    options::ioutils::Scope scope(out);
+    options::ioutils::applyDagThresh(out, 0);
+    if (d_resultStatus)
+    {
+      out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+          << std::endl;
+    }
+    else
+    {
+      out << "none" << std::endl;
+    }
+  }
+}
+
+Command* GetInterpolNextCommand::clone() const
+{
+  GetInterpolNextCommand* c = new GetInterpolNextCommand;
+  c->d_result = d_result;
+  c->d_resultStatus = d_resultStatus;
+  return c;
+}
+
+std::string GetInterpolNextCommand::getCommandName() const
+{
+  return "get-interpol-next";
+}
+
+void GetInterpolNextCommand::toStream(std::ostream& out,
+                                      int toDepth,
+                                      size_t dag,
+                                      Language language) const
+{
+  Printer::getPrinter(language)->toStreamCmdGetInterpolNext(out);
+}
+
+/* -------------------------------------------------------------------------- */
 /* class GetAbductCommand                                                     */
 /* -------------------------------------------------------------------------- */
 
diff --git a/src/smt/command.h b/src/smt/command.h
index 68ff7ffab..9a4b04196 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1058,6 +1058,35 @@ class CVC5_EXPORT GetInterpolCommand : public Command
   api::Term d_result;
 }; /* class GetInterpolCommand */
 
+/** The command (get-interpol-next) */
+class CVC5_EXPORT GetInterpolNextCommand : public Command
+{
+ public:
+  GetInterpolNextCommand();
+  /**
+   * Get the result of the query, which is the solution to the interpolation
+   * query.
+   */
+  api::Term getResult() const;
+
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
+  void printResult(std::ostream& out) const override;
+  Command* clone() const override;
+  std::string getCommandName() const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
+
+ protected:
+  /** The name of the interpolation predicate */
+  std::string d_name;
+  /** the return status of the command */
+  bool d_resultStatus;
+  /** the return expression of the command */
+  api::Term d_result;
+};
+
 /** The command (get-abduct s B (G)?)
  *
  * This command asks for an abduct from the current set of assertions and
@@ -1134,7 +1163,7 @@ class CVC5_EXPORT GetAbductNextCommand : public Command
   bool d_resultStatus;
   /** the return expression of the command */
   api::Term d_result;
-}; /* class GetAbductCommand */
+};
 
 class CVC5_EXPORT GetQuantifierEliminationCommand : public Command
 {
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index 20be53e85..97d3a4224 100644
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -36,10 +36,10 @@ InterpolationSolver::InterpolationSolver(Env& env) : EnvObj(env) {}
 
 InterpolationSolver::~InterpolationSolver() {}
 
-bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
-                                      const Node& conj,
-                                      const TypeNode& grammarType,
-                                      Node& interpol)
+bool InterpolationSolver::getInterpolant(const std::vector<Node>& axioms,
+                                         const Node& conj,
+                                         const TypeNode& grammarType,
+                                         Node& interpol)
 {
   if (options().smt.produceInterpols == options::ProduceInterpols::NONE)
   {
@@ -54,8 +54,8 @@ bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
   conjn = rewrite(conjn);
   std::string name("__internal_interpol");
 
-  quantifiers::SygusInterpol interpolSolver(d_env);
-  if (interpolSolver.solveInterpolation(
+  d_subsolver = std::make_unique<quantifiers::SygusInterpol>(d_env);
+  if (d_subsolver->solveInterpolation(
           name, axioms, conjn, grammarType, interpol))
   {
     if (options().smt.checkInterpols)
@@ -67,12 +67,12 @@ bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
   return false;
 }
 
-bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
-                                      const Node& conj,
-                                      Node& interpol)
+bool InterpolationSolver::getInterpolantNext(Node& interpol)
 {
-  TypeNode grammarType;
-  return getInterpol(axioms, conj, grammarType, interpol);
+  // should already have initialized a subsolver, since we are immediately
+  // preceeded by a successful call to get-interpol(-next).
+  Assert(d_subsolver != nullptr);
+  return d_subsolver->solveInterpolationNext(interpol);
 }
 
 void InterpolationSolver::checkInterpol(Node interpol,
diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h
index 39a241816..d1f1c7fd8 100644
--- a/src/smt/interpolation_solver.h
+++ b/src/smt/interpolation_solver.h
@@ -23,6 +23,13 @@
 #include "smt/env_obj.h"
 
 namespace cvc5 {
+
+namespace theory {
+namespace quantifiers {
+class SygusInterpol;
+}
+}  // namespace theory
+
 namespace smt {
 
 /**
@@ -55,19 +62,24 @@ class InterpolationSolver : protected EnvObj
    * This method invokes a separate copy of the SMT engine for solving the
    * corresponding sygus problem for generating such a solution.
    */
-  bool getInterpol(const std::vector<Node>& axioms,
-                   const Node& conj,
-                   const TypeNode& grammarType,
-                   Node& interpol);
+  bool getInterpolant(const std::vector<Node>& axioms,
+                      const Node& conj,
+                      const TypeNode& grammarType,
+                      Node& interpol);
 
   /**
-   * Same as above, but without user-provided grammar restrictions. A default
-   * grammar is chosen internally using the sygus grammar constructor utility.
+   * Get next interpolant. This can only be called immediately after a
+   * successful call to getInterpolant or getInterpolantNext.
+   *
+   * Returns true if an interpolant was found, and sets interpol to the
+   * interpolant.
+   *
+   * This method reuses the subsolver initialized by the last call to
+   * getInterpolant.
    */
-  bool getInterpol(const std::vector<Node>& axioms,
-                   const Node& conj,
-                   Node& interpol);
+  bool getInterpolantNext(Node& interpol);
 
+ private:
   /**
    * Check that a solution to an interpolation problem is indeed a solution.
    *
@@ -78,6 +90,9 @@ class InterpolationSolver : protected EnvObj
   void checkInterpol(Node interpol,
                      const std::vector<Node>& easserts,
                      const Node& conj);
+
+  /** The subsolver */
+  std::unique_ptr<theory::quantifiers::SygusInterpol> d_subsolver;
 };
 
 }  // namespace smt
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 2df3eafa1..e7f2e2069 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1632,25 +1632,35 @@ Node SolverEngine::getQuantifierElimination(Node q, bool doFull, bool strict)
       *d_asserts, q, doFull, d_isInternalSubsolver);
 }
 
-bool SolverEngine::getInterpol(const Node& conj,
-                               const TypeNode& grammarType,
-                               Node& interpol)
+bool SolverEngine::getInterpolant(const Node& conj,
+                                  const TypeNode& grammarType,
+                                  Node& interpol)
 {
   SolverEngineScope smts(this);
   finishInit();
   std::vector<Node> axioms = getExpandedAssertions();
   bool success =
-      d_interpolSolver->getInterpol(axioms, conj, grammarType, interpol);
+      d_interpolSolver->getInterpolant(axioms, conj, grammarType, interpol);
   // notify the state of whether the get-interpol call was successfuly, which
   // impacts the SMT mode.
   d_state->notifyGetInterpol(success);
   return success;
 }
 
-bool SolverEngine::getInterpol(const Node& conj, Node& interpol)
+bool SolverEngine::getInterpolantNext(Node& interpol)
 {
-  TypeNode grammarType;
-  return getInterpol(conj, grammarType, interpol);
+  SolverEngineScope smts(this);
+  finishInit();
+  if (d_state->getMode() != SmtMode::INTERPOL)
+  {
+    throw RecoverableModalException(
+        "Cannot get-interpol-next unless immediately preceded by a successful "
+        "call to get-interpol(-next).");
+  }
+  bool success = d_interpolSolver->getInterpolantNext(interpol);
+  // notify the state of whether the get-interpolant-next call was successful
+  d_state->notifyGetInterpol(success);
+  return success;
 }
 
 bool SolverEngine::getAbduct(const Node& conj,
diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 165424594..99d2502b9 100644
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -637,12 +637,18 @@ class CVC5_EXPORT SolverEngine
    * 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,
-                   const TypeNode& grammarType,
-                   Node& interpol);
+  bool getInterpolant(const Node& conj,
+                      const TypeNode& grammarType,
+                      Node& interpol);
 
-  /** Same as above, but without user-provided grammar restrictions */
-  bool getInterpol(const Node& conj, Node& interpol);
+  /**
+   * Get next interpolant. This can only be called immediately after a
+   * successful call to getInterpolant or getInterpolantNext.
+   *
+   * Returns true if an interpolant was found, and sets interpol to the
+   * interpolant.
+   */
+  bool getInterpolantNext(Node& interpol);
 
   /**
    * This method asks this SMT engine to find an abduct with respect to the
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 3e1a5b34c..eb9bed3dc 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -323,36 +323,50 @@ bool SygusInterpol::solveInterpolation(const std::string& name,
   createVariables(itpGType.isNull());
   TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj);
 
-  Node itp = mkPredicate(name);
-  mkSygusConjecture(itp, axioms, conj);
+  d_itp = mkPredicate(name);
+  mkSygusConjecture(d_itp, axioms, conj);
 
-  std::unique_ptr<SolverEngine> subSolver;
-  initializeSubsolver(subSolver, d_env);
+  initializeSubsolver(d_subSolver, d_env);
   // get the logic
-  LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy();
+  LogicInfo l = d_subSolver->getLogicInfo().getUnlockedCopy();
   // enable everything needed for sygus
   l.enableSygus();
-  subSolver->setLogic(l);
+  d_subSolver->setLogic(l);
 
   for (const Node& var : d_vars)
   {
-    subSolver->declareSygusVar(var);
+    d_subSolver->declareSygusVar(var);
   }
   std::vector<Node> vars_empty;
-  subSolver->declareSynthFun(itp, grammarType, false, vars_empty);
-  Trace("sygus-interpol") << "SolverEngine::getInterpol: made conjecture : "
-                          << d_sygusConj << ", solving for "
-                          << d_sygusConj[0][0] << std::endl;
-  subSolver->assertSygusConstraint(d_sygusConj);
+  d_subSolver->declareSynthFun(d_itp, grammarType, false, vars_empty);
+  Trace("sygus-interpol")
+      << "SygusInterpol::solveInterpolation: made conjecture : " << d_sygusConj
+      << ", solving for " << d_sygusConj[0][0] << std::endl;
+  d_subSolver->assertSygusConstraint(d_sygusConj);
 
-  Trace("sygus-interpol") << "  SolverEngine::getInterpol check sat..."
-                          << std::endl;
-  Result r = subSolver->checkSynth();
-  Trace("sygus-interpol") << "  SolverEngine::getInterpol result: " << r
+  Trace("sygus-interpol")
+      << "  SygusInterpol::solveInterpolation check synth..." << std::endl;
+  Result r = d_subSolver->checkSynth();
+  Trace("sygus-interpol") << "  SygusInterpol::solveInterpolation result: " << r
                           << std::endl;
   if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
   {
-    return findInterpol(subSolver.get(), interpol, itp);
+    return findInterpol(d_subSolver.get(), interpol, d_itp);
+  }
+  return false;
+}
+
+bool SygusInterpol::solveInterpolationNext(Node& interpol)
+{
+  Trace("sygus-interpol")
+      << "  SygusInterpol::solveInterpolationNext check synth..." << std::endl;
+  // invoke the check-synth with isNext = true.
+  Result r = d_subSolver->checkSynth(true);
+  Trace("sygus-interpol") << "  SygusInterpol::solveInterpolationNext result: "
+                          << r << std::endl;
+  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+  {
+    return findInterpol(d_subSolver.get(), interpol, d_itp);
   }
   return false;
 }
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 4d3ae0219..604e7435f 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -84,6 +84,21 @@ class SygusInterpol : protected EnvObj
                           const TypeNode& itpGType,
                           Node& interpol);
 
+  /**
+   * Returns the sygus conjecture in interpol corresponding to the interpolation
+   * problem for input problem (F above) given by axioms (Fa above), and conj
+   * (Fc above). And solve the interpolation by sygus. Note that axioms is
+   * expected to be a subset of assertions in SMT-LIB.
+   *
+   * @param name the name for the interpol-to-synthesize.
+   * @param axioms the assertions (Fa above)
+   * @param conj the conjecture (Fc above)
+   * @param itpGType (if non-null) a sygus datatype type that encodes the
+   * grammar that should be used for solutions of the interpolation conjecture.
+   * @interpol the solution to the sygus conjecture.
+   */
+  bool solveInterpolationNext(Node& interpol);
+
  private:
   /**
    * Collects symbols from axioms (axioms) and conjecture (conj), which are
@@ -212,6 +227,13 @@ class SygusInterpol : protected EnvObj
    * the sygus conjecture to synthesis for interpolation problem
    */
   Node d_sygusConj;
+  /**
+   * The predicate for interpolation in the subsolver, which we pass to
+   * findInterpol above when the solving is successful.
+   */
+  Node d_itp;
+  /** The subsolver to initialize */
+  std::unique_ptr<SolverEngine> d_subSolver;
 };
 
 }  // namespace quantifiers
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5c4cdcd4a..e19ef2f7e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2476,7 +2476,9 @@ set(regress_1_tests
   regress1/sygus/inv-missed-sol-true.sy
   regress1/sygus/inv-unused.sy
   regress1/sygus/interpol1.smt2
+  regress1/sygus/interpol1-push-pop.smt2 
   regress1/sygus/interpol3.smt2
+  regress1/sygus/interpol3-next.smt2
   regress1/sygus/interpol_arr1.smt2
   regress1/sygus/interpol_arr2.smt2
   regress1/sygus/interpol_cosa_1.smt2
diff --git a/test/regress/regress1/sygus/interpol1-push-pop.smt2 b/test/regress/regress1/sygus/interpol1-push-pop.smt2
new file mode 100644
index 000000000..5ea6d8568
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol1-push-pop.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols -i
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic NIA)
+(declare-fun x ( ) Int)
+(declare-fun y ( ) Int)
+(declare-fun z ( ) Int)
+(push)
+(assert (= (* 2 x) y))
+(get-interpol A (distinct (+ (* 2 z) 1) y)
+
+; the grammar for the interpol-to-synthesize
+((Start Bool) (StartInt Int))
+(
+(Start Bool ((< StartInt StartInt)))
+(StartInt Int 
+(y (+ StartInt StartInt) (div StartInt StartInt) (mod StartInt StartInt) 0 1 2))
+)
+)
+(pop)
+
+(assert (= (* 2 y) x))
+(get-interpol A (distinct (+ (* 2 z) 1) x)
+; the grammar for the interpol-to-synthesize
+((Start Bool) (StartInt Int))
+(
+(Start Bool ((< StartInt StartInt)))
+(StartInt Int 
+(x (+ StartInt StartInt) (div StartInt StartInt) (mod StartInt StartInt) 0 1 2))
+)
+)
diff --git a/test/regress/regress1/sygus/interpol3-next.smt2 b/test/regress/regress1/sygus/interpol3-next.smt2
new file mode 100644
index 000000000..b92a4254e
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol3-next.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-interpols=default --check-interpols -i
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic LIA)
+(declare-fun a () Int)
+(assert (> a 1))
+(get-interpol A (> a 0))
+(get-interpol-next)
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 934e0da0d..bdd8201bc 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -1448,6 +1448,35 @@ TEST_F(TestApiBlackSolver, getInterpolant)
   ASSERT_TRUE(output.getSort().isBoolean());
 }
 
+TEST_F(TestApiBlackSolver, getInterpolantNext)
+{
+  d_solver.setLogic("QF_LIA");
+  d_solver.setOption("produce-interpols", "default");
+  d_solver.setOption("incremental", "true");
+
+  Sort intSort = d_solver.getIntegerSort();
+  Term zero = d_solver.mkInteger(0);
+  Term x = d_solver.mkConst(intSort, "x");
+  Term y = d_solver.mkConst(intSort, "y");
+  Term z = d_solver.mkConst(intSort, "z");
+  // Assumptions for interpolation: x + y > 0 /\ x < 0
+  d_solver.assertFormula(
+      d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero));
+  d_solver.assertFormula(d_solver.mkTerm(LT, x, zero));
+  // Conjecture for interpolation: y + z > 0 \/ z < 0
+  Term conj =
+      d_solver.mkTerm(OR,
+                      d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero),
+                      d_solver.mkTerm(LT, z, zero));
+  Term output;
+  d_solver.getInterpolant(conj, output);
+  Term output2;
+  d_solver.getInterpolantNext(output2);
+
+  // We expect the next output to be distinct
+  ASSERT_TRUE(output != output2);
+}
+
 TEST_F(TestApiBlackSolver, declarePool)
 {
   Sort intSort = d_solver.getIntegerSort();
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 3fb9ca50e..7313405be 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1439,6 +1439,31 @@ class SolverTest
     assertTrue(output.getSort().isBoolean());
   }
 
+  @Test void getInterpolantNext() throws CVC5ApiException
+  {
+    d_solver.setLogic("QF_LIA");
+    d_solver.setOption("produce-interpols", "default");
+    d_solver.setOption("incremental", "true");
+
+    Sort intSort = d_solver.getIntegerSort();
+    Term zero = d_solver.mkInteger(0);
+    Term x = d_solver.mkConst(intSort, "x");
+    Term y = d_solver.mkConst(intSort, "y");
+    Term z = d_solver.mkConst(intSort, "z");
+
+    d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero));
+    d_solver.assertFormula(d_solver.mkTerm(LT, x, zero));
+    Term conj = d_solver.mkTerm(
+        OR, d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), d_solver.mkTerm(LT, z, zero));
+    Term output = d_solver.getNullTerm();
+    d_solver.getInterpolant(conj, output);
+    Term output2 = d_solver.getNullTerm();
+    d_solver.getInterpolantNext(output2);
+
+    // We expect the next output to be distinct
+    assertNotEquals(output, output2);
+  }
+
   @Test void getOp() throws CVC5ApiException
   {
     Sort bv32 = d_solver.mkBitVectorSort(32);