v_eq_check_legacy_bmc.h

Go to the documentation of this file.

#ifndef ILANG_ILA_MNGR_V_LEGACY_BMC_H__
#define ILANG_ILA_MNGR_V_LEGACY_BMC_H__

#include <map>

#include <z3++.h>

#include <ilang/ila/instr_lvl_abs.h>
#include <ilang/target-smt/z3_expr_adapter.h>
#include <ilang/util/container.h>

namespace ilang {

class LegacyBmc {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  LegacyBmc();
  ~LegacyBmc();

  // ------------------------- METHODS -------------------------------------- //
  void AddInit(ExprPtr init);

  void AddInvariant(ExprPtr inv);

  void AddProperty(ExprPtr prop);

  z3::check_result Check(InstrLvlAbsPtr m0, const int& k0, InstrLvlAbsPtr m1,
                         const int& k1);

private:
  // ------------------------- MEMBERS -------------------------------------- //
  z3::context ctx_;
  Z3ExprAdapter gen_ = Z3ExprAdapter(ctx_);

  ExprPtrVec invs_;
  //
  ExprPtrVec inits_;

  bool def_tran_ = false;

  // ------------------------- HELPERS -------------------------------------- //
  z3::expr UnrollCmplIla(InstrLvlAbsPtr m, const int& k, const int& pos = 0);

  z3::expr Instr(const InstrPtr& instr, const std::string& suffix_prev,
                 const std::string& suffix_next, bool complete);

  z3::expr IlaOneHotFlat(const InstrLvlAbsPtr& ila,
                         const std::string& suffix_prev,
                         const std::string& suffix_next);

}; // class LegacyBmc

} // namespace ilang

#endif // ILANG_ILA_MNGR_V_LEGACY_BMC_H__