summaryrefslogtreecommitdiff
path: root/src/options/language.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-07-01 16:33:34 -0500
committerGitHub <noreply@github.com>2019-07-01 16:33:34 -0500
commitc3b5f9d57eaf17612170b7401465b75053b07985 (patch)
treeaeef3125d045a21bda899a7f2be22a1da50ebbc3 /src/options/language.h
parentc365521b91520cf05739c7df6f2ae99f273c98d4 (diff)
Support sygus version 2 format (#3066)
Diffstat (limited to 'src/options/language.h')
-rw-r--r--src/options/language.h6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/options/language.h b/src/options/language.h
index 4d213c305..eec5ad158 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -64,6 +64,8 @@ enum CVC4_PUBLIC Language
LANG_Z3STR,
/** The SyGuS input language */
LANG_SYGUS,
+ /** The SyGuS input language version 2.0 */
+ LANG_SYGUS_V2,
// START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
// THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
@@ -103,6 +105,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
case LANG_SYGUS:
out << "LANG_SYGUS";
break;
+ case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
default:
out << "undefined_input_language";
}
@@ -147,6 +150,8 @@ enum CVC4_PUBLIC Language
LANG_Z3STR = input::LANG_Z3STR,
/** The sygus output language */
LANG_SYGUS = input::LANG_SYGUS,
+ /** The sygus output language version 2.0 */
+ LANG_SYGUS_V2 = input::LANG_SYGUS_V2,
// START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
// THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
@@ -186,6 +191,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
case LANG_SYGUS:
out << "LANG_SYGUS";
break;
+ case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break;
case LANG_AST:
out << "LANG_AST";
break;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback