cvc4-1.4
language.h
Go to the documentation of this file.
1 /********************* */
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 "util/exception.h"
27 
28 namespace CVC4 {
29 namespace language {
30 
31 namespace input {
32 
34  // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
35 
37  LANG_AUTO = -1,
38 
39  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9]
40  // AND SHOULD CORRESPOND IN PLACEMENT WITH OUTPUTLANGUAGE
41  //
42  // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
43  // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
44  // INCLUDE IT HERE
45 
56 
57  // START INPUT-ONLY LANGUAGES AT ENUM VALUE 10
58  // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES
59 
62 };/* enum Language */
63 
64 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
65 inline std::ostream& operator<<(std::ostream& out, Language lang) {
66  switch(lang) {
67  case LANG_AUTO:
68  out << "LANG_AUTO";
69  break;
70  case LANG_SMTLIB_V1:
71  out << "LANG_SMTLIB_V1";
72  break;
73  case LANG_SMTLIB_V2:
74  out << "LANG_SMTLIB_V2";
75  break;
76  case LANG_TPTP:
77  out << "LANG_TPTP";
78  break;
79  case LANG_CVC4:
80  out << "LANG_CVC4";
81  break;
82  case LANG_Z3STR:
83  out << "LANG_Z3STR";
84  break;
85  default:
86  out << "undefined_input_language";
87  }
88  return out;
89 }
90 
91 }/* CVC4::language::input namespace */
92 
93 namespace output {
94 
96  // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
97 
99  LANG_AUTO = -1,
100 
101  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9]
102  // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE
103  //
104  // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
105  // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
106  // INCLUDE IT HERE
107 
118 
119  // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
120  // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
121 
123  LANG_AST = 10,
126 
129 };/* enum Language */
130 
131 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
132 inline std::ostream& operator<<(std::ostream& out, Language lang) {
133  switch(lang) {
134  case LANG_SMTLIB_V1:
135  out << "LANG_SMTLIB_V1";
136  break;
137  case LANG_SMTLIB_V2:
138  out << "LANG_SMTLIB_V2";
139  break;
140  case LANG_TPTP:
141  out << "LANG_TPTP";
142  break;
143  case LANG_CVC4:
144  out << "LANG_CVC4";
145  break;
146  case LANG_Z3STR:
147  out << "LANG_Z3STR";
148  break;
149  case LANG_AST:
150  out << "LANG_AST";
151  break;
152  case LANG_CVC3:
153  out << "LANG_CVC3";
154  break;
155  default:
156  out << "undefined_output_language";
157  }
158  return out;
159 }
160 
161 }/* CVC4::language::output namespace */
162 
163 }/* CVC4::language namespace */
164 
167 
168 namespace language {
169 
170 InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC;
171 OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC;
172 InputLanguage toInputLanguage(std::string language) CVC4_PUBLIC;
173 OutputLanguage toOutputLanguage(std::string language) CVC4_PUBLIC;
174 
175 }/* CVC4::language namespace */
176 }/* CVC4 namespace */
177 
178 #endif /* __CVC4__LANGUAGE_H */
language::output::Language OutputLanguage
Definition: language.h:166
std::ostream & operator<<(std::ostream &out, Language lang)
Definition: language.h:65
Options-related exceptions.
language::input::Language InputLanguage
Definition: language.h:165
InputLanguage toInputLanguage(OutputLanguage language)
CVC4&#39;s exception base class and some associated utilities.
The SMTLIB v1 input language.
Definition: language.h:47
The CVC4 input language.
Definition: language.h:53
Auto-detect the language.
Definition: language.h:37
The AST output language.
Definition: language.h:123
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Macros that should be defined everywhere during the building of the libraries and driver binary...
OutputLanguage toOutputLanguage(InputLanguage language)
The TPTP input language.
Definition: language.h:51
The Z3-str input language.
Definition: language.h:55
LANG_MAX is > any valid InputLanguage id.
Definition: language.h:61
The CVC3-compatibility output language.
Definition: language.h:125
struct CVC4::options::out__option_t out
The SMTLIB v2 input language.
Definition: language.h:49