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

3 files changed, 18 insertions, 7 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;
   }
diff --git a/src/util/language.h b/src/util/language.h
index c865c2615..05574880f 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -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
@@ -57,11 +57,11 @@ enum CVC4_PUBLIC Language {
   LANG_CVC4,
   /** The Z3-str input language */
   LANG_Z3STR,
-
-  // START INPUT-ONLY LANGUAGES AT ENUM VALUE 10
-  // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES
   /** The SyGuS input language */
   LANG_SYGUS,
+  
+  // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
+  // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
 
   /** LANG_MAX is > any valid InputLanguage id */
   LANG_MAX
@@ -131,6 +131,8 @@ enum CVC4_PUBLIC Language {
   LANG_CVC4 = input::LANG_CVC4,
   /** The Z3-str output language */
   LANG_Z3STR = input::LANG_Z3STR,
+  /** The sygus output language */
+  LANG_SYGUS = input::LANG_SYGUS,
 
   // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
   // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
@@ -165,6 +167,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_Z3STR:
     out << "LANG_Z3STR";
     break;
+  case LANG_SYGUS:
+    out << "LANG_SYGUS";
+    break;
   case LANG_AST:
     out << "LANG_AST";
     break;
diff --git a/src/util/language.i b/src/util/language.i
index 3ffc518ac..ac20db33a 100644
--- a/src/util/language.i
+++ b/src/util/language.i
@@ -27,6 +27,7 @@ namespace CVC4 {
 %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4;
 %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX;
 %rename(INPUT_LANG_Z3STR) CVC4::language::input::LANG_Z3STR;
+%rename(INPUT_LANG_SYGUS) CVC4::language::input::LANG_SYGUS;
 
 %rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO;
 %rename(OUTPUT_LANG_SMTLIB_V1) CVC4::language::output::LANG_SMTLIB_V1;
@@ -38,5 +39,6 @@ namespace CVC4 {
 %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST;
 %rename(OUTPUT_LANG_MAX) CVC4::language::output::LANG_MAX;
 %rename(OUTPUT_LANG_Z3STR) CVC4::language::output::LANG_Z3STR;
+%rename(OUTPUT_LANG_SYGUS) CVC4::language::output::LANG_SYGUS;
 
 %include "util/language.h"