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/smt/command.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/smt/command.h')
| -rw-r--r-- | src/smt/command.h | 37 |
1 files changed, 0 insertions, 37 deletions
diff --git a/src/smt/command.h b/src/smt/command.h index 989e38ef0..0756714b6 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1232,25 +1232,6 @@ class CVC5_EXPORT GetAssertionsCommand : public Command Language language = Language::LANG_AUTO) const override; }; /* class GetAssertionsCommand */ -class CVC5_EXPORT SetBenchmarkStatusCommand : public Command -{ - protected: - BenchmarkStatus d_status; - - public: - SetBenchmarkStatusCommand(BenchmarkStatus status); - - BenchmarkStatus getStatus() const; - - void invoke(api::Solver* solver, SymbolManager* sm) override; - Command* clone() const override; - std::string getCommandName() const override; - void toStream(std::ostream& out, - int toDepth = -1, - size_t dag = 1, - Language language = Language::LANG_AUTO) const override; -}; /* class SetBenchmarkStatusCommand */ - class CVC5_EXPORT SetBenchmarkLogicCommand : public Command { protected: @@ -1413,24 +1394,6 @@ class CVC5_EXPORT QuitCommand : public Command Language language = Language::LANG_AUTO) const override; }; /* class QuitCommand */ -class CVC5_EXPORT CommentCommand : public Command -{ - std::string d_comment; - - public: - CommentCommand(std::string comment); - - std::string getComment() const; - - void invoke(api::Solver* solver, SymbolManager* sm) override; - Command* clone() const override; - std::string getCommandName() const override; - void toStream(std::ostream& out, - int toDepth = -1, - size_t dag = 1, - Language language = Language::LANG_AUTO) const override; -}; /* class CommentCommand */ - class CVC5_EXPORT CommandSequence : public Command { protected: |