ilang::Z3ExprAdapter Class Reference

The class for generating z3 expression from an ILA. More...

#include <z3_expr_adapter.h>

Public Member Functions
	Z3ExprAdapter (z3::context &ctx)
	Constructor.
	~Z3ExprAdapter ()
	~Default destructor.
z3::expr	GetExpr (const ExprPtr &expr, const std::string &suffix="")
	Get the z3 expression of the AST node.
void	operator() (const ExprPtr &expr)
	Function object for getting z3 expression.
z3::context &	context () const
	Return the underlying z3 context.
auto	GetShimExpr (const ExprPtr &expr, const std::string &suffix)
	Unified SmtShim interface to get z3::expr.
auto	GetShimFunc (const FuncPtr &func)
	Unified SmtShim interface to get z3::func_decl.
auto	BoolAnd (const z3::expr &a, const z3::expr &b)
	Unified SmtShim interface to AND two boolean z3::expr.
auto	Equal (const z3::expr &a, const z3::expr &b)
	Unified SmtShim interface to EQUAL two z3::expr.

Detailed Description

The class for generating z3 expression from an ILA.

---

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

• z3_expr_adapter.h