vtarget_gen_inv_chc.h

// ---Hongce Zhang

#ifndef VTARGET_GEN_INV_CHC_H__
#define VTARGET_GEN_INV_CHC_H__

#include <ilang/config.h>
#ifdef INVSYN_INTERFACE

#include <ilang/ila/instr_lvl_abs.h>
#include <ilang/smt-inout/yosys_smt_parser.h>
#include <ilang/vtarget-out/vlg_mod.h>
#include <ilang/vtarget-out/vtarget_gen_impl.h>
#include <iostream>
#include <memory>
#include <string>
#include <vector>

namespace ilang {

class VlgSglTgtGen_Chc;

class Chc_problem {
  friend class VlgSglTgtGen_Chc;
  typedef std::vector<std::string> prop_t;
  typedef struct {
    // the name in [??]
    // std::string  problem_name;
    prop_t exprs;
  } problem_t;
  typedef std::map<std::string, problem_t> problemset_t;

protected:
  problemset_t assumptions;
  problemset_t assertions;

}; // Chc_problem

class VlgSglTgtGen_Chc : public VlgSglTgtGen {

public:
  using target_type_t = VlgSglTgtGen::target_type_t;
  using info_t = VerilogModifier::info_t;
  using fn_l_map_t = VerilogModifier::fn_l_map_t;
  using advanced_parameters_t = VlgVerifTgtGenBase::advanced_parameters_t;
  using _chc_target_t = VlgVerifTgtGenBase::_chc_target_t;

public:
  // --------------------- CONSTRUCTOR ---------------------------- //
  VlgSglTgtGen_Chc(
      const std::string& output_path, // will be a sub directory of the
                                      // output_path of its parent
      const InstrPtr& instr_ptr, // which could be an empty pointer, and it will
                                 // be used to verify invariants
      const InstrLvlAbsPtr& ila_ptr,
      const VerilogGenerator::VlgGenConfig& config, nlohmann::json& _rf_vmap,
      nlohmann::json& _rf_cond, VlgTgtSupplementaryInfo& _sup_info,
      VerilogInfo* _vlg_info_ptr, const std::string& vlg_mod_inst_name,
      const std::string& ila_mod_inst_name, const std::string& wrapper_name,
      const std::vector<std::string>& implementation_srcs,
      const std::vector<std::string>& include_dirs,
      const vtg_config_t& vtg_config, backend_selector vbackend,
      synthesis_backend_selector sbackend, const target_type_t& target_tp,
      advanced_parameters_t* adv_ptr, bool generate_proof,
      _chc_target_t chc_target);

  // --------------------- Destructor ---------------------------- //
  virtual ~VlgSglTgtGen_Chc();

protected:
  Chc_problem _problems;
  std::string chc_prob_fname;
  std::string chc_run_script_name;
  std::vector<std::string> vlg_mod_inv_vec;
  synthesis_backend_selector s_backend;
  std::shared_ptr<smt::YosysSmtParser> design_smt_info;
  bool generate_proof;
  bool has_cex;
  _chc_target_t chc_target;

protected:
  virtual void add_a_direct_assumption(const std::string& aspt,
                                       const std::string& dspt) override;
  virtual void add_a_direct_assertion(const std::string& asst,
                                      const std::string& dspt) override;

  void virtual PreExportProcess() override;
  virtual void Export_script(const std::string& script_name) override;
  virtual void Export_problem(const std::string& extra_name) override;
  virtual void Export_mem(const std::string& mem_name) override;
  virtual void Export_modify_verilog() override;

private:
  void convert_smt_to_chc_datatype(const std::string& smt_fname,
                                   const std::string& chc_fname);
  void convert_smt_to_chc_bitvec(const std::string& smt_fname,
                                 const std::string& chc_fname,
                                 const std::string& wrapper_mod_name);
  void design_only_gen_smt(const std::string& smt_name,
                           const std::string& ys_script_name);

public:
  void virtual ExportAll(const std::string& wrapper_name,
                         const std::string& ila_vlg_name,
                         const std::string& script_name,
                         const std::string& extra_name,
                         const std::string& mem_name) override;
  std::shared_ptr<smt::YosysSmtParser> GetDesignSmtInfo() const;
  virtual void do_not_instantiate(void) override{};

}; // class VlgVerifTgtGenChc

}; // namespace ilang

#endif // INVSYN_INTERFACE

#endif // VTARGET_GEN_INV_CHC_H__