ILAng-Doc/expr__var_8h_source.html

 #ifndef ILANG_ILA_AST_EXPR_VAR_H__

 #define ILANG_ILA_AST_EXPR_VAR_H__


 #include <string>


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


 namespace ilang {


 class ExprVar : public Expr {

 public:

   // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //

   ExprVar(const std::string& name);

   ExprVar(const std::string& name, const int& bit_width);

   ExprVar(const std::string& name, const int& addr_width,

           const int& data_width);


   ~ExprVar();


   // ------------------------- ACCESSORS/MUTATORS --------------------------- //

   bool is_var() 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;


 private:

   // ------------------------- MEMBERS -------------------------------------- //


   // ------------------------- HELPERS -------------------------------------- //

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

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

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


 }; // class ExprVar


 } // namespace ilang


 #endif // ILANG_ILA_AST_EXPR_VAR_H__

ilang::ExprVar::Print
std::ostream & Print(std::ostream &out) const
Output to stream.

ilang::Expr
The class for expression, which is the basic type for variables, constraints, state update expression...
Definition: expr.h:25

ilang::Z3ExprVec
std::vector< z3::expr > Z3ExprVec
Vector type for z3 expression.
Definition: defines.h:19

ilang::ExprVar::GetZ3Expr
z3::expr GetZ3Expr(z3::context &z3_ctx, const Z3ExprVec &z3expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.

ilang::ExprVar::is_var
bool is_var() const
Return true since this is a variable.
Definition: expr_var.h:32

ilang::ExprVar::ExprVar
ExprVar(const std::string &name)
Constructor for Boolean variable.

ilang::ExprVar::~ExprVar
~ExprVar()
Default destructor.

ilang::ExprVar
Expression for variables (bool, bv, or mem). Variable should be the terminating nodes in the AST...
Definition: expr_var.h:16

expr.h

ilang::Object::name
const Symbol & name() const
Get the symbol (name).