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

+ 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. More...
 
bool is_bool () const
 Return true if this is a Boolean expression. More...
 
bool is_int () const
 Return true if this is an integer expression. More...
 
bool is_real () const
 Return true if this is a real expression. More...
 
bool is_arith () const
 Return true if this is an integer or real expression. More...
 
bool is_bv () const
 Return true if this is a Bit-vector expression. More...
 
bool is_array () const
 Return true if this is a Array expression. More...
 
bool is_datatype () const
 Return true if this is a Datatype expression. More...
 
bool is_relation () const
 Return true if this is a Relation expression. More...
 
bool is_seq () const
 Return true if this is a sequence expression. More...
 
bool is_re () const
 Return true if this is a regular expression. More...
 
bool is_finite_domain () const
 Return true if this is a Finite-domain expression. More...
 
bool is_fpa () const
 Return true if this is a FloatingPoint expression. . More...
 
bool is_numeral () const
 Return true if this expression is a numeral. Specialized functions also return representations for the numerals as small integers, 64 bit integers or rational or decimal strings. More...
 
bool is_numeral_i64 (int64_t &i) const
 
bool is_numeral_u64 (uint64_t &i) const
 
bool is_numeral_i (int &i) const
 
bool is_numeral_u (unsigned &i) const
 
bool is_numeral (std::string &s) const
 
bool is_numeral (std::string &s, unsigned precision) const
 
bool is_numeral (double &d) const
 
bool as_binary (std::string &s) const
 
double as_double () const
 
uint64_t as_uint64 () const
 
int64_t as_int64 () const
 
bool is_app () const
 Return true if this expression is an application. More...
 
bool is_const () const
 Return true if this expression is a constant (i.e., an application with 0 arguments). More...
 
bool is_quantifier () const
 Return true if this expression is a quantifier. More...
 
bool is_forall () const
 Return true if this expression is a universal quantifier. More...
 
bool is_exists () const
 Return true if this expression is an existential quantifier. More...
 
bool is_lambda () const
 Return true if this expression is a lambda expression. More...
 
bool is_var () const
 Return true if this expression is a variable. More...
 
bool is_algebraic () const
 Return true if expression is an algebraic number. More...
 
bool is_well_sorted () const
 Return true if this expression is well sorted (aka type correct). More...
 
expr mk_is_inf () const
 Return Boolean expression to test for whether an FP expression is inf. More...
 
expr mk_is_nan () const
 Return Boolean expression to test for whether an FP expression is a NaN. More...
 
expr mk_is_normal () const
 Return Boolean expression to test for whether an FP expression is a normal. More...
 
expr mk_is_subnormal () const
 Return Boolean expression to test for whether an FP expression is a subnormal. More...
 
expr mk_is_zero () const
 Return Boolean expression to test for whether an FP expression is a zero. More...
 
expr mk_to_ieee_bv () const
 Convert this fpa into an IEEE BV. More...
 
expr mk_from_ieee_bv (sort const &s) const
 Convert this IEEE BV into a fpa. More...
 
std::string get_decimal_string (int precision) const
 Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic. More...
 
expr algebraic_lower (unsigned precision) const
 
expr algebraic_upper (unsigned precision) const
 
expr_vector algebraic_poly () const
 Return coefficients for p of an algebraic number (root-obj p i) More...
 
unsigned algebraic_i () const
 Return i of an algebraic number (root-obj p i) More...
 
unsigned id () const
 retrieve unique identifier for expression. More...
 
int get_numeral_int () const
 Return int value of numeral, throw if result cannot fit in machine int. More...
 
unsigned get_numeral_uint () const
 Return uint value of numeral, throw if result cannot fit in machine uint. More...
 
int64_t get_numeral_int64 () const
 Return int64_t value of numeral, throw if result cannot fit in int64_t. More...
 
uint64_t get_numeral_uint64 () const
 Return uint64_t value of numeral, throw if result cannot fit in uint64_t. More...
 
Z3_lbool bool_value () const
 
expr numerator () const
 
expr denominator () const
 
bool is_string_value () const
 Return true if this expression is a string literal. The string can be accessed using get_string() and get_escaped_string() More...
 
std::string get_string () const
 for a string value expression return an escaped string value. More...
 
std::u32string get_u32string () const
 for a string value expression return an unespaced string value. More...
 
 operator Z3_app () const
 
func_decl decl () const
 Return the declaration associated with this application. This method assumes the expression is an application. More...
 
unsigned num_args () const
 Return the number of arguments in this application. This method assumes the expression is an application. More...
 
expr arg (unsigned i) const
 Return the i-th argument of this application. This method assumes the expression is an application. More...
 
expr_vector args () const
 Return a vector of all the arguments of this application. This method assumes the expression is an application. More...
 
expr body () const
 Return the 'body' of this quantifier. More...
 
bool is_true () const
 
bool is_false () const
 
bool is_not () const
 
bool is_and () const
 
bool is_or () const
 
bool is_xor () const
 
bool is_implies () const
 
bool is_eq () const
 
bool is_ite () const
 
bool is_distinct () const
 
expr rotate_left (unsigned i) const
 
expr rotate_right (unsigned i) const
 
expr repeat (unsigned i) const
 
expr extract (unsigned hi, unsigned lo) const
 
expr bit2bool (unsigned i) const
 
unsigned lo () const
 
unsigned hi () const
 
expr extract (expr const &offset, expr const &length) const
 sequence and regular expression operations. More...
 
expr replace (expr const &src, expr const &dst) const
 
expr unit () const
 
expr contains (expr const &s) const
 
expr at (expr const &index) const
 
expr nth (expr const &index) const
 
expr length () const
 
expr stoi () const
 
expr itos () const
 
expr ubvtos () const
 
expr sbvtos () const
 
expr char_to_int () const
 
expr char_to_bv () const
 
expr char_from_bv () const
 
expr is_digit () const
 
expr loop (unsigned lo)
 create a looping regular expression. More...
 
expr loop (unsigned lo, unsigned hi)
 
expr operator[] (expr const &index) const
 
expr operator[] (expr_vector const &index) const
 
expr simplify () const
 Return a simplified version of this expression. More...
 
expr simplify (params const &p) const
 Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier. More...
 
expr substitute (expr_vector const &src, expr_vector const &dst)
 Apply substitution. Replace src expressions by dst. More...
 
expr substitute (expr_vector const &dst)
 Apply substitution. Replace bound variables by expressions. More...
 
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). More...
 
expr operator&& (expr const &a, expr const &b)
 Return an expression representing a and b. More...
 
expr operator&& (expr const &a, bool b)
 Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant. More...
 
expr operator&& (bool a, expr const &b)
 Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant. More...
 
expr operator|| (expr const &a, expr const &b)
 Return an expression representing a or b. More...
 
expr operator|| (expr const &a, bool b)
 Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant. More...
 
expr operator|| (bool a, expr const &b)
 Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant. More...
 
expr implies (expr const &a, expr const &b)
 
expr implies (expr const &a, bool b)
 
expr implies (bool a, expr const &b)
 
expr mk_or (expr_vector const &args)
 
expr mk_xor (expr_vector const &args)
 
expr mk_and (expr_vector const &args)
 
expr ite (expr const &c, expr const &t, expr const &e)
 Create the if-then-else expression ite(c, t, e) More...
 
expr distinct (expr_vector const &args)
 
expr concat (expr const &a, expr const &b)
 
expr concat (expr_vector const &args)
 
expr operator== (expr const &a, expr const &b)
 
expr operator== (expr const &a, int b)
 
expr operator== (int a, expr const &b)
 
expr operator!= (expr const &a, expr const &b)
 
expr operator!= (expr const &a, int b)
 
expr operator!= (int a, expr const &b)
 
expr operator+ (expr const &a, expr const &b)
 
expr operator+ (expr const &a, int b)
 
expr operator+ (int a, expr const &b)
 
expr sum (expr_vector const &args)
 
expr operator* (expr const &a, expr const &b)
 
expr operator* (expr const &a, int b)
 
expr operator* (int a, expr const &b)
 
expr pw (expr const &a, expr const &b)
 
expr pw (expr const &a, int b)
 
expr pw (int a, expr const &b)
 
expr mod (expr const &a, expr const &b)
 
expr mod (expr const &a, int b)
 
expr mod (int a, expr const &b)
 
expr rem (expr const &a, expr const &b)
 
expr rem (expr const &a, int b)
 
expr rem (int a, expr const &b)
 
expr is_int (expr const &e)
 
expr operator/ (expr const &a, expr const &b)
 
expr operator/ (expr const &a, int b)
 
expr operator/ (int a, expr const &b)
 
expr operator- (expr const &a)
 
expr operator- (expr const &a, expr const &b)
 
expr operator- (expr const &a, int b)
 
expr operator- (int a, expr const &b)
 
expr operator<= (expr const &a, expr const &b)
 
expr operator<= (expr const &a, int b)
 
expr operator<= (int a, expr const &b)
 
expr operator>= (expr const &a, expr const &b)
 
expr operator>= (expr const &a, int b)
 
expr operator>= (int a, expr const &b)
 
expr operator< (expr const &a, expr const &b)
 
expr operator< (expr const &a, int b)
 
expr operator< (int a, expr const &b)
 
expr operator> (expr const &a, expr const &b)
 
expr operator> (expr const &a, int b)
 
expr operator> (int a, expr const &b)
 
expr pble (expr_vector const &es, int const *coeffs, int bound)
 
expr pbge (expr_vector const &es, int const *coeffs, int bound)
 
expr pbeq (expr_vector const &es, int const *coeffs, int bound)
 
expr atmost (expr_vector const &es, unsigned bound)
 
expr atleast (expr_vector const &es, unsigned bound)
 
expr operator& (expr const &a, expr const &b)
 
expr operator& (expr const &a, int b)
 
expr operator& (int a, expr const &b)
 
expr operator^ (expr const &a, expr const &b)
 
expr operator^ (expr const &a, int b)
 
expr operator^ (int a, expr const &b)
 
expr operator| (expr const &a, expr const &b)
 
expr operator| (expr const &a, int b)
 
expr operator| (int a, expr const &b)
 
expr nand (expr const &a, expr const &b)
 
expr nor (expr const &a, expr const &b)
 
expr xnor (expr const &a, expr const &b)
 
expr min (expr const &a, expr const &b)
 
expr max (expr const &a, expr const &b)
 
expr bv2int (expr const &a, bool is_signed)
 bit-vector and integer conversions. More...
 
expr int2bv (unsigned n, expr const &a)
 
expr bvadd_no_overflow (expr const &a, expr const &b, bool is_signed)
 bit-vector overflow/underflow checks More...
 
expr bvadd_no_underflow (expr const &a, expr const &b)
 
expr bvsub_no_overflow (expr const &a, expr const &b)
 
expr bvsub_no_underflow (expr const &a, expr const &b, bool is_signed)
 
expr bvsdiv_no_overflow (expr const &a, expr const &b)
 
expr bvneg_no_overflow (expr const &a)
 
expr bvmul_no_overflow (expr const &a, expr const &b, bool is_signed)
 
expr bvmul_no_underflow (expr const &a, expr const &b)
 
expr bvredor (expr const &a)
 
expr bvredand (expr const &a)
 
expr abs (expr const &a)
 
expr sqrt (expr const &a, expr const &rm)
 
expr fp_eq (expr const &a, expr const &b)
 
expr operator~ (expr const &a)
 
expr fma (expr const &a, expr const &b, expr const &c, expr const &rm)
 FloatingPoint fused multiply-add. More...
 
expr fpa_fp (expr const &sgn, expr const &exp, expr const &sig)
 Create an expression of FloatingPoint sort from three bit-vector expressions. More...
 
expr fpa_to_sbv (expr const &t, unsigned sz)
 Conversion of a floating-point term into a signed bit-vector. More...
 
expr fpa_to_ubv (expr const &t, unsigned sz)
 Conversion of a floating-point term into an unsigned bit-vector. More...
 
expr sbv_to_fpa (expr const &t, sort s)
 Conversion of a signed bit-vector term into a floating-point. More...
 
expr ubv_to_fpa (expr const &t, sort s)
 Conversion of an unsigned bit-vector term into a floating-point. More...
 
expr fpa_to_fpa (expr const &t, sort s)
 Conversion of a floating-point term into another floating-point. More...
 
expr round_fpa_to_closest_integer (expr const &t)
 Round a floating-point term into its closest integer. More...
 
expr range (expr const &lo, expr const &hi)
 

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

Constructor & Destructor Documentation

◆ expr() [1/2]

expr ( context c)
inline

◆ expr() [2/2]

expr ( context c,
Z3_ast  n 
)
inline

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

788 :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 1021 of file z3++.h.

1021  {
1022  assert(is_algebraic());
1023  unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
1024  check_error();
1025  return i;
1026  }

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

994  {
995  assert(is_algebraic());
996  Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
997  check_error();
998  return expr(ctx(), r);
999  }

◆ algebraic_poly()

expr_vector algebraic_poly ( ) const
inline

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

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

1011  {
1012  assert(is_algebraic());
1014  check_error();
1015  return expr_vector(ctx(), r);
1016  }

◆ algebraic_upper()

expr algebraic_upper ( unsigned  precision) const
inline

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

1001  {
1002  assert(is_algebraic());
1003  Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
1004  check_error();
1005  return expr(ctx(), r);
1006  }

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

1182 { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }

Referenced by AstRef::__bool__(), expr::args(), 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 1189 of file z3++.h.

1189  {
1190  expr_vector vec(ctx());
1191  unsigned argCnt = num_args();
1192  for (unsigned i = 0; i < argCnt; i++)
1193  vec.push_back(arg(i));
1194  return vec;
1195  }

◆ as_binary()

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

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

863 { if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }

◆ as_double()

double as_double ( ) const
inline

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

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

◆ as_int64()

int64_t as_int64 ( ) const
inline

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

867 { int64_t r = 0; is_numeral_i64(r); return r; }

◆ as_uint64()

uint64_t as_uint64 ( ) const
inline

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

866 { uint64_t r = 0; is_numeral_u64(r); return r; }

◆ at()

expr at ( expr const &  index) const
inline

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

1462  {
1463  check_context(*this, index);
1464  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1465  check_error();
1466  return expr(ctx(), r);
1467  }

◆ begin()

iterator begin ( )
inline

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

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

◆ bit2bool()

expr bit2bool ( unsigned  i) const
inline

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

1392 { Z3_ast r = Z3_mk_bit2bool(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }

◆ body()

expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

1202 { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }

◆ bool_value()

Z3_lbool bool_value ( ) const
inline

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

1107  {
1108  return Z3_get_bool_value(ctx(), m_ast);
1109  }

◆ char_from_bv()

expr char_from_bv ( ) const
inline

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

1509  {
1510  Z3_ast r = Z3_mk_char_from_bv(ctx(), *this);
1511  check_error();
1512  return expr(ctx(), r);
1513  }

◆ char_to_bv()

expr char_to_bv ( ) const
inline

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

1504  {
1505  Z3_ast r = Z3_mk_char_to_bv(ctx(), *this);
1506  check_error();
1507  return expr(ctx(), r);
1508  }

◆ char_to_int()

expr char_to_int ( ) const
inline

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

1499  {
1500  Z3_ast r = Z3_mk_char_to_int(ctx(), *this);
1501  check_error();
1502  return expr(ctx(), r);
1503  }

◆ contains()

expr contains ( expr const &  s) const
inline

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

1456  {
1457  check_context(*this, s);
1458  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1459  check_error();
1460  return expr(ctx(), r);
1461  }

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

1167 { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }

Referenced by expr::hi(), expr::is_and(), expr::is_distinct(), expr::is_eq(), expr::is_false(), expr::is_implies(), expr::is_ite(), expr::is_not(), expr::is_or(), expr::is_true(), expr::is_xor(), and expr::lo().

◆ denominator()

expr denominator ( ) const
inline

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

1119  {
1120  assert(is_numeral());
1122  check_error();
1123  return expr(ctx(),r);
1124  }

◆ end()

iterator end ( )
inline

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

1587 { return iterator(*this, is_app() ? num_args() : 0); }

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

1441  {
1442  check_context(*this, offset); check_context(offset, length);
1443  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1444  }

◆ extract() [2/2]

expr extract ( unsigned  hi,
unsigned  lo 
) const
inline

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

1391 { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }

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

986  {
987  assert(is_numeral() || is_algebraic());
988  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
989  }

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

1043  {
1044  int result = 0;
1045  if (!is_numeral_i(result)) {
1046  assert(ctx().enable_exceptions());
1047  if (!ctx().enable_exceptions()) return 0;
1048  Z3_THROW(exception("numeral does not fit in machine int"));
1049  }
1050  return result;
1051  }

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

1079  {
1080  assert(is_numeral());
1081  int64_t result = 0;
1082  if (!is_numeral_i64(result)) {
1083  assert(ctx().enable_exceptions());
1084  if (!ctx().enable_exceptions()) return 0;
1085  Z3_THROW(exception("numeral does not fit in machine int64_t"));
1086  }
1087  return result;
1088  }

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

1062  {
1063  assert(is_numeral());
1064  unsigned result = 0;
1065  if (!is_numeral_u(result)) {
1066  assert(ctx().enable_exceptions());
1067  if (!ctx().enable_exceptions()) return 0;
1068  Z3_THROW(exception("numeral does not fit in machine uint"));
1069  }
1070  return result;
1071  }

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

1096  {
1097  assert(is_numeral());
1098  uint64_t result = 0;
1099  if (!is_numeral_u64(result)) {
1100  assert(ctx().enable_exceptions());
1101  if (!ctx().enable_exceptions()) return 0;
1102  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
1103  }
1104  return result;
1105  }

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

1138  {
1139  assert(is_string_value());
1140  char const* s = Z3_get_string(ctx(), m_ast);
1141  check_error();
1142  return std::string(s);
1143  }

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

1150  {
1151  assert(is_string_value());
1152  unsigned n = Z3_get_string_length(ctx(), m_ast);
1153  std::u32string s;
1154  s.resize(n);
1155  Z3_get_string_contents(ctx(), m_ast, n, (unsigned*)s.data());
1156  return s;
1157  }

◆ hi()

unsigned hi ( ) const
inline

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

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

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

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for expression.

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

1031 { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }

◆ is_algebraic()

bool is_algebraic ( ) const
inline

Return true if expression is an algebraic number.

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

903 { return Z3_is_algebraic_number(ctx(), m_ast); }

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

1271 { return is_app() && Z3_OP_AND == decl().decl_kind(); }

◆ is_app()

bool is_app ( ) const
inline

◆ is_arith()

bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

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

810 { return get_sort().is_arith(); }

Referenced by z3::max(), z3::min(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), and z3::operator>=().

◆ is_array()

bool is_array ( ) const
inline

Return true if this is a Array expression.

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

818 { return get_sort().is_array(); }

Referenced by expr::operator[]().

◆ is_bool()

bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

798 { return get_sort().is_bool(); }

Referenced by solver::add(), optimize::add(), optimize::add_soft(), z3::implies(), z3::ite(), z3::nand(), z3::nor(), z3::operator!(), z3::operator&(), z3::operator&&(), z3::operator^(), z3::operator|(), z3::operator||(), and z3::xnor().

◆ is_bv()

bool is_bv ( ) const
inline

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

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

822 { return get_sort().is_datatype(); }

◆ is_digit()

expr is_digit ( ) const
inline

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

1514  {
1515  Z3_ast r = Z3_mk_char_is_digit(ctx(), *this);
1516  check_error();
1517  return expr(ctx(), r);
1518  }

◆ is_distinct()

bool is_distinct ( ) const
inline

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

1277 { return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }

◆ is_eq()

bool is_eq ( ) const
inline

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

1275 { return is_app() && Z3_OP_EQ == decl().decl_kind(); }

◆ is_exists()

bool is_exists ( ) const
inline

Return true if this expression is an existential quantifier.

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

890 { return Z3_is_quantifier_exists(ctx(), m_ast); }

◆ is_false()

bool is_false ( ) const
inline

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

1269 { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }

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

844 { return get_sort().is_finite_domain(); }

◆ is_forall()

bool is_forall ( ) const
inline

Return true if this expression is a universal quantifier.

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

886 { return Z3_is_quantifier_forall(ctx(), m_ast); }

◆ is_fpa()

bool is_fpa ( ) const
inline

◆ is_implies()

bool is_implies ( ) const
inline

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

1274 { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }

◆ is_int()

bool is_int ( ) const
inline

Return true if this is an integer expression.

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

802 { return get_sort().is_int(); }

Referenced by z3::abs().

◆ is_ite()

bool is_ite ( ) const
inline

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

1276 { return is_app() && Z3_OP_ITE == decl().decl_kind(); }

◆ is_lambda()

bool is_lambda ( ) const
inline

Return true if this expression is a lambda expression.

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

894 { return Z3_is_lambda(ctx(), m_ast); }

◆ is_not()

bool is_not ( ) const
inline

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

1270 { return is_app() && Z3_OP_NOT == decl().decl_kind(); }

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

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

862 { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }

Referenced by expr::is_numeral().

◆ is_numeral() [3/4]

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

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

860 { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }

Referenced by expr::is_numeral().

◆ is_numeral() [4/4]

bool is_numeral ( std::string &  s,
unsigned  precision 
) const
inline

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

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

858 { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}

Referenced by expr::get_numeral_int().

◆ is_numeral_i64()

bool is_numeral_i64 ( int64_t &  i) const
inline

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

856 { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}

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

◆ is_numeral_u()

bool is_numeral_u ( unsigned &  i) const
inline

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

859 { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}

Referenced by expr::get_numeral_uint().

◆ is_numeral_u64()

bool is_numeral_u64 ( uint64_t &  i) const
inline

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

857 { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}

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

◆ is_or()

bool is_or ( ) const
inline

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

1272 { return is_app() && Z3_OP_OR == decl().decl_kind(); }

◆ is_quantifier()

bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

881 { return kind() == Z3_QUANTIFIER_AST; }

Referenced by expr::body().

◆ is_re()

bool is_re ( ) const
inline

Return true if this is a regular expression.

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

834 { return get_sort().is_re(); }

Referenced by z3::operator+().

◆ is_real()

bool is_real ( ) const
inline

Return true if this is a real expression.

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

806 { return get_sort().is_real(); }

Referenced by z3::abs().

◆ is_relation()

bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

826 { return get_sort().is_relation(); }

◆ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

830 { return get_sort().is_seq(); }

Referenced by z3::operator+(), and 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 1131 of file z3++.h.

1131 { return Z3_is_string(ctx(), m_ast); }

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

◆ is_true()

bool is_true ( ) const
inline

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

1268 { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }

◆ is_var()

bool is_var ( ) const
inline

Return true if this expression is a variable.

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

899 { return kind() == Z3_VAR_AST; }

◆ is_well_sorted()

bool is_well_sorted ( ) const
inline

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

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

908 { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }

◆ is_xor()

bool is_xor ( ) const
inline

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

1273 { return is_app() && Z3_OP_XOR == decl().decl_kind(); }

◆ itos()

expr itos ( ) const
inline

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

1484  {
1485  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1486  check_error();
1487  return expr(ctx(), r);
1488  }

◆ length()

expr length ( ) const
inline

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

1474  {
1475  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1476  check_error();
1477  return expr(ctx(), r);
1478  }

Referenced by expr::extract().

◆ lo()

unsigned lo ( ) const
inline

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

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

1524  {
1525  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1526  check_error();
1527  return expr(ctx(), r);
1528  }

◆ loop() [2/2]

expr loop ( unsigned  lo,
unsigned  hi 
)
inline

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

1529  {
1530  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1531  check_error();
1532  return expr(ctx(), r);
1533  }

◆ mk_from_ieee_bv()

expr mk_from_ieee_bv ( sort const &  s) const
inline

Convert this IEEE BV into a fpa.

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

973  {
974  assert(is_bv());
975  Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
976  check_error();
977  return expr(ctx(), r);
978  }

◆ mk_is_inf()

expr mk_is_inf ( ) const
inline

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

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

913  {
914  assert(is_fpa());
916  check_error();
917  return expr(ctx(), r);
918  }

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

923  {
924  assert(is_fpa());
926  check_error();
927  return expr(ctx(), r);
928  }

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

933  {
934  assert(is_fpa());
936  check_error();
937  return expr(ctx(), r);
938  }

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

943  {
944  assert(is_fpa());
946  check_error();
947  return expr(ctx(), r);
948  }

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

953  {
954  assert(is_fpa());
956  check_error();
957  return expr(ctx(), r);
958  }

◆ mk_to_ieee_bv()

expr mk_to_ieee_bv ( ) const
inline

Convert this fpa into an IEEE BV.

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

963  {
964  assert(is_fpa());
966  check_error();
967  return expr(ctx(), r);
968  }

◆ nth()

expr nth ( expr const &  index) const
inline

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

1468  {
1469  check_context(*this, index);
1470  Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1471  check_error();
1472  return expr(ctx(), r);
1473  }

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

1174 { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }

Referenced by AstRef::__bool__(), expr::args(), expr::end(), and expr::is_const().

◆ numerator()

expr numerator ( ) const
inline

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

1111  {
1112  assert(is_numeral());
1113  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1114  check_error();
1115  return expr(ctx(),r);
1116  }

◆ operator Z3_app()

operator Z3_app ( ) const
inline

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

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

1538  {
1539  assert(is_array() || is_seq());
1540  if (is_array()) {
1541  return select(*this, index);
1542  }
1543  return nth(index);
1544  }

◆ operator[]() [2/2]

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

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

1546  {
1547  return select(*this, index);
1548  }

◆ repeat()

expr repeat ( unsigned  i) const
inline

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

1381 { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }

◆ replace()

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

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

1445  {
1446  check_context(*this, src); check_context(src, dst);
1447  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1448  check_error();
1449  return expr(ctx(), r);
1450  }

◆ rotate_left()

expr rotate_left ( unsigned  i) const
inline

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

1379 { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }

◆ rotate_right()

expr rotate_right ( unsigned  i) const
inline

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

1380 { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }

◆ sbvtos()

expr sbvtos ( ) const
inline

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

1494  {
1495  Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this);
1496  check_error();
1497  return expr(ctx(), r);
1498  }

◆ simplify() [1/2]

expr simplify ( ) const
inline

Return a simplified version of this expression.

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

1553 { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }

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

1557 { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }

◆ stoi()

expr stoi ( ) const
inline

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

1479  {
1480  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1481  check_error();
1482  return expr(ctx(), r);
1483  }

◆ substitute() [1/2]

expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

4052  {
4053  array<Z3_ast> _dst(dst.size());
4054  for (unsigned i = 0; i < dst.size(); ++i) {
4055  _dst[i] = dst[i];
4056  }
4057  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
4058  check_error();
4059  return expr(ctx(), r);
4060  }

◆ substitute() [2/2]

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

Apply substitution. Replace src expressions by dst.

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

4039  {
4040  assert(src.size() == dst.size());
4041  array<Z3_ast> _src(src.size());
4042  array<Z3_ast> _dst(dst.size());
4043  for (unsigned i = 0; i < src.size(); ++i) {
4044  _src[i] = src[i];
4045  _dst[i] = dst[i];
4046  }
4047  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
4048  check_error();
4049  return expr(ctx(), r);
4050  }

◆ ubvtos()

expr ubvtos ( ) const
inline

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

1489  {
1490  Z3_ast r = Z3_mk_ubv_to_str(ctx(), *this);
1491  check_error();
1492  return expr(ctx(), r);
1493  }

◆ unit()

expr unit ( ) const
inline

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

1451  {
1452  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1453  check_error();
1454  return expr(ctx(), r);
1455  }

Friends And Related Function Documentation

◆ abs

expr abs ( expr const &  a)
friend

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

1962  {
1963  Z3_ast r;
1964  if (a.is_int()) {
1965  expr zero = a.ctx().int_val(0);
1966  expr ge = a >= zero;
1967  expr na = -a;
1968  r = Z3_mk_ite(a.ctx(), ge, a, na);
1969  }
1970  else if (a.is_real()) {
1971  expr zero = a.ctx().real_val(0);
1972  expr ge = a >= zero;
1973  expr na = -a;
1974  r = Z3_mk_ite(a.ctx(), ge, a, na);
1975  }
1976  else {
1977  r = Z3_mk_fpa_abs(a.ctx(), a);
1978  }
1979  a.check_error();
1980  return expr(a.ctx(), r);
1981  }

◆ atleast

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

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

2397  {
2398  assert(es.size() > 0);
2399  context& ctx = es[0u].ctx();
2400  array<Z3_ast> _es(es);
2401  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2402  ctx.check_error();
2403  return expr(ctx, r);
2404  }

◆ atmost

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

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

2389  {
2390  assert(es.size() > 0);
2391  context& ctx = es[0u].ctx();
2392  array<Z3_ast> _es(es);
2393  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2394  ctx.check_error();
2395  return expr(ctx, r);
2396  }

◆ bv2int

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

bit-vector and integer conversions.

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

2200 { Z3_ast r = Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error(); return expr(a.ctx(), r); }

◆ bvadd_no_overflow

expr bvadd_no_overflow ( expr const &  a,
expr const &  b,
bool  is_signed 
)
friend

bit-vector overflow/underflow checks

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

2206  {
2207  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);
2208  }

◆ bvadd_no_underflow

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

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

2209  {
2210  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2211  }

◆ bvmul_no_overflow

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

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

2224  {
2225  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);
2226  }

◆ bvmul_no_underflow

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

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

2227  {
2228  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2229  }

◆ bvneg_no_overflow

expr bvneg_no_overflow ( expr const &  a)
friend

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

2221  {
2222  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2223  }

◆ bvredand

expr bvredand ( expr const &  a)
friend

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

1956  {
1957  assert(a.is_bv());
1958  Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
1959  a.check_error();
1960  return expr(a.ctx(), r);
1961  }

◆ bvredor

expr bvredor ( expr const &  a)
friend

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

1950  {
1951  assert(a.is_bv());
1952  Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1953  a.check_error();
1954  return expr(a.ctx(), r);
1955  }

◆ bvsdiv_no_overflow

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

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

2218  {
2219  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2220  }

◆ bvsub_no_overflow

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

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

2212  {
2213  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2214  }

◆ bvsub_no_underflow

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

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

2215  {
2216  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);
2217  }

◆ concat [1/2]

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

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

2423  {
2424  check_context(a, b);
2425  Z3_ast r;
2426  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2427  Z3_ast _args[2] = { a, b };
2428  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2429  }
2430  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2431  Z3_ast _args[2] = { a, b };
2432  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2433  }
2434  else {
2435  r = Z3_mk_concat(a.ctx(), a, b);
2436  }
2437  a.ctx().check_error();
2438  return expr(a.ctx(), r);
2439  }

◆ concat [2/2]

expr concat ( expr_vector const &  args)
friend

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

2441  {
2442  Z3_ast r;
2443  assert(args.size() > 0);
2444  if (args.size() == 1) {
2445  return args[0u];
2446  }
2447  context& ctx = args[0u].ctx();
2448  array<Z3_ast> _args(args);
2449  if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
2450  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2451  }
2452  else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
2453  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2454  }
2455  else {
2456  r = _args[args.size()-1];
2457  for (unsigned i = args.size()-1; i > 0; ) {
2458  --i;
2459  r = Z3_mk_concat(ctx, _args[i], r);
2460  ctx.check_error();
2461  }
2462  }
2463  ctx.check_error();
2464  return expr(ctx, r);
2465  }

◆ distinct

expr distinct ( expr_vector const &  args)
friend

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

2414  {
2415  assert(args.size() > 0);
2416  context& ctx = args[0u].ctx();
2417  array<Z3_ast> _args(args);
2418  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2419  ctx.check_error();
2420  return expr(ctx, r);
2421  }

◆ fma

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

FloatingPoint fused multiply-add.

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

1998  {
1999  check_context(a, b); check_context(a, c); check_context(a, rm);
2000  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2001  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
2002  a.check_error();
2003  return expr(a.ctx(), r);
2004  }

◆ fp_eq

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

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

1989  {
1990  check_context(a, b);
1991  assert(a.is_fpa());
1992  Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
1993  a.check_error();
1994  return expr(a.ctx(), r);
1995  }

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

2006  {
2007  check_context(sgn, exp); check_context(exp, sig);
2008  assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2009  Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
2010  sgn.check_error();
2011  return expr(sgn.ctx(), r);
2012  }

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

2042  {
2043  assert(t.is_fpa());
2044  Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2045  t.check_error();
2046  return expr(t.ctx(), r);
2047  }

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

2014  {
2015  assert(t.is_fpa());
2016  Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2017  t.check_error();
2018  return expr(t.ctx(), r);
2019  }

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

2021  {
2022  assert(t.is_fpa());
2023  Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2024  t.check_error();
2025  return expr(t.ctx(), r);
2026  }

◆ implies [1/3]

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

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

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

◆ implies [2/3]

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

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

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

◆ implies [3/3]

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

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

1598  {
1599  assert(a.is_bool() && b.is_bool());
1600  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1601  }

◆ int2bv

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

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

2201 { Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }

◆ is_int

expr is_int ( expr const &  e)
friend

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

1646 { _Z3_MK_UN_(e, Z3_mk_is_int); }

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

2061  {
2062  check_context(c, t); check_context(c, e);
2063  assert(c.is_bool());
2064  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
2065  c.check_error();
2066  return expr(c.ctx(), r);
2067  }

◆ max

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

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

1935  {
1936  check_context(a, b);
1937  Z3_ast r;
1938  if (a.is_arith()) {
1939  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1940  }
1941  else if (a.is_bv()) {
1942  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1943  }
1944  else {
1945  assert(a.is_fpa());
1946  r = Z3_mk_fpa_max(a.ctx(), a, b);
1947  }
1948  return expr(a.ctx(), r);
1949  }

◆ min

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

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

1920  {
1921  check_context(a, b);
1922  Z3_ast r;
1923  if (a.is_arith()) {
1924  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1925  }
1926  else if (a.is_bv()) {
1927  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1928  }
1929  else {
1930  assert(a.is_fpa());
1931  r = Z3_mk_fpa_min(a.ctx(), a, b);
1932  }
1933  return expr(a.ctx(), r);
1934  }

◆ mk_and

expr mk_and ( expr_vector const &  args)
friend

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

2473  {
2474  array<Z3_ast> _args(args);
2475  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2476  args.check_error();
2477  return expr(args.ctx(), r);
2478  }

◆ mk_or

expr mk_or ( expr_vector const &  args)
friend

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

2467  {
2468  array<Z3_ast> _args(args);
2469  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2470  args.check_error();
2471  return expr(args.ctx(), r);
2472  }

◆ mk_xor

expr mk_xor ( expr_vector const &  args)
friend

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

2479  {
2480  if (args.empty())
2481  return args.ctx().bool_val(false);
2482  expr r = args[0u];
2483  for (unsigned i = 1; i < args.size(); ++i)
2484  r = r ^ args[i];
2485  return r;
2486  }

◆ mod [1/3]

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

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

1610  {
1611  if (a.is_bv()) {
1612  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1613  }
1614  else {
1615  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1616  }
1617  }

◆ mod [2/3]

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

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

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

◆ mod [3/3]

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

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

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

◆ nand

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

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

1917 { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }

◆ nor

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

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

1918 { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }

◆ operator!

expr operator! ( expr const &  a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

1644 { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }

◆ operator!= [1/3]

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

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

1686  {
1687  check_context(a, b);
1688  Z3_ast args[2] = { a, b };
1689  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1690  a.check_error();
1691  return expr(a.ctx(), r);
1692  }

◆ operator!= [2/3]

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

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

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

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

1905 { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }

◆ operator& [2/3]

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

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

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

◆ operator& [3/3]

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

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

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

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

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

1650  {
1651  check_context(a, b);
1652  assert(a.is_bool() && b.is_bool());
1653  Z3_ast args[2] = { a, b };
1654  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1655  a.check_error();
1656  return expr(a.ctx(), r);
1657  }

◆ operator* [1/3]

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

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

1728  {
1729  check_context(a, b);
1730  Z3_ast r = 0;
1731  if (a.is_arith() && b.is_arith()) {
1732  Z3_ast args[2] = { a, b };
1733  r = Z3_mk_mul(a.ctx(), 2, args);
1734  }
1735  else if (a.is_bv() && b.is_bv()) {
1736  r = Z3_mk_bvmul(a.ctx(), a, b);
1737  }
1738  else if (a.is_fpa() && b.is_fpa()) {
1739  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1740  }
1741  else {
1742  // operator is not supported by given arguments.
1743  assert(false);
1744  }
1745  a.check_error();
1746  return expr(a.ctx(), r);
1747  }

◆ operator* [2/3]

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

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

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

◆ operator* [3/3]

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

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

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

1698  {
1699  check_context(a, b);
1700  Z3_ast r = 0;
1701  if (a.is_arith() && b.is_arith()) {
1702  Z3_ast args[2] = { a, b };
1703  r = Z3_mk_add(a.ctx(), 2, args);
1704  }
1705  else if (a.is_bv() && b.is_bv()) {
1706  r = Z3_mk_bvadd(a.ctx(), a, b);
1707  }
1708  else if (a.is_seq() && b.is_seq()) {
1709  return concat(a, b);
1710  }
1711  else if (a.is_re() && b.is_re()) {
1712  Z3_ast _args[2] = { a, b };
1713  r = Z3_mk_re_union(a.ctx(), 2, _args);
1714  }
1715  else if (a.is_fpa() && b.is_fpa()) {
1716  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1717  }
1718  else {
1719  // operator is not supported by given arguments.
1720  assert(false);
1721  }
1722  a.check_error();
1723  return expr(a.ctx(), r);
1724  }

◆ operator+ [2/3]

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

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

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

◆ operator+ [3/3]

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

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

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

◆ operator- [1/4]

expr operator- ( expr const &  a)
friend

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

1794  {
1795  Z3_ast r = 0;
1796  if (a.is_arith()) {
1797  r = Z3_mk_unary_minus(a.ctx(), a);
1798  }
1799  else if (a.is_bv()) {
1800  r = Z3_mk_bvneg(a.ctx(), a);
1801  }
1802  else if (a.is_fpa()) {
1803  r = Z3_mk_fpa_neg(a.ctx(), a);
1804  }
1805  else {
1806  // operator is not supported by given arguments.
1807  assert(false);
1808  }
1809  a.check_error();
1810  return expr(a.ctx(), r);
1811  }

◆ operator- [2/4]

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

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

1813  {
1814  check_context(a, b);
1815  Z3_ast r = 0;
1816  if (a.is_arith() && b.is_arith()) {
1817  Z3_ast args[2] = { a, b };
1818  r = Z3_mk_sub(a.ctx(), 2, args);
1819  }
1820  else if (a.is_bv() && b.is_bv()) {
1821  r = Z3_mk_bvsub(a.ctx(), a, b);
1822  }
1823  else if (a.is_fpa() && b.is_fpa()) {
1824  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1825  }
1826  else {
1827  // operator is not supported by given arguments.
1828  assert(false);
1829  }
1830  a.check_error();
1831  return expr(a.ctx(), r);
1832  }

◆ operator- [3/4]

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

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

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

◆ operator- [4/4]

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

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

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

1772  {
1773  check_context(a, b);
1774  Z3_ast r = 0;
1775  if (a.is_arith() && b.is_arith()) {
1776  r = Z3_mk_div(a.ctx(), a, b);
1777  }
1778  else if (a.is_bv() && b.is_bv()) {
1779  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1780  }
1781  else if (a.is_fpa() && b.is_fpa()) {
1782  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1783  }
1784  else {
1785  // operator is not supported by given arguments.
1786  assert(false);
1787  }
1788  a.check_error();
1789  return expr(a.ctx(), r);
1790  }

◆ operator/ [2/3]

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

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

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

◆ operator/ [3/3]

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

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

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

1861  {
1862  check_context(a, b);
1863  Z3_ast r = 0;
1864  if (a.is_arith() && b.is_arith()) {
1865  r = Z3_mk_lt(a.ctx(), a, b);
1866  }
1867  else if (a.is_bv() && b.is_bv()) {
1868  r = Z3_mk_bvslt(a.ctx(), a, b);
1869  }
1870  else if (a.is_fpa() && b.is_fpa()) {
1871  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1872  }
1873  else {
1874  // operator is not supported by given arguments.
1875  assert(false);
1876  }
1877  a.check_error();
1878  return expr(a.ctx(), r);
1879  }

◆ operator< [2/3]

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

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

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

◆ operator< [3/3]

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

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

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

1836  {
1837  check_context(a, b);
1838  Z3_ast r = 0;
1839  if (a.is_arith() && b.is_arith()) {
1840  r = Z3_mk_le(a.ctx(), a, b);
1841  }
1842  else if (a.is_bv() && b.is_bv()) {
1843  r = Z3_mk_bvsle(a.ctx(), a, b);
1844  }
1845  else if (a.is_fpa() && b.is_fpa()) {
1846  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1847  }
1848  else {
1849  // operator is not supported by given arguments.
1850  assert(false);
1851  }
1852  a.check_error();
1853  return expr(a.ctx(), r);
1854  }

◆ operator<= [2/3]

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

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

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

◆ operator<= [3/3]

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

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

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

1675  {
1676  check_context(a, b);
1677  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1678  a.check_error();
1679  return expr(a.ctx(), r);
1680  }

◆ operator== [2/3]

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

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

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

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

1883  {
1884  check_context(a, b);
1885  Z3_ast r = 0;
1886  if (a.is_arith() && b.is_arith()) {
1887  r = Z3_mk_gt(a.ctx(), a, b);
1888  }
1889  else if (a.is_bv() && b.is_bv()) {
1890  r = Z3_mk_bvsgt(a.ctx(), a, b);
1891  }
1892  else if (a.is_fpa() && b.is_fpa()) {
1893  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1894  }
1895  else {
1896  // operator is not supported by given arguments.
1897  assert(false);
1898  }
1899  a.check_error();
1900  return expr(a.ctx(), r);
1901  }

◆ operator> [2/3]

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

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

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

◆ operator> [3/3]

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

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

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

1752  {
1753  check_context(a, b);
1754  Z3_ast r = 0;
1755  if (a.is_arith() && b.is_arith()) {
1756  r = Z3_mk_ge(a.ctx(), a, b);
1757  }
1758  else if (a.is_bv() && b.is_bv()) {
1759  r = Z3_mk_bvsge(a.ctx(), a, b);
1760  }
1761  else if (a.is_fpa() && b.is_fpa()) {
1762  r = Z3_mk_fpa_geq(a.ctx(), a, b);
1763  }
1764  else {
1765  // operator is not supported by given arguments.
1766  assert(false);
1767  }
1768  a.check_error();
1769  return expr(a.ctx(), r);
1770  }

◆ operator>= [2/3]

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

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

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

◆ operator>= [3/3]

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

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

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

1909 { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }

◆ operator^ [2/3]

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

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

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

◆ operator^ [3/3]

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

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

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

1913 { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }

◆ operator| [2/3]

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

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

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

◆ operator| [3/3]

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

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

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

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

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

1662  {
1663  check_context(a, b);
1664  assert(a.is_bool() && b.is_bool());
1665  Z3_ast args[2] = { a, b };
1666  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1667  a.check_error();
1668  return expr(a.ctx(), r);
1669  }

◆ operator~

expr operator~ ( expr const &  a)
friend

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

1996 { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }

◆ pbeq

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

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

2381  {
2382  assert(es.size() > 0);
2383  context& ctx = es[0u].ctx();
2384  array<Z3_ast> _es(es);
2385  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2386  ctx.check_error();
2387  return expr(ctx, r);
2388  }

◆ pbge

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

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

2373  {
2374  assert(es.size() > 0);
2375  context& ctx = es[0u].ctx();
2376  array<Z3_ast> _es(es);
2377  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2378  ctx.check_error();
2379  return expr(ctx, r);
2380  }

◆ pble

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

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

2365  {
2366  assert(es.size() > 0);
2367  context& ctx = es[0u].ctx();
2368  array<Z3_ast> _es(es);
2369  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2370  ctx.check_error();
2371  return expr(ctx, r);
2372  }

◆ pw [1/3]

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

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

1606 { _Z3_MK_BIN_(a, b, Z3_mk_power); }

◆ pw [2/3]

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

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

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

◆ pw [3/3]

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

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

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

◆ range

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

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

3946  {
3947  check_context(lo, hi);
3948  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3949  lo.check_error();
3950  return expr(lo.ctx(), r);
3951  }

◆ rem [1/3]

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

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

1626  {
1627  if (a.is_fpa() && b.is_fpa()) {
1628  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1629  } else {
1630  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1631  }
1632  }

◆ rem [2/3]

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

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

1633 { return rem(a, a.ctx().num_val(b, a.get_sort())); }

◆ rem [3/3]

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

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

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

2049  {
2050  assert(t.is_fpa());
2051  Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
2052  t.check_error();
2053  return expr(t.ctx(), r);
2054  }

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

2028  {
2029  assert(t.is_bv());
2030  Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2031  t.check_error();
2032  return expr(t.ctx(), r);
2033  }

◆ sqrt

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

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

1982  {
1983  check_context(a, rm);
1984  assert(a.is_fpa());
1985  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1986  a.check_error();
1987  return expr(a.ctx(), r);
1988  }

◆ sum

expr sum ( expr_vector const &  args)
friend

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

2405  {
2406  assert(args.size() > 0);
2407  context& ctx = args[0u].ctx();
2408  array<Z3_ast> _args(args);
2409  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2410  ctx.check_error();
2411  return expr(ctx, r);
2412  }

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

2035  {
2036  assert(t.is_bv());
2037  Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2038  t.check_error();
2039  return expr(t.ctx(), r);
2040  }

◆ xnor

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

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

1919 { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
Z3_mk_pble
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_mk_fpa_lt
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
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.
Z3_mk_bvuge
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_mk_bvmul_no_overflow
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
z3::expr::lo
unsigned lo() const
Definition: z3++.h:1393
Z3_mk_fpa_fp
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.
z3::ast::kind
Z3_ast_kind kind() const
Definition: z3++.h:546
Z3_VAR_AST
@ Z3_VAR_AST
Definition: z3_api.h:142
z3::sort::is_fpa
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:701
Z3_mk_atmost
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_mk_fpa_is_zero
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.
z3::sort::is_relation
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:685
Z3_mk_div
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_mk_rem
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
Z3_mk_fpa_min
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
Z3_mk_int2bv
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.
Z3_mk_fpa_to_fp_unsigned
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.
Z3_OP_NOT
@ Z3_OP_NOT
Definition: z3_api.h:972
_Z3_MK_BIN_
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1591
Z3_mk_ite
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_mk_fpa_to_ubv
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.
Z3_mk_char_to_bv
Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch)
Create a bit-vector (code point) from character.
Z3_get_denominator
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
z3::expr::is_numeral_i
bool is_numeral_i(int &i) const
Definition: z3++.h:858
Z3_mk_fpa_sub
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
z3::sort::is_re
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:693
Z3_mk_seq_length
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
Z3_mk_bvadd_no_underflow
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.
Z3_mk_pbeq
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.
Z3_mk_fpa_is_nan
Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t)
Predicate indicating whether t is a NaN.
Z3_mk_fpa_to_fp_float
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.
Z3_mk_bvmul
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_mk_bvsle
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_mk_re_concat
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_mk_fpa_add
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
z3::expr::arg
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application.
Definition: z3++.h:1182
Z3_THROW
#define Z3_THROW(x)
Definition: z3++.h:102
Z3_mk_concat
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
z3::expr::is_numeral_u
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:859
Z3_is_well_sorted
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
Z3_mk_sub
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
z3::select
expr select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3764
z3::expr::rem
friend expr rem(expr const &a, expr const &b)
Definition: z3++.h:1626
Z3_mk_fpa_is_subnormal
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.
z3::sort::is_array
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:677
Z3_mk_char_from_bv
Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv)
Create a character from a bit-vector (code point).
Z3_mk_seq_at
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index. The sequence is empty if the index is...
Z3_mk_unary_minus
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_get_numeral_int
bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int....
z3::expr::hi
unsigned hi() const
Definition: z3++.h:1394
Z3_mk_distinct
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_mk_fpa_rem
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
Z3_mk_fpa_is_infinite
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.
Z3_mk_seq_replace
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.
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:143
Microsoft.Z3.Z3_sort
System.IntPtr Z3_sort
Definition: NativeContext.cs:33
Z3_is_quantifier_forall
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
Z3_mk_bvnand
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
Z3_is_quantifier_exists
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
Z3_get_string_length
unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s)
Retrieve the length of the unescaped string constant stored in s.
Z3_mk_bit2bool
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.
Z3_mk_ge
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
z3::expr::num_args
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:1174
Z3_mk_seq_concat
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
z3::sort::is_bv
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:673
Z3_mk_bvneg_no_overflow
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
Z3_mk_fpa_to_fp_bv
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.
Z3_mk_bv2int
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...
Microsoft.Z3.Z3_func_decl
System.IntPtr Z3_func_decl
Definition: NativeContext.cs:30
Z3_mk_or
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
z3::ast_vector_tpl::size
unsigned size() const
Definition: z3++.h:575
Z3_OP_TRUE
@ Z3_OP_TRUE
Definition: z3_api.h:963
Z3_mk_seq_extract
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.
Z3_mk_bvnor
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
Z3_mk_fpa_eq
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.
Z3_mk_char_to_int
Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)
Create an integer (code point) from character.
Z3_mk_bvredand
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
_Z3_MK_UN_
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1638
Z3_OP_IMPLIES
@ Z3_OP_IMPLIES
Definition: z3_api.h:973
Z3_is_algebraic_number
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.
Z3_mk_ubv_to_str
Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s)
Unsigned bit-vector to string conversion.
Z3_mk_rotate_right
Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the right i times.
Z3_mk_lt
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
z3::expr::is_quantifier
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:881
Z3_mk_bvsub_no_underflow
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
Z3_mk_add
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].
Z3_get_decl_int_parameter
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.
Z3_mk_fpa_max
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
Z3_mk_implies
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
z3::expr::is_seq
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:830
Z3_mk_bvsdiv
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_mk_not
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_get_app_arg
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
Z3_substitute_vars
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs,...
Z3_mk_bvsge
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_is_re_sort
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
Z3_mk_seq_nth
Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the element positioned at position index. The function is under-specified if the inde...
Z3_get_algebraic_number_upper
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...
z3::object::m_ctx
context * m_ctx
Definition: z3++.h:448
Z3_get_app_decl
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
z3::ast::m_ast
Z3_ast m_ast
Definition: z3++.h:530
Z3_get_decl_num_parameters
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
z3::func_decl::decl_kind
Z3_decl_kind decl_kind() const
Definition: z3++.h:751
Z3_get_numeral_binary_string
Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a)
Return numeral value, as a binary string of a numeric constant term.
Z3_mk_seq_unit
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
Z3_get_numeral_string
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.
Z3_mk_atleast
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_mk_fpa_abs
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
Z3_OP_EQ
@ Z3_OP_EQ
Definition: z3_api.h:965
Z3_mk_bvsub_no_overflow
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.
z3::sort::is_datatype
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:681
Z3_get_quantifier_body
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
Z3_mk_and
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
Z3_get_string
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...
Z3_mk_fpa_is_normal
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.
Z3_mk_str_to_int
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
Z3_substitute
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....
z3::expr::implies
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:1598
Z3_mk_sbv_to_str
Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s)
Signed bit-vector to string conversion.
Microsoft.Z3.Z3_ast_vector
System.IntPtr Z3_ast_vector
Definition: NativeContext.cs:29
z3::expr::is_numeral
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:855
Z3_mk_bvxnor
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Z3_mk_int_to_str
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
Z3_mk_eq
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
Microsoft.Z3.Z3_app
System.IntPtr Z3_app
Definition: NativeContext.cs:27
Z3_mk_extract
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,...
Z3_get_numerator
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
z3::expr::expr
expr(context &c)
Definition: z3++.h:787
Z3_simplify_ex
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_mk_re_union
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_OP_DISTINCT
@ Z3_OP_DISTINCT
Definition: z3_api.h:966
Z3_mk_bvadd_no_overflow
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
Z3_mk_fpa_mul
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
Z3_mk_mul
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_mk_bvor
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
Z3_is_seq_sort
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
z3::expr::pw
friend expr pw(expr const &a, expr const &b)
Definition: z3++.h:1606
z3::sort::is_finite_domain
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:697
Z3_mk_bvsgt
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_OP_XOR
@ Z3_OP_XOR
Definition: z3_api.h:971
z3::expr::is_algebraic
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:903
z3::expr::decl
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1167
z3::sort::is_int
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:661
Z3_mk_bvadd
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:75
z3::sort::is_seq
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:689
z3::expr::concat
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:2423
Z3_OP_AND
@ Z3_OP_AND
Definition: z3_api.h:968
Z3_algebraic_get_poly
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
Z3_mk_bvnot
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_mk_le
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_mk_repeat
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
z3::sort::is_arith
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:669
Z3_mk_bvsdiv_no_overflow
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
Z3_mk_bvmul_no_underflow
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
Z3_is_lambda
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
Z3_APP_AST
@ Z3_APP_AST
Definition: z3_api.h:141
Z3_mk_fpa_neg
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_OP_ITE
@ Z3_OP_ITE
Definition: z3_api.h:967
Z3_mk_bvneg
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:455
Z3_get_numeral_int64
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....
z3::expr::mod
friend expr mod(expr const &a, expr const &b)
Definition: z3++.h:1610
z3::expr::args
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:1189
Z3_simplify
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_mk_mod
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::expr::is_bv
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:814
Z3_mk_rotate_left
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.
z3::expr::is_array
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:818
Z3_get_numeral_double
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
z3::sort::is_real
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:665
z3::expr::nth
expr nth(expr const &index) const
Definition: z3++.h:1468
z3::ast::ast
ast(context &c)
Definition: z3++.h:532
Z3_get_numeral_decimal_string
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.
z3::sort::is_bool
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:657
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.
Z3_get_bool_value
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.
Z3_mk_re_range
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
Z3_mk_fpa_round_to_integral
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,...
Z3_get_app_num_args
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
Z3_is_string
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
Z3_mk_gt
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_get_string_contents
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.
Microsoft.Z3.Z3_ast
System.IntPtr Z3_ast
Definition: NativeContext.cs:28
Z3_get_algebraic_number_lower
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...
Z3_mk_fpa_to_ieee_bv
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.
Z3_mk_bvslt
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
z3::expr::is_numeral_i64
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:856
Z3_get_sort
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
Z3_mk_fpa_div
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
Z3_mk_bvsmod
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
Z3_mk_fpa_fma
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.
Z3_algebraic_get_i
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.
Z3_mk_pbge
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
z3::expr::length
expr length() const
Definition: z3++.h:1474
Z3_mk_bvsub
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_mk_bvand
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
Z3_get_numeral_uint
bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int....
Z3_OP_FALSE
@ Z3_OP_FALSE
Definition: z3_api.h:964
Z3_mk_fpa_to_fp_signed
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.
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:452
Z3_mk_bvxor
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_mk_fpa_geq
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:190
z3::expr::is_fpa
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:848
Z3_get_numeral_uint64
bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int....
z3::ast_vector_tpl::empty
bool empty() const
Definition: z3++.h:581
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition: z3_api.h:140
Z3_mk_seq_contains
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
z3::object::ctx
context & ctx() const
Definition: z3++.h:451
Z3_mk_fpa_gt
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
Z3_mk_char_is_digit
Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch)
Create a check if the character is a digit.
Z3_mk_fpa_to_sbv
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.
Z3_get_ast_id
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality....
Z3_mk_re_loop
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_OP_OR
@ Z3_OP_OR
Definition: z3_api.h:969
Z3_mk_bvredor
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
Z3_mk_xor
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
z3::expr::is_app
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:873
z3::expr::is_string_value
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:1131
z3::expr::is_numeral_u64
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:857
z3::expr::get_sort
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:793
Z3_mk_fpa_leq
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
Z3_mk_fpa_sqrt
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.