ilang  1.0.2
ILAng: A Modeling and Verification Platform for SoCs
expr.h
Go to the documentation of this file.
1 
4 #ifndef ILANG_ILA_AST_EXPR_H__
5 #define ILANG_ILA_AST_EXPR_H__
6 
7 #include <memory>
8 #include <ostream>
9 #include <string>
10 #include <unordered_map>
11 #include <unordered_set>
12 #include <vector>
13 
14 #include "z3++.h"
15 #include "z3_api.h"
16 #include <ilang/ila/ast/ast.h>
17 #include <ilang/ila/ast/sort.h>
18 #include <ilang/ila/defines.h>
19 
21 namespace ilang {
22 
25 class Expr : public Ast, public std::enable_shared_from_this<Expr> {
26 public:
28  typedef std::shared_ptr<Expr> ExprPtr;
30  typedef std::vector<ExprPtr> ExprPtrVec;
31 
32  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
34  Expr();
36  Expr(const std::string& name);
38  virtual ~Expr();
39 
40  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
42  inline const SortPtr sort() const { return sort_; }
44  inline size_t arg_num() const { return args_.size(); }
46  inline ExprPtr arg(const size_t& i) const { return args_.at(i); }
48  inline size_t param_num() const { return params_.size(); }
50  inline int param(const size_t& i) const { return params_.at(i); }
51 
53  void set_sort(const SortPtr sort);
55  void set_args(const ExprPtrVec& args);
57  void set_params(const std::vector<int> params);
59  void replace_arg(const int& idx, const ExprPtr arg);
61  void replace_arg(const ExprPtr a, const ExprPtr b);
62 
64  bool is_expr() const { return true; }
65 
67  virtual bool is_const() const { return false; }
69  virtual bool is_var() const { return false; }
71  virtual bool is_op() const { return false; }
72 
74  inline bool is_bool() const { return sort_->is_bool(); }
76  inline bool is_bv(const int& width = 0) const { return sort_->is_bv(width); }
78  inline bool is_mem() const { return sort_->is_mem(); }
79 
80  // ------------------------- METHODS -------------------------------------- //
82  virtual z3::expr GetZ3Expr(z3::context& z3_ctx, const Z3ExprVec& z3expr_vec,
83  const std::string& suffix = "") const = 0;
84 
86  virtual std::ostream& Print(std::ostream& out) const = 0;
87 
89  friend std::ostream& operator<<(std::ostream& out, const ExprPtr expr) {
90  return expr->Print(out);
91  }
92 
95  template <class F> void DepthFirstVisit(F& func) {
96  for (size_t i = 0; i != arg_num(); i++) {
97  const ExprPtr arg_i = this->arg(i);
98  arg_i->DepthFirstVisit<F>(func);
99  }
100  func(shared_from_this());
101  }
102 
105  template <class F> void DepthFirstVisitPrePost(F& func) {
106  // pre check
107  if (func.pre(shared_from_this())) { // break if return true
108  return;
109  }
110  // traverse child
111  for (size_t i = 0; i != arg_num(); i++) {
112  auto arg_i = this->arg(i);
113  arg_i->DepthFirstVisitPrePost<F>(func);
114  }
115  // post
116  func.post(shared_from_this());
117  }
118 
119 private:
120  // ------------------------- MEMBERS -------------------------------------- //
122  SortPtr sort_;
124  ExprPtrVec args_;
126  std::vector<int> params_;
127 
128  // ------------------------- HELPERS -------------------------------------- //
129 
130 }; // class Expr
131 
136 
139 class ExprHash {
140 public:
142  size_t operator()(const ExprPtr expr) const { return expr->name().id(); }
143 }; // class ExprHash
144 
146 typedef std::unordered_map<const ExprPtr, const ExprPtr, ExprHash> ExprMap;
148 typedef std::unordered_set<ExprPtr, ExprHash> ExprSet;
149 
150 } // namespace ilang
151 
152 #endif // ILANG_ILA_AST_EXPR_H__
ilang::ExprPtr
Expr::ExprPtr ExprPtr
Pointer type for normal use of Expr.
Definition: expr.h:133
ilang::Ast
The class for the Abstract Syntax Tree. An Ast object can be an expression or function definition (in...
Definition: ast.h:20
ilang::Z3ExprVec
std::vector< z3::expr > Z3ExprVec
Vector type for z3 expression.
Definition: defines.h:18
ilang::Expr::is_expr
bool is_expr() const
Is type expr (object).
Definition: expr.h:64
ast.h
ilang::Expr::is_op
virtual bool is_op() const
Return true if this is an operation.
Definition: expr.h:71
ilang::Expr::Expr
Expr()
Default constructor.
ilang::Expr::replace_arg
void replace_arg(const int &idx, const ExprPtr arg)
Replace the i-th argument.
ilang::ExprPtrVec
Expr::ExprPtrVec ExprPtrVec
Type for storing a set of Expr.
Definition: expr.h:135
ilang::Expr::ExprPtr
std::shared_ptr< Expr > ExprPtr
Pointer type for normal use of Expr.
Definition: expr.h:28
ilang::Expr::sort
const SortPtr sort() const
Return the pointer of the sort.
Definition: expr.h:42
defines.h
ilang::Expr::param
int param(const size_t &i) const
Return the i-th paramter.
Definition: expr.h:50
ilang::Expr::param_num
size_t param_num() const
Return the number of parameters.
Definition: expr.h:48
ilang::Expr::is_mem
bool is_mem() const
Return true if this is an Array expression.
Definition: expr.h:78
ilang::Expr::operator<<
friend std::ostream & operator<<(std::ostream &out, const ExprPtr expr)
Overload output stream operator for pointer.
Definition: expr.h:89
ilang::Expr::is_bv
bool is_bv(const int &width=0) const
Return true if this is a Bitvector expression.
Definition: expr.h:76
ilang::Expr
The class for expression, which is the basic type for variables, constraints, state update expression...
Definition: expr.h:25
ilang::Expr::set_sort
void set_sort(const SortPtr sort)
Set the sort of the expression.
ilang::Expr::arg
ExprPtr arg(const size_t &i) const
Return the i-th argument.
Definition: expr.h:46
ilang::ExprSet
std::unordered_set< ExprPtr, ExprHash > ExprSet
Type for storing a set of Expr.
Definition: expr.h:148
ilang::ExprMap
std::unordered_map< const ExprPtr, const ExprPtr, ExprHash > ExprMap
Type for mapping between Expr.
Definition: expr.h:146
ilang::SortPtr
Sort::SortPtr SortPtr
Pointer type for storing/passing Sort.
Definition: sort.h:76
ilang::ExprHash::operator()
size_t operator()(const ExprPtr expr) const
Function object for hashing.
Definition: expr.h:142
ilang::Expr::DepthFirstVisitPrePost
void DepthFirstVisitPrePost(F &func)
Templated visitor: visit each node in a depth-first order and apply the function object F pre/pose on...
Definition: expr.h:105
ilang
ilang::Expr::is_var
virtual bool is_var() const
Return true if this is a variable.
Definition: expr.h:69
ilang::Expr::GetZ3Expr
virtual z3::expr GetZ3Expr(z3::context &z3_ctx, const Z3ExprVec &z3expr_vec, const std::string &suffix="") const =0
Return the z3 expression for the node.
sort.h
ilang::Expr::~Expr
virtual ~Expr()
Default destructor.
ilang::Expr::arg_num
size_t arg_num() const
Retrun the number of argument (arity).
Definition: expr.h:44
ilang::Expr::is_bool
bool is_bool() const
Return true if this is a Boolean expression.
Definition: expr.h:74
ilang::Object::name
const Symbol & name() const
Get the symbol (name).
ilang::Expr::set_args
void set_args(const ExprPtrVec &args)
Set the arguments.
ilang::Expr::set_params
void set_params(const std::vector< int > params)
Set the parameters.
ilang::ExprHash
The function object for hashing Expr. The hash value is the id of the symbol, which is supposed to be...
Definition: expr.h:139
ilang::Expr::ExprPtrVec
std::vector< ExprPtr > ExprPtrVec
Type for storing a set of Expr.
Definition: expr.h:30
ilang::Expr::Print
virtual std::ostream & Print(std::ostream &out) const =0
Output to stream.
ilang::Expr::DepthFirstVisit
void DepthFirstVisit(F &func)
Templated visitor: visit each node in a depth-first order and apply the function object F on it.
Definition: expr.h:95
ilang::Expr::is_const
virtual bool is_const() const
Return true if this is a constant.
Definition: expr.h:67