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 <optional>
#include <sstream>
#include <string>
 
class smt2_tokenizert
{
public:
  explicit smt2_tokenizert(std::istream &_in) : in(&_in)
  {
  }
 
  class smt2_errort
  {
  public:
    smt2_errort(smt2_errort &&) = default;
 
    smt2_errort(const smt2_errort &other)
    {
      // ostringstream does not have a copy constructor
      message << other.message.str();
      line_no = other.line_no;
    }
 
    smt2_errort(const std::string &_message, unsigned _line_no)
      : line_no(_line_no)
    {
      message << _message;
    }
 
    explicit smt2_errort(unsigned _line_no) : line_no(_line_no)
    {
    }
 
    std::string what() const
    {
      return message.str();
    }
 
    unsigned get_line_no() const
    {
      return line_no;
    }
 
    std::ostringstream &message_ostream()
    {
      return message;
    }
 
  protected:
    std::ostringstream message;
    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();
};
 
template <typename T>
smt2_tokenizert::smt2_errort
operator<<(smt2_tokenizert::smt2_errort &&e, const T &message)
{
  e.message_ostream() << message;
  return std::move(e);
}
 
bool is_smt2_simple_symbol_character(char);
 
#endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H