1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Andres Noetzli, Morgan Deters |
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 |
|
* Definitions of SMT2 constants. |
14 |
|
*/ |
15 |
|
#include "parser/smt2/smt2.h" |
16 |
|
|
17 |
|
#include <algorithm> |
18 |
|
|
19 |
|
#include "base/check.h" |
20 |
|
#include "parser/antlr_input.h" |
21 |
|
#include "parser/parser.h" |
22 |
|
#include "parser/smt2/smt2_input.h" |
23 |
|
|
24 |
|
// ANTLR defines these, which is really bad! |
25 |
|
#undef true |
26 |
|
#undef false |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace parser { |
30 |
|
|
31 |
5477 |
Smt2::Smt2(api::Solver* solver, |
32 |
|
SymbolManager* sm, |
33 |
|
bool strictMode, |
34 |
5477 |
bool parseOnly) |
35 |
|
: Parser(solver, sm, strictMode, parseOnly), |
36 |
|
d_logicSet(false), |
37 |
5477 |
d_seenSetLogic(false) |
38 |
|
{ |
39 |
5477 |
} |
40 |
|
|
41 |
10954 |
Smt2::~Smt2() {} |
42 |
|
|
43 |
5499 |
void Smt2::addArithmeticOperators() { |
44 |
5499 |
addOperator(api::PLUS, "+"); |
45 |
5499 |
addOperator(api::MINUS, "-"); |
46 |
|
// api::MINUS is converted to api::UMINUS if there is only a single operand |
47 |
5499 |
Parser::addOperator(api::UMINUS); |
48 |
5499 |
addOperator(api::MULT, "*"); |
49 |
5499 |
addOperator(api::LT, "<"); |
50 |
5499 |
addOperator(api::LEQ, "<="); |
51 |
5499 |
addOperator(api::GT, ">"); |
52 |
5499 |
addOperator(api::GEQ, ">="); |
53 |
|
|
54 |
5499 |
if (!strictModeEnabled()) |
55 |
|
{ |
56 |
|
// NOTE: this operator is non-standard |
57 |
5495 |
addOperator(api::POW, "^"); |
58 |
|
} |
59 |
5499 |
} |
60 |
|
|
61 |
1669 |
void Smt2::addTranscendentalOperators() |
62 |
|
{ |
63 |
1669 |
addOperator(api::EXPONENTIAL, "exp"); |
64 |
1669 |
addOperator(api::SINE, "sin"); |
65 |
1669 |
addOperator(api::COSINE, "cos"); |
66 |
1669 |
addOperator(api::TANGENT, "tan"); |
67 |
1669 |
addOperator(api::COSECANT, "csc"); |
68 |
1669 |
addOperator(api::SECANT, "sec"); |
69 |
1669 |
addOperator(api::COTANGENT, "cot"); |
70 |
1669 |
addOperator(api::ARCSINE, "arcsin"); |
71 |
1669 |
addOperator(api::ARCCOSINE, "arccos"); |
72 |
1669 |
addOperator(api::ARCTANGENT, "arctan"); |
73 |
1669 |
addOperator(api::ARCCOSECANT, "arccsc"); |
74 |
1669 |
addOperator(api::ARCSECANT, "arcsec"); |
75 |
1669 |
addOperator(api::ARCCOTANGENT, "arccot"); |
76 |
1669 |
addOperator(api::SQRT, "sqrt"); |
77 |
1669 |
} |
78 |
|
|
79 |
2357 |
void Smt2::addQuantifiersOperators() |
80 |
|
{ |
81 |
2357 |
} |
82 |
|
|
83 |
2817 |
void Smt2::addBitvectorOperators() { |
84 |
2817 |
addOperator(api::BITVECTOR_CONCAT, "concat"); |
85 |
2817 |
addOperator(api::BITVECTOR_NOT, "bvnot"); |
86 |
2817 |
addOperator(api::BITVECTOR_AND, "bvand"); |
87 |
2817 |
addOperator(api::BITVECTOR_OR, "bvor"); |
88 |
2817 |
addOperator(api::BITVECTOR_NEG, "bvneg"); |
89 |
2817 |
addOperator(api::BITVECTOR_ADD, "bvadd"); |
90 |
2817 |
addOperator(api::BITVECTOR_MULT, "bvmul"); |
91 |
2817 |
addOperator(api::BITVECTOR_UDIV, "bvudiv"); |
92 |
2817 |
addOperator(api::BITVECTOR_UREM, "bvurem"); |
93 |
2817 |
addOperator(api::BITVECTOR_SHL, "bvshl"); |
94 |
2817 |
addOperator(api::BITVECTOR_LSHR, "bvlshr"); |
95 |
2817 |
addOperator(api::BITVECTOR_ULT, "bvult"); |
96 |
2817 |
addOperator(api::BITVECTOR_NAND, "bvnand"); |
97 |
2817 |
addOperator(api::BITVECTOR_NOR, "bvnor"); |
98 |
2817 |
addOperator(api::BITVECTOR_XOR, "bvxor"); |
99 |
2817 |
addOperator(api::BITVECTOR_XNOR, "bvxnor"); |
100 |
2817 |
addOperator(api::BITVECTOR_COMP, "bvcomp"); |
101 |
2817 |
addOperator(api::BITVECTOR_SUB, "bvsub"); |
102 |
2817 |
addOperator(api::BITVECTOR_SDIV, "bvsdiv"); |
103 |
2817 |
addOperator(api::BITVECTOR_SREM, "bvsrem"); |
104 |
2817 |
addOperator(api::BITVECTOR_SMOD, "bvsmod"); |
105 |
2817 |
addOperator(api::BITVECTOR_ASHR, "bvashr"); |
106 |
2817 |
addOperator(api::BITVECTOR_ULE, "bvule"); |
107 |
2817 |
addOperator(api::BITVECTOR_UGT, "bvugt"); |
108 |
2817 |
addOperator(api::BITVECTOR_UGE, "bvuge"); |
109 |
2817 |
addOperator(api::BITVECTOR_SLT, "bvslt"); |
110 |
2817 |
addOperator(api::BITVECTOR_SLE, "bvsle"); |
111 |
2817 |
addOperator(api::BITVECTOR_SGT, "bvsgt"); |
112 |
2817 |
addOperator(api::BITVECTOR_SGE, "bvsge"); |
113 |
2817 |
addOperator(api::BITVECTOR_REDOR, "bvredor"); |
114 |
2817 |
addOperator(api::BITVECTOR_REDAND, "bvredand"); |
115 |
|
|
116 |
2817 |
addIndexedOperator(api::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract"); |
117 |
2817 |
addIndexedOperator(api::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat"); |
118 |
2817 |
addIndexedOperator( |
119 |
|
api::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend"); |
120 |
2817 |
addIndexedOperator( |
121 |
|
api::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend"); |
122 |
2817 |
addIndexedOperator( |
123 |
|
api::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left"); |
124 |
2817 |
addIndexedOperator( |
125 |
|
api::BITVECTOR_ROTATE_RIGHT, api::BITVECTOR_ROTATE_RIGHT, "rotate_right"); |
126 |
2817 |
} |
127 |
|
|
128 |
1633 |
void Smt2::addDatatypesOperators() |
129 |
|
{ |
130 |
1633 |
Parser::addOperator(api::APPLY_CONSTRUCTOR); |
131 |
1633 |
Parser::addOperator(api::APPLY_TESTER); |
132 |
1633 |
Parser::addOperator(api::APPLY_SELECTOR); |
133 |
|
|
134 |
1633 |
if (!strictModeEnabled()) |
135 |
|
{ |
136 |
1633 |
Parser::addOperator(api::APPLY_UPDATER); |
137 |
1633 |
addOperator(api::DT_SIZE, "dt.size"); |
138 |
1633 |
addIndexedOperator(api::APPLY_UPDATER, api::APPLY_UPDATER, "tuple_update"); |
139 |
|
} |
140 |
1633 |
} |
141 |
|
|
142 |
2016 |
void Smt2::addStringOperators() { |
143 |
4032 |
defineVar( |
144 |
|
"re.all", |
145 |
4032 |
getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())); |
146 |
2016 |
addOperator(api::STRING_CONCAT, "str.++"); |
147 |
2016 |
addOperator(api::STRING_LENGTH, "str.len"); |
148 |
2016 |
addOperator(api::STRING_SUBSTR, "str.substr"); |
149 |
2016 |
addOperator(api::STRING_CONTAINS, "str.contains"); |
150 |
2016 |
addOperator(api::STRING_CHARAT, "str.at"); |
151 |
2016 |
addOperator(api::STRING_INDEXOF, "str.indexof"); |
152 |
2016 |
addOperator(api::STRING_REPLACE, "str.replace"); |
153 |
2016 |
addOperator(api::STRING_PREFIX, "str.prefixof"); |
154 |
2016 |
addOperator(api::STRING_SUFFIX, "str.suffixof"); |
155 |
2016 |
addOperator(api::STRING_FROM_CODE, "str.from_code"); |
156 |
2016 |
addOperator(api::STRING_IS_DIGIT, "str.is_digit"); |
157 |
2016 |
addOperator(api::STRING_REPLACE_RE, "str.replace_re"); |
158 |
2016 |
addOperator(api::STRING_REPLACE_RE_ALL, "str.replace_re_all"); |
159 |
2016 |
if (!strictModeEnabled()) |
160 |
|
{ |
161 |
2016 |
addOperator(api::STRING_INDEXOF_RE, "str.indexof_re"); |
162 |
2016 |
addOperator(api::STRING_UPDATE, "str.update"); |
163 |
2016 |
addOperator(api::STRING_TOLOWER, "str.tolower"); |
164 |
2016 |
addOperator(api::STRING_TOUPPER, "str.toupper"); |
165 |
2016 |
addOperator(api::STRING_REV, "str.rev"); |
166 |
|
// sequence versions |
167 |
2016 |
addOperator(api::SEQ_CONCAT, "seq.++"); |
168 |
2016 |
addOperator(api::SEQ_LENGTH, "seq.len"); |
169 |
2016 |
addOperator(api::SEQ_EXTRACT, "seq.extract"); |
170 |
2016 |
addOperator(api::SEQ_UPDATE, "seq.update"); |
171 |
2016 |
addOperator(api::SEQ_AT, "seq.at"); |
172 |
2016 |
addOperator(api::SEQ_CONTAINS, "seq.contains"); |
173 |
2016 |
addOperator(api::SEQ_INDEXOF, "seq.indexof"); |
174 |
2016 |
addOperator(api::SEQ_REPLACE, "seq.replace"); |
175 |
2016 |
addOperator(api::SEQ_PREFIX, "seq.prefixof"); |
176 |
2016 |
addOperator(api::SEQ_SUFFIX, "seq.suffixof"); |
177 |
2016 |
addOperator(api::SEQ_REV, "seq.rev"); |
178 |
2016 |
addOperator(api::SEQ_REPLACE_ALL, "seq.replace_all"); |
179 |
2016 |
addOperator(api::SEQ_UNIT, "seq.unit"); |
180 |
2016 |
addOperator(api::SEQ_NTH, "seq.nth"); |
181 |
|
} |
182 |
2016 |
addOperator(api::STRING_FROM_INT, "str.from_int"); |
183 |
2016 |
addOperator(api::STRING_TO_INT, "str.to_int"); |
184 |
2016 |
addOperator(api::STRING_IN_REGEXP, "str.in_re"); |
185 |
2016 |
addOperator(api::STRING_TO_REGEXP, "str.to_re"); |
186 |
2016 |
addOperator(api::STRING_TO_CODE, "str.to_code"); |
187 |
2016 |
addOperator(api::STRING_REPLACE_ALL, "str.replace_all"); |
188 |
|
|
189 |
2016 |
addOperator(api::REGEXP_CONCAT, "re.++"); |
190 |
2016 |
addOperator(api::REGEXP_UNION, "re.union"); |
191 |
2016 |
addOperator(api::REGEXP_INTER, "re.inter"); |
192 |
2016 |
addOperator(api::REGEXP_STAR, "re.*"); |
193 |
2016 |
addOperator(api::REGEXP_PLUS, "re.+"); |
194 |
2016 |
addOperator(api::REGEXP_OPT, "re.opt"); |
195 |
2016 |
addIndexedOperator(api::REGEXP_REPEAT, api::REGEXP_REPEAT, "re.^"); |
196 |
2016 |
addIndexedOperator(api::REGEXP_LOOP, api::REGEXP_LOOP, "re.loop"); |
197 |
2016 |
addOperator(api::REGEXP_RANGE, "re.range"); |
198 |
2016 |
addOperator(api::REGEXP_COMPLEMENT, "re.comp"); |
199 |
2016 |
addOperator(api::REGEXP_DIFF, "re.diff"); |
200 |
2016 |
addOperator(api::STRING_LT, "str.<"); |
201 |
2016 |
addOperator(api::STRING_LEQ, "str.<="); |
202 |
2016 |
} |
203 |
|
|
204 |
1632 |
void Smt2::addFloatingPointOperators() { |
205 |
1632 |
addOperator(api::FLOATINGPOINT_FP, "fp"); |
206 |
1632 |
addOperator(api::FLOATINGPOINT_EQ, "fp.eq"); |
207 |
1632 |
addOperator(api::FLOATINGPOINT_ABS, "fp.abs"); |
208 |
1632 |
addOperator(api::FLOATINGPOINT_NEG, "fp.neg"); |
209 |
1632 |
addOperator(api::FLOATINGPOINT_ADD, "fp.add"); |
210 |
1632 |
addOperator(api::FLOATINGPOINT_SUB, "fp.sub"); |
211 |
1632 |
addOperator(api::FLOATINGPOINT_MULT, "fp.mul"); |
212 |
1632 |
addOperator(api::FLOATINGPOINT_DIV, "fp.div"); |
213 |
1632 |
addOperator(api::FLOATINGPOINT_FMA, "fp.fma"); |
214 |
1632 |
addOperator(api::FLOATINGPOINT_SQRT, "fp.sqrt"); |
215 |
1632 |
addOperator(api::FLOATINGPOINT_REM, "fp.rem"); |
216 |
1632 |
addOperator(api::FLOATINGPOINT_RTI, "fp.roundToIntegral"); |
217 |
1632 |
addOperator(api::FLOATINGPOINT_MIN, "fp.min"); |
218 |
1632 |
addOperator(api::FLOATINGPOINT_MAX, "fp.max"); |
219 |
1632 |
addOperator(api::FLOATINGPOINT_LEQ, "fp.leq"); |
220 |
1632 |
addOperator(api::FLOATINGPOINT_LT, "fp.lt"); |
221 |
1632 |
addOperator(api::FLOATINGPOINT_GEQ, "fp.geq"); |
222 |
1632 |
addOperator(api::FLOATINGPOINT_GT, "fp.gt"); |
223 |
1632 |
addOperator(api::FLOATINGPOINT_ISN, "fp.isNormal"); |
224 |
1632 |
addOperator(api::FLOATINGPOINT_ISSN, "fp.isSubnormal"); |
225 |
1632 |
addOperator(api::FLOATINGPOINT_ISZ, "fp.isZero"); |
226 |
1632 |
addOperator(api::FLOATINGPOINT_ISINF, "fp.isInfinite"); |
227 |
1632 |
addOperator(api::FLOATINGPOINT_ISNAN, "fp.isNaN"); |
228 |
1632 |
addOperator(api::FLOATINGPOINT_ISNEG, "fp.isNegative"); |
229 |
1632 |
addOperator(api::FLOATINGPOINT_ISPOS, "fp.isPositive"); |
230 |
1632 |
addOperator(api::FLOATINGPOINT_TO_REAL, "fp.to_real"); |
231 |
|
|
232 |
1632 |
addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC, |
233 |
|
api::FLOATINGPOINT_TO_FP_GENERIC, |
234 |
|
"to_fp"); |
235 |
1632 |
addIndexedOperator(api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, |
236 |
|
api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, |
237 |
|
"to_fp_unsigned"); |
238 |
1632 |
addIndexedOperator( |
239 |
|
api::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv"); |
240 |
1632 |
addIndexedOperator( |
241 |
|
api::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv"); |
242 |
|
|
243 |
1632 |
if (!strictModeEnabled()) |
244 |
|
{ |
245 |
1630 |
addIndexedOperator(api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, |
246 |
|
api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, |
247 |
|
"to_fp_bv"); |
248 |
1630 |
addIndexedOperator(api::FLOATINGPOINT_TO_FP_FLOATINGPOINT, |
249 |
|
api::FLOATINGPOINT_TO_FP_FLOATINGPOINT, |
250 |
|
"to_fp_fp"); |
251 |
1630 |
addIndexedOperator(api::FLOATINGPOINT_TO_FP_REAL, |
252 |
|
api::FLOATINGPOINT_TO_FP_REAL, |
253 |
|
"to_fp_real"); |
254 |
1630 |
addIndexedOperator(api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, |
255 |
|
api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, |
256 |
|
"to_fp_signed"); |
257 |
|
} |
258 |
1632 |
} |
259 |
|
|
260 |
1575 |
void Smt2::addSepOperators() { |
261 |
1575 |
addOperator(api::SEP_STAR, "sep"); |
262 |
1575 |
addOperator(api::SEP_PTO, "pto"); |
263 |
1575 |
addOperator(api::SEP_WAND, "wand"); |
264 |
1575 |
addOperator(api::SEP_EMP, "emp"); |
265 |
1575 |
Parser::addOperator(api::SEP_STAR); |
266 |
1575 |
Parser::addOperator(api::SEP_PTO); |
267 |
1575 |
Parser::addOperator(api::SEP_WAND); |
268 |
1575 |
Parser::addOperator(api::SEP_EMP); |
269 |
1575 |
} |
270 |
|
|
271 |
5435 |
void Smt2::addCoreSymbols() |
272 |
|
{ |
273 |
5435 |
defineType("Bool", d_solver->getBooleanSort(), true, true); |
274 |
5435 |
defineVar("true", d_solver->mkTrue(), true, true); |
275 |
5435 |
defineVar("false", d_solver->mkFalse(), true, true); |
276 |
5435 |
addOperator(api::AND, "and"); |
277 |
5435 |
addOperator(api::DISTINCT, "distinct"); |
278 |
5435 |
addOperator(api::EQUAL, "="); |
279 |
5435 |
addOperator(api::IMPLIES, "=>"); |
280 |
5435 |
addOperator(api::ITE, "ite"); |
281 |
5435 |
addOperator(api::NOT, "not"); |
282 |
5435 |
addOperator(api::OR, "or"); |
283 |
5435 |
addOperator(api::XOR, "xor"); |
284 |
5435 |
} |
285 |
|
|
286 |
427206 |
void Smt2::addOperator(api::Kind kind, const std::string& name) |
287 |
|
{ |
288 |
854412 |
Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )" |
289 |
427206 |
<< std::endl; |
290 |
427206 |
Parser::addOperator(kind); |
291 |
427206 |
operatorKindMap[name] = kind; |
292 |
427206 |
} |
293 |
|
|
294 |
44334 |
void Smt2::addIndexedOperator(api::Kind tKind, |
295 |
|
api::Kind opKind, |
296 |
|
const std::string& name) |
297 |
|
{ |
298 |
44334 |
Parser::addOperator(tKind); |
299 |
44334 |
d_indexedOpKindMap[name] = opKind; |
300 |
44334 |
} |
301 |
|
|
302 |
2892015 |
api::Kind Smt2::getOperatorKind(const std::string& name) const |
303 |
|
{ |
304 |
|
// precondition: isOperatorEnabled(name) |
305 |
2892015 |
return operatorKindMap.find(name)->second; |
306 |
|
} |
307 |
|
|
308 |
3393074 |
bool Smt2::isOperatorEnabled(const std::string& name) const { |
309 |
3393074 |
return operatorKindMap.find(name) != operatorKindMap.end(); |
310 |
|
} |
311 |
|
|
312 |
40453 |
bool Smt2::isTheoryEnabled(theory::TheoryId theory) const |
313 |
|
{ |
314 |
40453 |
return d_logic.isTheoryEnabled(theory); |
315 |
|
} |
316 |
|
|
317 |
2894271 |
bool Smt2::isHoEnabled() const { return d_logic.isHigherOrder(); } |
318 |
|
|
319 |
259195 |
bool Smt2::logicIsSet() { |
320 |
259195 |
return d_logicSet; |
321 |
|
} |
322 |
|
|
323 |
3485218 |
api::Term Smt2::getExpressionForNameAndType(const std::string& name, |
324 |
|
api::Sort t) |
325 |
|
{ |
326 |
3485218 |
if (isAbstractValue(name)) |
327 |
|
{ |
328 |
|
return mkAbstractValue(name); |
329 |
|
} |
330 |
3485218 |
return Parser::getExpressionForNameAndType(name, t); |
331 |
|
} |
332 |
|
|
333 |
2197 |
bool Smt2::getTesterName(api::Term cons, std::string& name) |
334 |
|
{ |
335 |
2197 |
if ((v2_6() || sygus()) && strictModeEnabled()) |
336 |
|
{ |
337 |
|
// 2.6 or above uses indexed tester symbols, if we are in strict mode, |
338 |
|
// we do not automatically define is-cons for constructor cons. |
339 |
|
return false; |
340 |
|
} |
341 |
4394 |
std::stringstream ss; |
342 |
2197 |
ss << "is-" << cons; |
343 |
2197 |
name = ss.str(); |
344 |
2197 |
return true; |
345 |
|
} |
346 |
|
|
347 |
89123 |
api::Term Smt2::mkIndexedConstant(const std::string& name, |
348 |
|
const std::vector<uint64_t>& numerals) |
349 |
|
{ |
350 |
89123 |
if (d_logic.isTheoryEnabled(theory::THEORY_FP)) |
351 |
|
{ |
352 |
1090 |
if (name == "+oo") |
353 |
|
{ |
354 |
4 |
return d_solver->mkPosInf(numerals[0], numerals[1]); |
355 |
|
} |
356 |
1086 |
else if (name == "-oo") |
357 |
|
{ |
358 |
2 |
return d_solver->mkNegInf(numerals[0], numerals[1]); |
359 |
|
} |
360 |
1084 |
else if (name == "NaN") |
361 |
|
{ |
362 |
4 |
return d_solver->mkNaN(numerals[0], numerals[1]); |
363 |
|
} |
364 |
1080 |
else if (name == "+zero") |
365 |
|
{ |
366 |
5 |
return d_solver->mkPosZero(numerals[0], numerals[1]); |
367 |
|
} |
368 |
1075 |
else if (name == "-zero") |
369 |
|
{ |
370 |
2 |
return d_solver->mkNegZero(numerals[0], numerals[1]); |
371 |
|
} |
372 |
|
} |
373 |
|
|
374 |
89106 |
if (d_logic.isTheoryEnabled(theory::THEORY_BV) && name.find("bv") == 0) |
375 |
|
{ |
376 |
178212 |
std::string bvStr = name.substr(2); |
377 |
89106 |
return d_solver->mkBitVector(numerals[0], bvStr, 10); |
378 |
|
} |
379 |
|
|
380 |
|
// NOTE: Theory parametric constants go here |
381 |
|
|
382 |
|
parseError(std::string("Unknown indexed literal `") + name + "'"); |
383 |
|
return api::Term(); |
384 |
|
} |
385 |
|
|
386 |
76450 |
api::Kind Smt2::getIndexedOpKind(const std::string& name) |
387 |
|
{ |
388 |
76450 |
const auto& kIt = d_indexedOpKindMap.find(name); |
389 |
76450 |
if (kIt != d_indexedOpKindMap.end()) |
390 |
|
{ |
391 |
76450 |
return (*kIt).second; |
392 |
|
} |
393 |
|
parseError(std::string("Unknown indexed function `") + name + "'"); |
394 |
|
return api::UNDEFINED_KIND; |
395 |
|
} |
396 |
|
|
397 |
150 |
api::Term Smt2::bindDefineFunRec( |
398 |
|
const std::string& fname, |
399 |
|
const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames, |
400 |
|
api::Sort t, |
401 |
|
std::vector<api::Term>& flattenVars) |
402 |
|
{ |
403 |
300 |
std::vector<api::Sort> sorts; |
404 |
454 |
for (const std::pair<std::string, api::Sort>& svn : sortedVarNames) |
405 |
|
{ |
406 |
304 |
sorts.push_back(svn.second); |
407 |
|
} |
408 |
|
|
409 |
|
// make the flattened function type, add bound variables |
410 |
|
// to flattenVars if the defined function was given a function return type. |
411 |
300 |
api::Sort ft = mkFlatFunctionType(sorts, t, flattenVars); |
412 |
|
|
413 |
|
// allow overloading |
414 |
300 |
return bindVar(fname, ft, false, true); |
415 |
|
} |
416 |
|
|
417 |
150 |
void Smt2::pushDefineFunRecScope( |
418 |
|
const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames, |
419 |
|
api::Term func, |
420 |
|
const std::vector<api::Term>& flattenVars, |
421 |
|
std::vector<api::Term>& bvs) |
422 |
|
{ |
423 |
150 |
pushScope(); |
424 |
|
|
425 |
|
// bound variables are those that are explicitly named in the preamble |
426 |
|
// of the define-fun(s)-rec command, we define them here |
427 |
454 |
for (const std::pair<std::string, api::Sort>& svn : sortedVarNames) |
428 |
|
{ |
429 |
608 |
api::Term v = bindBoundVar(svn.first, svn.second); |
430 |
304 |
bvs.push_back(v); |
431 |
|
} |
432 |
|
|
433 |
150 |
bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end()); |
434 |
150 |
} |
435 |
|
|
436 |
41 |
void Smt2::reset() { |
437 |
41 |
d_logicSet = false; |
438 |
41 |
d_seenSetLogic = false; |
439 |
41 |
d_logic = LogicInfo(); |
440 |
41 |
operatorKindMap.clear(); |
441 |
41 |
d_lastNamedTerm = std::pair<api::Term, std::string>(); |
442 |
41 |
} |
443 |
|
|
444 |
14 |
std::unique_ptr<Command> Smt2::invConstraint( |
445 |
|
const std::vector<std::string>& names) |
446 |
|
{ |
447 |
14 |
checkThatLogicIsSet(); |
448 |
14 |
Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl; |
449 |
14 |
Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl; |
450 |
|
|
451 |
14 |
if (names.size() != 4) |
452 |
|
{ |
453 |
|
parseError( |
454 |
|
"Bad syntax for inv-constraint: expected 4 " |
455 |
|
"arguments."); |
456 |
|
} |
457 |
|
|
458 |
28 |
std::vector<api::Term> terms; |
459 |
70 |
for (const std::string& name : names) |
460 |
|
{ |
461 |
56 |
if (!isDeclared(name)) |
462 |
|
{ |
463 |
|
std::stringstream ss; |
464 |
|
ss << "Function " << name << " in inv-constraint is not defined."; |
465 |
|
parseError(ss.str()); |
466 |
|
} |
467 |
|
|
468 |
56 |
terms.push_back(getVariable(name)); |
469 |
|
} |
470 |
|
|
471 |
28 |
return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms)); |
472 |
|
} |
473 |
|
|
474 |
5441 |
Command* Smt2::setLogic(std::string name, bool fromCommand) |
475 |
|
{ |
476 |
5441 |
if (fromCommand) |
477 |
|
{ |
478 |
5365 |
if (d_seenSetLogic) |
479 |
|
{ |
480 |
2 |
parseError("Only one set-logic is allowed."); |
481 |
|
} |
482 |
5364 |
d_seenSetLogic = true; |
483 |
|
|
484 |
5364 |
if (logicIsForced()) |
485 |
|
{ |
486 |
|
// If the logic is forced, we ignore all set-logic requests from commands. |
487 |
5 |
return new EmptyCommand(); |
488 |
|
} |
489 |
|
} |
490 |
|
|
491 |
5435 |
d_logicSet = true; |
492 |
5435 |
d_logic = name; |
493 |
|
|
494 |
|
// if sygus is enabled, we must enable UF, datatypes, and integer arithmetic |
495 |
5435 |
if(sygus()) { |
496 |
198 |
if (!d_logic.isQuantified()) |
497 |
|
{ |
498 |
|
warning("Logics in sygus are assumed to contain quantifiers."); |
499 |
|
warning("Omit QF_ from the logic to avoid this warning."); |
500 |
|
} |
501 |
|
} |
502 |
|
|
503 |
|
// Core theory belongs to every logic |
504 |
5435 |
addCoreSymbols(); |
505 |
|
|
506 |
5435 |
if(d_logic.isTheoryEnabled(theory::THEORY_UF)) { |
507 |
2969 |
Parser::addOperator(api::APPLY_UF); |
508 |
|
|
509 |
2969 |
if (!strictModeEnabled() && d_logic.hasCardinalityConstraints()) |
510 |
|
{ |
511 |
22 |
addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card"); |
512 |
22 |
addOperator(api::CARDINALITY_VALUE, "fmf.card.val"); |
513 |
|
} |
514 |
|
} |
515 |
|
|
516 |
5435 |
if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) { |
517 |
3773 |
if(d_logic.areIntegersUsed()) { |
518 |
3245 |
defineType("Int", d_solver->getIntegerSort(), true, true); |
519 |
3245 |
addArithmeticOperators(); |
520 |
3245 |
if (!strictModeEnabled() || !d_logic.isLinear()) |
521 |
|
{ |
522 |
3241 |
addOperator(api::INTS_DIVISION, "div"); |
523 |
3241 |
addOperator(api::INTS_MODULUS, "mod"); |
524 |
3241 |
addOperator(api::ABS, "abs"); |
525 |
|
} |
526 |
3245 |
addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible"); |
527 |
|
} |
528 |
|
|
529 |
3773 |
if (d_logic.areRealsUsed()) |
530 |
|
{ |
531 |
2254 |
defineType("Real", d_solver->getRealSort(), true, true); |
532 |
2254 |
addArithmeticOperators(); |
533 |
2254 |
addOperator(api::DIVISION, "/"); |
534 |
2254 |
if (!strictModeEnabled()) |
535 |
|
{ |
536 |
2254 |
addOperator(api::ABS, "abs"); |
537 |
|
} |
538 |
|
} |
539 |
|
|
540 |
3773 |
if (d_logic.areIntegersUsed() && d_logic.areRealsUsed()) |
541 |
|
{ |
542 |
1726 |
addOperator(api::TO_INTEGER, "to_int"); |
543 |
1726 |
addOperator(api::IS_INTEGER, "is_int"); |
544 |
1726 |
addOperator(api::TO_REAL, "to_real"); |
545 |
|
} |
546 |
|
|
547 |
3773 |
if (d_logic.areTranscendentalsUsed()) |
548 |
|
{ |
549 |
1669 |
defineVar("real.pi", d_solver->mkTerm(api::PI)); |
550 |
1669 |
addTranscendentalOperators(); |
551 |
|
} |
552 |
3773 |
if (!strictModeEnabled()) |
553 |
|
{ |
554 |
|
// integer version of AND |
555 |
3769 |
addIndexedOperator(api::IAND, api::IAND, "iand"); |
556 |
|
// pow2 |
557 |
3769 |
addOperator(api::POW2, "int.pow2"); |
558 |
|
} |
559 |
|
} |
560 |
|
|
561 |
5435 |
if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) { |
562 |
2203 |
addOperator(api::SELECT, "select"); |
563 |
2203 |
addOperator(api::STORE, "store"); |
564 |
2203 |
addOperator(api::EQ_RANGE, "eqrange"); |
565 |
|
} |
566 |
|
|
567 |
5435 |
if(d_logic.isTheoryEnabled(theory::THEORY_BV)) { |
568 |
2817 |
addBitvectorOperators(); |
569 |
|
|
570 |
8446 |
if (!strictModeEnabled() && d_logic.isTheoryEnabled(theory::THEORY_ARITH) |
571 |
4530 |
&& d_logic.areIntegersUsed()) |
572 |
|
{ |
573 |
|
// Conversions between bit-vectors and integers |
574 |
1705 |
addOperator(api::BITVECTOR_TO_NAT, "bv2nat"); |
575 |
1705 |
addIndexedOperator( |
576 |
|
api::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv"); |
577 |
|
} |
578 |
|
} |
579 |
|
|
580 |
5435 |
if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) { |
581 |
3266 |
const std::vector<api::Sort> types; |
582 |
1633 |
defineType("Tuple", d_solver->mkTupleSort(types), true, true); |
583 |
1633 |
addDatatypesOperators(); |
584 |
|
} |
585 |
|
|
586 |
5435 |
if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) { |
587 |
1653 |
defineVar("emptyset", d_solver->mkEmptySet(d_solver->getNullSort())); |
588 |
|
// the Boolean sort is a placeholder here since we don't have type info |
589 |
|
// without type annotation |
590 |
1653 |
defineVar("univset", d_solver->mkUniverseSet(d_solver->getBooleanSort())); |
591 |
|
|
592 |
1653 |
addOperator(api::UNION, "union"); |
593 |
1653 |
addOperator(api::INTERSECTION, "intersection"); |
594 |
1653 |
addOperator(api::SETMINUS, "setminus"); |
595 |
1653 |
addOperator(api::SUBSET, "subset"); |
596 |
1653 |
addOperator(api::MEMBER, "member"); |
597 |
1653 |
addOperator(api::SINGLETON, "singleton"); |
598 |
1653 |
addOperator(api::INSERT, "insert"); |
599 |
1653 |
addOperator(api::CARD, "card"); |
600 |
1653 |
addOperator(api::COMPLEMENT, "complement"); |
601 |
1653 |
addOperator(api::CHOOSE, "choose"); |
602 |
1653 |
addOperator(api::IS_SINGLETON, "is_singleton"); |
603 |
1653 |
addOperator(api::JOIN, "join"); |
604 |
1653 |
addOperator(api::PRODUCT, "product"); |
605 |
1653 |
addOperator(api::TRANSPOSE, "transpose"); |
606 |
1653 |
addOperator(api::TCLOSURE, "tclosure"); |
607 |
|
} |
608 |
|
|
609 |
5435 |
if (d_logic.isTheoryEnabled(theory::THEORY_BAGS)) |
610 |
|
{ |
611 |
1571 |
defineVar("emptybag", d_solver->mkEmptyBag(d_solver->getNullSort())); |
612 |
1571 |
addOperator(api::UNION_MAX, "union_max"); |
613 |
1571 |
addOperator(api::UNION_DISJOINT, "union_disjoint"); |
614 |
1571 |
addOperator(api::INTERSECTION_MIN, "intersection_min"); |
615 |
1571 |
addOperator(api::DIFFERENCE_SUBTRACT, "difference_subtract"); |
616 |
1571 |
addOperator(api::DIFFERENCE_REMOVE, "difference_remove"); |
617 |
1571 |
addOperator(api::SUBBAG, "subbag"); |
618 |
1571 |
addOperator(api::BAG_COUNT, "bag.count"); |
619 |
1571 |
addOperator(api::DUPLICATE_REMOVAL, "duplicate_removal"); |
620 |
1571 |
addOperator(api::MK_BAG, "bag"); |
621 |
1571 |
addOperator(api::BAG_CARD, "bag.card"); |
622 |
1571 |
addOperator(api::BAG_CHOOSE, "bag.choose"); |
623 |
1571 |
addOperator(api::BAG_IS_SINGLETON, "bag.is_singleton"); |
624 |
1571 |
addOperator(api::BAG_FROM_SET, "bag.from_set"); |
625 |
1571 |
addOperator(api::BAG_TO_SET, "bag.to_set"); |
626 |
1571 |
addOperator(api::BAG_MAP, "bag.map"); |
627 |
|
} |
628 |
5435 |
if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) { |
629 |
2016 |
defineType("String", d_solver->getStringSort(), true, true); |
630 |
2016 |
defineType("RegLan", d_solver->getRegExpSort(), true, true); |
631 |
2016 |
defineType("Int", d_solver->getIntegerSort(), true, true); |
632 |
|
|
633 |
2016 |
defineVar("re.none", d_solver->mkRegexpEmpty()); |
634 |
2016 |
defineVar("re.allchar", d_solver->mkRegexpSigma()); |
635 |
|
|
636 |
|
// Boolean is a placeholder |
637 |
4032 |
defineVar("seq.empty", |
638 |
4032 |
d_solver->mkEmptySequence(d_solver->getBooleanSort())); |
639 |
|
|
640 |
2016 |
addStringOperators(); |
641 |
|
} |
642 |
|
|
643 |
5435 |
if(d_logic.isQuantified()) { |
644 |
2357 |
addQuantifiersOperators(); |
645 |
|
} |
646 |
|
|
647 |
5435 |
if (d_logic.isTheoryEnabled(theory::THEORY_FP)) { |
648 |
1632 |
defineType("RoundingMode", d_solver->getRoundingModeSort(), true, true); |
649 |
1632 |
defineType("Float16", d_solver->mkFloatingPointSort(5, 11), true, true); |
650 |
1632 |
defineType("Float32", d_solver->mkFloatingPointSort(8, 24), true, true); |
651 |
1632 |
defineType("Float64", d_solver->mkFloatingPointSort(11, 53), true, true); |
652 |
1632 |
defineType("Float128", d_solver->mkFloatingPointSort(15, 113), true, true); |
653 |
|
|
654 |
1632 |
defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN)); |
655 |
3264 |
defineVar("roundNearestTiesToEven", |
656 |
3264 |
d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN)); |
657 |
1632 |
defineVar("RNA", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY)); |
658 |
3264 |
defineVar("roundNearestTiesToAway", |
659 |
3264 |
d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY)); |
660 |
1632 |
defineVar("RTP", d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE)); |
661 |
3264 |
defineVar("roundTowardPositive", |
662 |
3264 |
d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE)); |
663 |
1632 |
defineVar("RTN", d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE)); |
664 |
3264 |
defineVar("roundTowardNegative", |
665 |
3264 |
d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE)); |
666 |
1632 |
defineVar("RTZ", d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO)); |
667 |
3264 |
defineVar("roundTowardZero", |
668 |
3264 |
d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO)); |
669 |
|
|
670 |
1632 |
addFloatingPointOperators(); |
671 |
|
} |
672 |
|
|
673 |
5435 |
if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) { |
674 |
|
// the Boolean sort is a placeholder here since we don't have type info |
675 |
|
// without type annotation |
676 |
1575 |
defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort())); |
677 |
|
|
678 |
1575 |
addSepOperators(); |
679 |
|
} |
680 |
|
|
681 |
10870 |
std::string logic = sygus() ? d_logic.getLogicString() : name; |
682 |
5435 |
if (!fromCommand) |
683 |
|
{ |
684 |
|
// If not from a command, just set the logic directly. Notice this is |
685 |
|
// important since we do not want to enqueue a set-logic command and |
686 |
|
// fully initialize the underlying SmtEngine in the meantime before the |
687 |
|
// command has a chance to execute, which would lead to an error. |
688 |
76 |
d_solver->setLogic(logic); |
689 |
76 |
return nullptr; |
690 |
|
} |
691 |
5359 |
Command* cmd = new SetBenchmarkLogicCommand(logic); |
692 |
5359 |
return cmd; |
693 |
|
} /* Smt2::setLogic() */ |
694 |
|
|
695 |
152 |
api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars, |
696 |
|
const std::vector<api::Term>& ntSymbols) |
697 |
|
{ |
698 |
152 |
d_allocGrammars.emplace_back( |
699 |
304 |
new api::Grammar(d_solver->mkSygusGrammar(boundVars, ntSymbols))); |
700 |
152 |
return d_allocGrammars.back().get(); |
701 |
|
} |
702 |
|
|
703 |
236662 |
bool Smt2::sygus() const |
704 |
|
{ |
705 |
236662 |
return d_solver->getOption("input-language") == "LANG_SYGUS_V2"; |
706 |
|
} |
707 |
|
|
708 |
259195 |
void Smt2::checkThatLogicIsSet() |
709 |
|
{ |
710 |
259195 |
if (!logicIsSet()) |
711 |
|
{ |
712 |
80 |
if (strictModeEnabled()) |
713 |
|
{ |
714 |
8 |
parseError("set-logic must appear before this point."); |
715 |
|
} |
716 |
|
else |
717 |
|
{ |
718 |
|
// the calls to setLogic below set the logic on the solver directly |
719 |
76 |
if (logicIsForced()) |
720 |
|
{ |
721 |
8 |
setLogic(getForcedLogic(), false); |
722 |
|
} |
723 |
|
else |
724 |
|
{ |
725 |
68 |
warning("No set-logic command was given before this point."); |
726 |
68 |
warning("cvc5 will make all theories available."); |
727 |
68 |
warning( |
728 |
|
"Consider setting a stricter logic for (likely) better " |
729 |
|
"performance."); |
730 |
68 |
warning("To suppress this warning in the future use (set-logic ALL)."); |
731 |
|
|
732 |
68 |
setLogic("ALL", false); |
733 |
|
} |
734 |
|
} |
735 |
|
} |
736 |
259191 |
} |
737 |
|
|
738 |
3699 |
void Smt2::checkLogicAllowsFreeSorts() |
739 |
|
{ |
740 |
7398 |
if (!d_logic.isTheoryEnabled(theory::THEORY_UF) |
741 |
34 |
&& !d_logic.isTheoryEnabled(theory::THEORY_ARRAYS) |
742 |
|
&& !d_logic.isTheoryEnabled(theory::THEORY_DATATYPES) |
743 |
|
&& !d_logic.isTheoryEnabled(theory::THEORY_SETS) |
744 |
3699 |
&& !d_logic.isTheoryEnabled(theory::THEORY_BAGS)) |
745 |
|
{ |
746 |
|
parseErrorLogic("Free sort symbols not allowed in "); |
747 |
|
} |
748 |
3699 |
} |
749 |
|
|
750 |
14413 |
void Smt2::checkLogicAllowsFunctions() |
751 |
|
{ |
752 |
14413 |
if (!d_logic.isTheoryEnabled(theory::THEORY_UF) && !isHoEnabled()) |
753 |
|
{ |
754 |
|
parseError( |
755 |
|
"Functions (of non-zero arity) cannot " |
756 |
|
"be declared in logic " |
757 |
|
+ d_logic.getLogicString() |
758 |
|
+ ". Try including UF or adding the prefix HO_."); |
759 |
|
} |
760 |
14413 |
} |
761 |
|
|
762 |
|
/* The include are managed in the lexer but called in the parser */ |
763 |
|
// Inspired by http://www.antlr3.org/api/C/interop.html |
764 |
|
|
765 |
|
static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) { |
766 |
|
Debug("parser") << "Including " << filename << std::endl; |
767 |
|
// Create a new input stream and take advantage of built in stream stacking |
768 |
|
// in C target runtime. |
769 |
|
// |
770 |
|
pANTLR3_INPUT_STREAM in; |
771 |
|
#ifdef CVC5_ANTLR3_OLD_INPUT_STREAM |
772 |
|
in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str()); |
773 |
|
#else /* CVC5_ANTLR3_OLD_INPUT_STREAM */ |
774 |
|
in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT); |
775 |
|
#endif /* CVC5_ANTLR3_OLD_INPUT_STREAM */ |
776 |
|
if( in == NULL ) { |
777 |
|
Debug("parser") << "Can't open " << filename << std::endl; |
778 |
|
return false; |
779 |
|
} |
780 |
|
// Same thing as the predefined PUSHSTREAM(in); |
781 |
|
lexer->pushCharStream(lexer, in); |
782 |
|
// restart it |
783 |
|
//lexer->rec->state->tokenStartCharIndex = -10; |
784 |
|
//lexer->emit(lexer); |
785 |
|
|
786 |
|
// Note that the input stream is not closed when it EOFs, I don't bother |
787 |
|
// to do it here, but it is up to you to track streams created like this |
788 |
|
// and destroy them when the whole parse session is complete. Remember that you |
789 |
|
// don't want to do this until all tokens have been manipulated all the way through |
790 |
|
// your tree parsers etc as the token does not store the text it just refers |
791 |
|
// back to the input stream and trying to get the text for it will abort if you |
792 |
|
// close the input stream too early. |
793 |
|
|
794 |
|
//TODO what said before |
795 |
|
return true; |
796 |
|
} |
797 |
|
|
798 |
|
void Smt2::includeFile(const std::string& filename) { |
799 |
|
// security for online version |
800 |
|
if(!canIncludeFile()) { |
801 |
|
parseError("include-file feature was disabled for this run."); |
802 |
|
} |
803 |
|
|
804 |
|
// Get the lexer |
805 |
|
AntlrInput* ai = static_cast<AntlrInput*>(getInput()); |
806 |
|
pANTLR3_LEXER lexer = ai->getAntlr3Lexer(); |
807 |
|
// get the name of the current stream "Does it work inside an include?" |
808 |
|
const std::string inputName = ai->getInputStreamName(); |
809 |
|
|
810 |
|
// Find the directory of the current input file |
811 |
|
std::string path; |
812 |
|
size_t pos = inputName.rfind('/'); |
813 |
|
if(pos != std::string::npos) { |
814 |
|
path = std::string(inputName, 0, pos + 1); |
815 |
|
} |
816 |
|
path.append(filename); |
817 |
|
if(!newInputStream(path, lexer)) { |
818 |
|
parseError("Couldn't open include file `" + path + "'"); |
819 |
|
} |
820 |
|
} |
821 |
10808605 |
bool Smt2::isAbstractValue(const std::string& name) |
822 |
|
{ |
823 |
20888077 |
return name.length() >= 2 && name[0] == '@' && name[1] != '0' |
824 |
10808617 |
&& name.find_first_not_of("0123456789", 1) == std::string::npos; |
825 |
|
} |
826 |
|
|
827 |
|
api::Term Smt2::mkAbstractValue(const std::string& name) |
828 |
|
{ |
829 |
|
Assert(isAbstractValue(name)); |
830 |
|
// remove the '@' |
831 |
|
return d_solver->mkAbstractValue(name.substr(1)); |
832 |
|
} |
833 |
|
|
834 |
355 |
void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) |
835 |
|
{ |
836 |
710 |
Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type |
837 |
355 |
<< std::endl; |
838 |
|
// (as const (Array T1 T2)) |
839 |
355 |
if (p.d_kind == api::CONST_ARRAY) |
840 |
|
{ |
841 |
65 |
if (!type.isArray()) |
842 |
|
{ |
843 |
|
std::stringstream ss; |
844 |
|
ss << "expected array constant term, but cast is not of array type" |
845 |
|
<< std::endl |
846 |
|
<< "cast type: " << type; |
847 |
|
parseError(ss.str()); |
848 |
|
} |
849 |
65 |
p.d_type = type; |
850 |
65 |
return; |
851 |
|
} |
852 |
290 |
if (p.d_expr.isNull()) |
853 |
|
{ |
854 |
580 |
Trace("parser-overloading") |
855 |
290 |
<< "Getting variable expression with name " << p.d_name << " and type " |
856 |
290 |
<< type << std::endl; |
857 |
|
// get the variable expression for the type |
858 |
290 |
if (isDeclared(p.d_name, SYM_VARIABLE)) |
859 |
|
{ |
860 |
290 |
p.d_expr = getExpressionForNameAndType(p.d_name, type); |
861 |
290 |
p.d_name = std::string(""); |
862 |
|
} |
863 |
290 |
if (p.d_expr.isNull()) |
864 |
|
{ |
865 |
|
std::stringstream ss; |
866 |
|
ss << "Could not resolve expression with name " << p.d_name |
867 |
|
<< " and type " << type << std::endl; |
868 |
|
parseError(ss.str()); |
869 |
|
} |
870 |
|
} |
871 |
290 |
Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr; |
872 |
290 |
Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getSort(); |
873 |
290 |
Trace("parser-qid") << std::endl; |
874 |
|
// otherwise, we process the type ascription |
875 |
290 |
p.d_expr = applyTypeAscription(p.d_expr, type); |
876 |
|
} |
877 |
|
|
878 |
3485225 |
api::Term Smt2::parseOpToExpr(ParseOp& p) |
879 |
|
{ |
880 |
3485225 |
Debug("parser") << "parseOpToExpr: " << p << std::endl; |
881 |
3485225 |
api::Term expr; |
882 |
3485225 |
if (p.d_kind != api::NULL_EXPR || !p.d_type.isNull()) |
883 |
|
{ |
884 |
|
parseError( |
885 |
|
"Bad syntax for qualified identifier operator in term position."); |
886 |
|
} |
887 |
3485225 |
else if (!p.d_expr.isNull()) |
888 |
|
{ |
889 |
288 |
expr = p.d_expr; |
890 |
|
} |
891 |
3484937 |
else if (!isDeclared(p.d_name, SYM_VARIABLE)) |
892 |
|
{ |
893 |
18 |
std::stringstream ss; |
894 |
9 |
ss << "Symbol " << p.d_name << " is not declared."; |
895 |
18 |
parseError(ss.str()); |
896 |
|
} |
897 |
|
else |
898 |
|
{ |
899 |
3484928 |
expr = getExpressionForName(p.d_name); |
900 |
|
} |
901 |
3485216 |
Assert(!expr.isNull()); |
902 |
3485216 |
return expr; |
903 |
|
} |
904 |
|
|
905 |
3295161 |
api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) |
906 |
|
{ |
907 |
3295161 |
bool isBuiltinOperator = false; |
908 |
|
// the builtin kind of the overall return expression |
909 |
3295161 |
api::Kind kind = api::NULL_EXPR; |
910 |
|
// First phase: process the operator |
911 |
3295161 |
if (Debug.isOn("parser")) |
912 |
|
{ |
913 |
|
Debug("parser") << "applyParseOp: " << p << " to:" << std::endl; |
914 |
|
for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); |
915 |
|
++i) |
916 |
|
{ |
917 |
|
Debug("parser") << "++ " << *i << std::endl; |
918 |
|
} |
919 |
|
} |
920 |
6590322 |
api::Op op; |
921 |
3295161 |
if (p.d_kind != api::NULL_EXPR) |
922 |
|
{ |
923 |
|
// It is a special case, e.g. tupSel or array constant specification. |
924 |
|
// We have to wait until the arguments are parsed to resolve it. |
925 |
|
} |
926 |
3295086 |
else if (!p.d_expr.isNull()) |
927 |
|
{ |
928 |
|
// An explicit operator, e.g. an apply function |
929 |
1424 |
api::Kind fkind = getKindForFunction(p.d_expr); |
930 |
1424 |
if (fkind != api::UNDEFINED_KIND) |
931 |
|
{ |
932 |
|
// Some operators may require a specific kind. |
933 |
|
// Testers are handled differently than other indexed operators, |
934 |
|
// since they require a kind. |
935 |
1424 |
kind = fkind; |
936 |
2848 |
Debug("parser") << "Got function kind " << kind << " for expression " |
937 |
1424 |
<< std::endl; |
938 |
|
} |
939 |
1424 |
args.insert(args.begin(), p.d_expr); |
940 |
|
} |
941 |
3293662 |
else if (!p.d_op.isNull()) |
942 |
|
{ |
943 |
|
// it was given an operator |
944 |
76445 |
op = p.d_op; |
945 |
|
} |
946 |
|
else |
947 |
|
{ |
948 |
3217217 |
isBuiltinOperator = isOperatorEnabled(p.d_name); |
949 |
3217217 |
if (isBuiltinOperator) |
950 |
|
{ |
951 |
|
// a builtin operator, convert to kind |
952 |
2892015 |
kind = getOperatorKind(p.d_name); |
953 |
|
} |
954 |
|
else |
955 |
|
{ |
956 |
|
// A non-built-in function application, get the expression |
957 |
325224 |
checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE); |
958 |
650360 |
api::Term v = getVariable(p.d_name); |
959 |
325180 |
if (!v.isNull()) |
960 |
|
{ |
961 |
325060 |
checkFunctionLike(v); |
962 |
325056 |
kind = getKindForFunction(v); |
963 |
325056 |
args.insert(args.begin(), v); |
964 |
|
} |
965 |
|
else |
966 |
|
{ |
967 |
|
// Overloaded symbol? |
968 |
|
// Could not find the expression. It may be an overloaded symbol, |
969 |
|
// in which case we may find it after knowing the types of its |
970 |
|
// arguments. |
971 |
244 |
std::vector<api::Sort> argTypes; |
972 |
268 |
for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); |
973 |
|
++i) |
974 |
|
{ |
975 |
146 |
argTypes.push_back((*i).getSort()); |
976 |
|
} |
977 |
244 |
api::Term fop = getOverloadedFunctionForTypes(p.d_name, argTypes); |
978 |
122 |
if (!fop.isNull()) |
979 |
|
{ |
980 |
122 |
checkFunctionLike(fop); |
981 |
122 |
kind = getKindForFunction(fop); |
982 |
122 |
args.insert(args.begin(), fop); |
983 |
|
} |
984 |
|
else |
985 |
|
{ |
986 |
|
parseError( |
987 |
|
"Cannot find unambiguous overloaded function for argument " |
988 |
|
"types."); |
989 |
|
} |
990 |
|
} |
991 |
|
} |
992 |
|
} |
993 |
|
// handle special cases |
994 |
3295137 |
if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull()) |
995 |
|
{ |
996 |
65 |
if (args.size() != 1) |
997 |
|
{ |
998 |
|
parseError("Too many arguments to array constant."); |
999 |
|
} |
1000 |
130 |
api::Term constVal = args[0]; |
1001 |
|
|
1002 |
|
// To parse array constants taking reals whose values are specified by |
1003 |
|
// rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle |
1004 |
|
// the fact that (/ 1 3) is the division of constants 1 and 3, and not |
1005 |
|
// the resulting constant rational value. Thus, we must construct the |
1006 |
|
// resulting rational here. This also is applied for integral real values |
1007 |
|
// like 5.0 which are converted to (/ 5 1) to distinguish them from |
1008 |
|
// integer constants. We must ensure numerator and denominator are |
1009 |
|
// constant and the denominator is non-zero. |
1010 |
65 |
if (constVal.getKind() == api::DIVISION) |
1011 |
|
{ |
1012 |
4 |
std::stringstream sdiv; |
1013 |
2 |
sdiv << constVal[0] << "/" << constVal[1]; |
1014 |
2 |
constVal = d_solver->mkReal(sdiv.str()); |
1015 |
|
} |
1016 |
|
|
1017 |
65 |
if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort())) |
1018 |
|
{ |
1019 |
|
std::stringstream ss; |
1020 |
|
ss << "type mismatch inside array constant term:" << std::endl |
1021 |
|
<< "array type: " << p.d_type << std::endl |
1022 |
|
<< "expected const type: " << p.d_type.getArrayElementSort() |
1023 |
|
<< std::endl |
1024 |
|
<< "computed const type: " << constVal.getSort(); |
1025 |
|
parseError(ss.str()); |
1026 |
|
} |
1027 |
130 |
api::Term ret = d_solver->mkConstArray(p.d_type, constVal); |
1028 |
65 |
Debug("parser") << "applyParseOp: return store all " << ret << std::endl; |
1029 |
65 |
return ret; |
1030 |
|
} |
1031 |
9885212 |
else if ((p.d_kind == api::APPLY_SELECTOR || p.d_kind == api::APPLY_UPDATER) |
1032 |
3295080 |
&& !p.d_expr.isNull()) |
1033 |
|
{ |
1034 |
|
// tuple selector case |
1035 |
8 |
if (!p.d_expr.isUInt64Value()) |
1036 |
|
{ |
1037 |
|
parseError( |
1038 |
|
"index of tuple select or update is larger than size of uint64_t"); |
1039 |
|
} |
1040 |
8 |
uint64_t n = p.d_expr.getUInt64Value(); |
1041 |
8 |
if (args.size() != (p.d_kind == api::APPLY_SELECTOR ? 1 : 2)) |
1042 |
|
{ |
1043 |
|
parseError("wrong number of arguments for tuple select or update"); |
1044 |
|
} |
1045 |
16 |
api::Sort t = args[0].getSort(); |
1046 |
8 |
if (!t.isTuple()) |
1047 |
|
{ |
1048 |
|
parseError("tuple select or update applied to non-tuple"); |
1049 |
|
} |
1050 |
8 |
size_t length = t.getTupleLength(); |
1051 |
8 |
if (n >= length) |
1052 |
|
{ |
1053 |
|
std::stringstream ss; |
1054 |
|
ss << "tuple is of length " << length << "; cannot access index " << n; |
1055 |
|
parseError(ss.str()); |
1056 |
|
} |
1057 |
16 |
const api::Datatype& dt = t.getDatatype(); |
1058 |
16 |
api::Term ret; |
1059 |
8 |
if (p.d_kind == api::APPLY_SELECTOR) |
1060 |
|
{ |
1061 |
8 |
ret = d_solver->mkTerm( |
1062 |
8 |
api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]); |
1063 |
|
} |
1064 |
|
else |
1065 |
|
{ |
1066 |
8 |
ret = d_solver->mkTerm( |
1067 |
8 |
api::APPLY_UPDATER, dt[0][n].getUpdaterTerm(), args[0], args[1]); |
1068 |
|
} |
1069 |
8 |
Debug("parser") << "applyParseOp: return selector " << ret << std::endl; |
1070 |
8 |
return ret; |
1071 |
|
} |
1072 |
3295064 |
else if (p.d_kind == api::TUPLE_PROJECT) |
1073 |
|
{ |
1074 |
4 |
api::Term ret = d_solver->mkTerm(p.d_op, args[0]); |
1075 |
2 |
Debug("parser") << "applyParseOp: return projection " << ret << std::endl; |
1076 |
2 |
return ret; |
1077 |
|
} |
1078 |
3295062 |
else if (p.d_kind != api::NULL_EXPR) |
1079 |
|
{ |
1080 |
|
// it should not have an expression or type specified at this point |
1081 |
|
if (!p.d_expr.isNull() || !p.d_type.isNull()) |
1082 |
|
{ |
1083 |
|
std::stringstream ss; |
1084 |
|
ss << "Could not process parsed qualified identifier kind " << p.d_kind; |
1085 |
|
parseError(ss.str()); |
1086 |
|
} |
1087 |
|
// otherwise it is a simple application |
1088 |
|
kind = p.d_kind; |
1089 |
|
} |
1090 |
3295062 |
else if (isBuiltinOperator) |
1091 |
|
{ |
1092 |
2892015 |
if (!isHoEnabled() && (kind == api::EQUAL || kind == api::DISTINCT)) |
1093 |
|
{ |
1094 |
|
// need hol if these operators are applied over function args |
1095 |
719114 |
for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); |
1096 |
|
++i) |
1097 |
|
{ |
1098 |
481415 |
if ((*i).getSort().isFunction()) |
1099 |
|
{ |
1100 |
|
parseError( |
1101 |
|
"Cannot apply equality to functions unless logic is prefixed by " |
1102 |
|
"HO_."); |
1103 |
|
} |
1104 |
|
} |
1105 |
|
} |
1106 |
8675958 |
if (!strictModeEnabled() && (kind == api::AND || kind == api::OR) |
1107 |
3725632 |
&& args.size() == 1) |
1108 |
|
{ |
1109 |
|
// Unary AND/OR can be replaced with the argument. |
1110 |
96 |
Debug("parser") << "applyParseOp: return unary " << args[0] << std::endl; |
1111 |
96 |
return args[0]; |
1112 |
|
} |
1113 |
2891919 |
else if (kind == api::MINUS && args.size() == 1) |
1114 |
|
{ |
1115 |
240762 |
api::Term ret = d_solver->mkTerm(api::UMINUS, args[0]); |
1116 |
120381 |
Debug("parser") << "applyParseOp: return uminus " << ret << std::endl; |
1117 |
120381 |
return ret; |
1118 |
|
} |
1119 |
2771538 |
if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true") |
1120 |
|
{ |
1121 |
|
parseError( |
1122 |
|
"eqrange predicate requires option --arrays-exp to be enabled."); |
1123 |
|
} |
1124 |
2771538 |
if (kind == api::SINGLETON && args.size() == 1) |
1125 |
|
{ |
1126 |
386 |
api::Term ret = d_solver->mkTerm(api::SINGLETON, args[0]); |
1127 |
193 |
Debug("parser") << "applyParseOp: return singleton " << ret << std::endl; |
1128 |
193 |
return ret; |
1129 |
|
} |
1130 |
5542690 |
api::Term ret = d_solver->mkTerm(kind, args); |
1131 |
5542690 |
Debug("parser") << "applyParseOp: return default builtin " << ret |
1132 |
2771345 |
<< std::endl; |
1133 |
2771345 |
return ret; |
1134 |
|
} |
1135 |
|
|
1136 |
403047 |
if (args.size() >= 2) |
1137 |
|
{ |
1138 |
|
// may be partially applied function, in this case we use HO_APPLY |
1139 |
653181 |
api::Sort argt = args[0].getSort(); |
1140 |
326744 |
if (argt.isFunction()) |
1141 |
|
{ |
1142 |
310248 |
unsigned arity = argt.getFunctionArity(); |
1143 |
310248 |
if (args.size() - 1 < arity) |
1144 |
|
{ |
1145 |
307 |
if (!isHoEnabled()) |
1146 |
|
{ |
1147 |
|
parseError( |
1148 |
|
"Cannot partially apply functions unless logic is prefixed by " |
1149 |
|
"HO_."); |
1150 |
|
} |
1151 |
307 |
Debug("parser") << "Partial application of " << args[0]; |
1152 |
307 |
Debug("parser") << " : #argTypes = " << arity; |
1153 |
307 |
Debug("parser") << ", #args = " << args.size() - 1 << std::endl; |
1154 |
614 |
api::Term ret = d_solver->mkTerm(api::HO_APPLY, args); |
1155 |
614 |
Debug("parser") << "applyParseOp: return curry higher order " << ret |
1156 |
307 |
<< std::endl; |
1157 |
|
// must curry the partial application |
1158 |
307 |
return ret; |
1159 |
|
} |
1160 |
|
} |
1161 |
|
} |
1162 |
402740 |
if (!op.isNull()) |
1163 |
|
{ |
1164 |
152889 |
api::Term ret = d_solver->mkTerm(op, args); |
1165 |
76444 |
Debug("parser") << "applyParseOp: return op : " << ret << std::endl; |
1166 |
76444 |
return ret; |
1167 |
|
} |
1168 |
326295 |
if (kind == api::NULL_EXPR) |
1169 |
|
{ |
1170 |
|
// should never happen in the new API |
1171 |
|
parseError("do not know how to process parse op"); |
1172 |
|
} |
1173 |
652590 |
Debug("parser") << "Try default term construction for kind " << kind |
1174 |
326295 |
<< " #args = " << args.size() << "..." << std::endl; |
1175 |
652589 |
api::Term ret = d_solver->mkTerm(kind, args); |
1176 |
326294 |
Debug("parser") << "applyParseOp: return : " << ret << std::endl; |
1177 |
326294 |
return ret; |
1178 |
|
} |
1179 |
|
|
1180 |
4673 |
void Smt2::notifyNamedExpression(api::Term& expr, std::string name) |
1181 |
|
{ |
1182 |
4673 |
checkUserSymbol(name); |
1183 |
|
// remember the expression name in the symbol manager |
1184 |
9346 |
if (getSymbolManager()->setExpressionName(expr, name, false) |
1185 |
4673 |
== NamingResult::ERROR_IN_BINDER) |
1186 |
|
{ |
1187 |
2 |
parseError( |
1188 |
|
"Cannot name a term in a binder (e.g., quantifiers, definitions)"); |
1189 |
|
} |
1190 |
|
// define the variable |
1191 |
4672 |
defineVar(name, expr); |
1192 |
|
// set the last named term, which ensures that we catch when assertions are |
1193 |
|
// named |
1194 |
4672 |
setLastNamedTerm(expr, name); |
1195 |
4672 |
} |
1196 |
|
|
1197 |
|
api::Term Smt2::mkAnd(const std::vector<api::Term>& es) |
1198 |
|
{ |
1199 |
|
if (es.size() == 0) |
1200 |
|
{ |
1201 |
|
return d_solver->mkTrue(); |
1202 |
|
} |
1203 |
|
else if (es.size() == 1) |
1204 |
|
{ |
1205 |
|
return es[0]; |
1206 |
|
} |
1207 |
|
else |
1208 |
|
{ |
1209 |
|
return d_solver->mkTerm(api::AND, es); |
1210 |
|
} |
1211 |
|
} |
1212 |
|
|
1213 |
|
} // namespace parser |
1214 |
29583 |
} // namespace cvc5 |