diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-25 13:36:09 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-25 13:36:09 -0500 |
| commit | 8374a8dd4bf740bf26748c1dbe1616ad798cf624 (patch) | |
| tree | 97b08464f2ab9b31a4f763f0d570082125c78bc6 /src/util | |
| parent | 1af865f3429c0dd5910b5a8d1e12d690c3623dfa (diff) | |
Remove sygus1 parser (#4651)
We no longer support sygus v1 inputs. This PR removes support for sygus v1 (as well as a deprecated "z3str" variant of smt lib 2 which is subsumed by the new strings standard).
As mentioned in the release notes, CVC4 1.8 supports a conversion from sygus v1 to v2 script.
This removal is required for further updates to the new API. Further infrastructure (e.g. the sygus print callback) will be removed in a separate PR.
FYI @abdoo8080 .
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/result.cpp | 1 | ||||
| -rw-r--r-- | src/util/sexpr.cpp | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/src/util/result.cpp b/src/util/result.cpp index 8b527d322..0ed063ebc 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -374,7 +374,6 @@ void Result::toStreamTptp(std::ostream& out) const { void Result::toStream(std::ostream& out, OutputLanguage language) const { switch (language) { - case language::output::LANG_SYGUS_V1: case language::output::LANG_SYGUS_V2: toStreamSmt2(out); break; case language::output::LANG_TPTP: toStreamTptp(out); diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index 9b8ad81b8..6f2da480e 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -272,7 +272,6 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, bool SExpr::languageQuotesKeywords(OutputLanguage language) { switch (language) { - case language::output::LANG_SYGUS_V1: case language::output::LANG_TPTP: return true; case language::output::LANG_AST: |