vtarget_gen_relchc.h

// ---Hongce Zhang

#ifndef VTARGET_GEN_RELCHC_H__
#define VTARGET_GEN_RELCHC_H__

#include <ilang/config.h>

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

namespace ilang {

class VlgSglTgtGen_Relchc;

class Relchc_problem {
  friend class VlgSglTgtGen_Relchc;
  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;

}; // Relchc_problem


class VlgSglTgtGen_Relchc : public VlgSglTgtGen {
  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;

public:
  // --------------------- CONSTRUCTOR ---------------------------- //
  VlgSglTgtGen_Relchc(
      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 backend,
      const target_type_t& target_tp,
      advanced_parameters_t * adv_ptr);
  
  virtual ~VlgSglTgtGen_Relchc() {}

protected:
  Relchc_problem _problems;
  std::string relchc_prob_fname;
  std::string relchc_run_script_name;
  std::vector<std::string> vlg_mod_inv_vec;

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:
  // Here begins the specific functions
  // single_inv_problem()  : gensmt.ys
  // dual_inv_problem()    : gensmt.ys
  // single_inv_script()   : same run.sh
  // dual_inv_script() 
  // single_inv_tpl() :
  // dual_inv_tpl() :

  void dual_inv_problem(const std::string& ys_script_name);

  void dual_inv_tpl(const std::string & tpl_name, const std::string & smt_info);

  std::string dual_inv_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;
  

  virtual void do_not_instantiate(void) override { };

}; // class VlgVerifTgtGenRelchc


}; // namespace ilang

#endif // VTARGET_GEN_RELCHC_H__