RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/classz3_1_1expr.html below:

Z3: expr Class Reference

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) 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 double as_double () const uint64_t as_uint64 () const int64_t as_int64 () 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...
expr mk_is_inf () const Return Boolean expression to test for whether an FP expression is inf. More...
expr mk_is_nan () const Return Boolean expression to test for whether an FP expression is a NaN. More...
expr mk_is_normal () const Return Boolean expression to test for whether an FP expression is a normal. More...
expr mk_is_subnormal () const Return Boolean expression to test for whether an FP expression is a subnormal. More...
expr mk_is_zero () const Return Boolean expression to test for whether an FP expression is a zero. More...
expr mk_to_ieee_bv () const Convert this fpa into an IEEE BV. More...
expr mk_from_ieee_bv (sort const &s) const Convert this IEEE BV into a fpa. 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_string () const for a string value expression return an escaped string value. More...
std::u32string get_u32string () const for a string value expression return an unespaced string value. More...
operator Z3_app () const func_decl decl () const Return the declaration associated with this application. This method assumes the expression is an application. More...
unsigned num_args () const Return the number of arguments in this application. This method assumes the expression is an application. More...
expr arg (unsigned i) const Return the i-th argument of this application. This method assumes the expression is an application. More...
expr_vector args () const Return a vector of all the arguments 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) const expr rotate_right (unsigned i) const expr repeat (unsigned i) const expr extract (unsigned hi, unsigned lo) const expr bit2bool (unsigned i) 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) const expr at (expr const &index) const expr nth (expr const &index) const expr length () const expr stoi () const expr itos () const expr ubvtos () const expr sbvtos () const expr char_to_int () const expr char_to_bv () const expr char_from_bv () const expr is_digit () 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...
expr substitute (func_decl_vector const &funs, expr_vector const &bodies) Apply function substitution by macro definitions.
More...
iterator begin () iterator end () ast (context &c) ast (context &c, Z3_ast n) ast (ast const &s) ~ast () override 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) virtual ~object ()=default 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_xor (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 bvredor (expr const &a) expr bvredand (expr const &a) expr abs (expr const &a) expr sqrt (expr const &a, expr const &rm) expr fp_eq (expr const &a, expr const &b) 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 fpa_fp (expr const &sgn, expr const &exp, expr const &sig) Create an expression of FloatingPoint sort from three bit-vector expressions. More...
expr fpa_to_sbv (expr const &t, unsigned sz) Conversion of a floating-point term into a signed bit-vector. More...
expr fpa_to_ubv (expr const &t, unsigned sz) Conversion of a floating-point term into an unsigned bit-vector. More...
expr sbv_to_fpa (expr const &t, sort s) Conversion of a signed bit-vector term into a floating-point. More...
expr ubv_to_fpa (expr const &t, sort s) Conversion of an unsigned bit-vector term into a floating-point. More...
expr fpa_to_fpa (expr const &t, sort s) Conversion of a floating-point term into another floating-point. More...
expr round_fpa_to_closest_integer (expr const &t) Round a floating-point term into its closest integer. 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 811 of file z3++.h.

◆ expr() [1/2]

Definition at line 813 of file z3++.h.

Referenced by expr::algebraic_lower(), expr::algebraic_upper(), expr::arg(), expr::at(), expr::bit2bool(), expr::body(), expr::char_from_bv(), expr::char_to_bv(), expr::char_to_int(), expr::contains(), expr::denominator(), expr::extract(), expr::is_digit(), expr::itos(), expr::length(), expr::loop(), expr::mk_from_ieee_bv(), expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), expr::mk_to_ieee_bv(), expr::nth(), expr::numerator(), expr::repeat(), expr::replace(), expr::rotate_left(), expr::rotate_right(), expr::sbvtos(), expr::simplify(), expr::stoi(), expr::substitute(), expr::ubvtos(), and expr::unit().

◆ expr() [2/2] ◆ algebraic_i() unsigned algebraic_i ( ) const inline

Return i of an algebraic number (root-obj p i)

Definition at line 1047 of file z3++.h.

bool is_algebraic() const

Return true if expression is an algebraic number.

Z3_error_code check_error() const

unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)

Return which root of the polynomial the algebraic number represents.

◆ 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 1020 of file z3++.h.

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...

◆ algebraic_poly()

Return coefficients for p of an algebraic number (root-obj p i)

Definition at line 1037 of file z3++.h.

Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)

Return the coefficients of the defining polynomial.

System.IntPtr Z3_ast_vector

ast_vector_tpl< expr > expr_vector

◆ algebraic_upper() expr algebraic_upper ( unsigned precision ) const inline

Definition at line 1027 of file z3++.h.

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...

◆ arg() expr arg ( unsigned i ) const inline ◆ args()

Return a vector of all the arguments of this application. This method assumes the expression is an application.

Precondition: is_app()

Definition at line 1215 of file z3++.h.

1218 for

(

unsigned

i = 0; i < argCnt; i++)

1219

vec.push_back(

arg

(i));

unsigned num_args() const

Return the number of arguments in this application. This method assumes the expression is an applicat...

expr arg(unsigned i) const

Return the i-th argument of this application. This method assumes the expression is an application.

◆ as_binary() bool as_binary ( std::string & s ) const inline

Definition at line 889 of file z3++.h.

bool is_numeral() const

Return true if this expression is a numeral. Specialized functions also return representations for th...

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.

◆ as_double() double as_double ( ) const inline ◆ as_int64() int64_t as_int64 ( ) const inline

Definition at line 893 of file z3++.h.

bool is_numeral_i64(int64_t &i) const

◆ as_uint64() uint64_t as_uint64 ( ) const inline

Definition at line 892 of file z3++.h.

bool is_numeral_u64(uint64_t &i) const

◆ at()

Definition at line 1488 of file z3++.h.

friend void check_context(object const &a, object const &b)

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...

◆ begin()

Definition at line 1617 of file z3++.h.

1617

{

return

iterator(*

this

, 0); }

◆ bit2bool() expr bit2bool ( unsigned i ) const inline

Definition at line 1418 of file z3++.h.

Z3_error_code check_error() const

Auxiliary method used to check for API usage errors.

Z3_ast Z3_API Z3_mk_bit2bool(Z3_context c, unsigned i, Z3_ast t1)

Extracts the bit at position i of a bit-vector and yields a boolean.

◆ body()

Return the 'body' of this quantifier.

Precondition: is_quantifier()

Definition at line 1228 of file z3++.h.

bool is_quantifier() const

Return true if this expression is a quantifier.

Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)

Return body of quantifier.

Referenced by QuantifierRef::children().

◆ bool_value()

Definition at line 1133 of file z3++.h.

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.

◆ char_from_bv() expr char_from_bv ( ) const inline

Definition at line 1535 of file z3++.h.

Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv)

Create a character from a bit-vector (code point).

◆ char_to_bv() expr char_to_bv ( ) const inline

Definition at line 1530 of file z3++.h.

Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch)

Create a bit-vector (code point) from character.

◆ char_to_int() expr char_to_int ( ) const inline

Definition at line 1525 of file z3++.h.

Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)

Create an integer (code point) from character.

◆ contains()

Definition at line 1482 of file z3++.h.

Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)

Check if container contains containee.

◆ decl()

Return the declaration associated with this application. This method assumes the expression is an application.

Precondition: is_app()

Definition at line 1193 of file z3++.h.

Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)

Return the declaration of a constant or function application.

System.IntPtr Z3_func_decl

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(), expr::lo(), and ExprRef::params().

◆ denominator() expr denominator ( ) const inline ◆ end()

Definition at line 1618 of file z3++.h.

bool is_app() const

Return true if this expression is an application.

◆ 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 1467 of file z3++.h.

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.

◆ extract() [2/2] expr extract ( unsigned hi, unsigned lo ) const inline

Definition at line 1417 of file z3++.h.

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,...

◆ 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 1012 of file z3++.h.

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.

◆ 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 1069 of file z3++.h.

1072

assert(

ctx

().enable_exceptions());

1073 if

ctx

().enable_exceptions())

return

1074 Z3_THROW

(exception(

"numeral does not fit in machine int"

));

bool is_numeral_i(int &i) const

◆ 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 1105 of file z3++.h.

1109

assert(

ctx

().enable_exceptions());

1110 if

ctx

().enable_exceptions())

return

1111 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 1088 of file z3++.h.

1090 unsigned

result = 0;

1092

assert(

ctx

().enable_exceptions());

1093 if

ctx

().enable_exceptions())

return

1094 Z3_THROW

(exception(

"numeral does not fit in machine uint"

));

bool is_numeral_u(unsigned &i) const

◆ 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 1122 of file z3++.h.

1124

uint64_t result = 0;

1126

assert(

ctx

().enable_exceptions());

1127 if

ctx

().enable_exceptions())

return

1128 Z3_THROW

(exception(

"numeral does not fit in machine uint64_t"

));

◆ get_sort()

Return the sort of this expression.

Definition at line 819 of file z3++.h.

Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)

Return the sort of an AST node.

Referenced by z3::ashr(), 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::select(), solver::set_initial_value(), optimize::set_initial_value(), z3::sge(), z3::sgt(), z3::shl(), z3::sle(), z3::slt(), z3::smod(), ModelRef::sorts(), 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

for a string value expression return an escaped string value.

Precondition: expression is for a string value.

Definition at line 1164 of file z3++.h.

1168 return

std::string(s);

bool is_string_value() const

Return true if this expression is a string literal. The string can be accessed using get_string() and...

Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)

Retrieve the string constant stored in s. Characters outside the basic printable ASCII range are esca...

◆ get_u32string() std::u32string get_u32string ( ) const inline

for a string value expression return an unespaced string value.

Precondition: expression is for a string value.

Definition at line 1176 of file z3++.h.

void Z3_API Z3_get_string_contents(Z3_context c, Z3_ast s, unsigned length, unsigned contents[])

Retrieve the unescaped string constant stored in s.

unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s)

Retrieve the length of the unescaped string constant stored in s.

◆ hi()

Definition at line 1420 of file z3++.h.

func_decl decl() const

Return the declaration associated with this application. This method assumes the expression is an app...

unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)

Return the number of parameters associated with a declaration.

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.

Referenced by expr::extract(), and expr::loop().

◆ id()

retrieve unique identifier for expression.

Definition at line 1057 of file z3++.h.

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....

◆ is_algebraic() bool is_algebraic ( ) const inline ◆ is_and()

Definition at line 1297 of file z3++.h.

Z3_decl_kind decl_kind() const

◆ is_app()

Return true if this expression is an application.

Definition at line 899 of file z3++.h.

Referenced by expr::end(), 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 836 of file z3++.h.

sort get_sort() const

Return the sort of this expression.

bool is_arith() const

Return true if this sort is the Integer or Real sort.

◆ is_array()

Return true if this is a Array expression.

Definition at line 844 of file z3++.h.

bool is_array() const

Return true if this sort is a Array sort.

Referenced by expr::operator[]().

◆ is_bool() ◆ is_bv()

Return true if this is a Bit-vector expression.

Definition at line 840 of file z3++.h.

bool is_bv() const

Return true if this sort is a Bit-vector sort.

Referenced by expr::mk_from_ieee_bv().

◆ is_const()

Return true if this expression is a constant (i.e., an application with 0 arguments).

Definition at line 903 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 848 of file z3++.h.

bool is_datatype() const

Return true if this sort is a Datatype sort.

◆ is_digit()

Definition at line 1540 of file z3++.h.

Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch)

Create a check if the character is a digit.

◆ is_distinct() bool is_distinct ( ) const inline ◆ is_eq() ◆ is_exists()

Return true if this expression is an existential quantifier.

Definition at line 916 of file z3++.h.

bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)

Determine if ast is an existential quantifier.

◆ is_false() ◆ is_finite_domain() bool is_finite_domain ( ) const inline

Return true if this is a Finite-domain expression.

Definition at line 870 of file z3++.h.

bool is_finite_domain() const

Return true if this sort is a Finite domain sort.

◆ is_forall()

Return true if this expression is a universal quantifier.

Definition at line 912 of file z3++.h.

bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)

Determine if an ast is a universal quantifier.

◆ is_fpa() ◆ is_implies() bool is_implies ( ) const inline ◆ is_int() ◆ is_ite() ◆ is_lambda() ◆ is_not() ◆ is_numeral() [1/4] bool is_numeral ( ) const inline ◆ is_numeral() [2/4] bool is_numeral ( double & d ) const inline

Definition at line 888 of file z3++.h.

double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)

Return numeral as a double.

Referenced by expr::is_numeral().

◆ is_numeral() [3/4] bool is_numeral ( std::string & s ) const inline

Definition at line 886 of file z3++.h.

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.

Referenced by expr::is_numeral().

◆ 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

Definition at line 884 of file z3++.h.

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....

Referenced by expr::get_numeral_int().

◆ is_numeral_i64() bool is_numeral_i64 ( int64_t & i ) const inline

Definition at line 882 of file z3++.h.

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....

Referenced by expr::as_int64(), and expr::get_numeral_int64().

◆ is_numeral_u() bool is_numeral_u ( unsigned & i ) const inline

Definition at line 885 of file z3++.h.

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....

Referenced by expr::get_numeral_uint().

◆ is_numeral_u64() bool is_numeral_u64 ( uint64_t & i ) const inline

Definition at line 883 of file z3++.h.

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....

Referenced by expr::as_uint64(), and expr::get_numeral_uint64().

◆ is_or() ◆ is_quantifier() bool is_quantifier ( ) const inline

Return true if this expression is a quantifier.

Definition at line 907 of file z3++.h.

Referenced by expr::body().

◆ is_re()

Return true if this is a regular expression.

Definition at line 860 of file z3++.h.

bool is_re() const

Return true if this sort is a regular expression sort.

◆ is_real()

Return true if this is a real expression.

Definition at line 832 of file z3++.h.

bool is_real() const

Return true if this sort is the Real sort.

◆ is_relation() bool is_relation ( ) const inline

Return true if this is a Relation expression.

Definition at line 852 of file z3++.h.

bool is_relation() const

Return true if this sort is a Relation sort.

◆ is_seq()

Return true if this is a sequence expression.

Definition at line 856 of file z3++.h.

bool is_seq() const

Return true if this sort is a Sequence sort.

Referenced by expr::operator[]().

◆ is_string_value() bool is_string_value ( ) const inline ◆ is_true() ◆ is_var()

Return true if this expression is a variable.

Definition at line 925 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 934 of file z3++.h.

bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)

Return true if the given expression t is well sorted.

◆ is_xor() ◆ itos()

Definition at line 1510 of file z3++.h.

Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)

Integer to string conversion.

◆ length()

Definition at line 1500 of file z3++.h.

Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)

Return the length of the sequence s.

Referenced by expr::extract().

◆ lo() ◆ loop() [1/2] expr loop ( unsigned lo ) inline

create a looping regular expression.

Definition at line 1550 of file z3++.h.

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...

◆ loop() [2/2] expr loop ( unsigned lo, unsigned hi ) inline ◆ mk_from_ieee_bv() expr mk_from_ieee_bv ( sort const & s ) const inline

Convert this IEEE BV into a fpa.

Definition at line 999 of file z3++.h.

bool is_bv() const

Return true if this is a Bit-vector expression.

Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)

Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.

◆ mk_is_inf()

Return Boolean expression to test for whether an FP expression is inf.

Definition at line 939 of file z3++.h.

bool is_fpa() const

Return true if this is a FloatingPoint expression. .

Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t)

Predicate indicating whether t is a floating-point number representing +oo or -oo.

◆ mk_is_nan()

Return Boolean expression to test for whether an FP expression is a NaN.

Definition at line 949 of file z3++.h.

Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t)

Predicate indicating whether t is a NaN.

◆ mk_is_normal() expr mk_is_normal ( ) const inline

Return Boolean expression to test for whether an FP expression is a normal.

Definition at line 959 of file z3++.h.

Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t)

Predicate indicating whether t is a normal floating-point number.

◆ mk_is_subnormal() expr mk_is_subnormal ( ) const inline

Return Boolean expression to test for whether an FP expression is a subnormal.

Definition at line 969 of file z3++.h.

Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t)

Predicate indicating whether t is a subnormal floating-point number.

◆ mk_is_zero() expr mk_is_zero ( ) const inline

Return Boolean expression to test for whether an FP expression is a zero.

Definition at line 979 of file z3++.h.

Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t)

Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.

◆ mk_to_ieee_bv() expr mk_to_ieee_bv ( ) const inline

Convert this fpa into an IEEE BV.

Definition at line 989 of file z3++.h.

Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t)

Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.

◆ nth()

Definition at line 1494 of file z3++.h.

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...

Referenced by expr::operator[]().

◆ num_args() unsigned num_args ( ) const inline ◆ numerator()

Definition at line 1137 of file z3++.h.

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.

Referenced by RatNumRef::numerator_as_long().

◆ operator Z3_app() operator Z3_app ( ) const inline ◆ operator[]() [1/2] expr operator[] ( expr const & index ) const inline

index operator defined on arrays and sequences.

Definition at line 1564 of file z3++.h.

1567 return select

this

, index);

bool is_array() const

Return true if this is a Array expression.

expr nth(expr const &index) const

bool is_seq() const

Return true if this is a sequence expression.

expr select(expr const &a, expr const &i)

forward declarations

◆ operator[]() [2/2] ◆ repeat() expr repeat ( unsigned i ) const inline

Definition at line 1407 of file z3++.h.

Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)

Repeat the given bit-vector up length i.

◆ replace()

Definition at line 1471 of file z3++.h.

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.

◆ rotate_left() expr rotate_left ( unsigned i ) const inline

Definition at line 1405 of file z3++.h.

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.

◆ rotate_right() expr rotate_right ( unsigned i ) const inline

Definition at line 1406 of file z3++.h.

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.

◆ sbvtos()

Definition at line 1520 of file z3++.h.

Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s)

Signed bit-vector to string conversion.

◆ simplify() [1/2]

Return a simplified version of this expression.

Definition at line 1579 of file z3++.h.

Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)

Interface to simplifier.

◆ 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 1583 of file z3++.h.

Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)

Interface to simplifier.

◆ stoi()

Definition at line 1505 of file z3++.h.

Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)

Convert string to integer.

◆ substitute() [1/3]

Apply substitution. Replace bound variables by expressions.

Definition at line 4242 of file z3++.h.

4243

array<Z3_ast> _dst(dst.size());

4244 for

(

unsigned

i = 0; i < dst.size(); ++i) {

Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])

Substitute the variables in a with the expressions in to. For every i smaller than num_exprs,...

◆ substitute() [2/3]

Apply substitution. Replace src expressions by dst.

Definition at line 4229 of file z3++.h.

4230

assert(src.size() == dst.size());

4231

array<Z3_ast> _src(src.size());

4232

array<Z3_ast> _dst(dst.size());

4233 for

(

unsigned

i = 0; i < src.size(); ++i) {

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....

◆ substitute() [3/3]

Apply function substitution by macro definitions.

Definition at line 4252 of file z3++.h.

4253

array<Z3_ast> _dst(dst.size());

4254

array<Z3_func_decl> _funs(funs.size());

4255 if

(dst.size() != funs.size()) {

4256 Z3_THROW

(exception(

"length of argument lists don't align"

));

4257 return expr

(

ctx

(),

nullptr

);

4259 for

(

unsigned

i = 0; i < dst.size(); ++i) {

Z3_ast Z3_API Z3_substitute_funs(Z3_context c, Z3_ast a, unsigned num_funs, Z3_func_decl const from[], Z3_ast const to[])

Substitute functions in from with new expressions in to.

◆ ubvtos()

Definition at line 1515 of file z3++.h.

Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s)

Unsigned bit-vector to string conversion.

◆ unit()

Definition at line 1477 of file z3++.h.

Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)

Create a unit sequence of a.

◆ abs

Definition at line 1995 of file z3++.h.

1998 expr

zero = a.ctx().int_val(0);

1999 expr

ge = a >= zero;

2003 else if

(a.is_real()) {

2004 expr

zero = a.ctx().real_val(0);

2005 expr

ge = a >= zero;

2013 return expr

(a.ctx(), r);

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_fpa_abs(Z3_context c, Z3_ast t)

Floating-point absolute value.

◆ atleast

Definition at line 2430 of file z3++.h.

2431

assert(es.size() > 0);

2432

context&

ctx

= es[0u].ctx();

2433

array<Z3_ast> _es(es);

Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)

Pseudo-Boolean relations.

◆ atmost

Definition at line 2422 of file z3++.h.

2423

assert(es.size() > 0);

2424

context&

ctx

= es[0u].ctx();

2425

array<Z3_ast> _es(es);

Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)

Pseudo-Boolean relations.

◆ bv2int expr bv2int ( expr const & a, bool is_signed ) friend

bit-vector and integer conversions.

Definition at line 2233 of file z3++.h.

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...

◆ 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 2239 of file z3++.h.

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.

◆ bvadd_no_underflow

Definition at line 2242 of file z3++.h.

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.

◆ bvmul_no_overflow expr bvmul_no_overflow ( expr const & a, expr const & b, bool is_signed ) friend

Definition at line 2257 of file z3++.h.

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.

◆ bvmul_no_underflow

Definition at line 2260 of file z3++.h.

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...

◆ bvneg_no_overflow expr bvneg_no_overflow ( expr const & a ) friend

Definition at line 2254 of file z3++.h.

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.

◆ bvredand

Definition at line 1989 of file z3++.h.

1993 return expr

(a.ctx(), r);

Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)

Take conjunction of bits in vector, return vector of length 1.

◆ bvredor

Definition at line 1983 of file z3++.h.

1987 return expr

(a.ctx(), r);

Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)

Take disjunction of bits in vector, return vector of length 1.

◆ bvsdiv_no_overflow

Definition at line 2251 of file z3++.h.

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.

◆ bvsub_no_overflow

Definition at line 2245 of file z3++.h.

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.

◆ bvsub_no_underflow expr bvsub_no_underflow ( expr const & a, expr const & b, bool is_signed ) friend

Definition at line 2248 of file z3++.h.

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.

◆ concat [1/2]

Definition at line 2456 of file z3++.h.

2460 Z3_ast

_args[2] = { a, b };

2464 Z3_ast

_args[2] = { a, b };

2470

a.ctx().check_error();

2471 return expr

(a.ctx(), r);

bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)

Check if s is a sequence 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_re_concat(Z3_context c, unsigned n, Z3_ast const args[])

Create the concatenation of the regular languages.

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_re_sort(Z3_context c, Z3_sort s)

Check if s is a regular expression sort.

◆ concat [2/2]

Definition at line 2474 of file z3++.h.

2481

array<Z3_ast> _args(

args

);

2490 for

(

unsigned

i =

args

size

()-1; i > 0; ) {

expr_vector args() const

Return a vector of all the arguments of this application. This method assumes the expression is an ap...

◆ distinct

Definition at line 2447 of file z3++.h.

2450

array<Z3_ast> _args(

args

);

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]).

◆ fma

FloatingPoint fused multiply-add.

Definition at line 2031 of file z3++.h.

2033

assert(a.is_fpa() && b.is_fpa() && c.is_fpa());

2036 return expr

(a.ctx(), r);

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.

◆ fp_eq

Definition at line 2022 of file z3++.h.

2027 return expr

(a.ctx(), r);

Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point equality.

◆ fpa_fp

Create an expression of FloatingPoint sort from three bit-vector expressions.

Definition at line 2039 of file z3++.h.

2041

assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());

2044 return expr

(sgn.ctx(), r);

Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)

Create an expression of FloatingPoint sort from three bit-vector expressions.

◆ fpa_to_fpa

Conversion of a floating-point term into another floating-point.

Definition at line 2075 of file z3++.h.

2079 return expr

(t.ctx(), r);

Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)

Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

◆ fpa_to_sbv expr fpa_to_sbv ( expr const & t, unsigned sz ) friend

Conversion of a floating-point term into a signed bit-vector.

Definition at line 2047 of file z3++.h.

2051 return expr

(t.ctx(), r);

Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)

Conversion of a floating-point term into a signed bit-vector.

◆ fpa_to_ubv expr fpa_to_ubv ( expr const & t, unsigned sz ) friend

Conversion of a floating-point term into an unsigned bit-vector.

Definition at line 2054 of file z3++.h.

2058 return expr

(t.ctx(), r);

Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)

Conversion of a floating-point term into an unsigned bit-vector.

◆ implies [1/3]

Definition at line 1634 of file z3++.h.

1634

{

return implies

(b.ctx().bool_val(a), b); }

friend expr implies(expr const &a, expr const &b)

◆ implies [2/3]

Definition at line 1633 of file z3++.h.

1633

{

return implies

(a, a.ctx().bool_val(b)); }

◆ implies [3/3]

Definition at line 1629 of file z3++.h.

1630

assert(a.is_bool() && b.is_bool());

Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)

Create an AST node representing t1 implies t2.

#define _Z3_MK_BIN_(a, b, binop)

◆ int2bv expr int2bv ( unsigned n, expr const & a ) friend

Definition at line 2234 of file z3++.h.

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.

◆ is_int ◆ ite

Create the if-then-else expression ite(c, t, e)

Precondition: c.is_bool()

Definition at line 2094 of file z3++.h.

2096

assert(c.is_bool());

2099 return expr

(c.ctx(), r);

◆ max

Definition at line 1967 of file z3++.h.

1973 else if

(a.is_bv()) {

1981 return expr

(a.ctx(), r);

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_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)

Maximum of floating-point numbers.

Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)

Unsigned greater than or equal to.

◆ min

Definition at line 1951 of file z3++.h.

1957 else if

(a.is_bv()) {

1965 return expr

(a.ctx(), r);

Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)

Minimum of floating-point numbers.

◆ mk_and

Definition at line 2534 of file z3++.h.

2535

array<Z3_ast> _args(

args

);

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].

◆ mk_or

Definition at line 2528 of file z3++.h.

2529

array<Z3_ast> _args(

args

);

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].

◆ mk_xor

Definition at line 2540 of file z3++.h.

2544 for

(

unsigned

i = 1; i <

args

size

(); ++i)

◆ mod [1/3]

Definition at line 1641 of file z3++.h.

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_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed remainder (sign follows divisor).

◆ mod [2/3]

Definition at line 1649 of file z3++.h.

1649

{

return mod

(a, a.ctx().num_val(b, a.get_sort())); }

friend expr mod(expr const &a, expr const &b)

◆ mod [3/3]

Definition at line 1650 of file z3++.h.

1650

{

return mod

(b.ctx().num_val(a, b.get_sort()), b); }

◆ nand

Definition at line 1948 of file z3++.h.

Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise nand.

◆ nor

Definition at line 1949 of file z3++.h.

Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise nor.

◆ operator!

Return an expression representing not(a).

Precondition: a.is_bool()

Definition at line 1675 of file z3++.h.

Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)

Create an AST node representing not(a).

◆ operator!= [1/3]

Definition at line 1717 of file z3++.h.

1722 return expr

(a.ctx(), r);

◆ operator!= [2/3]

Definition at line 1724 of file z3++.h.

1724

{ 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 1725 of file z3++.h.

1725

{ 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 1936 of file z3++.h.

Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise and.

◆ operator& [2/3] expr operator& ( expr const & a, int b ) friend

Definition at line 1937 of file z3++.h.

1937

{

return

a & a.ctx().num_val(b, a.get_sort()); }

◆ operator& [3/3] expr operator& ( int a, expr const & b ) friend

Definition at line 1938 of file z3++.h.

1938

{

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 1691 of file z3++.h.

1691

{

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 1690 of file z3++.h.

1690

{

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 1681 of file z3++.h.

1683

assert(a.is_bool() && b.is_bool());

1687 return expr

(a.ctx(), r);

◆ operator* [1/3]

Definition at line 1759 of file z3++.h.

1762 if

(a.is_arith() && b.is_arith()) {

1766 else if

(a.is_bv() && b.is_bv()) {

1769 else if

(a.is_fpa() && b.is_fpa()) {

1770

r =

Z3_mk_fpa_mul

(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);

1777 return expr

(a.ctx(), r);

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_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)

Standard two's complement multiplication.

Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)

Floating-point multiplication.

◆ operator* [2/3] expr operator* ( expr const & a, int b ) friend

Definition at line 1779 of file z3++.h.

1779

{

return

a * a.ctx().num_val(b, a.get_sort()); }

◆ operator* [3/3] expr operator* ( int a, expr const & b ) friend

Definition at line 1780 of file z3++.h.

1780

{

return

b.ctx().num_val(a, b.get_sort()) * b; }

◆ operator+ [1/3]

Definition at line 1729 of file z3++.h.

1732 if

(a.is_arith() && b.is_arith()) {

1736 else if

(a.is_bv() && b.is_bv()) {

1739 else if

(a.is_seq() && b.is_seq()) {

1742 else if

(a.is_re() && b.is_re()) {

1743 Z3_ast

_args[2] = { a, b };

1746 else if

(a.is_fpa() && b.is_fpa()) {

1747

r =

Z3_mk_fpa_add

(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);

1754 return expr

(a.ctx(), r);

friend expr concat(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_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)

Standard two's complement addition.

Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)

Floating-point addition.

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].

◆ operator+ [2/3] expr operator+ ( expr const & a, int b ) friend

Definition at line 1756 of file z3++.h.

1756

{

return

a + a.ctx().num_val(b, a.get_sort()); }

◆ operator+ [3/3] expr operator+ ( int a, expr const & b ) friend

Definition at line 1757 of file z3++.h.

1757

{

return

b.ctx().num_val(a, b.get_sort()) + b; }

◆ operator- [1/4]

Definition at line 1825 of file z3++.h.

1830 else if

(a.is_bv()) {

1833 else if

(a.is_fpa()) {

1841 return expr

(a.ctx(), r);

Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)

Create an AST node representing - arg.

Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)

Floating-point negation.

Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)

Standard two's complement unary minus.

◆ operator- [2/4]

Definition at line 1844 of file z3++.h.

1847 if

(a.is_arith() && b.is_arith()) {

1851 else if

(a.is_bv() && b.is_bv()) {

1854 else if

(a.is_fpa() && b.is_fpa()) {

1855

r =

Z3_mk_fpa_sub

(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);

1862 return expr

(a.ctx(), r);

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_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)

Standard two's complement subtraction.

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].

◆ operator- [3/4] expr operator- ( expr const & a, int b ) friend

Definition at line 1864 of file z3++.h.

1864

{

return

a - a.ctx().num_val(b, a.get_sort()); }

◆ operator- [4/4] expr operator- ( int a, expr const & b ) friend

Definition at line 1865 of file z3++.h.

1865

{

return

b.ctx().num_val(a, b.get_sort()) - b; }

◆ operator/ [1/3]

Definition at line 1803 of file z3++.h.

1806 if

(a.is_arith() && b.is_arith()) {

1809 else if

(a.is_bv() && b.is_bv()) {

1812 else if

(a.is_fpa() && b.is_fpa()) {

1813

r =

Z3_mk_fpa_div

(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);

1820 return expr

(a.ctx(), r);

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_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)

Two's complement signed division.

Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)

Floating-point division.

◆ operator/ [2/3] expr operator/ ( expr const & a, int b ) friend

Definition at line 1822 of file z3++.h.

1822

{

return

a / a.ctx().num_val(b, a.get_sort()); }

◆ operator/ [3/3] expr operator/ ( int a, expr const & b ) friend

Definition at line 1823 of file z3++.h.

1823

{

return

b.ctx().num_val(a, b.get_sort()) / b; }

◆ operator< [1/3]

Definition at line 1892 of file z3++.h.

1895 if

(a.is_arith() && b.is_arith()) {

1898 else if

(a.is_bv() && b.is_bv()) {

1901 else if

(a.is_fpa() && b.is_fpa()) {

1909 return expr

(a.ctx(), r);

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_lt(Z3_context c, Z3_ast t1, Z3_ast t2)

Create less than.

Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point less than.

◆ operator< [2/3] expr operator< ( expr const & a, int b ) friend

Definition at line 1911 of file z3++.h.

1911

{

return

a < a.ctx().num_val(b, a.get_sort()); }

◆ operator< [3/3] expr operator< ( int a, expr const & b ) friend

Definition at line 1912 of file z3++.h.

1912

{

return

b.ctx().num_val(a, b.get_sort()) < b; }

◆ operator<= [1/3]

Definition at line 1867 of file z3++.h.

1870 if

(a.is_arith() && b.is_arith()) {

1873 else if

(a.is_bv() && b.is_bv()) {

1876 else if

(a.is_fpa() && b.is_fpa()) {

1884 return expr

(a.ctx(), r);

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_le(Z3_context c, Z3_ast t1, Z3_ast t2)

Create less than or equal to.

Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point less than or equal.

◆ operator<= [2/3] expr operator<= ( expr const & a, int b ) friend

Definition at line 1886 of file z3++.h.

1886

{

return

a <= a.ctx().num_val(b, a.get_sort()); }

◆ operator<= [3/3] expr operator<= ( int a, expr const & b ) friend

Definition at line 1887 of file z3++.h.

1887

{

return

b.ctx().num_val(a, b.get_sort()) <= b; }

◆ operator== [1/3]

Definition at line 1706 of file z3++.h.

1710 return expr

(a.ctx(), r);

Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)

Create an AST node representing l = r.

◆ operator== [2/3] expr operator== ( expr const & a, int b ) friend

Definition at line 1712 of file z3++.h.

1712

{ 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 1713 of file z3++.h.

1713

{ 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 1914 of file z3++.h.

1917 if

(a.is_arith() && b.is_arith()) {

1920 else if

(a.is_bv() && b.is_bv()) {

1923 else if

(a.is_fpa() && b.is_fpa()) {

1931 return expr

(a.ctx(), r);

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_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point greater than.

Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)

Create greater than.

◆ operator> [2/3] expr operator> ( expr const & a, int b ) friend

Definition at line 1933 of file z3++.h.

1933

{

return

a > a.ctx().num_val(b, a.get_sort()); }

◆ operator> [3/3] expr operator> ( int a, expr const & b ) friend

Definition at line 1934 of file z3++.h.

1934

{

return

b.ctx().num_val(a, b.get_sort()) > b; }

◆ operator>= [1/3]

Definition at line 1783 of file z3++.h.

1786 if

(a.is_arith() && b.is_arith()) {

1789 else if

(a.is_bv() && b.is_bv()) {

1792 else if

(a.is_fpa() && b.is_fpa()) {

1800 return expr

(a.ctx(), r);

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_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point greater than or equal.

◆ operator>= [2/3] expr operator>= ( expr const & a, int b ) friend

Definition at line 1889 of file z3++.h.

1889

{

return

a >= a.ctx().num_val(b, a.get_sort()); }

◆ operator>= [3/3] expr operator>= ( int a, expr const & b ) friend

Definition at line 1890 of file z3++.h.

1890

{

return

b.ctx().num_val(a, b.get_sort()) >= b; }

◆ operator^ [1/3]

Definition at line 1940 of file z3++.h.

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_xor(Z3_context c, Z3_ast t1, Z3_ast t2)

Create an AST node representing t1 xor t2.

◆ operator^ [2/3] expr operator^ ( expr const & a, int b ) friend

Definition at line 1941 of file z3++.h.

1941

{

return

a ^ a.ctx().num_val(b, a.get_sort()); }

◆ operator^ [3/3] expr operator^ ( int a, expr const & b ) friend

Definition at line 1942 of file z3++.h.

1942

{

return

b.ctx().num_val(a, b.get_sort()) ^ b; }

◆ operator| [1/3]

Definition at line 1944 of file z3++.h.

Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise or.

◆ operator| [2/3] expr operator| ( expr const & a, int b ) friend

Definition at line 1945 of file z3++.h.

1945

{

return

a | a.ctx().num_val(b, a.get_sort()); }

◆ operator| [3/3] expr operator| ( int a, expr const & b ) friend

Definition at line 1946 of file z3++.h.

1946

{

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 1704 of file z3++.h.

1704

{

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 1702 of file z3++.h.

1702

{

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 1693 of file z3++.h.

1695

assert(a.is_bool() && b.is_bool());

1699 return expr

(a.ctx(), r);

◆ operator~

Definition at line 2029 of file z3++.h.

Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)

Bitwise negation.

◆ pbeq

Definition at line 2414 of file z3++.h.

2415

assert(es.size() > 0);

2416

context&

ctx

= es[0u].ctx();

2417

array<Z3_ast> _es(es);

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.

◆ pbge

Definition at line 2406 of file z3++.h.

2407

assert(es.size() > 0);

2408

context&

ctx

= es[0u].ctx();

2409

array<Z3_ast> _es(es);

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.

◆ pble

Definition at line 2398 of file z3++.h.

2399

assert(es.size() > 0);

2400

context&

ctx

= es[0u].ctx();

2401

array<Z3_ast> _es(es);

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.

◆ pw [1/3]

Definition at line 1637 of file z3++.h.

Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Create an AST node representing arg1 ^ arg2.

◆ pw [2/3]

Definition at line 1638 of file z3++.h.

1638

{

return pw

(a, a.ctx().num_val(b, a.get_sort())); }

friend expr pw(expr const &a, expr const &b)

◆ pw [3/3]

Definition at line 1639 of file z3++.h.

1639

{

return pw

(b.ctx().num_val(a, b.get_sort()), b); }

◆ range

Definition at line 4136 of file z3++.h.

4140 return expr

(

.ctx(), r);

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.

◆ rem [1/3]

Definition at line 1657 of file z3++.h.

1658 if

(a.is_fpa() && b.is_fpa()) {

Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)

Floating-point remainder.

Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)

Create an AST node representing arg1 rem arg2.

◆ rem [2/3]

Definition at line 1664 of file z3++.h.

1664

{

return rem

(a, a.ctx().num_val(b, a.get_sort())); }

friend expr rem(expr const &a, expr const &b)

◆ rem [3/3]

Definition at line 1665 of file z3++.h.

1665

{

return rem

(b.ctx().num_val(a, b.get_sort()), b); }

◆ round_fpa_to_closest_integer expr round_fpa_to_closest_integer ( expr const & t ) friend

Round a floating-point term into its closest integer.

Definition at line 2082 of file z3++.h.

2086 return expr

(t.ctx(), r);

Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t)

Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...

◆ sbv_to_fpa

Conversion of a signed bit-vector term into a floating-point.

Definition at line 2061 of file z3++.h.

2065 return expr

(t.ctx(), r);

Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)

Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.

◆ sqrt

Definition at line 2015 of file z3++.h.

2020 return expr

(a.ctx(), r);

Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)

Floating-point square root.

◆ sum

Definition at line 2438 of file z3++.h.

2441

array<Z3_ast> _args(

args

);

◆ ubv_to_fpa

Conversion of an unsigned bit-vector term into a floating-point.

Definition at line 2068 of file z3++.h.

2072 return expr

(t.ctx(), r);

Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)

Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.

◆ xnor

Definition at line 1950 of file z3++.h.

Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)

Bitwise xnor.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4