Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Andres Noetzli
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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_state.h"
16 : :
17 : : #include <algorithm>
18 : :
19 : : #include "base/check.h"
20 : : #include "base/output.h"
21 : : #include "parser/commands.h"
22 : : #include "util/floatingpoint_size.h"
23 : :
24 : : namespace cvc5 {
25 : : namespace parser {
26 : :
27 : 24101 : Smt2State::Smt2State(ParserStateCallback* psc,
28 : : Solver* solver,
29 : : SymManager* sm,
30 : : ParsingMode parsingMode,
31 : 24101 : bool isSygus)
32 : : : ParserState(psc, solver, sm, parsingMode),
33 : : d_isSygus(isSygus),
34 : 24101 : d_logicSet(false)
35 : : {
36 : 24101 : d_freshBinders = (d_solver->getOption("fresh-binders") == "true");
37 : 24101 : }
38 : :
39 : 24080 : Smt2State::~Smt2State() {}
40 : :
41 : 29556 : void Smt2State::addArithmeticOperators()
42 : : {
43 : 29556 : addOperator(Kind::ADD, "+");
44 : 29556 : addOperator(Kind::SUB, "-");
45 : : // SUB is converted to NEG if there is only a single operand
46 : 29556 : ParserState::addOperator(Kind::NEG);
47 : 29556 : addOperator(Kind::MULT, "*");
48 : 29556 : addOperator(Kind::LT, "<");
49 : 29556 : addOperator(Kind::LEQ, "<=");
50 : 29556 : addOperator(Kind::GT, ">");
51 : 29556 : addOperator(Kind::GEQ, ">=");
52 : :
53 [ + + ]: 29556 : if (!strictModeEnabled())
54 : : {
55 : : // NOTE: this operator is non-standard
56 : 29519 : addOperator(Kind::POW, "^");
57 : : }
58 : 29556 : }
59 : :
60 : 11346 : void Smt2State::addTranscendentalOperators()
61 : : {
62 : 11346 : addOperator(Kind::EXPONENTIAL, "exp");
63 : 11346 : addOperator(Kind::SINE, "sin");
64 : 11346 : addOperator(Kind::COSINE, "cos");
65 : 11346 : addOperator(Kind::TANGENT, "tan");
66 : 11346 : addOperator(Kind::COSECANT, "csc");
67 : 11346 : addOperator(Kind::SECANT, "sec");
68 : 11346 : addOperator(Kind::COTANGENT, "cot");
69 : 11346 : addOperator(Kind::ARCSINE, "arcsin");
70 : 11346 : addOperator(Kind::ARCCOSINE, "arccos");
71 : 11346 : addOperator(Kind::ARCTANGENT, "arctan");
72 : 11346 : addOperator(Kind::ARCCOSECANT, "arccsc");
73 : 11346 : addOperator(Kind::ARCSECANT, "arcsec");
74 : 11346 : addOperator(Kind::ARCCOTANGENT, "arccot");
75 : 11346 : addOperator(Kind::SQRT, "sqrt");
76 : 11346 : }
77 : :
78 : 13864 : void Smt2State::addQuantifiersOperators() {}
79 : :
80 : 15554 : void Smt2State::addBitvectorOperators()
81 : : {
82 : 15554 : addOperator(Kind::BITVECTOR_CONCAT, "concat");
83 : 15554 : addOperator(Kind::BITVECTOR_NOT, "bvnot");
84 : 15554 : addOperator(Kind::BITVECTOR_AND, "bvand");
85 : 15554 : addOperator(Kind::BITVECTOR_OR, "bvor");
86 : 15554 : addOperator(Kind::BITVECTOR_NEG, "bvneg");
87 : 15554 : addOperator(Kind::BITVECTOR_ADD, "bvadd");
88 : 15554 : addOperator(Kind::BITVECTOR_MULT, "bvmul");
89 : 15554 : addOperator(Kind::BITVECTOR_UDIV, "bvudiv");
90 : 15554 : addOperator(Kind::BITVECTOR_UREM, "bvurem");
91 : 15554 : addOperator(Kind::BITVECTOR_SHL, "bvshl");
92 : 15554 : addOperator(Kind::BITVECTOR_LSHR, "bvlshr");
93 : 15554 : addOperator(Kind::BITVECTOR_ULT, "bvult");
94 : 15554 : addOperator(Kind::BITVECTOR_NAND, "bvnand");
95 : 15554 : addOperator(Kind::BITVECTOR_NOR, "bvnor");
96 : 15554 : addOperator(Kind::BITVECTOR_XOR, "bvxor");
97 : 15554 : addOperator(Kind::BITVECTOR_XNOR, "bvxnor");
98 : 15554 : addOperator(Kind::BITVECTOR_COMP, "bvcomp");
99 : 15554 : addOperator(Kind::BITVECTOR_SUB, "bvsub");
100 : 15554 : addOperator(Kind::BITVECTOR_SDIV, "bvsdiv");
101 : 15554 : addOperator(Kind::BITVECTOR_SREM, "bvsrem");
102 : 15554 : addOperator(Kind::BITVECTOR_SMOD, "bvsmod");
103 : 15554 : addOperator(Kind::BITVECTOR_ASHR, "bvashr");
104 : 15554 : addOperator(Kind::BITVECTOR_ULE, "bvule");
105 : 15554 : addOperator(Kind::BITVECTOR_UGT, "bvugt");
106 : 15554 : addOperator(Kind::BITVECTOR_UGE, "bvuge");
107 : 15554 : addOperator(Kind::BITVECTOR_SLT, "bvslt");
108 : 15554 : addOperator(Kind::BITVECTOR_SLE, "bvsle");
109 : 15554 : addOperator(Kind::BITVECTOR_SGT, "bvsgt");
110 : 15554 : addOperator(Kind::BITVECTOR_SGE, "bvsge");
111 : 15554 : addOperator(Kind::BITVECTOR_REDOR, "bvredor");
112 : 15554 : addOperator(Kind::BITVECTOR_REDAND, "bvredand");
113 : 15554 : addOperator(Kind::BITVECTOR_NEGO, "bvnego");
114 : 15554 : addOperator(Kind::BITVECTOR_UADDO, "bvuaddo");
115 : 15554 : addOperator(Kind::BITVECTOR_SADDO, "bvsaddo");
116 : 15554 : addOperator(Kind::BITVECTOR_UMULO, "bvumulo");
117 : 15554 : addOperator(Kind::BITVECTOR_SMULO, "bvsmulo");
118 : 15554 : addOperator(Kind::BITVECTOR_USUBO, "bvusubo");
119 : 15554 : addOperator(Kind::BITVECTOR_SSUBO, "bvssubo");
120 : 15554 : addOperator(Kind::BITVECTOR_SDIVO, "bvsdivo");
121 [ + + ]: 15554 : if (!strictModeEnabled())
122 : : {
123 : 15533 : addOperator(Kind::BITVECTOR_ITE, "bvite");
124 : : }
125 : :
126 : :
127 : 15554 : addIndexedOperator(Kind::BITVECTOR_EXTRACT, "extract");
128 : 15554 : addIndexedOperator(Kind::BITVECTOR_REPEAT, "repeat");
129 : 15554 : addIndexedOperator(Kind::BITVECTOR_ZERO_EXTEND, "zero_extend");
130 : 15554 : addIndexedOperator(Kind::BITVECTOR_SIGN_EXTEND, "sign_extend");
131 : 15554 : addIndexedOperator(Kind::BITVECTOR_ROTATE_LEFT, "rotate_left");
132 : 15554 : addIndexedOperator(Kind::BITVECTOR_ROTATE_RIGHT, "rotate_right");
133 : 15554 : }
134 : :
135 : 11386 : void Smt2State::addFiniteFieldOperators()
136 : : {
137 : 11386 : addOperator(cvc5::Kind::FINITE_FIELD_ADD, "ff.add");
138 : 11386 : addOperator(cvc5::Kind::FINITE_FIELD_MULT, "ff.mul");
139 : 11386 : addOperator(cvc5::Kind::FINITE_FIELD_NEG, "ff.neg");
140 : 11386 : addOperator(cvc5::Kind::FINITE_FIELD_BITSUM, "ff.bitsum");
141 : 11386 : }
142 : :
143 : 11441 : void Smt2State::addDatatypesOperators()
144 : : {
145 : 11441 : ParserState::addOperator(Kind::APPLY_CONSTRUCTOR);
146 : 11441 : ParserState::addOperator(Kind::APPLY_TESTER);
147 : 11441 : ParserState::addOperator(Kind::APPLY_SELECTOR);
148 : :
149 : 11441 : addIndexedOperator(Kind::APPLY_TESTER, "is");
150 [ + + ]: 11441 : if (!strictModeEnabled())
151 : : {
152 : 11432 : ParserState::addOperator(Kind::APPLY_UPDATER);
153 : 11432 : addIndexedOperator(Kind::APPLY_UPDATER, "update");
154 : : // Tuple projection is both indexed and non-indexed (when indices are empty)
155 : 11432 : addOperator(Kind::TUPLE_PROJECT, "tuple.project");
156 : 11432 : addIndexedOperator(Kind::TUPLE_PROJECT, "tuple.project");
157 : : // Notice that tuple operators, we use the UNDEFINED_KIND kind.
158 : : // These are processed based on the context in which they are parsed, e.g.
159 : : // when parsing identifiers.
160 : : // For the tuple constructor "tuple", this is both a nullary operator
161 : : // (for the 0-ary tuple), and a operator, hence we call both addOperator
162 : : // and defineVar here.
163 : 11432 : addOperator(Kind::APPLY_CONSTRUCTOR, "tuple");
164 : 11432 : defineVar("tuple.unit", d_tm.mkTuple({}));
165 : 11432 : addIndexedOperator(Kind::UNDEFINED_KIND, "tuple.select");
166 : 11432 : addIndexedOperator(Kind::UNDEFINED_KIND, "tuple.update");
167 : 11432 : Sort btype = d_tm.getBooleanSort();
168 : 11432 : defineVar("nullable.null", d_tm.mkNullableNull(d_tm.mkNullableSort(btype)));
169 : 11432 : addOperator(Kind::APPLY_CONSTRUCTOR, "nullable.some");
170 : 11432 : addOperator(Kind::APPLY_SELECTOR, "nullable.val");
171 : 11432 : addOperator(Kind::NULLABLE_LIFT, "nullable.lift");
172 : 11432 : addOperator(Kind::APPLY_TESTER, "nullable.is_null");
173 : 11432 : addOperator(Kind::APPLY_TESTER, "nullable.is_some");
174 : 11432 : addIndexedOperator(Kind::NULLABLE_LIFT, "nullable.lift");
175 : : }
176 : 11441 : }
177 : :
178 : 12718 : void Smt2State::addStringOperators()
179 : : {
180 : 12718 : defineVar("re.all", d_tm.mkRegexpAll());
181 : 12718 : addOperator(Kind::STRING_CONCAT, "str.++");
182 : 12718 : addOperator(Kind::STRING_LENGTH, "str.len");
183 : 12718 : addOperator(Kind::STRING_SUBSTR, "str.substr");
184 : 12718 : addOperator(Kind::STRING_CONTAINS, "str.contains");
185 : 12718 : addOperator(Kind::STRING_CHARAT, "str.at");
186 : 12718 : addOperator(Kind::STRING_INDEXOF, "str.indexof");
187 : 12718 : addOperator(Kind::STRING_REPLACE, "str.replace");
188 : 12718 : addOperator(Kind::STRING_PREFIX, "str.prefixof");
189 : 12718 : addOperator(Kind::STRING_SUFFIX, "str.suffixof");
190 : 12718 : addOperator(Kind::STRING_FROM_CODE, "str.from_code");
191 : 12718 : addOperator(Kind::STRING_IS_DIGIT, "str.is_digit");
192 : 12718 : addOperator(Kind::STRING_REPLACE_RE, "str.replace_re");
193 : 12718 : addOperator(Kind::STRING_REPLACE_RE_ALL, "str.replace_re_all");
194 [ + + ]: 12718 : if (!strictModeEnabled())
195 : : {
196 : 12709 : addOperator(Kind::STRING_INDEXOF_RE, "str.indexof_re");
197 : 12709 : addOperator(Kind::STRING_UPDATE, "str.update");
198 : 12709 : addOperator(Kind::STRING_TO_LOWER, "str.to_lower");
199 : 12709 : addOperator(Kind::STRING_TO_UPPER, "str.to_upper");
200 : 12709 : addOperator(Kind::STRING_REV, "str.rev");
201 : : // sequence versions
202 : 12709 : addOperator(Kind::SEQ_CONCAT, "seq.++");
203 : 12709 : addOperator(Kind::SEQ_LENGTH, "seq.len");
204 : 12709 : addOperator(Kind::SEQ_EXTRACT, "seq.extract");
205 : 12709 : addOperator(Kind::SEQ_UPDATE, "seq.update");
206 : 12709 : addOperator(Kind::SEQ_AT, "seq.at");
207 : 12709 : addOperator(Kind::SEQ_CONTAINS, "seq.contains");
208 : 12709 : addOperator(Kind::SEQ_INDEXOF, "seq.indexof");
209 : 12709 : addOperator(Kind::SEQ_REPLACE, "seq.replace");
210 : 12709 : addOperator(Kind::SEQ_PREFIX, "seq.prefixof");
211 : 12709 : addOperator(Kind::SEQ_SUFFIX, "seq.suffixof");
212 : 12709 : addOperator(Kind::SEQ_REV, "seq.rev");
213 : 12709 : addOperator(Kind::SEQ_REPLACE_ALL, "seq.replace_all");
214 : 12709 : addOperator(Kind::SEQ_UNIT, "seq.unit");
215 : 12709 : addOperator(Kind::SEQ_NTH, "seq.nth");
216 : : }
217 : 12718 : addOperator(Kind::STRING_FROM_INT, "str.from_int");
218 : 12718 : addOperator(Kind::STRING_TO_INT, "str.to_int");
219 : 12718 : addOperator(Kind::STRING_IN_REGEXP, "str.in_re");
220 : 12718 : addOperator(Kind::STRING_TO_REGEXP, "str.to_re");
221 : 12718 : addOperator(Kind::STRING_TO_CODE, "str.to_code");
222 : 12718 : addOperator(Kind::STRING_REPLACE_ALL, "str.replace_all");
223 : :
224 : 12718 : addOperator(Kind::REGEXP_CONCAT, "re.++");
225 : 12718 : addOperator(Kind::REGEXP_UNION, "re.union");
226 : 12718 : addOperator(Kind::REGEXP_INTER, "re.inter");
227 : 12718 : addOperator(Kind::REGEXP_STAR, "re.*");
228 : 12718 : addOperator(Kind::REGEXP_PLUS, "re.+");
229 : 12718 : addOperator(Kind::REGEXP_OPT, "re.opt");
230 : 12718 : addIndexedOperator(Kind::REGEXP_REPEAT, "re.^");
231 : 12718 : addIndexedOperator(Kind::REGEXP_LOOP, "re.loop");
232 : 12718 : addOperator(Kind::REGEXP_RANGE, "re.range");
233 : 12718 : addOperator(Kind::REGEXP_COMPLEMENT, "re.comp");
234 : 12718 : addOperator(Kind::REGEXP_DIFF, "re.diff");
235 : 12718 : addOperator(Kind::STRING_LT, "str.<");
236 : 12718 : addOperator(Kind::STRING_LEQ, "str.<=");
237 : 12718 : }
238 : :
239 : 11211 : void Smt2State::addFloatingPointOperators()
240 : : {
241 : 11211 : addOperator(Kind::FLOATINGPOINT_FP, "fp");
242 : 11211 : addOperator(Kind::FLOATINGPOINT_EQ, "fp.eq");
243 : 11211 : addOperator(Kind::FLOATINGPOINT_ABS, "fp.abs");
244 : 11211 : addOperator(Kind::FLOATINGPOINT_NEG, "fp.neg");
245 : 11211 : addOperator(Kind::FLOATINGPOINT_ADD, "fp.add");
246 : 11211 : addOperator(Kind::FLOATINGPOINT_SUB, "fp.sub");
247 : 11211 : addOperator(Kind::FLOATINGPOINT_MULT, "fp.mul");
248 : 11211 : addOperator(Kind::FLOATINGPOINT_DIV, "fp.div");
249 : 11211 : addOperator(Kind::FLOATINGPOINT_FMA, "fp.fma");
250 : 11211 : addOperator(Kind::FLOATINGPOINT_SQRT, "fp.sqrt");
251 : 11211 : addOperator(Kind::FLOATINGPOINT_REM, "fp.rem");
252 : 11211 : addOperator(Kind::FLOATINGPOINT_RTI, "fp.roundToIntegral");
253 : 11211 : addOperator(Kind::FLOATINGPOINT_MIN, "fp.min");
254 : 11211 : addOperator(Kind::FLOATINGPOINT_MAX, "fp.max");
255 : 11211 : addOperator(Kind::FLOATINGPOINT_LEQ, "fp.leq");
256 : 11211 : addOperator(Kind::FLOATINGPOINT_LT, "fp.lt");
257 : 11211 : addOperator(Kind::FLOATINGPOINT_GEQ, "fp.geq");
258 : 11211 : addOperator(Kind::FLOATINGPOINT_GT, "fp.gt");
259 : 11211 : addOperator(Kind::FLOATINGPOINT_IS_NORMAL, "fp.isNormal");
260 : 11211 : addOperator(Kind::FLOATINGPOINT_IS_SUBNORMAL, "fp.isSubnormal");
261 : 11211 : addOperator(Kind::FLOATINGPOINT_IS_ZERO, "fp.isZero");
262 : 11211 : addOperator(Kind::FLOATINGPOINT_IS_INF, "fp.isInfinite");
263 : 11211 : addOperator(Kind::FLOATINGPOINT_IS_NAN, "fp.isNaN");
264 : 11211 : addOperator(Kind::FLOATINGPOINT_IS_NEG, "fp.isNegative");
265 : 11211 : addOperator(Kind::FLOATINGPOINT_IS_POS, "fp.isPositive");
266 : 11211 : addOperator(Kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
267 : :
268 : 11211 : addIndexedOperator(Kind::UNDEFINED_KIND, "to_fp");
269 : 11211 : addIndexedOperator(Kind::FLOATINGPOINT_TO_FP_FROM_UBV, "to_fp_unsigned");
270 : 11211 : addIndexedOperator(Kind::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
271 : 11211 : addIndexedOperator(Kind::FLOATINGPOINT_TO_SBV, "fp.to_sbv");
272 : :
273 [ + + ]: 11211 : if (!strictModeEnabled())
274 : : {
275 : 11198 : addIndexedOperator(Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV, "to_fp_bv");
276 : 11198 : addIndexedOperator(Kind::FLOATINGPOINT_TO_FP_FROM_FP, "to_fp_fp");
277 : 11198 : addIndexedOperator(Kind::FLOATINGPOINT_TO_FP_FROM_REAL, "to_fp_real");
278 : 11198 : addIndexedOperator(Kind::FLOATINGPOINT_TO_FP_FROM_SBV, "to_fp_signed");
279 : : }
280 : 11211 : }
281 : :
282 : 11053 : void Smt2State::addSepOperators()
283 : : {
284 : 11053 : defineVar("sep.emp", d_tm.mkSepEmp());
285 : : // the Boolean sort is a placeholder here since we don't have type info
286 : : // without type annotation
287 : 11053 : defineVar("sep.nil", d_tm.mkSepNil(d_tm.getBooleanSort()));
288 : 11053 : addOperator(Kind::SEP_STAR, "sep");
289 : 11053 : addOperator(Kind::SEP_PTO, "pto");
290 : 11053 : addOperator(Kind::SEP_WAND, "wand");
291 : 11053 : ParserState::addOperator(Kind::SEP_STAR);
292 : 11053 : ParserState::addOperator(Kind::SEP_PTO);
293 : 11053 : ParserState::addOperator(Kind::SEP_WAND);
294 : 11053 : }
295 : :
296 : 24056 : void Smt2State::addCoreSymbols()
297 : : {
298 : 24056 : defineType("Bool", d_tm.getBooleanSort(), false);
299 : 24056 : Sort tupleSort = d_tm.mkTupleSort({});
300 : 24056 : defineType("Relation", d_tm.mkSetSort(tupleSort), false);
301 : 24056 : defineType("Table", d_tm.mkBagSort(tupleSort), false);
302 : 24056 : defineVar("true", d_tm.mkTrue(), true);
303 : 24056 : defineVar("false", d_tm.mkFalse(), true);
304 : 24056 : addOperator(Kind::AND, "and");
305 : 24056 : addOperator(Kind::DISTINCT, "distinct");
306 : 24056 : addOperator(Kind::EQUAL, "=");
307 : 24056 : addOperator(Kind::IMPLIES, "=>");
308 : 24056 : addOperator(Kind::ITE, "ite");
309 : 24056 : addOperator(Kind::NOT, "not");
310 : 24056 : addOperator(Kind::OR, "or");
311 : 24056 : addOperator(Kind::XOR, "xor");
312 : 24056 : addClosureKind(Kind::FORALL, "forall");
313 : 24056 : addClosureKind(Kind::EXISTS, "exists");
314 : 24056 : }
315 : :
316 : 16 : void Smt2State::addSkolemSymbols()
317 : : {
318 : 992 : for (int32_t s = static_cast<int32_t>(SkolemId::INTERNAL);
319 [ + + ]: 992 : s <= static_cast<int32_t>(SkolemId::NONE);
320 : : ++s)
321 : : {
322 : 976 : auto skolem = static_cast<SkolemId>(s);
323 : 976 : std::stringstream ss;
324 : 976 : ss << "@" << skolem;
325 : 976 : addSkolemId(skolem, ss.str());
326 : : }
327 : 16 : }
328 : :
329 : 3197040 : void Smt2State::addOperator(Kind kind, const std::string& name)
330 : : {
331 [ + - ]: 6394080 : Trace("parser") << "Smt2State::addOperator( " << kind << ", " << name << " )"
332 : 3197040 : << std::endl;
333 : 3197040 : ParserState::addOperator(kind);
334 : 3197040 : d_operatorKindMap[name] = kind;
335 : 3197040 : }
336 : :
337 : 423273 : void Smt2State::addIndexedOperator(Kind tKind, const std::string& name)
338 : : {
339 : 423273 : ParserState::addOperator(tKind);
340 : 423273 : d_indexedOpKindMap[name] = tKind;
341 : 423273 : }
342 : :
343 : 60395 : void Smt2State::addClosureKind(Kind tKind, const std::string& name)
344 : : {
345 : : // also include it as a normal operator
346 : 60395 : addOperator(tKind, name);
347 : 60395 : d_closureKindMap[name] = tKind;
348 : 60395 : }
349 : :
350 : 976 : void Smt2State::addSkolemId(SkolemId skolemID, const std::string& name)
351 : : {
352 : 976 : addOperator(Kind::SKOLEM, name);
353 : 976 : d_skolemMap[name] = skolemID;
354 : 976 : }
355 : :
356 : 0 : bool Smt2State::isIndexedOperatorEnabled(const std::string& name) const
357 : : {
358 : 0 : return d_indexedOpKindMap.find(name) != d_indexedOpKindMap.end();
359 : : }
360 : :
361 : 5176160 : Kind Smt2State::getOperatorKind(const std::string& name) const
362 : : {
363 : : // precondition: isOperatorEnabled(name)
364 : 5176160 : return d_operatorKindMap.find(name)->second;
365 : : }
366 : :
367 : 6335660 : bool Smt2State::isOperatorEnabled(const std::string& name) const
368 : : {
369 : 6335660 : return d_operatorKindMap.find(name) != d_operatorKindMap.end();
370 : : }
371 : :
372 : 38 : modes::BlockModelsMode Smt2State::getBlockModelsMode(const std::string& mode)
373 : : {
374 [ + + ]: 38 : if (mode == "literals")
375 : : {
376 : 22 : return modes::BlockModelsMode::LITERALS;
377 : : }
378 [ + - ]: 16 : else if (mode == "values")
379 : : {
380 : 16 : return modes::BlockModelsMode::VALUES;
381 : : }
382 : 0 : parseError(std::string("Unknown block models mode `") + mode + "'");
383 : 0 : return modes::BlockModelsMode::LITERALS;
384 : : }
385 : :
386 : 23 : modes::LearnedLitType Smt2State::getLearnedLitType(const std::string& mode)
387 : : {
388 [ + + ]: 23 : if (mode == "preprocess_solved")
389 : : {
390 : 4 : return modes::LearnedLitType::PREPROCESS_SOLVED;
391 : : }
392 [ + + ]: 19 : else if (mode == "preprocess")
393 : : {
394 : 4 : return modes::LearnedLitType::PREPROCESS;
395 : : }
396 [ + + ]: 15 : else if (mode == "input")
397 : : {
398 : 3 : return modes::LearnedLitType::INPUT;
399 : : }
400 [ + + ]: 12 : else if (mode == "solvable")
401 : : {
402 : 4 : return modes::LearnedLitType::SOLVABLE;
403 : : }
404 [ + + ]: 8 : else if (mode == "constant_prop")
405 : : {
406 : 4 : return modes::LearnedLitType::CONSTANT_PROP;
407 : : }
408 [ + - ]: 4 : else if (mode == "internal")
409 : : {
410 : 4 : return modes::LearnedLitType::INTERNAL;
411 : : }
412 : 0 : parseError(std::string("Unknown learned literal type `") + mode + "'");
413 : 0 : return modes::LearnedLitType::UNKNOWN;
414 : : }
415 : :
416 : 25 : modes::ProofComponent Smt2State::getProofComponent(const std::string& pc)
417 : : {
418 [ + + ]: 25 : if (pc == "raw_preprocess")
419 : : {
420 : 5 : return modes::ProofComponent::RAW_PREPROCESS;
421 : : }
422 [ + + ]: 20 : else if (pc == "preprocess")
423 : : {
424 : 5 : return modes::ProofComponent::PREPROCESS;
425 : : }
426 [ + + ]: 15 : else if (pc == "sat")
427 : : {
428 : 6 : return modes::ProofComponent::SAT;
429 : : }
430 [ + + ]: 9 : else if (pc == "theory_lemmas")
431 : : {
432 : 5 : return modes::ProofComponent::THEORY_LEMMAS;
433 : : }
434 [ + - ]: 4 : else if (pc == "full")
435 : : {
436 : 4 : return modes::ProofComponent::FULL;
437 : : }
438 : 0 : parseError(std::string("Unknown proof component `") + pc + "'");
439 : 0 : return modes::ProofComponent::FULL;
440 : : }
441 : :
442 : 93 : modes::FindSynthTarget Smt2State::getFindSynthTarget(const std::string& fst)
443 : : {
444 [ + + ]: 93 : if (fst == "enum")
445 : : {
446 : 3 : return modes::FindSynthTarget::ENUM;
447 : : }
448 [ + + ]: 90 : else if (fst == "rewrite")
449 : : {
450 : 24 : return modes::FindSynthTarget::REWRITE;
451 : : }
452 [ + + ]: 66 : else if (fst == "rewrite_unsound")
453 : : {
454 : 24 : return modes::FindSynthTarget::REWRITE_UNSOUND;
455 : : }
456 [ + + ]: 42 : else if (fst == "rewrite_input")
457 : : {
458 : 30 : return modes::FindSynthTarget::REWRITE_INPUT;
459 : : }
460 [ + - ]: 12 : else if (fst == "query")
461 : : {
462 : 12 : return modes::FindSynthTarget::QUERY;
463 : : }
464 : 0 : parseError(std::string("Unknown find synth target `") + fst + "'");
465 : 0 : return modes::FindSynthTarget::ENUM;
466 : : }
467 : :
468 : 13282 : bool Smt2State::isTheoryEnabled(internal::theory::TheoryId theory) const
469 : : {
470 : 13282 : return d_logic.isTheoryEnabled(theory);
471 : : }
472 : :
473 : 1196980 : bool Smt2State::isHoEnabled() const { return d_logic.isHigherOrder(); }
474 : :
475 : 0 : bool Smt2State::hasCardinalityConstraints() const
476 : : {
477 : 0 : return d_logic.hasCardinalityConstraints();
478 : : }
479 : :
480 : 613949 : bool Smt2State::logicIsSet() { return d_logicSet; }
481 : :
482 : 0 : bool Smt2State::getTesterName(Term cons, std::string& name)
483 : : {
484 [ - - ]: 0 : if (strictModeEnabled())
485 : : {
486 : : // 2.6 or above uses indexed tester symbols, if we are in strict mode,
487 : : // we do not automatically define is-cons for constructor cons.
488 : 0 : return false;
489 : : }
490 : 0 : std::stringstream ss;
491 : 0 : ss << "is-" << cons;
492 : 0 : name = ss.str();
493 : 0 : return true;
494 : : }
495 : :
496 : 183658 : Term Smt2State::mkIndexedConstant(const std::string& name,
497 : : const std::vector<uint32_t>& numerals)
498 : : {
499 [ + + ]: 183658 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_FP))
500 : : {
501 [ + + ]: 3024 : if (name == "+oo")
502 : : {
503 [ - + ]: 9 : if (numerals.size() != 2)
504 : : {
505 : 0 : parseError("Unexpected number of numerals for +oo.");
506 : : }
507 : 9 : return d_tm.mkFloatingPointPosInf(numerals[0], numerals[1]);
508 : : }
509 [ + + ]: 3015 : else if (name == "-oo")
510 : : {
511 [ - + ]: 18 : if (numerals.size() != 2)
512 : : {
513 : 0 : parseError("Unexpected number of numerals for -oo.");
514 : : }
515 : 18 : return d_tm.mkFloatingPointNegInf(numerals[0], numerals[1]);
516 : : }
517 [ + + ]: 2997 : else if (name == "NaN")
518 : : {
519 [ - + ]: 15 : if (numerals.size() != 2)
520 : : {
521 : 0 : parseError("Unexpected number of numerals for NaN.");
522 : : }
523 : 15 : return d_tm.mkFloatingPointNaN(numerals[0], numerals[1]);
524 : : }
525 [ + + ]: 2982 : else if (name == "+zero")
526 : : {
527 [ + + ]: 29 : if (numerals.size() != 2)
528 : : {
529 : 3 : parseError("Unexpected number of numerals for +zero.");
530 : : }
531 : 28 : return d_tm.mkFloatingPointPosZero(numerals[0], numerals[1]);
532 : : }
533 [ + + ]: 2953 : else if (name == "-zero")
534 : : {
535 [ - + ]: 18 : if (numerals.size() != 2)
536 : : {
537 : 0 : parseError("Unexpected number of numerals for -zero.");
538 : : }
539 : 18 : return d_tm.mkFloatingPointNegZero(numerals[0], numerals[1]);
540 : : }
541 : : }
542 : :
543 : 183569 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_BV)
544 [ + - ][ + - ]: 183569 : && name.find("bv") == 0)
[ + - ]
545 : : {
546 [ - + ]: 183569 : if (numerals.size() != 1)
547 : : {
548 : 0 : parseError("Unexpected number of numerals for bit-vector constant.");
549 : : }
550 : 367138 : std::string bvStr = name.substr(2);
551 : 183569 : return d_tm.mkBitVector(numerals[0], bvStr, 10);
552 : : }
553 : :
554 : : // NOTE: Theory parametric constants go here
555 : :
556 : 0 : parseError(std::string("Unknown indexed literal `") + name + "'");
557 : 0 : return Term();
558 : : }
559 : :
560 : 118 : Term Smt2State::mkIndexedConstant(const std::string& name,
561 : : const std::vector<std::string>& symbols)
562 : : {
563 [ + + ]: 118 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_STRINGS))
564 : : {
565 [ + - ]: 14 : if (name == "char")
566 : : {
567 [ - + ]: 14 : if (symbols.size() != 1)
568 : : {
569 : 0 : parseError("Unexpected number of indices for char");
570 : : }
571 [ + - ][ - + ]: 14 : if (symbols[0].length() <= 2 || symbols[0].substr(0, 2) != "#x")
[ + - ][ - + ]
[ - - ]
572 : : {
573 : 0 : parseError(std::string("Unexpected index for char: `") + symbols[0]
574 : 0 : + "'");
575 : : }
576 : 28 : return mkCharConstant(symbols[0].substr(2));
577 : : }
578 : : }
579 [ + - ]: 104 : else if (d_logic.hasCardinalityConstraints())
580 : : {
581 [ + - ]: 104 : if (name == "fmf.card")
582 : : {
583 [ - + ]: 104 : if (symbols.size() != 2)
584 : : {
585 : 0 : parseError("Unexpected number of indices for fmf.card");
586 : : }
587 : 208 : Sort t = getSort(symbols[0]);
588 : : // convert second symbol back to a numeral
589 : 104 : uint32_t ubound = stringToUnsigned(symbols[1]);
590 : 104 : return d_tm.mkCardinalityConstraint(t, ubound);
591 : : }
592 : : }
593 : 0 : parseError(std::string("Unknown indexed literal `") + name + "'");
594 : 0 : return Term();
595 : : }
596 : :
597 : 4443 : Term Smt2State::mkIndexedOp(Kind k,
598 : : const std::vector<std::string>& symbols,
599 : : const std::vector<Term>& args)
600 : : {
601 [ + + ][ + - ]: 4443 : if (k == Kind::APPLY_TESTER || k == Kind::APPLY_UPDATER)
602 : : {
603 [ - + ][ - + ]: 4443 : Assert(symbols.size() == 1);
[ - - ]
604 [ + + ]: 4443 : if (args.empty())
605 : : {
606 : 3 : parseError("Expected argument to tester/updater");
607 : : }
608 : 4442 : const std::string& cname = symbols[0];
609 : : // must be declared
610 : 4442 : checkDeclaration(cname, CHECK_DECLARED, SYM_VARIABLE);
611 : 8884 : Term f = getExpressionForNameAndType(cname, args[0].getSort());
612 [ + + ][ + - ]: 4442 : if (f.getKind() == Kind::APPLY_CONSTRUCTOR && f.getNumChildren() == 1)
[ + + ]
613 : : {
614 : : // for nullary constructors, must get the operator
615 : 1010 : f = f[0];
616 : : }
617 [ + + ]: 4442 : if (k == Kind::APPLY_TESTER)
618 : : {
619 [ - + ]: 4328 : if (!f.getSort().isDatatypeConstructor())
620 : : {
621 : 0 : parseError("Bad syntax for (_ is X), X must be a constructor.");
622 : : }
623 : : // get the datatype that f belongs to
624 : 8656 : Sort sf = f.getSort().getDatatypeConstructorCodomainSort();
625 : 8656 : Datatype d = sf.getDatatype();
626 : : // lookup by name
627 : 8656 : DatatypeConstructor dc = d.getConstructor(f.toString());
628 : 4328 : return dc.getTesterTerm();
629 : : }
630 : : else
631 : : {
632 [ - + ][ - + ]: 114 : Assert(k == Kind::APPLY_UPDATER);
[ - - ]
633 [ - + ]: 114 : if (!f.getSort().isDatatypeSelector())
634 : : {
635 : 0 : parseError("Bad syntax for (_ update X), X must be a selector.");
636 : : }
637 : 228 : std::string sname = f.toString();
638 : : // get the datatype that f belongs to
639 : 228 : Sort sf = f.getSort().getDatatypeSelectorDomainSort();
640 : 228 : Datatype d = sf.getDatatype();
641 : : // find the selector
642 : 228 : DatatypeSelector ds = d.getSelector(f.toString());
643 : : // get the updater term
644 : 114 : return ds.getUpdaterTerm();
645 : : }
646 : : }
647 : 0 : std::stringstream ss;
648 : 0 : ss << "Unknown indexed op kind " << k;
649 : 0 : parseError(ss.str());
650 : 0 : return Term();
651 : : }
652 : :
653 : 176533 : Kind Smt2State::getIndexedOpKind(const std::string& name)
654 : : {
655 : 176533 : const auto& kIt = d_indexedOpKindMap.find(name);
656 [ + - ]: 176533 : if (kIt != d_indexedOpKindMap.end())
657 : : {
658 : 176533 : return (*kIt).second;
659 : : }
660 : 0 : parseError(std::string("Unknown indexed function `") + name + "'");
661 : 0 : return Kind::UNDEFINED_KIND;
662 : : }
663 : :
664 : 0 : Kind Smt2State::getClosureKind(const std::string& name)
665 : : {
666 : 0 : const auto& kIt = d_closureKindMap.find(name);
667 [ - - ]: 0 : if (kIt != d_closureKindMap.end())
668 : : {
669 : 0 : return (*kIt).second;
670 : : }
671 : 0 : parseError(std::string("Unknown closure `") + name + "'");
672 : 0 : return Kind::UNDEFINED_KIND;
673 : : }
674 : :
675 : 758 : Term Smt2State::setupDefineFunRecScope(
676 : : const std::string& fname,
677 : : const std::vector<std::pair<std::string, Sort>>& sortedVarNames,
678 : : Sort t,
679 : : std::vector<Term>& flattenVars)
680 : : {
681 : 1516 : std::vector<Sort> sorts;
682 [ + + ]: 2186 : for (const std::pair<std::string, Sort>& svn : sortedVarNames)
683 : : {
684 : 1428 : sorts.push_back(svn.second);
685 : : }
686 : :
687 : : // make the flattened function type, add bound variables
688 : : // to flattenVars if the defined function was given a function return type.
689 : 1516 : Sort ft = flattenFunctionType(sorts, t, flattenVars);
690 : :
691 [ + + ]: 758 : if (!sorts.empty())
692 : : {
693 : 722 : ft = d_tm.mkFunctionSort(sorts, ft);
694 : : }
695 : : // bind now, with overloading
696 : 1516 : return bindVar(fname, ft, true);
697 : : }
698 : :
699 : 758 : void Smt2State::pushDefineFunRecScope(
700 : : const std::vector<std::pair<std::string, Sort>>& sortedVarNames,
701 : : Term func,
702 : : const std::vector<Term>& flattenVars,
703 : : std::vector<Term>& bvs)
704 : : {
705 : 758 : pushScope();
706 : : // bound variables are those that are explicitly named in the preamble
707 : : // of the define-fun(s)-rec command, we define them here
708 [ + + ]: 2186 : for (const std::pair<std::string, Sort>& svn : sortedVarNames)
709 : : {
710 : 2856 : Term v = bindBoundVar(svn.first, svn.second, d_freshBinders);
711 : 1428 : bvs.push_back(v);
712 : : }
713 : :
714 : 758 : bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end());
715 : 758 : }
716 : :
717 : 83 : void Smt2State::reset()
718 : : {
719 : 83 : d_logicSet = false;
720 : 83 : d_logic = internal::LogicInfo();
721 : 83 : d_operatorKindMap.clear();
722 : 83 : d_lastNamedTerm = std::pair<Term, std::string>();
723 : 83 : }
724 : :
725 : 53 : std::unique_ptr<Cmd> Smt2State::invConstraint(
726 : : const std::vector<std::string>& names)
727 : : {
728 : 53 : checkThatLogicIsSet();
729 [ + - ]: 53 : Trace("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
730 [ + - ]: 53 : Trace("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
731 : :
732 [ - + ]: 53 : if (names.size() != 4)
733 : : {
734 : 0 : parseError(
735 : : "Bad syntax for inv-constraint: expected 4 "
736 : : "arguments.");
737 : : }
738 : :
739 : 106 : std::vector<Term> terms;
740 [ + + ]: 265 : for (const std::string& name : names)
741 : : {
742 [ - + ]: 212 : if (!isDeclared(name))
743 : : {
744 : 0 : std::stringstream ss;
745 : 0 : ss << "Function " << name << " in inv-constraint is not defined.";
746 : 0 : parseError(ss.str());
747 : : }
748 : :
749 : 212 : terms.push_back(getVariable(name));
750 : : }
751 : :
752 : 106 : return std::unique_ptr<Cmd>(new SygusInvConstraintCommand(terms));
753 : : }
754 : :
755 : 24061 : void Smt2State::setLogic(std::string name)
756 : : {
757 : 24061 : bool smLogicAlreadySet = getSymbolManager()->isLogicSet();
758 : : // if logic is already set, this is an error
759 [ + + ]: 24061 : if (d_logicSet)
760 : : {
761 : 15 : parseError("Only one set-logic is allowed.");
762 : : }
763 : 24056 : d_logicSet = true;
764 : 24056 : d_logic = name;
765 : :
766 : : // if sygus is enabled, we must enable UF, datatypes, and integer arithmetic
767 [ + + ]: 24056 : if (sygus())
768 : : {
769 [ - + ]: 963 : if (!d_logic.isQuantified())
770 : : {
771 : 0 : warning("Logics in sygus are assumed to contain quantifiers.");
772 : 0 : warning("Omit QF_ from the logic to avoid this warning.");
773 : : }
774 : : }
775 : :
776 : : // Core theory belongs to every logic
777 : 24056 : addCoreSymbols();
778 : :
779 : : // add skolems
780 [ + + ]: 24056 : if (d_solver->getOption("parse-skolem-definitions") == "true")
781 : : {
782 : 16 : addSkolemSymbols();
783 : : }
784 : :
785 [ + + ]: 24056 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_UF))
786 : : {
787 : 15094 : ParserState::addOperator(Kind::APPLY_UF);
788 : : }
789 : :
790 [ + + ]: 24056 : if (d_logic.isHigherOrder())
791 : : {
792 : 1045 : addOperator(Kind::HO_APPLY, "@");
793 : : // lambda is a closure kind
794 : 1045 : addClosureKind(Kind::LAMBDA, "lambda");
795 : : }
796 : :
797 [ + + ]: 24056 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_ARITH))
798 : : {
799 [ + + ]: 17944 : if (d_logic.areIntegersUsed())
800 : : {
801 : 16409 : defineType("Int", d_tm.getIntegerSort(), false);
802 : 16409 : addArithmeticOperators();
803 [ + + ][ + + ]: 16409 : if (!strictModeEnabled() || !d_logic.isLinear())
[ + + ]
804 : : {
805 : 16398 : addOperator(Kind::INTS_DIVISION, "div");
806 : 16398 : addOperator(Kind::INTS_MODULUS, "mod");
807 : 16398 : addOperator(Kind::ABS, "abs");
808 : : }
809 [ + + ]: 16409 : if (!strictModeEnabled())
810 : : {
811 : 16389 : addOperator(Kind::INTS_DIVISION_TOTAL, "div_total");
812 : 16389 : addOperator(Kind::INTS_MODULUS_TOTAL, "mod_total");
813 : : }
814 : 16409 : addIndexedOperator(Kind::DIVISIBLE, "divisible");
815 : : }
816 : :
817 [ + + ]: 17944 : if (d_logic.areRealsUsed())
818 : : {
819 : 13147 : defineType("Real", d_tm.getRealSort(), false);
820 : 13147 : addArithmeticOperators();
821 : 13147 : addOperator(Kind::DIVISION, "/");
822 [ + + ]: 13147 : if (!strictModeEnabled())
823 : : {
824 : 13130 : addOperator(Kind::ABS, "abs");
825 : 13130 : addOperator(Kind::DIVISION_TOTAL, "/_total");
826 : : }
827 : : }
828 : :
829 [ + + ][ + + ]: 17944 : if (d_logic.areIntegersUsed() && d_logic.areRealsUsed())
[ + + ]
830 : : {
831 : 11612 : addOperator(Kind::TO_INTEGER, "to_int");
832 : 11612 : addOperator(Kind::IS_INTEGER, "is_int");
833 : 11612 : addOperator(Kind::TO_REAL, "to_real");
834 : : }
835 : :
836 [ + + ]: 17944 : if (d_logic.areTranscendentalsUsed())
837 : : {
838 : 11346 : defineVar("real.pi", d_tm.mkPi());
839 : 11346 : addTranscendentalOperators();
840 : : }
841 [ + + ]: 17944 : if (!strictModeEnabled())
842 : : {
843 : : // integer version of AND
844 : 17920 : addIndexedOperator(Kind::IAND, "iand");
845 : : // parametric integer version of AND
846 : 17920 : addOperator(Kind::PIAND, "piand");
847 : : // pow2
848 : 17920 : addOperator(Kind::POW2, "int.pow2");
849 : : // log2
850 : 17920 : addOperator(Kind::LOG2, "int.log2");
851 : : }
852 : : }
853 : :
854 [ + + ]: 24056 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_ARRAYS))
855 : : {
856 : 12968 : addOperator(Kind::SELECT, "select");
857 : 12968 : addOperator(Kind::STORE, "store");
858 : 12968 : addOperator(Kind::EQ_RANGE, "eqrange");
859 : : }
860 : :
861 [ + + ]: 24056 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_BV))
862 : : {
863 : 15554 : addBitvectorOperators();
864 : :
865 : 15554 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_ARITH)
866 [ + + ][ + + ]: 15554 : && d_logic.areIntegersUsed())
[ + + ]
867 : : {
868 : : // Conversions between bit-vectors and integers
869 [ + + ]: 11418 : if (!strictModeEnabled())
870 : : {
871 : : // For the sake of backwards compatability at the moment we support
872 : : // the old syntax, which in the case of bv2nat maps directly to
873 : : // Kind::BITVECTOR_UBV_TO_INT.
874 : 11409 : addOperator(Kind::BITVECTOR_UBV_TO_INT, "bv2nat");
875 : 11409 : addIndexedOperator(Kind::INT_TO_BITVECTOR, "int2bv");
876 : : }
877 : 11418 : addIndexedOperator(Kind::INT_TO_BITVECTOR, "int_to_bv");
878 : 11418 : addOperator(Kind::BITVECTOR_UBV_TO_INT, "ubv_to_int");
879 : 11418 : addOperator(Kind::BITVECTOR_SBV_TO_INT, "sbv_to_int");
880 : : }
881 : : }
882 : :
883 [ + + ]: 24056 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_DATATYPES))
884 : : {
885 : 22882 : const std::vector<Sort> types;
886 : 11441 : defineType("UnitTuple", d_tm.mkTupleSort(types), false);
887 : 11441 : addDatatypesOperators();
888 : : }
889 : :
890 [ + + ]: 24056 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_SETS))
891 : : {
892 : : // the Boolean sort is a placeholder here since we don't have type info
893 : : // without type annotation
894 : 11238 : Sort btype = d_tm.getBooleanSort();
895 : 11238 : defineVar("set.empty", d_tm.mkEmptySet(d_tm.mkSetSort(btype)));
896 : 11238 : defineVar("set.universe", d_tm.mkUniverseSet(btype));
897 : :
898 : 11238 : addOperator(Kind::SET_UNION, "set.union");
899 : 11238 : addOperator(Kind::SET_INTER, "set.inter");
900 : 11238 : addOperator(Kind::SET_MINUS, "set.minus");
901 : 11238 : addOperator(Kind::SET_SUBSET, "set.subset");
902 : 11238 : addOperator(Kind::SET_MEMBER, "set.member");
903 : 11238 : addOperator(Kind::SET_SINGLETON, "set.singleton");
904 : 11238 : addOperator(Kind::SET_INSERT, "set.insert");
905 : 11238 : addOperator(Kind::SET_CARD, "set.card");
906 : 11238 : addOperator(Kind::SET_COMPLEMENT, "set.complement");
907 : 11238 : addOperator(Kind::SET_CHOOSE, "set.choose");
908 : 11238 : addOperator(Kind::SET_IS_EMPTY, "set.is_empty");
909 : 11238 : addOperator(Kind::SET_IS_SINGLETON, "set.is_singleton");
910 : 11238 : addOperator(Kind::SET_MAP, "set.map");
911 : 11238 : addOperator(Kind::SET_FILTER, "set.filter");
912 : 11238 : addOperator(Kind::SET_ALL, "set.all");
913 : 11238 : addOperator(Kind::SET_SOME, "set.some");
914 : 11238 : addOperator(Kind::SET_FOLD, "set.fold");
915 : 11238 : addOperator(Kind::RELATION_JOIN, "rel.join");
916 : 11238 : addOperator(Kind::RELATION_TABLE_JOIN, "rel.table_join");
917 : 11238 : addOperator(Kind::RELATION_PRODUCT, "rel.product");
918 : 11238 : addOperator(Kind::RELATION_TRANSPOSE, "rel.transpose");
919 : 11238 : addOperator(Kind::RELATION_TCLOSURE, "rel.tclosure");
920 : 11238 : addOperator(Kind::RELATION_JOIN_IMAGE, "rel.join_image");
921 : 11238 : addOperator(Kind::RELATION_IDEN, "rel.iden");
922 : : // these operators can be with/without indices
923 : 11238 : addOperator(Kind::RELATION_GROUP, "rel.group");
924 : 11238 : addOperator(Kind::RELATION_AGGREGATE, "rel.aggr");
925 : 11238 : addOperator(Kind::RELATION_PROJECT, "rel.project");
926 : 11238 : addIndexedOperator(Kind::RELATION_GROUP, "rel.group");
927 : 11238 : addIndexedOperator(Kind::RELATION_TABLE_JOIN, "rel.table_join");
928 : 11238 : addIndexedOperator(Kind::RELATION_AGGREGATE, "rel.aggr");
929 : 11238 : addIndexedOperator(Kind::RELATION_PROJECT, "rel.project");
930 : : // set.comprehension is a closure kind
931 : 11238 : addClosureKind(Kind::SET_COMPREHENSION, "set.comprehension");
932 : : }
933 : :
934 [ + + ]: 24056 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_BAGS))
935 : : {
936 : : // the Boolean sort is a placeholder here since we don't have type info
937 : : // without type annotation
938 : 11042 : Sort btype = d_tm.getBooleanSort();
939 : 11042 : defineVar("bag.empty", d_tm.mkEmptyBag(d_tm.mkBagSort(btype)));
940 : 11042 : addOperator(Kind::BAG_UNION_MAX, "bag.union_max");
941 : 11042 : addOperator(Kind::BAG_UNION_DISJOINT, "bag.union_disjoint");
942 : 11042 : addOperator(Kind::BAG_INTER_MIN, "bag.inter_min");
943 : 11042 : addOperator(Kind::BAG_DIFFERENCE_SUBTRACT, "bag.difference_subtract");
944 : 11042 : addOperator(Kind::BAG_DIFFERENCE_REMOVE, "bag.difference_remove");
945 : 11042 : addOperator(Kind::BAG_SUBBAG, "bag.subbag");
946 : 11042 : addOperator(Kind::BAG_COUNT, "bag.count");
947 : 11042 : addOperator(Kind::BAG_MEMBER, "bag.member");
948 : 11042 : addOperator(Kind::BAG_SETOF, "bag.setof");
949 : 11042 : addOperator(Kind::BAG_MAKE, "bag");
950 : 11042 : addOperator(Kind::BAG_CARD, "bag.card");
951 : 11042 : addOperator(Kind::BAG_CHOOSE, "bag.choose");
952 : 11042 : addOperator(Kind::BAG_MAP, "bag.map");
953 : 11042 : addOperator(Kind::BAG_FILTER, "bag.filter");
954 : 11042 : addOperator(Kind::BAG_ALL, "bag.all");
955 : 11042 : addOperator(Kind::BAG_SOME, "bag.some");
956 : 11042 : addOperator(Kind::BAG_FOLD, "bag.fold");
957 : 11042 : addOperator(Kind::BAG_PARTITION, "bag.partition");
958 : 11042 : addOperator(Kind::TABLE_PRODUCT, "table.product");
959 : 11042 : addOperator(Kind::BAG_PARTITION, "table.group");
960 : : // these operators can be with/without indices
961 : 11042 : addOperator(Kind::TABLE_PROJECT, "table.project");
962 : 11042 : addOperator(Kind::TABLE_AGGREGATE, "table.aggr");
963 : 11042 : addOperator(Kind::TABLE_JOIN, "table.join");
964 : 11042 : addOperator(Kind::TABLE_GROUP, "table.group");
965 : 11042 : addIndexedOperator(Kind::TABLE_PROJECT, "table.project");
966 : 11042 : addIndexedOperator(Kind::TABLE_AGGREGATE, "table.aggr");
967 : 11042 : addIndexedOperator(Kind::TABLE_JOIN, "table.join");
968 : 11042 : addIndexedOperator(Kind::TABLE_GROUP, "table.group");
969 : : }
970 [ + + ]: 24056 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_STRINGS))
971 : : {
972 : 12718 : defineType("String", d_tm.getStringSort(), false);
973 : 12718 : defineType("RegLan", d_tm.getRegExpSort(), false);
974 : 12718 : defineType("Int", d_tm.getIntegerSort(), false);
975 : :
976 : 12718 : defineVar("re.none", d_tm.mkRegexpNone());
977 : 12718 : defineVar("re.allchar", d_tm.mkRegexpAllchar());
978 : :
979 : : // Boolean is a placeholder
980 : 12718 : defineVar("seq.empty", d_tm.mkEmptySequence(d_tm.getBooleanSort()));
981 : :
982 : 12718 : addStringOperators();
983 : : }
984 : :
985 [ + + ]: 24056 : if (d_logic.isQuantified())
986 : : {
987 : 13864 : addQuantifiersOperators();
988 : : }
989 : :
990 [ + + ]: 24056 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_FP))
991 : : {
992 : 11211 : defineType("RoundingMode", d_tm.getRoundingModeSort(), false);
993 : 11211 : defineType("Float16", d_tm.mkFloatingPointSort(5, 11), false);
994 : 11211 : defineType("Float32", d_tm.mkFloatingPointSort(8, 24), false);
995 : 11211 : defineType("Float64", d_tm.mkFloatingPointSort(11, 53), false);
996 : 11211 : defineType("Float128", d_tm.mkFloatingPointSort(15, 113), false);
997 : :
998 : 11211 : defineVar("RNE",
999 : 22422 : d_tm.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN));
1000 : 11211 : defineVar("roundNearestTiesToEven",
1001 : 22422 : d_tm.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN));
1002 : 11211 : defineVar("RNA",
1003 : 22422 : d_tm.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY));
1004 : 11211 : defineVar("roundNearestTiesToAway",
1005 : 22422 : d_tm.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY));
1006 : 11211 : defineVar("RTP", d_tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE));
1007 : 11211 : defineVar("roundTowardPositive",
1008 : 22422 : d_tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE));
1009 : 11211 : defineVar("RTN", d_tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_NEGATIVE));
1010 : 11211 : defineVar("roundTowardNegative",
1011 : 22422 : d_tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_NEGATIVE));
1012 : 11211 : defineVar("RTZ", d_tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
1013 : 11211 : defineVar("roundTowardZero",
1014 : 22422 : d_tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
1015 : :
1016 : 11211 : addFloatingPointOperators();
1017 : : }
1018 : :
1019 [ + + ]: 24056 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_FF))
1020 : : {
1021 : 11386 : addFiniteFieldOperators();
1022 : : }
1023 : :
1024 [ + + ]: 24056 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_SEP))
1025 : : {
1026 : 11053 : addSepOperators();
1027 : : }
1028 : :
1029 : : // Builtin symbols of the logic are declared at context level zero, hence
1030 : : // we push the outermost scope in the symbol manager here.
1031 : : // We only do this if the logic has not already been set, in which case we have already
1032 : : // pushed the outermost context (and this method redeclares the symbols which does
1033 : : // not impact the symbol manager).
1034 : : // TODO (cvc5-projects #693): refactor this so that this method is moved to the
1035 : : // symbol manager and only called once per symbol manager.
1036 [ + + ]: 24056 : if (!smLogicAlreadySet)
1037 : : {
1038 : 23839 : pushScope(true);
1039 : : }
1040 : 24056 : }
1041 : :
1042 : 808 : Grammar* Smt2State::mkGrammar(const std::vector<Term>& boundVars,
1043 : : const std::vector<Term>& ntSymbols)
1044 : : {
1045 : : d_allocGrammars.emplace_back(
1046 : 808 : new Grammar(d_solver->mkGrammar(boundVars, ntSymbols)));
1047 : 808 : return d_allocGrammars.back().get();
1048 : : }
1049 : :
1050 : 50330 : bool Smt2State::sygus() const { return d_isSygus; }
1051 : :
1052 : 0 : bool Smt2State::hasGrammars() const
1053 : : {
1054 : 0 : return sygus() || d_solver->getOption("produce-abducts") == "true"
1055 : 0 : || d_solver->getOption("produce-interpolants") == "true";
1056 : : }
1057 : :
1058 : 93960 : bool Smt2State::usingFreshBinders() const { return d_freshBinders; }
1059 : :
1060 : 613949 : void Smt2State::checkThatLogicIsSet()
1061 : : {
1062 [ + + ]: 613949 : if (!logicIsSet())
1063 : : {
1064 [ + + ]: 50 : if (strictModeEnabled())
1065 : : {
1066 : 6 : parseError("set-logic must appear before this point.");
1067 : : }
1068 : : else
1069 : : {
1070 : 48 : SymManager* sm = getSymbolManager();
1071 : : // the calls to setLogic below set the logic on the solver directly
1072 [ + + ]: 48 : if (sm->isLogicForced())
1073 : : {
1074 : 4 : setLogic(sm->getLogic());
1075 : : }
1076 : : else
1077 : : {
1078 : 44 : warning("No set-logic command was given before this point.");
1079 : 44 : warning("cvc5 will make all theories available.");
1080 : 44 : warning(
1081 : : "Consider setting a stricter logic for (likely) better "
1082 : : "performance.");
1083 : 44 : warning("To suppress this warning in the future use (set-logic ALL).");
1084 : :
1085 : 44 : setLogic("ALL");
1086 : : }
1087 : : // Set the logic directly in the solver, without a command. Notice this is
1088 : : // important since we do not want to enqueue a set-logic command and
1089 : : // fully initialize the underlying SolverEngine in the meantime before the
1090 : : // command has a chance to execute, which would lead to an error.
1091 : 96 : std::string logic = d_logic.getLogicString();
1092 : 48 : d_solver->setLogic(logic);
1093 : : // set the logic on the symbol manager as well, non-forced
1094 : 48 : sm->setLogic(logic);
1095 : : }
1096 : : }
1097 : 613947 : }
1098 : :
1099 : 11431 : void Smt2State::checkLogicAllowsFreeSorts()
1100 : : {
1101 : 11431 : if (!d_logic.isTheoryEnabled(internal::theory::THEORY_UF)
1102 [ + + ]: 108 : && !d_logic.isTheoryEnabled(internal::theory::THEORY_ARRAYS)
1103 [ - + ]: 8 : && !d_logic.isTheoryEnabled(internal::theory::THEORY_DATATYPES)
1104 [ - - ]: 0 : && !d_logic.isTheoryEnabled(internal::theory::THEORY_SETS)
1105 [ + + ][ - - ]: 11539 : && !d_logic.isTheoryEnabled(internal::theory::THEORY_BAGS))
[ - + ]
1106 : : {
1107 : 0 : parseErrorLogic("Free sort symbols not allowed in ");
1108 : : }
1109 : 11431 : }
1110 : :
1111 : 41545 : void Smt2State::checkLogicAllowsFunctions()
1112 : : {
1113 [ + + ][ - + ]: 41545 : if (!d_logic.isTheoryEnabled(internal::theory::THEORY_UF) && !isHoEnabled())
[ - + ]
1114 : : {
1115 : 0 : parseError(
1116 : : "Functions (of non-zero arity) cannot "
1117 : : "be declared in logic "
1118 : 0 : + d_logic.getLogicString()
1119 : 0 : + ". Try including UF or adding the prefix HO_.");
1120 : : }
1121 : 41545 : }
1122 : :
1123 : 1242150 : bool Smt2State::isAbstractValue(const std::string& name)
1124 : : {
1125 [ + + ][ + - ]: 2411300 : return name.length() >= 2 && name[0] == '@' && name[1] != '0'
1126 [ + + ][ - + ]: 2411300 : && name.find_first_not_of("0123456789", 1) == std::string::npos;
1127 : : }
1128 : :
1129 : 839682 : Term Smt2State::mkRealOrIntFromNumeral(const std::string& str)
1130 : : {
1131 : : // if arithmetic is enabled, and integers are disabled
1132 : 839682 : if (d_logic.isTheoryEnabled(internal::theory::THEORY_ARITH)
1133 [ + + ][ + + ]: 839682 : && !d_logic.areIntegersUsed())
[ + + ]
1134 : : {
1135 : 77604 : return d_tm.mkReal(str);
1136 : : }
1137 : 762078 : return d_tm.mkInteger(str);
1138 : : }
1139 : :
1140 : 2051 : void Smt2State::parseOpApplyTypeAscription(ParseOp& p, Sort type)
1141 : : {
1142 [ + - ]: 4102 : Trace("parser") << "parseOpApplyTypeAscription : " << p << " " << type
1143 : 2051 : << std::endl;
1144 [ + - ]: 2051 : if (p.d_expr.isNull())
1145 : : {
1146 [ + - ]: 4102 : Trace("parser-overloading")
1147 : 0 : << "Getting variable expression with name " << p.d_name << " and type "
1148 : 2051 : << type << std::endl;
1149 : : // get the variable expression for the type
1150 [ + + ]: 2051 : if (isDeclared(p.d_name, SYM_VARIABLE))
1151 : : {
1152 : 1267 : p.d_expr = getExpressionForNameAndType(p.d_name, type);
1153 : 1267 : p.d_name = std::string("");
1154 : : }
1155 [ + + ]: 2051 : if (p.d_name == "const")
1156 : : {
1157 : : // We use a placeholder as a way to store the type of the constant array.
1158 : : // Since ParseOp only contains a Term field, it is stored as a constant
1159 : : // of the given type. The kind INTERNAL_KIND is used to mark that we
1160 : : // are a placeholder.
1161 : 221 : p.d_kind = Kind::INTERNAL_KIND;
1162 : 221 : p.d_expr = d_tm.mkConst(type, "_placeholder_");
1163 : 221 : return;
1164 : : }
1165 [ + + ]: 1830 : else if (p.d_name.find("ff") == 0)
1166 : : {
1167 : 563 : std::string rest = p.d_name.substr(2);
1168 [ - + ]: 563 : if (!type.isFiniteField())
1169 : : {
1170 : 0 : std::stringstream ss;
1171 : 0 : ss << "expected finite field sort to ascribe " << p.d_name
1172 : 0 : << " but found sort: " << type;
1173 : 0 : parseError(ss.str());
1174 : : }
1175 : 563 : p.d_expr = d_tm.mkFiniteFieldElem(rest, type);
1176 : 563 : return;
1177 : : }
1178 [ - + ]: 1267 : if (p.d_expr.isNull())
1179 : : {
1180 : 0 : std::stringstream ss;
1181 : 0 : ss << "Could not resolve expression with name " << p.d_name
1182 : 0 : << " and type " << type << std::endl;
1183 : 0 : parseError(ss.str());
1184 : : }
1185 : : }
1186 [ + - ]: 1267 : Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr;
1187 [ + - ][ - + ]: 1267 : Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getSort();
[ - - ]
1188 [ + - ]: 1267 : Trace("parser-qid") << std::endl;
1189 : : // otherwise, we process the type ascription
1190 : 1267 : p.d_expr = applyTypeAscription(p.d_expr, type);
1191 : : }
1192 : :
1193 : 0 : Term Smt2State::parseOpToExpr(ParseOp& p)
1194 : : {
1195 [ - - ]: 0 : Trace("parser") << "parseOpToExpr: " << p << std::endl;
1196 : 0 : Term expr;
1197 [ - - ]: 0 : if (p.d_kind != Kind::NULL_TERM)
1198 : : {
1199 : 0 : parseError(
1200 : : "Bad syntax for qualified identifier operator in term position.");
1201 : : }
1202 [ - - ]: 0 : else if (!p.d_expr.isNull())
1203 : : {
1204 : 0 : expr = p.d_expr;
1205 : : }
1206 : : else
1207 : : {
1208 : 0 : checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE);
1209 : 0 : expr = getVariable(p.d_name);
1210 : : }
1211 : 0 : Assert(!expr.isNull());
1212 : 0 : return expr;
1213 : : }
1214 : :
1215 : 6157670 : Term Smt2State::applyParseOp(const ParseOp& p, std::vector<Term>& args)
1216 : : {
1217 : 6157670 : bool isBuiltinOperator = false;
1218 : : // the builtin kind of the overall return expression
1219 : 6157670 : Kind kind = Kind::NULL_TERM;
1220 : : // First phase: process the operator
1221 [ - + ]: 6157670 : if (TraceIsOn("parser"))
1222 : : {
1223 [ - - ]: 0 : Trace("parser") << "applyParseOp: " << p << " to:" << std::endl;
1224 [ - - ]: 0 : for (std::vector<Term>::iterator i = args.begin(); i != args.end(); ++i)
1225 : : {
1226 [ - - ]: 0 : Trace("parser") << "++ " << *i << std::endl;
1227 : : }
1228 : : }
1229 [ + + ]: 6157670 : if (p.d_kind == Kind::NULLABLE_LIFT)
1230 : : {
1231 : 12 : auto it = d_operatorKindMap.find(p.d_name);
1232 [ + + ]: 12 : if (it == d_operatorKindMap.end())
1233 : : {
1234 : : // the lifted symbol is not a defined kind. So we construct a normal
1235 : : // term.
1236 : : // Input : ((_ nullable.lift f) x y)
1237 : : // output: (nullable.lift f x y)
1238 : 9 : ParserState::checkDeclaration(p.d_name, DeclarationCheck::CHECK_DECLARED);
1239 : 18 : Term function = getVariable(p.d_name);
1240 : 9 : args.insert(args.begin(), function);
1241 : 9 : return d_tm.mkTerm(Kind::NULLABLE_LIFT, args);
1242 : : }
1243 : : else
1244 : : {
1245 : 3 : Kind liftedKind = getOperatorKind(p.d_name);
1246 : 3 : return d_tm.mkNullableLift(liftedKind, args);
1247 : : }
1248 : : }
1249 [ + + ]: 6157660 : if (!p.d_indices.empty())
1250 : : {
1251 : 344156 : Op op;
1252 : 172078 : Kind k = getIndexedOpKind(p.d_name);
1253 [ + + ]: 172078 : if (k == Kind::UNDEFINED_KIND)
1254 : : {
1255 : : // Resolve indexed symbols that cannot be resolved without knowing the
1256 : : // type of the arguments. This is currently limited to `to_fp`,
1257 : : // `tuple.select`, and `tuple.update`.
1258 : 1263 : size_t nchildren = args.size();
1259 [ + + ]: 1263 : if (p.d_name == "to_fp")
1260 : : {
1261 [ + + ]: 272 : if (nchildren == 1)
1262 : : {
1263 : 107 : kind = Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV;
1264 : 107 : op = d_tm.mkOp(kind, p.d_indices);
1265 : : }
1266 [ + - ][ + + ]: 165 : else if (nchildren > 2 || nchildren == 0)
1267 : : {
1268 : 2 : std::stringstream ss;
1269 : : ss << "Wrong number of arguments for indexed operator to_fp, "
1270 : : "expected "
1271 : 1 : "1 or 2, got "
1272 : 1 : << nchildren;
1273 : 2 : parseError(ss.str());
1274 : : }
1275 [ - + ]: 164 : else if (!args[0].getSort().isRoundingMode())
1276 : : {
1277 : 0 : std::stringstream ss;
1278 : 0 : ss << "Expected a rounding mode as the first argument, got "
1279 : 0 : << args[0].getSort();
1280 : 0 : parseError(ss.str());
1281 : : }
1282 : : else
1283 : : {
1284 : 328 : Sort t = args[1].getSort();
1285 : :
1286 [ + + ]: 164 : if (t.isFloatingPoint())
1287 : : {
1288 : 16 : kind = Kind::FLOATINGPOINT_TO_FP_FROM_FP;
1289 : 16 : op = d_tm.mkOp(kind, p.d_indices);
1290 : : }
1291 [ + - ][ + + ]: 148 : else if (t.isInteger() || t.isReal())
[ + + ]
1292 : : {
1293 : 101 : kind = Kind::FLOATINGPOINT_TO_FP_FROM_REAL;
1294 : 101 : op = d_tm.mkOp(kind, p.d_indices);
1295 : : }
1296 : : else
1297 : : {
1298 : 47 : kind = Kind::FLOATINGPOINT_TO_FP_FROM_SBV;
1299 : 47 : op = d_tm.mkOp(kind, p.d_indices);
1300 : : }
1301 : : }
1302 : : }
1303 [ + + ][ + - ]: 991 : else if (p.d_name == "tuple.select" || p.d_name == "tuple.update")
[ + - ]
1304 : : {
1305 : 991 : bool isSelect = (p.d_name == "tuple.select");
1306 [ - + ]: 991 : if (p.d_indices.size() != 1)
1307 : : {
1308 : 0 : parseError("wrong number of indices for tuple select or update");
1309 : : }
1310 : 991 : uint64_t n = p.d_indices[0];
1311 [ + + ][ - + ]: 991 : if (args.size() != (isSelect ? 1 : 2))
1312 : : {
1313 : 0 : parseError("wrong number of arguments for tuple select or update");
1314 : : }
1315 : 1982 : Sort t = args[0].getSort();
1316 [ - + ]: 991 : if (!t.isTuple())
1317 : : {
1318 : 0 : parseError("tuple select or update applied to non-tuple");
1319 : : }
1320 : 991 : size_t length = t.getTupleLength();
1321 [ - + ]: 991 : if (n >= length)
1322 : : {
1323 : 0 : std::stringstream ss;
1324 : 0 : ss << "tuple is of length " << length << "; cannot access index "
1325 : 0 : << n;
1326 : 0 : parseError(ss.str());
1327 : : }
1328 : 1982 : const Datatype& dt = t.getDatatype();
1329 : 1982 : Term ret;
1330 [ + + ]: 991 : if (isSelect)
1331 : : {
1332 : : ret =
1333 [ + + ][ - - ]: 2853 : d_tm.mkTerm(Kind::APPLY_SELECTOR, {dt[0][n].getTerm(), args[0]});
1334 : : }
1335 : : else
1336 : : {
1337 [ + + ][ - - ]: 280 : ret = d_tm.mkTerm(Kind::APPLY_UPDATER,
1338 : 240 : {dt[0][n].getUpdaterTerm(), args[0], args[1]});
1339 : : }
1340 [ + - ]: 1982 : Trace("parser") << "applyParseOp: return selector/updater " << ret
1341 : 991 : << std::endl;
1342 : 991 : return ret;
1343 : : }
1344 : : else
1345 : : {
1346 : 0 : DebugUnhandled() << "Failed to resolve indexed operator " << p.d_name;
1347 : : }
1348 : : }
1349 : : else
1350 : : {
1351 : : // otherwise, an ordinary operator
1352 : 170815 : op = d_tm.mkOp(k, p.d_indices);
1353 : : }
1354 : 171083 : return d_tm.mkTerm(op, args);
1355 : : }
1356 [ + + ]: 5985580 : else if (p.d_kind != Kind::NULL_TERM)
1357 : : {
1358 : : // It is a special case, e.g. tuple.select or array constant specification.
1359 : : // We have to wait until the arguments are parsed to resolve it.
1360 : : }
1361 [ + + ]: 5970890 : else if (!p.d_expr.isNull())
1362 : : {
1363 : : // An explicit operator, e.g. an apply function
1364 : 27 : Kind fkind = getKindForFunction(p.d_expr);
1365 [ + - ]: 27 : if (fkind != Kind::UNDEFINED_KIND)
1366 : : {
1367 : : // Some operators may require a specific kind.
1368 : : // Testers are handled differently than other indexed operators,
1369 : : // since they require a kind.
1370 : 27 : kind = fkind;
1371 [ + - ]: 54 : Trace("parser") << "Got function kind " << kind << " for expression "
1372 : 27 : << std::endl;
1373 : : }
1374 : 27 : args.insert(args.begin(), p.d_expr);
1375 : : }
1376 : : else
1377 : : {
1378 : 5970860 : isBuiltinOperator = isOperatorEnabled(p.d_name);
1379 [ + + ]: 5970860 : if (isBuiltinOperator)
1380 : : {
1381 : : // a builtin operator, convert to kind
1382 : 5176160 : kind = getOperatorKind(p.d_name);
1383 : : // special case: indexed operators with zero arguments
1384 [ + + ][ + + ]: 5176160 : if (kind == Kind::TUPLE_PROJECT || kind == Kind::TABLE_PROJECT
1385 [ + - ][ + - ]: 5176150 : || kind == Kind::TABLE_AGGREGATE || kind == Kind::TABLE_JOIN
1386 [ + + ][ + + ]: 5176150 : || kind == Kind::TABLE_GROUP || kind == Kind::RELATION_GROUP
1387 [ + - ][ + + ]: 5176140 : || kind == Kind::RELATION_AGGREGATE || kind == Kind::RELATION_PROJECT
1388 [ - + ]: 5176120 : || kind == Kind::RELATION_TABLE_JOIN)
1389 : : {
1390 : 76 : std::vector<uint32_t> indices;
1391 : 76 : Op op = d_tm.mkOp(kind, indices);
1392 : 38 : return d_tm.mkTerm(op, args);
1393 : : }
1394 [ + + ]: 5176120 : else if (kind == Kind::APPLY_CONSTRUCTOR)
1395 : : {
1396 [ + + ]: 5558 : if (p.d_name == "tuple")
1397 : : {
1398 : : // tuple application
1399 : 5381 : return d_tm.mkTuple(args);
1400 : : }
1401 [ + - ]: 177 : else if (p.d_name == "nullable.some")
1402 : : {
1403 [ + + ]: 177 : if (args.size() == 1)
1404 : : {
1405 : 176 : return d_tm.mkNullableSome(args[0]);
1406 : : }
1407 : 3 : parseError("nullable.some requires exactly one argument.");
1408 : : }
1409 : : else
1410 : : {
1411 : 0 : std::stringstream ss;
1412 : 0 : ss << "Unknown APPLY_CONSTRUCTOR symbol '" << p.d_name << "'";
1413 : 0 : parseError(ss.str());
1414 : : }
1415 : : }
1416 [ + + ]: 5170560 : else if (kind == Kind::APPLY_SELECTOR)
1417 : : {
1418 [ + - ]: 63 : if (p.d_name == "nullable.val")
1419 : : {
1420 [ + - ]: 63 : if (args.size() == 1)
1421 : : {
1422 : 63 : return d_tm.mkNullableVal(args[0]);
1423 : : }
1424 : 0 : parseError("nullable.val requires exactly one argument.");
1425 : : }
1426 : : else
1427 : : {
1428 : 0 : std::stringstream ss;
1429 : 0 : ss << "Unknown APPLY_SELECTOR symbol '" << p.d_name << "'";
1430 : 0 : parseError(ss.str());
1431 : : }
1432 : : }
1433 [ + + ]: 5170500 : else if (kind == Kind::APPLY_TESTER)
1434 : : {
1435 [ + + ]: 67 : if (p.d_name == "nullable.is_null")
1436 : : {
1437 [ + - ]: 53 : if (args.size() == 1)
1438 : : {
1439 : 53 : return d_tm.mkNullableIsNull(args[0]);
1440 : : }
1441 : 0 : parseError("nullable.is_null requires exactly one argument.");
1442 : : }
1443 [ + - ]: 14 : else if (p.d_name == "nullable.is_some")
1444 : : {
1445 [ + - ]: 14 : if (args.size() == 1)
1446 : : {
1447 : 14 : return d_tm.mkNullableIsSome(args[0]);
1448 : : }
1449 : 0 : parseError("nullable.is_some requires exactly one argument.");
1450 : : }
1451 : : else
1452 : : {
1453 : 0 : std::stringstream ss;
1454 : 0 : ss << "Unknown APPLY_TESTER symbol '" << p.d_name << "'";
1455 : 0 : parseError(ss.str());
1456 : : }
1457 : : }
1458 [ + - ]: 10340900 : Trace("parser") << "Got builtin kind " << kind << " for name"
1459 : 5170430 : << std::endl;
1460 : : }
1461 : : else
1462 : : {
1463 : : // A non-built-in function application, get the expression
1464 : 794726 : checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE);
1465 : 1589370 : Term v = getVariable(p.d_name);
1466 [ + + ]: 794687 : if (!v.isNull())
1467 : : {
1468 : 793852 : checkFunctionLike(v);
1469 : 793850 : kind = getKindForFunction(v);
1470 : 793850 : args.insert(args.begin(), v);
1471 : : }
1472 : : else
1473 : : {
1474 : : // Overloaded symbol?
1475 : : // Could not find the expression. It may be an overloaded symbol,
1476 : : // in which case we may find it after knowing the types of its
1477 : : // arguments.
1478 : 1672 : std::vector<Sort> argTypes;
1479 [ + + ]: 2152 : for (std::vector<Term>::iterator i = args.begin(); i != args.end(); ++i)
1480 : : {
1481 : 1316 : argTypes.push_back((*i).getSort());
1482 : : }
1483 : 1672 : Term fop = getOverloadedFunctionForTypes(p.d_name, argTypes);
1484 [ + - ]: 836 : if (!fop.isNull())
1485 : : {
1486 : 836 : checkFunctionLike(fop);
1487 : 836 : kind = getKindForFunction(fop);
1488 : 836 : args.insert(args.begin(), fop);
1489 : : }
1490 : : else
1491 : : {
1492 : 0 : parseError(
1493 : : "Cannot find unambiguous overloaded function for argument "
1494 : : "types.");
1495 : : }
1496 : : }
1497 : : }
1498 : : }
1499 : : // handle special cases
1500 : : // If we marked the operator as "INTERNAL_KIND", then the name/expr
1501 : : // determine the operator. This handles constant arrays.
1502 [ + + ]: 5979840 : if (p.d_kind == Kind::INTERNAL_KIND)
1503 : : {
1504 : : // (as const (Array T1 T2))
1505 [ + - ]: 440 : if (!strictModeEnabled() && p.d_name == "const"
1506 [ + - ][ + - ]: 440 : && isTheoryEnabled(internal::theory::THEORY_ARRAYS))
[ + - ]
1507 : : {
1508 [ - + ]: 220 : if (args.size() != 1)
1509 : : {
1510 : 0 : parseError("Too many arguments to array constant.");
1511 : : }
1512 : 440 : Term constVal = args[0];
1513 : :
1514 [ - + ][ - + ]: 220 : Assert(!p.d_expr.isNull());
[ - - ]
1515 : 440 : Sort sort = p.d_expr.getSort();
1516 [ - + ]: 220 : if (!sort.isArray())
1517 : : {
1518 : 0 : std::stringstream ss;
1519 : 0 : ss << "expected array constant term, but cast is not of array type"
1520 : 0 : << std::endl
1521 : 0 : << "cast type: " << sort;
1522 : 0 : parseError(ss.str());
1523 : : }
1524 [ - + ]: 220 : if (sort.getArrayElementSort() != constVal.getSort())
1525 : : {
1526 : 0 : std::stringstream ss;
1527 : 0 : ss << "type mismatch inside array constant term:" << std::endl
1528 : 0 : << "array type: " << sort << std::endl
1529 : 0 : << "expected const type: " << sort.getArrayElementSort() << std::endl
1530 : 0 : << "computed const type: " << constVal.getSort();
1531 : 0 : parseError(ss.str());
1532 : : }
1533 : 440 : Term ret = d_tm.mkConstArray(sort, constVal);
1534 [ + - ]: 220 : Trace("parser") << "applyParseOp: return store all " << ret << std::endl;
1535 : 220 : return ret;
1536 : : }
1537 : : else
1538 : : {
1539 : : // should never happen
1540 : 0 : parseError("Could not process internal parsed operator");
1541 : : }
1542 : : }
1543 [ + + ][ + + ]: 5979620 : else if (p.d_kind == Kind::APPLY_TESTER || p.d_kind == Kind::APPLY_UPDATER)
1544 : : {
1545 : 13331 : Term iop = mkIndexedOp(p.d_kind, {p.d_name}, args);
1546 : 4442 : kind = p.d_kind;
1547 : 4442 : args.insert(args.begin(), iop);
1548 : : }
1549 [ + + ]: 5975180 : else if (p.d_kind != Kind::NULL_TERM)
1550 : : {
1551 : : // it should not have an expression or type specified at this point
1552 [ - + ]: 10033 : if (!p.d_expr.isNull())
1553 : : {
1554 : 0 : std::stringstream ss;
1555 : 0 : ss << "Could not process parsed qualified identifier kind " << p.d_kind;
1556 : 0 : parseError(ss.str());
1557 : : }
1558 : : // otherwise it is a simple application
1559 : 10033 : kind = p.d_kind;
1560 : : }
1561 [ + + ]: 5965150 : else if (isBuiltinOperator)
1562 : : {
1563 [ + + ][ + + ]: 5170430 : if (kind == Kind::EQUAL || kind == Kind::DISTINCT)
1564 : : {
1565 : 582138 : bool isReal = false;
1566 : : // need hol if these operators are applied over function args
1567 [ + + ]: 1758480 : for (const Term& i : args)
1568 : : {
1569 : 2352690 : Sort s = i.getSort();
1570 [ + + ]: 1176340 : if (!isHoEnabled())
1571 : : {
1572 [ - + ]: 1137130 : if (s.isFunction())
1573 : : {
1574 : 0 : parseError(
1575 : : "Cannot apply equality to functions unless logic is prefixed "
1576 : : "by HO_.");
1577 : : }
1578 : : }
1579 [ + + ]: 1176340 : if (s.isReal())
1580 : : {
1581 : 110670 : isReal = true;
1582 : : }
1583 : : }
1584 : : // If strict mode is not enabled, we are permissive for Int and Real
1585 : : // subtyping. Note that other arithmetic operators and relations are
1586 : : // already permissive, e.g. <=, +.
1587 [ + + ][ + + ]: 582138 : if (isReal && !strictModeEnabled())
[ + + ]
1588 : : {
1589 [ + + ]: 166072 : for (Term& i : args)
1590 : : {
1591 : 221482 : Sort s = i.getSort();
1592 [ + + ]: 110741 : if (s.isInteger())
1593 : : {
1594 : 160 : i = d_tm.mkTerm(Kind::TO_REAL, {i});
1595 : : }
1596 : : }
1597 : : }
1598 : : }
1599 [ + + ]: 5170430 : if (strictModeEnabled())
1600 : : {
1601 : : // Catch cases of mixed arithmetic, which our internal type checker is
1602 : : // lenient for. In particular, any case that is ill-typed according to
1603 : : // the SMT standard but not in our internal type checker are handled
1604 : : // here.
1605 : 480 : Sort sreq; // if applicable, the sort which all arguments must be.
1606 : 240 : bool sameType = false;
1607 [ + + ][ + - ]: 240 : if (kind == Kind::ADD || kind == Kind::MULT || kind == Kind::SUB
[ + - ]
1608 [ + - ][ + - ]: 239 : || kind == Kind::GEQ || kind == Kind::GT || kind == Kind::LEQ
[ + - ]
1609 [ - + ]: 239 : || kind == Kind::LT)
1610 : : {
1611 : : // no mixed arithmetic
1612 : 1 : sreq = args[0].getSort();
1613 : 1 : sameType = true;
1614 : : }
1615 [ + - ]: 239 : else if (kind == Kind::DIVISION
1616 [ + - ][ - + ]: 239 : || kind == Kind::TO_INTEGER || kind == Kind::IS_INTEGER)
1617 : : {
1618 : : // must apply division, to_int, is_int to real only
1619 : 0 : sreq = d_tm.getRealSort();
1620 : : }
1621 [ + + ][ - + ]: 239 : else if (kind == Kind::TO_REAL || kind == Kind::ABS)
1622 : : {
1623 : : // must apply to_real, abs to integer only
1624 : 1 : sreq = d_tm.getIntegerSort();
1625 : : }
1626 [ + + ]: 240 : if (!sreq.isNull())
1627 : : {
1628 [ + - ]: 3 : for (Term& i : args)
1629 : : {
1630 : 6 : Sort s = i.getSort();
1631 [ + + ]: 3 : if (s != sreq)
1632 : : {
1633 : 4 : std::stringstream ss;
1634 : 2 : ss << "Due to strict parsing, we require the arguments of " << kind;
1635 [ + + ]: 2 : if (sameType)
1636 : : {
1637 : 1 : ss << " to have the same type";
1638 : : }
1639 : : else
1640 : : {
1641 : 1 : ss << " to have type " << sreq;
1642 : : }
1643 : 4 : parseError(ss.str());
1644 : : }
1645 : : }
1646 : : }
1647 : : }
1648 [ + + ][ + + ]: 10340600 : if (!strictModeEnabled() && (kind == Kind::AND || kind == Kind::OR)
1649 [ + + ][ + + ]: 10340600 : && args.size() == 1)
[ + + ]
1650 : : {
1651 : : // Unary AND/OR can be replaced with the argument.
1652 [ + - ]: 1133 : Trace("parser") << "applyParseOp: return unary " << args[0] << std::endl;
1653 : 1133 : return args[0];
1654 : : }
1655 [ + + ][ + + ]: 5169300 : else if (kind == Kind::SUB && args.size() == 1)
[ + + ]
1656 : : {
1657 : 1035980 : Term ret = d_tm.mkTerm(Kind::NEG, {args[0]});
1658 [ + - ]: 258994 : Trace("parser") << "applyParseOp: return uminus " << ret << std::endl;
1659 : 258994 : return ret;
1660 : : }
1661 [ + + ]: 4910300 : else if (kind == Kind::FLOATINGPOINT_FP)
1662 : : {
1663 : : // (fp #bX #bY #bZ) denotes a floating-point value
1664 [ + + ]: 176 : if (args.size() != 3)
1665 : : {
1666 : 1 : parseError("expected 3 arguments to 'fp', got "
1667 : 4 : + std::to_string(args.size()));
1668 : : }
1669 [ + + ][ + - ]: 175 : if (isConstBv(args[0]) && isConstBv(args[1]) && isConstBv(args[2]))
[ + + ][ + + ]
1670 : : {
1671 : 325 : Term ret = d_tm.mkFloatingPoint(args[0], args[1], args[2]);
1672 [ + - ]: 324 : Trace("parser") << "applyParseOp: return floating-point value " << ret
1673 : 162 : << std::endl;
1674 : 162 : return ret;
1675 : : }
1676 : : }
1677 [ + + ]: 4910130 : else if (kind == Kind::SKOLEM)
1678 : : {
1679 : 62 : Term ret;
1680 : 31 : SkolemId skolemId = d_skolemMap[p.d_name];
1681 : 31 : size_t numSkolemIndices = d_tm.getNumIndicesForSkolemId(skolemId);
1682 [ + + ]: 31 : if (numSkolemIndices == args.size())
1683 : : {
1684 : 20 : ret = d_tm.mkSkolem(skolemId, args);
1685 : : }
1686 : : else
1687 : : {
1688 : : std::vector<Term> skolemArgs(args.begin(),
1689 : 22 : args.begin() + numSkolemIndices);
1690 : 22 : Term skolem = d_tm.mkSkolem(skolemId, skolemArgs);
1691 : 33 : std::vector<Term> finalArgs = {skolem};
1692 : : finalArgs.insert(
1693 : 11 : finalArgs.end(), args.begin() + numSkolemIndices, args.end());
1694 : 11 : ret = d_tm.mkTerm(Kind::APPLY_UF, finalArgs);
1695 : : }
1696 [ + - ]: 31 : Trace("parser") << "applyParseOp: return skolem " << ret << std::endl;
1697 : 31 : return ret;
1698 : : }
1699 : 9820210 : Term ret = d_tm.mkTerm(kind, args);
1700 [ + - ]: 9820200 : Trace("parser") << "applyParseOp: return default builtin " << ret
1701 : 4910100 : << std::endl;
1702 : 4910100 : return ret;
1703 : : }
1704 : :
1705 [ + + ]: 809188 : if (args.size() >= 2)
1706 : : {
1707 : : // may be partially applied function, in this case we use HO_APPLY
1708 : 800289 : Sort argt = args[0].getSort();
1709 [ + + ]: 800289 : if (argt.isFunction())
1710 : : {
1711 : 754799 : unsigned arity = argt.getFunctionArity();
1712 [ + + ]: 754799 : if (args.size() - 1 < arity)
1713 : : {
1714 [ - + ]: 791 : if (!isHoEnabled())
1715 : : {
1716 : 0 : parseError(
1717 : : "Cannot partially apply functions unless logic is prefixed by "
1718 : : "HO_.");
1719 : : }
1720 [ + - ]: 791 : Trace("parser") << "Partial application of " << args[0];
1721 [ + - ]: 791 : Trace("parser") << " : #argTypes = " << arity;
1722 [ + - ]: 791 : Trace("parser") << ", #args = " << args.size() - 1 << std::endl;
1723 : 1582 : Term ret = d_tm.mkTerm(Kind::HO_APPLY, args);
1724 [ + - ]: 1582 : Trace("parser") << "applyParseOp: return curry higher order " << ret
1725 : 791 : << std::endl;
1726 : : // must curry the partial application
1727 : 791 : return ret;
1728 : : }
1729 : : }
1730 : : }
1731 [ - + ]: 808397 : if (kind == Kind::NULL_TERM)
1732 : : {
1733 : : // should never happen in the new API
1734 : 0 : parseError("do not know how to process parse op");
1735 : : }
1736 [ + - ]: 1616790 : Trace("parser") << "Try default term construction for kind " << kind
1737 : 808397 : << " #args = " << args.size() << "..." << std::endl;
1738 : 1616790 : Term ret = d_tm.mkTerm(kind, args);
1739 [ + - ]: 808393 : Trace("parser") << "applyParseOp: return : " << ret << std::endl;
1740 : 808393 : return ret;
1741 : : }
1742 : :
1743 : 41317 : Sort Smt2State::getParametricSort(const std::string& name,
1744 : : const std::vector<Sort>& args)
1745 : : {
1746 [ - + ]: 41317 : if (args.empty())
1747 : : {
1748 : 0 : parseError(
1749 : : "Extra parentheses around sort name not "
1750 : : "permitted in SMT-LIB");
1751 : : }
1752 : : // builtin parametric sorts are handled manually
1753 : 41317 : Sort t;
1754 [ + + ][ + + ]: 41317 : if (name == "Array" && isTheoryEnabled(internal::theory::THEORY_ARRAYS))
[ + + ]
1755 : : {
1756 [ - + ]: 7038 : if (args.size() != 2)
1757 : : {
1758 : 0 : parseError("Illegal array type.");
1759 : : }
1760 : 7038 : t = d_tm.mkArraySort(args[0], args[1]);
1761 : : }
1762 [ + + ][ + + ]: 34279 : else if (name == "Set" && isTheoryEnabled(internal::theory::THEORY_SETS))
[ + + ]
1763 : : {
1764 [ - + ]: 3803 : if (args.size() != 1)
1765 : : {
1766 : 0 : parseError("Illegal set type.");
1767 : : }
1768 : 3803 : t = d_tm.mkSetSort(args[0]);
1769 : : }
1770 [ + + ][ + - ]: 30476 : else if (name == "Bag" && isTheoryEnabled(internal::theory::THEORY_BAGS))
[ + + ]
1771 : : {
1772 [ - + ]: 714 : if (args.size() != 1)
1773 : : {
1774 : 0 : parseError("Illegal bag type.");
1775 : : }
1776 : 714 : t = d_tm.mkBagSort(args[0]);
1777 : : }
1778 [ + - ]: 31097 : else if (name == "Seq" && !strictModeEnabled()
1779 [ + + ][ + - ]: 31097 : && isTheoryEnabled(internal::theory::THEORY_STRINGS))
[ + + ]
1780 : : {
1781 [ - + ]: 1335 : if (args.size() != 1)
1782 : : {
1783 : 0 : parseError("Illegal sequence type.");
1784 : : }
1785 : 1335 : t = d_tm.mkSequenceSort(args[0]);
1786 : : }
1787 [ + + ][ + - ]: 28427 : else if (name == "Tuple" && !strictModeEnabled())
[ + + ]
1788 : : {
1789 : 4161 : t = d_tm.mkTupleSort(args);
1790 : : }
1791 [ + + ][ + - ]: 24266 : else if (name == "Nullable" && !strictModeEnabled())
[ + + ]
1792 : : {
1793 [ - + ]: 718 : if (args.size() != 1)
1794 : : {
1795 : 0 : parseError("Illegal nullable type.");
1796 : : }
1797 : 718 : t = d_tm.mkNullableSort(args[0]);
1798 : : }
1799 [ + + ][ + - ]: 23548 : else if (name == "Relation" && !strictModeEnabled())
[ + + ]
1800 : : {
1801 : 1942 : Sort tupleSort = d_tm.mkTupleSort(args);
1802 : 1942 : t = d_tm.mkSetSort(tupleSort);
1803 : : }
1804 [ + + ][ + - ]: 21606 : else if (name == "Table" && !strictModeEnabled())
[ + + ]
1805 : : {
1806 : 182 : Sort tupleSort = d_tm.mkTupleSort(args);
1807 : 182 : t = d_tm.mkBagSort(tupleSort);
1808 : : }
1809 [ + + ][ + + ]: 21424 : else if (name == "->" && isHoEnabled())
[ + + ]
1810 : : {
1811 [ - + ]: 19841 : if (args.size() < 2)
1812 : : {
1813 : 0 : parseError("Arrow types must have at least 2 arguments");
1814 : : }
1815 : : // flatten the type
1816 : 39682 : Sort rangeType = args.back();
1817 : 19841 : std::vector<Sort> dargs(args.begin(), args.end() - 1);
1818 : 19841 : t = mkFlatFunctionType(dargs, rangeType);
1819 : : }
1820 : : else
1821 : : {
1822 : 1583 : t = ParserState::getParametricSort(name, args);
1823 : : }
1824 : 41314 : return t;
1825 : : }
1826 : :
1827 : 34268 : Sort Smt2State::getIndexedSort(const std::string& name,
1828 : : const std::vector<std::string>& numerals)
1829 : : {
1830 : 34268 : Sort ret;
1831 [ + + ]: 34268 : if (name == "BitVec")
1832 : : {
1833 [ - + ]: 32700 : if (numerals.size() != 1)
1834 : : {
1835 : 0 : parseError("Illegal bitvector type.");
1836 : : }
1837 : 32700 : uint32_t n0 = stringToUnsigned(numerals[0]);
1838 [ - + ]: 32700 : if (n0 == 0)
1839 : : {
1840 : 0 : parseError("Illegal bitvector size: 0");
1841 : : }
1842 : 32700 : ret = d_tm.mkBitVectorSort(n0);
1843 : : }
1844 [ + + ]: 1568 : else if (name == "FiniteField")
1845 : : {
1846 [ - + ]: 1084 : if (numerals.size() != 1)
1847 : : {
1848 : 0 : parseError("Illegal finite field type.");
1849 : : }
1850 : 1084 : ret = d_tm.mkFiniteFieldSort(numerals.front());
1851 : : }
1852 [ + - ]: 484 : else if (name == "FloatingPoint")
1853 : : {
1854 [ - + ]: 484 : if (numerals.size() != 2)
1855 : : {
1856 : 0 : parseError("Illegal floating-point type.");
1857 : : }
1858 : 484 : uint32_t n0 = stringToUnsigned(numerals[0]);
1859 : 484 : uint32_t n1 = stringToUnsigned(numerals[1]);
1860 [ - + ]: 484 : if (!internal::validExponentSize(n0))
1861 : : {
1862 : 0 : parseError("Illegal floating-point exponent size");
1863 : : }
1864 [ - + ]: 484 : if (!internal::validSignificandSize(n1))
1865 : : {
1866 : 0 : parseError("Illegal floating-point significand size");
1867 : : }
1868 : 484 : ret = d_tm.mkFloatingPointSort(n0, n1);
1869 : : }
1870 : : else
1871 : : {
1872 : 0 : std::stringstream ss;
1873 : 0 : ss << "unknown indexed sort symbol `" << name << "'";
1874 : 0 : parseError(ss.str());
1875 : : }
1876 : 34268 : return ret;
1877 : : }
1878 : :
1879 : 5970920 : bool Smt2State::isClosure(const std::string& name)
1880 : : {
1881 : 5970920 : return d_closureKindMap.find(name) != d_closureKindMap.end();
1882 : : }
1883 : :
1884 : 5681 : std::unique_ptr<Cmd> Smt2State::handlePush(std::optional<uint32_t> nscopes)
1885 : : {
1886 : 5681 : checkThatLogicIsSet();
1887 : :
1888 [ + + ]: 5681 : if (!nscopes)
1889 : : {
1890 [ - + ]: 453 : if (strictModeEnabled())
1891 : : {
1892 : 0 : parseError(
1893 : : "Strict compliance mode demands an integer to be provided to "
1894 : : "(push). Maybe you want (push 1)?");
1895 : : }
1896 : 453 : nscopes = 1;
1897 : : }
1898 : :
1899 [ + + ]: 11385 : for (uint32_t i = 0; i < *nscopes; i++)
1900 : : {
1901 : 5704 : pushScope(true);
1902 : : }
1903 : 5681 : return std::make_unique<PushCommand>(*nscopes);
1904 : : }
1905 : :
1906 : 4564 : std::unique_ptr<Cmd> Smt2State::handlePop(std::optional<uint32_t> nscopes)
1907 : : {
1908 : 4564 : checkThatLogicIsSet();
1909 : :
1910 [ + + ]: 4564 : if (!nscopes)
1911 : : {
1912 [ - + ]: 359 : if (strictModeEnabled())
1913 : : {
1914 : 0 : parseError(
1915 : : "Strict compliance mode demands an integer to be provided to "
1916 : : "(pop). Maybe you want (pop 1)?");
1917 : : }
1918 : 359 : nscopes = 1;
1919 : : }
1920 : :
1921 [ + + ]: 9275 : for (uint32_t i = 0; i < *nscopes; i++)
1922 : : {
1923 : 4711 : popScope();
1924 : : }
1925 : 4564 : return std::make_unique<PopCommand>(*nscopes);
1926 : : }
1927 : :
1928 : 11261 : void Smt2State::notifyNamedExpression(Term& expr, std::string name)
1929 : : {
1930 : 11261 : checkUserSymbol(name);
1931 : : // remember the expression name in the symbol manager
1932 : 11261 : NamingResult nr = getSymbolManager()->setExpressionName(expr, name, false);
1933 [ + + ]: 11261 : if (nr == NamingResult::ERROR_IN_BINDER)
1934 : : {
1935 : 3 : parseError(
1936 : : "Cannot name a term in a binder (e.g., quantifiers, definitions)");
1937 : : }
1938 : : // define the variable. This needs to be done here so that in the rest of the
1939 : : // command we can use this name, which is required by the semantics of :named.
1940 : : //
1941 : : // Note that as we are defining the name to the expression here, names never
1942 : : // show up in "-o raw-benchmark" nor in proofs. To be able to do it it'd be
1943 : : // necessary to not define this variable here and create a
1944 : : // DefineFunctionCommand with the binding, so that names are handled as
1945 : : // defined functions. However, these commands would need to be processed
1946 : : // *before* the rest of the command in which the :named attribute appears, so
1947 : : // the name can be defined in the rest of the command. This would greatly
1948 : : // complicate the design of the parser and provide little gain, so we opt to
1949 : : // handle :named as a macro processed directly in the parser.
1950 : 11260 : defineVar(name, expr);
1951 : : // set the last named term, which ensures that we catch when assertions are
1952 : : // named
1953 : 11260 : setLastNamedTerm(expr, name);
1954 : 11260 : }
1955 : :
1956 : 0 : Term Smt2State::mkAnd(const std::vector<Term>& es) const
1957 : : {
1958 [ - - ]: 0 : if (es.size() == 0)
1959 : : {
1960 : 0 : return d_tm.mkTrue();
1961 : : }
1962 [ - - ]: 0 : else if (es.size() == 1)
1963 : : {
1964 : 0 : return es[0];
1965 : : }
1966 : 0 : return d_tm.mkTerm(Kind::AND, es);
1967 : : }
1968 : :
1969 : 0 : bool Smt2State::isConstInt(const Term& t)
1970 : : {
1971 : 0 : return t.getKind() == Kind::CONST_INTEGER;
1972 : : }
1973 : :
1974 : 517 : bool Smt2State::isConstBv(const Term& t)
1975 : : {
1976 : 517 : return t.getKind() == Kind::CONST_BITVECTOR;
1977 : : }
1978 : :
1979 : : } // namespace parser
1980 : : } // namespace cvc5
|
