1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Morgan Deters, Andrew Reynolds, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Definition of input and output languages. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_public.h" |
17 |
|
|
18 |
|
#ifndef CVC5__LANGUAGE_H |
19 |
|
#define CVC5__LANGUAGE_H |
20 |
|
|
21 |
|
#include <ostream> |
22 |
|
#include <string> |
23 |
|
|
24 |
|
#include "cvc5_export.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace language { |
28 |
|
|
29 |
|
namespace input { |
30 |
|
|
31 |
|
enum CVC5_EXPORT Language |
32 |
|
{ |
33 |
|
// SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 |
34 |
|
|
35 |
|
/** Auto-detect the language */ |
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 |
|
|
45 |
|
/** The SMTLIB v2.6 input language, with support for the strings standard */ |
46 |
|
LANG_SMTLIB_V2_6 = 0, |
47 |
|
/** Backward-compatibility for enumeration naming */ |
48 |
|
LANG_SMTLIB_V2 = LANG_SMTLIB_V2_6, |
49 |
|
/** The TPTP input language */ |
50 |
|
LANG_TPTP, |
51 |
|
/** The cvc5 input language */ |
52 |
|
LANG_CVC, |
53 |
|
/** The SyGuS input language version 2.0 */ |
54 |
|
LANG_SYGUS_V2, |
55 |
|
|
56 |
|
// START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10 |
57 |
|
// THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES |
58 |
|
|
59 |
|
/** LANG_MAX is > any valid InputLanguage id */ |
60 |
|
LANG_MAX |
61 |
|
}; /* enum Language */ |
62 |
|
|
63 |
|
inline std::ostream& operator<<(std::ostream& out, Language lang) CVC5_EXPORT; |
64 |
29 |
inline std::ostream& operator<<(std::ostream& out, Language lang) { |
65 |
29 |
switch(lang) { |
66 |
|
case LANG_AUTO: |
67 |
|
out << "LANG_AUTO"; |
68 |
|
break; |
69 |
18 |
case LANG_SMTLIB_V2_6: |
70 |
18 |
out << "LANG_SMTLIB_V2_6"; |
71 |
18 |
break; |
72 |
|
case LANG_TPTP: |
73 |
|
out << "LANG_TPTP"; |
74 |
|
break; |
75 |
11 |
case LANG_CVC: out << "LANG_CVC"; break; |
76 |
|
case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break; |
77 |
|
default: |
78 |
|
out << "undefined_input_language"; |
79 |
|
} |
80 |
29 |
return out; |
81 |
|
} |
82 |
|
|
83 |
|
} // namespace input |
84 |
|
|
85 |
|
namespace output { |
86 |
|
|
87 |
|
enum CVC5_EXPORT Language |
88 |
|
{ |
89 |
|
// SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 |
90 |
|
|
91 |
|
/** Match the output language to the input language */ |
92 |
|
LANG_AUTO = -1, |
93 |
|
|
94 |
|
// COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] |
95 |
|
// AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE |
96 |
|
// |
97 |
|
// EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR |
98 |
|
// OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE, |
99 |
|
// INCLUDE IT HERE |
100 |
|
|
101 |
|
/** The SMTLIB v2.6 output language, with support for the strings standard */ |
102 |
|
LANG_SMTLIB_V2_6 = input::LANG_SMTLIB_V2_6, |
103 |
|
/** Backward-compatibility for enumeration naming */ |
104 |
|
LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2, |
105 |
|
/** The TPTP output language */ |
106 |
|
LANG_TPTP = input::LANG_TPTP, |
107 |
|
/** The cvc5 output language */ |
108 |
|
LANG_CVC = input::LANG_CVC, |
109 |
|
/** The sygus output language version 2.0 */ |
110 |
|
LANG_SYGUS_V2 = input::LANG_SYGUS_V2, |
111 |
|
|
112 |
|
// START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10 |
113 |
|
// THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES |
114 |
|
|
115 |
|
/** The AST output language */ |
116 |
|
LANG_AST = 10, |
117 |
|
|
118 |
|
/** LANG_MAX is > any valid OutputLanguage id */ |
119 |
|
LANG_MAX |
120 |
|
}; /* enum Language */ |
121 |
|
|
122 |
|
inline std::ostream& operator<<(std::ostream& out, Language lang) CVC5_EXPORT; |
123 |
12 |
inline std::ostream& operator<<(std::ostream& out, Language lang) { |
124 |
12 |
switch(lang) { |
125 |
8 |
case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break; |
126 |
|
case LANG_TPTP: |
127 |
|
out << "LANG_TPTP"; |
128 |
|
break; |
129 |
4 |
case LANG_CVC: out << "LANG_CVC"; break; |
130 |
|
case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break; |
131 |
|
case LANG_AST: |
132 |
|
out << "LANG_AST"; |
133 |
|
break; |
134 |
|
default: |
135 |
|
out << "undefined_output_language"; |
136 |
|
} |
137 |
12 |
return out; |
138 |
|
} |
139 |
|
|
140 |
|
} // namespace output |
141 |
|
|
142 |
|
} // namespace language |
143 |
|
|
144 |
|
typedef language::input::Language InputLanguage; |
145 |
|
typedef language::output::Language OutputLanguage; |
146 |
|
|
147 |
|
namespace language { |
148 |
|
|
149 |
|
/** Is the language a variant of the smtlib version 2 language? */ |
150 |
|
bool isInputLang_smt2(InputLanguage lang) CVC5_EXPORT; |
151 |
|
bool isOutputLang_smt2(OutputLanguage lang) CVC5_EXPORT; |
152 |
|
|
153 |
|
/** |
154 |
|
* Is the language smtlib 2.6 or above? If exact=true, then this method returns |
155 |
|
* false if the input language is not exactly SMT-LIB 2.6. |
156 |
|
*/ |
157 |
|
bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC5_EXPORT; |
158 |
|
bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC5_EXPORT; |
159 |
|
|
160 |
|
/** Is the language a variant of the SyGuS input language? */ |
161 |
|
bool isInputLangSygus(InputLanguage lang) CVC5_EXPORT; |
162 |
|
bool isOutputLangSygus(OutputLanguage lang) CVC5_EXPORT; |
163 |
|
|
164 |
|
InputLanguage toInputLanguage(OutputLanguage language) CVC5_EXPORT; |
165 |
|
OutputLanguage toOutputLanguage(InputLanguage language) CVC5_EXPORT; |
166 |
|
InputLanguage toInputLanguage(std::string language) CVC5_EXPORT; |
167 |
|
OutputLanguage toOutputLanguage(std::string language) CVC5_EXPORT; |
168 |
|
|
169 |
|
} // namespace language |
170 |
|
} // namespace cvc5 |
171 |
|
|
172 |
|
#endif /* CVC5__LANGUAGE_H */ |