expr_const.h

Go to the documentation of this file.

#ifndef ILANG_ILA_AST_EXPR_CONST_H__
#define ILANG_ILA_AST_EXPR_CONST_H__

#include <ilang/ila/ast/expr.h>
#include <ilang/ila/ast/sort_value.h>

namespace ilang {

class ExprConst : public Expr {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  ExprConst(const BoolVal& bool_val);
  ExprConst(const BvVal& bv_val, const int& bit_width);
  ExprConst(const MemVal& mem_val, const int& addr_width,
            const int& data_width);
  ~ExprConst();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  bool is_const() const { return true; }

  // ------------------------- METHODS -------------------------------------- //
  z3::expr GetZ3Expr(z3::context& z3_ctx, const Z3ExprVec& z3expr_vec,
                     const std::string& suffix = "") const;

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

  BoolValPtr val_bool() const;
  BvValPtr val_bv() const;
  MemValPtr val_mem() const;

private:
  // ------------------------- MEMBERS -------------------------------------- //
  ValPtr val_;

}; // class ExprConst

} // namespace ilang

#endif // ILANG_ILA_AST_EXPR_CONST_H__