diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-23 20:58:08 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2015-01-14 06:33:49 -0500 |
| commit | 0042f301908763cf1edb8a2d56b3f373a0055908 (patch) | |
| tree | 4f2a66c39bf5511c3f00dca9f4d1bc475435359a /src/util | |
| parent | ba1ae20edf3f4b2321a05b39cb218940e926d436 (diff) | |
sygus input language and benchmark
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/language.cpp | 2 | ||||
| -rw-r--r-- | src/util/language.h | 5 |
2 files changed, 7 insertions, 0 deletions
diff --git a/src/util/language.cpp b/src/util/language.cpp index ca611f729..4b213422c 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -113,6 +113,8 @@ InputLanguage toInputLanguage(std::string language) { } else if(language == "smtlib2.5" || language == "smt2.5" || language == "LANG_SMTLIB_V2_5") { return input::LANG_SMTLIB_V2_5; + } else if(language == "sygus" || language == "LANG_SYGUS") { + return input::LANG_SYGUS; } else if(language == "tptp" || language == "LANG_TPTP") { return input::LANG_TPTP; } else if(language == "z3str" || language == "z3-str" || diff --git a/src/util/language.h b/src/util/language.h index abde0b509..c865c2615 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -60,6 +60,8 @@ enum CVC4_PUBLIC Language { // START INPUT-ONLY LANGUAGES AT ENUM VALUE 10 // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES + /** The SyGuS input language */ + LANG_SYGUS, /** LANG_MAX is > any valid InputLanguage id */ LANG_MAX @@ -89,6 +91,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_Z3STR: out << "LANG_Z3STR"; break; + case LANG_SYGUS: + out << "LANG_SYGUS"; + break; default: out << "undefined_input_language"; } |