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...
|
| 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_seq () const |
| Return true if this is a sequence expression. More...
|
|
bool | is_re () const |
| Return true if this is a regular expression. More...
|
|
bool | is_finite_domain () const |
| Return true if this is a Finite-domain expression. More...
|
|
bool | is_fpa () const |
| Return true if this is a FloatingPoint expression. . More...
|
|
bool | is_numeral () const |
| Return true if this expression is a numeral. Specialized functions also return representations for the numerals as small integers, 64 bit integers or rational or decimal strings. More...
|
|
bool | is_numeral_i64 (int64_t &i) const |
|
bool | is_numeral_u64 (uint64_t &i) const |
|
bool | is_numeral_i (int &i) const |
|
bool | is_numeral_u (unsigned &i) const |
|
bool | is_numeral (std::string &s) const |
|
bool | is_numeral (std::string &s, unsigned precision) const |
|
bool | is_numeral (double &d) const |
|
bool | as_binary (std::string &s) const |
|
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_forall () const |
| Return true if this expression is a universal quantifier. More...
|
|
bool | is_exists () const |
| Return true if this expression is an existential quantifier. More...
|
|
bool | is_lambda () const |
| Return true if this expression is a lambda expression. More...
|
|
bool | is_var () const |
| Return true if this expression is a variable. More...
|
|
bool | is_algebraic () const |
| Return true if expression is an algebraic number. More...
|
|
bool | is_well_sorted () const |
| Return true if this expression is well sorted (aka type correct). More...
|
|
std::string | get_decimal_string (int precision) const |
| Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic. More...
|
|
expr | algebraic_lower (unsigned precision) const |
|
expr | algebraic_upper (unsigned precision) const |
|
expr_vector | algebraic_poly () const |
| Return coefficients for p of an algebraic number (root-obj p i) More...
|
|
unsigned | algebraic_i () const |
| Return i of an algebraic number (root-obj p i) More...
|
|
unsigned | id () const |
| retrieve unique identifier for expression. More...
|
|
int | get_numeral_int () const |
| Return int value of numeral, throw if result cannot fit in machine int. More...
|
|
unsigned | get_numeral_uint () const |
| Return uint value of numeral, throw if result cannot fit in machine uint. More...
|
|
int64_t | get_numeral_int64 () const |
| Return int64_t value of numeral, throw if result cannot fit in int64_t . More...
|
|
uint64_t | get_numeral_uint64 () const |
| Return uint64_t value of numeral, throw if result cannot fit in uint64_t . More...
|
|
Z3_lbool | bool_value () const |
|
expr | numerator () const |
|
expr | denominator () const |
|
bool | is_string_value () const |
| Return true if this expression is a string literal. The string can be accessed using get_string() and get_escaped_string() More...
|
|
std::string | get_escaped_string () const |
| for a string value expression return an escaped or unescaped string value. More...
|
|
std::string | get_string () const |
|
| operator Z3_app () const |
|
sort | fpa_rounding_mode () |
| Return a RoundingMode sort. More...
|
|
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...
|
|
bool | is_true () const |
|
bool | is_false () const |
|
bool | is_not () const |
|
bool | is_and () const |
|
bool | is_or () const |
|
bool | is_xor () const |
|
bool | is_implies () const |
|
bool | is_eq () const |
|
bool | is_ite () const |
|
bool | is_distinct () const |
|
expr | rotate_left (unsigned i) |
|
expr | rotate_right (unsigned i) |
|
expr | repeat (unsigned i) |
|
expr | extract (unsigned hi, unsigned lo) const |
|
unsigned | lo () const |
|
unsigned | hi () const |
|
expr | extract (expr const &offset, expr const &length) const |
| sequence and regular expression operations. More...
|
|
expr | replace (expr const &src, expr const &dst) const |
|
expr | unit () const |
|
expr | contains (expr const &s) |
|
expr | at (expr const &index) const |
|
expr | nth (expr const &index) const |
|
expr | length () const |
|
expr | stoi () const |
|
expr | itos () const |
|
expr | loop (unsigned lo) |
| create a looping regular expression. More...
|
|
expr | loop (unsigned lo, unsigned hi) |
|
expr | operator[] (expr const &index) const |
|
expr | operator[] (expr_vector const &index) 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 |
|
std::string | to_string () const |
|
| object (context &c) |
|
| object (object const &s) |
|
context & | ctx () const |
|
Z3_error_code | check_error () const |
|
|
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 | mk_or (expr_vector const &args) |
|
expr | mk_and (expr_vector const &args) |
|
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 | concat (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 | sum (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 | pw (expr const &a, expr const &b) |
|
expr | pw (expr const &a, int b) |
|
expr | pw (int a, expr const &b) |
|
expr | mod (expr const &a, expr const &b) |
|
expr | mod (expr const &a, int b) |
|
expr | mod (int a, expr const &b) |
|
expr | rem (expr const &a, expr const &b) |
|
expr | rem (expr const &a, int b) |
|
expr | rem (int a, expr const &b) |
|
expr | is_int (expr const &e) |
|
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 | pble (expr_vector const &es, int const *coeffs, int bound) |
|
expr | pbge (expr_vector const &es, int const *coeffs, int bound) |
|
expr | pbeq (expr_vector const &es, int const *coeffs, int bound) |
|
expr | atmost (expr_vector const &es, unsigned bound) |
|
expr | atleast (expr_vector const &es, unsigned bound) |
|
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 | nand (expr const &a, expr const &b) |
|
expr | nor (expr const &a, expr const &b) |
|
expr | xnor (expr const &a, expr const &b) |
|
expr | min (expr const &a, expr const &b) |
|
expr | max (expr const &a, expr const &b) |
|
expr | bv2int (expr const &a, bool is_signed) |
| bit-vector and integer conversions. More...
|
|
expr | int2bv (unsigned n, expr const &a) |
|
expr | bvadd_no_overflow (expr const &a, expr const &b, bool is_signed) |
| bit-vector overflow/underflow checks More...
|
|
expr | bvadd_no_underflow (expr const &a, expr const &b) |
|
expr | bvsub_no_overflow (expr const &a, expr const &b) |
|
expr | bvsub_no_underflow (expr const &a, expr const &b, bool is_signed) |
|
expr | bvsdiv_no_overflow (expr const &a, expr const &b) |
|
expr | bvneg_no_overflow (expr const &a) |
|
expr | bvmul_no_overflow (expr const &a, expr const &b, bool is_signed) |
|
expr | bvmul_no_underflow (expr const &a, expr const &b) |
|
expr | abs (expr const &a) |
|
expr | sqrt (expr const &a, expr const &rm) |
|
expr | operator~ (expr const &a) |
|
expr | fma (expr const &a, expr const &b, expr const &c, expr const &rm) |
| FloatingPoint fused multiply-add. More...
|
|
expr | range (expr const &lo, expr const &hi) |
|
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 746 of file z3++.h.
◆ expr() [1/3]
Definition at line 748 of file z3++.h.
Referenced by expr::algebraic_lower(), expr::algebraic_upper(), expr::arg(), expr::at(), expr::body(), expr::contains(), expr::denominator(), expr::extract(), expr::itos(), expr::length(), expr::loop(), expr::nth(), expr::numerator(), expr::repeat(), expr::replace(), expr::rotate_left(), expr::rotate_right(), expr::simplify(), expr::stoi(), expr::substitute(), and expr::unit().
◆ expr() [2/3]
Definition at line 749 of file z3++.h.
749 :
ast(c,
reinterpret_cast<Z3_ast
>(n)) {}
◆ expr() [3/3]
◆ algebraic_i()
unsigned algebraic_i |
( |
| ) |
const |
|
inline |
Return i of an algebraic number (root-obj p i)
Definition at line 909 of file z3++.h.
◆ algebraic_lower()
expr algebraic_lower |
( |
unsigned |
precision | ) |
const |
|
inline |
Retrieve lower and upper bounds for algebraic numerals based on a decimal precision
Definition at line 882 of file z3++.h.
◆ algebraic_poly()
Return coefficients for p of an algebraic number (root-obj p i)
Definition at line 899 of file z3++.h.
◆ algebraic_upper()
expr algebraic_upper |
( |
unsigned |
precision | ) |
const |
|
inline |
◆ arg()
expr arg |
( |
unsigned |
i | ) |
const |
|
inline |
◆ as_binary()
bool as_binary |
( |
std::string & |
s | ) |
const |
|
inline |
◆ at()
◆ body()
◆ bool_value()
◆ contains()
◆ decl()
Return the declaration associated with this application. This method assumes the expression is an application.
- Precondition
- is_app()
Definition at line 1060 of file z3++.h.
Referenced by expr::hi(), expr::is_and(), expr::is_distinct(), expr::is_eq(), expr::is_false(), expr::is_implies(), expr::is_ite(), expr::is_not(), expr::is_or(), expr::is_true(), expr::is_xor(), and expr::lo().
◆ denominator()
expr denominator |
( |
| ) |
const |
|
inline |
◆ extract() [1/2]
expr extract |
( |
expr const & |
offset, |
|
|
expr const & |
length |
|
) |
| const |
|
inline |
sequence and regular expression operations.
- is overloaded as sequence concatenation and regular expression union. concat is overloaded to handle sequences and regular expressions
Definition at line 1280 of file z3++.h.
◆ extract() [2/2]
expr extract |
( |
unsigned |
hi, |
|
|
unsigned |
lo |
|
) |
| const |
|
inline |
◆ fpa_rounding_mode()
sort fpa_rounding_mode |
( |
| ) |
|
|
inline |
Return a RoundingMode sort.
Definition at line 1046 of file z3++.h.
1050 return sort(
ctx(), s);
◆ get_decimal_string()
std::string get_decimal_string |
( |
int |
precision | ) |
const |
|
inline |
Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic.
- Precondition
- is_numeral() || is_algebraic()
Definition at line 874 of file z3++.h.
◆ get_escaped_string()
std::string get_escaped_string |
( |
| ) |
const |
|
inline |
for a string value expression return an escaped or unescaped string value.
- Precondition
- expression is for a string value.
Definition at line 1026 of file z3++.h.
1030 return std::string(s);
◆ get_numeral_int()
int get_numeral_int |
( |
| ) |
const |
|
inline |
Return int value of numeral, throw if result cannot fit in machine int.
It only makes sense to use this function if the caller can ensure that the result is an integer or if exceptions are enabled. If exceptions are disabled, then use the is_numeral_i function.
- Precondition
- is_numeral()
Definition at line 931 of file z3++.h.
934 assert(
ctx().enable_exceptions());
935 if (!
ctx().enable_exceptions())
return 0;
936 Z3_THROW(exception(
"numeral does not fit in machine int"));
◆ get_numeral_int64()
int64_t get_numeral_int64 |
( |
| ) |
const |
|
inline |
Return int64_t
value of numeral, throw if result cannot fit in int64_t
.
- Precondition
- is_numeral()
Definition at line 967 of file z3++.h.
971 assert(
ctx().enable_exceptions());
972 if (!
ctx().enable_exceptions())
return 0;
973 Z3_THROW(exception(
"numeral does not fit in machine int64_t"));
◆ get_numeral_uint()
unsigned get_numeral_uint |
( |
| ) |
const |
|
inline |
Return uint value of numeral, throw if result cannot fit in machine uint.
It only makes sense to use this function if the caller can ensure that the result is an integer or if exceptions are enabled. If exceptions are disabled, then use the is_numeral_u function.
- Precondition
- is_numeral()
Definition at line 950 of file z3++.h.
954 assert(
ctx().enable_exceptions());
955 if (!
ctx().enable_exceptions())
return 0;
956 Z3_THROW(exception(
"numeral does not fit in machine uint"));
◆ get_numeral_uint64()
uint64_t get_numeral_uint64 |
( |
| ) |
const |
|
inline |
Return uint64_t
value of numeral, throw if result cannot fit in uint64_t
.
- Precondition
- is_numeral()
Definition at line 984 of file z3++.h.
988 assert(
ctx().enable_exceptions());
989 if (!
ctx().enable_exceptions())
return 0;
990 Z3_THROW(exception(
"numeral does not fit in machine uint64_t"));
◆ get_sort()
Return the sort of this expression.
Definition at line 756 of file z3++.h.
Referenced by z3::ashr(), z3::concat(), expr::is_arith(), expr::is_array(), expr::is_bool(), expr::is_bv(), expr::is_datatype(), expr::is_finite_domain(), expr::is_fpa(), expr::is_int(), expr::is_re(), expr::is_real(), expr::is_relation(), expr::is_seq(), z3::lshr(), z3::mod(), z3::operator!=(), z3::operator&(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::operator^(), z3::operator|(), z3::pw(), z3::rem(), z3::select(), z3::shl(), z3::sle(), z3::slt(), z3::smod(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().
◆ get_string()
std::string get_string |
( |
| ) |
const |
|
inline |
Definition at line 1033 of file z3++.h.
1038 return std::string(s, n);
◆ hi()
◆ id()
retrieve unique identifier for expression.
Definition at line 919 of file z3++.h.
◆ is_algebraic()
bool is_algebraic |
( |
| ) |
const |
|
inline |
◆ is_and()
◆ is_app()
Return true if this expression is an application.
Definition at line 831 of file z3++.h.
Referenced by expr::hi(), expr::is_and(), expr::is_const(), expr::is_distinct(), expr::is_eq(), expr::is_false(), expr::is_implies(), expr::is_ite(), expr::is_not(), expr::is_or(), expr::is_true(), expr::is_xor(), expr::lo(), and expr::operator Z3_app().
◆ is_arith()
Return true if this is an integer or real expression.
Definition at line 773 of file z3++.h.
Referenced by z3::max(), z3::min(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), and z3::operator>=().
◆ is_array()
◆ is_bool()
Return true if this is a Boolean expression.
Definition at line 761 of file z3++.h.
Referenced by solver::add(), optimize::add(), optimize::add_soft(), z3::implies(), z3::ite(), z3::nand(), z3::nor(), z3::operator!(), z3::operator&(), z3::operator&&(), z3::operator^(), z3::operator|(), z3::operator||(), and z3::xnor().
◆ is_bv()
Return true if this is a Bit-vector expression.
Definition at line 777 of file z3++.h.
Referenced by z3::max(), z3::min(), z3::mod(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), and z3::operator>=().
◆ is_const()
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition at line 835 of file z3++.h.
Referenced by solver::add().
◆ is_datatype()
bool is_datatype |
( |
| ) |
const |
|
inline |
Return true if this is a Datatype expression.
Definition at line 785 of file z3++.h.
◆ is_distinct()
bool is_distinct |
( |
| ) |
const |
|
inline |
◆ is_eq()
◆ is_exists()
Return true if this expression is an existential quantifier.
Definition at line 848 of file z3++.h.
◆ is_false()
◆ is_finite_domain()
bool is_finite_domain |
( |
| ) |
const |
|
inline |
Return true if this is a Finite-domain expression.
Definition at line 807 of file z3++.h.
◆ is_forall()
Return true if this expression is a universal quantifier.
Definition at line 844 of file z3++.h.
◆ is_fpa()
Return true if this is a FloatingPoint expression. .
Definition at line 811 of file z3++.h.
Referenced by z3::fma(), expr::fpa_rounding_mode(), z3::max(), z3::min(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::rem(), and z3::sqrt().
◆ is_implies()
bool is_implies |
( |
| ) |
const |
|
inline |
◆ is_int()
Return true if this is an integer expression.
Definition at line 765 of file z3++.h.
Referenced by z3::abs().
◆ is_ite()
◆ is_lambda()
Return true if this expression is a lambda expression.
Definition at line 852 of file z3++.h.
◆ is_not()
◆ is_numeral() [1/4]
bool is_numeral |
( |
| ) |
const |
|
inline |
◆ is_numeral() [2/4]
bool is_numeral |
( |
double & |
d | ) |
const |
|
inline |
◆ is_numeral() [3/4]
bool is_numeral |
( |
std::string & |
s | ) |
const |
|
inline |
◆ is_numeral() [4/4]
bool is_numeral |
( |
std::string & |
s, |
|
|
unsigned |
precision |
|
) |
| const |
|
inline |
◆ is_numeral_i()
bool is_numeral_i |
( |
int & |
i | ) |
const |
|
inline |
◆ is_numeral_i64()
bool is_numeral_i64 |
( |
int64_t & |
i | ) |
const |
|
inline |
◆ is_numeral_u()
bool is_numeral_u |
( |
unsigned & |
i | ) |
const |
|
inline |
◆ is_numeral_u64()
bool is_numeral_u64 |
( |
uint64_t & |
i | ) |
const |
|
inline |
◆ is_or()
◆ is_quantifier()
bool is_quantifier |
( |
| ) |
const |
|
inline |
Return true if this expression is a quantifier.
Definition at line 839 of file z3++.h.
Referenced by expr::body().
◆ is_re()
◆ is_real()
Return true if this is a real expression.
Definition at line 769 of file z3++.h.
Referenced by z3::abs().
◆ is_relation()
bool is_relation |
( |
| ) |
const |
|
inline |
Return true if this is a Relation expression.
Definition at line 789 of file z3++.h.
◆ is_seq()
◆ is_string_value()
bool is_string_value |
( |
| ) |
const |
|
inline |
◆ is_true()
◆ is_var()
Return true if this expression is a variable.
Definition at line 857 of file z3++.h.
◆ is_well_sorted()
bool is_well_sorted |
( |
| ) |
const |
|
inline |
Return true if this expression is well sorted (aka type correct).
Definition at line 866 of file z3++.h.
◆ is_xor()
◆ itos()
◆ length()
◆ lo()
◆ loop() [1/2]
create a looping regular expression.
Definition at line 1333 of file z3++.h.
◆ loop() [2/2]
expr loop |
( |
unsigned |
lo, |
|
|
unsigned |
hi |
|
) |
| |
|
inline |
◆ nth()
◆ num_args()
unsigned num_args |
( |
| ) |
const |
|
inline |
◆ numerator()
◆ operator Z3_app()
operator Z3_app |
( |
| ) |
const |
|
inline |
Definition at line 1041 of file z3++.h.
1041 { assert(
is_app());
return reinterpret_cast<Z3_app
>(
m_ast); }
◆ operator=()
◆ operator[]() [1/2]
expr operator[] |
( |
expr const & |
index | ) |
const |
|
inline |
index operator defined on arrays and sequences.
Definition at line 1347 of file z3++.h.
1350 return select(*
this, index);
◆ operator[]() [2/2]
◆ repeat()
expr repeat |
( |
unsigned |
i | ) |
|
|
inline |
◆ replace()
◆ rotate_left()
expr rotate_left |
( |
unsigned |
i | ) |
|
|
inline |
◆ rotate_right()
expr rotate_right |
( |
unsigned |
i | ) |
|
|
inline |
◆ simplify() [1/2]
Return a simplified version of this expression.
Definition at line 1362 of file z3++.h.
◆ simplify() [2/2]
Return a simplified version of this expression. The parameter p
is a set of parameters for the Z3 simplifier.
Definition at line 1366 of file z3++.h.
◆ stoi()
◆ substitute() [1/2]
Apply substitution. Replace bound variables by expressions.
Definition at line 3588 of file z3++.h.
3589 array<Z3_ast> _dst(dst.size());
3590 for (
unsigned i = 0; i < dst.size(); ++i) {
◆ substitute() [2/2]
Apply substitution. Replace src expressions by dst.
Definition at line 3575 of file z3++.h.
3576 assert(src.size() == dst.size());
3577 array<Z3_ast> _src(src.size());
3578 array<Z3_ast> _dst(dst.size());
3579 for (
unsigned i = 0; i < src.size(); ++i) {
◆ unit()
◆ abs
Definition at line 1732 of file z3++.h.
1735 expr zero = a.ctx().int_val(0);
1738 else if (a.is_real()) {
1739 expr zero = a.ctx().real_val(0);
1746 return expr(a.ctx(), r);
◆ atleast
Definition at line 2097 of file z3++.h.
2098 assert(es.size() > 0);
2099 context&
ctx = es[0].ctx();
2100 array<Z3_ast> _es(es);
◆ atmost
Definition at line 2089 of file z3++.h.
2090 assert(es.size() > 0);
2091 context&
ctx = es[0].ctx();
2092 array<Z3_ast> _es(es);
◆ bv2int
expr bv2int |
( |
expr const & |
a, |
|
|
bool |
is_signed |
|
) |
| |
|
friend |
bit-vector and integer conversions.
Definition at line 1898 of file z3++.h.
1898 { Z3_ast r =
Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error();
return expr(a.ctx(), r); }
◆ bvadd_no_overflow
expr bvadd_no_overflow |
( |
expr const & |
a, |
|
|
expr const & |
b, |
|
|
bool |
is_signed |
|
) |
| |
|
friend |
bit-vector overflow/underflow checks
Definition at line 1904 of file z3++.h.
◆ bvadd_no_underflow
◆ bvmul_no_overflow
expr bvmul_no_overflow |
( |
expr const & |
a, |
|
|
expr const & |
b, |
|
|
bool |
is_signed |
|
) |
| |
|
friend |
◆ bvmul_no_underflow
◆ bvneg_no_overflow
expr bvneg_no_overflow |
( |
expr const & |
a | ) |
|
|
friend |
◆ bvsdiv_no_overflow
◆ bvsub_no_overflow
◆ bvsub_no_underflow
expr bvsub_no_underflow |
( |
expr const & |
a, |
|
|
expr const & |
b, |
|
|
bool |
is_signed |
|
) |
| |
|
friend |
◆ concat [1/2]
Definition at line 2123 of file z3++.h.
2127 Z3_ast _args[2] = { a, b };
2131 Z3_ast _args[2] = { a, b };
2137 a.ctx().check_error();
2138 return expr(a.ctx(), r);
◆ concat [2/2]
Definition at line 2141 of file z3++.h.
2143 assert(args.size() > 0);
2144 if (args.size() == 1) {
2147 context&
ctx = args[0].ctx();
2148 array<Z3_ast> _args(args);
2156 r = _args[args.size()-1];
2157 for (
unsigned i = args.size()-1; i > 0; ) {
◆ distinct
Definition at line 2114 of file z3++.h.
2115 assert(args.size() > 0);
2116 context&
ctx = args[0].ctx();
2117 array<Z3_ast> _args(args);
◆ fma
FloatingPoint fused multiply-add.
Definition at line 1757 of file z3++.h.
1759 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1762 return expr(a.ctx(), r);
◆ implies [1/3]
Definition at line 1392 of file z3++.h.
1392 {
return implies(b.ctx().bool_val(a), b); }
◆ implies [2/3]
Definition at line 1391 of file z3++.h.
1391 {
return implies(a, a.ctx().bool_val(b)); }
◆ implies [3/3]
Definition at line 1387 of file z3++.h.
1388 assert(a.is_bool() && b.is_bool());
◆ int2bv
expr int2bv |
( |
unsigned |
n, |
|
|
expr const & |
a |
|
) |
| |
|
friend |
Definition at line 1899 of file z3++.h.
1899 { Z3_ast r =
Z3_mk_int2bv(a.ctx(), n, a); a.check_error();
return expr(a.ctx(), r); }
◆ is_int
◆ ite
Create the if-then-else expression ite(c, t, e)
- Precondition
- c.is_bool()
Definition at line 1771 of file z3++.h.
1773 assert(c.is_bool());
1776 return expr(c.ctx(), r);
◆ max
Definition at line 1717 of file z3++.h.
1723 else if (a.is_bv()) {
1730 return expr(a.ctx(), r);
◆ min
Definition at line 1702 of file z3++.h.
1708 else if (a.is_bv()) {
1715 return expr(a.ctx(), r);
◆ mk_and
Definition at line 2173 of file z3++.h.
2174 array<Z3_ast> _args(args);
2175 Z3_ast r =
Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2177 return expr(args.ctx(), r);
◆ mk_or
Definition at line 2167 of file z3++.h.
2168 array<Z3_ast> _args(args);
2169 Z3_ast r =
Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2171 return expr(args.ctx(), r);
◆ mod [1/3]
◆ mod [2/3]
Definition at line 1407 of file z3++.h.
1407 {
return mod(a, a.ctx().num_val(b, a.get_sort())); }
◆ mod [3/3]
Definition at line 1408 of file z3++.h.
1408 {
return mod(b.ctx().num_val(a, b.get_sort()), b); }
◆ nand
◆ nor
◆ operator!
Return an expression representing not(a)
.
- Precondition
- a.is_bool()
Definition at line 1433 of file z3++.h.
◆ operator!= [1/3]
Definition at line 1473 of file z3++.h.
1475 Z3_ast args[2] = { a, b };
1478 return expr(a.ctx(), r);
◆ operator!= [2/3]
Definition at line 1480 of file z3++.h.
1480 { assert(a.is_arith() || a.is_bv() || a.is_fpa());
return a != a.ctx().num_val(b, a.get_sort()); }
◆ operator!= [3/3]
Definition at line 1481 of file z3++.h.
1481 { assert(b.is_arith() || b.is_bv() || b.is_fpa());
return b.ctx().num_val(a, b.get_sort()) != b; }
◆ operator& [1/3]
◆ operator& [2/3]
expr operator& |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1688 of file z3++.h.
1688 {
return a & a.ctx().num_val(b, a.get_sort()); }
◆ operator& [3/3]
expr operator& |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1689 of file z3++.h.
1689 {
return b.ctx().num_val(a, b.get_sort()) & b; }
◆ operator&& [1/3]
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 1449 of file z3++.h.
1449 {
return b.ctx().bool_val(a) && b; }
◆ operator&& [2/3]
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 1448 of file z3++.h.
1448 {
return a && a.ctx().bool_val(b); }
◆ operator&& [3/3]
Return an expression representing a and b
.
- Precondition
- a.is_bool()
-
b.is_bool()
Definition at line 1439 of file z3++.h.
1441 assert(a.is_bool() && b.is_bool());
1442 Z3_ast args[2] = { a, b };
1445 return expr(a.ctx(), r);
◆ operator* [1/3]
Definition at line 1513 of file z3++.h.
1516 if (a.is_arith() && b.is_arith()) {
1517 Z3_ast args[2] = { a, b };
1520 else if (a.is_bv() && b.is_bv()) {
1523 else if (a.is_fpa() && b.is_fpa()) {
1524 r =
Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1531 return expr(a.ctx(), r);
◆ operator* [2/3]
expr operator* |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1533 of file z3++.h.
1533 {
return a * a.ctx().num_val(b, a.get_sort()); }
◆ operator* [3/3]
expr operator* |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1534 of file z3++.h.
1534 {
return b.ctx().num_val(a, b.get_sort()) * b; }
◆ operator+ [1/3]
Definition at line 1483 of file z3++.h.
1486 if (a.is_arith() && b.is_arith()) {
1487 Z3_ast args[2] = { a, b };
1490 else if (a.is_bv() && b.is_bv()) {
1493 else if (a.is_seq() && b.is_seq()) {
1496 else if (a.is_re() && b.is_re()) {
1497 Z3_ast _args[2] = { a, b };
1500 else if (a.is_fpa() && b.is_fpa()) {
1501 r =
Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1508 return expr(a.ctx(), r);
◆ operator+ [2/3]
expr operator+ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1510 of file z3++.h.
1510 {
return a + a.ctx().num_val(b, a.get_sort()); }
◆ operator+ [3/3]
expr operator+ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1511 of file z3++.h.
1511 {
return b.ctx().num_val(a, b.get_sort()) + b; }
◆ operator- [1/4]
Definition at line 1576 of file z3++.h.
1581 else if (a.is_bv()) {
1584 else if (a.is_fpa()) {
1592 return expr(a.ctx(), r);
◆ operator- [2/4]
Definition at line 1595 of file z3++.h.
1598 if (a.is_arith() && b.is_arith()) {
1599 Z3_ast args[2] = { a, b };
1602 else if (a.is_bv() && b.is_bv()) {
1605 else if (a.is_fpa() && b.is_fpa()) {
1606 r =
Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1613 return expr(a.ctx(), r);
◆ operator- [3/4]
expr operator- |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1615 of file z3++.h.
1615 {
return a - a.ctx().num_val(b, a.get_sort()); }
◆ operator- [4/4]
expr operator- |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1616 of file z3++.h.
1616 {
return b.ctx().num_val(a, b.get_sort()) - b; }
◆ operator/ [1/3]
Definition at line 1554 of file z3++.h.
1557 if (a.is_arith() && b.is_arith()) {
1560 else if (a.is_bv() && b.is_bv()) {
1563 else if (a.is_fpa() && b.is_fpa()) {
1564 r =
Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1571 return expr(a.ctx(), r);
◆ operator/ [2/3]
expr operator/ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1573 of file z3++.h.
1573 {
return a / a.ctx().num_val(b, a.get_sort()); }
◆ operator/ [3/3]
expr operator/ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1574 of file z3++.h.
1574 {
return b.ctx().num_val(a, b.get_sort()) / b; }
◆ operator< [1/3]
Definition at line 1643 of file z3++.h.
1646 if (a.is_arith() && b.is_arith()) {
1649 else if (a.is_bv() && b.is_bv()) {
1652 else if (a.is_fpa() && b.is_fpa()) {
1660 return expr(a.ctx(), r);
◆ operator< [2/3]
expr operator< |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1662 of file z3++.h.
1662 {
return a < a.ctx().num_val(b, a.get_sort()); }
◆ operator< [3/3]
expr operator< |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1663 of file z3++.h.
1663 {
return b.ctx().num_val(a, b.get_sort()) < b; }
◆ operator<= [1/3]
Definition at line 1618 of file z3++.h.
1621 if (a.is_arith() && b.is_arith()) {
1624 else if (a.is_bv() && b.is_bv()) {
1627 else if (a.is_fpa() && b.is_fpa()) {
1635 return expr(a.ctx(), r);
◆ operator<= [2/3]
expr operator<= |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1637 of file z3++.h.
1637 {
return a <= a.ctx().num_val(b, a.get_sort()); }
◆ operator<= [3/3]
expr operator<= |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1638 of file z3++.h.
1638 {
return b.ctx().num_val(a, b.get_sort()) <= b; }
◆ operator== [1/3]
Definition at line 1464 of file z3++.h.
1466 Z3_ast r =
Z3_mk_eq(a.ctx(), a, b);
1468 return expr(a.ctx(), r);
◆ operator== [2/3]
expr operator== |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1470 of file z3++.h.
1470 { assert(a.is_arith() || a.is_bv() || a.is_fpa());
return a == a.ctx().num_val(b, a.get_sort()); }
◆ operator== [3/3]
expr operator== |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1471 of file z3++.h.
1471 { assert(b.is_arith() || b.is_bv() || b.is_fpa());
return b.ctx().num_val(a, b.get_sort()) == b; }
◆ operator> [1/3]
Definition at line 1665 of file z3++.h.
1668 if (a.is_arith() && b.is_arith()) {
1671 else if (a.is_bv() && b.is_bv()) {
1674 else if (a.is_fpa() && b.is_fpa()) {
1682 return expr(a.ctx(), r);
◆ operator> [2/3]
expr operator> |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1684 of file z3++.h.
1684 {
return a > a.ctx().num_val(b, a.get_sort()); }
◆ operator> [3/3]
expr operator> |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1685 of file z3++.h.
1685 {
return b.ctx().num_val(a, b.get_sort()) > b; }
◆ operator>= [1/3]
Definition at line 1537 of file z3++.h.
1540 if (a.is_arith() && b.is_arith()) {
1543 else if (a.is_bv() && b.is_bv()) {
1551 return expr(a.ctx(), r);
◆ operator>= [2/3]
expr operator>= |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1640 of file z3++.h.
1640 {
return a >= a.ctx().num_val(b, a.get_sort()); }
◆ operator>= [3/3]
expr operator>= |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1641 of file z3++.h.
1641 {
return b.ctx().num_val(a, b.get_sort()) >= b; }
◆ operator^ [1/3]
◆ operator^ [2/3]
expr operator^ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1692 of file z3++.h.
1692 {
return a ^ a.ctx().num_val(b, a.get_sort()); }
◆ operator^ [3/3]
expr operator^ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1693 of file z3++.h.
1693 {
return b.ctx().num_val(a, b.get_sort()) ^ b; }
◆ operator| [1/3]
◆ operator| [2/3]
expr operator| |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1696 of file z3++.h.
1696 {
return a | a.ctx().num_val(b, a.get_sort()); }
◆ operator| [3/3]
expr operator| |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1697 of file z3++.h.
1697 {
return b.ctx().num_val(a, b.get_sort()) | b; }
◆ operator|| [1/3]
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 1462 of file z3++.h.
1462 {
return b.ctx().bool_val(a) || b; }
◆ operator|| [2/3]
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 1460 of file z3++.h.
1460 {
return a || a.ctx().bool_val(b); }
◆ operator|| [3/3]
Return an expression representing a or b
.
- Precondition
- a.is_bool()
-
b.is_bool()
Definition at line 1451 of file z3++.h.
1453 assert(a.is_bool() && b.is_bool());
1454 Z3_ast args[2] = { a, b };
1455 Z3_ast r =
Z3_mk_or(a.ctx(), 2, args);
1457 return expr(a.ctx(), r);
◆ operator~
◆ pbeq
Definition at line 2081 of file z3++.h.
2082 assert(es.size() > 0);
2083 context&
ctx = es[0].ctx();
2084 array<Z3_ast> _es(es);
2085 Z3_ast r =
Z3_mk_pbeq(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pbge
Definition at line 2073 of file z3++.h.
2074 assert(es.size() > 0);
2075 context&
ctx = es[0].ctx();
2076 array<Z3_ast> _es(es);
2077 Z3_ast r =
Z3_mk_pbge(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pble
Definition at line 2065 of file z3++.h.
2066 assert(es.size() > 0);
2067 context&
ctx = es[0].ctx();
2068 array<Z3_ast> _es(es);
2069 Z3_ast r =
Z3_mk_pble(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pw [1/3]
◆ pw [2/3]
Definition at line 1396 of file z3++.h.
1396 {
return pw(a, a.ctx().num_val(b, a.get_sort())); }
◆ pw [3/3]
Definition at line 1397 of file z3++.h.
1397 {
return pw(b.ctx().num_val(a, b.get_sort()), b); }
◆ range
◆ rem [1/3]
Definition at line 1415 of file z3++.h.
1416 if (a.is_fpa() && b.is_fpa()) {
◆ rem [2/3]
Definition at line 1422 of file z3++.h.
1422 {
return rem(a, a.ctx().num_val(b, a.get_sort())); }
◆ rem [3/3]
Definition at line 1423 of file z3++.h.
1423 {
return rem(b.ctx().num_val(a, b.get_sort()), b); }
◆ sqrt
◆ sum
Definition at line 2105 of file z3++.h.
2106 assert(args.size() > 0);
2107 context&
ctx = args[0].ctx();
2108 array<Z3_ast> _args(args);
◆ xnor
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
bool is_fpa() const
Return true if this sort is a Floating point sort.
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
bool is_relation() const
Return true if this sort is a Relation sort.
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
#define _Z3_MK_BIN_(a, b, binop)
bool is_numeral_i(int &i) const
bool is_re() const
Return true if this sort is a regular expression sort.
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Floating-point fused multiply-add.
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the unescaped string constant stored in s.
Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a)
Return numeral value, as a binary string of a numeric constant term.
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.
bool is_numeral_u(unsigned &i) const
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
expr select(expr const &a, expr const &i)
forward declarations
friend expr rem(expr const &a, expr const &b)
bool is_array() const
Return true if this sort is a Array sort.
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a decimal string of a numeric constant term.
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
ast & operator=(ast const &s)
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
#define _Z3_MK_UN_(a, mkun)
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
bool is_quantifier() const
Return true if this expression is a quantifier.
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
bool is_seq() const
Return true if this is a sequence expression.
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s.
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
Z3_decl_kind decl_kind() const
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
bool is_datatype() const
Return true if this sort is a Datatype sort.
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality....
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n,...
friend expr implies(expr const &a, expr const &b)
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int....
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int....
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.
friend expr pw(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
bool is_algebraic() const
Return true if expression is an algebraic number.
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int....
bool is_int() const
Return true if this sort is the Integer sort.
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
ast_vector_tpl< expr > expr_vector
bool is_seq() const
Return true if this sort is a Sequence sort.
friend expr concat(expr const &a, expr const &b)
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places.
bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int....
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
friend void check_context(object const &a, object const &b)
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
friend expr mod(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
sort fpa_rounding_mode()
Return a RoundingMode sort.
bool is_array() const
Return true if this is a Array expression.
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a)
Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
bool is_real() const
Return true if this sort is the Real sort.
Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision)
Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...
expr nth(expr const &index) const
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
bool is_bool() const
Return true if this sort is the Boolean sort.
Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the right i times.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs,...
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
bool is_numeral_i64(int64_t &i) const
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index. The sequence is empty if the index is...
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_error_code check_error() const
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the element positioned at position index. The function is under-specified if the inde...
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.
bool is_app() const
Return true if this expression is an application.
bool is_string_value() const
Return true if this expression is a string literal. The string can be accessed using get_string() and...
bool is_numeral_u64(uint64_t &i) const
sort get_sort() const
Return the sort of this expression.
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.