1 /********************* */ 2 /*! \file language.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Morgan Deters, Andrew Reynolds, Francois Bobot 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief Definition of input and output languages 13 ** 14 ** Definition of input and output languages. 15 **/ 16 17 #include "cvc4_public.h" 18 19 #ifndef __CVC4__LANGUAGE_H 20 #define __CVC4__LANGUAGE_H 21 22 #include <sstream> 23 #include <string> 24 25 #include "base/exception.h" 26 #include "options/option_exception.h" 27 28 namespace CVC4 { 29 namespace language { 30 31 namespace input { 32 33 enum CVC4_PUBLIC Language 34 { 35 // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 36 37 /** Auto-detect the language */ 38 LANG_AUTO = -1, 39 40 // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] 41 // AND SHOULD CORRESPOND IN PLACEMENT WITH OUTPUTLANGUAGE 42 // 43 // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR 44 // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE, 45 // INCLUDE IT HERE 46 47 /** The SMTLIB v1 input language */ 48 LANG_SMTLIB_V1 = 0, 49 /** The SMTLIB v2.0 input language */ 50 LANG_SMTLIB_V2_0, 51 /** The SMTLIB v2.5 input language */ 52 LANG_SMTLIB_V2_5, 53 /** The SMTLIB v2.6 input language */ 54 LANG_SMTLIB_V2_6, 55 /** Backward-compatibility for enumeration naming */ 56 LANG_SMTLIB_V2 = LANG_SMTLIB_V2_6, 57 /** The SMTLIB v2.6 input language, with support for the strings standard */ 58 LANG_SMTLIB_V2_6_1, 59 /** The TPTP input language */ 60 LANG_TPTP, 61 /** The CVC4 input language */ 62 LANG_CVC4, 63 /** The Z3-str input language */ 64 LANG_Z3STR, 65 /** The SyGuS input language */ 66 LANG_SYGUS, 67 68 // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10 69 // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES 70 71 /** LANG_MAX is > any valid InputLanguage id */ 72 LANG_MAX 73 }; /* enum Language */ 74 75 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC; 76 inline std::ostream& operator<<(std::ostream& out, Language lang) { 77 switch(lang) { 78 case LANG_AUTO: 79 out << "LANG_AUTO"; 80 break; 81 case LANG_SMTLIB_V1: 82 out << "LANG_SMTLIB_V1"; 83 break; 84 case LANG_SMTLIB_V2_0: 85 out << "LANG_SMTLIB_V2_0"; 86 break; 87 case LANG_SMTLIB_V2_5: 88 out << "LANG_SMTLIB_V2_5"; 89 break; 90 case LANG_SMTLIB_V2_6: 91 out << "LANG_SMTLIB_V2_6"; 92 break; 93 case LANG_SMTLIB_V2_6_1: out << "LANG_SMTLIB_V2_6_1"; break; 94 case LANG_TPTP: 95 out << "LANG_TPTP"; 96 break; 97 case LANG_CVC4: 98 out << "LANG_CVC4"; 99 break; 100 case LANG_Z3STR: 101 out << "LANG_Z3STR"; 102 break; 103 case LANG_SYGUS: 104 out << "LANG_SYGUS"; 105 break; 106 default: 107 out << "undefined_input_language"; 108 } 109 return out; 110 } 111 112 }/* CVC4::language::input namespace */ 113 114 namespace output { 115 116 enum CVC4_PUBLIC Language 117 { 118 // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 119 120 /** Match the output language to the input language */ 121 LANG_AUTO = -1, 122 123 // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] 124 // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE 125 // 126 // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR 127 // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE, 128 // INCLUDE IT HERE 129 130 /** The SMTLIB v1 output language (unsupported) */ 131 LANG_SMTLIB_V1 = input::LANG_SMTLIB_V1, 132 /** The SMTLIB v2.0 output language */ 133 LANG_SMTLIB_V2_0 = input::LANG_SMTLIB_V2_0, 134 /** The SMTLIB v2.5 output language */ 135 LANG_SMTLIB_V2_5 = input::LANG_SMTLIB_V2_5, 136 /** The SMTLIB v2.6 output language */ 137 LANG_SMTLIB_V2_6 = input::LANG_SMTLIB_V2_6, 138 /** Backward-compatibility for enumeration naming */ 139 LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2, 140 /** The SMTLIB v2.6 output language */ 141 LANG_SMTLIB_V2_6_1 = input::LANG_SMTLIB_V2_6_1, 142 /** The TPTP output language */ 143 LANG_TPTP = input::LANG_TPTP, 144 /** The CVC4 output language */ 145 LANG_CVC4 = input::LANG_CVC4, 146 /** The Z3-str output language */ 147 LANG_Z3STR = input::LANG_Z3STR, 148 /** The sygus output language */ 149 LANG_SYGUS = input::LANG_SYGUS, 150 151 // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10 152 // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES 153 154 /** The AST output language */ 155 LANG_AST = 10, 156 /** The CVC3-compatibility output language */ 157 LANG_CVC3, 158 159 /** LANG_MAX is > any valid OutputLanguage id */ 160 LANG_MAX 161 }; /* enum Language */ 162 163 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC; 164 inline std::ostream& operator<<(std::ostream& out, Language lang) { 165 switch(lang) { 166 case LANG_SMTLIB_V1: 167 out << "LANG_SMTLIB_V1"; 168 break; 169 case LANG_SMTLIB_V2_0: 170 out << "LANG_SMTLIB_V2_0"; 171 break; 172 case LANG_SMTLIB_V2_5: 173 out << "LANG_SMTLIB_V2_5"; 174 break; 175 case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break; 176 case LANG_SMTLIB_V2_6_1: out << "LANG_SMTLIB_V2_6_1"; break; 177 case LANG_TPTP: 178 out << "LANG_TPTP"; 179 break; 180 case LANG_CVC4: 181 out << "LANG_CVC4"; 182 break; 183 case LANG_Z3STR: 184 out << "LANG_Z3STR"; 185 break; 186 case LANG_SYGUS: 187 out << "LANG_SYGUS"; 188 break; 189 case LANG_AST: 190 out << "LANG_AST"; 191 break; 192 case LANG_CVC3: 193 out << "LANG_CVC3"; 194 break; 195 default: 196 out << "undefined_output_language"; 197 } 198 return out; 199 } 200 201 }/* CVC4::language::output namespace */ 202 203 }/* CVC4::language namespace */ 204 205 typedef language::input::Language InputLanguage; 206 typedef language::output::Language OutputLanguage; 207 208 namespace language { 209 210 /** Is the language a variant of the smtlib version 2 language? */ 211 bool isInputLang_smt2(InputLanguage lang) CVC4_PUBLIC; 212 bool isOutputLang_smt2(OutputLanguage lang) CVC4_PUBLIC; 213 214 /** 215 * Is the language smtlib 2.5 or above? If exact=true, then this method returns 216 * false if the input language is not exactly SMT-LIB 2.6. 217 */ 218 bool isInputLang_smt2_5(InputLanguage lang, bool exact = false) CVC4_PUBLIC; 219 bool isOutputLang_smt2_5(OutputLanguage lang, bool exact = false) CVC4_PUBLIC; 220 /** 221 * Is the language smtlib 2.6 or above? If exact=true, then this method returns 222 * false if the input language is not exactly SMT-LIB 2.6. 223 */ 224 bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_PUBLIC; 225 bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_PUBLIC; 226 227 InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC; 228 OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC; 229 InputLanguage toInputLanguage(std::string language) CVC4_PUBLIC; 230 OutputLanguage toOutputLanguage(std::string language) CVC4_PUBLIC; 231 232 }/* CVC4::language namespace */ 233 }/* CVC4 namespace */ 234 235 #endif /* __CVC4__LANGUAGE_H */ 236