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.

1 files changed, 4 insertions, 4 deletions

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