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