GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/parser/smt2/smt2.cpp Lines: 587 671 87.5 %
Date: 2021-03-23 Branches: 975 2058 47.4 %

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