Make sygus an output language. Parse declare-fun in sygus. Minor improvements to robustness of sygus parsing.

1 files changed, 7 insertions, 3 deletions

diff --git a/src/util/language.cpp b/src/util/language.cpp
index 4b213422c..193db09e8 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Francois Bobot
+ ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -27,6 +27,7 @@ InputLanguage toInputLanguage(OutputLanguage language) {
   case output::LANG_TPTP:
   case output::LANG_CVC4:
   case output::LANG_Z3STR:
+  case output::LANG_SYGUS:
     // these entries directly correspond (by design)
     return InputLanguage(int(language));
 
@@ -47,6 +48,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   case input::LANG_TPTP:
   case input::LANG_CVC4:
   case input::LANG_Z3STR:
+  case input::LANG_SYGUS:
     // these entries directly correspond (by design)
     return OutputLanguage(int(language));
 
@@ -88,6 +90,8 @@ OutputLanguage toOutputLanguage(std::string language) {
   } else if(language == "z3str" || language == "z3-str" ||
             language == "LANG_Z3STR") {
     return output::LANG_Z3STR;
+  } else if(language == "sygus" || language == "LANG_SYGUS") {
+    return output::LANG_SYGUS;
   } else if(language == "ast" || language == "LANG_AST") {
     return output::LANG_AST;
   } else if(language == "auto" || language == "LANG_AUTO") {
@@ -113,13 +117,13 @@ 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" ||
             language == "LANG_Z3STR") {
     return input::LANG_Z3STR;
+  } else if(language == "sygus" || language == "LANG_SYGUS") {
+    return input::LANG_SYGUS;
   } else if(language == "auto" || language == "LANG_AUTO") {
     return input::LANG_AUTO;
   }