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.

2 files changed, 40 insertions, 0 deletions

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