z3_helper.h File Reference

#include <string>
#include <ilang/config.h>
#include <ilang/ila/ast/sort_value.h>
#include <z3++.h>

Go to the source code of this file.

Namespaces
	ilang

Functions
BvValType	ilang::Z3BvVal (const BvValType &bv_val)
	Interface z3 bit-vector constant numeric.
z3::expr	ilang::Z3Implies (z3::context &ctx, const z3::expr &a, const z3::expr &b)
	Interface z3 implies ast node construction.
z3::expr	ilang::Z3Shl (z3::context &ctx, const z3::expr &a, const z3::expr &b)
	Interface z3 shl ast node construction.
z3::expr	ilang::Z3Ashr (z3::context &ctx, const z3::expr &a, const z3::expr &b)
	Interface z3 ashr ast node construction.
z3::expr	ilang::Z3Lshr (z3::context &ctx, const z3::expr &a, const z3::expr &b)
	Interface z3 lshr ast node construction.
z3::expr	ilang::Z3SRem (z3::context &ctx, const z3::expr &a, const z3::expr &b)
	Interface z3 shl ast node construction.
z3::expr	ilang::Z3URem (z3::context &ctx, const z3::expr &a, const z3::expr &b)
	Interface z3 shl ast node construction.
z3::expr	ilang::Z3SMod (z3::context &ctx, const z3::expr &a, const z3::expr &b)
	Interface z3 shl ast node construction.
z3::expr	ilang::Z3ZExt (z3::context &ctx, const z3::expr &e, const unsigned &w)
	Interface z3 zext ast node construction.
z3::expr	ilang::Z3SExt (z3::context &ctx, const z3::expr &e, const unsigned &w)
	Interface z3 sext ast node construction.
z3::expr	ilang::Z3LRotate (z3::context &ctx, z3::expr &e, unsigned &w)
	Interface z3 left rotate ast node construction.
z3::expr	ilang::Z3RRotate (z3::context &ctx, z3::expr &e, unsigned &w)
	Interface z3 right rotate ast node construction.
std::string	ilang::Z3Expr2String (z3::context &ctx, const z3::expr &e)
	Return the output string of the given z3::expr.

Detailed Description

Header for helpers for interfacing the z3 API