diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-09-04 10:42:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-04 10:42:33 -0500 |
| commit | 21e1d2b6441f85a9776310779ebc6ad9e13f5b45 (patch) | |
| tree | c37eebbcf87aa3e1b04beb5441455d1bd99037aa /src/smt/command.cpp | |
| parent | 0d0c1cdbce4fb46ad5c7d4bc620b712ea014722e (diff) | |
Use Result::Sat instead of BenchmarkStatus in printers. (#5026)
This PR modifies the printers to use Result::Sat, "internal" version of BenchmarkStatus, for printing benchmark status commands.
Diffstat (limited to 'src/smt/command.cpp')
| -rw-r--r-- | src/smt/command.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index cb95cf348..64ef60906 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2977,7 +2977,15 @@ void SetBenchmarkStatusCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdSetBenchmarkStatus(out, d_status); + Result::Sat status; + switch (d_status) + { + case BenchmarkStatus::SMT_SATISFIABLE: status = Result::SAT; break; + case BenchmarkStatus::SMT_UNSATISFIABLE: status = Result::UNSAT; break; + case BenchmarkStatus::SMT_UNKNOWN: status = Result::SAT_UNKNOWN; break; + } + + Printer::getPrinter(language)->toStreamCmdSetBenchmarkStatus(out, status); } /* -------------------------------------------------------------------------- */ |