src/parser/parser.h

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