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...
|
|
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 |
|
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) |
| 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 667 of file z3++.h.
◆ expr() [1/3]
Definition at line 669 of file z3++.h.
Referenced by 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 670 of file z3++.h.
670 :
ast(c,
reinterpret_cast<Z3_ast
>(n)) {}
◆ expr() [3/3]
◆ 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 934 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 1154 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 920 of file z3++.h.
924 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 793 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 902 of file z3++.h.
905 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 814 of file z3++.h.
817 assert(
ctx().enable_exceptions());
818 if (!
ctx().enable_exceptions())
return 0;
819 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 850 of file z3++.h.
854 assert(
ctx().enable_exceptions());
855 if (!
ctx().enable_exceptions())
return 0;
856 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 833 of file z3++.h.
837 assert(
ctx().enable_exceptions());
838 if (!
ctx().enable_exceptions())
return 0;
839 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 867 of file z3++.h.
871 assert(
ctx().enable_exceptions());
872 if (!
ctx().enable_exceptions())
return 0;
873 Z3_THROW(exception(
"numeral does not fit in machine uint64_t"));
◆ get_sort()
Return the sort of this expression.
Definition at line 677 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 908 of file z3++.h.
912 return std::string(s, n);
◆ hi()
◆ id()
retrieve unique identifier for expression.
Definition at line 802 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 750 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 694 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 698 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 754 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 706 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 767 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 728 of file z3++.h.
◆ is_forall()
Return true if this expression is a universal quantifier.
Definition at line 763 of file z3++.h.
◆ is_fpa()
Return true if this is a FloatingPoint expression. .
Definition at line 732 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 686 of file z3++.h.
Referenced by z3::abs().
◆ is_ite()
◆ is_lambda()
Return true if this expression is a lambda expression.
Definition at line 771 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 758 of file z3++.h.
Referenced by expr::body().
◆ is_re()
◆ is_real()
Return true if this is a real expression.
Definition at line 690 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 710 of file z3++.h.
◆ is_seq()
◆ is_true()
◆ is_var()
Return true if this expression is a variable.
Definition at line 776 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 785 of file z3++.h.
◆ is_xor()
◆ itos()
◆ length()
◆ lo()
◆ loop() [1/2]
create a looping regular expression.
Definition at line 1207 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 915 of file z3++.h.
915 { 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 1221 of file z3++.h.
1224 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 1236 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 1240 of file z3++.h.
◆ stoi()
◆ substitute() [1/2]
Apply substitution. Replace bound variables by expressions.
Definition at line 3501 of file z3++.h.
3502 array<Z3_ast> _dst(dst.size());
3503 for (
unsigned i = 0; i < dst.size(); ++i) {
◆ substitute() [2/2]
Apply substitution. Replace src expressions by dst.
Definition at line 3488 of file z3++.h.
3489 assert(src.size() == dst.size());
3490 array<Z3_ast> _src(src.size());
3491 array<Z3_ast> _dst(dst.size());
3492 for (
unsigned i = 0; i < src.size(); ++i) {
◆ unit()
◆ abs
Definition at line 1606 of file z3++.h.
1609 expr zero = a.ctx().int_val(0);
1612 else if (a.is_real()) {
1613 expr zero = a.ctx().real_val(0);
1620 return expr(a.ctx(), r);
◆ atleast
Definition at line 2040 of file z3++.h.
2041 assert(es.size() > 0);
2042 context&
ctx = es[0].ctx();
2043 array<Z3_ast> _es(es);
◆ atmost
Definition at line 2032 of file z3++.h.
2033 assert(es.size() > 0);
2034 context&
ctx = es[0].ctx();
2035 array<Z3_ast> _es(es);
◆ bv2int
expr bv2int |
( |
expr const & |
a, |
|
|
bool |
is_signed |
|
) |
| |
|
friend |
bit-vector and integer conversions.
Definition at line 1772 of file z3++.h.
1772 { 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 1778 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 2066 of file z3++.h.
2070 Z3_ast _args[2] = { a, b };
2074 Z3_ast _args[2] = { a, b };
2080 a.ctx().check_error();
2081 return expr(a.ctx(), r);
◆ concat [2/2]
Definition at line 2084 of file z3++.h.
2086 assert(args.size() > 0);
2087 if (args.size() == 1) {
2090 context&
ctx = args[0].ctx();
2091 array<Z3_ast> _args(args);
2099 r = _args[args.size()-1];
2100 for (
unsigned i = args.size()-1; i > 0; ) {
◆ distinct
Definition at line 2057 of file z3++.h.
2058 assert(args.size() > 0);
2059 context&
ctx = args[0].ctx();
2060 array<Z3_ast> _args(args);
◆ fma
FloatingPoint fused multiply-add.
◆ implies [1/3]
Definition at line 1266 of file z3++.h.
1266 {
return implies(b.ctx().bool_val(a), b); }
◆ implies [2/3]
Definition at line 1265 of file z3++.h.
1265 {
return implies(a, a.ctx().bool_val(b)); }
◆ implies [3/3]
Definition at line 1261 of file z3++.h.
1262 assert(a.is_bool() && b.is_bool());
◆ int2bv
expr int2bv |
( |
unsigned |
n, |
|
|
expr const & |
a |
|
) |
| |
|
friend |
Definition at line 1773 of file z3++.h.
1773 { 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 1645 of file z3++.h.
1647 assert(c.is_bool());
1650 return expr(c.ctx(), r);
◆ max
Definition at line 1591 of file z3++.h.
1597 else if (a.is_bv()) {
1604 return expr(a.ctx(), r);
◆ min
Definition at line 1576 of file z3++.h.
1582 else if (a.is_bv()) {
1589 return expr(a.ctx(), r);
◆ mk_and
Definition at line 2116 of file z3++.h.
2117 array<Z3_ast> _args(args);
2118 Z3_ast r =
Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2120 return expr(args.ctx(), r);
◆ mk_or
Definition at line 2110 of file z3++.h.
2111 array<Z3_ast> _args(args);
2112 Z3_ast r =
Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2114 return expr(args.ctx(), r);
◆ mod [1/3]
◆ mod [2/3]
Definition at line 1281 of file z3++.h.
1281 {
return mod(a, a.ctx().num_val(b, a.get_sort())); }
◆ mod [3/3]
Definition at line 1282 of file z3++.h.
1282 {
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 1307 of file z3++.h.
◆ operator!= [1/3]
Definition at line 1347 of file z3++.h.
1349 Z3_ast args[2] = { a, b };
1352 return expr(a.ctx(), r);
◆ operator!= [2/3]
Definition at line 1354 of file z3++.h.
1354 { 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 1355 of file z3++.h.
1355 { 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 1562 of file z3++.h.
1562 {
return a & a.ctx().num_val(b, a.get_sort()); }
◆ operator& [3/3]
expr operator& |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1563 of file z3++.h.
1563 {
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 1323 of file z3++.h.
1323 {
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 1322 of file z3++.h.
1322 {
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 1313 of file z3++.h.
1315 assert(a.is_bool() && b.is_bool());
1316 Z3_ast args[2] = { a, b };
1319 return expr(a.ctx(), r);
◆ operator* [1/3]
Definition at line 1387 of file z3++.h.
1390 if (a.is_arith() && b.is_arith()) {
1391 Z3_ast args[2] = { a, b };
1394 else if (a.is_bv() && b.is_bv()) {
1397 else if (a.is_fpa() && b.is_fpa()) {
1398 r =
Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1405 return expr(a.ctx(), r);
◆ operator* [2/3]
expr operator* |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1407 of file z3++.h.
1407 {
return a * a.ctx().num_val(b, a.get_sort()); }
◆ operator* [3/3]
expr operator* |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1408 of file z3++.h.
1408 {
return b.ctx().num_val(a, b.get_sort()) * b; }
◆ operator+ [1/3]
Definition at line 1357 of file z3++.h.
1360 if (a.is_arith() && b.is_arith()) {
1361 Z3_ast args[2] = { a, b };
1364 else if (a.is_bv() && b.is_bv()) {
1367 else if (a.is_seq() && b.is_seq()) {
1370 else if (a.is_re() && b.is_re()) {
1371 Z3_ast _args[2] = { a, b };
1374 else if (a.is_fpa() && b.is_fpa()) {
1375 r =
Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1382 return expr(a.ctx(), r);
◆ operator+ [2/3]
expr operator+ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1384 of file z3++.h.
1384 {
return a + a.ctx().num_val(b, a.get_sort()); }
◆ operator+ [3/3]
expr operator+ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1385 of file z3++.h.
1385 {
return b.ctx().num_val(a, b.get_sort()) + b; }
◆ operator- [1/4]
Definition at line 1450 of file z3++.h.
1455 else if (a.is_bv()) {
1458 else if (a.is_fpa()) {
1466 return expr(a.ctx(), r);
◆ operator- [2/4]
Definition at line 1469 of file z3++.h.
1472 if (a.is_arith() && b.is_arith()) {
1473 Z3_ast args[2] = { a, b };
1476 else if (a.is_bv() && b.is_bv()) {
1479 else if (a.is_fpa() && b.is_fpa()) {
1480 r =
Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1487 return expr(a.ctx(), r);
◆ operator- [3/4]
expr operator- |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1489 of file z3++.h.
1489 {
return a - a.ctx().num_val(b, a.get_sort()); }
◆ operator- [4/4]
expr operator- |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1490 of file z3++.h.
1490 {
return b.ctx().num_val(a, b.get_sort()) - b; }
◆ operator/ [1/3]
Definition at line 1428 of file z3++.h.
1431 if (a.is_arith() && b.is_arith()) {
1434 else if (a.is_bv() && b.is_bv()) {
1437 else if (a.is_fpa() && b.is_fpa()) {
1438 r =
Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1445 return expr(a.ctx(), r);
◆ operator/ [2/3]
expr operator/ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1447 of file z3++.h.
1447 {
return a / a.ctx().num_val(b, a.get_sort()); }
◆ operator/ [3/3]
expr operator/ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1448 of file z3++.h.
1448 {
return b.ctx().num_val(a, b.get_sort()) / b; }
◆ operator< [1/3]
Definition at line 1517 of file z3++.h.
1520 if (a.is_arith() && b.is_arith()) {
1523 else if (a.is_bv() && b.is_bv()) {
1526 else if (a.is_fpa() && b.is_fpa()) {
1534 return expr(a.ctx(), r);
◆ operator< [2/3]
expr operator< |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1536 of file z3++.h.
1536 {
return a < a.ctx().num_val(b, a.get_sort()); }
◆ operator< [3/3]
expr operator< |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1537 of file z3++.h.
1537 {
return b.ctx().num_val(a, b.get_sort()) < b; }
◆ operator<= [1/3]
Definition at line 1492 of file z3++.h.
1495 if (a.is_arith() && b.is_arith()) {
1498 else if (a.is_bv() && b.is_bv()) {
1501 else if (a.is_fpa() && b.is_fpa()) {
1509 return expr(a.ctx(), r);
◆ operator<= [2/3]
expr operator<= |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1511 of file z3++.h.
1511 {
return a <= a.ctx().num_val(b, a.get_sort()); }
◆ operator<= [3/3]
expr operator<= |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1512 of file z3++.h.
1512 {
return b.ctx().num_val(a, b.get_sort()) <= b; }
◆ operator== [1/3]
Definition at line 1338 of file z3++.h.
1340 Z3_ast r =
Z3_mk_eq(a.ctx(), a, b);
1342 return expr(a.ctx(), r);
◆ operator== [2/3]
expr operator== |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1344 of file z3++.h.
1344 { 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 1345 of file z3++.h.
1345 { 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 1539 of file z3++.h.
1542 if (a.is_arith() && b.is_arith()) {
1545 else if (a.is_bv() && b.is_bv()) {
1548 else if (a.is_fpa() && b.is_fpa()) {
1556 return expr(a.ctx(), r);
◆ operator> [2/3]
expr operator> |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1558 of file z3++.h.
1558 {
return a > a.ctx().num_val(b, a.get_sort()); }
◆ operator> [3/3]
expr operator> |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1559 of file z3++.h.
1559 {
return b.ctx().num_val(a, b.get_sort()) > b; }
◆ operator>= [1/3]
Definition at line 1411 of file z3++.h.
1414 if (a.is_arith() && b.is_arith()) {
1417 else if (a.is_bv() && b.is_bv()) {
1425 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/3]
◆ operator^ [2/3]
expr operator^ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1566 of file z3++.h.
1566 {
return a ^ a.ctx().num_val(b, a.get_sort()); }
◆ operator^ [3/3]
expr operator^ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1567 of file z3++.h.
1567 {
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 1570 of file z3++.h.
1570 {
return a | a.ctx().num_val(b, a.get_sort()); }
◆ operator| [3/3]
expr operator| |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1571 of file z3++.h.
1571 {
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 1336 of file z3++.h.
1336 {
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 1334 of file z3++.h.
1334 {
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 1325 of file z3++.h.
1327 assert(a.is_bool() && b.is_bool());
1328 Z3_ast args[2] = { a, b };
1329 Z3_ast r =
Z3_mk_or(a.ctx(), 2, args);
1331 return expr(a.ctx(), r);
◆ operator~
◆ pbeq
Definition at line 2024 of file z3++.h.
2025 assert(es.size() > 0);
2026 context&
ctx = es[0].ctx();
2027 array<Z3_ast> _es(es);
2028 Z3_ast r =
Z3_mk_pbeq(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pbge
Definition at line 2016 of file z3++.h.
2017 assert(es.size() > 0);
2018 context&
ctx = es[0].ctx();
2019 array<Z3_ast> _es(es);
2020 Z3_ast r =
Z3_mk_pbge(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pble
Definition at line 2008 of file z3++.h.
2009 assert(es.size() > 0);
2010 context&
ctx = es[0].ctx();
2011 array<Z3_ast> _es(es);
2012 Z3_ast r =
Z3_mk_pble(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pw [1/3]
◆ pw [2/3]
Definition at line 1270 of file z3++.h.
1270 {
return pw(a, a.ctx().num_val(b, a.get_sort())); }
◆ pw [3/3]
Definition at line 1271 of file z3++.h.
1271 {
return pw(b.ctx().num_val(a, b.get_sort()), b); }
◆ range
◆ rem [1/3]
Definition at line 1289 of file z3++.h.
1290 if (a.is_fpa() && b.is_fpa()) {
◆ rem [2/3]
Definition at line 1296 of file z3++.h.
1296 {
return rem(a, a.ctx().num_val(b, a.get_sort())); }
◆ rem [3/3]
Definition at line 1297 of file z3++.h.
1297 {
return rem(b.ctx().num_val(a, b.get_sort()), b); }
◆ sqrt
◆ sum
Definition at line 2048 of file z3++.h.
2049 assert(args.size() > 0);
2050 context&
ctx = args[0].ctx();
2051 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.
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_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].
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.
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 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.
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.
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_string 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_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_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.