Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Friends
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)
exproperator= (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.
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 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 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]
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); }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines