cex_extract.h

// ---Hongce Zhang

#ifndef ILANG_VTARGET_OUT_CEX_EXTRACT_H__
#define ILANG_VTARGET_OUT_CEX_EXTRACT_H__

#include <functional>
#include <map>
#include <set>
#include <string>

namespace ilang {

class CexExtractor {
public:
  // -------------------- TYPES ------------------ //
  typedef std::string vlg_val;
  typedef std::map<std::string, vlg_val> cex_t;
  typedef std::map<std::string, bool> cex_is_reg_t;
  typedef std::function<bool(const std::string&)> is_reg_t;

protected:
  cex_t cex;
  cex_is_reg_t cex_is_reg;
  void virtual parse_from(const std::string& vcd_file_name,
                          const std::string& scope, is_reg_t is_reg,
                          bool reg_only);

public:
  // -------------------- CONSTRUCTOR ------------------ //
  CexExtractor(const std::string& vcd_file_name, const std::string& scope,
               is_reg_t is_reg, bool reg_only);

  CexExtractor(const std::string& fin);

  // -------------------- MEMBERS ------------------ //
  std::string GenInvAssert(
      const std::string& prefix,
      const std::set<std::string>& focus_name = std::set<std::string>()) const;
  const cex_t& GetCex() const;
  // save to file
  static void StoreCexToFile(const std::string& fn, const cex_t& c);
  // save to file (invoke within)
  void StoreCexToFile(const std::string& fn) const;
  // generalize cex
  void DropStates(const std::vector<std::string>& vnames);

}; // class CexExtractor

}; // namespace ilang

#endif // ILANG_VTARGET_OUT_CEX_EXTRACT_H__