instr.h

Go to the documentation of this file.

#ifndef ILANG_ILA_INSTR_H__
#define ILANG_ILA_INSTR_H__

#include <memory>
#include <set>
#include <string>

#include <ilang/ila/hash_ast.h>
#include <ilang/ila/object.h>

namespace ilang {

// Forward declaration for adding host ila.
class InstrLvlAbs;

class Instr : public Object {
public:
  typedef std::shared_ptr<Instr> InstrPtr;
  typedef std::shared_ptr<const Instr> InstrCnstPtr;
  typedef std::set<std::string> StateNameSet;

private:
  typedef std::map<std::string, ExprPtr> ExprPtrMap;
  typedef std::shared_ptr<InstrLvlAbs> InstrLvlAbsPtr;

public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  Instr(const std::string& name, const InstrLvlAbsPtr& host = nullptr);
  ~Instr();

  // ------------------------- HELPERS -------------------------------------- //
  static InstrPtr New(const std::string& name, InstrLvlAbsPtr host = nullptr);

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  bool is_instr() const { return true; }
  inline InstrLvlAbsPtr host() const { return host_; }

  void set_decode(const ExprPtr& decode);

  void set_update(const std::string& name, const ExprPtr& update);

  void set_update(const ExprPtr& state, const ExprPtr& update);

  void set_program(const InstrLvlAbsPtr& program);

  inline ExprPtr decode() const { return decode_; }

  ExprPtr update(const std::string& name) const;

  ExprPtr update(const ExprPtr& state) const;

  StateNameSet updated_states() const;

  inline InstrLvlAbsPtr program() const { return prog_; }

  // ------------------------- METHODS -------------------------------------- //
  void ForceSetDecode(const ExprPtr& decode);

  void ForceAddUpdate(const std::string& name, const ExprPtr& update);

  std::ostream& Print(std::ostream& out) const;

  friend std::ostream& operator<<(std::ostream& out, InstrPtr i);
  friend std::ostream& operator<<(std::ostream& out, InstrCnstPtr i);

private:
  // ------------------------- MEMBERS -------------------------------------- //
  ExprPtr decode_ = nullptr;
  ExprPtrMap updates_;

  InstrLvlAbsPtr host_ = nullptr;

  InstrLvlAbsPtr prog_ = nullptr;

  // ------------------------- HELPERS -------------------------------------- //
  ExprPtr Unify(const ExprPtr& e);

}; // class Instr

typedef Instr::InstrPtr InstrPtr;
typedef Instr::InstrCnstPtr InstrCnstPtr;
typedef std::vector<InstrPtr> InstrVec;

} // namespace ilang

#endif // ILNAG_ILA_INSTR_H__