Update to sygus standard output for check-synth responses (#6521)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 21 May 2021 17:15:28 +0000 (12:15 -0500)
committerGitHub <noreply@github.com>
Fri, 21 May 2021 17:15:28 +0000 (17:15 +0000)
commit624292d7fb5bd27b10bdce285441540d6931fa57
tree73169808ce6106ba4ab18f515bb1752e1227ff3e
parentbb39d534c89dc2569aa048bb053196bfa5bbb3a1
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.
22 files changed:
src/api/cpp/cvc5.cpp
src/api/cpp/cvc5.h
src/expr/symbol_manager.cpp
src/expr/symbol_manager.h
src/options/smt_options.toml
src/printer/printer.cpp
src/printer/printer.h
src/smt/command.cpp
src/smt/command.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/smt/sygus_solver.cpp
src/smt/sygus_solver.h
src/theory/quantifiers/sygus/synth_conjecture.cpp
src/theory/quantifiers/sygus/synth_conjecture.h
src/theory/quantifiers/sygus/synth_engine.cpp
src/theory/quantifiers/sygus/synth_engine.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
test/regress/regress0/sygus/print-debug.sy
test/regress/regress0/sygus/print-define-fun.sy
test/regress/regress1/sygus/no-var-in-sol.sy