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	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.
Public Member Functions inherited from ast
	ast (context &c)
	ast (context &c, Z3_ast n)
	ast (ast const &s)
	~ast ()
	operator Z3_ast () const
	operator bool () const
ast &	operator= (ast const &s)
Z3_ast_kind	kind () const
unsigned	hash () const
Public Member Functions inherited from object
	object (context &c)
	object (object const &s)
context &	ctx () const
void	check_error () const

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	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)

Additional Inherited Members
Protected Attributes inherited from ast
Z3_ast	m_ast

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 427 of file z3++.h.

Constructor & Destructor Documentation

expr ( context &  c )

inline

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

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

:ast(c) {}

expr ( context &  c, Z3_ast  n  )

inline

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

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

expr ( expr const &  n )

inline

Definition at line 431 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 530 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 537 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 515 of file z3++.h.

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

sort get_sort ( ) const

inline

Return the sort of this expression.

Definition at line 437 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::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); }

bool is_app ( ) const

inline

Return true if this expression is an application.

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

Referenced by expr::is_const(), 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 454 of file z3++.h.

{ return get_sort().is_arith(); }

bool is_array ( ) const

inline

Return true if this is a Array expression.

Definition at line 462 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 442 of file z3++.h.

Referenced by solver::add().

{ return get_sort().is_bool(); }

bool is_bv ( ) const

inline

Return true if this is a Bit-vector expression.

Definition at line 458 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 492 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 466 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 479 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 446 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 484 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 496 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 450 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 470 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 500 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 505 of file z3++.h.

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

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 522 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 507 of file z3++.h.

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

expr& operator= ( expr const &  n )

inline

Definition at line 432 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 838 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 842 of file z3++.h.

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

Friends And Related Function Documentation

expr implies ( expr const &  a, expr const &  b  )

friend

Definition at line 610 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 operator! ( expr const &  a )

friend

Return an expression representing not(a).

Precondition

a.is_bool()

Definition at line 544 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 627 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 634 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 635 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 821 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 822 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 823 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 557 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 572 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 579 of file z3++.h.

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

expr operator* ( expr const &  a, expr const &  b  )

friend

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

                                                              {
            check_context(a, b);
            Z3_ast r;
            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 674 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 675 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 637 of file z3++.h.

                                                              {
            check_context(a, b);
            Z3_ast r;
            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 654 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 655 of file z3++.h.

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

expr operator- ( expr const &  a )

friend

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

                                              {
            Z3_ast r;
            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 725 of file z3++.h.

                                                              {
            check_context(a, b);
            Z3_ast r;
            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 742 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 743 of file z3++.h.

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

expr operator/ ( expr const &  a, expr const &  b  )

friend

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

                                                              {
            check_context(a, b);
            Z3_ast r;
            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 706 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 707 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 783 of file z3++.h.

                                                              {
            check_context(a, b);
            Z3_ast r;
            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 799 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 800 of file z3++.h.

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

expr operator<= ( expr const &  a, expr const &  b  )

friend

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

                                                               {
            check_context(a, b);
            Z3_ast r;
            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 761 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 762 of file z3++.h.

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

expr operator== ( expr const &  a, expr const &  b  )

friend

Definition at line 618 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 624 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 625 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 802 of file z3++.h.

                                                              {
            check_context(a, b);
            Z3_ast r;
            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 818 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 819 of file z3++.h.

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

expr operator>= ( expr const &  a, expr const &  b  )

friend

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

                                                               {
            check_context(a, b);
            Z3_ast r;
            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 780 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 781 of file z3++.h.

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

expr operator^ ( expr const &  a, expr const &  b  )

friend

Definition at line 825 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 826 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 827 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 829 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 830 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 831 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 587 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 601 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 608 of file z3++.h.

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

expr operator~ ( expr const &  a )

friend

Definition at line 833 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 680 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 687 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 688 of file z3++.h.

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