Branch data     Line data    Source code

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