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.

10 files changed, 60 insertions, 15 deletions

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.
    *