projects / cvc5.git / blob
? search:


291885278107d424b52d0999db8164b26d7fe12a
[cvc5.git] / src / parser / smt2 / smt2.cpp
1 /********************* */
2 /*! \file smt2.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Kshitij Bansal, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief Definitions of SMT2 constants.
13 **
14 ** Definitions of SMT2 constants.
15 **/
16 #include "parser/smt2/smt2.h"
17
18 #include <algorithm>
19
20 #include "base/check.h"
21 #include "expr/type.h"
22 #include "options/options.h"
23 #include "parser/antlr_input.h"
24 #include "parser/parser.h"
25 #include "parser/smt2/smt2_input.h"
26 #include "printer/sygus_print_callback.h"
27 #include "util/bitvector.h"
28
29 // ANTLR defines these, which is really bad!
30 #undef true
31 #undef false
32
33 namespace CVC4 {
34 namespace parser {
35
36 Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
37 : Parser(solver, input, strictMode, parseOnly),
38 d_logicSet(false),
39 d_seenSetLogic(false)
40 {
41 if (!strictModeEnabled())
42 {
43 addTheory(Smt2::THEORY_CORE);
44 }
45 }
46
47 void Smt2::addArithmeticOperators() {
48 addOperator(kind::PLUS, "+");
49 addOperator(kind::MINUS, "-");
50 // kind::MINUS is converted to kind::UMINUS if there is only a single operand
51 Parser::addOperator(kind::UMINUS);
52 addOperator(kind::MULT, "*");
53 addOperator(kind::LT, "<");
54 addOperator(kind::LEQ, "<=");
55 addOperator(kind::GT, ">");
56 addOperator(kind::GEQ, ">=");
57
58 if (!strictModeEnabled())
59 {
60 // NOTE: this operator is non-standard
61 addOperator(kind::POW, "^");
62 }
63 }
64
65 void Smt2::addTranscendentalOperators()
66 {
67 addOperator(kind::EXPONENTIAL, "exp");
68 addOperator(kind::SINE, "sin");
69 addOperator(kind::COSINE, "cos");
70 addOperator(kind::TANGENT, "tan");
71 addOperator(kind::COSECANT, "csc");
72 addOperator(kind::SECANT, "sec");
73 addOperator(kind::COTANGENT, "cot");
74 addOperator(kind::ARCSINE, "arcsin");
75 addOperator(kind::ARCCOSINE, "arccos");
76 addOperator(kind::ARCTANGENT, "arctan");
77 addOperator(kind::ARCCOSECANT, "arccsc");
78 addOperator(kind::ARCSECANT, "arcsec");
79 addOperator(kind::ARCCOTANGENT, "arccot");
80 addOperator(kind::SQRT, "sqrt");
81 }
82
83 void Smt2::addQuantifiersOperators()
84 {
85 if (!strictModeEnabled())
86 {
87 addOperator(kind::INST_CLOSURE, "inst-closure");
88 }
89 }
90
91 void Smt2::addBitvectorOperators() {
92 addOperator(kind::BITVECTOR_CONCAT, "concat");
93 addOperator(kind::BITVECTOR_NOT, "bvnot");
94 addOperator(kind::BITVECTOR_AND, "bvand");
95 addOperator(kind::BITVECTOR_OR, "bvor");
96 addOperator(kind::BITVECTOR_NEG, "bvneg");
97 addOperator(kind::BITVECTOR_PLUS, "bvadd");
98 addOperator(kind::BITVECTOR_MULT, "bvmul");
99 addOperator(kind::BITVECTOR_UDIV, "bvudiv");
100 addOperator(kind::BITVECTOR_UREM, "bvurem");
101 addOperator(kind::BITVECTOR_SHL, "bvshl");
102 addOperator(kind::BITVECTOR_LSHR, "bvlshr");
103 addOperator(kind::BITVECTOR_ULT, "bvult");
104 addOperator(kind::BITVECTOR_NAND, "bvnand");
105 addOperator(kind::BITVECTOR_NOR, "bvnor");
106 addOperator(kind::BITVECTOR_XOR, "bvxor");
107 addOperator(kind::BITVECTOR_XNOR, "bvxnor");
108 addOperator(kind::BITVECTOR_COMP, "bvcomp");
109 addOperator(kind::BITVECTOR_SUB, "bvsub");
110 addOperator(kind::BITVECTOR_SDIV, "bvsdiv");
111 addOperator(kind::BITVECTOR_SREM, "bvsrem");
112 addOperator(kind::BITVECTOR_SMOD, "bvsmod");
113 addOperator(kind::BITVECTOR_ASHR, "bvashr");
114 addOperator(kind::BITVECTOR_ULE, "bvule");
115 addOperator(kind::BITVECTOR_UGT, "bvugt");
116 addOperator(kind::BITVECTOR_UGE, "bvuge");
117 addOperator(kind::BITVECTOR_SLT, "bvslt");
118 addOperator(kind::BITVECTOR_SLE, "bvsle");
119 addOperator(kind::BITVECTOR_SGT, "bvsgt");
120 addOperator(kind::BITVECTOR_SGE, "bvsge");
121 addOperator(kind::BITVECTOR_REDOR, "bvredor");
122 addOperator(kind::BITVECTOR_REDAND, "bvredand");
123 addOperator(kind::BITVECTOR_TO_NAT, "bv2nat");
124
125 addIndexedOperator(
126 kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract");
127 addIndexedOperator(kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat");
128 addIndexedOperator(
129 kind::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend");
130 addIndexedOperator(
131 kind::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend");
132 addIndexedOperator(
133 kind::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left");
134 addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT,
135 api::BITVECTOR_ROTATE_RIGHT,
136 "rotate_right");
137 addIndexedOperator(kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv");
138 }
139
140 void Smt2::addDatatypesOperators()
141 {
142 Parser::addOperator(kind::APPLY_CONSTRUCTOR);
143 Parser::addOperator(kind::APPLY_TESTER);
144 Parser::addOperator(kind::APPLY_SELECTOR);
145 Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
146
147 if (!strictModeEnabled())
148 {
149 addOperator(kind::DT_SIZE, "dt.size");
150 }
151 }
152
153 void Smt2::addStringOperators() {
154 defineVar("re.all",
155 getSolver()
156 ->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())
157 .getExpr());
158
159 addOperator(kind::STRING_CONCAT, "str.++");
160 addOperator(kind::STRING_LENGTH, "str.len");
161 addOperator(kind::STRING_SUBSTR, "str.substr" );
162 addOperator(kind::STRING_STRCTN, "str.contains" );
163 addOperator(kind::STRING_CHARAT, "str.at" );
164 addOperator(kind::STRING_STRIDOF, "str.indexof" );
165 addOperator(kind::STRING_STRREPL, "str.replace" );
166 addOperator(kind::STRING_STRREPLALL, "str.replaceall");
167 if (!strictModeEnabled())
168 {
169 addOperator(kind::STRING_TOLOWER, "str.tolower");
170 addOperator(kind::STRING_TOUPPER, "str.toupper");
171 addOperator(kind::STRING_REV, "str.rev");
172 }
173 addOperator(kind::STRING_PREFIX, "str.prefixof" );
174 addOperator(kind::STRING_SUFFIX, "str.suffixof" );
175 // at the moment, we only use this syntax for smt2.6.1
176 if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
177 {
178 addOperator(kind::STRING_ITOS, "str.from-int");
179 addOperator(kind::STRING_STOI, "str.to-int");
180 addOperator(kind::STRING_IN_REGEXP, "str.in-re");
181 addOperator(kind::STRING_TO_REGEXP, "str.to-re");
182 }
183 else
184 {
185 addOperator(kind::STRING_ITOS, "int.to.str");
186 addOperator(kind::STRING_STOI, "str.to.int");
187 addOperator(kind::STRING_IN_REGEXP, "str.in.re");
188 addOperator(kind::STRING_TO_REGEXP, "str.to.re");
189 }
190
191 addOperator(kind::REGEXP_CONCAT, "re.++");
192 addOperator(kind::REGEXP_UNION, "re.union");
193 addOperator(kind::REGEXP_INTER, "re.inter");
194 addOperator(kind::REGEXP_STAR, "re.*");
195 addOperator(kind::REGEXP_PLUS, "re.+");
196 addOperator(kind::REGEXP_OPT, "re.opt");
197 addOperator(kind::REGEXP_RANGE, "re.range");
198 addOperator(kind::REGEXP_LOOP, "re.loop");
199 addOperator(kind::STRING_CODE, "str.code");
200 addOperator(kind::STRING_LT, "str.<");
201 addOperator(kind::STRING_LEQ, "str.<=");
202 }
203
204 void Smt2::addFloatingPointOperators() {
205 addOperator(kind::FLOATINGPOINT_FP, "fp");
206 addOperator(kind::FLOATINGPOINT_EQ, "fp.eq");
207 addOperator(kind::FLOATINGPOINT_ABS, "fp.abs");
208 addOperator(kind::FLOATINGPOINT_NEG, "fp.neg");
209 addOperator(kind::FLOATINGPOINT_PLUS, "fp.add");
210 addOperator(kind::FLOATINGPOINT_SUB, "fp.sub");
211 addOperator(kind::FLOATINGPOINT_MULT, "fp.mul");
212 addOperator(kind::FLOATINGPOINT_DIV, "fp.div");
213 addOperator(kind::FLOATINGPOINT_FMA, "fp.fma");
214 addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt");
215 addOperator(kind::FLOATINGPOINT_REM, "fp.rem");
216 addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral");
217 addOperator(kind::FLOATINGPOINT_MIN, "fp.min");
218 addOperator(kind::FLOATINGPOINT_MAX, "fp.max");
219 addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq");
220 addOperator(kind::FLOATINGPOINT_LT, "fp.lt");
221 addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq");
222 addOperator(kind::FLOATINGPOINT_GT, "fp.gt");
223 addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal");
224 addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal");
225 addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero");
226 addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite");
227 addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN");
228 addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative");
229 addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
230 addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
231
232 addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC,
233 api::FLOATINGPOINT_TO_FP_GENERIC,
234 "to_fp");
235 addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
236 api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
237 "to_fp_unsigned");
238 addIndexedOperator(
239 kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
240 addIndexedOperator(
241 kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv");
242
243 if (!strictModeEnabled())
244 {
245 addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
246 api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
247 "to_fp_bv");
248 addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
249 api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
250 "to_fp_fp");
251 addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL,
252 api::FLOATINGPOINT_TO_FP_REAL,
253 "to_fp_real");
254 addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
255 api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
256 "to_fp_signed");
257 }
258 }
259
260 void Smt2::addSepOperators() {
261 addOperator(kind::SEP_STAR, "sep");
262 addOperator(kind::SEP_PTO, "pto");
263 addOperator(kind::SEP_WAND, "wand");
264 addOperator(kind::SEP_EMP, "emp");
265 Parser::addOperator(kind::SEP_STAR);
266 Parser::addOperator(kind::SEP_PTO);
267 Parser::addOperator(kind::SEP_WAND);
268 Parser::addOperator(kind::SEP_EMP);
269 }
270
271 void Smt2::addTheory(Theory theory) {
272 switch(theory) {
273 case THEORY_ARRAYS:
274 addOperator(kind::SELECT, "select");
275 addOperator(kind::STORE, "store");
276 break;
277
278 case THEORY_BITVECTORS:
279 addBitvectorOperators();
280 break;
281
282 case THEORY_CORE:
283 defineType("Bool", getExprManager()->booleanType());
284 defineVar("true", getExprManager()->mkConst(true));
285 defineVar("false", getExprManager()->mkConst(false));
286 addOperator(kind::AND, "and");
287 addOperator(kind::DISTINCT, "distinct");
288 addOperator(kind::EQUAL, "=");
289 addOperator(kind::IMPLIES, "=>");
290 addOperator(kind::ITE, "ite");
291 addOperator(kind::NOT, "not");
292 addOperator(kind::OR, "or");
293 addOperator(kind::XOR, "xor");
294 break;
295
296 case THEORY_REALS_INTS:
297 defineType("Real", getExprManager()->realType());
298 addOperator(kind::DIVISION, "/");
299 addOperator(kind::TO_INTEGER, "to_int");
300 addOperator(kind::IS_INTEGER, "is_int");
301 addOperator(kind::TO_REAL, "to_real");
302 // falling through on purpose, to add Ints part of Reals_Ints
303 CVC4_FALLTHROUGH;
304 case THEORY_INTS:
305 defineType("Int", getExprManager()->integerType());
306 addArithmeticOperators();
307 addOperator(kind::INTS_DIVISION, "div");
308 addOperator(kind::INTS_MODULUS, "mod");
309 addOperator(kind::ABS, "abs");
310 addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE, "divisible");
311 break;
312
313 case THEORY_REALS:
314 defineType("Real", getExprManager()->realType());
315 addArithmeticOperators();
316 addOperator(kind::DIVISION, "/");
317 if (!strictModeEnabled())
318 {
319 addOperator(kind::ABS, "abs");
320 }
321 break;
322
323 case THEORY_TRANSCENDENTALS:
324 defineVar("real.pi",
325 getExprManager()->mkNullaryOperator(getExprManager()->realType(),
326 CVC4::kind::PI));
327 addTranscendentalOperators();
328 break;
329
330 case THEORY_QUANTIFIERS: addQuantifiersOperators(); break;
331
332 case THEORY_SETS:
333 defineVar("emptyset",
334 d_solver->mkEmptySet(d_solver->getNullSort()).getExpr());
335 // the Boolean sort is a placeholder here since we don't have type info
336 // without type annotation
337 defineVar("univset",
338 d_solver->mkUniverseSet(d_solver->getBooleanSort()).getExpr());
339
340 addOperator(kind::UNION, "union");
341 addOperator(kind::INTERSECTION, "intersection");
342 addOperator(kind::SETMINUS, "setminus");
343 addOperator(kind::SUBSET, "subset");
344 addOperator(kind::MEMBER, "member");
345 addOperator(kind::SINGLETON, "singleton");
346 addOperator(kind::INSERT, "insert");
347 addOperator(kind::CARD, "card");
348 addOperator(kind::COMPLEMENT, "complement");
349 addOperator(kind::JOIN, "join");
350 addOperator(kind::PRODUCT, "product");
351 addOperator(kind::TRANSPOSE, "transpose");
352 addOperator(kind::TCLOSURE, "tclosure");
353 break;
354
355 case THEORY_DATATYPES:
356 {
357 const std::vector<Type> types;
358 defineType("Tuple", getExprManager()->mkTupleType(types));
359 addDatatypesOperators();
360 break;
361 }
362
363 case THEORY_STRINGS:
364 defineType("String", getExprManager()->stringType());
365 defineType("RegLan", getExprManager()->regExpType());
366 defineType("Int", getExprManager()->integerType());
367
368 defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr());
369 defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr());
370
371 addStringOperators();
372 break;
373
374 case THEORY_UF:
375 Parser::addOperator(kind::APPLY_UF);
376
377 if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
378 {
379 addOperator(kind::CARDINALITY_CONSTRAINT, "fmf.card");
380 addOperator(kind::CARDINALITY_VALUE, "fmf.card.val");
381 }
382 break;
383
384 case THEORY_FP:
385 defineType("RoundingMode", getExprManager()->roundingModeType());
386 defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
387 defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
388 defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
389 defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
390
391 defineVar(
392 "RNE",
393 d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
394 defineVar(
395 "roundNearestTiesToEven",
396 d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
397 defineVar(
398 "RNA",
399 d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
400 defineVar(
401 "roundNearestTiesToAway",
402 d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
403 defineVar("RTP",
404 d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
405 defineVar("roundTowardPositive",
406 d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
407 defineVar("RTN",
408 d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
409 defineVar("roundTowardNegative",
410 d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
411 defineVar("RTZ",
412 d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
413 defineVar("roundTowardZero",
414 d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
415
416 addFloatingPointOperators();
417 break;
418
419 case THEORY_SEP:
420 // the Boolean sort is a placeholder here since we don't have type info
421 // without type annotation
422 defineVar("sep.nil",
423 d_solver->mkSepNil(d_solver->getBooleanSort()).getExpr());
424
425 addSepOperators();
426 break;
427
428 default:
429 std::stringstream ss;
430 ss << "internal error: unsupported theory " << theory;
431 throw ParserException(ss.str());
432 }
433 }
434
435 void Smt2::addOperator(Kind kind, const std::string& name) {
436 Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
437 << std::endl;
438 Parser::addOperator(kind);
439 operatorKindMap[name] = kind;
440 }
441
442 void Smt2::addIndexedOperator(Kind tKind,
443 api::Kind opKind,
444 const std::string& name)
445 {
446 Parser::addOperator(tKind);
447 d_indexedOpKindMap[name] = opKind;
448 }
449
450 Kind Smt2::getOperatorKind(const std::string& name) const {
451 // precondition: isOperatorEnabled(name)
452 return operatorKindMap.find(name)->second;
453 }
454
455 bool Smt2::isOperatorEnabled(const std::string& name) const {
456 return operatorKindMap.find(name) != operatorKindMap.end();
457 }
458
459 bool Smt2::isTheoryEnabled(Theory theory) const {
460 switch(theory) {
461 case THEORY_ARRAYS:
462 return d_logic.isTheoryEnabled(theory::THEORY_ARRAYS);
463 case THEORY_BITVECTORS:
464 return d_logic.isTheoryEnabled(theory::THEORY_BV);
465 case THEORY_CORE:
466 return true;
467 case THEORY_DATATYPES:
468 return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
469 case THEORY_INTS:
470 return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
471 d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
472 case THEORY_REALS:
473 return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
474 ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
475 case THEORY_REALS_INTS:
476 return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
477 d_logic.areIntegersUsed() && d_logic.areRealsUsed();
478 case THEORY_QUANTIFIERS:
479 return d_logic.isQuantified();
480 case THEORY_SETS:
481 return d_logic.isTheoryEnabled(theory::THEORY_SETS);
482 case THEORY_STRINGS:
483 return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
484 case THEORY_UF:
485 return d_logic.isTheoryEnabled(theory::THEORY_UF);
486 case THEORY_FP:
487 return d_logic.isTheoryEnabled(theory::THEORY_FP);
488 case THEORY_SEP:
489 return d_logic.isTheoryEnabled(theory::THEORY_SEP);
490 default:
491 std::stringstream ss;
492 ss << "internal error: unsupported theory " << theory;
493 throw ParserException(ss.str());
494 }
495 }
496
497 bool Smt2::logicIsSet() {
498 return d_logicSet;
499 }
500
501 Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
502 if (isAbstractValue(name))
503 {
504 return mkAbstractValue(name);
505 }
506 return Parser::getExpressionForNameAndType(name, t);
507 }
508
509 api::Term Smt2::mkIndexedConstant(const std::string& name,
510 const std::vector<uint64_t>& numerals)
511 {
512 if (isTheoryEnabled(THEORY_FP))
513 {
514 if (name == "+oo")
515 {
516 return d_solver->mkPosInf(numerals[0], numerals[1]);
517 }
518 else if (name == "-oo")
519 {
520 return d_solver->mkNegInf(numerals[0], numerals[1]);
521 }
522 else if (name == "NaN")
523 {
524 return d_solver->mkNaN(numerals[0], numerals[1]);
525 }
526 else if (name == "+zero")
527 {
528 return d_solver->mkPosZero(numerals[0], numerals[1]);
529 }
530 else if (name == "-zero")
531 {
532 return d_solver->mkNegZero(numerals[0], numerals[1]);
533 }
534 }
535
536 if (isTheoryEnabled(THEORY_BITVECTORS) && name.find("bv") == 0)
537 {
538 std::string bvStr = name.substr(2);
539 return d_solver->mkBitVector(numerals[0], bvStr, 10);
540 }
541
542 // NOTE: Theory parametric constants go here
543
544 parseError(std::string("Unknown indexed literal `") + name + "'");
545 return api::Term();
546 }
547
548 api::Op Smt2::mkIndexedOp(const std::string& name,
549 const std::vector<uint64_t>& numerals)
550 {
551 const auto& kIt = d_indexedOpKindMap.find(name);
552 if (kIt != d_indexedOpKindMap.end())
553 {
554 api::Kind k = (*kIt).second;
555 if (numerals.size() == 1)
556 {
557 return d_solver->mkOp(k, numerals[0]);
558 }
559 else if (numerals.size() == 2)
560 {
561 return d_solver->mkOp(k, numerals[0], numerals[1]);
562 }
563 }
564
565 parseError(std::string("Unknown indexed function `") + name + "'");
566 return api::Op();
567 }
568
569 Expr Smt2::mkDefineFunRec(
570 const std::string& fname,
571 const std::vector<std::pair<std::string, Type> >& sortedVarNames,
572 Type t,
573 std::vector<Expr>& flattenVars)
574 {
575 std::vector<Type> sorts;
576 for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
577 {
578 sorts.push_back(svn.second);
579 }
580
581 // make the flattened function type, add bound variables
582 // to flattenVars if the defined function was given a function return type.
583 Type ft = mkFlatFunctionType(sorts, t, flattenVars);
584
585 // allow overloading
586 return mkVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
587 }
588
589 void Smt2::pushDefineFunRecScope(
590 const std::vector<std::pair<std::string, Type> >& sortedVarNames,
591 Expr func,
592 const std::vector<Expr>& flattenVars,
593 std::vector<Expr>& bvs,
594 bool bindingLevel)
595 {
596 pushScope(bindingLevel);
597
598 // bound variables are those that are explicitly named in the preamble
599 // of the define-fun(s)-rec command, we define them here
600 for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
601 {
602 Expr v = mkBoundVar(svn.first, svn.second);
603 bvs.push_back(v);
604 }
605
606 bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end());
607 }
608
609 void Smt2::reset() {
610 d_logicSet = false;
611 d_seenSetLogic = false;
612 d_logic = LogicInfo();
613 operatorKindMap.clear();
614 d_lastNamedTerm = std::pair<Expr, std::string>();
615 this->Parser::reset();
616
617 if( !strictModeEnabled() ) {
618 addTheory(Smt2::THEORY_CORE);
619 }
620 }
621
622 void Smt2::resetAssertions() {
623 // Remove all declarations except the ones at level 0.
624 while (this->scopeLevel() > 0) {
625 this->popScope();
626 }
627 }
628
629 std::unique_ptr<Command> Smt2::assertRewriteRule(
630 Kind kind,
631 Expr bvl,
632 const std::vector<Expr>& triggers,
633 const std::vector<Expr>& guards,
634 const std::vector<Expr>& heads,
635 Expr body)
636 {
637 assert(kind == kind::RR_REWRITE || kind == kind::RR_REDUCTION
638 || kind == kind::RR_DEDUCTION);
639
640 ExprManager* em = getExprManager();
641
642 std::vector<Expr> args;
643 args.push_back(mkAnd(heads));
644 args.push_back(body);
645
646 if (!triggers.empty())
647 {
648 args.push_back(em->mkExpr(kind::INST_PATTERN_LIST, triggers));
649 }
650
651 Expr rhs = em->mkExpr(kind, args);
652 Expr rule = em->mkExpr(kind::REWRITE_RULE, bvl, mkAnd(guards), rhs);
653 return std::unique_ptr<Command>(new AssertCommand(rule, false));
654 }
655
656 Smt2::SynthFunFactory::SynthFunFactory(
657 Smt2* smt2,
658 const std::string& fun,
659 bool isInv,
660 Type range,
661 std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames)
662 : d_smt2(smt2), d_fun(fun), d_isInv(isInv)
663 {
664 if (range.isNull())
665 {
666 smt2->parseError("Must supply return type for synth-fun.");
667 }
668 if (range.isFunction())
669 {
670 smt2->parseError("Cannot use synth-fun with function return type.");
671 }
672 std::vector<Type> varSorts;
673 for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
674 {
675 varSorts.push_back(p.second);
676 }
677 Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
678 Type synthFunType =
679 varSorts.size() > 0
680 ? d_smt2->getExprManager()->mkFunctionType(varSorts, range)
681 : range;
682
683 // we do not allow overloading for synth fun
684 d_synthFun = d_smt2->mkBoundVar(fun, synthFunType);
685 // set the sygus type to be range by default, which is overwritten below
686 // if a grammar is provided
687 d_sygusType = range;
688
689 d_smt2->pushScope(true);
690 d_sygusVars = d_smt2->mkBoundVars(sortedVarNames);
691 }
692
693 Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); }
694
695 std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(Type grammar)
696 {
697 Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl;
698 return std::unique_ptr<Command>(
699 new SynthFunCommand(d_fun,
700 d_synthFun,
701 grammar.isNull() ? d_sygusType : grammar,
702 d_isInv,
703 d_sygusVars));
704 }
705
706 std::unique_ptr<Command> Smt2::invConstraint(
707 const std::vector<std::string>& names)
708 {
709 checkThatLogicIsSet();
710 Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
711 Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
712
713 if (names.size() != 4)
714 {
715 parseError(
716 "Bad syntax for inv-constraint: expected 4 "
717 "arguments.");
718 }
719
720 std::vector<Expr> terms;
721 for (const std::string& name : names)
722 {
723 if (!isDeclared(name))
724 {
725 std::stringstream ss;
726 ss << "Function " << name << " in inv-constraint is not defined.";
727 parseError(ss.str());
728 }
729
730 terms.push_back(getVariable(name));
731 }
732
733 return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms));
734 }
735
736 Command* Smt2::setLogic(std::string name, bool fromCommand)
737 {
738 if (fromCommand)
739 {
740 if (d_seenSetLogic)
741 {
742 parseError("Only one set-logic is allowed.");
743 }
744 d_seenSetLogic = true;
745
746 if (logicIsForced())
747 {
748 // If the logic is forced, we ignore all set-logic requests from commands.
749 return new EmptyCommand();
750 }
751 }
752
753 if (sygus_v1())
754 {
755 // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2)
756 if(name == "Arrays") {
757 name = "A";
758 }else if(name == "Reals") {
759 name = "LRA";
760 }
761 }
762
763 d_logicSet = true;
764 d_logic = name;
765
766 // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
767 // higher-order
768 if(sygus()) {
769 if (!d_logic.isQuantified())
770 {
771 warning("Logics in sygus are assumed to contain quantifiers.");
772 warning("Omit QF_ from the logic to avoid this warning.");
773 }
774 // get unlocked copy, modify, copy and relock
775 LogicInfo log(d_logic.getUnlockedCopy());
776 // enable everything needed for sygus
777 log.enableSygus();
778 d_logic = log;
779 d_logic.lock();
780 }
781
782 // Core theory belongs to every logic
783 addTheory(THEORY_CORE);
784
785 if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
786 addTheory(THEORY_UF);
787 }
788
789 if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
790 if(d_logic.areIntegersUsed()) {
791 if(d_logic.areRealsUsed()) {
792 addTheory(THEORY_REALS_INTS);
793 } else {
794 addTheory(THEORY_INTS);
795 }
796 } else if(d_logic.areRealsUsed()) {
797 addTheory(THEORY_REALS);
798 }
799
800 if (d_logic.areTranscendentalsUsed())
801 {
802 addTheory(THEORY_TRANSCENDENTALS);
803 }
804 }
805
806 if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
807 addTheory(THEORY_ARRAYS);
808 }
809
810 if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
811 addTheory(THEORY_BITVECTORS);
812 }
813
814 if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
815 addTheory(THEORY_DATATYPES);
816 }
817
818 if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
819 addTheory(THEORY_SETS);
820 }
821
822 if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
823 addTheory(THEORY_STRINGS);
824 }
825
826 if(d_logic.isQuantified()) {
827 addTheory(THEORY_QUANTIFIERS);
828 }
829
830 if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
831 addTheory(THEORY_FP);
832 }
833
834 if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
835 addTheory(THEORY_SEP);
836 }
837
838 Command* cmd =
839 new SetBenchmarkLogicCommand(sygus() ? d_logic.getLogicString() : name);
840 cmd->setMuted(!fromCommand);
841 return cmd;
842 } /* Smt2::setLogic() */
843
844 bool Smt2::sygus() const
845 {
846 InputLanguage ilang = getLanguage();
847 return ilang == language::input::LANG_SYGUS
848 || ilang == language::input::LANG_SYGUS_V2;
849 }
850 bool Smt2::sygus_v1() const
851 {
852 return getLanguage() == language::input::LANG_SYGUS;
853 }
854
855 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
856 // TODO: ???
857 }
858
859 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
860 // TODO: ???
861 }
862
863 void Smt2::checkThatLogicIsSet()
864 {
865 if (!logicIsSet())
866 {
867 if (strictModeEnabled())
868 {
869 parseError("set-logic must appear before this point.");
870 }
871 else
872 {
873 Command* cmd = nullptr;
874 if (logicIsForced())
875 {
876 cmd = setLogic(getForcedLogic(), false);
877 }
878 else
879 {
880 warning("No set-logic command was given before this point.");
881 warning("CVC4 will make all theories available.");
882 warning(
883 "Consider setting a stricter logic for (likely) better "
884 "performance.");
885 warning("To suppress this warning in the future use (set-logic ALL).");
886
887 cmd = setLogic("ALL", false);
888 }
889 preemptCommand(cmd);
890 }
891 }
892 }
893
894 /* The include are managed in the lexer but called in the parser */
895 // Inspired by http://www.antlr3.org/api/C/interop.html
896
897 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
898 Debug("parser") << "Including " << filename << std::endl;
899 // Create a new input stream and take advantage of built in stream stacking
900 // in C target runtime.
901 //
902 pANTLR3_INPUT_STREAM in;
903 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
904 in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
905 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
906 in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
907 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
908 if( in == NULL ) {
909 Debug("parser") << "Can't open " << filename << std::endl;
910 return false;
911 }
912 // Same thing as the predefined PUSHSTREAM(in);
913 lexer->pushCharStream(lexer, in);
914 // restart it
915 //lexer->rec->state->tokenStartCharIndex = -10;
916 //lexer->emit(lexer);
917
918 // Note that the input stream is not closed when it EOFs, I don't bother
919 // to do it here, but it is up to you to track streams created like this
920 // and destroy them when the whole parse session is complete. Remember that you
921 // don't want to do this until all tokens have been manipulated all the way through
922 // your tree parsers etc as the token does not store the text it just refers
923 // back to the input stream and trying to get the text for it will abort if you
924 // close the input stream too early.
925
926 //TODO what said before
927 return true;
928 }
929
930 void Smt2::includeFile(const std::string& filename) {
931 // security for online version
932 if(!canIncludeFile()) {
933 parseError("include-file feature was disabled for this run.");
934 }
935
936 // Get the lexer
937 AntlrInput* ai = static_cast<AntlrInput*>(getInput());
938 pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
939 // get the name of the current stream "Does it work inside an include?"
940 const std::string inputName = ai->getInputStreamName();
941
942 // Find the directory of the current input file
943 std::string path;
944 size_t pos = inputName.rfind('/');
945 if(pos != std::string::npos) {
946 path = std::string(inputName, 0, pos + 1);
947 }
948 path.append(filename);
949 if(!newInputStream(path, lexer)) {
950 parseError("Couldn't open include file `" + path + "'");
951 }
952 }
953
954 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
955 if( type.isInteger() ){
956 ops.push_back(getExprManager()->mkConst(Rational(0)));
957 ops.push_back(getExprManager()->mkConst(Rational(1)));
958 }else if( type.isBitVector() ){
959 unsigned sz = ((BitVectorType)type).getSize();
960 BitVector bval0(sz, (unsigned int)0);
961 ops.push_back( getExprManager()->mkConst(bval0) );
962 BitVector bval1(sz, (unsigned int)1);
963 ops.push_back( getExprManager()->mkConst(bval1) );
964 }else if( type.isBoolean() ){
965 ops.push_back(getExprManager()->mkConst(true));
966 ops.push_back(getExprManager()->mkConst(false));
967 }
968 //TODO : others?
969 }
970
971 // This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
972 // This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
973 void Smt2::processSygusGTerm(
974 CVC4::SygusGTerm& sgt,
975 int index,
976 std::vector<CVC4::Datatype>& datatypes,
977 std::vector<CVC4::Type>& sorts,
978 std::vector<std::vector<CVC4::Expr>>& ops,
979 std::vector<std::vector<std::string>>& cnames,
980 std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
981 std::vector<bool>& allow_const,
982 std::vector<std::vector<std::string>>& unresolved_gterm_sym,
983 const std::vector<CVC4::Expr>& sygus_vars,
984 std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
985 std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
986 CVC4::Type& ret,
987 bool isNested)
988 {
989 if (sgt.d_gterm_type == SygusGTerm::gterm_op)
990 {
991 Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index
992 << std::endl;
993 Kind oldKind;
994 Kind newKind = kind::UNDEFINED_KIND;
995 //convert to UMINUS if one child of MINUS
996 if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){
997 oldKind = kind::MINUS;
998 newKind = kind::UMINUS;
999 }
1000 if( newKind!=kind::UNDEFINED_KIND ){
1001 Expr newExpr = getExprManager()->operatorOf(newKind);
1002 Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl;
1003 sgt.d_expr = newExpr;
1004 std::string oldName = kind::kindToString(oldKind);
1005 std::string newName = kind::kindToString(newKind);
1006 size_t pos = 0;
1007 if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){
1008 sgt.d_name.replace(pos, oldName.length(), newName);
1009 }
1010 }
1011 ops[index].push_back( sgt.d_expr );
1012 cnames[index].push_back( sgt.d_name );
1013 cargs[index].push_back( std::vector< CVC4::Type >() );
1014 for( unsigned i=0; i<sgt.d_children.size(); i++ ){
1015 std::stringstream ss;
1016 ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
1017 std::string sub_dname = ss.str();
1018 //add datatype for child
1019 Type null_type;
1020 pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
1021 int sub_dt_index = datatypes.size()-1;
1022 //process child
1023 Type sub_ret;
1024 processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
1025 sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
1026 //process the nested gterm (either pop the last datatype, or flatten the argument)
1027 Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
1028 sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
1029 cargs[index].back().push_back(tt);
1030 }
1031 }
1032 else if (sgt.d_gterm_type == SygusGTerm::gterm_constant)
1033 {
1034 if( sgt.getNumChildren()!=0 ){
1035 parseError("Bad syntax for Sygus Constant.");
1036 }
1037 std::vector< Expr > consts;
1038 mkSygusConstantsForType( sgt.d_type, consts );
1039 Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
1040 for( unsigned i=0; i<consts.size(); i++ ){
1041 std::stringstream ss;
1042 ss << consts[i];
1043 Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
1044 ops[index].push_back( consts[i] );
1045 cnames[index].push_back( ss.str() );
1046 cargs[index].push_back( std::vector< CVC4::Type >() );
1047 }
1048 allow_const[index] = true;
1049 }
1050 else if (sgt.d_gterm_type == SygusGTerm::gterm_variable
1051 || sgt.d_gterm_type == SygusGTerm::gterm_input_variable)
1052 {
1053 if( sgt.getNumChildren()!=0 ){
1054 parseError("Bad syntax for Sygus Variable.");
1055 }
1056 Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
1057 for( unsigned i=0; i<sygus_vars.size(); i++ ){
1058 if( sygus_vars[i].getType()==sgt.d_type ){
1059 std::stringstream ss;
1060 ss << sygus_vars[i];
1061 Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
1062 ops[index].push_back( sygus_vars[i] );
1063 cnames[index].push_back( ss.str() );
1064 cargs[index].push_back( std::vector< CVC4::Type >() );
1065 }
1066 }
1067 }
1068 else if (sgt.d_gterm_type == SygusGTerm::gterm_nested_sort)
1069 {
1070 ret = sgt.d_type;
1071 }
1072 else if (sgt.d_gterm_type == SygusGTerm::gterm_unresolved)
1073 {
1074 if( isNested ){
1075 if( isUnresolvedType(sgt.d_name) ){
1076 ret = getSort(sgt.d_name);
1077 }else{
1078 //nested, unresolved symbol...fail
1079 std::stringstream ss;
1080 ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl;
1081 parseError(ss.str());
1082 }
1083 }else{
1084 //will resolve when adding constructors
1085 unresolved_gterm_sym[index].push_back(sgt.d_name);
1086 }
1087 }
1088 else if (sgt.d_gterm_type == SygusGTerm::gterm_ignore)
1089 {
1090 // do nothing
1091 }
1092 }
1093
1094 bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
1095 std::vector< CVC4::Datatype >& datatypes,
1096 std::vector< CVC4::Type>& sorts,
1097 std::vector< std::vector<CVC4::Expr> >& ops,
1098 std::vector< std::vector<std::string> >& cnames,
1099 std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
1100 std::vector< bool >& allow_const,
1101 std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
1102 sorts.push_back(t);
1103 datatypes.push_back(Datatype(getExprManager(), dname));
1104 ops.push_back(std::vector<Expr>());
1105 cnames.push_back(std::vector<std::string>());
1106 cargs.push_back(std::vector<std::vector<CVC4::Type> >());
1107 allow_const.push_back(false);
1108 unresolved_gterm_sym.push_back(std::vector< std::string >());
1109 return true;
1110 }
1111
1112 bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
1113 std::vector< CVC4::Type>& sorts,
1114 std::vector< std::vector<CVC4::Expr> >& ops,
1115 std::vector< std::vector<std::string> >& cnames,
1116 std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
1117 std::vector< bool >& allow_const,
1118 std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
1119 sorts.pop_back();
1120 datatypes.pop_back();
1121 ops.pop_back();
1122 cnames.pop_back();
1123 cargs.pop_back();
1124 allow_const.pop_back();
1125 unresolved_gterm_sym.pop_back();
1126 return true;
1127 }
1128
1129 Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
1130 std::vector< CVC4::Type>& sorts,
1131 std::vector< std::vector<CVC4::Expr> >& ops,
1132 std::vector< std::vector<std::string> >& cnames,
1133 std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
1134 std::vector< bool >& allow_const,
1135 std::vector< std::vector< std::string > >& unresolved_gterm_sym,
1136 std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
1137 std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) {
1138 Type t = sub_ret;
1139 Debug("parser-sygus") << "Argument is ";
1140 if( t.isNull() ){
1141 //then, it is the datatype we constructed, which should have a single constructor
1142 t = mkUnresolvedType(sub_dname);
1143 Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t << std::endl;
1144 Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs[sub_dt_index].size() << std::endl;
1145 if( cargs[sub_dt_index].empty() ){
1146 parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
1147 }
1148 Expr sop = ops[sub_dt_index][0];
1149 Type curr_t;
1150 if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){
1151 curr_t = sop.getType();
1152 Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl;
1153 // only cache if it is a singleton datatype (has unique expr)
1154 if (ops[sub_dt_index].size() == 1)
1155 {
1156 sygus_to_builtin_expr[t] = sop;
1157 // store that term sop has dedicated sygus type t
1158 if (d_sygus_bound_var_type.find(sop) == d_sygus_bound_var_type.end())
1159 {
1160 d_sygus_bound_var_type[sop] = t;
1161 }
1162 }
1163 }else{
1164 std::vector< Expr > children;
1165 if( sop.getKind() != kind::BUILTIN ){
1166 children.push_back( sop );
1167 }
1168 for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
1169 std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
1170 if( it==sygus_to_builtin_expr.end() ){
1171 if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){
1172 std::stringstream ss;
1173 ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl;
1174 ss << "Builtin types are currently : " << std::endl;
1175 for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){
1176 ss << " " << itb->first << " -> " << itb->second << std::endl;
1177 }
1178 parseError(ss.str());
1179 }
1180 Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
1181 Debug("parser-sygus") << ": child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
1182 std::stringstream ss;
1183 ss << t << "_x_" << i;
1184 Expr bv = mkBoundVar(ss.str(), bt);
1185 children.push_back( bv );
1186 d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i];
1187 }else{
1188 Debug("parser-sygus") << ": child " << i << " existing sygus to builtin expr : " << it->second << std::endl;
1189 children.push_back( it->second );
1190 }
1191 }
1192 Kind sk = sop.getKind() != kind::BUILTIN
1193 ? getKindForFunction(sop)
1194 : getExprManager()->operatorToKind(sop);
1195 Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl;
1196 Expr e = getExprManager()->mkExpr( sk, children );
1197 Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
1198 curr_t = e.getType();
1199 sygus_to_builtin_expr[t] = e;
1200 }
1201 sorts[sub_dt_index] = curr_t;
1202 sygus_to_builtin[t] = curr_t;
1203 }else{
1204 Debug("parser-sygus") << "simple argument " << t << std::endl;
1205 Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl;
1206 //otherwise, datatype was unecessary
1207 //pop argument datatype definition
1208 popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
1209 }
1210 return t;
1211 }
1212
1213 void Smt2::setSygusStartIndex(const std::string& fun,
1214 int startIndex,
1215 std::vector<CVC4::Datatype>& datatypes,
1216 std::vector<CVC4::Type>& sorts,
1217 std::vector<std::vector<CVC4::Expr>>& ops)
1218 {
1219 if( startIndex>0 ){
1220 CVC4::Datatype tmp_dt = datatypes[0];
1221 Type tmp_sort = sorts[0];
1222 std::vector< Expr > tmp_ops;
1223 tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
1224 datatypes[0] = datatypes[startIndex];
1225 sorts[0] = sorts[startIndex];
1226 ops[0].clear();
1227 ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
1228 datatypes[startIndex] = tmp_dt;
1229 sorts[startIndex] = tmp_sort;
1230 ops[startIndex].clear();
1231 ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
1232 }else if( startIndex<0 ){
1233 std::stringstream ss;
1234 ss << "warning: no symbol named Start for synth-fun " << fun << std::endl;
1235 warning(ss.str());
1236 }
1237 }
1238
1239 void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
1240 std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
1241 std::vector<std::string>& unresolved_gterm_sym,
1242 std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
1243 Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
1244 Debug("parser-sygus") << " add constructors..." << std::endl;
1245
1246 Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl;
1247 Debug("parser-sygus") << " add constructors..." << std::endl;
1248 // size of cnames changes, this loop must check size
1249 for (unsigned i = 0; i < cnames.size(); i++)
1250 {
1251 bool is_dup = false;
1252 bool is_dup_op = false;
1253 for (unsigned j = 0; j < i; j++)
1254 {
1255 if( ops[i]==ops[j] ){
1256 is_dup_op = true;
1257 if( cargs[i].size()==cargs[j].size() ){
1258 is_dup = true;
1259 for( unsigned k=0; k<cargs[i].size(); k++ ){
1260 if( cargs[i][k]!=cargs[j][k] ){
1261 is_dup = false;
1262 break;
1263 }
1264 }
1265 }
1266 if( is_dup ){
1267 break;
1268 }
1269 }
1270 }
1271 Debug("parser-sygus") << "SYGUS CONS " << i << " : ";
1272 if( is_dup ){
1273 Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl;
1274 ops.erase( ops.begin() + i, ops.begin() + i + 1 );
1275 cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 );
1276 cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 );
1277 i--;
1278 }
1279 else
1280 {
1281 std::shared_ptr<SygusPrintCallback> spc;
1282 if (is_dup_op)
1283 {
1284 Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i]
1285 << std::endl;
1286 // make into define-fun
1287 std::vector<Type> ltypes;
1288 for (unsigned j = 0, size = cargs[i].size(); j < size; j++)
1289 {
1290 ltypes.push_back(sygus_to_builtin[cargs[i][j]]);
1291 }
1292 std::vector<Expr> largs;
1293 Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
1294
1295 // make the let_body
1296 std::vector<Expr> children;
1297 if (ops[i].getKind() != kind::BUILTIN)
1298 {
1299 children.push_back(ops[i]);
1300 }
1301 children.insert(children.end(), largs.begin(), largs.end());
1302 Kind sk = ops[i].getKind() != kind::BUILTIN
1303 ? getKindForFunction(ops[i])
1304 : getExprManager()->operatorToKind(ops[i]);
1305 Expr body = getExprManager()->mkExpr(sk, children);
1306 // replace by lambda
1307 ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
1308 Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl;
1309 // callback prints as the expression
1310 spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs);
1311 }
1312 else
1313 {
1314 if (ops[i].getType().isBitVector() && ops[i].isConst())
1315 {
1316 Debug("parser-sygus") << "--> Bit-vector constant " << ops[i] << " ("
1317 << cnames[i] << ")" << std::endl;
1318 // Since there are multiple output formats for bit-vectors and
1319 // we are required by sygus standards to print in the exact input
1320 // format given by the user, we use a print callback to custom print
1321 // the given name.
1322 spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
1323 }
1324 else if (ops[i].getKind() == kind::VARIABLE)
1325 {
1326 Debug("parser-sygus") << "--> Defined function " << ops[i]
1327 << std::endl;
1328 // turn f into (lammbda (x) (f x))
1329 // in a degenerate case, ops[i] may be a defined constant,
1330 // in which case we do not replace by a lambda.
1331 if (ops[i].getType().isFunction())
1332 {
1333 std::vector<Type> ftypes =
1334 static_cast<FunctionType>(ops[i].getType()).getArgTypes();
1335 std::vector<Expr> largs;
1336 Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
1337 largs.insert(largs.begin(), ops[i]);
1338 Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs);
1339 ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
1340 Debug("parser-sygus") << " ...replace op : " << ops[i]
1341 << std::endl;
1342 }
1343 else
1344 {
1345 Debug("parser-sygus") << " ...replace op : " << ops[i]
1346 << std::endl;
1347 }
1348 // keep a callback to say it should be printed with the defined name
1349 spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
1350 }
1351 else
1352 {
1353 Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl;
1354 }
1355 }
1356 // must rename to avoid duplication
1357 std::stringstream ss;
1358 ss << dt.getName() << "_" << i << "_" << cnames[i];
1359 cnames[i] = ss.str();
1360 Debug("parser-sygus") << " construct the datatype " << cnames[i] << "..."
1361 << std::endl;
1362 // add the sygus constructor
1363 dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc);
1364 Debug("parser-sygus") << " finished constructing the datatype"
1365 << std::endl;
1366 }
1367 }
1368
1369 Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl;
1370 if( !unresolved_gterm_sym.empty() ){
1371 std::vector< Type > types;
1372 Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl;
1373 for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){
1374 Debug("parser-sygus") << " resolve : " << unresolved_gterm_sym[i] << std::endl;
1375 if( isUnresolvedType(unresolved_gterm_sym[i]) ){
1376 Debug("parser-sygus") << " it is an unresolved type." << std::endl;
1377 Type t = getSort(unresolved_gterm_sym[i]);
1378 if( std::find( types.begin(), types.end(), t )==types.end() ){
1379 types.push_back( t );
1380 //identity element
1381 Type bt = dt.getSygusType();
1382 Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl;
1383
1384 std::stringstream ss;
1385 ss << t << "_x";
1386 Expr var = mkBoundVar(ss.str(), bt);
1387 std::vector<Expr> lchildren;
1388 lchildren.push_back(
1389 getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var));
1390 lchildren.push_back(var);
1391 Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren);
1392
1393 // empty sygus callback (should not be printed)
1394 std::shared_ptr<SygusPrintCallback> sepc =
1395 std::make_shared<printer::SygusEmptyPrintCallback>();
1396
1397 //make the sygus argument list
1398 std::vector< Type > id_carg;
1399 id_carg.push_back( t );
1400 dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc);
1401
1402 //add to operators
1403 ops.push_back( id_op );
1404 }
1405 }else{
1406 std::stringstream ss;
1407 ss << "Unhandled sygus constructor " << unresolved_gterm_sym[i];
1408 throw ParserException(ss.str());
1409 }
1410 }
1411 }
1412 }
1413
1414 Expr Smt2::makeSygusBoundVarList(Datatype& dt,
1415 unsigned i,
1416 const std::vector<Type>& ltypes,
1417 std::vector<Expr>& lvars)
1418 {
1419 for (unsigned j = 0, size = ltypes.size(); j < size; j++)
1420 {
1421 std::stringstream ss;
1422 ss << dt.getName() << "_x_" << i << "_" << j;
1423 Expr v = mkBoundVar(ss.str(), ltypes[j]);
1424 lvars.push_back(v);
1425 }
1426 return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
1427 }
1428
1429 void Smt2::addSygusConstructorTerm(Datatype& dt,
1430 Expr term,
1431 std::map<Expr, Type>& ntsToUnres) const
1432 {
1433 Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl;
1434 // Ensure that we do type checking here to catch sygus constructors with
1435 // malformed builtin operators. The argument "true" to getType here forces
1436 // a recursive well-typedness check.
1437 term.getType(true);
1438 // purify each occurrence of a non-terminal symbol in term, replace by
1439 // free variables. These become arguments to constructors. Notice we must do
1440 // a tree traversal in this function, since unique paths to the same term
1441 // should be treated as distinct terms.
1442 // Notice that let expressions are forbidden in the input syntax of term, so
1443 // this does not lead to exponential behavior with respect to input size.
1444 std::vector<Expr> args;
1445 std::vector<Type> cargs;
1446 Expr op = purifySygusGTerm(term, ntsToUnres, args, cargs);
1447 Trace("parser-sygus2") << "Purified operator " << op
1448 << ", #args/cargs=" << args.size() << "/"
1449 << cargs.size() << std::endl;
1450 std::shared_ptr<SygusPrintCallback> spc;
1451 // callback prints as the expression
1452 spc = std::make_shared<printer::SygusExprPrintCallback>(op, args);
1453 if (!args.empty())
1454 {
1455 bool pureVar = false;
1456 if (op.getNumChildren() == args.size())
1457 {
1458 pureVar = true;
1459 for (unsigned i = 0, nchild = op.getNumChildren(); i < nchild; i++)
1460 {
1461 if (op[i] != args[i])
1462 {
1463 pureVar = false;
1464 break;
1465 }
1466 }
1467 }
1468 Trace("parser-sygus2") << "Pure var is " << pureVar
1469 << ", hasOp=" << op.hasOperator() << std::endl;
1470 if (pureVar && op.hasOperator())
1471 {
1472 // optimization: use just the operator if it an application to only vars
1473 op = op.getOperator();
1474 }
1475 else
1476 {
1477 Expr lbvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, args);
1478 // its operator is a lambda
1479 op = getExprManager()->mkExpr(kind::LAMBDA, lbvl, op);
1480 }
1481 }
1482 Trace("parser-sygus2") << "Generated operator " << op << std::endl;
1483 std::stringstream ss;
1484 ss << op.getKind();
1485 dt.addSygusConstructor(op, ss.str(), cargs, spc);
1486 }
1487
1488 Expr Smt2::purifySygusGTerm(Expr term,
1489 std::map<Expr, Type>& ntsToUnres,
1490 std::vector<Expr>& args,
1491 std::vector<Type>& cargs) const
1492 {
1493 Trace("parser-sygus2-debug")
1494 << "purifySygusGTerm: " << term << " #nchild=" << term.getNumChildren()
1495 << std::endl;
1496 std::map<Expr, Type>::iterator itn = ntsToUnres.find(term);
1497 if (itn != ntsToUnres.end())
1498 {
1499 Expr ret = getExprManager()->mkBoundVar(term.getType());
1500 Trace("parser-sygus2-debug")
1501 << "...unresolved non-terminal, intro " << ret << std::endl;
1502 args.push_back(ret);
1503 cargs.push_back(itn->second);
1504 return ret;
1505 }
1506 std::vector<Expr> pchildren;
1507 // To test whether the operator should be passed to mkExpr below, we check
1508 // whether this term is parameterized. This includes APPLY_UF terms and BV
1509 // extraction terms, but excludes applications of most interpreted symbols
1510 // like PLUS.
1511 if (term.isParameterized())
1512 {
1513 pchildren.push_back(term.getOperator());
1514 }
1515 bool childChanged = false;
1516 for (unsigned i = 0, nchild = term.getNumChildren(); i < nchild; i++)
1517 {
1518 Trace("parser-sygus2-debug")
1519 << "......purify child " << i << " : " << term[i] << std::endl;
1520 Expr ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs);
1521 pchildren.push_back(ptermc);
1522 childChanged = childChanged || ptermc != term[i];
1523 }
1524 if (!childChanged)
1525 {
1526 Trace("parser-sygus2-debug") << "...no child changed" << std::endl;
1527 return term;
1528 }
1529 Expr nret = getExprManager()->mkExpr(term.getKind(), pchildren);
1530 Trace("parser-sygus2-debug")
1531 << "...child changed, return " << nret << std::endl;
1532 return nret;
1533 }
1534
1535 void Smt2::addSygusConstructorVariables(Datatype& dt,
1536 const std::vector<Expr>& sygusVars,
1537 Type type) const
1538 {
1539 // each variable of appropriate type becomes a sygus constructor in dt.
1540 for (unsigned i = 0, size = sygusVars.size(); i < size; i++)
1541 {
1542 Expr v = sygusVars[i];
1543 if (v.getType() == type)
1544 {
1545 std::stringstream ss;
1546 ss << v;
1547 std::vector<CVC4::Type> cargs;
1548 dt.addSygusConstructor(v, ss.str(), cargs);
1549 }
1550 }
1551 }
1552
1553 InputLanguage Smt2::getLanguage() const
1554 {
1555 ExprManager* em = getExprManager();
1556 return em->getOptions().getInputLanguage();
1557 }
1558
1559 void Smt2::applyTypeAscription(ParseOp& p, Type type)
1560 {
1561 // (as const (Array T1 T2))
1562 if (p.d_kind == kind::STORE_ALL)
1563 {
1564 if (!type.isArray())
1565 {
1566 std::stringstream ss;
1567 ss << "expected array constant term, but cast is not of array type"
1568 << std::endl
1569 << "cast type: " << type;
1570 parseError(ss.str());
1571 }
1572 p.d_type = type;
1573 return;
1574 }
1575 if (p.d_expr.isNull())
1576 {
1577 Trace("parser-overloading")
1578 << "Getting variable expression with name " << p.d_name << " and type "
1579 << type << std::endl;
1580 // get the variable expression for the type
1581 if (isDeclared(p.d_name, SYM_VARIABLE))
1582 {
1583 p.d_expr = getExpressionForNameAndType(p.d_name, type);
1584 }
1585 if (p.d_expr.isNull())
1586 {
1587 std::stringstream ss;
1588 ss << "Could not resolve expression with name " << p.d_name
1589 << " and type " << type << std::endl;
1590 parseError(ss.str());
1591 }
1592 }
1593 ExprManager* em = getExprManager();
1594 Type etype = p.d_expr.getType();
1595 Kind ekind = p.d_expr.getKind();
1596 Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr;
1597 Trace("parser-qid") << " " << ekind << " " << etype;
1598 Trace("parser-qid") << std::endl;
1599 if (ekind == kind::APPLY_CONSTRUCTOR && type.isDatatype())
1600 {
1601 // nullary constructors with a type ascription
1602 // could be a parametric constructor or just an overloaded constructor
1603 DatatypeType dtype = static_cast<DatatypeType>(type);
1604 if (dtype.isParametric())
1605 {
1606 std::vector<Expr> v;
1607 Expr e = p.d_expr.getOperator();
1608 const DatatypeConstructor& dtc =
1609 Datatype::datatypeOf(e)[Datatype::indexOf(e)];
1610 v.push_back(em->mkExpr(
1611 kind::APPLY_TYPE_ASCRIPTION,
1612 em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))),
1613 p.d_expr.getOperator()));
1614 v.insert(v.end(), p.d_expr.begin(), p.d_expr.end());
1615 p.d_expr = em->mkExpr(kind::APPLY_CONSTRUCTOR, v);
1616 }
1617 }
1618 else if (etype.isConstructor())
1619 {
1620 // a non-nullary constructor with a type ascription
1621 DatatypeType dtype = static_cast<DatatypeType>(type);
1622 if (dtype.isParametric())
1623 {
1624 const DatatypeConstructor& dtc =
1625 Datatype::datatypeOf(p.d_expr)[Datatype::indexOf(p.d_expr)];
1626 p.d_expr = em->mkExpr(
1627 kind::APPLY_TYPE_ASCRIPTION,
1628 em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))),
1629 p.d_expr);
1630 }
1631 }
1632 else if (ekind == kind::EMPTYSET)
1633 {
1634 Debug("parser") << "Empty set encountered: " << p.d_expr << " " << type
1635 << std::endl;
1636 p.d_expr = em->mkConst(EmptySet(type));
1637 }
1638 else if (ekind == kind::UNIVERSE_SET)
1639 {
1640 p.d_expr = em->mkNullaryOperator(type, kind::UNIVERSE_SET);
1641 }
1642 else if (ekind == kind::SEP_NIL)
1643 {
1644 // We don't want the nil reference to be a constant: for instance, it
1645 // could be of type Int but is not a const rational. However, the
1646 // expression has 0 children. So we convert to a SEP_NIL variable.
1647 p.d_expr = em->mkNullaryOperator(type, kind::SEP_NIL);
1648 }
1649 else if (etype != type)
1650 {
1651 parseError("Type ascription not satisfied.");
1652 }
1653 }
1654
1655 Expr Smt2::parseOpToExpr(ParseOp& p)
1656 {
1657 Expr expr;
1658 if (p.d_kind != kind::NULL_EXPR || !p.d_type.isNull())
1659 {
1660 parseError(
1661 "Bad syntax for qualified identifier operator in term position.");
1662 }
1663 else if (!p.d_expr.isNull())
1664 {
1665 expr = p.d_expr;
1666 }
1667 else if (!isDeclared(p.d_name, SYM_VARIABLE))
1668 {
1669 if (sygus_v1() && p.d_name[0] == '-'
1670 && p.d_name.find_first_not_of("0123456789", 1) == std::string::npos)
1671 {
1672 // allow unary minus in sygus version 1
1673 expr = getExprManager()->mkConst(Rational(p.d_name));
1674 }
1675 else
1676 {
1677 std::stringstream ss;
1678 ss << "Symbol " << p.d_name << " is not declared.";
1679 parseError(ss.str());
1680 }
1681 }
1682 else
1683 {
1684 expr = getExpressionForName(p.d_name);
1685 }
1686 assert(!expr.isNull());
1687 return expr;
1688 }
1689
1690 Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
1691 {
1692 bool isBuiltinOperator = false;
1693 // the builtin kind of the overall return expression
1694 Kind kind = kind::NULL_EXPR;
1695 // First phase: process the operator
1696 if (Debug.isOn("parser"))
1697 {
1698 Debug("parser") << "Apply parse op to:" << std::endl;
1699 Debug("parser") << "args has size " << args.size() << std::endl;
1700 for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
1701 {
1702 Debug("parser") << "++ " << *i << std::endl;
1703 }
1704 }
1705 if (p.d_kind != kind::NULL_EXPR)
1706 {
1707 // It is a special case, e.g. tupSel or array constant specification.
1708 // We have to wait until the arguments are parsed to resolve it.
1709 }
1710 else if (!p.d_expr.isNull())
1711 {
1712 // An explicit operator, e.g. an indexed symbol.
1713 args.insert(args.begin(), p.d_expr);
1714 if (p.d_expr.getType().isTester())
1715 {
1716 // Testers are handled differently than other indexed operators,
1717 // since they require a kind.
1718 kind = kind::APPLY_TESTER;
1719 }
1720 }
1721 else
1722 {
1723 isBuiltinOperator = isOperatorEnabled(p.d_name);
1724 if (isBuiltinOperator)
1725 {
1726 // a builtin operator, convert to kind
1727 kind = getOperatorKind(p.d_name);
1728 }
1729 else
1730 {
1731 // A non-built-in function application, get the expression
1732 checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE);
1733 Expr v = getVariable(p.d_name);
1734 if (!v.isNull())
1735 {
1736 checkFunctionLike(v);
1737 kind = getKindForFunction(v);
1738 args.insert(args.begin(), v);
1739 }
1740 else
1741 {
1742 // Overloaded symbol?
1743 // Could not find the expression. It may be an overloaded symbol,
1744 // in which case we may find it after knowing the types of its
1745 // arguments.
1746 std::vector<Type> argTypes;
1747 for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
1748 {
1749 argTypes.push_back((*i).getType());
1750 }
1751 Expr op = getOverloadedFunctionForTypes(p.d_name, argTypes);
1752 if (!op.isNull())
1753 {
1754 checkFunctionLike(op);
1755 kind = getKindForFunction(op);
1756 args.insert(args.begin(), op);
1757 }
1758 else
1759 {
1760 parseError(
1761 "Cannot find unambiguous overloaded function for argument "
1762 "types.");
1763 }
1764 }
1765 }
1766 }
1767 // Second phase: apply the arguments to the parse op
1768 ExprManager* em = getExprManager();
1769 // handle special cases
1770 if (p.d_kind == kind::STORE_ALL)
1771 {
1772 if (args.size() != 1)
1773 {
1774 parseError("Too many arguments to array constant.");
1775 }
1776 Expr constVal = args[0];
1777 if (!constVal.isConst())
1778 {
1779 // To parse array constants taking reals whose values are specified by
1780 // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
1781 // the fact that (/ 1 3) is the division of constants 1 and 3, and not
1782 // the resulting constant rational value. Thus, we must construct the
1783 // resulting rational here. This also is applied for integral real values
1784 // like 5.0 which are converted to (/ 5 1) to distinguish them from
1785 // integer constants. We must ensure numerator and denominator are
1786 // constant and the denominator is non-zero.
1787 if (constVal.getKind() == kind::DIVISION && constVal[0].isConst()
1788 && constVal[1].isConst()
1789 && !constVal[1].getConst<Rational>().isZero())
1790 {
1791 constVal = em->mkConst(constVal[0].getConst<Rational>()
1792 / constVal[1].getConst<Rational>());
1793 }
1794 if (!constVal.isConst())
1795 {
1796 std::stringstream ss;
1797 ss << "expected constant term inside array constant, but found "
1798 << "nonconstant term:" << std::endl
1799 << "the term: " << constVal;
1800 parseError(ss.str());
1801 }
1802 }
1803 ArrayType aqtype = static_cast<ArrayType>(p.d_type);
1804 if (!aqtype.getConstituentType().isComparableTo(constVal.getType()))
1805 {
1806 std::stringstream ss;
1807 ss << "type mismatch inside array constant term:" << std::endl
1808 << "array type: " << p.d_type << std::endl
1809 << "expected const type: " << aqtype.getConstituentType() << std::endl
1810 << "computed const type: " << constVal.getType();
1811 parseError(ss.str());
1812 }
1813 return em->mkConst(ArrayStoreAll(p.d_type, constVal));
1814 }
1815 else if (p.d_kind == kind::APPLY_SELECTOR)
1816 {
1817 if (p.d_expr.isNull())
1818 {
1819 parseError("Could not process parsed tuple selector.");
1820 }
1821 // tuple selector case
1822 Integer x = p.d_expr.getConst<Rational>().getNumerator();
1823 if (!x.fitsUnsignedInt())
1824 {
1825 parseError("index of tupSel is larger than size of unsigned int");
1826 }
1827 unsigned int n = x.toUnsignedInt();
1828 if (args.size() > 1)
1829 {
1830 parseError("tupSel applied to more than one tuple argument");
1831 }
1832 Type t = args[0].getType();
1833 if (!t.isTuple())
1834 {
1835 parseError("tupSel applied to non-tuple");
1836 }
1837 size_t length = ((DatatypeType)t).getTupleLength();
1838 if (n >= length)
1839 {
1840 std::stringstream ss;
1841 ss << "tuple is of length " << length << "; cannot access index " << n;
1842 parseError(ss.str());
1843 }
1844 const Datatype& dt = ((DatatypeType)t).getDatatype();
1845 return em->mkExpr(kind::APPLY_SELECTOR, dt[0][n].getSelector(), args);
1846 }
1847 else if (p.d_kind != kind::NULL_EXPR)
1848 {
1849 std::stringstream ss;
1850 ss << "Could not process parsed qualified identifier kind " << p.d_kind;
1851 parseError(ss.str());
1852 }
1853 else if (isBuiltinOperator)
1854 {
1855 if (!em->getOptions().getUfHo()
1856 && (kind == kind::EQUAL || kind == kind::DISTINCT))
1857 {
1858 // need --uf-ho if these operators are applied over function args
1859 for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
1860 {
1861 if ((*i).getType().isFunction())
1862 {
1863 parseError(
1864 "Cannot apply equalty to functions unless --uf-ho is set.");
1865 }
1866 }
1867 }
1868 if (args.size() > 2)
1869 {
1870 if (kind == kind::INTS_DIVISION || kind == kind::XOR
1871 || kind == kind::MINUS || kind == kind::DIVISION
1872 || (kind == kind::BITVECTOR_XNOR && v2_6()))
1873 {
1874 // Builtin operators that are not tokenized, are left associative,
1875 // but not internally variadic must set this.
1876 return em->mkLeftAssociative(kind, args);
1877 }
1878 else if (kind == kind::IMPLIES)
1879 {
1880 /* right-associative, but CVC4 internally only supports 2 args */
1881 return em->mkRightAssociative(kind, args);
1882 }
1883 else if (kind == kind::EQUAL || kind == kind::LT || kind == kind::GT
1884 || kind == kind::LEQ || kind == kind::GEQ)
1885 {
1886 /* "chainable", but CVC4 internally only supports 2 args */
1887 return em->mkExpr(em->mkConst(Chain(kind)), args);
1888 }
1889 }
1890
1891 if (kind::isAssociative(kind) && args.size() > em->maxArity(kind))
1892 {
1893 /* Special treatment for associative operators with lots of children
1894 */
1895 return em->mkAssociative(kind, args);
1896 }
1897 else if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR)
1898 && args.size() == 1)
1899 {
1900 // Unary AND/OR can be replaced with the argument.
1901 return args[0];
1902 }
1903 else if (kind == kind::MINUS && args.size() == 1)
1904 {
1905 return em->mkExpr(kind::UMINUS, args[0]);
1906 }
1907 else
1908 {
1909 checkOperator(kind, args.size());
1910 return em->mkExpr(kind, args);
1911 }
1912 }
1913
1914 if (args.size() >= 2)
1915 {
1916 // may be partially applied function, in this case we use HO_APPLY
1917 Type argt = args[0].getType();
1918 if (argt.isFunction())
1919 {
1920 unsigned arity = static_cast<FunctionType>(argt).getArity();
1921 if (args.size() - 1 < arity)
1922 {
1923 Debug("parser") << "Partial application of " << args[0];
1924 Debug("parser") << " : #argTypes = " << arity;
1925 Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
1926 // must curry the partial application
1927 return em->mkLeftAssociative(kind::HO_APPLY, args);
1928 }
1929 }
1930 }
1931 if (kind == kind::NULL_EXPR)
1932 {
1933 std::vector<Expr> eargs(args.begin() + 1, args.end());
1934 return em->mkExpr(args[0], eargs);
1935 }
1936 return em->mkExpr(kind, args);
1937 }
1938
1939 Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr)
1940 {
1941 if (!sexpr.isKeyword())
1942 {
1943 parseError("improperly formed :named annotation");
1944 }
1945 std::string name = sexpr.getValue();
1946 checkUserSymbol(name);
1947 // ensure expr is a closed subterm
1948 if (expr.hasFreeVariable())
1949 {
1950 std::stringstream ss;
1951 ss << ":named annotations can only name terms that are closed";
1952 parseError(ss.str());
1953 }
1954 // check that sexpr is a fresh function symbol, and reserve it
1955 reserveSymbolAtAssertionLevel(name);
1956 // define it
1957 Expr func = mkVar(name, expr.getType(), ExprManager::VAR_FLAG_DEFINED);
1958 // remember the last term to have been given a :named attribute
1959 setLastNamedTerm(expr, name);
1960 return func;
1961 }
1962
1963 Expr Smt2::mkAnd(const std::vector<Expr>& es)
1964 {
1965 ExprManager* em = getExprManager();
1966
1967 if (es.size() == 0)
1968 {
1969 return em->mkConst(true);
1970 }
1971 else if (es.size() == 1)
1972 {
1973 return es[0];
1974 }
1975 else
1976 {
1977 return em->mkExpr(kind::AND, es);
1978 }
1979 }
1980
1981 } // namespace parser
1982 }/* CVC4 namespace */