ilang::Expr Class Reference

The class for expression, which is the basic type for variables, constraints, state update expressions, etc. More...

#include <expr.h>

Inheritance diagram for ilang::Expr:

Public Types
typedef std::shared_ptr< Expr >	ExprPtr
	Pointer type for normal use of Expr.
typedef std::vector< ExprPtr >	ExprPtrVec
	Type for storing a set of Expr.
Public Types inherited from ilang::Object
typedef std::shared_ptr< Object >	ObjPtr
	Pointer type for normal use of Object.

Public Member Functions
	Expr ()
	Default constructor.
	Expr (const std::string &name)
	Constructor with name.
virtual	~Expr ()
	Default destructor.
const SortPtr	sort () const
	Return the pointer of the sort.
size_t	arg_num () const
	Retrun the number of argument (arity).
ExprPtr	arg (const size_t &i) const
	Return the i-th argument.
size_t	param_num () const
	Return the number of parameters.
int	param (const size_t &i) const
	Return the i-th paramter.
void	set_sort (const SortPtr sort)
	Set the sort of the expression.
void	set_args (const ExprPtrVec &args)
	Set the arguments.
void	set_params (const std::vector< int > params)
	Set the parameters.
void	replace_arg (const int &idx, const ExprPtr &arg)
	Replace the i-th argument.
void	replace_arg (const ExprPtr &a, const ExprPtr &b)
	Replace the "a" argument with "b" argument with "exist".
bool	is_expr () const
	Is type expr (object).
virtual bool	is_const () const
	Return true if this is a constant.
virtual bool	is_var () const
	Return true if this is a variable.
virtual bool	is_op () const
	Return true if this is an operation.
bool	is_bool () const
	Return true if this is a Boolean expression.
bool	is_bv (const int &width=0) const
	Return true if this is a Bitvector expression.
bool	is_mem () const
	Return true if this is an Array expression.
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.
virtual std::ostream &	Print (std::ostream &out) const =0
	Output to stream.
template<class F >
void	DepthFirstVisit (F &func)
	Templated visitor: visit each node in a depth-first order and apply the function object F on it.
template<class F >
void	DepthFirstVisitPrePost (F &func)
	Templated visitor: visit each node in a depth-first order and apply the function object F pre/pose on it.
Public Member Functions inherited from ilang::Ast
	Ast ()
	Default constructor.
	Ast (const std::string &name)
	Constructor with name.
virtual	~Ast ()
	Default destructor.
bool	is_ast () const
	Is type Ast.
virtual bool	is_func () const
	Is type Ast::Func.
InstrLvlAbsPtr	host () const
	Return the hosting ILA.
void	set_host (const InstrLvlAbsPtr &host)
	Set the hosting ILA.
Public Member Functions inherited from ilang::Object
	Object ()
	Default constructor.
	Object (const std::string &name)
	Constructor with string name.
virtual	~Object ()
	Default destructor.
const Symbol &	name () const
	Get the symbol (name).
virtual bool	is_instr_lvl_abs () const
	Is type InstrLvlAbs.
virtual bool	is_instr () const
	Is type Instr.

Protected Types
typedef std::vector< z3::expr >	Z3ExprVec
	Vector type for z3 expression.
Protected Types inherited from ilang::Ast
typedef std::shared_ptr < InstrLvlAbs >	InstrLvlAbsPtr
	Type for forward declaration of ILA.

Friends
std::ostream &	operator<< (std::ostream &out, const ExprPtr &expr)
	Overload output stream operator for pointer.

Detailed Description

The class for expression, which is the basic type for variables, constraints, state update expressions, etc.

---

The documentation for this class was generated from the following file:

• expr.h