summaryrefslogtreecommitdiff
path: root/src/options/language.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-11-29 09:31:54 -0600
committerGitHub <noreply@github.com>2019-11-29 09:31:54 -0600
commit043de624d75615ae0f5b163e2effb44cac0885a3 (patch)
tree68108695b4f7954714118c2950957d2361c8fe8b /src/options/language.cpp
parent5e2d39ccd22f38c6a3f2aab24136b07b65b3f81e (diff)
Check free variables in assertions when using SyGuS (#3504)
Diffstat (limited to 'src/options/language.cpp')
-rw-r--r--src/options/language.cpp10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/options/language.cpp b/src/options/language.cpp
index 0f2c513b6..8c6f8421f 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -68,6 +68,16 @@ bool isOutputLang_smt2_6(OutputLanguage lang, bool exact)
&& lang <= output::LANG_SMTLIB_V2_END);
}
+bool isInputLangSygus(InputLanguage lang)
+{
+ return lang == input::LANG_SYGUS || lang == input::LANG_SYGUS_V2;
+}
+
+bool isOutputLangSygus(OutputLanguage lang)
+{
+ return lang == output::LANG_SYGUS || lang == output::LANG_SYGUS_V2;
+}
+
InputLanguage toInputLanguage(OutputLanguage language) {
switch(language) {
case output::LANG_SMTLIB_V2_0:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback