Update to sygus standard output for check-synth responses (#6521)

This PR does two things:
(1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model.
(2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model.

It also removes the unused command GetSynthSolutionCommand.

19 files changed, 73 insertions, 160 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index b7923321c..0da42f173 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7437,15 +7437,6 @@ std::vector<Term> Solver::getSynthSolutions(
   CVC5_API_TRY_CATCH_END;
 }
 
-void Solver::printSynthSolution(std::ostream& out) const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  //////// all checks before this line
-  d_smtEngine->printSynthSolution(out);
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 /*
  * !!! This is only temporarily available until the parser is fully migrated to
  * the new API. !!!
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index f77869c2c..e8f7737a6 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4118,12 +4118,6 @@ class CVC5_EXPORT Solver
    */
   std::vector<Term> getSynthSolutions(const std::vector<Term>& terms) const;
 
-  /**
-   * Print solution for synthesis conjecture to the given output stream.
-   * @param out the output stream
-   */
-  void printSynthSolution(std::ostream& out) const;
-
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
   SmtEngine* getSmtEngine(void) const;
diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index 8d4870966..687f4963f 100644
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -40,6 +40,7 @@ class SymbolManager::Implementation
         d_namedAsserts(&d_context),
         d_declareSorts(&d_context),
         d_declareTerms(&d_context),
+        d_funToSynth(&d_context),
         d_hasPushedScope(&d_context, false)
   {
     // use an outermost push, to be able to clear all definitions
@@ -65,10 +66,14 @@ class SymbolManager::Implementation
   std::vector<api::Sort> getModelDeclareSorts() const;
   /** get model declare terms */
   std::vector<api::Term> getModelDeclareTerms() const;
+  /** get functions to synthesize */
+  std::vector<api::Term> getFunctionsToSynthesize() const;
   /** Add declared sort to the list of model declarations. */
   void addModelDeclarationSort(api::Sort s);
   /** Add declared term to the list of model declarations. */
   void addModelDeclarationTerm(api::Term t);
+  /** Add function to the list of functions to synthesize. */
+  void addFunctionToSynthesize(api::Term t);
   /** reset */
   void reset();
   /** reset assertions */
@@ -91,6 +96,8 @@ class SymbolManager::Implementation
   SortList d_declareSorts;
   /** Declared terms (for model printing) */
   TermList d_declareTerms;
+  /** Functions to synthesize (for response to check-synth) */
+  TermList d_funToSynth;
   /**
    * Have we pushed a scope (e.g. a let or quantifier) in the current context?
    */
@@ -192,6 +199,12 @@ std::vector<api::Term> SymbolManager::Implementation::getModelDeclareTerms()
   return declareTerms;
 }
 
+std::vector<api::Term> SymbolManager::Implementation::getFunctionsToSynthesize()
+    const
+{
+  return std::vector<api::Term>(d_funToSynth.begin(), d_funToSynth.end());
+}
+
 void SymbolManager::Implementation::addModelDeclarationSort(api::Sort s)
 {
   Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s
@@ -206,6 +219,13 @@ void SymbolManager::Implementation::addModelDeclarationTerm(api::Term t)
   d_declareTerms.push_back(t);
 }
 
+void SymbolManager::Implementation::addFunctionToSynthesize(api::Term f)
+{
+  Trace("sym-manager") << "SymbolManager: addFunctionToSynthesize " << f
+                       << std::endl;
+  d_funToSynth.push_back(f);
+}
+
 void SymbolManager::Implementation::pushScope(bool isUserContext)
 {
   Trace("sym-manager") << "SymbolManager: pushScope, isUserContext = "
@@ -306,6 +326,11 @@ std::vector<api::Term> SymbolManager::getModelDeclareTerms() const
   return d_implementation->getModelDeclareTerms();
 }
 
+std::vector<api::Term> SymbolManager::getFunctionsToSynthesize() const
+{
+  return d_implementation->getFunctionsToSynthesize();
+}
+
 void SymbolManager::addModelDeclarationSort(api::Sort s)
 {
   d_implementation->addModelDeclarationSort(s);
@@ -316,6 +341,11 @@ void SymbolManager::addModelDeclarationTerm(api::Term t)
   d_implementation->addModelDeclarationTerm(t);
 }
 
+void SymbolManager::addFunctionToSynthesize(api::Term f)
+{
+  d_implementation->addFunctionToSynthesize(f);
+}
+
 size_t SymbolManager::scopeLevel() const
 {
   return d_symtabAllocated.getLevel();
diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index 271825e07..d8b7e23bd 100644
--- a/src/expr/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -113,6 +113,11 @@ class CVC5_EXPORT SymbolManager
    */
   std::vector<api::Term> getModelDeclareTerms() const;
   /**
+   * @return The functions we have declared that should be printed in a response
+   * to check-synth.
+   */
+  std::vector<api::Term> getFunctionsToSynthesize() const;
+  /**
    * Add declared sort to the list of model declarations.
    */
   void addModelDeclarationSort(api::Sort s);
@@ -120,6 +125,11 @@ class CVC5_EXPORT SymbolManager
    * Add declared term to the list of model declarations.
    */
   void addModelDeclarationTerm(api::Term t);
+  /**
+   * Add a function to synthesize. This ensures the solution for f is printed
+   * in a successful response to check-synth.
+   */
+  void addFunctionToSynthesize(api::Term f);
 
   //---------------------------- end named expressions
   /**
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 880bbe0fb..d1354f777 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -158,7 +158,7 @@ name   = "SMT Layer"
   category   = "regular"
   long       = "sygus-out=MODE"
   type       = "SygusSolutionOutMode"
-  default    = "STATUS_AND_DEF"
+  default    = "STANDARD"
   help       = "output mode for sygus"
   help_mode  = "Modes for sygus solution output."
 [[option.mode.STATUS]]
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 927fd1d13..048f5d06b 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -333,11 +333,6 @@ void Printer::toStreamCmdGetInstantiations(std::ostream& out) const
   printUnknownCommand(out, "get-instantiations");
 }
 
-void Printer::toStreamCmdGetSynthSolution(std::ostream& out) const
-{
-  printUnknownCommand(out, "get-synth-solution");
-}
-
 void Printer::toStreamCmdGetInterpol(std::ostream& out,
                                      const std::string& name,
                                      Node conj,
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 86f3dbb2b..6c00ebad5 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -181,9 +181,6 @@ class Printer
   /** Print get-instantiations command */
   void toStreamCmdGetInstantiations(std::ostream& out) const;
 
-  /** Print get-synth-solution command */
-  void toStreamCmdGetSynthSolution(std::ostream& out) const;
-
   /** Print get-interpol command */
   void toStreamCmdGetInterpol(std::ostream& out,
                               const std::string& name,
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 02cea842a..bf7d5ef3d 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -699,6 +699,7 @@ const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
 
 void SynthFunCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
+  sm->addFunctionToSynthesize(d_fun);
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -846,7 +847,7 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm)
     {
       if (options::sygusOut() == options::SygusSolutionOutMode::STANDARD)
       {
-        d_solution << "(fail)" << endl;
+        d_solution << "fail" << endl;
       }
       else
       {
@@ -857,12 +858,30 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm)
     if (d_result.isUnsat()
         && options::sygusOut() != options::SygusSolutionOutMode::STATUS)
     {
-      // printing a synthesis solution is a non-constant
-      // method, since it invokes a sophisticated algorithm
-      // (Figure 5 of Reynolds et al. CAV 2015).
-      // Hence, we must call here print solution here,
-      // instead of during printResult.
-      solver->printSynthSolution(d_solution);
+      std::vector<api::Term> synthFuns = sm->getFunctionsToSynthesize();
+      d_solution << "(" << std::endl;
+      Printer* p = Printer::getPrinter(language::output::LANG_SYGUS_V2);
+      for (api::Term& f : synthFuns)
+      {
+        api::Term sol = solver->getSynthSolution(f);
+        std::vector<api::Term> formals;
+        if (sol.getKind() == api::LAMBDA)
+        {
+          formals.insert(formals.end(), sol[0].begin(), sol[0].end());
+          sol = sol[1];
+        }
+        api::Sort rangeSort = f.getSort();
+        if (rangeSort.isFunction())
+        {
+          rangeSort = rangeSort.getFunctionCodomainSort();
+        }
+        p->toStreamCmdDefineFunction(d_solution,
+                                     f.toString(),
+                                     termVectorToNodes(formals),
+                                     sortToTypeNode(rangeSort),
+                                     termToNode(sol));
+      }
+      d_solution << ")" << std::endl;
     }
   }
   catch (exception& e)
@@ -2070,57 +2089,6 @@ void GetInstantiationsCommand::toStream(std::ostream& out,
 }
 
 /* -------------------------------------------------------------------------- */
-/* class GetSynthSolutionCommand                                              */
-/* -------------------------------------------------------------------------- */
-
-GetSynthSolutionCommand::GetSynthSolutionCommand() : d_solver(nullptr) {}
-void GetSynthSolutionCommand::invoke(api::Solver* solver, SymbolManager* sm)
-{
-  try
-  {
-    d_solver = solver;
-    d_commandStatus = CommandSuccess::instance();
-  }
-  catch (exception& e)
-  {
-    d_commandStatus = new CommandFailure(e.what());
-  }
-}
-
-void GetSynthSolutionCommand::printResult(std::ostream& out,
-                                          uint32_t verbosity) const
-{
-  if (!ok())
-  {
-    this->Command::printResult(out, verbosity);
-  }
-  else
-  {
-    d_solver->printSynthSolution(out);
-  }
-}
-
-Command* GetSynthSolutionCommand::clone() const
-{
-  GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
-  c->d_solver = d_solver;
-  return c;
-}
-
-std::string GetSynthSolutionCommand::getCommandName() const
-{
-  return "get-synth-solution";
-}
-
-void GetSynthSolutionCommand::toStream(std::ostream& out,
-                                       int toDepth,
-                                       size_t dag,
-                                       OutputLanguage language) const
-{
-  Printer::getPrinter(language)->toStreamCmdGetSynthSolution(out);
-}
-
-/* -------------------------------------------------------------------------- */
 /* class GetInterpolCommand                                                   */
 /* -------------------------------------------------------------------------- */
 
diff --git a/src/smt/command.h b/src/smt/command.h
index 41a3639c9..21ecd1964 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1091,25 +1091,6 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command
   api::Solver* d_solver;
 }; /* class GetInstantiationsCommand */
 
-class CVC5_EXPORT GetSynthSolutionCommand : public Command
-{
- public:
-  GetSynthSolutionCommand();
-
-  void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
-  Command* clone() const override;
-  std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
-
- protected:
-  api::Solver* d_solver;
-}; /* class GetSynthSolutionCommand */
-
 /** The command (get-interpol s B (G)?)
  *
  * This command asks for an interpolant from the current set of assertions and
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bd38f630d..6377091f2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1629,12 +1629,6 @@ void SmtEngine::getInstantiationTermVectors(
   }
 }
 
-void SmtEngine::printSynthSolution( std::ostream& out ) {
-  SmtScope smts(this);
-  finishInit();
-  d_sygusSolver->printSynthSolution(out);
-}
-
 bool SmtEngine::getSynthSolutions(std::map<Node, Node>& solMap)
 {
   SmtScope smts(this);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index b8cd1c3d7..3128257e6 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -543,11 +543,6 @@ class CVC5_EXPORT SmtEngine
    * in the proper format.
    */
   void printProof();
-  /**
-   * Print solution for synthesis conjectures found by counter-example guided
-   * instantiation module.
-   */
-  void printSynthSolution(std::ostream& out);
 
   /**
    * Get synth solution.
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 37d752230..4e5d6cd8c 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -251,18 +251,6 @@ bool SygusSolver::getSynthSolutions(std::map<Node, Node>& sol_map)
   return true;
 }
 
-void SygusSolver::printSynthSolution(std::ostream& out)
-{
-  QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
-  if (qe == nullptr)
-  {
-    InternalError()
-        << "SygusSolver::printSynthSolution(): Cannot print synth solution in "
-           "the current logic, which does not include quantifiers";
-  }
-  qe->printSynthSolution(out);
-}
-
 void SygusSolver::checkSynthSolution(Assertions& as)
 {
   NodeManager* nm = NodeManager::currentNM();
diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index 5b3bca928..ff9b7e513 100644
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -137,11 +137,6 @@ class SygusSolver
    * is a valid formula.
    */
   bool getSynthSolutions(std::map<Node, Node>& sol_map);
-  /**
-   * Print solution for synthesis conjectures found by counter-example guided
-   * instantiation module.
-   */
-  void printSynthSolution(std::ostream& out);
 
  private:
   /**
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 0eb96e277..e4ec40325 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -995,7 +995,7 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
   // we have generated a solution, print it
   // get the current output stream
   Options& sopts = smt::currentSmtEngine()->getOptions();
-  printSynthSolution(*sopts.getOut());
+  printSynthSolutionInternal(*sopts.getOut());
   excludeCurrentSolution(enums, values);
 }
 
@@ -1041,7 +1041,7 @@ void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& enums,
   }
 }
 
-void SynthConjecture::printSynthSolution(std::ostream& out)
+void SynthConjecture::printSynthSolutionInternal(std::ostream& out)
 {
   Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl;
   Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index a7ecd4ead..4329a9c60 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -134,11 +134,11 @@ class SynthConjecture
   bool doRefine();
   //-------------------------------end for counterexample-guided check/refine
   /**
-   * Prints the synthesis solution to output stream out. This invokes solution
-   * reconstruction if the conjecture is single invocation. Otherwise, it
-   * returns the solution found by sygus enumeration.
+   * Prints the current synthesis solution to output stream out. This is
+   * currently used for printing solutions for sygusStream only. We do not
+   * enclose solutions in parentheses.
    */
-  void printSynthSolution(std::ostream& out);
+  void printSynthSolutionInternal(std::ostream& out);
   /** get synth solutions
    *
    * This method returns true if this class has a solution available to the
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 173f58060..86c3f62d0 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -246,18 +246,6 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
   return conj->doRefine();
 }
 
-void SynthEngine::printSynthSolution(std::ostream& out)
-{
-  Assert(!d_conjs.empty());
-  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
-  {
-    if (d_conjs[i]->isAssigned())
-    {
-      d_conjs[i]->printSynthSolution(out);
-    }
-  }
-}
-
 bool SynthEngine::getSynthSolutions(
     std::map<Node, std::map<Node, Node> >& sol_map)
 {
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index df73c4821..d37df4e28 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -57,8 +57,6 @@ class SynthEngine : public QuantifiersModule
   void registerQuantifier(Node q) override;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const override { return "SynthEngine"; }
-  /** print solution for synthesis conjectures */
-  void printSynthSolution(std::ostream& out);
   /** get synth solutions
    *
    * This function adds entries to sol_map that map functions-to-synthesize
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2d1eeab84..40f5b901f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -651,15 +651,6 @@ void QuantifiersEngine::getInstantiations(Node q, std::vector<Node>& insts)
   d_qim.getInstantiate()->getInstantiations(q, insts);
 }
 
-void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
-  if (d_qmodules->d_synth_e)
-  {
-    d_qmodules->d_synth_e->printSynthSolution(out);
-  }else{
-    out << "Internal error : module for synth solution not found." << std::endl;
-  }
-}
-
 void QuantifiersEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
 {
   d_qim.getInstantiate()->getInstantiatedQuantifiedFormulas(qs);
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index fc29ab8e8..482dbfaee 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -134,8 +134,6 @@ public:
 
 public:
  //----------user interface for instantiations (see quantifiers/instantiate.h)
- /** print solution for synthesis conjectures */
- void printSynthSolution(std::ostream& out);
  /** get list of quantified formulas that were instantiated */
  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
  /** get instantiation term vectors */