From 61415ee2c5659893055f71d84a38eab8701dc47a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 12 Jun 2015 16:32:32 +0200 Subject: Make sygus an output language. Parse declare-fun in sygus. Minor improvements to robustness of sygus parsing. --- src/util/language.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'src/util/language.cpp') 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; } -- cgit v1.2.3