cvc4-1.3
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"
26 
27 namespace CVC4 {
28 namespace language {
29 
30 namespace input {
31 
33  // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
34 
36  LANG_AUTO = -1,
37 
38  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9]
39  // AND SHOULD CORRESPOND IN PLACEMENT WITH OUTPUTLANGUAGE
40  //
41  // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
42  // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
43  // INCLUDE IT HERE
44 
53 
54  // START INPUT-ONLY LANGUAGES AT ENUM VALUE 10
55  // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES
56 
59 };/* enum Language */
60 
61 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
62 inline std::ostream& operator<<(std::ostream& out, Language lang) {
63  switch(lang) {
64  case LANG_AUTO:
65  out << "LANG_AUTO";
66  break;
67  case LANG_SMTLIB_V1:
68  out << "LANG_SMTLIB_V1";
69  break;
70  case LANG_SMTLIB_V2:
71  out << "LANG_SMTLIB_V2";
72  break;
73  case LANG_TPTP:
74  out << "LANG_TPTP";
75  break;
76  case LANG_CVC4:
77  out << "LANG_CVC4";
78  break;
79  default:
80  out << "undefined_input_language";
81  }
82  return out;
83 }
84 
85 }/* CVC4::language::input namespace */
86 
87 namespace output {
88 
90  // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
91 
93  LANG_AUTO = -1,
94 
95  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9]
96  // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE
97  //
98  // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
99  // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
100  // INCLUDE IT HERE
101 
110 
111  // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
112  // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
113 
115  LANG_AST = 10,
116 
119 };/* enum Language */
120 
121 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
122 inline std::ostream& operator<<(std::ostream& out, Language lang) {
123  switch(lang) {
124  case LANG_SMTLIB_V1:
125  out << "LANG_SMTLIB_V1";
126  break;
127  case LANG_SMTLIB_V2:
128  out << "LANG_SMTLIB_V2";
129  break;
130  case LANG_TPTP:
131  out << "LANG_TPTP";
132  break;
133  case LANG_CVC4:
134  out << "LANG_CVC4";
135  break;
136  case LANG_AST:
137  out << "LANG_AST";
138  break;
139  default:
140  out << "undefined_output_language";
141  }
142  return out;
143 }
144 
145 }/* CVC4::language::output namespace */
146 
147 }/* CVC4::language namespace */
148 
151 
152 namespace language {
153 
156 
157 }/* CVC4::language namespace */
158 }/* CVC4 namespace */
159 
160 #endif /* __CVC4__LANGUAGE_H */
language::output::Language OutputLanguage
Definition: language.h:150
std::ostream & operator<<(std::ostream &out, Language lang)
Definition: language.h:62
The SMTLIB v1 output language.
Definition: language.h:103
The SMTLIB v2 output language.
Definition: language.h:105
The TPTP output language.
Definition: language.h:107
LANG_MAX is > any valid OutputLanguage id.
Definition: language.h:118
language::input::Language InputLanguage
Definition: language.h:149
InputLanguage toInputLanguage(OutputLanguage language)
CVC4's exception base class and some associated utilities.
The SMTLIB v1 input language.
Definition: language.h:46
The CVC4 input language.
Definition: language.h:52
Match the output language to the input language.
Definition: language.h:93
Auto-detect the language.
Definition: language.h:36
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
The AST output language.
Definition: language.h:115
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
The CVC4 output language.
Definition: language.h:109
Macros that should be defined everywhere during the building of the libraries and driver binary...
OutputLanguage toOutputLanguage(InputLanguage language)
struct CVC4::options::out__option_t out
The TPTP input language.
Definition: language.h:50
std::ostream & operator<<(std::ostream &out, Language lang)
Definition: language.h:122
LANG_MAX is > any valid InputLanguage id.
Definition: language.h:58
The SMTLIB v2 input language.
Definition: language.h:48