smt2_tokenizer.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/

 
#ifndef CPROVER_SOLVERS_SMT2_SMT2_TOKENIZER_H
#define CPROVER_SOLVERS_SMT2_SMT2_TOKENIZER_H
 
#include <util/exception_utils.h>
 
#include <optional>
#include <sstream>
#include <string>
 
class smt2_tokenizert
{
public:
  explicit smt2_tokenizert(std::istream &_in) : in(&_in)
  {
  }

  class smt2_errort : public cprover_exception_baset
  {
  public:
    smt2_errort(const std::string &_message, unsigned _line_no)
      : line_no(_line_no)
    {
      _reason << _message;
    }
 
    explicit smt2_errort(unsigned _line_no) : line_no(_line_no)
    {
    }
 
    unsigned get_line_no() const
    {
      return line_no;
    }
 
  protected:
    unsigned line_no;
  };
 
  using token_kindt = enum {
    NONE,
    END_OF_FILE,
    STRING_LITERAL,
    NUMERAL,
    SYMBOL,
    KEYWORD,
    OPEN,
    CLOSE
  };

  class tokent
  {
  public:
    tokent() = default;
    explicit tokent(token_kindt _kind) : kind(_kind)
    {
    }

    token_kindt kind = NONE;
    std::string text;
    unsigned line_no = 0;
    bool quoted_symbol = false;

    operator token_kindt() const
    {
      return kind;
    }
  };

  tokent next_token();

  const tokent &peek()
  {
    if(!peeked.has_value())
      peeked = read_token();
    return *peeked;
  }

  smt2_errort error(const std::string &message) const
  {
    return smt2_errort(message, current_line_no());
  }

  smt2_errort error() const
  {
    return smt2_errort(current_line_no());
  }
 
protected:
  std::istream *in;

  void skip_to_end_of_list();
 
private:
  unsigned line_no = 1;

  std::optional<tokent> peeked;

  unsigned current_line_no() const
  {
    return peeked.has_value() ? peeked->line_no : line_no;
  }

  tokent get_decimal_numeral();
  tokent get_hex_numeral();
  tokent get_bin_numeral();
  tokent get_simple_symbol();
  tokent get_quoted_symbol();
  tokent get_string_literal();

  tokent read_token();
};
 
bool is_smt2_simple_symbol_character(char);
 
#endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H