vtarget_gen_inv_abc.h

// ---Hongce Zhang

#ifndef VTARGET_GEN_INV_ABC_H__
#define VTARGET_GEN_INV_ABC_H__

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

#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 <memory>
#include <string>
#include <vector>

namespace ilang {

class VlgSglTgtGen_Abc;

class Abc_problem {
  friend class VlgSglTgtGen_Abc;
  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;

}; // Abc_problem

class VlgSglTgtGen_Abc : 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_Abc(
      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 Abc_target, bool useGLA, bool useCORR, bool useAIGER);

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

protected:
  Abc_problem _problems;
  std::string blif_fname;
  std::string aiger_fname;
  std::string abc_run_script_name;
  std::vector<std::string> vlg_mod_inv_vec;
  synthesis_backend_selector s_backend;
  bool generate_proof;
  bool has_cex;
  _chc_target_t chc_target;
  const bool useGla;
  const bool useCorr;
  const bool useAiger;
  bool disallowGla;

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 generate_blif(const std::string& blif_name,
                     const std::string& ys_script_name);
  void generate_aiger(const std::string& blif_name,
                      const std::string& aiger_name,
                      const std::string& map_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 VlgVerifTgtGenAbc

}; // namespace ilang

#endif // INVSYN_INTERFACE

#endif // VTARGET_GEN_INV_ABC_H__