GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/parser/parser.cpp Lines: 360 493 73.0 %
Date: 2021-03-22 Branches: 446 1299 34.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file parser.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Christopher L. Conway
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 Parser state implementation.
13
 **
14
 ** Parser state implementation.
15
 **/
16
17
#include "parser/parser.h"
18
19
#include <clocale>
20
#include <fstream>
21
#include <iostream>
22
#include <iterator>
23
#include <sstream>
24
#include <unordered_set>
25
26
#include "api/cvc4cpp.h"
27
#include "base/check.h"
28
#include "base/output.h"
29
#include "expr/kind.h"
30
#include "options/options.h"
31
#include "parser/input.h"
32
#include "parser/parser_exception.h"
33
#include "smt/command.h"
34
35
using namespace std;
36
using namespace CVC4::kind;
37
38
namespace CVC4 {
39
namespace parser {
40
41
5724
Parser::Parser(api::Solver* solver,
42
               SymbolManager* sm,
43
               Input* input,
44
               bool strictMode,
45
5724
               bool parseOnly)
46
    : d_input(input),
47
      d_symman(sm),
48
5724
      d_symtab(sm->getSymbolTable()),
49
      d_assertionLevel(0),
50
      d_anonymousFunctionCount(0),
51
      d_done(false),
52
      d_checksEnabled(true),
53
      d_strictMode(strictMode),
54
      d_parseOnly(parseOnly),
55
      d_canIncludeFile(true),
56
      d_logicIsForced(false),
57
      d_forcedLogic(),
58
11448
      d_solver(solver)
59
{
60
5724
  d_input->setParser(*this);
61
5724
}
62
63
11448
Parser::~Parser() {
64
5729
  for (std::list<Command*>::iterator iter = d_commandQueue.begin();
65
5729
       iter != d_commandQueue.end(); ++iter) {
66
5
    Command* command = *iter;
67
5
    delete command;
68
  }
69
5724
  d_commandQueue.clear();
70
5724
  delete d_input;
71
5724
}
72
73
921391
api::Solver* Parser::getSolver() const { return d_solver; }
74
75
3806792
api::Term Parser::getSymbol(const std::string& name, SymbolType type)
76
{
77
3806792
  checkDeclaration(name, CHECK_DECLARED, type);
78
3806792
  Assert(isDeclared(name, type));
79
3806792
  Assert(type == SYM_VARIABLE);
80
  // Functions share var namespace
81
3806792
  return d_symtab->lookup(name);
82
}
83
84
9
void Parser::forceLogic(const std::string& logic)
85
{
86
9
  Assert(!d_logicIsForced);
87
9
  d_logicIsForced = true;
88
9
  d_forcedLogic = logic;
89
9
}
90
91
3806792
api::Term Parser::getVariable(const std::string& name)
92
{
93
3806792
  return getSymbol(name, SYM_VARIABLE);
94
}
95
96
api::Term Parser::getFunction(const std::string& name)
97
{
98
  return getSymbol(name, SYM_VARIABLE);
99
}
100
101
3437469
api::Term Parser::getExpressionForName(const std::string& name)
102
{
103
6874938
  api::Sort t;
104
6874938
  return getExpressionForNameAndType(name, t);
105
}
106
107
3437753
api::Term Parser::getExpressionForNameAndType(const std::string& name,
108
                                              api::Sort t)
109
{
110
3437753
  Assert(isDeclared(name));
111
  // first check if the variable is declared and not overloaded
112
3437753
  api::Term expr = getVariable(name);
113
3437753
  if(expr.isNull()) {
114
    // the variable is overloaded, try with type if the type exists
115
6
    if(!t.isNull()) {
116
      // if we decide later to support annotations for function types, this will update to
117
      // separate t into ( argument types, return type )
118
6
      expr = getOverloadedConstantForType(name, t);
119
6
      if(expr.isNull()) {
120
        parseError("Cannot get overloaded constant for type ascription.");
121
      }
122
    }else{
123
      parseError("Overloaded constants must be type cast.");
124
    }
125
  }
126
  // now, post-process the expression
127
3437753
  Assert(!expr.isNull());
128
6875506
  api::Sort te = expr.getSort();
129
3437753
  if (te.isConstructor() && te.getConstructorArity() == 0)
130
  {
131
    // nullary constructors have APPLY_CONSTRUCTOR kind with no children
132
2091
    expr = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, expr);
133
  }
134
6875506
  return expr;
135
}
136
137
bool Parser::getTesterName(api::Term cons, std::string& name) { return false; }
138
139
325757
api::Kind Parser::getKindForFunction(api::Term fun)
140
{
141
651514
  api::Sort t = fun.getSort();
142
325757
  if (t.isFunction())
143
  {
144
310489
    return api::APPLY_UF;
145
  }
146
15268
  else if (t.isConstructor())
147
  {
148
4534
    return api::APPLY_CONSTRUCTOR;
149
  }
150
10734
  else if (t.isSelector())
151
  {
152
9203
    return api::APPLY_SELECTOR;
153
  }
154
1531
  else if (t.isTester())
155
  {
156
1531
    return api::APPLY_TESTER;
157
  }
158
  return api::UNDEFINED_KIND;
159
}
160
161
272271
api::Sort Parser::getSort(const std::string& name)
162
{
163
272272
  checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
164
272270
  Assert(isDeclared(name, SYM_SORT));
165
272270
  api::Sort t = d_symtab->lookupType(name);
166
272270
  return t;
167
}
168
169
590
api::Sort Parser::getSort(const std::string& name,
170
                          const std::vector<api::Sort>& params)
171
{
172
592
  checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
173
588
  Assert(isDeclared(name, SYM_SORT));
174
588
  api::Sort t = d_symtab->lookupType(name, params);
175
588
  return t;
176
}
177
178
5488
size_t Parser::getArity(const std::string& sort_name) {
179
5488
  checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
180
5488
  Assert(isDeclared(sort_name, SYM_SORT));
181
5488
  return d_symtab->lookupArity(sort_name);
182
}
183
184
/* Returns true if name is bound to a boolean variable. */
185
bool Parser::isBoolean(const std::string& name) {
186
  api::Term expr = getVariable(name);
187
  return !expr.isNull() && expr.getSort().isBoolean();
188
}
189
190
324381
bool Parser::isFunctionLike(api::Term fun)
191
{
192
324381
  if(fun.isNull()) {
193
    return false;
194
  }
195
648762
  api::Sort type = fun.getSort();
196
333588
  return type.isFunction() || type.isConstructor() || type.isTester() ||
197
333588
         type.isSelector();
198
}
199
200
/* Returns true if name is bound to a function returning boolean. */
201
bool Parser::isPredicate(const std::string& name) {
202
  api::Term expr = getVariable(name);
203
  return !expr.isNull() && expr.getSort().isPredicate();
204
}
205
206
169798
api::Term Parser::bindVar(const std::string& name,
207
                          const api::Sort& type,
208
                          bool levelZero,
209
                          bool doOverload)
210
{
211
169798
  bool globalDecls = d_symman->getGlobalDeclarations();
212
169798
  Debug("parser") << "bindVar(" << name << ", " << type << ")" << std::endl;
213
169798
  api::Term expr = d_solver->mkConst(type, name);
214
169798
  defineVar(name, expr, globalDecls || levelZero, doOverload);
215
169798
  return expr;
216
}
217
218
59073
api::Term Parser::bindBoundVar(const std::string& name, const api::Sort& type)
219
{
220
118146
  Debug("parser") << "bindBoundVar(" << name << ", " << type << ")"
221
59073
                  << std::endl;
222
59073
  api::Term expr = d_solver->mkVar(type, name);
223
59073
  defineVar(name, expr);
224
59073
  return expr;
225
}
226
227
30508
std::vector<api::Term> Parser::bindBoundVars(
228
    std::vector<std::pair<std::string, api::Sort> >& sortedVarNames)
229
{
230
30508
  std::vector<api::Term> vars;
231
85630
  for (std::pair<std::string, api::Sort>& i : sortedVarNames)
232
  {
233
55122
    vars.push_back(bindBoundVar(i.first, i.second));
234
  }
235
30508
  return vars;
236
}
237
238
std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names,
239
                                        const api::Sort& type,
240
                                        bool levelZero,
241
                                        bool doOverload)
242
{
243
  std::vector<api::Term> vars;
244
  for (unsigned i = 0; i < names.size(); ++i) {
245
    vars.push_back(bindVar(names[i], type, levelZero, doOverload));
246
  }
247
  return vars;
248
}
249
250
27
std::vector<api::Term> Parser::bindBoundVars(
251
    const std::vector<std::string> names, const api::Sort& type)
252
{
253
27
  std::vector<api::Term> vars;
254
54
  for (unsigned i = 0; i < names.size(); ++i) {
255
27
    vars.push_back(bindBoundVar(names[i], type));
256
  }
257
27
  return vars;
258
}
259
260
362450
void Parser::defineVar(const std::string& name,
261
                       const api::Term& val,
262
                       bool levelZero,
263
                       bool doOverload)
264
{
265
362450
  Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;
266
362450
  if (!d_symtab->bind(name, val, levelZero, doOverload))
267
  {
268
    std::stringstream ss;
269
    ss << "Cannot bind " << name << " to symbol of type " << val.getSort();
270
    ss << ", maybe the symbol has already been defined?";
271
    parseError(ss.str());
272
  }
273
362450
  Assert(isDeclared(name));
274
362450
}
275
276
29868
void Parser::defineType(const std::string& name,
277
                        const api::Sort& type,
278
                        bool levelZero,
279
                        bool skipExisting)
280
{
281
29868
  if (skipExisting && isDeclared(name, SYM_SORT))
282
  {
283
1591
    Assert(d_symtab->lookupType(name) == type);
284
1591
    return;
285
  }
286
28277
  d_symtab->bindType(name, type, levelZero);
287
28277
  Assert(isDeclared(name, SYM_SORT));
288
}
289
290
334
void Parser::defineType(const std::string& name,
291
                        const std::vector<api::Sort>& params,
292
                        const api::Sort& type,
293
                        bool levelZero)
294
{
295
334
  d_symtab->bindType(name, params, type, levelZero);
296
334
  Assert(isDeclared(name, SYM_SORT));
297
334
}
298
299
211
void Parser::defineParameterizedType(const std::string& name,
300
                                     const std::vector<api::Sort>& params,
301
                                     const api::Sort& type)
302
{
303
211
  if (Debug.isOn("parser")) {
304
    Debug("parser") << "defineParameterizedType(" << name << ", "
305
                    << params.size() << ", [";
306
    if (params.size() > 0) {
307
      copy(params.begin(),
308
           params.end() - 1,
309
           ostream_iterator<api::Sort>(Debug("parser"), ", "));
310
      Debug("parser") << params.back();
311
    }
312
    Debug("parser") << "], " << type << ")" << std::endl;
313
  }
314
211
  defineType(name, params, type);
315
211
}
316
317
4184
api::Sort Parser::mkSort(const std::string& name)
318
{
319
4184
  Debug("parser") << "newSort(" << name << ")" << std::endl;
320
4184
  bool globalDecls = d_symman->getGlobalDeclarations();
321
4184
  api::Sort type = d_solver->mkUninterpretedSort(name);
322
4184
  defineType(name, type, globalDecls);
323
4184
  return type;
324
}
325
326
23
api::Sort Parser::mkSortConstructor(const std::string& name, size_t arity)
327
{
328
46
  Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
329
23
                  << std::endl;
330
23
  bool globalDecls = d_symman->getGlobalDeclarations();
331
23
  api::Sort type = d_solver->mkSortConstructorSort(name, arity);
332
23
  defineType(name, vector<api::Sort>(arity), type, globalDecls);
333
23
  return type;
334
}
335
336
1079
api::Sort Parser::mkUnresolvedType(const std::string& name)
337
{
338
1079
  api::Sort unresolved = d_solver->mkUninterpretedSort(name);
339
1079
  defineType(name, unresolved);
340
1079
  d_unresolved.insert(unresolved);
341
1079
  return unresolved;
342
}
343
344
39
api::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name,
345
                                              size_t arity)
346
{
347
39
  api::Sort unresolved = d_solver->mkSortConstructorSort(name, arity);
348
39
  defineType(name, vector<api::Sort>(arity), unresolved);
349
39
  d_unresolved.insert(unresolved);
350
39
  return unresolved;
351
}
352
353
10
api::Sort Parser::mkUnresolvedTypeConstructor(
354
    const std::string& name, const std::vector<api::Sort>& params)
355
{
356
20
  Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
357
10
                  << ")" << std::endl;
358
10
  api::Sort unresolved = d_solver->mkSortConstructorSort(name, params.size());
359
10
  defineType(name, params, unresolved);
360
20
  api::Sort t = getSort(name, params);
361
10
  d_unresolved.insert(unresolved);
362
20
  return unresolved;
363
}
364
365
1026
api::Sort Parser::mkUnresolvedType(const std::string& name, size_t arity)
366
{
367
1026
  if (arity == 0)
368
  {
369
987
    return mkUnresolvedType(name);
370
  }
371
39
  return mkUnresolvedTypeConstructor(name, arity);
372
}
373
374
135
bool Parser::isUnresolvedType(const std::string& name) {
375
135
  if (!isDeclared(name, SYM_SORT)) {
376
133
    return false;
377
  }
378
2
  return d_unresolved.find(getSort(name)) != d_unresolved.end();
379
}
380
381
885
std::vector<api::Sort> Parser::bindMutualDatatypeTypes(
382
    std::vector<api::DatatypeDecl>& datatypes, bool doOverload)
383
{
384
  try {
385
    std::vector<api::Sort> types =
386
1770
        d_solver->mkDatatypeSorts(datatypes, d_unresolved);
387
388
885
    Assert(datatypes.size() == types.size());
389
885
    bool globalDecls = d_symman->getGlobalDeclarations();
390
391
2039
    for (unsigned i = 0; i < datatypes.size(); ++i) {
392
2314
      api::Sort t = types[i];
393
2314
      const api::Datatype& dt = t.getDatatype();
394
2314
      const std::string& name = dt.getName();
395
1157
      Debug("parser-idt") << "define " << name << " as " << t << std::endl;
396
1157
      if (isDeclared(name, SYM_SORT)) {
397
        throw ParserException(name + " already declared");
398
      }
399
1157
      if (t.isParametricDatatype())
400
      {
401
102
        std::vector<api::Sort> paramTypes = t.getDatatypeParamSorts();
402
51
        defineType(name, paramTypes, t, globalDecls);
403
      }
404
      else
405
      {
406
1106
        defineType(name, t, globalDecls);
407
      }
408
2314
      std::unordered_set< std::string > consNames;
409
2314
      std::unordered_set< std::string > selNames;
410
3394
      for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
411
      {
412
4480
        const api::DatatypeConstructor& ctor = dt[j];
413
4480
        api::Term constructor = ctor.getConstructorTerm();
414
2240
        Debug("parser-idt") << "+ define " << constructor << std::endl;
415
4480
        string constructorName = ctor.getName();
416
2240
        if(consNames.find(constructorName)==consNames.end()) {
417
2239
          if(!doOverload) {
418
346
            checkDeclaration(constructorName, CHECK_UNDECLARED);
419
          }
420
2237
          defineVar(constructorName, constructor, globalDecls, doOverload);
421
2237
          consNames.insert(constructorName);
422
        }else{
423
1
          throw ParserException(constructorName + " already declared in this datatype");
424
        }
425
4474
        std::string testerName;
426
2237
        if (getTesterName(constructor, testerName))
427
        {
428
4474
          api::Term tester = ctor.getTesterTerm();
429
2237
          Debug("parser-idt") << "+ define " << testerName << std::endl;
430
2237
          if (!doOverload)
431
          {
432
342
            checkDeclaration(testerName, CHECK_UNDECLARED);
433
          }
434
2237
          defineVar(testerName, tester, globalDecls, doOverload);
435
        }
436
4456
        for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++)
437
        {
438
4438
          const api::DatatypeSelector& sel = ctor[k];
439
4438
          api::Term selector = sel.getSelectorTerm();
440
2219
          Debug("parser-idt") << "+++ define " << selector << std::endl;
441
4438
          string selectorName = sel.getName();
442
2219
          if(selNames.find(selectorName)==selNames.end()) {
443
2219
            if(!doOverload) {
444
137
              checkDeclaration(selectorName, CHECK_UNDECLARED);
445
            }
446
2219
            defineVar(selectorName, selector, globalDecls, doOverload);
447
2219
            selNames.insert(selectorName);
448
          }else{
449
            throw ParserException(selectorName + " already declared in this datatype");
450
          }
451
        }
452
      }
453
    }
454
455
    // These are no longer used, and the ExprManager would have
456
    // complained of a bad substitution if anything is left unresolved.
457
    // Clear out the set.
458
882
    d_unresolved.clear();
459
460
    // throw exception if any datatype is not well-founded
461
2036
    for (unsigned i = 0; i < datatypes.size(); ++i) {
462
2308
      const api::Datatype& dt = types[i].getDatatype();
463
1154
      if (!dt.isCodatatype() && !dt.isWellFounded()) {
464
        throw ParserException(dt.getName() + " is not well-founded");
465
      }
466
    }
467
1764
    return types;
468
  } catch (IllegalArgumentException& ie) {
469
    throw ParserException(ie.getMessage());
470
  }
471
}
472
473
3663
api::Sort Parser::mkFlatFunctionType(std::vector<api::Sort>& sorts,
474
                                     api::Sort range,
475
                                     std::vector<api::Term>& flattenVars)
476
{
477
3663
  if (range.isFunction())
478
  {
479
24
    std::vector<api::Sort> domainTypes = range.getFunctionDomainSorts();
480
27
    for (unsigned i = 0, size = domainTypes.size(); i < size; i++)
481
    {
482
15
      sorts.push_back(domainTypes[i]);
483
      // the introduced variable is internal (not parsable)
484
30
      std::stringstream ss;
485
15
      ss << "__flatten_var_" << i;
486
30
      api::Term v = d_solver->mkVar(domainTypes[i], ss.str());
487
15
      flattenVars.push_back(v);
488
    }
489
12
    range = range.getFunctionCodomainSort();
490
  }
491
3663
  if (sorts.empty())
492
  {
493
2100
    return range;
494
  }
495
1563
  return d_solver->mkFunctionSort(sorts, range);
496
}
497
498
18631
api::Sort Parser::mkFlatFunctionType(std::vector<api::Sort>& sorts,
499
                                     api::Sort range)
500
{
501
18631
  if (sorts.empty())
502
  {
503
    // no difference
504
1182
    return range;
505
  }
506
17449
  if (Debug.isOn("parser"))
507
  {
508
    Debug("parser") << "mkFlatFunctionType: range " << range << " and domains ";
509
    for (api::Sort t : sorts)
510
    {
511
      Debug("parser") << " " << t;
512
    }
513
    Debug("parser") << "\n";
514
  }
515
17651
  while (range.isFunction())
516
  {
517
202
    std::vector<api::Sort> domainTypes = range.getFunctionDomainSorts();
518
101
    sorts.insert(sorts.end(), domainTypes.begin(), domainTypes.end());
519
101
    range = range.getFunctionCodomainSort();
520
  }
521
17449
  return d_solver->mkFunctionSort(sorts, range);
522
}
523
524
12
api::Term Parser::mkHoApply(api::Term expr, const std::vector<api::Term>& args)
525
{
526
27
  for (unsigned i = 0; i < args.size(); i++)
527
  {
528
15
    expr = d_solver->mkTerm(api::HO_APPLY, expr, args[i]);
529
  }
530
12
  return expr;
531
}
532
533
384
api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
534
{
535
384
  api::Kind k = t.getKind();
536
384
  if (k == api::EMPTYSET)
537
  {
538
143
    t = d_solver->mkEmptySet(s);
539
  }
540
241
  else if (k == api::EMPTYBAG)
541
  {
542
16
    t = d_solver->mkEmptyBag(s);
543
  }
544
225
  else if (k == api::CONST_SEQUENCE)
545
  {
546
9
    if (!s.isSequence())
547
    {
548
      std::stringstream ss;
549
      ss << "Type ascription on empty sequence must be a sequence, got " << s;
550
      parseError(ss.str());
551
    }
552
9
    if (!t.getConstSequenceElements().empty())
553
    {
554
      std::stringstream ss;
555
      ss << "Cannot apply a type ascription to a non-empty sequence";
556
      parseError(ss.str());
557
    }
558
9
    t = d_solver->mkEmptySequence(s.getSequenceElementSort());
559
  }
560
216
  else if (k == api::UNIVERSE_SET)
561
  {
562
87
    t = d_solver->mkUniverseSet(s);
563
  }
564
129
  else if (k == api::SEP_NIL)
565
  {
566
43
    t = d_solver->mkSepNil(s);
567
  }
568
86
  else if (k == api::APPLY_CONSTRUCTOR)
569
  {
570
80
    std::vector<api::Term> children(t.begin(), t.end());
571
    // apply type ascription to the operator and reconstruct
572
40
    children[0] = applyTypeAscription(children[0], s);
573
40
    t = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, children);
574
  }
575
  // !!! temporary until datatypes are refactored in the new API
576
768
  api::Sort etype = t.getSort();
577
384
  if (etype.isConstructor())
578
  {
579
    // Type ascriptions only have an effect on the node structure if this is a
580
    // parametric datatype.
581
42
    if (s.isParametricDatatype())
582
    {
583
      // get the datatype that t belongs to
584
72
      api::Sort etyped = etype.getConstructorCodomainSort();
585
72
      api::Datatype d = etyped.getDatatype();
586
      // lookup by name
587
72
      api::DatatypeConstructor dc = d.getConstructor(t.toString());
588
      // ask the constructor for the specialized constructor term
589
36
      t = dc.getSpecializedConstructorTerm(s);
590
    }
591
    // the type of t does not match the sort s by design (constructor type
592
    // vs datatype type), thus we use an alternative check here.
593
42
    if (t.getSort().getConstructorCodomainSort() != s)
594
    {
595
      std::stringstream ss;
596
      ss << "Type ascription on constructor not satisfied, term " << t
597
         << " expected sort " << s << " but has sort "
598
         << t.getSort().getConstructorCodomainSort();
599
      parseError(ss.str());
600
    }
601
42
    return t;
602
  }
603
  // otherwise, nothing to do
604
  // check that the type is correct
605
342
  if (t.getSort() != s)
606
  {
607
    std::stringstream ss;
608
    ss << "Type ascription not satisfied, term " << t << " expected sort " << s
609
       << " but has sort " << t.getSort();
610
    parseError(ss.str());
611
  }
612
342
  return t;
613
}
614
615
15850207
bool Parser::isDeclared(const std::string& name, SymbolType type) {
616
15850207
  switch (type) {
617
15225734
    case SYM_VARIABLE: return d_symtab->isBound(name);
618
624473
    case SYM_SORT:
619
624473
      return d_symtab->isBoundType(name);
620
  }
621
  Assert(false);  // Unhandled(type);
622
  return false;
623
}
624
625
11653924
void Parser::checkDeclaration(const std::string& varName,
626
                              DeclarationCheck check,
627
                              SymbolType type,
628
                              std::string notes)
629
{
630
11653924
  if (!d_checksEnabled) {
631
    return;
632
  }
633
634
11653924
  switch (check) {
635
4445628
    case CHECK_DECLARED:
636
4445628
      if (!isDeclared(varName, type)) {
637
87
        parseError("Symbol '" + varName + "' not declared as a " +
638
58
                   (type == SYM_VARIABLE ? "variable" : "type") +
639
58
                   (notes.size() == 0 ? notes : "\n" + notes));
640
      }
641
4445599
      break;
642
643
11165
    case CHECK_UNDECLARED:
644
11165
      if (isDeclared(varName, type)) {
645
30
        parseError("Symbol '" + varName + "' previously declared as a " +
646
20
                   (type == SYM_VARIABLE ? "variable" : "type") +
647
20
                   (notes.size() == 0 ? notes : "\n" + notes));
648
      }
649
11155
      break;
650
651
7197131
    case CHECK_NONE:
652
7197131
      break;
653
654
    default: Assert(false);  // Unhandled(check);
655
  }
656
}
657
658
324381
void Parser::checkFunctionLike(api::Term fun)
659
{
660
324381
  if (d_checksEnabled && !isFunctionLike(fun)) {
661
8
    stringstream ss;
662
4
    ss << "Expecting function-like symbol, found '";
663
4
    ss << fun;
664
4
    ss << "'";
665
8
    parseError(ss.str());
666
  }
667
324377
}
668
669
417543
void Parser::addOperator(api::Kind kind) { d_logicOperators.insert(kind); }
670
671
399
void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); }
672
281021
Command* Parser::nextCommand()
673
{
674
281021
  Debug("parser") << "nextCommand()" << std::endl;
675
281021
  Command* cmd = NULL;
676
281021
  if (!d_commandQueue.empty()) {
677
394
    cmd = d_commandQueue.front();
678
394
    d_commandQueue.pop_front();
679
394
    setDone(cmd == NULL);
680
  } else {
681
    try {
682
280627
      cmd = d_input->parseCommand();
683
280546
      d_commandQueue.push_back(cmd);
684
280546
      cmd = d_commandQueue.front();
685
280546
      d_commandQueue.pop_front();
686
280546
      setDone(cmd == NULL);
687
154
    } catch (ParserException& e) {
688
77
      setDone();
689
77
      throw;
690
8
    } catch (exception& e) {
691
4
      setDone();
692
8
      parseError(e.what());
693
    }
694
  }
695
280940
  Debug("parser") << "nextCommand() => " << cmd << std::endl;
696
280940
  return cmd;
697
}
698
699
176
api::Term Parser::nextExpression()
700
{
701
176
  Debug("parser") << "nextExpression()" << std::endl;
702
176
  api::Term result;
703
176
  if (!done()) {
704
    try {
705
176
      result = d_input->parseExpr();
706
134
      setDone(result.isNull());
707
84
    } catch (ParserException& e) {
708
42
      setDone();
709
42
      throw;
710
    } catch (exception& e) {
711
      setDone();
712
      parseError(e.what());
713
    }
714
  }
715
134
  Debug("parser") << "nextExpression() => " << result << std::endl;
716
134
  return result;
717
}
718
719
32
void Parser::attributeNotSupported(const std::string& attr) {
720
32
  if (d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) {
721
16
    stringstream ss;
722
    ss << "warning: Attribute '" << attr
723
8
       << "' not supported (ignoring this and all following uses)";
724
8
    d_input->warning(ss.str());
725
8
    d_attributesWarnedAbout.insert(attr);
726
  }
727
32
}
728
729
2115
size_t Parser::scopeLevel() const { return d_symman->scopeLevel(); }
730
731
102304
void Parser::pushScope(bool isUserContext)
732
{
733
102304
  d_symman->pushScope(isUserContext);
734
102304
}
735
736
101862
void Parser::popScope()
737
{
738
101862
  d_symman->popScope();
739
101862
}
740
741
6
void Parser::reset() {}
742
743
12886
SymbolManager* Parser::getSymbolManager() { return d_symman; }
744
745
13000
std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
746
{
747
26000
  std::wstring ws;
748
  {
749
13000
    std::setlocale(LC_ALL, "en_US.utf8");
750
13000
    std::mbtowc(nullptr, nullptr, 0);
751
13000
    const char* end = s.data() + s.size();
752
13000
    const char* ptr = s.data();
753
274010
    for (wchar_t c; ptr != end; ) {
754
130505
      int res = std::mbtowc(&c, ptr, end - ptr);
755
130505
      if (res == -1) {
756
        std::cerr << "Invalid escape sequence in " << s << std::endl;
757
        break;
758
130505
      } else if (res == 0) {
759
        break;
760
      } else {
761
130505
        ws += c;
762
130505
        ptr += res;
763
      }
764
    }
765
  }
766
767
13000
  std::vector<unsigned> str;
768
13000
  unsigned i = 0;
769
274010
  while (i < ws.size())
770
  {
771
    // get the current character
772
261010
    if (ws[i] != '\\')
773
    {
774
      // don't worry about printable here
775
130505
      str.push_back(static_cast<unsigned>(ws[i]));
776
130505
      ++i;
777
130505
      continue;
778
    }
779
    // slash is always escaped
780
    ++i;
781
    if (i >= ws.size())
782
    {
783
      // slash cannot be the last character if we are parsing escape sequences
784
      std::stringstream serr;
785
      serr << "Escape sequence at the end of string: \"" << s
786
           << "\" should be handled by lexer";
787
      parseError(serr.str());
788
    }
789
    switch (ws[i])
790
    {
791
      case 'n':
792
      {
793
        str.push_back(static_cast<unsigned>('\n'));
794
        i++;
795
      }
796
      break;
797
      case 't':
798
      {
799
        str.push_back(static_cast<unsigned>('\t'));
800
        i++;
801
      }
802
      break;
803
      case 'v':
804
      {
805
        str.push_back(static_cast<unsigned>('\v'));
806
        i++;
807
      }
808
      break;
809
      case 'b':
810
      {
811
        str.push_back(static_cast<unsigned>('\b'));
812
        i++;
813
      }
814
      break;
815
      case 'r':
816
      {
817
        str.push_back(static_cast<unsigned>('\r'));
818
        i++;
819
      }
820
      break;
821
      case 'f':
822
      {
823
        str.push_back(static_cast<unsigned>('\f'));
824
        i++;
825
      }
826
      break;
827
      case 'a':
828
      {
829
        str.push_back(static_cast<unsigned>('\a'));
830
        i++;
831
      }
832
      break;
833
      case '\\':
834
      {
835
        str.push_back(static_cast<unsigned>('\\'));
836
        i++;
837
      }
838
      break;
839
      case 'x':
840
      {
841
        bool isValid = false;
842
        if (i + 2 < ws.size())
843
        {
844
          if (std::isxdigit(ws[i + 1]) && std::isxdigit(ws[i + 2]))
845
          {
846
            std::wstringstream shex;
847
            shex << ws[i + 1] << ws[i + 2];
848
            unsigned val;
849
            shex >> std::hex >> val;
850
            str.push_back(val);
851
            i += 3;
852
            isValid = true;
853
          }
854
        }
855
        if (!isValid)
856
        {
857
          std::stringstream serr;
858
          serr << "Illegal String Literal: \"" << s
859
               << "\", must have two digits after \\x";
860
          parseError(serr.str());
861
        }
862
      }
863
      break;
864
      default:
865
      {
866
        if (std::isdigit(ws[i]))
867
        {
868
          // octal escape sequences  TODO : revisit (issue #1251).
869
          unsigned num = static_cast<unsigned>(ws[i]) - 48;
870
          bool flag = num < 4;
871
          if (i + 1 < ws.size() && num < 8 && std::isdigit(ws[i + 1])
872
              && ws[i + 1] < '8')
873
          {
874
            num = num * 8 + static_cast<unsigned>(ws[i + 1]) - 48;
875
            if (flag && i + 2 < ws.size() && std::isdigit(ws[i + 2])
876
                && ws[i + 2] < '8')
877
            {
878
              num = num * 8 + static_cast<unsigned>(ws[i + 2]) - 48;
879
              str.push_back(num);
880
              i += 3;
881
            }
882
            else
883
            {
884
              str.push_back(num);
885
              i += 2;
886
            }
887
          }
888
          else
889
          {
890
            str.push_back(num);
891
            i++;
892
          }
893
        }
894
      }
895
    }
896
  }
897
26000
  return str;
898
}
899
900
8841
api::Term Parser::mkStringConstant(const std::string& s)
901
{
902
8841
  if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage()))
903
  {
904
7884
    return d_solver->mkString(s, true);
905
  }
906
  // otherwise, we must process ad-hoc escape sequences
907
1914
  std::vector<unsigned> str = processAdHocStringEsc(s);
908
957
  return d_solver->mkString(str);
909
}
910
911
} /* CVC4::parser namespace */
912
26664
} /* CVC4 namespace */