expr Class Reference

A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More...

Inheritance diagram for expr:

Public Member Functions
	expr (context &c)
	expr (context &c, Z3_ast n)
	expr (expr const &n)
expr &	operator= (expr const &n)
sort	get_sort () const
	Return the sort of this expression.
bool	is_bool () const
	Return true if this is a Boolean expression.
bool	is_int () const
	Return true if this is an integer expression.
bool	is_real () const
	Return true if this is a real expression.
bool	is_arith () const
	Return true if this is an integer or real expression.
bool	is_bv () const
	Return true if this is a Bit-vector expression.
bool	is_array () const
	Return true if this is a Array expression.
bool	is_datatype () const
	Return true if this is a Datatype expression.
bool	is_relation () const
	Return true if this is a Relation expression.
bool	is_finite_domain () const
	Return true if this is a Finite-domain expression.
bool	is_numeral () const
	Return true if this expression is a numeral.
bool	is_app () const
	Return true if this expression is an application.
bool	is_const () const
	Return true if this expression is a constant (i.e., an application with 0 arguments).
bool	is_quantifier () const
	Return true if this expression is a quantifier.
bool	is_var () const
	Return true if this expression is a variable.
bool	is_well_sorted () const
	Return true if this expression is well sorted (aka type correct).
	operator Z3_app () const
func_decl	decl () const
	Return the declaration associated with this application. This method assumes the expression is an application.
unsigned	num_args () const
	Return the number of arguments in this application. This method assumes the expression is an application.
expr	arg (unsigned i) const
	Return the i-th argument of this application. This method assumes the expression is an application.
expr	body () const
	Return the 'body' of this quantifier.
expr	extract (unsigned hi, unsigned lo) const
unsigned	lo () const
unsigned	hi () const
expr	simplify () const
	Return a simplified version of this expression.
expr	simplify (params const &p) const
	Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier.
expr	substitute (expr_vector const &src, expr_vector const &dst)
	Apply substitution. Replace src expressions by dst.
expr	substitute (expr_vector const &dst)
	Apply substitution. Replace bound variables by expressions.
Friends
expr	operator! (expr const &a)
	Return an expression representing not(a).
expr	operator&& (expr const &a, expr const &b)
	Return an expression representing a and b.
expr	operator&& (expr const &a, bool b)
	Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
expr	operator&& (bool a, expr const &b)
	Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
expr	operator|| (expr const &a, expr const &b)
	Return an expression representing a or b.
expr	operator|| (expr const &a, bool b)
	Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
expr	operator|| (bool a, expr const &b)
	Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
expr	implies (expr const &a, expr const &b)
expr	implies (expr const &a, bool b)
expr	implies (bool a, expr const &b)
expr	ite (expr const &c, expr const &t, expr const &e)
	Create the if-then-else expression ite(c, t, e)
expr	distinct (expr_vector const &args)
expr	concat (expr const &a, expr const &b)
expr	operator== (expr const &a, expr const &b)
expr	operator== (expr const &a, int b)
expr	operator== (int a, expr const &b)
expr	operator!= (expr const &a, expr const &b)
expr	operator!= (expr const &a, int b)
expr	operator!= (int a, expr const &b)
expr	operator+ (expr const &a, expr const &b)
expr	operator+ (expr const &a, int b)
expr	operator+ (int a, expr const &b)
expr	operator* (expr const &a, expr const &b)
expr	operator* (expr const &a, int b)
expr	operator* (int a, expr const &b)
expr	pw (expr const &a, expr const &b)
	Power operator.
expr	pw (expr const &a, int b)
expr	pw (int a, expr const &b)
expr	operator/ (expr const &a, expr const &b)
expr	operator/ (expr const &a, int b)
expr	operator/ (int a, expr const &b)
expr	operator- (expr const &a)
expr	operator- (expr const &a, expr const &b)
expr	operator- (expr const &a, int b)
expr	operator- (int a, expr const &b)
expr	operator<= (expr const &a, expr const &b)
expr	operator<= (expr const &a, int b)
expr	operator<= (int a, expr const &b)
expr	operator>= (expr const &a, expr const &b)
expr	operator>= (expr const &a, int b)
expr	operator>= (int a, expr const &b)
expr	operator< (expr const &a, expr const &b)
expr	operator< (expr const &a, int b)
expr	operator< (int a, expr const &b)
expr	operator> (expr const &a, expr const &b)
expr	operator> (expr const &a, int b)
expr	operator> (int a, expr const &b)
expr	operator& (expr const &a, expr const &b)
expr	operator& (expr const &a, int b)
expr	operator& (int a, expr const &b)
expr	operator^ (expr const &a, expr const &b)
expr	operator^ (expr const &a, int b)
expr	operator^ (int a, expr const &b)
expr	operator| (expr const &a, expr const &b)
expr	operator| (expr const &a, int b)
expr	operator| (int a, expr const &b)
expr	operator~ (expr const &a)

---

Detailed Description

A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort.

Definition at line 465 of file z3++.h.

---

Constructor & Destructor Documentation

expr

(

context &

c

)

[inline]

Definition at line 467 of file z3++.h.

Referenced by expr::arg(), expr::body(), expr::extract(), expr::simplify(), and expr::substitute().

:ast(c) {}

expr	(	context &	c,
		Z3_ast	n
	)		[inline]

Definition at line 468 of file z3++.h.

:ast(c, reinterpret_cast<Z3_ast>(n)) {}

expr

(

expr const &

n

)

[inline]

Definition at line 469 of file z3++.h.

:ast(n) {}

---

Member Function Documentation

expr arg

(

unsigned

i

)

const [inline]

Return the i-th argument of this application. This method assumes the expression is an application.

Precondition:

is_app()

i < num_args()

Definition at line 568 of file z3++.h.

Referenced by ExprRef::children().

{ Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }

expr body

(

)

const [inline]

Return the 'body' of this quantifier.

Precondition:

is_quantifier()

Definition at line 575 of file z3++.h.

Referenced by QuantifierRef::children().

{ assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }

func_decl decl

(

)

const [inline]

Return the declaration associated with this application. This method assumes the expression is an application.

Precondition:

is_app()

Definition at line 553 of file z3++.h.

Referenced by expr::hi(), and expr::lo().

{ Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }

expr extract	(	unsigned	hi,
		unsigned	lo
	)		const [inline]

Definition at line 875 of file z3++.h.

{ Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); return expr(ctx(), r); }

sort get_sort

(

)

const [inline]

Return the sort of this expression.

Definition at line 475 of file z3++.h.

Referenced by expr::is_arith(), expr::is_array(), expr::is_bool(), expr::is_bv(), expr::is_datatype(), expr::is_finite_domain(), expr::is_int(), expr::is_real(), expr::is_relation(), z3::pw(), z3::select(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), and z3::ult().

{ Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }

unsigned hi

(

)

const [inline]

Definition at line 877 of file z3++.h.

{ assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); } 

bool is_app

(

)

const [inline]

Return true if this expression is an application.

Definition at line 526 of file z3++.h.

Referenced by expr::hi(), expr::is_const(), expr::lo(), and expr::operator Z3_app().

{ return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }

bool is_arith

(

)

const [inline]

Return true if this is an integer or real expression.

Definition at line 492 of file z3++.h.

Referenced by z3::pw().

{ return get_sort().is_arith(); }

bool is_array

(

)

const [inline]

Return true if this is a Array expression.

Definition at line 500 of file z3++.h.

{ return get_sort().is_array(); }

bool is_bool

(

)

const [inline]

Return true if this is a Boolean expression.

Definition at line 480 of file z3++.h.

Referenced by solver::add(), optimize::add(), and z3::ite().

{ return get_sort().is_bool(); }

bool is_bv

(

)

const [inline]

Return true if this is a Bit-vector expression.

Definition at line 496 of file z3++.h.

{ return get_sort().is_bv(); }

bool is_const

(

)

const [inline]

Return true if this expression is a constant (i.e., an application with 0 arguments).

Definition at line 530 of file z3++.h.

Referenced by solver::add().

{ return is_app() && num_args() == 0; }

bool is_datatype

(

)

const [inline]

Return true if this is a Datatype expression.

Definition at line 504 of file z3++.h.

{ return get_sort().is_datatype(); }

bool is_finite_domain

(

)

const [inline]

Return true if this is a Finite-domain expression.

Remarks:

Finite-domain is special kind of interpreted sort: is_bool(), is_bv() and is_finite_domain() are mutually exclusive.

Definition at line 517 of file z3++.h.

{ return get_sort().is_finite_domain(); }

bool is_int

(

)

const [inline]

Return true if this is an integer expression.

Definition at line 484 of file z3++.h.

{ return get_sort().is_int(); }

bool is_numeral

(

)

const [inline]

Return true if this expression is a numeral.

Definition at line 522 of file z3++.h.

{ return kind() == Z3_NUMERAL_AST; }

bool is_quantifier

(

)

const [inline]

Return true if this expression is a quantifier.

Definition at line 534 of file z3++.h.

Referenced by expr::body().

{ return kind() == Z3_QUANTIFIER_AST; }

bool is_real

(

)

const [inline]

Return true if this is a real expression.

Definition at line 488 of file z3++.h.

{ return get_sort().is_real(); }

bool is_relation

(

)

const [inline]

Return true if this is a Relation expression.

Definition at line 508 of file z3++.h.

{ return get_sort().is_relation(); }

bool is_var

(

)

const [inline]

Return true if this expression is a variable.

Definition at line 538 of file z3++.h.

{ return kind() == Z3_VAR_AST; }

bool is_well_sorted

(

)

const [inline]

Return true if this expression is well sorted (aka type correct).

Definition at line 543 of file z3++.h.

{ bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }

unsigned lo

(

)

const [inline]

Definition at line 876 of file z3++.h.

{ assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); } 

unsigned num_args

(

)

const [inline]

Return the number of arguments in this application. This method assumes the expression is an application.

Precondition:

is_app()

Definition at line 560 of file z3++.h.

Referenced by ExprRef::arg(), ExprRef::children(), and expr::is_const().

{ unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }

operator Z3_app

(

)

const [inline]

Definition at line 545 of file z3++.h.

{ assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }

expr& operator=

(

expr const &

n

)

[inline]

Definition at line 470 of file z3++.h.

{ return static_cast<expr&>(ast::operator=(n)); }

expr simplify

(

)

const [inline]

Return a simplified version of this expression.

Definition at line 882 of file z3++.h.

{ Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }

expr simplify

(

params const &

p

)

const [inline]

Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier.

Definition at line 886 of file z3++.h.

{ Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }

expr substitute	(	expr_vector const &	src,
		expr_vector const &	dst
	)		[inline]

Apply substitution. Replace src expressions by dst.

Definition at line 1889 of file z3++.h.

                                                                               {
        assert(src.size() == dst.size());
        array<Z3_ast> _src(src.size());
        array<Z3_ast> _dst(dst.size());    
        for (unsigned i = 0; i < src.size(); ++i) {
            _src[i] = src[i];
            _dst[i] = dst[i];
        }
        Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
        check_error();
        return expr(ctx(), r);
    }

expr substitute

(

expr_vector const &

dst

)

[inline]

Apply substitution. Replace bound variables by expressions.

Definition at line 1902 of file z3++.h.

                                                       {
        array<Z3_ast> _dst(dst.size());
        for (unsigned i = 0; i < dst.size(); ++i) {
            _dst[i] = dst[i];
        }
        Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
        check_error();
        return expr(ctx(), r);
    }

---

Friends And Related Function Documentation

expr concat	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 1118 of file z3++.h.

                                                     {
        check_context(a, b);
        Z3_ast r = Z3_mk_concat(a.ctx(), a, b);
        a.ctx().check_error();
        return expr(a.ctx(), r);
    }

expr distinct

(

expr_vector const &

args

)

[friend]

Definition at line 1109 of file z3++.h.

                                                  {
        assert(args.size() > 0);
        context& ctx = args[0].ctx();
        array<Z3_ast> _args(args);
        Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
        ctx.check_error();
        return expr(ctx, r);
    }

expr implies	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 650 of file z3++.h.

                                                            {
            check_context(a, b);
            assert(a.is_bool() && b.is_bool());
            Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
            a.check_error();
            return expr(a.ctx(), r);
        }

expr implies	(	expr const &	a,
		bool	b
	)		[friend]

Definition at line 900 of file z3++.h.

{ return implies(a, a.ctx().bool_val(b)); }

expr implies	(	bool	a,
		expr const &	b
	)		[friend]

Definition at line 901 of file z3++.h.

{ return implies(b.ctx().bool_val(a), b); }

expr ite	(	expr const &	c,
		expr const &	t,
		expr const &	e
	)		[friend]

Create the if-then-else expression ite(c, t, e)

Precondition:

c.is_bool()

Definition at line 923 of file z3++.h.

                                                                    {
        check_context(c, t); check_context(c, e);
        assert(c.is_bool());
        Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
        c.check_error();
        return expr(c.ctx(), r);
    }

expr operator!

(

expr const &

a

)

[friend]

Return an expression representing not(a).

Precondition:

a.is_bool()

Definition at line 582 of file z3++.h.

                                              {
            assert(a.is_bool());
            Z3_ast r = Z3_mk_not(a.ctx(), a);
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator!=	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 674 of file z3++.h.

                                                               {
            check_context(a, b);
            Z3_ast args[2] = { a, b };
            Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator!=	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 681 of file z3++.h.

{ assert(a.is_arith() || a.is_bv()); return a != a.ctx().num_val(b, a.get_sort()); }

expr operator!=	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 682 of file z3++.h.

{ assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) != b; }

expr operator&	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 862 of file z3++.h.

{ check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }

expr operator&	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 863 of file z3++.h.

{ return a & a.ctx().num_val(b, a.get_sort()); }

expr operator&	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 864 of file z3++.h.

{ return b.ctx().num_val(a, b.get_sort()) & b; }

expr operator&&	(	expr const &	a,
		expr const &	b
	)		[friend]

Return an expression representing a and b.

Precondition:

a.is_bool()

b.is_bool()

Definition at line 596 of file z3++.h.

                                                               {
            check_context(a, b);
            assert(a.is_bool() && b.is_bool());
            Z3_ast args[2] = { a, b };
            Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator&&	(	expr const &	a,
		bool	b
	)		[friend]

Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.

Precondition:

a.is_bool()

Definition at line 612 of file z3++.h.

{ return a && a.ctx().bool_val(b); }

expr operator&&	(	bool	a,
		expr const &	b
	)		[friend]

Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.

Precondition:

b.is_bool()

Definition at line 619 of file z3++.h.

{ return b.ctx().bool_val(a) && b; }

expr operator*	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 704 of file z3++.h.

                                                              {
            check_context(a, b);
            Z3_ast r = 0;
            if (a.is_arith() && b.is_arith()) {
                Z3_ast args[2] = { a, b };
                r = Z3_mk_mul(a.ctx(), 2, args);
            }
            else if (a.is_bv() && b.is_bv()) {
                r = Z3_mk_bvmul(a.ctx(), a, b);
            }
            else {
                // operator is not supported by given arguments.
                assert(false);
            }
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator*	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 721 of file z3++.h.

{ return a * a.ctx().num_val(b, a.get_sort()); }

expr operator*	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 722 of file z3++.h.

{ return b.ctx().num_val(a, b.get_sort()) * b; }

expr operator+	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 684 of file z3++.h.

                                                              {
            check_context(a, b);
            Z3_ast r = 0;
            if (a.is_arith() && b.is_arith()) {
                Z3_ast args[2] = { a, b };
                r = Z3_mk_add(a.ctx(), 2, args);
            }
            else if (a.is_bv() && b.is_bv()) {
                r = Z3_mk_bvadd(a.ctx(), a, b);
            }
            else {
                // operator is not supported by given arguments.
                assert(false);
            }
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator+	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 701 of file z3++.h.

{ return a + a.ctx().num_val(b, a.get_sort()); }

expr operator+	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 702 of file z3++.h.

{ return b.ctx().num_val(a, b.get_sort()) + b; }

expr operator-

(

expr const &

a

)

[friend]

Definition at line 750 of file z3++.h.

                                              {
            Z3_ast r = 0;
            if (a.is_arith()) {
                r = Z3_mk_unary_minus(a.ctx(), a);
            }
            else if (a.is_bv()) {
                r = Z3_mk_bvneg(a.ctx(), a);
            }
            else {
                // operator is not supported by given arguments.
                assert(false);
            }
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator-	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 766 of file z3++.h.

                                                              {
            check_context(a, b);
            Z3_ast r = 0;
            if (a.is_arith() && b.is_arith()) {
                Z3_ast args[2] = { a, b };
                r = Z3_mk_sub(a.ctx(), 2, args);
            }
            else if (a.is_bv() && b.is_bv()) {
                r = Z3_mk_bvsub(a.ctx(), a, b);
            }
            else {
                // operator is not supported by given arguments.
                assert(false);
            }
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator-	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 783 of file z3++.h.

{ return a - a.ctx().num_val(b, a.get_sort()); }

expr operator-	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 784 of file z3++.h.

{ return b.ctx().num_val(a, b.get_sort()) - b; }

expr operator/	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 731 of file z3++.h.

                                                              {
            check_context(a, b);
            Z3_ast r = 0;
            if (a.is_arith() && b.is_arith()) {
                r = Z3_mk_div(a.ctx(), a, b);
            }
            else if (a.is_bv() && b.is_bv()) {
                r = Z3_mk_bvsdiv(a.ctx(), a, b);
            }
            else {
                // operator is not supported by given arguments.
                assert(false);
            }
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator/	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 747 of file z3++.h.

{ return a / a.ctx().num_val(b, a.get_sort()); }

expr operator/	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 748 of file z3++.h.

{ return b.ctx().num_val(a, b.get_sort()) / b; }

expr operator<	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 824 of file z3++.h.

                                                              {
            check_context(a, b);
            Z3_ast r = 0;
            if (a.is_arith() && b.is_arith()) {
                r = Z3_mk_lt(a.ctx(), a, b);
            }
            else if (a.is_bv() && b.is_bv()) {
                r = Z3_mk_bvslt(a.ctx(), a, b);
            }
            else {
                // operator is not supported by given arguments.
                assert(false);
            }
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator<	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 840 of file z3++.h.

{ return a < a.ctx().num_val(b, a.get_sort()); }

expr operator<	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 841 of file z3++.h.

{ return b.ctx().num_val(a, b.get_sort()) < b; }

expr operator<=	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 786 of file z3++.h.

                                                               {
            check_context(a, b);
            Z3_ast r = 0;
            if (a.is_arith() && b.is_arith()) {
                r = Z3_mk_le(a.ctx(), a, b);
            }
            else if (a.is_bv() && b.is_bv()) {
                r = Z3_mk_bvsle(a.ctx(), a, b);
            }
            else {
                // operator is not supported by given arguments.
                assert(false);
            }
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator<=	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 802 of file z3++.h.

{ return a <= a.ctx().num_val(b, a.get_sort()); }

expr operator<=	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 803 of file z3++.h.

{ return b.ctx().num_val(a, b.get_sort()) <= b; }

expr operator==	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 665 of file z3++.h.

                                                               {
            check_context(a, b);
            Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator==	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 671 of file z3++.h.

{ assert(a.is_arith() || a.is_bv()); return a == a.ctx().num_val(b, a.get_sort()); }

expr operator==	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 672 of file z3++.h.

{ assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) == b; }

expr operator>	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 843 of file z3++.h.

                                                              {
            check_context(a, b);
            Z3_ast r = 0;
            if (a.is_arith() && b.is_arith()) {
                r = Z3_mk_gt(a.ctx(), a, b);
            }
            else if (a.is_bv() && b.is_bv()) {
                r = Z3_mk_bvsgt(a.ctx(), a, b);
            }
            else {
                // operator is not supported by given arguments.
                assert(false);
            }
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator>	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 859 of file z3++.h.

{ return a > a.ctx().num_val(b, a.get_sort()); }

expr operator>	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 860 of file z3++.h.

{ return b.ctx().num_val(a, b.get_sort()) > b; }

expr operator>=	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 805 of file z3++.h.

                                                               {
            check_context(a, b);
            Z3_ast r = 0;
            if (a.is_arith() && b.is_arith()) {
                r = Z3_mk_ge(a.ctx(), a, b);
            }
            else if (a.is_bv() && b.is_bv()) {
                r = Z3_mk_bvsge(a.ctx(), a, b);
            }
            else {
                // operator is not supported by given arguments.
                assert(false);
            }
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator>=	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 821 of file z3++.h.

{ return a >= a.ctx().num_val(b, a.get_sort()); }

expr operator>=	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 822 of file z3++.h.

{ return b.ctx().num_val(a, b.get_sort()) >= b; }

expr operator^	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 866 of file z3++.h.

{ check_context(a, b); Z3_ast r = Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }

expr operator^	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 867 of file z3++.h.

{ return a ^ a.ctx().num_val(b, a.get_sort()); }

expr operator^	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 868 of file z3++.h.

{ return b.ctx().num_val(a, b.get_sort()) ^ b; }

expr operator|	(	expr const &	a,
		expr const &	b
	)		[friend]

Definition at line 870 of file z3++.h.

{ check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }

expr operator|	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 871 of file z3++.h.

{ return a | a.ctx().num_val(b, a.get_sort()); }

expr operator|	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 872 of file z3++.h.

{ return b.ctx().num_val(a, b.get_sort()) | b; }

expr operator||	(	expr const &	a,
		expr const &	b
	)		[friend]

Return an expression representing a or b.

Precondition:

a.is_bool()

b.is_bool()

Definition at line 627 of file z3++.h.

                                                               {
            check_context(a, b);
            assert(a.is_bool() && b.is_bool());
            Z3_ast args[2] = { a, b };
            Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
            a.check_error();
            return expr(a.ctx(), r);
        }

expr operator||	(	expr const &	a,
		bool	b
	)		[friend]

Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.

Precondition:

a.is_bool()

Definition at line 641 of file z3++.h.

{ return a || a.ctx().bool_val(b); }

expr operator||	(	bool	a,
		expr const &	b
	)		[friend]

Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.

Precondition:

b.is_bool()

Definition at line 648 of file z3++.h.

{ return b.ctx().bool_val(a) || b; }

expr operator~

(

expr const &

a

)

[friend]

Definition at line 874 of file z3++.h.

{ Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }

expr pw	(	expr const &	a,
		expr const &	b
	)		[friend]

Power operator.

Definition at line 903 of file z3++.h.

                                                   {
        assert(a.is_arith() && b.is_arith());
        check_context(a, b);
        Z3_ast r = Z3_mk_power(a.ctx(), a, b);
        a.check_error();
        return expr(a.ctx(), r);
    }

expr pw	(	expr const &	a,
		int	b
	)		[friend]

Definition at line 910 of file z3++.h.

{ return pw(a, a.ctx().num_val(b, a.get_sort())); }

expr pw	(	int	a,
		expr const &	b
	)		[friend]

Definition at line 911 of file z3++.h.

{ return pw(b.ctx().num_val(a, b.get_sort()), b); }