4 #ifndef ILANG_ILA_AST_HUB_H__
5 #define ILANG_ILA_AST_HUB_H__
20 return expr->sort()->uid();
25 return std::dynamic_pointer_cast<ExprOp>(expr)->uid();
32 ExprPtr NewBoolVar(
const std::string& name);
34 ExprPtr NewBvVar(
const std::string& name,
const int& bit_width);
36 ExprPtr NewMemVar(
const std::string& name,
const int& addr_width,
37 const int& data_width);
52 const int& data_width);
55 const int& data_width);
183 bool SetMemSize(
const ExprPtr& mem,
const int& size = 0);
185 int GetMemSize(
const ExprPtr& mem);
234 #endif // ILANG_ILA_AST_HUB_H__
ExprRef BvConst(const NumericType &bv_val, const int &bit_width)
Return a bit-vector constant.
ExprRef SRem(const ExprRef &a, const ExprRef &b)
Arithmetic signed remainder.
ExprRef LRotate(const ExprRef &bv, const int &immediate)
Left-rotate the bit-vector with immediate number of times.
Expr::ExprPtr ExprPtr
Pointer type for normal use of Expr.
Definition: expr.h:138
ExprRef Ule(const ExprRef &a, const ExprRef &b)
Unsigned less than or equal to (bit-vectors only).
AstUidSort
Unified ID for Sort.
Definition: sort.h:18
ExprRef URem(const ExprRef &a, const ExprRef &b)
Arithmetic unsigned remainder.
AstUidExprOp
Unified ID for ExprOp.
Definition: expr_op.h:14
ExprRef Lshr(const ExprRef &a, const ExprRef &b)
Logical right shift for bit-vectors.
ExprRef Uge(const ExprRef &a, const ExprRef &b)
Unsigned greater than or equal to (bit-vectors only).
ExprRef Store(const ExprRef &mem, const ExprRef &addr, const ExprRef &data)
Store to memory.
ExprRef ZExt(const ExprRef &bv, const int &length)
Zero-extend the bit-vector to the specified length.
ExprRef SMod(const ExprRef &a, const ExprRef &b)
Arithmetic signed modular.
ExprRef Ugt(const ExprRef &a, const ExprRef &b)
Unsigned greater than (bit-vectors only).
ExprRef Load(const ExprRef &mem, const ExprRef &addr)
Load from memory.
Func::FuncPtr FuncPtr
Pointer type for normal use of Func.
Definition: func.h:83
ExprRef Imply(const ExprRef &ante, const ExprRef &cons)
Logical imply for Booleans.
ExprRef Extract(const ExprRef &bv, const int &hi, const int &lo)
Extract bit-field in the bit-vector.
Expr::ExprPtrVec ExprPtrVec
Type for storing a set of Expr.
Definition: expr.h:140
ExprRef BoolConst(bool bool_val)
Return a Boolean constant.
ExprRef Ite(const ExprRef &cond, const ExprRef &t, const ExprRef &f)
If-then-else on the Boolean condition.
ExprRef MemConst(const NumericType &def_val, const std::map< NumericType, NumericType > &vals, const int &addr_width, const int &data_width)
Return a memory constant.
ExprRef Concat(const ExprRef &msbv, const ExprRef &lsbv)
Concatenate two bit-vectors.
ExprRef RRotate(const ExprRef &bv, const int &immediate)
Right-rotate the bit-vector with immediate number of times.
ExprRef SExt(const ExprRef &bv, const int &length)
Sign-extend the bit-vector to the specified length.
BvVal::BvValType BvValType
Data type for storing BvVal.
Definition: sort_value.h:103
ExprRef Ult(const ExprRef &a, const ExprRef &b)
Unsigned less than (bit-vectors only).