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	extract (unsigned hi, unsigned lo) const
unsigned	lo () const
unsigned	hi () const
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	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. 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 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); }