From 624292d7fb5bd27b10bdce285441540d6931fa57 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 21 May 2021 12:15:28 -0500 Subject: 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. --- src/printer/printer.cpp | 5 ----- src/printer/printer.h | 3 --- 2 files changed, 8 deletions(-) (limited to 'src/printer') 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, -- cgit v1.2.3