Allow SyGuS subsolver to be reused in incremental mode (#7785)

This allows SyGuS subsolvers to be called multiple times to produce solutions for a given set of SyGuS constraints using a new command check-synth-next.

By default, the SyGuS subsolver will generate a new solution for each successive check-synth.

This simplifies the internal SyGuS solver in several ways for this purpose. It also ensures that solutions are cached; current master may recompute solutions in the same state more than once if asked, which is no longer the case.

This completes our support for incremental SyGuS.

28 files changed, 365 insertions, 70 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 24b4500d5..bdaef769e 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7944,6 +7944,18 @@ Result Solver::checkSynth() const
   CVC5_API_TRY_CATCH_END;
 }
 
+Result Solver::checkSynthNext() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving)
+      << "Cannot checkSynthNext when not solving incrementally (use "
+         "--incremental)";
+  //////// all checks before this line
+  return d_slv->checkSynth(true);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Term Solver::getSynthSolution(Term term) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index f2bfb48e2..3b22f0c6f 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4811,11 +4811,31 @@ class CVC5_EXPORT Solver
    *     (check-synth)
    * \endverbatim
    *
-   * @return the result of the synthesis conjecture.
+   * @return the result of the check, which is unsat if the check succeeded,
+   * in which case solutions are available via getSynthSolutions.
    */
   Result checkSynth() const;
 
   /**
+   * Try to find a next solution for the synthesis conjecture corresponding to
+   * the current list of functions-to-synthesize, universal variables and
+   * constraints. Must be called immediately after a successful call to
+   * check-synth or check-synth-next. Requires incremental mode.
+   *
+   * SyGuS v2:
+   *
+   * \verbatim embed:rst:leading-asterisk
+   * .. code:: smtlib
+   *
+   *     (check-synth-next)
+   * \endverbatim
+   *
+   * @return the result of the check, which is unsat if the check succeeded,
+   * in which case solutions are available via getSynthSolutions.
+   */
+  Result checkSynthNext() const;
+
+  /**
    * Get the synthesis solution of the given term. This method should be called
    * immediately after the solver answers unsat for sygus input.
    * @param term the term for which the synthesis solution is queried
diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index d04b766e0..64bef09c9 100644
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -2594,7 +2594,8 @@ public class Solver implements IPointer, AutoCloseable
    * {@code
    *   ( check-synth )
    * }
-   * @return the result of the synthesis conjecture.
+   * @return the result of the check, which is unsat if the check succeeded,
+   * in which case solutions are available via getSynthSolutions.
    */
   public Result checkSynth()
   {
@@ -2605,6 +2606,26 @@ public class Solver implements IPointer, AutoCloseable
   private native long checkSynth(long pointer);
 
   /**
+   * Try to find a next solution for the synthesis conjecture corresponding to
+   * the current list of functions-to-synthesize, universal variables and
+   * constraints. Must be called immediately after a successful call to
+   * check-synth or check-synth-next. Requires incremental mode.
+   * SyGuS v2:
+   * {@code
+   *   ( check-synth-next )
+   * }
+   * @return the result of the check, which is UNSAT if the check succeeded,
+   * in which case solutions are available via getSynthSolutions.
+   */
+  public Result checkSynthNext()
+  {
+    long resultPointer = checkSynthNext(pointer);
+    return new Result(this, resultPointer);
+  }
+
+  private native long checkSynthNext(long pointer);
+
+  /**
    * Get the synthesis solution of the given term. This method should be called
    * immediately after the solver answers unsat for sygus input.
    * @param term the term for which the synthesis solution is queried
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index 8008ebada..73e481b49 100644
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -2631,6 +2631,21 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSynth(JNIEnv* env,
 
 /*
  * Class:     io_github_cvc5_api_Solver
+ * Method:    checkSynthNext
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSynthNext(
+    JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Solver* solver = reinterpret_cast<Solver*>(pointer);
+  Result* retPointer = new Result(solver->checkSynthNext());
+  return reinterpret_cast<jlong>(retPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     io_github_cvc5_api_Solver
  * Method:    getSynthSolution
  * Signature: (JJ)J
  */
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 5a33628a6..552fe6399 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -204,6 +204,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort) except +
         Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort, Grammar grammar) except +
         Result checkSynth() except +
+        Result checkSynthNext() except +
         Term getSynthSolution(Term t) except +
         vector[Term] getSynthSolutions(const vector[Term]& terms) except +
         Term synthInv(const string& symbol, const vector[Term]& bound_vars) except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index d3f58ce62..63e21bf7e 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1694,6 +1694,26 @@ cdef class Solver:
         r.cr = self.csolver.checkSynth()
         return r
 
+    def checkSynthNext(self):
+        """
+        Try to find a next solution for the synthesis conjecture corresponding
+        to the current list of functions-to-synthesize, universal variables and
+        constraints. Must be called immediately after a successful call to
+        check-synth or check-synth-next. Requires incremental mode.
+
+        SyGuS v2:
+
+        .. code-block:: smtlib
+
+            ( check-synth )
+
+        :return: the result of the check, which is unsat if the check succeeded,
+        in which case solutions are available via getSynthSolutions.
+        """
+        cdef Result r = Result()
+        r.cr = self.csolver.checkSynthNext()
+        return r
+
     def getSynthSolution(self, Term term):
         """
         Get the synthesis solution of the given term. This method should be
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 41cd4869a..7f95368b0 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -576,6 +576,12 @@ sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
       PARSER_STATE->checkThatLogicIsSet();
       cmd.reset(new CheckSynthCommand());
     }
+  | /* check-synth-next */
+    CHECK_SYNTH_NEXT_TOK
+    {
+      PARSER_STATE->checkThatLogicIsSet();
+      cmd.reset(new CheckSynthCommand(true));
+    }
   | /* set-feature */
     SET_FEATURE_TOK keyword[name] symbolicExpr[expr]
     {
@@ -2240,6 +2246,7 @@ DECLARE_POOL : 'declare-pool';
 SYNTH_FUN_TOK : { PARSER_STATE->sygus() }?'synth-fun';
 SYNTH_INV_TOK : { PARSER_STATE->sygus()}?'synth-inv';
 CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth';
+CHECK_SYNTH_NEXT_TOK : { PARSER_STATE->sygus()}?'check-synth-next';
 DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var';
 CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint';
 ASSUME_TOK : { PARSER_STATE->sygus()}?'assume';
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 16b626e30..d1c2c58a5 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -350,6 +350,10 @@ void Printer::toStreamCmdCheckSynth(std::ostream& out) const
 {
   printUnknownCommand(out, "check-synth");
 }
+void Printer::toStreamCmdCheckSynthNext(std::ostream& out) const
+{
+  printUnknownCommand(out, "check-synth-next");
+}
 
 void Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
 {
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 485cd70e6..d55723443 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -165,6 +165,9 @@ class Printer
   /** Print check-synth command */
   virtual void toStreamCmdCheckSynth(std::ostream& out) const;
 
+  /** Print check-synth-next command */
+  virtual void toStreamCmdCheckSynthNext(std::ostream& out) const;
+
   /** Print simplify command */
   virtual void toStreamCmdSimplify(std::ostream& out, Node n) const;
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 875ca7dc2..2a20bba36 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1899,6 +1899,11 @@ void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const
   out << "(check-synth)" << std::endl;
 }
 
+void Smt2Printer::toStreamCmdCheckSynthNext(std::ostream& out) const
+{
+  out << "(check-synth-next)" << std::endl;
+}
+
 void Smt2Printer::toStreamCmdGetInterpol(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 4ee333f67..b97ad2ffb 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -142,6 +142,9 @@ class Smt2Printer : public cvc5::Printer
   /** Print check-synth command */
   void toStreamCmdCheckSynth(std::ostream& out) const override;
 
+  /** Print check-synth-next command */
+  void toStreamCmdCheckSynthNext(std::ostream& out) const override;
+
   /** Print simplify command */
   void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
 
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 1321c558e..ac393d568 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -833,7 +833,7 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    d_result = solver->checkSynth();
+    d_result = d_isNext ? solver->checkSynthNext() : solver->checkSynth();
     d_commandStatus = CommandSuccess::instance();
     d_solution.clear();
     // check whether we should print the status
@@ -901,14 +901,24 @@ void CheckSynthCommand::printResult(std::ostream& out) const
 
 Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
 
-std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
+std::string CheckSynthCommand::getCommandName() const
+{
+  return d_isNext ? "check-synth-next" : "check-synth";
+}
 
 void CheckSynthCommand::toStream(std::ostream& out,
                                  int toDepth,
                                  size_t dag,
                                  Language language) const
 {
-  Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
+  if (d_isNext)
+  {
+    Printer::getPrinter(language)->toStreamCmdCheckSynthNext(out);
+  }
+  else
+  {
+    Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
+  }
 }
 
 /* -------------------------------------------------------------------------- */
diff --git a/src/smt/command.h b/src/smt/command.h
index 6ca5a7fc8..1a00c2ada 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -821,7 +821,7 @@ class CVC5_EXPORT SygusInvConstraintCommand : public Command
 class CVC5_EXPORT CheckSynthCommand : public Command
 {
  public:
-  CheckSynthCommand(){};
+  CheckSynthCommand(bool isNext = false) : d_isNext(isNext){};
   /** returns the result of the check-synth call */
   api::Result getResult() const;
   /** prints the result of the check-synth-call */
@@ -846,6 +846,8 @@ class CVC5_EXPORT CheckSynthCommand : public Command
                 Language language = Language::LANG_AUTO) const override;
 
  protected:
+  /** Whether this is a check-synth-next call */
+  bool d_isNext;
   /** result of the check-synth call */
   api::Result d_result;
   /** string stream that stores the output of the solution */
diff --git a/src/smt/smt_mode.cpp b/src/smt/smt_mode.cpp
index 6a6e35dd9..37d1d5950 100644
--- a/src/smt/smt_mode.cpp
+++ b/src/smt/smt_mode.cpp
@@ -30,6 +30,7 @@ std::ostream& operator<<(std::ostream& out, SmtMode m)
     case SmtMode::UNSAT: out << "UNSAT"; break;
     case SmtMode::ABDUCT: out << "ABDUCT"; break;
     case SmtMode::INTERPOL: out << "INTERPOL"; break;
+    case SmtMode::SYNTH: out << "SYNTH"; break;
     default: out << "SmtMode!Unknown"; break;
   }
   return out;
diff --git a/src/smt/smt_mode.h b/src/smt/smt_mode.h
index aff9b6366..098bf1cb7 100644
--- a/src/smt/smt_mode.h
+++ b/src/smt/smt_mode.h
@@ -42,7 +42,9 @@ enum class SmtMode
   // immediately after a successful call to get-abduct
   ABDUCT,
   // immediately after a successful call to get-interpol
-  INTERPOL
+  INTERPOL,
+  // immediately after a successful call to check-synth or check-synth-next
+  SYNTH
 };
 /**
  * Writes a SmtMode to a stream.
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 13d061f1f..09814c300 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -934,11 +934,19 @@ void SolverEngine::assertSygusInvConstraint(Node inv,
   d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
 }
 
-Result SolverEngine::checkSynth()
+Result SolverEngine::checkSynth(bool isNext)
 {
   SolverEngineScope smts(this);
   finishInit();
-  return d_sygusSolver->checkSynth(*d_asserts);
+  if (isNext && d_state->getMode() != SmtMode::SYNTH)
+  {
+    throw RecoverableModalException(
+        "Cannot check-synth-next unless immediately preceded by a successful "
+        "call to check-synth.");
+  }
+  Result r = d_sygusSolver->checkSynth(*d_asserts, isNext);
+  d_state->notifyCheckSynthResult(r);
+  return r;
 }
 
 /*
diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 1299a493a..ecfb521a0 100644
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -451,9 +451,12 @@ class CVC5_EXPORT SolverEngine
    * in which f1...fn are the functions-to-synthesize, v1...vm are the declared
    * universal variables and F is the set of declared constraints.
    *
+   * @param isNext Whether we are asking for the next synthesis solution (if
+   * using incremental).
+   *
    * @throw Exception
    */
-  Result checkSynth();
+  Result checkSynth(bool isNext = false);
 
   /*------------------------- end of sygus commands ------------------------*/
 
diff --git a/src/smt/solver_engine_state.cpp b/src/smt/solver_engine_state.cpp
index 8558e91cf..4ec577b68 100644
--- a/src/smt/solver_engine_state.cpp
+++ b/src/smt/solver_engine_state.cpp
@@ -113,6 +113,20 @@ void SolverEngineState::notifyCheckSatResult(bool hasAssumptions, Result r)
   }
 }
 
+void SolverEngineState::notifyCheckSynthResult(Result r)
+{
+  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+  {
+    // successfully generated a synthesis solution, update to abduct state
+    d_smtMode = SmtMode::SYNTH;
+  }
+  else
+  {
+    // failed, we revert to the assert state
+    d_smtMode = SmtMode::ASSERT;
+  }
+}
+
 void SolverEngineState::notifyGetAbduct(bool success)
 {
   if (success)
diff --git a/src/smt/solver_engine_state.h b/src/smt/solver_engine_state.h
index 7a06b0510..5cc72fd08 100644
--- a/src/smt/solver_engine_state.h
+++ b/src/smt/solver_engine_state.h
@@ -88,6 +88,11 @@ class SolverEngineState : protected EnvObj
    */
   void notifyCheckSatResult(bool hasAssumptions, Result r);
   /**
+   * Notify that the result of the last check-synth or check-synth-next was r.
+   * @param r The result of the check-synth or check-synth-next call.
+   */
+  void notifyCheckSynthResult(Result r);
+  /**
    * Notify that we finished an abduction query, where success is whether the
    * command was successful. This is managed independently of the above
    * calls for notifying check-sat. In other words, if a get-abduct command
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 70ad65644..692a123db 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -183,10 +183,15 @@ void SygusSolver::assertSygusInvConstraint(Node inv,
   d_sygusConjectureStale = true;
 }
 
-Result SygusSolver::checkSynth(Assertions& as)
+Result SygusSolver::checkSynth(Assertions& as, bool isNext)
 {
   Trace("smt") << "SygusSolver::checkSynth" << std::endl;
   // if applicable, check if the subsolver is the correct one
+  if (!isNext)
+  {
+    // if we are not using check-synth-next, we always reconstruct the solver.
+    d_sygusConjectureStale = true;
+  }
   if (usingSygusSubsolver() && d_subsolverCd.get() != d_subsolver.get())
   {
     // this can occur if we backtrack to a place where we were using a different
@@ -194,11 +199,6 @@ Result SygusSolver::checkSynth(Assertions& as)
     // the subsolver.
     d_sygusConjectureStale = true;
   }
-  // TODO (project #7): we currently must always rebuild the synthesis
-  // conjecture + subsolver, since it answers unsat. When the subsolver is
-  // updated to treat "sat" as solution for synthesis conjecture, this line
-  // will be deleted.
-  d_sygusConjectureStale = true;
   if (d_sygusConjectureStale)
   {
     NodeManager* nm = NodeManager::currentNM();
diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index 4e7a04364..b37762ce1 100644
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -131,7 +131,7 @@ class SygusSolver : protected EnvObj
    * in which f1...fn are the functions-to-synthesize, v1...vm are the declared
    * universal variables and F is the set of declared constraints.
    */
-  Result checkSynth(Assertions& as);
+  Result checkSynth(Assertions& as, bool isNext);
   /**
    * Get synth solution.
    *
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e5dfe408b..2a1258082 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -59,6 +59,7 @@ SynthConjecture::SynthConjecture(Env& env,
       d_tds(tr.getTermDatabaseSygus()),
       d_verify(env, d_tds),
       d_hasSolution(false),
+      d_computedSolution(false),
       d_ceg_si(new CegSingleInv(env, tr, s)),
       d_templInfer(new SygusTemplateInfer(env)),
       d_ceg_proc(new SynthConjectureProcess(env)),
@@ -93,8 +94,22 @@ SynthConjecture::~SynthConjecture() {}
 
 void SynthConjecture::presolve()
 {
-  // we don't have a solution yet
-  d_hasSolution = false;
+  // If we previously had a solution, block it. Notice that
+  // excludeCurrentSolution in the block below ensures we implement a
+  // policy where a *new* solution is generated for check-synth if the set of
+  // SyGuS constraints has not changed. This call will block solutions for
+  // *smart* enumerators only. This behavior makes smart enumeration have
+  // a consistent policy with *fast* enumerators, which will generate
+  // a new, next solution in their enumeration.
+  if (d_hasSolution)
+  {
+    excludeCurrentSolution(d_solutionValues.back());
+    // we don't have a solution yet
+    d_hasSolution = false;
+    d_computedSolution = false;
+    d_sol.clear();
+    d_solStatus.clear();
+  }
 }
 
 void SynthConjecture::assign(Node q)
@@ -345,15 +360,10 @@ bool SynthConjecture::doCheck()
   {
     // have we tried to repair the previous solution?
     // if not, call the repair constant utility
-    unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size();
+    size_t ninst = d_solutionValues.size();
     if (d_repair_index < ninst)
     {
-      std::vector<Node> fail_cvs;
-      for (const Node& cprog : d_candidates)
-      {
-        Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
-        fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
-      }
+      std::vector<Node> fail_cvs = d_solutionValues[d_repair_index];
       if (Trace.isOn("sygus-engine"))
       {
         Trace("sygus-engine") << "CegConjuncture : repair previous solution ";
@@ -468,7 +478,7 @@ bool SynthConjecture::doCheck()
   {
     if (!checkSideCondition(candidate_values))
     {
-      excludeCurrentSolution(terms, candidate_values);
+      excludeCurrentSolution(candidate_values);
       Trace("sygus-engine") << "...failed side condition" << std::endl;
       return false;
     }
@@ -555,7 +565,7 @@ bool SynthConjecture::doCheck()
     // In the rare case that the subcall is unknown, we simply exclude the
     // solution, without adding a counterexample point. This should only
     // happen if the quantifier free logic is undecidable.
-    excludeCurrentSolution(terms, candidate_values);
+    excludeCurrentSolution(candidate_values);
     // We should set incomplete, since a "sat" answer should not be
     // interpreted as "infeasible", which would make a difference in the rare
     // case where e.g. we had a finite grammar and exhausted the grammar.
@@ -569,9 +579,12 @@ bool SynthConjecture::doCheck()
   if (options().quantifiers.sygusStream)
   {
     // immediately print the current solution
-    printAndContinueStream(terms, candidate_values);
+    printAndContinueStream(candidate_values);
     // streaming means now we immediately are looking for a new solution
     d_hasSolution = false;
+    d_computedSolution = false;
+    d_sol.clear();
+    d_solStatus.clear();
     return false;
   }
   // We set incomplete and terminate with unknown.
@@ -634,13 +647,9 @@ bool SynthConjecture::processCounterexample(const std::vector<Node>& skModel)
     Trace("sygus-engine-debug") << "  ...(warning) failed to refine candidate, "
                                    "manually exclude candidate."
                                 << std::endl;
-    std::vector<Node> cvals;
-    for (const Node& c : d_candidates)
-    {
-      cvals.push_back(d_cinfo[c].d_inst.back());
-    }
+    std::vector<Node> cvals = d_solutionValues.back();
     // something went wrong, exclude the current candidate
-    excludeCurrentSolution(d_candidates, cvals);
+    excludeCurrentSolution(cvals);
     // Note this happens when evaluation is incapable of disproving a candidate
     // for counterexample point c, but satisfiability checking happened to find
     // the the same point c is indeed a true counterexample. It is sound
@@ -728,28 +737,26 @@ void SynthConjecture::debugPrint(const char* c)
   Trace(c) << "  * Counterexample skolems : " << d_innerSks << std::endl;
 }
 
-void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
-                                             const std::vector<Node>& values)
+void SynthConjecture::printAndContinueStream(const std::vector<Node>& values)
 {
   Assert(d_master != nullptr);
   // we have generated a solution, print it
   // get the current output stream
   printSynthSolutionInternal(*options().base.out);
-  excludeCurrentSolution(enums, values);
+  excludeCurrentSolution(values);
 }
 
-void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& enums,
-                                             const std::vector<Node>& values)
+void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& values)
 {
-  Trace("cegqi-debug") << "Exclude current solution: " << enums << " / "
-                       << values << std::endl;
+  Assert(values.size() == d_candidates.size());
+  Trace("cegqi-debug") << "Exclude current solution: " << values << std::endl;
   // However, we need to exclude the current solution using an explicit
   // blocking clause, so that we proceed to the next solution. We do this only
   // for passively-generated enumerators (TermDbSygus::isPassiveEnumerator).
   std::vector<Node> exp;
-  for (unsigned i = 0, tsize = enums.size(); i < tsize; i++)
+  for (size_t i = 0, tsize = d_candidates.size(); i < tsize; i++)
   {
-    Node cprog = enums[i];
+    Node cprog = d_candidates[i];
     Assert(d_tds->isEnumerator(cprog));
     if (d_tds->isPassiveEnumerator(cprog))
     {
@@ -935,14 +942,11 @@ bool SynthConjecture::getSynthSolutions(
   return true;
 }
 
-void SynthConjecture::recordSolution(std::vector<Node>& vs)
+void SynthConjecture::recordSolution(const std::vector<Node>& vs)
 {
   Assert(vs.size() == d_candidates.size());
-  d_cinfo.clear();
-  for (unsigned i = 0; i < vs.size(); i++)
-  {
-    d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
-  }
+  d_solutionValues.clear();
+  d_solutionValues.push_back(vs);
 }
 
 bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
@@ -952,6 +956,19 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
   {
     return false;
   }
+  if (d_computedSolution)
+  {
+    sols.insert(sols.end(), d_sol.begin(), d_sol.end());
+    statuses.insert(statuses.end(), d_solStatus.begin(), d_solStatus.end());
+    return true;
+  }
+  d_computedSolution = true;
+  // get the (SyGuS datatype) values of the solutions, if they exist
+  std::vector<Node> svals;
+  if (!d_solutionValues.empty())
+  {
+    svals = d_solutionValues.back();
+  }
   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
   {
     Node prog = d_embed_quant[0][i];
@@ -974,10 +991,10 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
     else
     {
       Node cprog = d_candidates[i];
-      if (!d_cinfo[cprog].d_inst.empty())
+      if (!svals.empty())
       {
-        // the solution is just the last instantiated term
-        sol = d_cinfo[cprog].d_inst.back();
+        // the solution is the value of the last term
+        sol = svals[i];
         status = 1;
 
         // check if there was a template
@@ -1025,9 +1042,11 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
                             << std::endl;
       }
     }
-    sols.push_back(sol);
-    statuses.push_back(status);
+    d_sol.push_back(sol);
+    d_solStatus.push_back(status);
   }
+  sols.insert(sols.end(), d_sol.begin(), d_sol.end());
+  statuses.insert(statuses.end(), d_solStatus.begin(), d_solStatus.end());
   return true;
 }
 
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 005ae4361..ce9788c50 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -62,7 +62,9 @@ class SynthConjecture : protected EnvObj
                   TermRegistry& tr,
                   SygusStatistics& s);
   ~SynthConjecture();
-  /** presolve */
+  /**
+   * Presolve, called once at the beginning of every check-sat.
+   */
   void presolve();
   /** get original version of conjecture */
   Node getConjecture() const { return d_quant; }
@@ -197,6 +199,19 @@ class SynthConjecture : protected EnvObj
    * on every call to presolve.
    */
   bool d_hasSolution;
+  /** Whether we have computed a solution */
+  bool d_computedSolution;
+  /**
+   * The final solution and status, caches getSynthSolutionsInternal, valid
+   * if d_computedSolution is true.
+   */
+  std::vector<Node> d_sol;
+  std::vector<int8_t> d_solStatus;
+  /**
+   * (SyGuS datatype) values for solutions, which is populated if we have a
+   * solution and only if we are not using the single invocation solver.
+   */
+  std::vector<std::vector<Node>> d_solutionValues;
   /** the decision strategy for the feasible guard */
   std::unique_ptr<DecisionStrategy> d_feasible_strategy;
   /** single invocation utility */
@@ -283,22 +298,13 @@ class SynthConjecture : protected EnvObj
   Node d_simp_quant;
   /** (negated) conjecture after simplification, conversion to deep embedding */
   Node d_embed_quant;
-  /** candidate information */
-  class CandidateInfo
-  {
-   public:
-    CandidateInfo() {}
-    /** list of terms we have instantiated candidates with */
-    std::vector<Node> d_inst;
-  };
-  std::map<Node, CandidateInfo> d_cinfo;
   /**
    * The first index of an instantiation in CandidateInfo::d_inst that we have
    * not yet tried to repair.
    */
   unsigned d_repair_index;
   /** record solution (this is used to construct solutions later) */
-  void recordSolution(std::vector<Node>& vs);
+  void recordSolution(const std::vector<Node>& vs);
   /** get synth solutions internal
    *
    * This function constructs the body of solutions for all
@@ -328,11 +334,9 @@ class SynthConjecture : protected EnvObj
    * The argument enums is the set of enumerators that comprise the current
    * solution, and values is their current values.
    */
-  void printAndContinueStream(const std::vector<Node>& enums,
-                              const std::vector<Node>& values);
+  void printAndContinueStream(const std::vector<Node>& values);
   /** exclude the current solution { enums -> values } */
-  void excludeCurrentSolution(const std::vector<Node>& enums,
-                              const std::vector<Node>& values);
+  void excludeCurrentSolution(const std::vector<Node>& values);
   /**
    * Whether we have guarded a stream exclusion lemma when using sygusStream.
    * This is an optimization that allows us to guard only the first stream
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 568fec3ce..4a54e2fcb 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2468,6 +2468,7 @@ set(regress_1_tests
   regress1/sygus/icfp_14_12_diff_types.sy
   regress1/sygus/icfp_28_10.sy
   regress1/sygus/icfp_easy-ite.sy
+  regress1/sygus/incremental-stream-ex.sy
   regress1/sygus/int-any-const.sy
   regress1/sygus/inv-example.sy
   regress1/sygus/inv-missed-sol-true.sy
diff --git a/test/regress/regress1/sygus/incremental-stream-ex.sy b/test/regress/regress1/sygus/incremental-stream-ex.sy
new file mode 100644
index 000000000..127a2e3bc
--- /dev/null
+++ b/test/regress/regress1/sygus/incremental-stream-ex.sy
@@ -0,0 +1,28 @@
+; COMMAND-LINE: -i --sygus-out=status
+;EXPECT: unsat
+;EXPECT: unsat
+;EXPECT: unsat
+;EXPECT: unsat
+
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Int
+  ((Start Int) (StartBool Bool))
+  ((Start Int (0 1 x y
+               (+ Start Start)
+               (- Start Start)
+               (ite StartBool Start Start)))
+   (StartBool Bool ((and StartBool StartBool)
+                    (not StartBool)
+                    (<= Start Start)))))
+
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (>= (f x y) 0))
+
+(check-synth)
+(check-synth-next)
+(check-synth-next)
+(check-synth-next)
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index f3bc91eaa..d96ff17a0 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -2589,6 +2589,37 @@ TEST_F(TestApiBlackSolver, getSynthSolutions)
   ASSERT_THROW(slv.getSynthSolutions({x}), CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSolver, checkSynthNext)
+{
+  d_solver.setOption("lang", "sygus2");
+  d_solver.setOption("incremental", "true");
+  Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
+
+  d_solver.checkSynth();
+  ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
+  d_solver.checkSynthNext();
+  ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
+}
+
+TEST_F(TestApiBlackSolver, checkSynthNext2)
+{
+  d_solver.setOption("lang", "sygus2");
+  d_solver.setOption("incremental", "false");
+  Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
+
+  d_solver.checkSynth();
+  ASSERT_THROW(d_solver.checkSynthNext(), CVC5ApiException);
+}
+
+TEST_F(TestApiBlackSolver, checkSynthNext3)
+{
+  d_solver.setOption("lang", "sygus2");
+  d_solver.setOption("incremental", "true");
+  Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
+
+  ASSERT_THROW(d_solver.checkSynthNext(), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackSolver, tupleProject)
 {
   std::vector<Sort> sorts = {d_solver.getBooleanSort(),
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index f6fa3d6f1..128141bfa 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -2584,6 +2584,36 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> slv.getSynthSolutions(new Term[] {x}));
     slv.close();
   }
+  @Test void checkSynthNext() throws CVC5ApiException
+  {
+    d_solver.setOption("lang", "sygus2");
+    d_solver.setOption("incremental", "true");
+    Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
+
+    d_solver.checkSynth();
+    assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f}));
+    d_solver.checkSynthNext();
+    assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f}));
+  }
+
+  @Test void checkSynthNext2() throws CVC5ApiException
+  {
+    d_solver.setOption("lang", "sygus2");
+    d_solver.setOption("incremental", "false");
+    Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
+
+    d_solver.checkSynth();
+    assertThrows(CVC5ApiException.class, () -> d_solver.checkSynthNext());
+  }
+
+  @Test void checkSynthNext3() throws CVC5ApiException
+  {
+    d_solver.setOption("lang", "sygus2");
+    d_solver.setOption("incremental", "true");
+    Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.checkSynthNext());
+  }
 
   @Test void tupleProject() throws CVC5ApiException
   {
diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 1e9dbcf1f..0fe0d465e 100644
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -1960,6 +1960,32 @@ def test_get_synth_solution(solver):
     with pytest.raises(RuntimeError):
         slv.getSynthSolution(f)
 
+def test_check_synth_next(solver):
+    solver.setOption("lang", "sygus2")
+    solver.setOption("incremental", "true")
+    f = solver.synthFun("f", [], solver.getBooleanSort())
+
+    solver.checkSynth()
+    solver.getSynthSolutions([f])
+
+    solver.checkSynthNext()
+    solver.getSynthSolutions([f])
+
+def test_check_synth_next2(solver):
+    solver.setOption("lang", "sygus2")
+    solver.setOption("incremental", "false")
+    f = solver.synthFun("f", [], solver.getBooleanSort())
+
+    solver.checkSynth()
+    with pytest.raises(RuntimeError):
+        solver.checkSynthNext()
+
+def test_check_synth_next3(solver):
+    solver.setOption("lang", "sygus2")
+    solver.setOption("incremental", "true")
+    f = solver.synthFun("f", [], solver.getBooleanSort())
+    with pytest.raises(RuntimeError):
+        solver.checkSynthNext()
 
 def test_declare_pool(solver):
     intSort = solver.getIntegerSort()