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::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=()
Definition at line 751 of file z3++.h.
751 {
return static_cast<expr&>(ast::operator=(n)); }
◆ 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 3585 of file z3++.h.
3586 array<Z3_ast> _dst(dst.size());
3587 for (
unsigned i = 0; i < dst.size(); ++i) {
◆ substitute() [2/2]
Apply substitution. Replace src expressions by dst.
Definition at line 3572 of file z3++.h.
3573 assert(src.size() == dst.size());
3574 array<Z3_ast> _src(src.size());
3575 array<Z3_ast> _dst(dst.size());
3576 for (
unsigned i = 0; i < src.size(); ++i) {
◆ unit()
◆ abs
Definition at line 1739 of file z3++.h.
1742 expr zero = a.ctx().int_val(0);
1745 else if (a.is_real()) {
1746 expr zero = a.ctx().real_val(0);
1753 return expr(a.ctx(), r);
◆ atleast
Definition at line 2104 of file z3++.h.
2105 assert(es.size() > 0);
2106 context&
ctx = es[0].ctx();
2107 array<Z3_ast> _es(es);
◆ atmost
Definition at line 2096 of file z3++.h.
2097 assert(es.size() > 0);
2098 context&
ctx = es[0].ctx();
2099 array<Z3_ast> _es(es);
◆ bv2int
expr bv2int |
( |
expr const & |
a, |
|
|
bool |
is_signed |
|
) |
| |
|
friend |
bit-vector and integer conversions.
Definition at line 1905 of file z3++.h.
1905 { 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 1911 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 2130 of file z3++.h.
2134 Z3_ast _args[2] = { a, b };
2138 Z3_ast _args[2] = { a, b };
2144 a.ctx().check_error();
2145 return expr(a.ctx(), r);
◆ concat [2/2]
Definition at line 2148 of file z3++.h.
2150 assert(args.size() > 0);
2151 if (args.size() == 1) {
2154 context&
ctx = args[0].ctx();
2155 array<Z3_ast> _args(args);
2163 r = _args[args.size()-1];
2164 for (
unsigned i = args.size()-1; i > 0; ) {
◆ distinct
Definition at line 2121 of file z3++.h.
2122 assert(args.size() > 0);
2123 context&
ctx = args[0].ctx();
2124 array<Z3_ast> _args(args);
◆ fma
FloatingPoint fused multiply-add.
Definition at line 1764 of file z3++.h.
1766 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1769 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 1906 of file z3++.h.
1906 { 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 1778 of file z3++.h.
1780 assert(c.is_bool());
1783 return expr(c.ctx(), r);
◆ max
Definition at line 1724 of file z3++.h.
1730 else if (a.is_bv()) {
1737 return expr(a.ctx(), r);
◆ min
Definition at line 1709 of file z3++.h.
1715 else if (a.is_bv()) {
1722 return expr(a.ctx(), r);
◆ mk_and
Definition at line 2180 of file z3++.h.
2181 array<Z3_ast> _args(args);
2182 Z3_ast r =
Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2184 return expr(args.ctx(), r);
◆ mk_or
Definition at line 2174 of file z3++.h.
2175 array<Z3_ast> _args(args);
2176 Z3_ast r =
Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2178 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 1475 of file z3++.h.
1477 Z3_ast args[2] = { a, b };
1480 return expr(a.ctx(), r);
◆ operator!= [2/3]
Definition at line 1482 of file z3++.h.
1482 { 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 1483 of file z3++.h.
1483 { 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 1695 of file z3++.h.
1695 {
return a & a.ctx().num_val(b, a.get_sort()); }
◆ operator& [3/3]
expr operator& |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1696 of file z3++.h.
1696 {
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 1517 of file z3++.h.
1520 if (a.is_arith() && b.is_arith()) {
1521 Z3_ast args[2] = { a, b };
1524 else if (a.is_bv() && b.is_bv()) {
1527 else if (a.is_fpa() && b.is_fpa()) {
1528 r =
Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1535 return expr(a.ctx(), r);
◆ operator* [2/3]
expr operator* |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1537 of file z3++.h.
1537 {
return a * a.ctx().num_val(b, a.get_sort()); }
◆ operator* [3/3]
expr operator* |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1538 of file z3++.h.
1538 {
return b.ctx().num_val(a, b.get_sort()) * b; }
◆ operator+ [1/3]
Definition at line 1487 of file z3++.h.
1490 if (a.is_arith() && b.is_arith()) {
1491 Z3_ast args[2] = { a, b };
1494 else if (a.is_bv() && b.is_bv()) {
1497 else if (a.is_seq() && b.is_seq()) {
1500 else if (a.is_re() && b.is_re()) {
1501 Z3_ast _args[2] = { a, b };
1504 else if (a.is_fpa() && b.is_fpa()) {
1505 r =
Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1512 return expr(a.ctx(), r);
◆ operator+ [2/3]
expr operator+ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1514 of file z3++.h.
1514 {
return a + a.ctx().num_val(b, a.get_sort()); }
◆ operator+ [3/3]
expr operator+ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1515 of file z3++.h.
1515 {
return b.ctx().num_val(a, b.get_sort()) + b; }
◆ operator- [1/4]
Definition at line 1583 of file z3++.h.
1588 else if (a.is_bv()) {
1591 else if (a.is_fpa()) {
1599 return expr(a.ctx(), r);
◆ operator- [2/4]
Definition at line 1602 of file z3++.h.
1605 if (a.is_arith() && b.is_arith()) {
1606 Z3_ast args[2] = { a, b };
1609 else if (a.is_bv() && b.is_bv()) {
1612 else if (a.is_fpa() && b.is_fpa()) {
1613 r =
Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1620 return expr(a.ctx(), r);
◆ operator- [3/4]
expr operator- |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1622 of file z3++.h.
1622 {
return a - a.ctx().num_val(b, a.get_sort()); }
◆ operator- [4/4]
expr operator- |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1623 of file z3++.h.
1623 {
return b.ctx().num_val(a, b.get_sort()) - b; }
◆ operator/ [1/3]
Definition at line 1561 of file z3++.h.
1564 if (a.is_arith() && b.is_arith()) {
1567 else if (a.is_bv() && b.is_bv()) {
1570 else if (a.is_fpa() && b.is_fpa()) {
1571 r =
Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1578 return expr(a.ctx(), r);
◆ operator/ [2/3]
expr operator/ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1580 of file z3++.h.
1580 {
return a / a.ctx().num_val(b, a.get_sort()); }
◆ operator/ [3/3]
expr operator/ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1581 of file z3++.h.
1581 {
return b.ctx().num_val(a, b.get_sort()) / b; }
◆ operator< [1/3]
Definition at line 1650 of file z3++.h.
1653 if (a.is_arith() && b.is_arith()) {
1656 else if (a.is_bv() && b.is_bv()) {
1659 else if (a.is_fpa() && b.is_fpa()) {
1667 return expr(a.ctx(), r);
◆ operator< [2/3]
expr operator< |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1669 of file z3++.h.
1669 {
return a < a.ctx().num_val(b, a.get_sort()); }
◆ operator< [3/3]
expr operator< |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1670 of file z3++.h.
1670 {
return b.ctx().num_val(a, b.get_sort()) < b; }
◆ operator<= [1/3]
Definition at line 1625 of file z3++.h.
1628 if (a.is_arith() && b.is_arith()) {
1631 else if (a.is_bv() && b.is_bv()) {
1634 else if (a.is_fpa() && b.is_fpa()) {
1642 return expr(a.ctx(), r);
◆ operator<= [2/3]
expr operator<= |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1644 of file z3++.h.
1644 {
return a <= a.ctx().num_val(b, a.get_sort()); }
◆ operator<= [3/3]
expr operator<= |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1645 of file z3++.h.
1645 {
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 1672 of file z3++.h.
1675 if (a.is_arith() && b.is_arith()) {
1678 else if (a.is_bv() && b.is_bv()) {
1681 else if (a.is_fpa() && b.is_fpa()) {
1689 return expr(a.ctx(), r);
◆ operator> [2/3]
expr operator> |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1691 of file z3++.h.
1691 {
return a > a.ctx().num_val(b, a.get_sort()); }
◆ operator> [3/3]
expr operator> |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1692 of file z3++.h.
1692 {
return b.ctx().num_val(a, b.get_sort()) > b; }
◆ operator>= [1/3]
Definition at line 1541 of file z3++.h.
1544 if (a.is_arith() && b.is_arith()) {
1547 else if (a.is_bv() && b.is_bv()) {
1550 else if (a.is_fpa() && b.is_fpa()) {
1558 return expr(a.ctx(), r);
◆ operator>= [2/3]
expr operator>= |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1647 of file z3++.h.
1647 {
return a >= a.ctx().num_val(b, a.get_sort()); }
◆ operator>= [3/3]
expr operator>= |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1648 of file z3++.h.
1648 {
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 1699 of file z3++.h.
1699 {
return a ^ a.ctx().num_val(b, a.get_sort()); }
◆ operator^ [3/3]
expr operator^ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1700 of file z3++.h.
1700 {
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 1703 of file z3++.h.
1703 {
return a | a.ctx().num_val(b, a.get_sort()); }
◆ operator| [3/3]
expr operator| |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1704 of file z3++.h.
1704 {
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 2088 of file z3++.h.
2089 assert(es.size() > 0);
2090 context&
ctx = es[0].ctx();
2091 array<Z3_ast> _es(es);
2092 Z3_ast r =
Z3_mk_pbeq(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pbge
Definition at line 2080 of file z3++.h.
2081 assert(es.size() > 0);
2082 context&
ctx = es[0].ctx();
2083 array<Z3_ast> _es(es);
2084 Z3_ast r =
Z3_mk_pbge(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pble
Definition at line 2072 of file z3++.h.
2073 assert(es.size() > 0);
2074 context&
ctx = es[0].ctx();
2075 array<Z3_ast> _es(es);
2076 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 2112 of file z3++.h.
2113 assert(args.size() > 0);
2114 context&
ctx = args[0].ctx();
2115 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.
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_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.
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.