inv_obj.h

// Hongce Zhang

#ifndef ILANG_VTARGET_OUT_INV_OBJ_H__
#define ILANG_VTARGET_OUT_INV_OBJ_H__

#include <ilang/config.h>

#include <ilang/smt-inout/yosys_smt_parser.h>
#include <ilang/vtarget-out/inv-syn/inv_cnf.h>

#include <string>
#include <tuple>
#include <vector>

namespace ilang {

class InvariantInCnf;

class InvariantObject {
public:
  // ----------- TYPE DEFs ---------- //
  typedef std::vector<std::string> inv_vec_t;
  typedef std::vector<std::tuple<std::string, std::string, int>>
      extra_var_def_vec_t;
  typedef std::map<std::string, int> extra_free_var_def_vec_t;
  typedef std::vector<std::string> smt_formula_vec_t;
  // ----------- CONSTRUCTOR ---------- //
  InvariantObject();

#ifdef INVSYN_INTERFACE

  bool AddInvariantFromChcResultFile(
      smt::YosysSmtParser& design_info, const std::string& tag,
      const std::string& chc_result_fn, bool flatten_datatype,
      bool flatten_hierarchy, bool discourage_outside_var_referral = true);

  void
  AddInvariantFromGrainResultFile(smt::YosysSmtParser& design_info,
                                  const std::string& tag,
                                  const std::string& chc_result_fn,
                                  bool discourage_outside_var_referral = true,
                                  bool change_outside_var = true);

  bool AddInvariantFromAbcResultFile(
      const std::string& blif_fname, const std::string& abc_fname,
      bool warning_outside_var, bool replace_outside_var,
      const std::string& gla_map_fname, bool useAiger,
      const std::string& aiger_map_name, InvariantInCnf& inv_cnf,
      const InvariantInCnf& ref_cnf);

#endif // INVSYN_INTERFACE

  void AddInvariantFromVerilogExpr(const std::string& tag,
                                   const std::string& vlg_in);
  const inv_vec_t& GetVlgConstraints() const;
  const extra_var_def_vec_t& GetExtraVarDefs() const;
  const extra_free_var_def_vec_t& GetExtraFreeVarDefs() const;
  const smt_formula_vec_t& GetSmtFormulae() const;
  void set_dut_inst_name(const std::string& name);
  void ClearAllInvariants();
  void ExportToFile(const std::string& fn,
                    bool export_smt_encoding = true) const;
  void ImportFromFile(const std::string& fn);
  void InsertFromAnotherInvObj(const InvariantObject& r);
  size_t NumInvariant() const;
  void RemoveInvByIdx(size_t idx);

protected:
  std::vector<std::string> inv_vlg_exprs;
  extra_var_def_vec_t inv_extra_vlg_vars;
  extra_free_var_def_vec_t inv_extra_free_vars;
  smt_formula_vec_t smt_formula_vec;
  std::string dut_inst_name;
};

}; // namespace ilang

#endif // ILANG_VTARGET_OUT_INV_OBJ_H__