#include <Z3Expr.h>

Public Member Functions
	Z3Expr ()

	Z3Expr (const z3::expr &_e)

	Z3Expr (int i)

	Z3Expr (const Z3Expr &z3Expr)

	Z3Expr (float f)

	Z3Expr (double f)

virtual	~Z3Expr ()=default

Z3Expr &	operator= (const Z3Expr &rhs)

const z3::expr &	getExpr () const

u32_t	id () const
	get id

u32_t	hash () const
	get hash id

const std::string	to_string () const

bool	is_numeral () const

bool	is_bool () const

Z3Expr	simplify () const

int64_t	get_numeral_int64 () const

int	get_numeral_int () const

z3::sort	get_sort () const

Static Public Member Functions
static z3::solver &	getSolver ()
	Get z3 solver, singleton design here to make sure we only have one context.

static z3::context &	getContext ()
	Get z3 context, singleton design here to make sure we only have one context.

static void	releaseContext ()
	release z3 context

static void	releaseSolver ()
	release z3 solver

static z3::expr	nullExpr ()
	null expression

static std::string	dumpStr (const Z3Expr &z3Expr)
	output Z3 expression as a string

static u32_t	getExprSize (const Z3Expr &z3Expr)
	get the number of subexpression of a Z3 expression

static Z3Expr	getTrueCond ()
	Return the unique true condition.

static Z3Expr	getFalseCond ()
	Return the unique false condition.

static Z3Expr	NEG (const Z3Expr &z3Expr)
	compute NEG

static Z3Expr	AND (const Z3Expr &lhs, const Z3Expr &rhs)
	compute AND, used for branch condition

static Z3Expr	OR (const Z3Expr &lhs, const Z3Expr &rhs)
	compute OR, used for branch condition

Static Public Attributes
static z3::context *	ctx = nullptr

static z3::solver *	solver = nullptr

Private Attributes
z3::expr	e

Friends
Z3Expr	operator== (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator!= (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator> (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator< (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator<= (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator>= (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator+ (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator- (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator* (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator/ (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator% (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator^ (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator& (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator\| (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	ashr (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	shl (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	int2bv (u32_t n, const Z3Expr &e)

Z3Expr	bv2int (const Z3Expr &e, bool isSigned)

Z3Expr	operator&& (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator\|\| (const Z3Expr &lhs, const Z3Expr &rhs)

Z3Expr	operator! (const Z3Expr &lhs)

Z3Expr	ite (const Z3Expr &cond, const Z3Expr &lhs, const Z3Expr &rhs)

std::ostream &	operator<< (std::ostream &out, const Z3Expr &expr)

bool	eq (const Z3Expr &lhs, const Z3Expr &rhs)

Detailed Description

Definition at line 38 of file Z3Expr.h.

Constructor & Destructor Documentation

◆ Z3Expr() [1/6]

SVF::Z3Expr::Z3Expr ( )

inline

Definition at line 51 of file Z3Expr.h.

             : e(nullExpr())
    {
    }

◆ Z3Expr() [2/6]

SVF::Z3Expr::Z3Expr ( const z3::expr & _e )

inline

Definition at line 55 of file Z3Expr.h.

                             : e(_e)
    {
    }

◆ Z3Expr() [3/6]

SVF::Z3Expr::Z3Expr ( int i )

inline

Definition at line 59 of file Z3Expr.h.

                  : e(getContext().int_val(i))
    {
    }

◆ Z3Expr() [4/6]

SVF::Z3Expr::Z3Expr ( const Z3Expr & z3Expr )

inline

Definition at line 63 of file Z3Expr.h.

                                 : e(z3Expr.getExpr())
    {
    }

◆ Z3Expr() [5/6]

SVF::Z3Expr::Z3Expr ( float f )

inline

Definition at line 67 of file Z3Expr.h.

                    : Z3Expr((double) f)
    {
    }

◆ Z3Expr() [6/6]

SVF::Z3Expr::Z3Expr ( double f )

inline

Definition at line 71 of file Z3Expr.h.

                    : e(getContext().real_val(std::to_string(f).c_str()))
    {
    }

◆ ~Z3Expr()

virtual SVF::Z3Expr::~Z3Expr ( )

virtualdefault

Member Function Documentation

◆ AND()

Z3Expr SVF::Z3Expr::AND	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

static

compute AND, used for branch condition

Definition at line 92 of file Z3Expr.cpp.

{
    if (eq(lhs, Z3Expr::getFalseCond()) || eq(rhs, Z3Expr::getFalseCond()))
    {
        return Z3Expr::getFalseCond();
    }
    else if (eq(lhs, Z3Expr::getTrueCond()))
    {
        return rhs;
    }
    else if (eq(rhs, Z3Expr::getTrueCond()))
    {
        return lhs;
    }
    else
    {
        Z3Expr expr = (lhs && rhs).simplify();
        // check subexpression size and option limit
        if (Z3Expr::getExprSize(expr) > Options::MaxZ3Size())
        {
            getSolver().push();
            getSolver().add(expr.getExpr());
            z3::check_result res = getSolver().check();
            getSolver().pop();
            if (res != z3::unsat)
            {
                return lhs;
            }
            else
            {
                return Z3Expr::getFalseCond();
            }
        }
        return expr;
    }
}

◆ dumpStr()

std::string SVF::Z3Expr::dumpStr ( const Z3Expr & z3Expr )

static

output Z3 expression as a string

Definition at line 168 of file Z3Expr.cpp.

{
    std::ostringstream out;
    out << z3Expr.getExpr();
    return out.str();
}

◆ get_numeral_int()

int SVF::Z3Expr::get_numeral_int ( ) const

inline

Definition at line 147 of file Z3Expr.h.

    {
        return e.get_numeral_int();
    }

◆ get_numeral_int64()

int64_t SVF::Z3Expr::get_numeral_int64 ( ) const

inline

Definition at line 142 of file Z3Expr.h.

    {
        return e.get_numeral_int64();
    }

◆ get_sort()

z3::sort SVF::Z3Expr::get_sort ( ) const

inline

Definition at line 274 of file Z3Expr.h.

    {
        return getExpr().get_sort();
    }

◆ getContext()

z3::context & SVF::Z3Expr::getContext ( )

static

Get z3 context, singleton design here to make sure we only have one context.

Definition at line 66 of file Z3Expr.cpp.

{
    if (ctx == nullptr)
    {
        ctx = new z3::context();
    }
    return *ctx;
}

◆ getExpr()

const z3::expr & SVF::Z3Expr::getExpr ( ) const

inline

Definition at line 86 of file Z3Expr.h.

    {
        return e;
    }

◆ getExprSize()

u32_t SVF::Z3Expr::getExprSize ( const Z3Expr & z3Expr )

static

get the number of subexpression of a Z3 expression

Definition at line 76 of file Z3Expr.cpp.

{
    u32_t res = 1;
    if (z3Expr.getExpr().num_args() == 0)
    {
        return 1;
    }
    for (u32_t i = 0; i < z3Expr.getExpr().num_args(); ++i)
    {
        Z3Expr expr = z3Expr.getExpr().arg(i);
        res += getExprSize(expr);
    }
    return res;
}

◆ getFalseCond()

static Z3Expr SVF::Z3Expr::getFalseCond ( )

inlinestatic

Return the unique false condition.

Definition at line 295 of file Z3Expr.h.

    {
        return getContext().bool_val(false);
    }

◆ getSolver()

z3::solver & SVF::Z3Expr::getSolver ( )

static

Get z3 solver, singleton design here to make sure we only have one context.

Definition at line 56 of file Z3Expr.cpp.

{
    if (solver == nullptr)
    {
        solver = new z3::solver(getContext());
    }
    return *solver;
}

◆ getTrueCond()

static Z3Expr SVF::Z3Expr::getTrueCond ( )

inlinestatic

Return the unique true condition.

Definition at line 288 of file Z3Expr.h.

    {
        return getContext().bool_val(true);
    }

◆ hash()

u32_t SVF::Z3Expr::hash ( ) const

inline

get hash id

Definition at line 117 of file Z3Expr.h.

    {
        return e.hash();
    }

◆ id()

u32_t SVF::Z3Expr::id ( ) const

inline

get id

Definition at line 111 of file Z3Expr.h.

    {
        return e.id();
    }

◆ is_bool()

bool SVF::Z3Expr::is_bool ( ) const

inline

Definition at line 132 of file Z3Expr.h.

    {
        return e.is_bool();
    }

◆ is_numeral()

bool SVF::Z3Expr::is_numeral ( ) const

inline

Definition at line 127 of file Z3Expr.h.

    {
        return e.is_numeral();
    }

◆ NEG()

static Z3Expr SVF::Z3Expr::NEG ( const Z3Expr & z3Expr )

inlinestatic

compute NEG

Definition at line 301 of file Z3Expr.h.

    {
        return (!z3Expr).simplify();
    }

◆ nullExpr()

static z3::expr SVF::Z3Expr::nullExpr ( )

inlinestatic

null expression

Definition at line 105 of file Z3Expr.h.

    {
        return getContext().int_const("null");
    }

◆ operator=()

Z3Expr & SVF::Z3Expr::operator= ( const Z3Expr & rhs )

inline

Definition at line 77 of file Z3Expr.h.

    {
        if (this->id() != rhs.id())
        {
            e = rhs.getExpr();
        }
        return *this;
    }

◆ OR()

Z3Expr SVF::Z3Expr::OR	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

static

compute OR, used for branch condition

Definition at line 130 of file Z3Expr.cpp.

{
    if (eq(lhs, Z3Expr::getTrueCond()) || eq(rhs, Z3Expr::getTrueCond()))
    {
        return Z3Expr::getTrueCond();
    }
    else if (eq(lhs, Z3Expr::getFalseCond()))
    {
        return rhs;
    }
    else if (eq(rhs, Z3Expr::getFalseCond()))
    {
        return lhs;
    }
    else
    {
        Z3Expr expr = (lhs || rhs).simplify();
        // check subexpression size and option limit
        if (Z3Expr::getExprSize(expr) > Options::MaxZ3Size())
        {
            getSolver().push();
            getSolver().add(expr.getExpr());
            z3::check_result res = getSolver().check();
            getSolver().pop();
            if (res != z3::unsat)
            {
                return Z3Expr::getTrueCond();
            }
            else
            {
                return Z3Expr::getFalseCond();
            }
        }
        return expr;
    }
}

◆ releaseContext()

void SVF::Z3Expr::releaseContext ( )

static

release z3 context

Definition at line 40 of file Z3Expr.cpp.

{
    if(solver)
        releaseSolver();
    delete ctx;
    ctx = nullptr;
}

◆ releaseSolver()

void SVF::Z3Expr::releaseSolver ( )

static

release z3 solver

Definition at line 49 of file Z3Expr.cpp.

{
    delete solver;
    solver = nullptr;
}

◆ simplify()

Z3Expr SVF::Z3Expr::simplify ( ) const

inline

Definition at line 137 of file Z3Expr.h.

    {
        return e.simplify();
    }

◆ to_string()

const std::string SVF::Z3Expr::to_string ( ) const

inline

Definition at line 122 of file Z3Expr.h.

    {
        return e.to_string();
    }

Friends And Related Symbol Documentation

◆ ashr

Z3Expr ashr	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 223 of file Z3Expr.h.

    {
        return ashr(lhs.getExpr(), rhs.getExpr());
    }

◆ bv2int

Z3Expr bv2int	(	const Z3Expr &	e,
		bool	isSigned
	)

friend

Definition at line 238 of file Z3Expr.h.

    {
        return z3::bv2int(e.getExpr(), isSigned);
    }

◆ eq

bool eq	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 269 of file Z3Expr.h.

    {
        return eq(lhs.getExpr().simplify(), rhs.getExpr().simplify());
    }

◆ int2bv

Z3Expr int2bv	(	u32_t	n,
		const Z3Expr &	e
	)

friend

Definition at line 233 of file Z3Expr.h.

    {
        return int2bv(n, e.getExpr());
    }

◆ ite

Z3Expr ite	(	const Z3Expr &	cond,
		const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 258 of file Z3Expr.h.

    {
        return ite(cond.getExpr(), lhs.getExpr(), rhs.getExpr());
    }

◆ operator!

Z3Expr operator! ( const Z3Expr & lhs )

friend

Definition at line 253 of file Z3Expr.h.

    {
        return !lhs.getExpr();
    }

◆ operator!=

Z3Expr operator!=	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 158 of file Z3Expr.h.

    {
        return lhs.getExpr() != rhs.getExpr();
    }

◆ operator%

Z3Expr operator%	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 203 of file Z3Expr.h.

    {
        return lhs.getExpr() % rhs.getExpr();
    }

◆ operator&

Z3Expr operator&	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 213 of file Z3Expr.h.

    {
        return lhs.getExpr() & rhs.getExpr();
    }

◆ operator&&

Z3Expr operator&&	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 243 of file Z3Expr.h.

    {
        return lhs.getExpr() && rhs.getExpr();
    }

◆ operator*

Z3Expr operator*	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 193 of file Z3Expr.h.

    {
        return lhs.getExpr() * rhs.getExpr();
    }

◆ operator+

Z3Expr operator+	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 183 of file Z3Expr.h.

    {
        return lhs.getExpr() + rhs.getExpr();
    }

◆ operator-

Z3Expr operator-	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 188 of file Z3Expr.h.

    {
        return lhs.getExpr() - rhs.getExpr();
    }

◆ operator/

Z3Expr operator/	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 198 of file Z3Expr.h.

    {
        return lhs.getExpr() / rhs.getExpr();
    }

◆ operator<

Z3Expr operator<	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 168 of file Z3Expr.h.

    {
        return lhs.getExpr() < rhs.getExpr();
    }

◆ operator<<

std::ostream & operator<<	(	std::ostream &	out,
		const Z3Expr &	expr
	)

friend

Definition at line 263 of file Z3Expr.h.

    {
        out << expr.getExpr();
        return out;
    }

◆ operator<=

Z3Expr operator<=	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 173 of file Z3Expr.h.

    {
        return lhs.getExpr() <= rhs.getExpr();
    }

◆ operator==

Z3Expr operator==	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 153 of file Z3Expr.h.

    {
        return lhs.getExpr() == rhs.getExpr();
    }

◆ operator>

Z3Expr operator>	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 163 of file Z3Expr.h.

    {
        return lhs.getExpr() > rhs.getExpr();
    }

◆ operator>=

Z3Expr operator>=	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 178 of file Z3Expr.h.

    {
        return lhs.getExpr() >= rhs.getExpr();
    }

◆ operator^

Z3Expr operator^	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 208 of file Z3Expr.h.

    {
        return lhs.getExpr() ^ rhs.getExpr();
    }

◆ operator|

Z3Expr operator\|	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 218 of file Z3Expr.h.

    {
        return lhs.getExpr() | rhs.getExpr();
    }

◆ operator||

Z3Expr operator\|\|	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 248 of file Z3Expr.h.

    {
        return lhs.getExpr() || rhs.getExpr();
    }

◆ shl

Z3Expr shl	(	const Z3Expr &	lhs,
		const Z3Expr &	rhs
	)

friend

Definition at line 228 of file Z3Expr.h.

    {
        return shl(lhs.getExpr(), rhs.getExpr());
    }

Member Data Documentation

◆ ctx

z3::context * SVF::Z3Expr::ctx = nullptr

static

Definition at line 41 of file Z3Expr.h.

◆ e

z3::expr SVF::Z3Expr::e

private

Definition at line 45 of file Z3Expr.h.

◆ solver

z3::solver * SVF::Z3Expr::solver = nullptr

static

Definition at line 42 of file Z3Expr.h.

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

/home/runner/work/SVF/SVF/svf/include/Util/Z3Expr.h
/home/runner/work/SVF/SVF/svf/lib/Util/Z3Expr.cpp

Public Member Functions

Static Public Member Functions

Static Public Attributes

Private Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Z3Expr() [1/6]

◆ Z3Expr() [2/6]

◆ Z3Expr() [3/6]

◆ Z3Expr() [4/6]

◆ Z3Expr() [5/6]

◆ Z3Expr() [6/6]

◆ ~Z3Expr()

Member Function Documentation

◆ AND()

◆ dumpStr()

◆ get_numeral_int()

◆ get_numeral_int64()

◆ get_sort()

◆ getContext()

◆ getExpr()

◆ getExprSize()

◆ getFalseCond()

◆ getSolver()

◆ getTrueCond()

◆ hash()

◆ id()

◆ is_bool()

◆ is_numeral()

◆ NEG()

◆ nullExpr()

◆ operator=()

◆ OR()

◆ releaseContext()

◆ releaseSolver()

◆ simplify()

◆ to_string()

Friends And Related Symbol Documentation

◆ ashr

◆ bv2int

◆ eq

◆ int2bv

◆ ite

◆ operator!

◆ operator!=

◆ operator%

◆ operator&

◆ operator&&

◆ operator*

◆ operator+

◆ operator-

◆ operator/

◆ operator<

◆ operator<<

◆ operator<=

◆ operator==

◆ operator>

◆ operator>=

◆ operator^

◆ operator|

◆ operator||

◆ shl

Member Data Documentation

◆ ctx

◆ e

◆ solver