GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/parser/parser.h Lines: 25 35 71.4 %
Date: 2021-03-22 Branches: 2 8 25.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file parser.h
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 A collection of state for use by parser implementations.
13
 **
14
 ** A collection of state for use by parser implementations.
15
 **/
16
17
#include "cvc4parser_public.h"
18
19
#ifndef CVC4__PARSER__PARSER_H
20
#define CVC4__PARSER__PARSER_H
21
22
#include <list>
23
#include <set>
24
#include <string>
25
26
#include "api/cvc4cpp.h"
27
#include "cvc4_export.h"
28
#include "expr/kind.h"
29
#include "expr/symbol_manager.h"
30
#include "expr/symbol_table.h"
31
#include "parser/input.h"
32
#include "parser/parse_op.h"
33
#include "parser/parser_exception.h"
34
#include "util/unsafe_interrupt_exception.h"
35
36
namespace CVC4 {
37
38
// Forward declarations
39
class Command;
40
class ResourceManager;
41
42
namespace parser {
43
44
class Input;
45
46
/** Types of checks for the symbols */
47
enum DeclarationCheck {
48
  /** Enforce that the symbol has been declared */
49
  CHECK_DECLARED,
50
  /** Enforce that the symbol has not been declared */
51
  CHECK_UNDECLARED,
52
  /** Don't check anything */
53
  CHECK_NONE
54
};/* enum DeclarationCheck */
55
56
/**
57
 * Returns a string representation of the given object (for
58
 * debugging).
59
 */
60
inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check);
61
inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) {
62
  switch(check) {
63
  case CHECK_NONE:
64
    return out << "CHECK_NONE";
65
  case CHECK_DECLARED:
66
    return out << "CHECK_DECLARED";
67
  case CHECK_UNDECLARED:
68
    return out << "CHECK_UNDECLARED";
69
  default:
70
    return out << "DeclarationCheck!UNKNOWN";
71
  }
72
}
73
74
/**
75
 * Types of symbols. Used to define namespaces.
76
 */
77
enum SymbolType {
78
  /** Variables */
79
  SYM_VARIABLE,
80
  /** Sorts */
81
  SYM_SORT
82
};/* enum SymbolType */
83
84
/**
85
 * Returns a string representation of the given object (for
86
 * debugging).
87
 */
88
inline std::ostream& operator<<(std::ostream& out, SymbolType type);
89
inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
90
  switch(type) {
91
  case SYM_VARIABLE:
92
    return out << "SYM_VARIABLE";
93
  case SYM_SORT:
94
    return out << "SYM_SORT";
95
  default:
96
    return out << "SymbolType!UNKNOWN";
97
  }
98
}
99
100
/**
101
 * This class encapsulates all of the state of a parser, including the
102
 * name of the file, line number and column information, and in-scope
103
 * declarations.
104
 */
105
class CVC4_EXPORT Parser
106
{
107
  friend class ParserBuilder;
108
private:
109
110
 /** The input that we're parsing. */
111
 Input* d_input;
112
113
 /**
114
  * Reference to the symbol manager, which manages the symbol table used by
115
  * this parser.
116
  */
117
 SymbolManager* d_symman;
118
119
 /**
120
  * This current symbol table used by this parser, from symbol manager.
121
  */
122
 SymbolTable* d_symtab;
123
124
 /**
125
  * The level of the assertions in the declaration scope.  Things declared
126
  * after this level are bindings from e.g. a let, a quantifier, or a
127
  * lambda.
128
  */
129
 size_t d_assertionLevel;
130
131
 /** How many anonymous functions we've created. */
132
 size_t d_anonymousFunctionCount;
133
134
 /** Are we done */
135
 bool d_done;
136
137
 /** Are semantic checks enabled during parsing? */
138
 bool d_checksEnabled;
139
140
 /** Are we parsing in strict mode? */
141
 bool d_strictMode;
142
143
 /** Are we only parsing? */
144
 bool d_parseOnly;
145
146
 /**
147
  * Can we include files?  (Set to false for security purposes in
148
  * e.g. the online version.)
149
  */
150
 bool d_canIncludeFile;
151
152
 /**
153
  * Whether the logic has been forced with --force-logic.
154
  */
155
 bool d_logicIsForced;
156
157
 /**
158
  * The logic, if d_logicIsForced == true.
159
  */
160
 std::string d_forcedLogic;
161
162
 /** The set of operators available in the current logic. */
163
 std::set<api::Kind> d_logicOperators;
164
165
 /** The set of attributes already warned about. */
166
 std::set<std::string> d_attributesWarnedAbout;
167
168
 /**
169
  * The current set of unresolved types.  We can get by with this NOT
170
  * being on the scope, because we can only have one DATATYPE
171
  * definition going on at one time.  This is a bit hackish; we
172
  * depend on mkMutualDatatypeTypes() to check everything and clear
173
  * this out.
174
  */
175
 std::set<api::Sort> d_unresolved;
176
177
 /**
178
  * "Preemption commands": extra commands implied by subterms that
179
  * should be issued before the currently-being-parsed command is
180
  * issued.  Used to support SMT-LIBv2 ":named" attribute on terms.
181
  *
182
  * Owns the memory of the Commands in the queue.
183
  */
184
 std::list<Command*> d_commandQueue;
185
186
 /** Lookup a symbol in the given namespace (as specified by the type).
187
  * Only returns a symbol if it is not overloaded, returns null otherwise.
188
  */
189
 api::Term getSymbol(const std::string& var_name, SymbolType type);
190
191
protected:
192
 /** The API Solver object. */
193
 api::Solver* d_solver;
194
195
 /**
196
  * Create a parser state.
197
  *
198
  * @attention The parser takes "ownership" of the given
199
  * input and will delete it on destruction.
200
  *
201
  * @param solver solver API object
202
  * @param symm reference to the symbol manager
203
  * @param input the parser input
204
  * @param strictMode whether to incorporate strict(er) compliance checks
205
  * @param parseOnly whether we are parsing only (and therefore certain checks
206
  * need not be performed, like those about unimplemented features, @see
207
  * unimplementedFeature())
208
  */
209
 Parser(api::Solver* solver,
210
        SymbolManager* sm,
211
        Input* input,
212
        bool strictMode = false,
213
        bool parseOnly = false);
214
215
public:
216
217
  virtual ~Parser();
218
219
  /** Get the associated solver. */
220
  api::Solver* getSolver() const;
221
222
  /** Get the associated input. */
223
97
  inline Input* getInput() const {
224
97
    return d_input;
225
  }
226
227
  /** Get unresolved sorts */
228
  inline std::set<api::Sort>& getUnresolvedSorts() { return d_unresolved; }
229
230
  /** Deletes and replaces the current parser input. */
231
40
  void setInput(Input* input)  {
232
40
    delete d_input;
233
40
    d_input = input;
234
40
    d_input->setParser(*this);
235
40
    d_done = false;
236
40
  }
237
238
  /**
239
   * Check if we are done -- either the end of input has been reached, or some
240
   * error has been encountered.
241
   * @return true if parser is done
242
   */
243
488
  inline bool done() const {
244
488
    return d_done;
245
  }
246
247
  /** Sets the done flag */
248
281197
  inline void setDone(bool done = true) {
249
281197
    d_done = done;
250
281197
  }
251
252
  /** Enable semantic checks during parsing. */
253
5724
  void enableChecks() { d_checksEnabled = true; }
254
255
  /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
256
  void disableChecks() { d_checksEnabled = false; }
257
258
  /** Enable strict parsing, according to the language standards. */
259
  void enableStrictMode() { d_strictMode = true; }
260
261
  /** Disable strict parsing. Allows certain syntactic infelicities to
262
      pass without comment. */
263
  void disableStrictMode() { d_strictMode = false; }
264
265
4022052
  bool strictModeEnabled() { return d_strictMode; }
266
267
5724
  void allowIncludeFile() { d_canIncludeFile = true; }
268
  void disallowIncludeFile() { d_canIncludeFile = false; }
269
7
  bool canIncludeFile() const { return d_canIncludeFile; }
270
271
  /** Expose the functionality from SMT/SMT2 parsers, while making
272
      implementation optional by returning false by default. */
273
  virtual bool logicIsSet() { return false; }
274
275
  virtual void forceLogic(const std::string& logic);
276
277
8
  const std::string& getForcedLogic() const { return d_forcedLogic; }
278
4964
  bool logicIsForced() const { return d_logicIsForced; }
279
280
  /**
281
   * Gets the variable currently bound to name.
282
   *
283
   * @param name the name of the variable
284
   * @return the variable expression
285
   * Only returns a variable if its name is not overloaded, returns null otherwise.
286
   */
287
  api::Term getVariable(const std::string& name);
288
289
  /**
290
   * Gets the function currently bound to name.
291
   *
292
   * @param name the name of the variable
293
   * @return the variable expression
294
   * Only returns a function if its name is not overloaded, returns null otherwise.
295
   */
296
  api::Term getFunction(const std::string& name);
297
298
  /**
299
   * Returns the expression that name should be interpreted as, based on the current binding.
300
   *
301
   * The symbol name should be declared.
302
   * This creates the expression that the string "name" should be interpreted as.
303
   * Typically this corresponds to a variable, but it may also correspond to
304
   * a nullary constructor or a defined function.
305
   * Only returns an expression if its name is not overloaded, returns null otherwise.
306
   */
307
  virtual api::Term getExpressionForName(const std::string& name);
308
309
  /**
310
   * Returns the expression that name should be interpreted as, based on the current binding.
311
   *
312
   * This is the same as above but where the name has been type cast to t.
313
   */
314
  virtual api::Term getExpressionForNameAndType(const std::string& name,
315
                                                api::Sort t);
316
317
  /**
318
   * If this method returns true, then name is updated with the tester name
319
   * for constructor cons.
320
   *
321
   * In detail, notice that (user-defined) datatypes associate a unary predicate
322
   * for each constructor, called its "tester". This symbol is automatically
323
   * defined when a datatype is defined. The tester name for a constructor
324
   * (e.g. "cons") depends on the language:
325
   * - In smt versions < 2.6, the (non-standard) syntax is "is-cons",
326
   * - In smt versions >= 2.6, the indexed symbol "(_ is cons)" is used. Thus,
327
   * no tester symbol is necessary, since "is" is a builtin symbol. We still use
328
   * the above syntax if strict mode is disabled.
329
   * - In cvc, the syntax for testers is "is_cons".
330
   */
331
  virtual bool getTesterName(api::Term cons, std::string& name);
332
333
  /**
334
   * Returns the kind that should be used for applications of expression fun.
335
   * This is a generalization of ExprManager::operatorToKind that also
336
   * handles variables whose types are "function-like", i.e. where
337
   * checkFunctionLike(fun) returns true.
338
   *
339
   * For examples of the latter, this function returns
340
   *   APPLY_UF if fun has function type,
341
   *   APPLY_CONSTRUCTOR if fun has constructor type.
342
   */
343
  api::Kind getKindForFunction(api::Term fun);
344
345
  /**
346
   * Returns a sort, given a name.
347
   * @param sort_name the name to look up
348
   */
349
  api::Sort getSort(const std::string& sort_name);
350
351
  /**
352
   * Returns a (parameterized) sort, given a name and args.
353
   */
354
  api::Sort getSort(const std::string& sort_name,
355
                    const std::vector<api::Sort>& params);
356
357
  /**
358
   * Returns arity of a (parameterized) sort, given a name and args.
359
   */
360
  size_t getArity(const std::string& sort_name);
361
362
  /**
363
   * Checks if a symbol has been declared.
364
   * @param name the symbol name
365
   * @param type the symbol type
366
   * @return true iff the symbol has been declared with the given type
367
   */
368
  bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
369
370
  /**
371
   * Checks if the declaration policy we want to enforce holds
372
   * for the given symbol.
373
   * @param name the symbol to check
374
   * @param check the kind of check to perform
375
   * @param type the type of the symbol
376
   * @param notes notes to add to a parse error (if one is generated)
377
   * @throws ParserException if checks are enabled and the check fails
378
   */
379
  void checkDeclaration(const std::string& name,
380
                        DeclarationCheck check,
381
                        SymbolType type = SYM_VARIABLE,
382
                        std::string notes = "");
383
384
  /**
385
   * Checks whether the given expression is function-like, i.e.
386
   * it expects arguments. This is checked by looking at the type
387
   * of fun. Examples of function types are function, constructor,
388
   * selector, tester.
389
   * @param fun the expression to check
390
   * @throws ParserException if checks are enabled and fun is not
391
   * a function
392
   */
393
  void checkFunctionLike(api::Term fun);
394
395
  /** Create a new CVC4 variable expression of the given type.
396
   *
397
   * It is inserted at context level zero in the symbol table if levelZero is
398
   * true, or if we are using global declarations.
399
   *
400
   * If a symbol with name already exists,
401
   *  then if doOverload is true, we create overloaded operators.
402
   *  else if doOverload is false, the existing expression is shadowed by the
403
   * new expression.
404
   */
405
  api::Term bindVar(const std::string& name,
406
                    const api::Sort& type,
407
                    bool levelZero = false,
408
                    bool doOverload = false);
409
410
  /**
411
   * Create a set of new CVC4 variable expressions of the given type.
412
   *
413
   * It is inserted at context level zero in the symbol table if levelZero is
414
   * true, or if we are using global declarations.
415
   *
416
   * For each name, if a symbol with name already exists,
417
   *  then if doOverload is true, we create overloaded operators.
418
   *  else if doOverload is false, the existing expression is shadowed by the
419
   * new expression.
420
   */
421
  std::vector<api::Term> bindVars(const std::vector<std::string> names,
422
                                  const api::Sort& type,
423
                                  bool levelZero = false,
424
                                  bool doOverload = false);
425
426
  /**
427
   * Create a new CVC4 bound variable expression of the given type. This binds
428
   * the symbol name to that variable in the current scope.
429
   */
430
  api::Term bindBoundVar(const std::string& name, const api::Sort& type);
431
  /**
432
   * Create a new CVC4 bound variable expressions of the given names and types.
433
   * Like the method above, this binds these names to those variables in the
434
   * current scope.
435
   */
436
  std::vector<api::Term> bindBoundVars(
437
      std::vector<std::pair<std::string, api::Sort> >& sortedVarNames);
438
439
  /**
440
   * Create a set of new CVC4 bound variable expressions of the given type.
441
   *
442
   * For each name, if a symbol with name already exists,
443
   *  then if doOverload is true, we create overloaded operators.
444
   *  else if doOverload is false, the existing expression is shadowed by the new expression.
445
   */
446
  std::vector<api::Term> bindBoundVars(const std::vector<std::string> names,
447
                                       const api::Sort& type);
448
449
  /** Create a new variable definition (e.g., from a let binding).
450
   * levelZero is set if the binding must be done at level 0.
451
   * If a symbol with name already exists,
452
   *  then if doOverload is true, we create overloaded operators.
453
   *  else if doOverload is false, the existing expression is shadowed by the new expression.
454
   */
455
  void defineVar(const std::string& name,
456
                 const api::Term& val,
457
                 bool levelZero = false,
458
                 bool doOverload = false);
459
460
  /**
461
   * Create a new type definition.
462
   *
463
   * @param name The name of the type
464
   * @param type The type that should be associated with the name
465
   * @param levelZero If true, the type definition is considered global and
466
   *                  cannot be removed by popping the user context
467
   * @param skipExisting If true, the type definition is ignored if the same
468
   *                     symbol has already been defined. It is assumed that
469
   *                     the definition is the exact same as the existing one.
470
   */
471
  void defineType(const std::string& name,
472
                  const api::Sort& type,
473
                  bool levelZero = false,
474
                  bool skipExisting = false);
475
476
  /**
477
   * Create a new (parameterized) type definition.
478
   *
479
   * @param name The name of the type
480
   * @param params The type parameters
481
   * @param type The type that should be associated with the name
482
   * @param levelZero If true, the type definition is considered global and
483
   *                  cannot be removed by poppoing the user context
484
   */
485
  void defineType(const std::string& name,
486
                  const std::vector<api::Sort>& params,
487
                  const api::Sort& type,
488
                  bool levelZero = false);
489
490
  /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
491
  void defineParameterizedType(const std::string& name,
492
                               const std::vector<api::Sort>& params,
493
                               const api::Sort& type);
494
495
  /**
496
   * Creates a new sort with the given name.
497
   */
498
  api::Sort mkSort(const std::string& name);
499
500
  /**
501
   * Creates a new sort constructor with the given name and arity.
502
   */
503
  api::Sort mkSortConstructor(const std::string& name, size_t arity);
504
505
  /**
506
   * Creates a new "unresolved type," used only during parsing.
507
   */
508
  api::Sort mkUnresolvedType(const std::string& name);
509
510
  /**
511
   * Creates a new unresolved (parameterized) type constructor of the given
512
   * arity.
513
   */
514
  api::Sort mkUnresolvedTypeConstructor(const std::string& name, size_t arity);
515
  /**
516
   * Creates a new unresolved (parameterized) type constructor given the type
517
   * parameters.
518
   */
519
  api::Sort mkUnresolvedTypeConstructor(const std::string& name,
520
                                        const std::vector<api::Sort>& params);
521
522
  /**
523
   * Creates a new unresolved (parameterized) type constructor of the given
524
   * arity. Calls either mkUnresolvedType or mkUnresolvedTypeConstructor
525
   * depending on the arity.
526
   */
527
  api::Sort mkUnresolvedType(const std::string& name, size_t arity);
528
529
  /**
530
   * Returns true IFF name is an unresolved type.
531
   */
532
  bool isUnresolvedType(const std::string& name);
533
534
  /**
535
   * Creates and binds sorts of a list of mutually-recursive datatype
536
   * declarations.
537
   *
538
   * For each symbol defined by the datatype, if a symbol with name already
539
   * exists, then if doOverload is true, we create overloaded operators. Else, if
540
   * doOverload is false, the existing expression is shadowed by the new
541
   * expression.
542
   */
543
  std::vector<api::Sort> bindMutualDatatypeTypes(
544
      std::vector<api::DatatypeDecl>& datatypes, bool doOverload = false);
545
546
  /** make flat function type
547
   *
548
   * Returns the "flat" function type corresponding to the function taking
549
   * argument types "sorts" and range type "range".  A flat function type is
550
   * one whose range is not a function. Notice that if sorts is empty and range
551
   * is not a function, then this function returns range itself.
552
   *
553
   * If range is a function type, we add its function argument sorts to sorts
554
   * and consider its function range as the new range. For each sort S added
555
   * to sorts in this process, we add a new bound variable of sort S to
556
   * flattenVars.
557
   *
558
   * For example:
559
   * mkFlattenFunctionType( { Int, (-> Real Real) }, (-> Int Bool), {} ):
560
   * - returns the the function type (-> Int (-> Real Real) Int Bool)
561
   * - updates sorts to { Int, (-> Real Real), Int },
562
   * - updates flattenVars to { x }, where x is bound variable of type Int.
563
   *
564
   * Notice that this method performs only one level of flattening, for example,
565
   * mkFlattenFunctionType({ Int, (-> Real Real) }, (-> Int (-> Int Bool)), {}):
566
   * - returns the the function type (-> Int (-> Real Real) Int (-> Int Bool))
567
   * - updates sorts to { Int, (-> Real Real), Int },
568
   * - updates flattenVars to { x }, where x is bound variable of type Int.
569
   *
570
   * This method is required so that we do not return functions
571
   * that have function return type (these give an unhandled exception
572
   * in the ExprManager). For examples of the equivalence between function
573
   * definitions in the proposed higher-order extension of the smt2 language,
574
   * see page 3 of http://matryoshka.gforge.inria.fr/pubs/PxTP2017.pdf.
575
   *
576
   * The argument flattenVars is needed in the case of defined functions
577
   * with function return type. These have implicit arguments, for instance:
578
   *    (define-fun Q ((x Int)) (-> Int Int) (lambda y (P x)))
579
   * is equivalent to the command:
580
   *    (define-fun Q ((x Int) (z Int)) Int (@ (lambda y (P x)) z))
581
   * where @ is (higher-order) application. In this example, z is added to
582
   * flattenVars.
583
   */
584
  api::Sort mkFlatFunctionType(std::vector<api::Sort>& sorts,
585
                               api::Sort range,
586
                               std::vector<api::Term>& flattenVars);
587
588
  /** make flat function type
589
   *
590
   * Same as above, but does not take argument flattenVars.
591
   * This is used when the arguments of the function are not important (for
592
   * instance, if we are only using this type in a declare-fun).
593
   */
594
  api::Sort mkFlatFunctionType(std::vector<api::Sort>& sorts, api::Sort range);
595
596
  /** make higher-order apply
597
   *
598
   * This returns the left-associative curried application of (function) expr to
599
   * the arguments in args.
600
   *
601
   * For example, mkHoApply( f, { a, b }, 0 ) returns
602
   *  (HO_APPLY (HO_APPLY f a) b)
603
   *
604
   * If args is non-empty, the expected type of expr is (-> T0 ... Tn T), where
605
   *    args[i].getType() = Ti
606
   * for each i where 0 <= i < args.size(). If expr is not of this
607
   * type, the expression returned by this method will not be well typed.
608
   */
609
  api::Term mkHoApply(api::Term expr, const std::vector<api::Term>& args);
610
611
  /** Apply type ascription
612
   *
613
   * Return term t with a type ascription applied to it. This is used for
614
   * syntax like (as t T) in smt2 and t::T in the CVC language. This includes:
615
   * - (as emptyset (Set T))
616
   * - (as emptybag (Bag T))
617
   * - (as univset (Set T))
618
   * - (as sep.nil T)
619
   * - (cons T)
620
   * - ((as cons T) t1 ... tn) where cons is a parametric datatype constructor.
621
   *
622
   * The term to ascribe t is a term whose kind and children (but not type)
623
   * are equivalent to that of the term returned by this method.
624
   *
625
   * Notice that method is not necessarily a cast. In actuality, the above terms
626
   * should be understood as symbols indexed by types. However, SMT-LIB does not
627
   * permit types as indices, so we must use, e.g. (as emptyset (Set T))
628
   * instead of (_ emptyset (Set T)).
629
   *
630
   * @param t The term to ascribe a type
631
   * @param s The sort to ascribe
632
   * @return Term t with sort s ascribed.
633
   */
634
  api::Term applyTypeAscription(api::Term t, api::Sort s);
635
636
  /**
637
   * Add an operator to the current legal set.
638
   *
639
   * @param kind the built-in operator to add
640
   */
641
  void addOperator(api::Kind kind);
642
643
  /**
644
   * Preempt the next returned command with other ones; used to
645
   * support the :named attribute in SMT-LIBv2, which implicitly
646
   * inserts a new command before the current one. Also used in TPTP
647
   * because function and predicate symbols are implicitly declared.
648
   */
649
  void preemptCommand(Command* cmd);
650
651
  /** Is the symbol bound to a boolean variable? */
652
  bool isBoolean(const std::string& name);
653
654
  /** Is fun a function (or function-like thing)?
655
  * Currently this means its type is either a function, constructor, tester, or selector.
656
  */
657
  bool isFunctionLike(api::Term fun);
658
659
  /** Is the symbol bound to a predicate? */
660
  bool isPredicate(const std::string& name);
661
662
  /** Parse and return the next command. */
663
  Command* nextCommand();
664
665
  /** Parse and return the next expression. */
666
  api::Term nextExpression();
667
668
  /** Issue a warning to the user. */
669
136
  void warning(const std::string& msg) { d_input->warning(msg); }
670
  /** Issue a warning to the user, but only once per attribute. */
671
  void attributeNotSupported(const std::string& attr);
672
673
  /** Raise a parse error with the given message. */
674
74
  inline void parseError(const std::string& msg) { d_input->parseError(msg); }
675
  /** Unexpectedly encountered an EOF */
676
  inline void unexpectedEOF(const std::string& msg)
677
  {
678
    d_input->parseError(msg, true);
679
  }
680
681
  /**
682
   * If we are parsing only, don't raise an exception; if we are not,
683
   * raise a parse error with the given message.  There is no actual
684
   * parse error, everything is as expected, but we cannot create the
685
   * Expr, Type, or other requested thing yet due to internal
686
   * limitations.  Even though it's not a parse error, we throw a
687
   * parse error so that the input line and column information is
688
   * available.
689
   *
690
   * Think quantifiers.  We don't have a TheoryQuantifiers yet, so we
691
   * have no kind::FORALL or kind::EXISTS.  But we might want to
692
   * support parsing quantifiers (just not doing anything with them).
693
   * So this mechanism gives you a way to do it with --parse-only.
694
   */
695
  inline void unimplementedFeature(const std::string& msg)
696
  {
697
    if(!d_parseOnly) {
698
      parseError("Unimplemented feature: " + msg);
699
    }
700
  }
701
702
  /**
703
   * Gets the current declaration level.
704
   */
705
  size_t scopeLevel() const;
706
707
  /**
708
   * Pushes a scope. All subsequent symbol declarations made are only valid in
709
   * this scope, i.e. they are deleted on the next call to popScope.
710
   *
711
   * The argument isUserContext is true, when we are pushing a user context
712
   * e.g. via the smt2 command (push n). This may also include one initial
713
   * pushScope when the parser is initialized. User-context pushes and pops
714
   * have an impact on both expression names and the symbol table, whereas
715
   * other pushes and pops only have an impact on the symbol table.
716
   */
717
  void pushScope(bool isUserContext = false);
718
719
  void popScope();
720
721
  virtual void reset();
722
723
  /** Return the symbol manager used by this parser. */
724
  SymbolManager* getSymbolManager();
725
726
  //------------------------ operator overloading
727
  /** is this function overloaded? */
728
  bool isOverloadedFunction(api::Term fun)
729
  {
730
    return d_symtab->isOverloadedFunction(fun);
731
  }
732
733
  /** Get overloaded constant for type.
734
   * If possible, it returns a defined symbol with name
735
   * that has type t. Otherwise returns null expression.
736
  */
737
6
  api::Term getOverloadedConstantForType(const std::string& name, api::Sort t)
738
  {
739
6
    return d_symtab->getOverloadedConstantForType(name, t);
740
  }
741
742
  /**
743
   * If possible, returns a defined function for a name
744
   * and a vector of expected argument types. Otherwise returns
745
   * null expression.
746
   */
747
14
  api::Term getOverloadedFunctionForTypes(const std::string& name,
748
                                          std::vector<api::Sort>& argTypes)
749
  {
750
14
    return d_symtab->getOverloadedFunctionForTypes(name, argTypes);
751
  }
752
  //------------------------ end operator overloading
753
  /**
754
   * Make string constant
755
   *
756
   * This makes the string constant based on the string s. This may involve
757
   * processing ad-hoc escape sequences (if the language is not
758
   * SMT-LIB 2.6 or higher), or otherwise calling the solver to construct
759
   * the string.
760
   */
761
  api::Term mkStringConstant(const std::string& s);
762
763
  /** ad-hoc string escaping
764
   *
765
   * Returns the (internal) vector of code points corresponding to processing
766
   * the escape sequences in string s. This is to support string inputs that
767
   * do no comply with the SMT-LIB standard.
768
   *
769
   * This method handles escape sequences, including \n, \t, \v, \b, \r, \f, \a,
770
   * \\, \x[N] and octal escape sequences of the form \[c1]([c2]([c3])?)? where
771
   * c1, c2, c3 are digits from 0 to 7.
772
   */
773
  std::vector<unsigned> processAdHocStringEsc(const std::string& s);
774
}; /* class Parser */
775
776
}/* CVC4::parser namespace */
777
}/* CVC4 namespace */
778
779
#endif /* CVC4__PARSER__PARSER_STATE_H */