diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-09-23 11:30:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-23 11:30:07 -0500 |
| commit | 970072e32f860a43b37bc0473bfdf1ab0af5d01e (patch) | |
| tree | 69a3180689618858ec5e2981e64c7fda41f1f8ef /src/printer/ast/ast_printer.h | |
| parent | 55d3b25f8d18495f92c0058df73f6ed80a369186 (diff) | |
Use `|` to print quoted strings in `set-info` command. (#7240)
This PR is a step towards enabling raw-benchmark for cvc5 regressions. cvc5 fails to reparse 57 regressions (in regress0) printed be raw-benchmark because they contain multi-line strings in set-info that we don't print between vertical bars right now. This PR fixes that bug and removes 2 commands (derived from set-info commands) that are not used by the parsers anymore.
Diffstat (limited to 'src/printer/ast/ast_printer.h')
| -rw-r--r-- | src/printer/ast/ast_printer.h | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index fd4775da4..fd5742c60 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -112,10 +112,6 @@ class AstPrinter : public cvc5::Printer /** Print get-assertions command */ void toStreamCmdGetAssertions(std::ostream& out) const override; - /** Print set-info :status command */ - void toStreamCmdSetBenchmarkStatus(std::ostream& out, - Result::Sat status) const override; - /** Print set-logic command */ void toStreamCmdSetBenchmarkLogic(std::ostream& out, const std::string& logic) const override; @@ -151,10 +147,6 @@ class AstPrinter : public cvc5::Printer /** Print quit command */ void toStreamCmdQuit(std::ostream& out) const override; - /** Print comment command */ - void toStreamCmdComment(std::ostream& out, - const std::string& comment) const override; - /** Print command sequence command */ void toStreamCmdCommandSequence( std::ostream& out, const std::vector<Command*>& sequence) const override; |