diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-14 18:29:22 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-14 23:29:22 +0000 |
| commit | 57dc21b3ee7ba8b991712361fc8804e1e584e674 (patch) | |
| tree | 1210277e5b3d3080807928a566a3a227fc34aba6 /src/printer | |
| parent | 560391cf71c1004716168a979782875de98b867f (diff) | |
Add get-difficulty to the API (#7194)
Adds smt2 parsing, printing and API support for get-difficulty. Adds unit tests.
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/printer.cpp | 5 | ||||
| -rw-r--r-- | src/printer/printer.h | 3 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 5 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.h | 3 |
4 files changed, 16 insertions, 0 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 01fa7a9fd..f1ad9212f 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -430,6 +430,11 @@ void Printer::toStreamCmdGetUnsatCore(std::ostream& out) const printUnknownCommand(out, "get-unsat-core"); } +void Printer::toStreamCmdGetDifficulty(std::ostream& out) const +{ + printUnknownCommand(out, "get-difficulty"); +} + void Printer::toStreamCmdGetAssertions(std::ostream& out) const { printUnknownCommand(out, "get-assertions"); diff --git a/src/printer/printer.h b/src/printer/printer.h index 499a9398f..b657a6dfa 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -213,6 +213,9 @@ class Printer /** Print get-unsat-core command */ virtual void toStreamCmdGetUnsatCore(std::ostream& out) const; + /** Print get-difficulty command */ + virtual void toStreamCmdGetDifficulty(std::ostream& out) const; + /** Print get-assertions command */ virtual void toStreamCmdGetAssertions(std::ostream& out) const; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 07c5b10d8..b92d8fa43 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1612,6 +1612,11 @@ void Smt2Printer::toStreamCmdGetUnsatCore(std::ostream& out) const out << "(get-unsat-core)" << std::endl; } +void Smt2Printer::toStreamCmdGetDifficulty(std::ostream& out) const +{ + out << "(get-difficulty)" << std::endl; +} + void Smt2Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out, Result::Sat status) const { diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index fd7e0c7ac..839c016af 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -165,6 +165,9 @@ class Smt2Printer : public cvc5::Printer /** Print get-unsat-core command */ void toStreamCmdGetUnsatCore(std::ostream& out) const override; + /** Print get-difficulty command */ + void toStreamCmdGetDifficulty(std::ostream& out) const override; + /** Print get-assertions command */ void toStreamCmdGetAssertions(std::ostream& out) const override; |