yosys_smt_parser.h

#ifndef YOSYS_SMT_PARSER_H__
#define YOSYS_SMT_PARSER_H__

#include <ilang/smt-inout/smt_ast.h>

#include <iostream>
#include <set>
#include <string>

namespace ilang {
namespace smt {

class YosysSmtParser {
public:
  typedef std::map<std::string, state_var_t*> variable_idx_t;
  // ---------------- TYPE DEFs -------------------- //
protected:
  smt_file smt_ast;
  datatypes_t flatten_datatype;
  variable_idx_t variable_idx;
  // ------------- HELPER FUNCTIONS ---------------- //
  void construct_flatten_dataype();
  void replace_all_function_arg_body();
  void add_no_change_function();
  void create_variable_idx();

public:
  // ----------- HELPER FUNCTIONS - Low Level ----- //
  static void
  convert_flatten_datatype_to_arg_vec(const std::vector<state_var_t>&,
                                      std::vector<arg_t>&,
                                      const std::string& suffix);
  static void convert_datatype_to_type_vec(
      const std::vector<state_var_t>& all_flattened_state_var,
      std::vector<var_type>& args);
  static std::string st_name_add_suffix(const std::string& stname,
                                        const std::string& suffix);
  static std::string st_name_add_prefix(const std::string& stname,
                                        const std::string& prefix);
  static std::vector<std::string> str_to_list(const std::string& in);

protected:
  // ----------- HELPER FUNCTIONS - Low Level ----- //
  std::string replace_a_body(
      const std::string& current_module,
      const std::map<std::string, state_var_t>& current_mod_state_var_idx,
      const std::vector<std::string>& arg_def, // [state] or [state,next_state]
      const std::set<std::string>& defined_func, const std::string& body_text);
  void replace_a_func(
      std::shared_ptr<func_def_t> fn, const std::string& current_module,
      // string -> state_var of current map
      const std::map<std::string, state_var_t>& current_mod_state_var_idx,
      const std::set<std::string>& defined_func);

public:
  // -------------- CONSTRUCTOR -------------------- //
  YosysSmtParser(const std::string& buf);
  // -------------- DESTRUCTOR -------------------- //
  virtual ~YosysSmtParser();
  // -------------- Procedures -------------------- //
  void BreakDatatypes();
  void AddNoChangeStateUpdateFunction();
  std::string Export();
  const smt_file& GetRawSmtAst() const;
  // -------------- Helpers -------------------- //
  const std::vector<std::string>& get_module_def_orders() const;
  const std::vector<state_var_t>&
  get_module_flatten_dt(const std::string& mod_name) const;
  const variable_idx_t& get_var_idx() const;
  bool is_state_name(const std::string& state_name) const;
}; // class YosysSmtParser

}; // namespace smt
}; // namespace ilang

#endif