diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-12 16:32:32 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-12 16:32:32 +0200 |
commit | 61415ee2c5659893055f71d84a38eab8701dc47a (patch) | |
tree | ca7c2f9c5f0dc846dd91d6f96d569855eeee531e /src/util | |
parent | ad0863ae8333c4dcd950153e0db8cd4565a250b3 (diff) |
Make sygus an output language. Parse declare-fun in sygus. Minor improvements to robustness of sygus parsing.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/language.cpp | 10 | ||||
-rw-r--r-- | src/util/language.h | 13 | ||||
-rw-r--r-- | src/util/language.i | 2 |
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" |