smt_ast.h

#ifndef SMT_AST_H__
#define SMT_AST_H__

#include <map>
#include <memory>
#include <string>
#include <vector>

namespace ilang {
namespace smt {

struct str_iterator {
  const std::string buf;
  size_t pnt;
  str_iterator(const std::string&, size_t p = 0);
  str_iterator(const str_iterator&);

  // ------------- MEMBER FUNCTIONS ---------------- //
  void jump_to_next(const std::string& c);
  size_t next_non_space_pos(const std::string& s = " \t\n\r") const;
  size_t next_non_space_pos(const std::string& s, size_t pos) const;
  void skip(const std::string& s = " \t\n\r");
  void skip_m(const std::string& s);
  // return true if it is the end
  bool is_end() const;
  // return true if it is the end
  bool is_end(size_t pos) const;
  char head() const;
  std::string head_word(const std::string& s = " \t\n\r") const;
  void expect(const std::string& c) const;
  size_t next(const std::string& s) const;
  size_t next(const std::string& s, size_t pos) const;
  void accept(const std::string& s);
  std::string accept_current_and_read_untill(const std::string& delimiter);
  std::string read_till_pos(size_t pos);
  std::string extract_untill_stack_empty(char push_symbol, char pop_symbol);
  std::string readline_no_eol();

}; // struct str_iterator

struct smt_item {
  virtual std::string toString() const = 0;
}; // struct smt_item

typedef std::shared_ptr<smt_item> smt_item_ptr;

struct line_comment : public smt_item {
  std::string comment;
  virtual std::string toString() const override;
}; // struct line_comment

struct var_type {
  enum tp { Bool, BV, Datatype } _type;
  unsigned _width;
  std::string module_name;
  // ------------- FUNCTIONS ---------------- //
  static var_type ParseFromString(str_iterator&); // will update the iterator
  std::string toString() const;
  static std::string toString(const std::vector<var_type>&);
  // ------------- MEMBER ---------------- //
  static bool eqtype(const var_type& l, const var_type& r);
  unsigned GetBoolBvWidth() const;
  bool is_bv() const;
  bool is_bool() const;
  bool is_datatype() const;
  // ------------- CONSTRUCTOR ---------------- //
  // default constructor
  var_type();
  // complete constructor
  var_type(tp vtype, unsigned width, const std::string mod_name);
  // copy constructor
  var_type(const var_type& vp);
  // assignment operator
  var_type& operator=(const var_type&) = default;

}; // struct var_type

struct state_var_t {
  std::string internal_name;
  std::string module_name;
  std::string verilog_name;
  var_type _type;
  // ------------- FUNCTIONS ---------------- //
  static state_var_t ParseFromString(
      str_iterator&,
      const std::string& default_module_name); // will update the iterator
};                                             // struct state_var_t

// declaration of datatypes
typedef std::map<std::string, std::vector<state_var_t>> datatypes_t;
typedef std::vector<std::string> data_type_order_t;

struct arg_t {
  std::string arg_name;
  var_type arg_type;
  // ------------- CONSTRUCTOR -------------- //
  arg_t(const std::string&, const var_type&);
  // ------------- FUNCTIONS ---------------- //
  std::string toString() const;
  static std::string toString(const std::vector<arg_t>& va);
  static arg_t ParseFromString(str_iterator&);
}; // struct arg_t

struct func_def_t : public smt_item {
  std::string func_name;
  std::string func_module;
  std::string args_text;
  std::vector<arg_t> args;
  var_type ret_type;
  std::string func_body;
  std::string extra_comment;
  // ------------- MEMBER FUNCTIONS ---------------- //
  virtual std::string toString() const override;
  static void ParseFromString(str_iterator&,
                              func_def_t&); // will update the iterator
};                                          // struct func_def_t

struct smt_file {
  std::vector<smt_item_ptr> items;
  datatypes_t datatypes;
  data_type_order_t data_type_order;
  // ------------- MEMBER FUNCTIONS ---------------- //
  std::string toString() const;
}; // struct smt_file

std::string ParseFromString(str_iterator& it, datatypes_t& dtype);
void ParseFromString(str_iterator& it, smt_file& smt);

std::string convert_to_binary(unsigned v, unsigned w); // if we have value here
std::string convert_to_binary(const std::string& v, unsigned radix, unsigned w);
}; // namespace smt
}; // namespace ilang

#endif // SMT_AST_H__