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. More...
bool	is_bool () const
	Return true if this is a Boolean expression. More...
bool	is_int () const
	Return true if this is an integer expression. More...
bool	is_real () const
	Return true if this is a real expression. More...
bool	is_arith () const
	Return true if this is an integer or real expression. More...
bool	is_bv () const
	Return true if this is a Bit-vector expression. More...
bool	is_array () const
	Return true if this is a Array expression. More...
bool	is_datatype () const
	Return true if this is a Datatype expression. More...
bool	is_relation () const
	Return true if this is a Relation expression. More...
bool	is_finite_domain () const
	Return true if this is a Finite-domain expression. More...
bool	is_numeral () const
	Return true if this expression is a numeral. More...
bool	is_app () const
	Return true if this expression is an application. More...
bool	is_const () const
	Return true if this expression is a constant (i.e., an application with 0 arguments). More...
bool	is_quantifier () const
	Return true if this expression is a quantifier. More...
bool	is_var () const
	Return true if this expression is a variable. More...
bool	is_well_sorted () const
	Return true if this expression is well sorted (aka type correct). More...
	operator Z3_app () const
func_decl	decl () const
	Return the declaration associated with this application. This method assumes the expression is an application. More...
unsigned	num_args () const
	Return the number of arguments in this application. This method assumes the expression is an application. More...
expr	arg (unsigned i) const
	Return the i-th argument of this application. This method assumes the expression is an application. More...
expr	body () const
	Return the 'body' of this quantifier. More...
expr	simplify () const
	Return a simplified version of this expression. More...
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. More...
expr	substitute (expr_vector const &src, expr_vector const &dst)
	Apply substitution. Replace src expressions by dst. More...
expr	substitute (expr_vector const &dst)
	Apply substitution. Replace bound variables by expressions. More...
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). More...
expr	operator&& (expr const &a, expr const &b)
	Return an expression representing a and b. More...
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. More...
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. More...
expr	operator|| (expr const &a, expr const &b)
	Return an expression representing a or b. More...
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. More...
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. More...
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) More...
expr	distinct (expr_vector const &args)
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. More...
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
Protected Attributes inherited from object
context *	m_ctx

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

Constructor & Destructor Documentation

expr ( context &  c )

inline

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

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

:ast(c) {}

expr ( context &  c, Z3_ast  n  )

inline

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

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

expr ( expr const &  n )

inline

Definition at line 464 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 563 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 570 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 548 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 470 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); }

bool is_app ( ) const

inline

Return true if this expression is an application.

Definition at line 521 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 487 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 495 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 475 of file z3++.h.

Referenced by solver::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 491 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 525 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 499 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 512 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 479 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 517 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 529 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 483 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 503 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 533 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 538 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 555 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 540 of file z3++.h.

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

expr& operator= ( expr const &  n )

inline

Definition at line 465 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 873 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 877 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 1790 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 1803 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 distinct ( expr_vector const &  args )

friend

Definition at line 1100 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 645 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 891 of file z3++.h.

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

expr implies ( bool  a, expr const &  b  )

friend

Definition at line 892 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 914 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 577 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 668 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 675 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 676 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 856 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 857 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 858 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 591 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 607 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 614 of file z3++.h.

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

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

friend

Definition at line 698 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 715 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 716 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 678 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 695 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 696 of file z3++.h.

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

expr operator- ( expr const &  a )

friend

Definition at line 744 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 760 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 777 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 778 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 725 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 741 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 742 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 818 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 834 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 835 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 780 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 796 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 797 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 659 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 665 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 666 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 837 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 853 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 854 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 799 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 815 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 816 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 860 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 861 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 862 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 864 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 865 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 866 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 622 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 636 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 643 of file z3++.h.

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

expr operator~ ( expr const &  a )

friend

Definition at line 868 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 894 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 901 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 902 of file z3++.h.

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