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. 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... | |
![]() | |
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 |
![]() | |
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 | |
![]() | |
Z3_ast | m_ast |
![]() | |
context * | m_ctx |
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.
|
inline |
Return the i-th argument of this application. This method assumes the expression is an application.
Definition at line 568 of file z3++.h.
Referenced by ExprRef::children().
|
inline |
Return the 'body' of this quantifier.
Definition at line 575 of file z3++.h.
Referenced by QuantifierRef::children().
|
inline |
|
inline |
|
inline |
Return the sort of this expression.
Definition at line 475 of file z3++.h.
Referenced by z3::pw(), z3::select(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), and z3::ult().
|
inline |
Definition at line 877 of file z3++.h.
|
inline |
Return true if this expression is an application.
Definition at line 526 of file z3++.h.
|
inline |
Return true if this is an integer or real expression.
Definition at line 492 of file z3++.h.
Referenced by z3::pw().
|
inline |
Return true if this is a Array expression.
Definition at line 500 of file z3++.h.
|
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().
|
inline |
Return true if this is a Bit-vector expression.
Definition at line 496 of file z3++.h.
|
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().
|
inline |
Return true if this is a Datatype expression.
Definition at line 504 of file z3++.h.
|
inline |
Return true if this is a Finite-domain expression.
Definition at line 517 of file z3++.h.
|
inline |
Return true if this is an integer expression.
Definition at line 484 of file z3++.h.
|
inline |
Return true if this expression is a numeral.
Definition at line 522 of file z3++.h.
|
inline |
Return true if this expression is a quantifier.
Definition at line 534 of file z3++.h.
|
inline |
Return true if this is a real expression.
Definition at line 488 of file z3++.h.
|
inline |
Return true if this is a Relation expression.
Definition at line 508 of file z3++.h.
|
inline |
Return true if this expression is a variable.
Definition at line 538 of file z3++.h.
|
inline |
|
inline |
Definition at line 876 of file z3++.h.
|
inline |
Return the number of arguments in this application. This method assumes the expression is an application.
Definition at line 560 of file z3++.h.
Referenced by ExprRef::arg(), and ExprRef::children().
|
inline |
Definition at line 545 of file z3++.h.
|
inline |
|
inline |
Apply substitution. Replace src expressions by dst.
Definition at line 1889 of file z3++.h.
|
inline |
Definition at line 1118 of file z3++.h.
|
friend |
Definition at line 650 of file z3++.h.
Create the if-then-else expression ite(c, t, e)
Definition at line 923 of file z3++.h.
Return an expression representing not(a)
.
Definition at line 582 of file z3++.h.
Definition at line 674 of file z3++.h.
Definition at line 862 of file z3++.h.
Return an expression representing a and b
.
Definition at line 596 of file z3++.h.
Return an expression representing a and b
. The C++ Boolean value b
is automatically converted into a Z3 Boolean constant.
Return an expression representing a and b
. The C++ Boolean value a
is automatically converted into a Z3 Boolean constant.
Definition at line 704 of file z3++.h.
Definition at line 684 of file z3++.h.
Definition at line 766 of file z3++.h.
Definition at line 731 of file z3++.h.
Definition at line 824 of file z3++.h.
Definition at line 786 of file z3++.h.
Definition at line 665 of file z3++.h.
Definition at line 843 of file z3++.h.
Definition at line 805 of file z3++.h.
Definition at line 866 of file z3++.h.
Definition at line 870 of file z3++.h.
Return an expression representing a or b
.
Definition at line 627 of file z3++.h.
Return an expression representing a or b
. The C++ Boolean value b
is automatically converted into a Z3 Boolean constant.
Return an expression representing a or b
. The C++ Boolean value a
is automatically converted into a Z3 Boolean constant.
Power operator.
Definition at line 903 of file z3++.h.