Z3
 
Loading...
Searching...
No Matches
Data Structures | Public Member Functions | Friends
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...

#include <z3++.h>

+ Inheritance diagram for expr:

Data Structures

class  iterator
 

Public Member Functions

 expr (context &c)
 
 expr (context &c, Z3_ast n)
 
sort get_sort () const
 Return the sort of this expression.
 
bool is_bool () const
 Return true if this is a Boolean expression.
 
bool is_int () const
 Return true if this is an integer expression.
 
bool is_real () const
 Return true if this is a real expression.
 
bool is_arith () const
 Return true if this is an integer or real expression.
 
bool is_bv () const
 Return true if this is a Bit-vector expression.
 
bool is_array () const
 Return true if this is a Array expression.
 
bool is_datatype () const
 Return true if this is a Datatype expression.
 
bool is_relation () const
 Return true if this is a Relation expression.
 
bool is_seq () const
 Return true if this is a sequence expression.
 
bool is_re () const
 Return true if this is a regular expression.
 
bool is_finite_domain () const
 Return true if this is a Finite-domain expression.
 
bool is_fpa () const
 Return true if this is a FloatingPoint expression. .
 
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.
 
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.
 
bool is_const () const
 Return true if this expression is a constant (i.e., an application with 0 arguments).
 
bool is_quantifier () const
 Return true if this expression is a quantifier.
 
bool is_forall () const
 Return true if this expression is a universal quantifier.
 
bool is_exists () const
 Return true if this expression is an existential quantifier.
 
bool is_lambda () const
 Return true if this expression is a lambda expression.
 
bool is_var () const
 Return true if this expression is a variable.
 
bool is_algebraic () const
 Return true if expression is an algebraic number.
 
bool is_well_sorted () const
 Return true if this expression is well sorted (aka type correct).
 
expr mk_is_inf () const
 Return Boolean expression to test for whether an FP expression is inf.
 
expr mk_is_nan () const
 Return Boolean expression to test for whether an FP expression is a NaN.
 
expr mk_is_normal () const
 Return Boolean expression to test for whether an FP expression is a normal.
 
expr mk_is_subnormal () const
 Return Boolean expression to test for whether an FP expression is a subnormal.
 
expr mk_is_zero () const
 Return Boolean expression to test for whether an FP expression is a zero.
 
expr mk_to_ieee_bv () const
 Convert this fpa into an IEEE BV.
 
expr mk_from_ieee_bv (sort const &s) const
 Convert this IEEE BV into a fpa.
 
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.
 
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)
 
unsigned algebraic_i () const
 Return i of an algebraic number (root-obj p i)
 
unsigned id () const
 retrieve unique identifier for expression.
 
int get_numeral_int () const
 Return int value of numeral, throw if result cannot fit in machine int.
 
unsigned get_numeral_uint () const
 Return uint value of numeral, throw if result cannot fit in machine uint.
 
int64_t get_numeral_int64 () const
 Return int64_t value of numeral, throw if result cannot fit in int64_t.
 
uint64_t get_numeral_uint64 () const
 Return uint64_t value of numeral, throw if result cannot fit in uint64_t.
 
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()
 
std::string get_string () const
 for a string value expression return an escaped string value.
 
std::u32string get_u32string () const
 for a string value expression return an unespaced string value.
 
 operator Z3_app () const
 
func_decl decl () const
 Return the declaration associated with this application. This method assumes the expression is an application.
 
unsigned num_args () const
 Return the number of arguments in this application. This method assumes the expression is an application.
 
expr arg (unsigned i) const
 Return the i-th argument of this application. This method assumes the expression is an application.
 
expr_vector args () const
 Return a vector of all the arguments of this application. This method assumes the expression is an application.
 
expr body () const
 Return the 'body' of this quantifier.
 
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.
 
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.
 
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.
 
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.
 
expr substitute (expr_vector const &src, expr_vector const &dst)
 Apply substitution. Replace src expressions by dst.
 
expr substitute (expr_vector const &dst)
 Apply substitution. Replace bound variables by expressions.
 
expr substitute (func_decl_vector const &funs, expr_vector const &bodies)
 Apply function substitution by macro definitions.

 
iterator begin ()
 
iterator end ()
 
- Public Member Functions inherited from ast
 ast (context &c)
 
 ast (context &c, Z3_ast n)
 
 ast (ast const &s)
 
 ~ast ()
 
 operator Z3_ast () const
 
 operator bool () const
 
astoperator= (ast const &s)
 
Z3_ast_kind kind () const
 
unsigned hash () const
 
std::string to_string () const
 
- Public Member Functions inherited from object
 object (context &c)
 
contextctx () const
 
Z3_error_code check_error () const
 

Friends

expr operator! (expr const &a)
 Return an expression representing not(a).
 
expr operator&& (expr const &a, expr const &b)
 Return an expression representing a and b.
 
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.
 
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.
 
expr operator|| (expr const &a, expr const &b)
 Return an expression representing a or b.
 
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.
 
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.
 
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)
 
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.
 
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
 
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.
 
expr fpa_fp (expr const &sgn, expr const &exp, expr const &sig)
 Create an expression of FloatingPoint sort from three bit-vector expressions.
 
expr fpa_to_sbv (expr const &t, unsigned sz)
 Conversion of a floating-point term into a signed bit-vector.
 
expr fpa_to_ubv (expr const &t, unsigned sz)
 Conversion of a floating-point term into an unsigned bit-vector.
 
expr sbv_to_fpa (expr const &t, sort s)
 Conversion of a signed bit-vector term into a floating-point.
 
expr ubv_to_fpa (expr const &t, sort s)
 Conversion of an unsigned bit-vector term into a floating-point.
 
expr fpa_to_fpa (expr const &t, sort s)
 Conversion of a floating-point term into another floating-point.
 
expr round_fpa_to_closest_integer (expr const &t)
 Round a floating-point term into its closest integer.
 
expr range (expr const &lo, expr const &hi)
 

Additional Inherited Members

- Protected Attributes inherited from ast
Z3_ast m_ast
 
- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

◆ expr() [1/2]

expr ( context c)
inline

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

799:ast(c) {}
ast(context &c)
Definition: z3++.h:544

◆ expr() [2/2]

expr ( context c,
Z3_ast  n 
)
inline

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

800:ast(c, reinterpret_cast<Z3_ast>(n)) {}

Member Function Documentation

◆ algebraic_i()

unsigned algebraic_i ( ) const
inline

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

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

1033 {
1034 assert(is_algebraic());
1035 unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
1036 check_error();
1037 return i;
1038 }
Z3_ast m_ast
Definition: z3++.h:542
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:915
Z3_error_code check_error() const
Definition: z3++.h:464
context & ctx() const
Definition: z3++.h:463
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 1006 of file z3++.h.

1006 {
1007 assert(is_algebraic());
1008 Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
1009 check_error();
1010 return expr(ctx(), r);
1011 }
expr(context &c)
Definition: z3++.h:799
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()

expr_vector algebraic_poly ( ) const
inline

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

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

1023 {
1024 assert(is_algebraic());
1025 Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
1026 check_error();
1027 return expr_vector(ctx(), r);
1028 }
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:75

◆ algebraic_upper()

expr algebraic_upper ( unsigned  precision) const
inline

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

1013 {
1014 assert(is_algebraic());
1015 Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
1016 check_error();
1017 return expr(ctx(), r);
1018 }
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

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

Precondition
is_app()
i < num_args()

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

1194{ Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
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.

Referenced by AstRef::__bool__(), expr::args(), ExprRef::children(), and expr::iterator::operator*().

◆ args()

expr_vector args ( ) const
inline

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

Precondition
is_app()

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

1201 {
1202 expr_vector vec(ctx());
1203 unsigned argCnt = num_args();
1204 for (unsigned i = 0; i < argCnt; i++)
1205 vec.push_back(arg(i));
1206 return vec;
1207 }
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:1186
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application.
Definition: z3++.h:1194

◆ as_binary()

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

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

875{ if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:867
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

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

877{ double d = 0; is_numeral(d); return d; }

◆ as_int64()

int64_t as_int64 ( ) const
inline

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

879{ int64_t r = 0; is_numeral_i64(r); return r; }
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:868

◆ as_uint64()

uint64_t as_uint64 ( ) const
inline

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

878{ uint64_t r = 0; is_numeral_u64(r); return r; }
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:869

◆ at()

expr at ( expr const &  index) const
inline

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

1474 {
1475 check_context(*this, index);
1476 Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1477 check_error();
1478 return expr(ctx(), r);
1479 }
friend void check_context(object const &a, object const &b)
Definition: z3++.h:467
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()

iterator begin ( )
inline

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

1603{ return iterator(*this, 0); }

◆ bit2bool()

expr bit2bool ( unsigned  i) const
inline

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

1404{ Z3_ast r = Z3_mk_bit2bool(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:190
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()

expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

1214{ assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:893
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.

Referenced by QuantifierRef::children().

◆ bool_value()

Z3_lbool bool_value ( ) const
inline

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

1119 {
1120 return Z3_get_bool_value(ctx(), m_ast);
1121 }
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 1521 of file z3++.h.

1521 {
1522 Z3_ast r = Z3_mk_char_from_bv(ctx(), *this);
1523 check_error();
1524 return expr(ctx(), r);
1525 }
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 1516 of file z3++.h.

1516 {
1517 Z3_ast r = Z3_mk_char_to_bv(ctx(), *this);
1518 check_error();
1519 return expr(ctx(), r);
1520 }
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 1511 of file z3++.h.

1511 {
1512 Z3_ast r = Z3_mk_char_to_int(ctx(), *this);
1513 check_error();
1514 return expr(ctx(), r);
1515 }
Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)
Create an integer (code point) from character.

◆ contains()

expr contains ( expr const &  s) const
inline

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

1468 {
1469 check_context(*this, s);
1470 Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1471 check_error();
1472 return expr(ctx(), r);
1473 }
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.

◆ decl()

func_decl decl ( ) const
inline

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

Precondition
is_app()

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

1179{ Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.

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

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

1131 {
1132 assert(is_numeral());
1133 Z3_ast r = Z3_get_denominator(ctx(), m_ast);
1134 check_error();
1135 return expr(ctx(),r);
1136 }
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.

Referenced by RatNumRef::denominator_as_long(), and RatNumRef::is_int_value().

◆ end()

iterator end ( )
inline

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

1604{ return iterator(*this, is_app() ? num_args() : 0); }
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:885

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

1453 {
1454 check_context(*this, offset); check_context(offset, length);
1455 Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1456 }
expr length() const
Definition: z3++.h:1486
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 1403 of file z3++.h.

1403{ Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
unsigned hi() const
Definition: z3++.h:1406
unsigned lo() const
Definition: z3++.h:1405
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 998 of file z3++.h.

998 {
999 assert(is_numeral() || is_algebraic());
1000 return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
1001 }
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 1055 of file z3++.h.

1055 {
1056 int result = 0;
1057 if (!is_numeral_i(result)) {
1058 assert(ctx().enable_exceptions());
1059 if (!ctx().enable_exceptions()) return 0;
1060 Z3_THROW(exception("numeral does not fit in machine int"));
1061 }
1062 return result;
1063 }
bool is_numeral_i(int &i) const
Definition: z3++.h:870
#define Z3_THROW(x)
Definition: z3++.h:102

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

1091 {
1092 assert(is_numeral());
1093 int64_t result = 0;
1094 if (!is_numeral_i64(result)) {
1095 assert(ctx().enable_exceptions());
1096 if (!ctx().enable_exceptions()) return 0;
1097 Z3_THROW(exception("numeral does not fit in machine int64_t"));
1098 }
1099 return result;
1100 }

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

1074 {
1075 assert(is_numeral());
1076 unsigned result = 0;
1077 if (!is_numeral_u(result)) {
1078 assert(ctx().enable_exceptions());
1079 if (!ctx().enable_exceptions()) return 0;
1080 Z3_THROW(exception("numeral does not fit in machine uint"));
1081 }
1082 return result;
1083 }
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:871

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

1108 {
1109 assert(is_numeral());
1110 uint64_t result = 0;
1111 if (!is_numeral_u64(result)) {
1112 assert(ctx().enable_exceptions());
1113 if (!ctx().enable_exceptions()) return 0;
1114 Z3_THROW(exception("numeral does not fit in machine uint64_t"));
1115 }
1116 return result;
1117 }

◆ get_sort()

sort get_sort ( ) const
inline

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

1150 {
1151 assert(is_string_value());
1152 char const* s = Z3_get_string(ctx(), m_ast);
1153 check_error();
1154 return std::string(s);
1155 }
bool is_string_value() const
Return true if this expression is a string literal. The string can be accessed using get_string() and...
Definition: z3++.h:1143
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s. Characters outside the basic printiable ASCII range are esc...

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

1162 {
1163 assert(is_string_value());
1164 unsigned n = Z3_get_string_length(ctx(), m_ast);
1165 std::u32string s;
1166 s.resize(n);
1167 Z3_get_string_contents(ctx(), m_ast, n, (unsigned*)s.data());
1168 return s;
1169 }
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()

unsigned hi ( ) const
inline

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

1406{ assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1179
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()

unsigned id ( ) const
inline

retrieve unique identifier for expression.

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

1043{ unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
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

Return true if expression is an algebraic number.

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

915{ return Z3_is_algebraic_number(ctx(), m_ast); }
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.

Referenced by expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), and expr::get_decimal_string().

◆ is_and()

bool is_and ( ) const
inline

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

1283{ return is_app() && Z3_OP_AND == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:763
@ Z3_OP_AND
Definition: z3_api.h:968

◆ is_app()

bool is_app ( ) const
inline

Return true if this expression is an application.

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

885{ return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:558
@ Z3_APP_AST
Definition: z3_api.h:141
@ Z3_NUMERAL_AST
Definition: z3_api.h:140

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()

bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

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

822{ return get_sort().is_arith(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:805
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:681

◆ is_array()

bool is_array ( ) const
inline

Return true if this is a Array expression.

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

830{ return get_sort().is_array(); }
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:689

Referenced by expr::operator[]().

◆ is_bool()

bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

810{ return get_sort().is_bool(); }
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:669

Referenced by solver::add(), optimize::add(), and optimize::add_soft().

◆ is_bv()

bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

826{ return get_sort().is_bv(); }
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:685

Referenced by expr::mk_from_ieee_bv().

◆ is_const()

bool is_const ( ) const
inline

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

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

889{ return is_app() && num_args() == 0; }

Referenced by solver::add().

◆ is_datatype()

bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

834{ return get_sort().is_datatype(); }
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:693

◆ is_digit()

expr is_digit ( ) const
inline

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

1526 {
1527 Z3_ast r = Z3_mk_char_is_digit(ctx(), *this);
1528 check_error();
1529 return expr(ctx(), r);
1530 }
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

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

1289{ return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }
@ Z3_OP_DISTINCT
Definition: z3_api.h:966

◆ is_eq()

bool is_eq ( ) const
inline

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

1287{ return is_app() && Z3_OP_EQ == decl().decl_kind(); }
@ Z3_OP_EQ
Definition: z3_api.h:965

◆ is_exists()

bool is_exists ( ) const
inline

Return true if this expression is an existential quantifier.

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

902{ return Z3_is_quantifier_exists(ctx(), m_ast); }
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.

◆ is_false()

bool is_false ( ) const
inline

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

1281{ return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
@ Z3_OP_FALSE
Definition: z3_api.h:964

◆ is_finite_domain()

bool is_finite_domain ( ) const
inline

Return true if this is a Finite-domain expression.

Remarks
Finite-domain is special kind of interpreted sort: is_bool(), is_bv() and is_finite_domain() are mutually exclusive.

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

856{ return get_sort().is_finite_domain(); }
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:709

◆ is_forall()

bool is_forall ( ) const
inline

Return true if this expression is a universal quantifier.

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

898{ return Z3_is_quantifier_forall(ctx(), m_ast); }
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.

◆ is_fpa()

bool is_fpa ( ) const
inline

Return true if this is a FloatingPoint expression. .

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

860{ return get_sort().is_fpa(); }
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:713

Referenced by 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(), z3::operator!=(), and z3::operator==().

◆ is_implies()

bool is_implies ( ) const
inline

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

1286{ return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
@ Z3_OP_IMPLIES
Definition: z3_api.h:973

◆ is_int()

bool is_int ( ) const
inline

Return true if this is an integer expression.

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

814{ return get_sort().is_int(); }
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:673

Referenced by IntNumRef::as_long(), and ArithSortRef::subsort().

◆ is_ite()

bool is_ite ( ) const
inline

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

1288{ return is_app() && Z3_OP_ITE == decl().decl_kind(); }
@ Z3_OP_ITE
Definition: z3_api.h:967

◆ is_lambda()

bool is_lambda ( ) const
inline

Return true if this expression is a lambda expression.

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

906{ return Z3_is_lambda(ctx(), m_ast); }
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.

Referenced by QuantifierRef::__getitem__(), and QuantifierRef::sort().

◆ is_not()

bool is_not ( ) const
inline

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

1282{ return is_app() && Z3_OP_NOT == decl().decl_kind(); }
@ Z3_OP_NOT
Definition: z3_api.h:972

◆ is_numeral() [1/4]

bool is_numeral ( ) const
inline

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.

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

867{ return kind() == Z3_NUMERAL_AST; }

Referenced by expr::as_binary(), expr::as_double(), expr::denominator(), expr::get_decimal_string(), expr::get_numeral_int64(), expr::get_numeral_uint(), expr::get_numeral_uint64(), and expr::numerator().

◆ is_numeral() [2/4]

bool is_numeral ( double &  d) const
inline

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

874{ if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
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 872 of file z3++.h.

872{ if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
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

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

873{ if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }

Referenced by expr::is_numeral().

◆ is_numeral_i()

bool is_numeral_i ( int &  i) const
inline

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

870{ bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
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 868 of file z3++.h.

868{ bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
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 871 of file z3++.h.

871{ bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
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 869 of file z3++.h.

869{ bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
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()

bool is_or ( ) const
inline

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

1284{ return is_app() && Z3_OP_OR == decl().decl_kind(); }
@ Z3_OP_OR
Definition: z3_api.h:969

◆ is_quantifier()

bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

893{ return kind() == Z3_QUANTIFIER_AST; }
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:143

Referenced by expr::body().

◆ is_re()

bool is_re ( ) const
inline

Return true if this is a regular expression.

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

846{ return get_sort().is_re(); }
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:705

◆ is_real()

bool is_real ( ) const
inline

Return true if this is a real expression.

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

818{ return get_sort().is_real(); }
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:677

◆ is_relation()

bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

838{ return get_sort().is_relation(); }
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:697

◆ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

842{ return get_sort().is_seq(); }
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:701

Referenced by expr::operator[]().

◆ is_string_value()

bool is_string_value ( ) const
inline

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

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

1143{ return Z3_is_string(ctx(), m_ast); }
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.

Referenced by SeqRef::as_string(), expr::get_string(), and expr::get_u32string().

◆ is_true()

bool is_true ( ) const
inline

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

1280{ return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
@ Z3_OP_TRUE
Definition: z3_api.h:963

◆ is_var()

bool is_var ( ) const
inline

Return true if this expression is a variable.

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

911{ return kind() == Z3_VAR_AST; }
@ Z3_VAR_AST
Definition: z3_api.h:142

◆ is_well_sorted()

bool is_well_sorted ( ) const
inline

Return true if this expression is well sorted (aka type correct).

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

920{ bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
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()

bool is_xor ( ) const
inline

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

1285{ return is_app() && Z3_OP_XOR == decl().decl_kind(); }
@ Z3_OP_XOR
Definition: z3_api.h:971

◆ itos()

expr itos ( ) const
inline

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

1496 {
1497 Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1498 check_error();
1499 return expr(ctx(), r);
1500 }
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.

◆ length()

expr length ( ) const
inline

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

1486 {
1487 Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1488 check_error();
1489 return expr(ctx(), r);
1490 }
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()

unsigned lo ( ) const
inline

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

1405{ assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }

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

◆ loop() [1/2]

expr loop ( unsigned  lo)
inline

create a looping regular expression.

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

1536 {
1537 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1538 check_error();
1539 return expr(ctx(), r);
1540 }
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

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

1541 {
1542 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1543 check_error();
1544 return expr(ctx(), r);
1545 }

◆ mk_from_ieee_bv()

expr mk_from_ieee_bv ( sort const &  s) const
inline

Convert this IEEE BV into a fpa.

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

985 {
986 assert(is_bv());
987 Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
988 check_error();
989 return expr(ctx(), r);
990 }
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:826
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()

expr mk_is_inf ( ) const
inline

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

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

925 {
926 assert(is_fpa());
927 Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast);
928 check_error();
929 return expr(ctx(), r);
930 }
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:860
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()

expr mk_is_nan ( ) const
inline

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

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

935 {
936 assert(is_fpa());
937 Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast);
938 check_error();
939 return expr(ctx(), r);
940 }
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 945 of file z3++.h.

945 {
946 assert(is_fpa());
947 Z3_ast r = Z3_mk_fpa_is_normal(ctx(), m_ast);
948 check_error();
949 return expr(ctx(), r);
950 }
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 955 of file z3++.h.

955 {
956 assert(is_fpa());
957 Z3_ast r = Z3_mk_fpa_is_subnormal(ctx(), m_ast);
958 check_error();
959 return expr(ctx(), r);
960 }
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 965 of file z3++.h.

965 {
966 assert(is_fpa());
967 Z3_ast r = Z3_mk_fpa_is_zero(ctx(), m_ast);
968 check_error();
969 return expr(ctx(), r);
970 }
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 975 of file z3++.h.

975 {
976 assert(is_fpa());
977 Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast);
978 check_error();
979 return expr(ctx(), r);
980 }
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()

expr nth ( expr const &  index) const
inline

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

1480 {
1481 check_context(*this, index);
1482 Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1483 check_error();
1484 return expr(ctx(), r);
1485 }
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

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

Precondition
is_app()

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

1186{ unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
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...

Referenced by AstRef::__bool__(), ExprRef::arg(), FuncEntry::arg_value(), expr::args(), FuncEntry::as_list(), ExprRef::children(), expr::end(), and expr::is_const().

◆ numerator()

expr numerator ( ) const
inline

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

1123 {
1124 assert(is_numeral());
1125 Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1126 check_error();
1127 return expr(ctx(),r);
1128 }
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

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

1171{ assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }

◆ operator[]() [1/2]

expr operator[] ( expr const &  index) const
inline

index operator defined on arrays and sequences.

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

1550 {
1551 assert(is_array() || is_seq());
1552 if (is_array()) {
1553 return select(*this, index);
1554 }
1555 return nth(index);
1556 }
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:830
expr nth(expr const &index) const
Definition: z3++.h:1480
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:842
expr select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3788

◆ operator[]() [2/2]

expr operator[] ( expr_vector const &  index) const
inline

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

1558 {
1559 return select(*this, index);
1560 }

◆ repeat()

expr repeat ( unsigned  i) const
inline

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

1393{ Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.

◆ replace()

expr replace ( expr const &  src,
expr const &  dst 
) const
inline

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

1457 {
1458 check_context(*this, src); check_context(src, dst);
1459 Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1460 check_error();
1461 return expr(ctx(), r);
1462 }
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 1391 of file z3++.h.

1391{ Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
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 1392 of file z3++.h.

1392{ Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
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()

expr sbvtos ( ) const
inline

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

1506 {
1507 Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this);
1508 check_error();
1509 return expr(ctx(), r);
1510 }
Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s)
Signed bit-vector to string conversion.

◆ simplify() [1/2]

expr simplify ( ) const
inline

Return a simplified version of this expression.

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

1565{ Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.

◆ simplify() [2/2]

expr simplify ( params const &  p) const
inline

Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier.

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

1569{ Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.

◆ stoi()

expr stoi ( ) const
inline

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

1491 {
1492 Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1493 check_error();
1494 return expr(ctx(), r);
1495 }
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.

◆ substitute() [1/3]

expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

4076 {
4077 array<Z3_ast> _dst(dst.size());
4078 for (unsigned i = 0; i < dst.size(); ++i) {
4079 _dst[i] = dst[i];
4080 }
4081 Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
4082 check_error();
4083 return expr(ctx(), r);
4084 }
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]

expr substitute ( expr_vector const &  src,
expr_vector const &  dst 
)
inline

Apply substitution. Replace src expressions by dst.

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

4063 {
4064 assert(src.size() == dst.size());
4065 array<Z3_ast> _src(src.size());
4066 array<Z3_ast> _dst(dst.size());
4067 for (unsigned i = 0; i < src.size(); ++i) {
4068 _src[i] = src[i];
4069 _dst[i] = dst[i];
4070 }
4071 Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
4072 check_error();
4073 return expr(ctx(), r);
4074 }
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]

expr substitute ( func_decl_vector const &  funs,
expr_vector const &  bodies 
)
inline

Apply function substitution by macro definitions.

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

4086 {
4087 array<Z3_ast> _dst(dst.size());
4088 array<Z3_func_decl> _funs(funs.size());
4089 if (dst.size() != funs.size()) {
4090 Z3_THROW(exception("length of argument lists don't align"));
4091 return expr(ctx(), nullptr);
4092 }
4093 for (unsigned i = 0; i < dst.size(); ++i) {
4094 _dst[i] = dst[i];
4095 _funs[i] = funs[i];
4096 }
4097 Z3_ast r = Z3_substitute_funs(ctx(), m_ast, dst.size(), _funs.ptr(), _dst.ptr());
4098 check_error();
4099 return expr(ctx(), r);
4100 }
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 funcions in from with new expressions in to.

◆ ubvtos()

expr ubvtos ( ) const
inline

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

1501 {
1502 Z3_ast r = Z3_mk_ubv_to_str(ctx(), *this);
1503 check_error();
1504 return expr(ctx(), r);
1505 }
Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s)
Unsigned bit-vector to string conversion.

◆ unit()

expr unit ( ) const
inline

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

1463 {
1464 Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1465 check_error();
1466 return expr(ctx(), r);
1467 }
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.

Friends And Related Function Documentation

◆ abs

expr abs ( expr const &  a)
friend

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

1981 {
1982 Z3_ast r;
1983 if (a.is_int()) {
1984 expr zero = a.ctx().int_val(0);
1985 expr ge = a >= zero;
1986 expr na = -a;
1987 r = Z3_mk_ite(a.ctx(), ge, a, na);
1988 }
1989 else if (a.is_real()) {
1990 expr zero = a.ctx().real_val(0);
1991 expr ge = a >= zero;
1992 expr na = -a;
1993 r = Z3_mk_ite(a.ctx(), ge, a, na);
1994 }
1995 else {
1996 r = Z3_mk_fpa_abs(a.ctx(), a);
1997 }
1998 a.check_error();
1999 return expr(a.ctx(), r);
2000 }
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

expr atleast ( expr_vector const &  es,
unsigned  bound 
)
friend

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

2416 {
2417 assert(es.size() > 0);
2418 context& ctx = es[0u].ctx();
2419 array<Z3_ast> _es(es);
2420 Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2421 ctx.check_error();
2422 return expr(ctx, r);
2423 }
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ atmost

expr atmost ( expr_vector const &  es,
unsigned  bound 
)
friend

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

2408 {
2409 assert(es.size() > 0);
2410 context& ctx = es[0u].ctx();
2411 array<Z3_ast> _es(es);
2412 Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2413 ctx.check_error();
2414 return expr(ctx, r);
2415 }
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 2219 of file z3++.h.

2219{ Z3_ast r = Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error(); return expr(a.ctx(), r); }
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 2225 of file z3++.h.

2225 {
2226 check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
2227 }
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

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

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

2228 {
2229 check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2230 }
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 2243 of file z3++.h.

2243 {
2244 check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
2245 }
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

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

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

2246 {
2247 check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2248 }
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 2240 of file z3++.h.

2240 {
2241 Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2242 }
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

expr bvredand ( expr const &  a)
friend

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

1975 {
1976 assert(a.is_bv());
1977 Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
1978 a.check_error();
1979 return expr(a.ctx(), r);
1980 }
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

expr bvredor ( expr const &  a)
friend

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

1969 {
1970 assert(a.is_bv());
1971 Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1972 a.check_error();
1973 return expr(a.ctx(), r);
1974 }
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

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

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

2237 {
2238 check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2239 }
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

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

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

2231 {
2232 check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2233 }
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 2234 of file z3++.h.

2234 {
2235 check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_underflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
2236 }
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]

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

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

2442 {
2443 check_context(a, b);
2444 Z3_ast r;
2445 if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2446 Z3_ast _args[2] = { a, b };
2447 r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2448 }
2449 else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2450 Z3_ast _args[2] = { a, b };
2451 r = Z3_mk_re_concat(a.ctx(), 2, _args);
2452 }
2453 else {
2454 r = Z3_mk_concat(a.ctx(), a, b);
2455 }
2456 a.ctx().check_error();
2457 return expr(a.ctx(), r);
2458 }
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]

expr concat ( expr_vector const &  args)
friend

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

2460 {
2461 Z3_ast r;
2462 assert(args.size() > 0);
2463 if (args.size() == 1) {
2464 return args[0u];
2465 }
2466 context& ctx = args[0u].ctx();
2467 array<Z3_ast> _args(args);
2468 if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
2469 r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2470 }
2471 else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
2472 r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2473 }
2474 else {
2475 r = _args[args.size()-1];
2476 for (unsigned i = args.size()-1; i > 0; ) {
2477 --i;
2478 r = Z3_mk_concat(ctx, _args[i], r);
2479 ctx.check_error();
2480 }
2481 }
2482 ctx.check_error();
2483 return expr(ctx, r);
2484 }
unsigned size() const
Definition: z3++.h:587
expr_vector args() const
Return a vector of all the arguments of this application. This method assumes the expression is an ap...
Definition: z3++.h:1201

◆ distinct

expr distinct ( expr_vector const &  args)
friend

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

2433 {
2434 assert(args.size() > 0);
2435 context& ctx = args[0u].ctx();
2436 array<Z3_ast> _args(args);
2437 Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2438 ctx.check_error();
2439 return expr(ctx, r);
2440 }
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

expr fma ( expr const &  a,
expr const &  b,
expr const &  c,
expr const &  rm 
)
friend

FloatingPoint fused multiply-add.

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

2017 {
2018 check_context(a, b); check_context(a, c); check_context(a, rm);
2019 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2020 Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
2021 a.check_error();
2022 return expr(a.ctx(), r);
2023 }
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

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

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

2008 {
2009 check_context(a, b);
2010 assert(a.is_fpa());
2011 Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
2012 a.check_error();
2013 return expr(a.ctx(), r);
2014 }
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.

◆ fpa_fp

expr fpa_fp ( expr const &  sgn,
expr const &  exp,
expr const &  sig 
)
friend

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

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

2025 {
2026 check_context(sgn, exp); check_context(exp, sig);
2027 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2028 Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
2029 sgn.check_error();
2030 return expr(sgn.ctx(), r);
2031 }
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

expr fpa_to_fpa ( expr const &  t,
sort  s 
)
friend

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

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

2061 {
2062 assert(t.is_fpa());
2063 Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2064 t.check_error();
2065 return expr(t.ctx(), r);
2066 }
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 2033 of file z3++.h.

2033 {
2034 assert(t.is_fpa());
2035 Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2036 t.check_error();
2037 return expr(t.ctx(), r);
2038 }
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 2040 of file z3++.h.

2040 {
2041 assert(t.is_fpa());
2042 Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2043 t.check_error();
2044 return expr(t.ctx(), r);
2045 }
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]

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

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

1620{ return implies(b.ctx().bool_val(a), b); }
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:1615

◆ implies [2/3]

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

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

1619{ return implies(a, a.ctx().bool_val(b)); }

◆ implies [3/3]

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

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

1615 {
1616 assert(a.is_bool() && b.is_bool());
1618 }
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)
Definition: z3++.h:1608

◆ int2bv

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

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

2220{ Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }
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

expr is_int ( expr const &  e)
friend

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

1663{ _Z3_MK_UN_(e, Z3_mk_is_int); }
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1655

Referenced by IntNumRef::as_long(), and ArithSortRef::subsort().

◆ ite

expr ite ( expr const &  c,
expr const &  t,
expr const &  e 
)
friend

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

Precondition
c.is_bool()

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

2080 {
2081 check_context(c, t); check_context(c, e);
2082 assert(c.is_bool());
2083 Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
2084 c.check_error();
2085 return expr(c.ctx(), r);
2086 }

◆ max

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

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

1953 {
1954 check_context(a, b);
1955 Z3_ast r;
1956 if (a.is_arith()) {
1957 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1958 }
1959 else if (a.is_bv()) {
1960 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1961 }
1962 else {
1963 assert(a.is_fpa());
1964 r = Z3_mk_fpa_max(a.ctx(), a, b);
1965 }
1966 a.check_error();
1967 return expr(a.ctx(), r);
1968 }
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

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

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

1937 {
1938 check_context(a, b);
1939 Z3_ast r;
1940 if (a.is_arith()) {
1941 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1942 }
1943 else if (a.is_bv()) {
1944 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1945 }
1946 else {
1947 assert(a.is_fpa());
1948 r = Z3_mk_fpa_min(a.ctx(), a, b);
1949 }
1950 a.check_error();
1951 return expr(a.ctx(), r);
1952 }
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.

◆ mk_and

expr mk_and ( expr_vector const &  args)
friend

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

2492 {
2493 array<Z3_ast> _args(args);
2494 Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2495 args.check_error();
2496 return expr(args.ctx(), r);
2497 }
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

expr mk_or ( expr_vector const &  args)
friend

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

2486 {
2487 array<Z3_ast> _args(args);
2488 Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2489 args.check_error();
2490 return expr(args.ctx(), r);
2491 }
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

expr mk_xor ( expr_vector const &  args)
friend

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

2498 {
2499 if (args.empty())
2500 return args.ctx().bool_val(false);
2501 expr r = args[0u];
2502 for (unsigned i = 1; i < args.size(); ++i)
2503 r = r ^ args[i];
2504 return r;
2505 }
bool empty() const
Definition: z3++.h:593
expr bool_val(bool b)
Definition: z3++.h:3625

◆ mod [1/3]

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

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

1627 {
1628 if (a.is_bv()) {
1629 _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1630 }
1631 else {
1632 _Z3_MK_BIN_(a, b, Z3_mk_mod);
1633 }
1634 }
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]

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

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

1635{ return mod(a, a.ctx().num_val(b, a.get_sort())); }
friend expr mod(expr const &a, expr const &b)
Definition: z3++.h:1627

◆ mod [3/3]

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

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

1636{ return mod(b.ctx().num_val(a, b.get_sort()), b); }

◆ nand

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

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

1934{ if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.

◆ nor

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

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

1935{ if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.

◆ operator!

expr operator! ( expr const &  a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

1661{ assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).

◆ operator!= [1/3]

expr operator!= ( expr const &  a,
expr const &  b 
)
friend

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

1703 {
1704 check_context(a, b);
1705 Z3_ast args[2] = { a, b };
1706 Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1707 a.check_error();
1708 return expr(a.ctx(), r);
1709 }

◆ operator!= [2/3]

expr operator!= ( expr const &  a,
int  b 
)
friend

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

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

1711{ assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) != b; }

◆ operator& [1/3]

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

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

1922{ if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
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 1923 of file z3++.h.

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

◆ operator& [3/3]

expr operator& ( int  a,
expr const &  b 
)
friend

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

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

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

1676{ return a && a.ctx().bool_val(b); }

◆ operator&& [3/3]

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

Return an expression representing a and b.

Precondition
a.is_bool()
b.is_bool()

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

1667 {
1668 check_context(a, b);
1669 assert(a.is_bool() && b.is_bool());
1670 Z3_ast args[2] = { a, b };
1671 Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1672 a.check_error();
1673 return expr(a.ctx(), r);
1674 }

◆ operator* [1/3]

expr operator* ( expr const &  a,
expr const &  b 
)
friend

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

1745 {
1746 check_context(a, b);
1747 Z3_ast r = 0;
1748 if (a.is_arith() && b.is_arith()) {
1749 Z3_ast args[2] = { a, b };
1750 r = Z3_mk_mul(a.ctx(), 2, args);
1751 }
1752 else if (a.is_bv() && b.is_bv()) {
1753 r = Z3_mk_bvmul(a.ctx(), a, b);
1754 }
1755 else if (a.is_fpa() && b.is_fpa()) {
1756 r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1757 }
1758 else {
1759 // operator is not supported by given arguments.
1760 assert(false);
1761 }
1762 a.check_error();
1763 return expr(a.ctx(), r);
1764 }
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 1765 of file z3++.h.

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

◆ operator* [3/3]

expr operator* ( int  a,
expr const &  b 
)
friend

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

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

◆ operator+ [1/3]

expr operator+ ( expr const &  a,
expr const &  b 
)
friend

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

1715 {
1716 check_context(a, b);
1717 Z3_ast r = 0;
1718 if (a.is_arith() && b.is_arith()) {
1719 Z3_ast args[2] = { a, b };
1720 r = Z3_mk_add(a.ctx(), 2, args);
1721 }
1722 else if (a.is_bv() && b.is_bv()) {
1723 r = Z3_mk_bvadd(a.ctx(), a, b);
1724 }
1725 else if (a.is_seq() && b.is_seq()) {
1726 return concat(a, b);
1727 }
1728 else if (a.is_re() && b.is_re()) {
1729 Z3_ast _args[2] = { a, b };
1730 r = Z3_mk_re_union(a.ctx(), 2, _args);
1731 }
1732 else if (a.is_fpa() && b.is_fpa()) {
1733 r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1734 }
1735 else {
1736 // operator is not supported by given arguments.
1737 assert(false);
1738 }
1739 a.check_error();
1740 return expr(a.ctx(), r);
1741 }
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:2442
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 1742 of file z3++.h.

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

◆ operator+ [3/3]

expr operator+ ( int  a,
expr const &  b 
)
friend

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

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

◆ operator- [1/4]

expr operator- ( expr const &  a)
friend

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

1811 {
1812 Z3_ast r = 0;
1813 if (a.is_arith()) {
1814 r = Z3_mk_unary_minus(a.ctx(), a);
1815 }
1816 else if (a.is_bv()) {
1817 r = Z3_mk_bvneg(a.ctx(), a);
1818 }
1819 else if (a.is_fpa()) {
1820 r = Z3_mk_fpa_neg(a.ctx(), a);
1821 }
1822 else {
1823 // operator is not supported by given arguments.
1824 assert(false);
1825 }
1826 a.check_error();
1827 return expr(a.ctx(), r);
1828 }
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]

expr operator- ( expr const &  a,
expr const &  b 
)
friend

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

1830 {
1831 check_context(a, b);
1832 Z3_ast r = 0;
1833 if (a.is_arith() && b.is_arith()) {
1834 Z3_ast args[2] = { a, b };
1835 r = Z3_mk_sub(a.ctx(), 2, args);
1836 }
1837 else if (a.is_bv() && b.is_bv()) {
1838 r = Z3_mk_bvsub(a.ctx(), a, b);
1839 }
1840 else if (a.is_fpa() && b.is_fpa()) {
1841 r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1842 }
1843 else {
1844 // operator is not supported by given arguments.
1845 assert(false);
1846 }
1847 a.check_error();
1848 return expr(a.ctx(), r);
1849 }
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 1850 of file z3++.h.

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

◆ operator- [4/4]

expr operator- ( int  a,
expr const &  b 
)
friend

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

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

◆ operator/ [1/3]

expr operator/ ( expr const &  a,
expr const &  b 
)
friend

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

1789 {
1790 check_context(a, b);
1791 Z3_ast r = 0;
1792 if (a.is_arith() && b.is_arith()) {
1793 r = Z3_mk_div(a.ctx(), a, b);
1794 }
1795 else if (a.is_bv() && b.is_bv()) {
1796 r = Z3_mk_bvsdiv(a.ctx(), a, b);
1797 }
1798 else if (a.is_fpa() && b.is_fpa()) {
1799 r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1800 }
1801 else {
1802 // operator is not supported by given arguments.
1803 assert(false);
1804 }
1805 a.check_error();
1806 return expr(a.ctx(), r);
1807 }
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 1808 of file z3++.h.

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

◆ operator/ [3/3]

expr operator/ ( int  a,
expr const &  b 
)
friend

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

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

◆ operator< [1/3]

expr operator< ( expr const &  a,
expr const &  b 
)
friend

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

1878 {
1879 check_context(a, b);
1880 Z3_ast r = 0;
1881 if (a.is_arith() && b.is_arith()) {
1882 r = Z3_mk_lt(a.ctx(), a, b);
1883 }
1884 else if (a.is_bv() && b.is_bv()) {
1885 r = Z3_mk_bvslt(a.ctx(), a, b);
1886 }
1887 else if (a.is_fpa() && b.is_fpa()) {
1888 r = Z3_mk_fpa_lt(a.ctx(), a, b);
1889 }
1890 else {
1891 // operator is not supported by given arguments.
1892 assert(false);
1893 }
1894 a.check_error();
1895 return expr(a.ctx(), r);
1896 }
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 1897 of file z3++.h.

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

◆ operator< [3/3]

expr operator< ( int  a,
expr const &  b 
)
friend

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

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

◆ operator<= [1/3]

expr operator<= ( expr const &  a,
expr const &  b 
)
friend

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

1853 {
1854 check_context(a, b);
1855 Z3_ast r = 0;
1856 if (a.is_arith() && b.is_arith()) {
1857 r = Z3_mk_le(a.ctx(), a, b);
1858 }
1859 else if (a.is_bv() && b.is_bv()) {
1860 r = Z3_mk_bvsle(a.ctx(), a, b);
1861 }
1862 else if (a.is_fpa() && b.is_fpa()) {
1863 r = Z3_mk_fpa_leq(a.ctx(), a, b);
1864 }
1865 else {
1866 // operator is not supported by given arguments.
1867 assert(false);
1868 }
1869 a.check_error();
1870 return expr(a.ctx(), r);
1871 }
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 1872 of file z3++.h.

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

◆ operator<= [3/3]

expr operator<= ( int  a,
expr const &  b 
)
friend

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

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

◆ operator== [1/3]

expr operator== ( expr const &  a,
expr const &  b 
)
friend

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

1692 {
1693 check_context(a, b);
1694 Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1695 a.check_error();
1696 return expr(a.ctx(), r);
1697 }
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 1698 of file z3++.h.

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

1699{ assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) == b; }

◆ operator> [1/3]

expr operator> ( expr const &  a,
expr const &  b 
)
friend

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

1900 {
1901 check_context(a, b);
1902 Z3_ast r = 0;
1903 if (a.is_arith() && b.is_arith()) {
1904 r = Z3_mk_gt(a.ctx(), a, b);
1905 }
1906 else if (a.is_bv() && b.is_bv()) {
1907 r = Z3_mk_bvsgt(a.ctx(), a, b);
1908 }
1909 else if (a.is_fpa() && b.is_fpa()) {
1910 r = Z3_mk_fpa_gt(a.ctx(), a, b);
1911 }
1912 else {
1913 // operator is not supported by given arguments.
1914 assert(false);
1915 }
1916 a.check_error();
1917 return expr(a.ctx(), r);
1918 }
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 1919 of file z3++.h.

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

◆ operator> [3/3]

expr operator> ( int  a,
expr const &  b 
)
friend

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

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

◆ operator>= [1/3]

expr operator>= ( expr const &  a,
expr const &  b 
)
friend

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

1769 {
1770 check_context(a, b);
1771 Z3_ast r = 0;
1772 if (a.is_arith() && b.is_arith()) {
1773 r = Z3_mk_ge(a.ctx(), a, b);
1774 }
1775 else if (a.is_bv() && b.is_bv()) {
1776 r = Z3_mk_bvsge(a.ctx(), a, b);
1777 }
1778 else if (a.is_fpa() && b.is_fpa()) {
1779 r = Z3_mk_fpa_geq(a.ctx(), a, b);
1780 }
1781 else {
1782 // operator is not supported by given arguments.
1783 assert(false);
1784 }
1785 a.check_error();
1786 return expr(a.ctx(), r);
1787 }
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 1875 of file z3++.h.

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

◆ operator>= [3/3]

expr operator>= ( int  a,
expr const &  b 
)
friend

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

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

◆ operator^ [1/3]

expr operator^ ( expr const &  a,
expr const &  b 
)
friend

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

1926{ check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
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 1927 of file z3++.h.

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

◆ operator^ [3/3]

expr operator^ ( int  a,
expr const &  b 
)
friend

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

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

◆ operator| [1/3]

expr operator| ( expr const &  a,
expr const &  b 
)
friend

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

1930{ if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
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 1931 of file z3++.h.

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

◆ operator| [3/3]

expr operator| ( int  a,
expr const &  b 
)
friend

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

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

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

1688{ return a || a.ctx().bool_val(b); }

◆ operator|| [3/3]

expr operator|| ( expr const &  a,
expr const &  b 
)
friend

Return an expression representing a or b.

Precondition
a.is_bool()
b.is_bool()

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

1679 {
1680 check_context(a, b);
1681 assert(a.is_bool() && b.is_bool());
1682 Z3_ast args[2] = { a, b };
1683 Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1684 a.check_error();
1685 return expr(a.ctx(), r);
1686 }

◆ operator~

expr operator~ ( expr const &  a)
friend

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

2015{ Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.

◆ pbeq

expr pbeq ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
friend

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

2400 {
2401 assert(es.size() > 0);
2402 context& ctx = es[0u].ctx();
2403 array<Z3_ast> _es(es);
2404 Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2405 ctx.check_error();
2406 return expr(ctx, r);
2407 }
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

expr pbge ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
friend

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

2392 {
2393 assert(es.size() > 0);
2394 context& ctx = es[0u].ctx();
2395 array<Z3_ast> _es(es);
2396 Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2397 ctx.check_error();
2398 return expr(ctx, r);
2399 }
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

expr pble ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
friend

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

2384 {
2385 assert(es.size() > 0);
2386 context& ctx = es[0u].ctx();
2387 array<Z3_ast> _es(es);
2388 Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2389 ctx.check_error();
2390 return expr(ctx, r);
2391 }
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]

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

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

1623{ _Z3_MK_BIN_(a, b, Z3_mk_power); }
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]

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

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

1624{ return pw(a, a.ctx().num_val(b, a.get_sort())); }
friend expr pw(expr const &a, expr const &b)
Definition: z3++.h:1623

◆ pw [3/3]

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

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

1625{ return pw(b.ctx().num_val(a, b.get_sort()), b); }

◆ range

expr range ( expr const &  lo,
expr const &  hi 
)
friend

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

3970 {
3972 Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3973 lo.check_error();
3974 return expr(lo.ctx(), r);
3975 }
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]

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

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

1643 {
1644 if (a.is_fpa() && b.is_fpa()) {
1646 } else {
1647 _Z3_MK_BIN_(a, b, Z3_mk_rem);
1648 }
1649 }
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]

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

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

1650{ return rem(a, a.ctx().num_val(b, a.get_sort())); }
friend expr rem(expr const &a, expr const &b)
Definition: z3++.h:1643

◆ rem [3/3]

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

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

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

2068 {
2069 assert(t.is_fpa());
2070 Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
2071 t.check_error();
2072 return expr(t.ctx(), r);
2073 }
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

expr sbv_to_fpa ( expr const &  t,
sort  s 
)
friend

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

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

2047 {
2048 assert(t.is_bv());
2049 Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2050 t.check_error();
2051 return expr(t.ctx(), r);
2052 }
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

expr sqrt ( expr const &  a,
expr const &  rm 
)
friend

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

2001 {
2002 check_context(a, rm);
2003 assert(a.is_fpa());
2004 Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
2005 a.check_error();
2006 return expr(a.ctx(), r);
2007 }
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.

◆ sum

expr sum ( expr_vector const &  args)
friend

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

2424 {
2425 assert(args.size() > 0);
2426 context& ctx = args[0u].ctx();
2427 array<Z3_ast> _args(args);
2428 Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2429 ctx.check_error();
2430 return expr(ctx, r);
2431 }

◆ ubv_to_fpa

expr ubv_to_fpa ( expr const &  t,
sort  s 
)
friend

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

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

2054 {
2055 assert(t.is_bv());
2056 Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2057 t.check_error();
2058 return expr(t.ctx(), r);
2059 }
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

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

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

1936{ if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.