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 | 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 737 of file z3++.h.
◆ expr() [1/3]
Definition at line 739 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 740 of file z3++.h.
740 :
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 899 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 872 of file z3++.h.
◆ algebraic_poly()
Return coefficients for p of an algebraic number (root-obj p i)
Definition at line 889 of file z3++.h.
◆ algebraic_upper()
expr algebraic_upper |
( |
unsigned |
precision | ) |
const |
|
inline |
◆ arg()
expr arg |
( |
unsigned |
i | ) |
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 1050 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 1270 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 1036 of file z3++.h.
1040 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 864 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 1016 of file z3++.h.
1020 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 921 of file z3++.h.
924 assert(
ctx().enable_exceptions());
925 if (!
ctx().enable_exceptions())
return 0;
926 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 957 of file z3++.h.
961 assert(
ctx().enable_exceptions());
962 if (!
ctx().enable_exceptions())
return 0;
963 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 940 of file z3++.h.
944 assert(
ctx().enable_exceptions());
945 if (!
ctx().enable_exceptions())
return 0;
946 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 974 of file z3++.h.
978 assert(
ctx().enable_exceptions());
979 if (!
ctx().enable_exceptions())
return 0;
980 Z3_THROW(exception(
"numeral does not fit in machine uint64_t"));
◆ get_sort()
Return the sort of this expression.
Definition at line 747 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 1023 of file z3++.h.
1028 return std::string(s, n);
◆ hi()
◆ id()
retrieve unique identifier for expression.
Definition at line 909 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 821 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 764 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()
◆ is_bv()
Return true if this is a Bit-vector expression.
Definition at line 768 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 825 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 776 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 838 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 798 of file z3++.h.
◆ is_forall()
Return true if this expression is a universal quantifier.
Definition at line 834 of file z3++.h.
◆ is_fpa()
Return true if this is a FloatingPoint expression. .
Definition at line 802 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 756 of file z3++.h.
Referenced by z3::abs().
◆ is_ite()
◆ is_lambda()
Return true if this expression is a lambda expression.
Definition at line 842 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 829 of file z3++.h.
Referenced by expr::body().
◆ is_re()
◆ is_real()
Return true if this is a real expression.
Definition at line 760 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 780 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 847 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 856 of file z3++.h.
◆ is_xor()
◆ itos()
◆ length()
◆ lo()
◆ loop() [1/2]
create a looping regular expression.
Definition at line 1323 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 1031 of file z3++.h.
1031 { 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 1337 of file z3++.h.
1340 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 1352 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 1356 of file z3++.h.
◆ stoi()
◆ substitute() [1/2]
Apply substitution. Replace bound variables by expressions.
Definition at line 3558 of file z3++.h.
3559 array<Z3_ast> _dst(dst.size());
3560 for (
unsigned i = 0; i < dst.size(); ++i) {
◆ substitute() [2/2]
Apply substitution. Replace src expressions by dst.
Definition at line 3545 of file z3++.h.
3546 assert(src.size() == dst.size());
3547 array<Z3_ast> _src(src.size());
3548 array<Z3_ast> _dst(dst.size());
3549 for (
unsigned i = 0; i < src.size(); ++i) {
◆ unit()
◆ abs
Definition at line 1722 of file z3++.h.
1725 expr zero = a.ctx().int_val(0);
1728 else if (a.is_real()) {
1729 expr zero = a.ctx().real_val(0);
1736 return expr(a.ctx(), r);
◆ atleast
Definition at line 2087 of file z3++.h.
2088 assert(es.size() > 0);
2089 context&
ctx = es[0].ctx();
2090 array<Z3_ast> _es(es);
◆ atmost
Definition at line 2079 of file z3++.h.
2080 assert(es.size() > 0);
2081 context&
ctx = es[0].ctx();
2082 array<Z3_ast> _es(es);
◆ bv2int
expr bv2int |
( |
expr const & |
a, |
|
|
bool |
is_signed |
|
) |
| |
|
friend |
bit-vector and integer conversions.
Definition at line 1888 of file z3++.h.
1888 { 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 1894 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 2113 of file z3++.h.
2117 Z3_ast _args[2] = { a, b };
2121 Z3_ast _args[2] = { a, b };
2127 a.ctx().check_error();
2128 return expr(a.ctx(), r);
◆ concat [2/2]
Definition at line 2131 of file z3++.h.
2133 assert(args.size() > 0);
2134 if (args.size() == 1) {
2137 context&
ctx = args[0].ctx();
2138 array<Z3_ast> _args(args);
2146 r = _args[args.size()-1];
2147 for (
unsigned i = args.size()-1; i > 0; ) {
◆ distinct
Definition at line 2104 of file z3++.h.
2105 assert(args.size() > 0);
2106 context&
ctx = args[0].ctx();
2107 array<Z3_ast> _args(args);
◆ fma
FloatingPoint fused multiply-add.
Definition at line 1747 of file z3++.h.
1749 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1752 return expr(a.ctx(), r);
◆ implies [1/3]
Definition at line 1382 of file z3++.h.
1382 {
return implies(b.ctx().bool_val(a), b); }
◆ implies [2/3]
Definition at line 1381 of file z3++.h.
1381 {
return implies(a, a.ctx().bool_val(b)); }
◆ implies [3/3]
Definition at line 1377 of file z3++.h.
1378 assert(a.is_bool() && b.is_bool());
◆ int2bv
expr int2bv |
( |
unsigned |
n, |
|
|
expr const & |
a |
|
) |
| |
|
friend |
Definition at line 1889 of file z3++.h.
1889 { 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 1761 of file z3++.h.
1763 assert(c.is_bool());
1766 return expr(c.ctx(), r);
◆ max
Definition at line 1707 of file z3++.h.
1713 else if (a.is_bv()) {
1720 return expr(a.ctx(), r);
◆ min
Definition at line 1692 of file z3++.h.
1698 else if (a.is_bv()) {
1705 return expr(a.ctx(), r);
◆ mk_and
Definition at line 2163 of file z3++.h.
2164 array<Z3_ast> _args(args);
2165 Z3_ast r =
Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2167 return expr(args.ctx(), r);
◆ mk_or
Definition at line 2157 of file z3++.h.
2158 array<Z3_ast> _args(args);
2159 Z3_ast r =
Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2161 return expr(args.ctx(), r);
◆ mod [1/3]
◆ mod [2/3]
Definition at line 1397 of file z3++.h.
1397 {
return mod(a, a.ctx().num_val(b, a.get_sort())); }
◆ mod [3/3]
Definition at line 1398 of file z3++.h.
1398 {
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 1423 of file z3++.h.
◆ operator!= [1/3]
Definition at line 1463 of file z3++.h.
1465 Z3_ast args[2] = { a, b };
1468 return expr(a.ctx(), r);
◆ operator!= [2/3]
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]
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]
◆ operator& [2/3]
expr operator& |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1678 of file z3++.h.
1678 {
return a & a.ctx().num_val(b, a.get_sort()); }
◆ operator& [3/3]
expr operator& |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1679 of file z3++.h.
1679 {
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 1439 of file z3++.h.
1439 {
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 1438 of file z3++.h.
1438 {
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 1429 of file z3++.h.
1431 assert(a.is_bool() && b.is_bool());
1432 Z3_ast args[2] = { a, b };
1435 return expr(a.ctx(), r);
◆ operator* [1/3]
Definition at line 1503 of file z3++.h.
1506 if (a.is_arith() && b.is_arith()) {
1507 Z3_ast args[2] = { a, b };
1510 else if (a.is_bv() && b.is_bv()) {
1513 else if (a.is_fpa() && b.is_fpa()) {
1514 r =
Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1521 return expr(a.ctx(), r);
◆ operator* [2/3]
expr operator* |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1523 of file z3++.h.
1523 {
return a * a.ctx().num_val(b, a.get_sort()); }
◆ operator* [3/3]
expr operator* |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1524 of file z3++.h.
1524 {
return b.ctx().num_val(a, b.get_sort()) * b; }
◆ operator+ [1/3]
Definition at line 1473 of file z3++.h.
1476 if (a.is_arith() && b.is_arith()) {
1477 Z3_ast args[2] = { a, b };
1480 else if (a.is_bv() && b.is_bv()) {
1483 else if (a.is_seq() && b.is_seq()) {
1486 else if (a.is_re() && b.is_re()) {
1487 Z3_ast _args[2] = { a, b };
1490 else if (a.is_fpa() && b.is_fpa()) {
1491 r =
Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1498 return expr(a.ctx(), r);
◆ operator+ [2/3]
expr operator+ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1500 of file z3++.h.
1500 {
return a + a.ctx().num_val(b, a.get_sort()); }
◆ operator+ [3/3]
expr operator+ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1501 of file z3++.h.
1501 {
return b.ctx().num_val(a, b.get_sort()) + b; }
◆ operator- [1/4]
Definition at line 1566 of file z3++.h.
1571 else if (a.is_bv()) {
1574 else if (a.is_fpa()) {
1582 return expr(a.ctx(), r);
◆ operator- [2/4]
Definition at line 1585 of file z3++.h.
1588 if (a.is_arith() && b.is_arith()) {
1589 Z3_ast args[2] = { a, b };
1592 else if (a.is_bv() && b.is_bv()) {
1595 else if (a.is_fpa() && b.is_fpa()) {
1596 r =
Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1603 return expr(a.ctx(), r);
◆ operator- [3/4]
expr operator- |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1605 of file z3++.h.
1605 {
return a - a.ctx().num_val(b, a.get_sort()); }
◆ operator- [4/4]
expr operator- |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1606 of file z3++.h.
1606 {
return b.ctx().num_val(a, b.get_sort()) - b; }
◆ operator/ [1/3]
Definition at line 1544 of file z3++.h.
1547 if (a.is_arith() && b.is_arith()) {
1550 else if (a.is_bv() && b.is_bv()) {
1553 else if (a.is_fpa() && b.is_fpa()) {
1554 r =
Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1561 return expr(a.ctx(), r);
◆ operator/ [2/3]
expr operator/ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1563 of file z3++.h.
1563 {
return a / a.ctx().num_val(b, a.get_sort()); }
◆ operator/ [3/3]
expr operator/ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1564 of file z3++.h.
1564 {
return b.ctx().num_val(a, b.get_sort()) / b; }
◆ operator< [1/3]
Definition at line 1633 of file z3++.h.
1636 if (a.is_arith() && b.is_arith()) {
1639 else if (a.is_bv() && b.is_bv()) {
1642 else if (a.is_fpa() && b.is_fpa()) {
1650 return expr(a.ctx(), r);
◆ operator< [2/3]
expr operator< |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1652 of file z3++.h.
1652 {
return a < a.ctx().num_val(b, a.get_sort()); }
◆ operator< [3/3]
expr operator< |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1653 of file z3++.h.
1653 {
return b.ctx().num_val(a, b.get_sort()) < b; }
◆ operator<= [1/3]
Definition at line 1608 of file z3++.h.
1611 if (a.is_arith() && b.is_arith()) {
1614 else if (a.is_bv() && b.is_bv()) {
1617 else if (a.is_fpa() && b.is_fpa()) {
1625 return expr(a.ctx(), r);
◆ operator<= [2/3]
expr operator<= |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1627 of file z3++.h.
1627 {
return a <= a.ctx().num_val(b, a.get_sort()); }
◆ operator<= [3/3]
expr operator<= |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1628 of file z3++.h.
1628 {
return b.ctx().num_val(a, b.get_sort()) <= b; }
◆ operator== [1/3]
Definition at line 1454 of file z3++.h.
1456 Z3_ast r =
Z3_mk_eq(a.ctx(), a, b);
1458 return expr(a.ctx(), r);
◆ operator== [2/3]
expr operator== |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1460 of file z3++.h.
1460 { 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 1461 of file z3++.h.
1461 { 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 1655 of file z3++.h.
1658 if (a.is_arith() && b.is_arith()) {
1661 else if (a.is_bv() && b.is_bv()) {
1664 else if (a.is_fpa() && b.is_fpa()) {
1672 return expr(a.ctx(), r);
◆ operator> [2/3]
expr operator> |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1674 of file z3++.h.
1674 {
return a > a.ctx().num_val(b, a.get_sort()); }
◆ operator> [3/3]
expr operator> |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1675 of file z3++.h.
1675 {
return b.ctx().num_val(a, b.get_sort()) > b; }
◆ operator>= [1/3]
Definition at line 1527 of file z3++.h.
1530 if (a.is_arith() && b.is_arith()) {
1533 else if (a.is_bv() && b.is_bv()) {
1541 return expr(a.ctx(), r);
◆ operator>= [2/3]
expr operator>= |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1630 of file z3++.h.
1630 {
return a >= a.ctx().num_val(b, a.get_sort()); }
◆ operator>= [3/3]
expr operator>= |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1631 of file z3++.h.
1631 {
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 1682 of file z3++.h.
1682 {
return a ^ a.ctx().num_val(b, a.get_sort()); }
◆ operator^ [3/3]
expr operator^ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1683 of file z3++.h.
1683 {
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 1686 of file z3++.h.
1686 {
return a | a.ctx().num_val(b, a.get_sort()); }
◆ operator| [3/3]
expr operator| |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1687 of file z3++.h.
1687 {
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 1452 of file z3++.h.
1452 {
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 1450 of file z3++.h.
1450 {
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 1441 of file z3++.h.
1443 assert(a.is_bool() && b.is_bool());
1444 Z3_ast args[2] = { a, b };
1445 Z3_ast r =
Z3_mk_or(a.ctx(), 2, args);
1447 return expr(a.ctx(), r);
◆ operator~
◆ pbeq
Definition at line 2071 of file z3++.h.
2072 assert(es.size() > 0);
2073 context&
ctx = es[0].ctx();
2074 array<Z3_ast> _es(es);
2075 Z3_ast r =
Z3_mk_pbeq(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pbge
Definition at line 2063 of file z3++.h.
2064 assert(es.size() > 0);
2065 context&
ctx = es[0].ctx();
2066 array<Z3_ast> _es(es);
2067 Z3_ast r =
Z3_mk_pbge(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pble
Definition at line 2055 of file z3++.h.
2056 assert(es.size() > 0);
2057 context&
ctx = es[0].ctx();
2058 array<Z3_ast> _es(es);
2059 Z3_ast r =
Z3_mk_pble(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pw [1/3]
◆ pw [2/3]
Definition at line 1386 of file z3++.h.
1386 {
return pw(a, a.ctx().num_val(b, a.get_sort())); }
◆ pw [3/3]
Definition at line 1387 of file z3++.h.
1387 {
return pw(b.ctx().num_val(a, b.get_sort()), b); }
◆ range
◆ rem [1/3]
Definition at line 1405 of file z3++.h.
1406 if (a.is_fpa() && b.is_fpa()) {
◆ rem [2/3]
Definition at line 1412 of file z3++.h.
1412 {
return rem(a, a.ctx().num_val(b, a.get_sort())); }
◆ rem [3/3]
Definition at line 1413 of file z3++.h.
1413 {
return rem(b.ctx().num_val(a, b.get_sort()), b); }
◆ sqrt
◆ sum
Definition at line 2095 of file z3++.h.
2096 assert(args.size() > 0);
2097 context&
ctx = args[0].ctx();
2098 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_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_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 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.