src/parser/parser.h

   1 /*********************                                                        */
   2 /*! \file parser.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andrew Reynolds, Christopher L. Conway
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief 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_STATE_H
  20 #define CVC4__PARSER__PARSER_STATE_H
  21
  22 #include <cassert>
  23 #include <list>
  24 #include <set>
  25 #include <string>
  26
  27 #include "api/cvc4cpp.h"
  28 #include "expr/expr.h"
  29 #include "expr/expr_stream.h"
  30 #include "expr/kind.h"
  31 #include "expr/symbol_table.h"
  32 #include "parser/input.h"
  33 #include "parser/parse_op.h"
  34 #include "parser/parser_exception.h"
  35 #include "util/unsafe_interrupt_exception.h"
  36
  37 namespace CVC4 {
  38
  39 // Forward declarations
  40 class BooleanType;
  41 class Command;
  42 class FunctionType;
  43 class Type;
  44 class ResourceManager;
  45 namespace api {
  46 class Solver;
  47 }
  48
  49 //for sygus gterm two-pass parsing
  50 class CVC4_PUBLIC SygusGTerm {
  51 public:
  52   enum{
  53     gterm_op,
  54     gterm_constant,
  55     gterm_variable,
  56     gterm_input_variable,
  57     gterm_local_variable,
  58     gterm_nested_sort,
  59     gterm_unresolved,
  60     gterm_ignore,
  61   };
  62   Type d_type;
  63   /** The parsed operator */
  64   ParseOp d_op;
  65   std::vector< Expr > d_let_vars;
  66   unsigned d_gterm_type;
  67   std::string d_name;
  68   std::vector< SygusGTerm > d_children;
  69
  70   unsigned getNumChildren() { return d_children.size(); }
  71   void addChild(){
  72     d_children.push_back( SygusGTerm() );
  73   }
  74 };
  75
  76 namespace parser {
  77
  78 class Input;
  79
  80 /** Types of checks for the symbols */
  81 enum DeclarationCheck {
  82   /** Enforce that the symbol has been declared */
  83   CHECK_DECLARED,
  84   /** Enforce that the symbol has not been declared */
  85   CHECK_UNDECLARED,
  86   /** Don't check anything */
  87   CHECK_NONE
  88 };/* enum DeclarationCheck */
  89
  90 /**
  91  * Returns a string representation of the given object (for
  92  * debugging).
  93  */
  94 inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) CVC4_PUBLIC;
  95 inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) {
  96   switch(check) {
  97   case CHECK_NONE:
  98     return out << "CHECK_NONE";
  99   case CHECK_DECLARED:
 100     return out << "CHECK_DECLARED";
 101   case CHECK_UNDECLARED:
 102     return out << "CHECK_UNDECLARED";
 103   default:
 104     return out << "DeclarationCheck!UNKNOWN";
 105   }
 106 }
 107
 108 /**
 109  * Types of symbols. Used to define namespaces.
 110  */
 111 enum SymbolType {
 112   /** Variables */
 113   SYM_VARIABLE,
 114   /** Sorts */
 115   SYM_SORT
 116 };/* enum SymbolType */
 117
 118 /**
 119  * Returns a string representation of the given object (for
 120  * debugging).
 121  */
 122 inline std::ostream& operator<<(std::ostream& out, SymbolType type) CVC4_PUBLIC;
 123 inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
 124   switch(type) {
 125   case SYM_VARIABLE:
 126     return out << "SYM_VARIABLE";
 127   case SYM_SORT:
 128     return out << "SYM_SORT";
 129   default:
 130     return out << "SymbolType!UNKNOWN";
 131   }
 132 }
 133
 134 /**
 135  * This class encapsulates all of the state of a parser, including the
 136  * name of the file, line number and column information, and in-scope
 137  * declarations.
 138  */
 139 class CVC4_PUBLIC Parser {
 140   friend class ParserBuilder;
 141 private:
 142  /** The resource manager associated with this expr manager */
 143  ResourceManager* d_resourceManager;
 144
 145  /** The input that we're parsing. */
 146  Input* d_input;
 147
 148  /**
 149   * The declaration scope that is "owned" by this parser.  May or
 150   * may not be the current declaration scope in use.
 151   */
 152  SymbolTable d_symtabAllocated;
 153
 154  /**
 155   * This current symbol table used by this parser.  Initially points
 156   * to d_symtabAllocated, but can be changed (making this parser
 157   * delegate its definitions and lookups to another parser).
 158   * See useDeclarationsFrom().
 159   */
 160  SymbolTable* d_symtab;
 161
 162  /**
 163   * The level of the assertions in the declaration scope.  Things declared
 164   * after this level are bindings from e.g. a let, a quantifier, or a
 165   * lambda.
 166   */
 167  size_t d_assertionLevel;
 168
 169  /**
 170   * Whether we're in global declarations mode (all definitions and
 171   * declarations are global).
 172   */
 173  bool d_globalDeclarations;
 174
 175  /**
 176   * Maintains a list of reserved symbols at the assertion level that might
 177   * not occur in our symbol table.  This is necessary to e.g. support the
 178   * proper behavior of the :named annotation in SMT-LIBv2 when used under
 179   * a let or a quantifier, since inside a let/quant body the declaration
 180   * scope is that of the let/quant body, but the defined name should be
 181   * reserved at the assertion level.
 182   */
 183  std::set<std::string> d_reservedSymbols;
 184
 185  /** How many anonymous functions we've created. */
 186  size_t d_anonymousFunctionCount;
 187
 188  /** Are we done */
 189  bool d_done;
 190
 191  /** Are semantic checks enabled during parsing? */
 192  bool d_checksEnabled;
 193
 194  /** Are we parsing in strict mode? */
 195  bool d_strictMode;
 196
 197  /** Are we only parsing? */
 198  bool d_parseOnly;
 199
 200  /**
 201   * Can we include files?  (Set to false for security purposes in
 202   * e.g. the online version.)
 203   */
 204  bool d_canIncludeFile;
 205
 206  /**
 207   * Whether the logic has been forced with --force-logic.
 208   */
 209  bool d_logicIsForced;
 210
 211  /**
 212   * The logic, if d_logicIsForced == true.
 213   */
 214  std::string d_forcedLogic;
 215
 216  /** The set of operators available in the current logic. */
 217  std::set<Kind> d_logicOperators;
 218
 219  /** The set of attributes already warned about. */
 220  std::set<std::string> d_attributesWarnedAbout;
 221
 222  /**
 223   * The current set of unresolved types.  We can get by with this NOT
 224   * being on the scope, because we can only have one DATATYPE
 225   * definition going on at one time.  This is a bit hackish; we
 226   * depend on mkMutualDatatypeTypes() to check everything and clear
 227   * this out.
 228   */
 229  std::set<Type> d_unresolved;
 230
 231  /**
 232   * "Preemption commands": extra commands implied by subterms that
 233   * should be issued before the currently-being-parsed command is
 234   * issued.  Used to support SMT-LIBv2 ":named" attribute on terms.
 235   *
 236   * Owns the memory of the Commands in the queue.
 237   */
 238  std::list<Command*> d_commandQueue;
 239
 240  /** Lookup a symbol in the given namespace (as specified by the type).
 241   * Only returns a symbol if it is not overloaded, returns null otherwise.
 242   */
 243  Expr getSymbol(const std::string& var_name, SymbolType type);
 244
 245 protected:
 246  /** The API Solver object. */
 247  api::Solver* d_solver;
 248
 249  /**
 250   * Create a parser state.
 251   *
 252   * @attention The parser takes "ownership" of the given
 253   * input and will delete it on destruction.
 254   *
 255   * @param the solver API object
 256   * @param input the parser input
 257   * @param strictMode whether to incorporate strict(er) compliance checks
 258   * @param parseOnly whether we are parsing only (and therefore certain checks
 259   * need not be performed, like those about unimplemented features, @see
 260   * unimplementedFeature())
 261   */
 262  Parser(api::Solver* solver,
 263         Input* input,
 264         bool strictMode = false,
 265         bool parseOnly = false);
 266
 267 public:
 268
 269   virtual ~Parser();
 270
 271   /** Get the associated <code>ExprManager</code>. */
 272   ExprManager* getExprManager() const;
 273
 274   /** Get the associated solver. */
 275   api::Solver* getSolver() const;
 276
 277   /** Get the associated input. */
 278   inline Input* getInput() const {
 279     return d_input;
 280   }
 281
 282   /** Deletes and replaces the current parser input. */
 283   void setInput(Input* input)  {
 284     delete d_input;
 285     d_input = input;
 286     d_input->setParser(*this);
 287     d_done = false;
 288   }
 289
 290   /**
 291    * Check if we are done -- either the end of input has been reached, or some
 292    * error has been encountered.
 293    * @return true if parser is done
 294    */
 295   inline bool done() const {
 296     return d_done;
 297   }
 298
 299   /** Sets the done flag */
 300   inline void setDone(bool done = true) {
 301     d_done = done;
 302   }
 303
 304   /** Enable semantic checks during parsing. */
 305   void enableChecks() { d_checksEnabled = true; }
 306
 307   /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
 308   void disableChecks() { d_checksEnabled = false; }
 309
 310   /** Enable strict parsing, according to the language standards. */
 311   void enableStrictMode() { d_strictMode = true; }
 312
 313   /** Disable strict parsing. Allows certain syntactic infelicities to
 314       pass without comment. */
 315   void disableStrictMode() { d_strictMode = false; }
 316
 317   bool strictModeEnabled() { return d_strictMode; }
 318
 319   void allowIncludeFile() { d_canIncludeFile = true; }
 320   void disallowIncludeFile() { d_canIncludeFile = false; }
 321   bool canIncludeFile() const { return d_canIncludeFile; }
 322
 323   /** Expose the functionality from SMT/SMT2 parsers, while making
 324       implementation optional by returning false by default. */
 325   virtual bool logicIsSet() { return false; }
 326
 327   virtual void forceLogic(const std::string& logic)
 328   {
 329     assert(!d_logicIsForced);
 330     d_logicIsForced = true;
 331     d_forcedLogic = logic;
 332   }
 333   const std::string& getForcedLogic() const { return d_forcedLogic; }
 334   bool logicIsForced() const { return d_logicIsForced; }
 335
 336   /**
 337    * Gets the variable currently bound to name.
 338    *
 339    * @param name the name of the variable
 340    * @return the variable expression
 341    * Only returns a variable if its name is not overloaded, returns null otherwise.
 342    */
 343   Expr getVariable(const std::string& name);
 344
 345   /**
 346    * Gets the function currently bound to name.
 347    *
 348    * @param name the name of the variable
 349    * @return the variable expression
 350    * Only returns a function if its name is not overloaded, returns null otherwise.
 351    */
 352   Expr getFunction(const std::string& name);
 353
 354   /**
 355    * Returns the expression that name should be interpreted as, based on the current binding.
 356    *
 357    * The symbol name should be declared.
 358    * This creates the expression that the string "name" should be interpreted as.
 359    * Typically this corresponds to a variable, but it may also correspond to
 360    * a nullary constructor or a defined function.
 361    * Only returns an expression if its name is not overloaded, returns null otherwise.
 362    */
 363   virtual Expr getExpressionForName(const std::string& name);
 364
 365   /**
 366    * Returns the expression that name should be interpreted as, based on the current binding.
 367    *
 368    * This is the same as above but where the name has been type cast to t.
 369    */
 370   virtual Expr getExpressionForNameAndType(const std::string& name, Type t);
 371
 372   /**
 373    * Returns the kind that should be used for applications of expression fun.
 374    * This is a generalization of ExprManager::operatorToKind that also
 375    * handles variables whose types are "function-like", i.e. where
 376    * checkFunctionLike(fun) returns true.
 377    *
 378    * For examples of the latter, this function returns
 379    *   APPLY_UF if fun has function type,
 380    *   APPLY_CONSTRUCTOR if fun has constructor type.
 381    */
 382   Kind getKindForFunction(Expr fun);
 383
 384   /**
 385    * Returns a sort, given a name.
 386    * @param sort_name the name to look up
 387    */
 388   Type getSort(const std::string& sort_name);
 389
 390   /**
 391    * Returns a (parameterized) sort, given a name and args.
 392    */
 393   Type getSort(const std::string& sort_name,
 394                const std::vector<Type>& params);
 395
 396   /**
 397    * Returns arity of a (parameterized) sort, given a name and args.
 398    */
 399   size_t getArity(const std::string& sort_name);
 400
 401   /**
 402    * Checks if a symbol has been declared.
 403    * @param name the symbol name
 404    * @param type the symbol type
 405    * @return true iff the symbol has been declared with the given type
 406    */
 407   bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
 408
 409   /**
 410    * Checks if the declaration policy we want to enforce holds
 411    * for the given symbol.
 412    * @param name the symbol to check
 413    * @param check the kind of check to perform
 414    * @param type the type of the symbol
 415    * @param notes notes to add to a parse error (if one is generated)
 416    * @throws ParserException if checks are enabled and the check fails
 417    */
 418   void checkDeclaration(const std::string& name,
 419                         DeclarationCheck check,
 420                         SymbolType type = SYM_VARIABLE,
 421                         std::string notes = "");
 422
 423   /**
 424    * Reserve a symbol at the assertion level.
 425    */
 426   void reserveSymbolAtAssertionLevel(const std::string& name);
 427
 428   /**
 429    * Checks whether the given expression is function-like, i.e.
 430    * it expects arguments. This is checked by looking at the type
 431    * of fun. Examples of function types are function, constructor,
 432    * selector, tester.
 433    * @param fun the expression to check
 434    * @throws ParserException if checks are enabled and fun is not
 435    * a function
 436    */
 437   void checkFunctionLike(Expr fun);
 438
 439   /**
 440    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
 441    * @param kind the built-in operator to check
 442    * @param numArgs the number of actual arguments
 443    * @throws ParserException if checks are enabled and the operator
 444    * <code>kind</code> cannot be applied to <code>numArgs</code>
 445    * arguments.
 446    */
 447   void checkArity(Kind kind, unsigned numArgs);
 448
 449   /**
 450    * Check that <code>kind</code> is a legal operator in the current
 451    * logic and that it can accept <code>numArgs</code> arguments.
 452    *
 453    * @param kind the built-in operator to check
 454    * @param numArgs the number of actual arguments
 455    * @throws ParserException if the parser mode is strict and the
 456    * operator <code>kind</code> has not been enabled
 457    */
 458   void checkOperator(Kind kind, unsigned numArgs);
 459
 460   /** Create a new CVC4 variable expression of the given type.
 461    *
 462    * flags specify information about the variable, e.g. whether it is global or defined
 463    *   (see enum in expr_manager_template.h).
 464    *
 465    * If a symbol with name already exists,
 466    *  then if doOverload is true, we create overloaded operators.
 467    *  else if doOverload is false, the existing expression is shadowed by the new expression.
 468    */
 469   Expr mkVar(const std::string& name, const Type& type,
 470              uint32_t flags = ExprManager::VAR_FLAG_NONE,
 471              bool doOverload = false);
 472
 473   /**
 474    * Create a set of new CVC4 variable expressions of the given type.
 475    *
 476    * flags specify information about the variable, e.g. whether it is global or defined
 477    *   (see enum in expr_manager_template.h).
 478    *
 479    * For each name, if a symbol with name already exists,
 480    *  then if doOverload is true, we create overloaded operators.
 481    *  else if doOverload is false, the existing expression is shadowed by the new expression.
 482    */
 483   std::vector<Expr>
 484     mkVars(const std::vector<std::string> names, const Type& type,
 485            uint32_t flags = ExprManager::VAR_FLAG_NONE,
 486            bool doOverload = false);
 487
 488   /**
 489    * Create a new CVC4 bound variable expression of the given type. This binds
 490    * the symbol name to that variable in the current scope.
 491    */
 492   Expr mkBoundVar(const std::string& name, const Type& type);
 493   /**
 494    * Create a new CVC4 bound variable expressions of the given names and types.
 495    * Like the method above, this binds these names to those variables in the
 496    * current scope.
 497    */
 498   std::vector<Expr> mkBoundVars(
 499       std::vector<std::pair<std::string, Type> >& sortedVarNames);
 500
 501   /**
 502    * Create a set of new CVC4 bound variable expressions of the given type.
 503    *
 504    * flags specify information about the variable, e.g. whether it is global or defined
 505    *   (see enum in expr_manager_template.h).
 506    *
 507    * For each name, if a symbol with name already exists,
 508    *  then if doOverload is true, we create overloaded operators.
 509    *  else if doOverload is false, the existing expression is shadowed by the new expression.
 510    */
 511   std::vector<Expr> mkBoundVars(const std::vector<std::string> names, const Type& type);
 512
 513   /**
 514    * Create a new CVC4 function expression of the given type,
 515    * appending a unique index to its name.  (That's the ONLY
 516    * difference between mkAnonymousFunction() and mkVar()).
 517    *
 518    * flags specify information about the variable, e.g. whether it is global or defined
 519    *   (see enum in expr_manager_template.h).
 520    */
 521   Expr mkAnonymousFunction(const std::string& prefix, const Type& type,
 522                            uint32_t flags = ExprManager::VAR_FLAG_NONE);
 523
 524   /** Create a new variable definition (e.g., from a let binding).
 525    * levelZero is set if the binding must be done at level 0.
 526    * If a symbol with name already exists,
 527    *  then if doOverload is true, we create overloaded operators.
 528    *  else if doOverload is false, the existing expression is shadowed by the new expression.
 529    */
 530   void defineVar(const std::string& name, const Expr& val,
 531                  bool levelZero = false, bool doOverload = false);
 532
 533   /**
 534    * Create a new type definition.
 535    *
 536    * @param name The name of the type
 537    * @param type The type that should be associated with the name
 538    * @param levelZero If true, the type definition is considered global and
 539    *                  cannot be removed by poppoing the user context
 540    */
 541   void defineType(const std::string& name,
 542                   const Type& type,
 543                   bool levelZero = false);
 544
 545   /**
 546    * Create a new (parameterized) type definition.
 547    *
 548    * @param name The name of the type
 549    * @param params The type parameters
 550    * @param type The type that should be associated with the name
 551    * @param levelZero If true, the type definition is considered global and
 552    *                  cannot be removed by poppoing the user context
 553    */
 554   void defineType(const std::string& name,
 555                   const std::vector<Type>& params,
 556                   const Type& type,
 557                   bool levelZero = false);
 558
 559   /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
 560   void defineParameterizedType(const std::string& name,
 561                                const std::vector<Type>& params,
 562                                const Type& type);
 563
 564   /**
 565    * Creates a new sort with the given name.
 566    */
 567   SortType mkSort(const std::string& name,
 568                   uint32_t flags = ExprManager::SORT_FLAG_NONE);
 569
 570   /**
 571    * Creates a new sort constructor with the given name and arity.
 572    */
 573   SortConstructorType mkSortConstructor(
 574       const std::string& name,
 575       size_t arity,
 576       uint32_t flags = ExprManager::SORT_FLAG_NONE);
 577
 578   /**
 579    * Creates a new "unresolved type," used only during parsing.
 580    */
 581   SortType mkUnresolvedType(const std::string& name);
 582
 583   /**
 584    * Creates a new unresolved (parameterized) type constructor of the given
 585    * arity.
 586    */
 587   SortConstructorType mkUnresolvedTypeConstructor(const std::string& name,
 588                                                   size_t arity);
 589   /**
 590    * Creates a new unresolved (parameterized) type constructor given the type
 591    * parameters.
 592    */
 593   SortConstructorType mkUnresolvedTypeConstructor(const std::string& name,
 594                                                   const std::vector<Type>& params);
 595
 596   /**
 597    * Returns true IFF name is an unresolved type.
 598    */
 599   bool isUnresolvedType(const std::string& name);
 600
 601   /**
 602    * Create sorts of mutually-recursive datatypes.
 603    * For each symbol defined by the datatype, if a symbol with name already exists,
 604    *  then if doOverload is true, we create overloaded operators.
 605    *  else if doOverload is false, the existing expression is shadowed by the new expression.
 606    *
 607    * flags specify information about the datatype, e.g. whether it should be
 608    * printed out as a definition in models or not
 609    *   (see enum in expr_manager_template.h).
 610    */
 611   std::vector<DatatypeType> mkMutualDatatypeTypes(
 612       std::vector<Datatype>& datatypes,
 613       bool doOverload = false,
 614       uint32_t flags = ExprManager::DATATYPE_FLAG_NONE);
 615
 616   /** make flat function type
 617    *
 618    * Returns the "flat" function type corresponding to the function taking
 619    * argument types "sorts" and range type "range".  A flat function type is
 620    * one whose range is not a function. Notice that if sorts is empty and range
 621    * is not a function, then this function returns range itself.
 622    *
 623    * If range is a function type, we add its function argument sorts to sorts
 624    * and consider its function range as the new range. For each sort S added
 625    * to sorts in this process, we add a new bound variable of sort S to
 626    * flattenVars.
 627    *
 628    * For example:
 629    * mkFlattenFunctionType( { Int, (-> Real Real) }, (-> Int Bool), {} ):
 630    * - returns the the function type (-> Int (-> Real Real) Int Bool)
 631    * - updates sorts to { Int, (-> Real Real), Int },
 632    * - updates flattenVars to { x }, where x is bound variable of type Int.
 633    *
 634    * Notice that this method performs only one level of flattening, for example,
 635    * mkFlattenFunctionType({ Int, (-> Real Real) }, (-> Int (-> Int Bool)), {}):
 636    * - returns the the function type (-> Int (-> Real Real) Int (-> Int Bool))
 637    * - updates sorts to { Int, (-> Real Real), Int },
 638    * - updates flattenVars to { x }, where x is bound variable of type Int.
 639    *
 640    * This method is required so that we do not return functions
 641    * that have function return type (these give an unhandled exception
 642    * in the ExprManager). For examples of the equivalence between function
 643    * definitions in the proposed higher-order extension of the smt2 language,
 644    * see page 3 of http://matryoshka.gforge.inria.fr/pubs/PxTP2017.pdf.
 645    *
 646    * The argument flattenVars is needed in the case of defined functions
 647    * with function return type. These have implicit arguments, for instance:
 648    *    (define-fun Q ((x Int)) (-> Int Int) (lambda y (P x)))
 649    * is equivalent to the command:
 650    *    (define-fun Q ((x Int) (z Int)) Int (@ (lambda y (P x)) z))
 651    * where @ is (higher-order) application. In this example, z is added to
 652    * flattenVars.
 653    */
 654   Type mkFlatFunctionType(std::vector<Type>& sorts,
 655                           Type range,
 656                           std::vector<Expr>& flattenVars);
 657
 658   /** make flat function type
 659    *
 660    * Same as above, but does not take argument flattenVars.
 661    * This is used when the arguments of the function are not important (for
 662    * instance, if we are only using this type in a declare-fun).
 663    */
 664   Type mkFlatFunctionType(std::vector<Type>& sorts, Type range);
 665
 666   /** make higher-order apply
 667    *
 668    * This returns the left-associative curried application of (function) expr to
 669    * the arguments in args.
 670    *
 671    * For example, mkHoApply( f, { a, b }, 0 ) returns
 672    *  (HO_APPLY (HO_APPLY f a) b)
 673    *
 674    * If args is non-empty, the expected type of expr is (-> T0 ... Tn T), where
 675    *    args[i].getType() = Ti
 676    * for each i where 0 <= i < args.size(). If expr is not of this
 677    * type, the expression returned by this method will not be well typed.
 678    */
 679   Expr mkHoApply(Expr expr, std::vector<Expr>& args);
 680
 681   /** Apply type ascription
 682    *
 683    * Return term t with a type ascription applied to it. This is used for
 684    * syntax like (as t T) in smt2 and t::T in the CVC language. This includes:
 685    * - (as emptyset (Set T))
 686    * - (as univset (Set T))
 687    * - (as sep.nil T)
 688    * - (cons T)
 689    * - ((as cons T) t1 ... tn) where cons is a parametric datatype constructor.
 690    *
 691    * The term to ascribe t is a term whose kind and children (but not type)
 692    * are equivalent to that of the term returned by this method.
 693    *
 694    * Notice that method is not necessarily a cast. In actuality, the above terms
 695    * should be understood as symbols indexed by types. However, SMT-LIB does not
 696    * permit types as indices, so we must use, e.g. (as emptyset (Set T))
 697    * instead of (_ emptyset (Set T)).
 698    *
 699    * @param t The term to ascribe a type
 700    * @param s The sort to ascribe
 701    * @return Term t with sort s ascribed.
 702    */
 703   api::Term applyTypeAscription(api::Term t, api::Sort s);
 704
 705   /**
 706    * Add an operator to the current legal set.
 707    *
 708    * @param kind the built-in operator to add
 709    */
 710   void addOperator(Kind kind);
 711
 712   /**
 713    * Preempt the next returned command with other ones; used to
 714    * support the :named attribute in SMT-LIBv2, which implicitly
 715    * inserts a new command before the current one. Also used in TPTP
 716    * because function and predicate symbols are implicitly declared.
 717    */
 718   void preemptCommand(Command* cmd);
 719
 720   /** Is the symbol bound to a boolean variable? */
 721   bool isBoolean(const std::string& name);
 722
 723   /** Is fun a function (or function-like thing)?
 724   * Currently this means its type is either a function, constructor, tester, or selector.
 725   */
 726   bool isFunctionLike(Expr fun);
 727
 728   /** Is the symbol bound to a predicate? */
 729   bool isPredicate(const std::string& name);
 730
 731   /** Parse and return the next command. */
 732   Command* nextCommand();
 733
 734   /** Parse and return the next expression. */
 735   api::Term nextExpression();
 736
 737   /** Issue a warning to the user. */
 738   void warning(const std::string& msg) { d_input->warning(msg); }
 739   /** Issue a warning to the user, but only once per attribute. */
 740   void attributeNotSupported(const std::string& attr);
 741
 742   /** Raise a parse error with the given message. */
 743   inline void parseError(const std::string& msg) { d_input->parseError(msg); }
 744   /** Unexpectedly encountered an EOF */
 745   inline void unexpectedEOF(const std::string& msg)
 746   {
 747     d_input->parseError(msg, true);
 748   }
 749
 750   /**
 751    * If we are parsing only, don't raise an exception; if we are not,
 752    * raise a parse error with the given message.  There is no actual
 753    * parse error, everything is as expected, but we cannot create the
 754    * Expr, Type, or other requested thing yet due to internal
 755    * limitations.  Even though it's not a parse error, we throw a
 756    * parse error so that the input line and column information is
 757    * available.
 758    *
 759    * Think quantifiers.  We don't have a TheoryQuantifiers yet, so we
 760    * have no kind::FORALL or kind::EXISTS.  But we might want to
 761    * support parsing quantifiers (just not doing anything with them).
 762    * So this mechanism gives you a way to do it with --parse-only.
 763    */
 764   inline void unimplementedFeature(const std::string& msg)
 765   {
 766     if(!d_parseOnly) {
 767       parseError("Unimplemented feature: " + msg);
 768     }
 769   }
 770
 771   /**
 772    * Gets the current declaration level.
 773    */
 774   inline size_t scopeLevel() const { return d_symtab->getLevel(); }
 775
 776   /**
 777    * Pushes a scope. All subsequent symbol declarations made are only valid in
 778    * this scope, i.e. they are deleted on the next call to popScope.
 779    *
 780    * The argument bindingLevel is true, the assertion level is set to the
 781    * current scope level. This determines which scope assertions are declared
 782    * at.
 783    */
 784   inline void pushScope(bool bindingLevel = false) {
 785     d_symtab->pushScope();
 786     if(!bindingLevel) {
 787       d_assertionLevel = scopeLevel();
 788     }
 789   }
 790
 791   inline void popScope() {
 792     d_symtab->popScope();
 793     if(scopeLevel() < d_assertionLevel) {
 794       d_assertionLevel = scopeLevel();
 795       d_reservedSymbols.clear();
 796     }
 797   }
 798
 799   virtual void reset() {
 800     d_symtab->reset();
 801   }
 802
 803   void setGlobalDeclarations(bool flag) {
 804     d_globalDeclarations = flag;
 805   }
 806
 807   /**
 808    * Set the current symbol table used by this parser.
 809    * From now on, this parser will perform its definitions and
 810    * lookups in the declaration scope of the "parser" argument
 811    * (but doesn't re-delegate if the other parser's declaration scope
 812    * changes later).  A NULL argument restores this parser's
 813    * "primordial" declaration scope assigned at its creation.  Calling
 814    * p->useDeclarationsFrom(p) is a no-op.
 815    *
 816    * This feature is useful when e.g. reading out-of-band expression data:
 817    * 1. Parsing --replay log files produced with --replay-log.
 818    * 2. Perhaps a multi-query benchmark file is being single-stepped
 819    *    with intervening queries on stdin that must reference the same
 820    *    declaration scope(s).
 821    *
 822    * However, the feature must be used carefully.  Pushes and pops
 823    * should be performed with the correct current declaration scope.
 824    * Care must be taken to match up declaration scopes, of course;
 825    * If variables in the deferred-to parser go out of scope, the
 826    * secondary parser will give errors that they are undeclared.
 827    * Also, an outer-scope variable shadowed by an inner-scope one of
 828    * the same name may be temporarily inaccessible.
 829    *
 830    * In short, caveat emptor.
 831    */
 832   inline void useDeclarationsFrom(Parser* parser) {
 833     if(parser == NULL) {
 834       d_symtab = &d_symtabAllocated;
 835     } else {
 836       d_symtab = parser->d_symtab;
 837     }
 838   }
 839
 840   inline void useDeclarationsFrom(SymbolTable* symtab) {
 841     d_symtab = symtab;
 842   }
 843
 844   inline SymbolTable* getSymbolTable() const {
 845     return d_symtab;
 846   }
 847
 848   /**
 849    * An expression stream interface for a parser.  This stream simply
 850    * pulls expressions from the given Parser object.
 851    *
 852    * Here, the ExprStream base class allows a Parser (from the parser
 853    * library) and core components of CVC4 (in the core library) to
 854    * communicate without polluting the public interface or having them
 855    * reach into private (undocumented) interfaces.
 856    */
 857   class ExprStream : public CVC4::ExprStream {
 858     Parser* d_parser;
 859   public:
 860     ExprStream(Parser* parser) : d_parser(parser) {}
 861     ~ExprStream() { delete d_parser; }
 862     Expr nextExpr() override { return d_parser->nextExpression().getExpr(); }
 863   };/* class Parser::ExprStream */
 864
 865   //------------------------ operator overloading
 866   /** is this function overloaded? */
 867   bool isOverloadedFunction(Expr fun) {
 868     return d_symtab->isOverloadedFunction(fun);
 869   }
 870
 871   /** Get overloaded constant for type.
 872    * If possible, it returns a defined symbol with name
 873    * that has type t. Otherwise returns null expression.
 874   */
 875   Expr getOverloadedConstantForType(const std::string& name, Type t) {
 876     return d_symtab->getOverloadedConstantForType(name, t);
 877   }
 878
 879   /**
 880    * If possible, returns a defined function for a name
 881    * and a vector of expected argument types. Otherwise returns
 882    * null expression.
 883    */
 884   Expr getOverloadedFunctionForTypes(const std::string& name, std::vector< Type >& argTypes) {
 885     return d_symtab->getOverloadedFunctionForTypes(name, argTypes);
 886   }
 887   //------------------------ end operator overloading
 888 };/* class Parser */
 889
 890 }/* CVC4::parser namespace */
 891 }/* CVC4 namespace */
 892
 893 #endif /* CVC4__PARSER__PARSER_STATE_H */