Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Term parser for smt2
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5parser_public.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__PARSER__SMT2__SMT2_TERM_PARSER_H
      19                 :            : #define CVC5__PARSER__SMT2__SMT2_TERM_PARSER_H
      20                 :            : 
      21                 :            : #include <cvc5/cvc5.h>
      22                 :            : 
      23                 :            : #include "parser/smt2/smt2_state.h"
      24                 :            : #include "parser/smt2/smt2_lexer.h"
      25                 :            : 
      26                 :            : namespace cvc5 {
      27                 :            : namespace parser {
      28                 :            : 
      29                 :            : /**
      30                 :            :  * The smt2 term parser, which parses terms, sorts, symbol expressions
      31                 :            :  * and other miscellaneous expressions from the SMT2 language. It reads
      32                 :            :  * from the given lexer.
      33                 :            :  */
      34                 :            : class Smt2TermParser
      35                 :            : {
      36                 :            :  public:
      37                 :            :   Smt2TermParser(Smt2Lexer& lex, Smt2State& state);
      38                 :      22956 :   virtual ~Smt2TermParser() {}
      39                 :            : 
      40                 :            :   /** Parses an SMT-LIB term <term> */
      41                 :            :   Term parseTerm();
      42                 :            :   /** Parses parentheses-enclosed term list (<term>*) */
      43                 :            :   std::vector<Term> parseTermList();
      44                 :            :   /** Parse an SMT-LIB sort <sort> */
      45                 :            :   Sort parseSort();
      46                 :            :   /** Parses parentheses-enclosed sort list (<sort>*) */
      47                 :            :   std::vector<Sort> parseSortList();
      48                 :            :   /**
      49                 :            :    * Parse parentheses-enclosed sorted variable list of the form:
      50                 :            :    * ((<symbol> <sort>)*)
      51                 :            :    */
      52                 :            :   std::vector<std::pair<std::string, Sort>> parseSortedVarList();
      53                 :            :   /**
      54                 :            :    * Parses an SMT-LIB symbolic expr. A symbolic expression has the syntax:
      55                 :            :    * <sexpr> := (<sexpr>*) | <symbol> | <spec_constant>
      56                 :            :    * The returned term has AST that consists of applications of SEXPR (for the
      57                 :            :    * first case of the BNF) and constant strings (for the latter two cases).
      58                 :            :    */
      59                 :            :   Term parseSymbolicExpr();
      60                 :            :   /**
      61                 :            :    * Parse symbol, which returns the string of the parsed symbol if the next
      62                 :            :    * token is a valid smt2 symbol.
      63                 :            :    *
      64                 :            :    * @param check Specifies whether to check if the symbol is already declared
      65                 :            :    * or not declared,
      66                 :            :    * @param type The type of symbol we are expecting (variable or sort).
      67                 :            :    */
      68                 :            :   std::string parseSymbol(DeclarationCheck check = CHECK_NONE,
      69                 :            :                           SymbolType type = SYM_VARIABLE);
      70                 :            :   /**
      71                 :            :    * Parse parentheses-enclosed symbol list.
      72                 :            :    * Expects to parse '(<symbol>*)', where '<symbol>' is parsed by the above
      73                 :            :    * method.
      74                 :            :    */
      75                 :            :   std::vector<std::string> parseSymbolList(DeclarationCheck check = CHECK_NONE,
      76                 :            :                                            SymbolType type = SYM_VARIABLE);
      77                 :            :   /**
      78                 :            :    * Parses ':X', returns 'X'
      79                 :            :    */
      80                 :            :   std::string parseKeyword();
      81                 :            :   /**
      82                 :            :    * Parse grammar, SyGuS 2.1 <GrammarDef>, which has syntax:
      83                 :            :    *
      84                 :            :    * <GrammarDef> := ((<symbol> <sort>)^n+1) (<GroupedRuleList>^n+1)
      85                 :            :    * <GroupedRuleList> := (<symbol> <Sort> (<GTerm>+))
      86                 :            :    * where <GTerm> is a term that additionally allows the SyGuS-specific
      87                 :            :    * grammar rules for Constant and Variable.
      88                 :            :    */
      89                 :            :   Grammar* parseGrammar(const std::vector<Term>& sygusVars,
      90                 :            :                         const std::string& fun);
      91                 :            :   /**
      92                 :            :    * Parse optional grammar <GrammarDef>?, return null if a grammar was not
      93                 :            :    * parsed.
      94                 :            :    */
      95                 :            :   Grammar* parseGrammarOrNull(const std::vector<Term>& sygusVars,
      96                 :            :                               const std::string& fun);
      97                 :            :   /** Parse integer numeral */
      98                 :            :   uint32_t parseIntegerNumeral();
      99                 :            :   /**
     100                 :            :    * Parse numeral list without parentheses
     101                 :            :    */
     102                 :            :   std::vector<std::string> parseNumeralList();
     103                 :            :   /**
     104                 :            :    * Parse datatype def '<datatype_dec>', not parentheses enclosed. The syntax
     105                 :            :    * for datatype declarations is:
     106                 :            :    *
     107                 :            :    * datatype_dec :=
     108                 :            :    *   (<constructor_dec>+) | (par (<symbol>+) (<constructor_dec>+))
     109                 :            :    * constructor_dec := (<symbol> (<symbol> <sort>)∗)
     110                 :            :    */
     111                 :            :   std::vector<DatatypeDecl> parseDatatypesDef(
     112                 :            :       bool isCo,
     113                 :            :       const std::vector<std::string>& dnames,
     114                 :            :       const std::vector<size_t>& arities);
     115                 :            :   /**
     116                 :            :    * Matches a string, and (optionally) strips off the quotes/unescapes the
     117                 :            :    * string when `unescape` is set to true.
     118                 :            :    */
     119                 :            :   std::string parseStr(bool unescape);
     120                 :            : 
     121                 :            :  protected:
     122                 :            :   /** Return the unsigned for the current token string. */
     123                 :            :   uint32_t tokenStrToUnsigned();
     124                 :            :   /**
     125                 :            :    * Return the string content of the current token string when interpreted
     126                 :            :    * as the given token, e.g. return`abc` for token string `|abc|` where
     127                 :            :    * tok is QUOTED_SYMBOL.
     128                 :            :    */
     129                 :            :   std::string tokenStrToSymbol(Token tok);
     130                 :            :   /**
     131                 :            :    * Unescape string, which updates s based on processing escape sequences
     132                 :            :    * as defined in SMT2.
     133                 :            :    */
     134                 :            :   void unescapeString(std::string& s);
     135                 :            :   /**
     136                 :            :    * Parse constructor definition list, add to declaration type. The expected
     137                 :            :    * syntax is '(<constructor_dec>+)'.
     138                 :            :    */
     139                 :            :   void parseConstructorDefinitionList(DatatypeDecl& type);
     140                 :            :   /**
     141                 :            :    * Continue parse indexed identifier, we've parsed '(_ ', now parse
     142                 :            :    * remainder '<symbol> <index>+)' and return the result.
     143                 :            :    */
     144                 :            :   ParseOp continueParseIndexedIdentifier(bool isOperator);
     145                 :            :   /**
     146                 :            :    * Continue parse qualified identifier, we've parsed '(as ', now parse
     147                 :            :    * remainder '<identifier> <type>)' and return the result.
     148                 :            :    */
     149                 :            :   ParseOp continueParseQualifiedIdentifier(bool isOperator);
     150                 :            :   /**
     151                 :            :    * Parse match case pattern
     152                 :            :    */
     153                 :            :   Term parseMatchCasePattern(Sort headSort, std::vector<Term>& boundVars);
     154                 :            :   /** The lexer */
     155                 :            :   Smt2Lexer& d_lex;
     156                 :            :   /** The state */
     157                 :            :   Smt2State& d_state;
     158                 :            : };
     159                 :            : 
     160                 :            : }  // namespace parser
     161                 :            : }  // namespace cvc5
     162                 :            : 
     163                 :            : #endif /* CVC5__PARSER__SMT2_TERM_PARSER_H */