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...
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. | |
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) |
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 462 of file z3++.h.
Referenced by expr::arg(), expr::body(), expr::simplify(), and expr::substitute().
:ast(c) {}
Return the i-th argument of this application. This method assumes the expression is an application.
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); }
Return the 'body' of this 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); }
Return the declaration associated with this application. This method assumes the expression is an application.
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); }
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] |
bool is_array | ( | ) | const [inline] |
bool is_bool | ( | ) | const [inline] |
bool is_bv | ( | ) | const [inline] |
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().
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.
Definition at line 512 of file z3++.h.
{ return get_sort().is_finite_domain(); }
bool is_int | ( | ) | const [inline] |
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] |
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.
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 465 of file z3++.h.
{ return static_cast<expr&>(ast::operator=(n)); }
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); }
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); }
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); }
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); }
Create the if-then-else expression ite(c, t, e)
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); }
Return an expression representing not(a)
.
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); }
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); }
Return an expression representing a and b
.
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); }
Return an expression representing a and b
. The C++ Boolean value b
is automatically converted into a Z3 Boolean constant.
Definition at line 607 of file z3++.h.
{ return a && a.ctx().bool_val(b); }
Return an expression representing a and b
. The C++ Boolean value a
is automatically converted into a Z3 Boolean constant.
Definition at line 614 of file z3++.h.
{ return b.ctx().bool_val(a) && b; }
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); }
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); }
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); }
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); }
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); }
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); }
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); }
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); }
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); }
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); }
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); }
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); }
Return an expression representing a or b
.
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); }
Return an expression representing a or b
. The C++ Boolean value b
is automatically converted into a Z3 Boolean constant.
Definition at line 636 of file z3++.h.
{ return a || a.ctx().bool_val(b); }
Return an expression representing a or b
. The C++ Boolean value a
is automatically converted into a Z3 Boolean constant.
Definition at line 643 of file z3++.h.
{ return b.ctx().bool_val(a) || b; }
Definition at line 868 of file z3++.h.
{ Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
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); }