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

Public Member Functions

 expr (context &c)
 
 expr (context &c, Z3_ast n)
 
 expr (expr const &n)
 
exproperator= (expr const &n)
 
sort get_sort () const
 Return the sort of this expression. More...
 
bool is_bool () const
 Return true if this is a Boolean expression. More...
 
bool is_int () const
 Return true if this is an integer expression. More...
 
bool is_real () const
 Return true if this is a real expression. More...
 
bool is_arith () const
 Return true if this is an integer or real expression. More...
 
bool is_bv () const
 Return true if this is a Bit-vector expression. More...
 
bool is_array () const
 Return true if this is a Array expression. More...
 
bool is_datatype () const
 Return true if this is a Datatype expression. More...
 
bool is_relation () const
 Return true if this is a Relation expression. More...
 
bool is_seq () const
 Return true if this is a sequence expression. More...
 
bool is_re () const
 Return true if this is a regular expression. More...
 
bool is_finite_domain () const
 Return true if this is a Finite-domain expression. More...
 
bool is_fpa () const
 Return true if this is a FloatingPoint expression. . More...
 
bool is_numeral () const
 Return true if this expression is a numeral. Specialized functions also return representations for the numerals as small integers, 64 bit integers or rational or decimal strings. More...
 
bool is_numeral_i64 (int64_t &i) const
 
bool is_numeral_u64 (uint64_t &i) const
 
bool is_numeral_i (int &i) const
 
bool is_numeral_u (unsigned &i) const
 
bool is_numeral (std::string &s) const
 
bool is_numeral (std::string &s, unsigned precision) const
 
bool is_numeral (double &d) const
 
bool is_app () const
 Return true if this expression is an application. More...
 
bool is_const () const
 Return true if this expression is a constant (i.e., an application with 0 arguments). More...
 
bool is_quantifier () const
 Return true if this expression is a quantifier. More...
 
bool is_forall () const
 Return true if this expression is a universal quantifier. More...
 
bool is_exists () const
 Return true if this expression is an existential quantifier. More...
 
bool is_lambda () const
 Return true if this expression is a lambda expression. More...
 
bool is_var () const
 Return true if this expression is a variable. More...
 
bool is_algebraic () const
 Return true if expression is an algebraic number. More...
 
bool is_well_sorted () const
 Return true if this expression is well sorted (aka type correct). More...
 
std::string get_decimal_string (int precision) const
 Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic. More...
 
expr algebraic_lower (unsigned precision) const
 
expr algebraic_upper (unsigned precision) const
 
expr_vector algebraic_poly () const
 Return coefficients for p of an algebraic number (root-obj p i) More...
 
unsigned algebraic_i () const
 Return i of an algebraic number (root-obj p i) More...
 
unsigned id () const
 retrieve unique identifier for expression. More...
 
int get_numeral_int () const
 Return int value of numeral, throw if result cannot fit in machine int. More...
 
unsigned get_numeral_uint () const
 Return uint value of numeral, throw if result cannot fit in machine uint. More...
 
int64_t get_numeral_int64 () const
 Return int64_t value of numeral, throw if result cannot fit in int64_t. More...
 
uint64_t get_numeral_uint64 () const
 Return uint64_t value of numeral, throw if result cannot fit in uint64_t. More...
 
Z3_lbool bool_value () const
 
expr numerator () const
 
expr denominator () const
 
bool is_string_value () const
 Return true if this expression is a string literal. The string can be accessed using get_string() and get_escaped_string() More...
 
std::string get_escaped_string () const
 for a string value expression return an escaped or unescaped string value. More...
 
std::string get_string () const
 
 operator Z3_app () const
 
sort fpa_rounding_mode ()
 Return a RoundingMode sort. More...
 
func_decl decl () const
 Return the declaration associated with this application. This method assumes the expression is an application. More...
 
unsigned num_args () const
 Return the number of arguments in this application. This method assumes the expression is an application. More...
 
expr arg (unsigned i) const
 Return the i-th argument of this application. This method assumes the expression is an application. More...
 
expr body () const
 Return the 'body' of this quantifier. More...
 
bool is_true () const
 
bool is_false () const
 
bool is_not () const
 
bool is_and () const
 
bool is_or () const
 
bool is_xor () const
 
bool is_implies () const
 
bool is_eq () const
 
bool is_ite () const
 
bool is_distinct () const
 
expr rotate_left (unsigned i)
 
expr rotate_right (unsigned i)
 
expr repeat (unsigned i)
 
expr extract (unsigned hi, unsigned lo) const
 
unsigned lo () const
 
unsigned hi () const
 
expr extract (expr const &offset, expr const &length) const
 sequence and regular expression operations. More...
 
expr replace (expr const &src, expr const &dst) const
 
expr unit () const
 
expr contains (expr const &s)
 
expr at (expr const &index) const
 
expr nth (expr const &index) const
 
expr length () const
 
expr stoi () const
 
expr itos () const
 
expr loop (unsigned lo)
 create a looping regular expression. More...
 
expr loop (unsigned lo, unsigned hi)
 
expr operator[] (expr const &index) const
 
expr operator[] (expr_vector const &index) const
 
expr simplify () const
 Return a simplified version of this expression. More...
 
expr simplify (params const &p) const
 Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier. More...
 
expr substitute (expr_vector const &src, expr_vector const &dst)
 Apply substitution. Replace src expressions by dst. More...
 
expr substitute (expr_vector const &dst)
 Apply substitution. Replace bound variables by expressions. More...
 
- 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)
 
 object (object const &s)
 
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_and (expr_vector const &args)
 
expr ite (expr const &c, expr const &t, expr const &e)
 Create the if-then-else expression ite(c, t, e) More...
 
expr distinct (expr_vector const &args)
 
expr concat (expr const &a, expr const &b)
 
expr concat (expr_vector const &args)
 
expr operator== (expr const &a, expr const &b)
 
expr operator== (expr const &a, int b)
 
expr operator== (int a, expr const &b)
 
expr operator!= (expr const &a, expr const &b)
 
expr operator!= (expr const &a, int b)
 
expr operator!= (int a, expr const &b)
 
expr operator+ (expr const &a, expr const &b)
 
expr operator+ (expr const &a, int b)
 
expr operator+ (int a, expr const &b)
 
expr sum (expr_vector const &args)
 
expr operator* (expr const &a, expr const &b)
 
expr operator* (expr const &a, int b)
 
expr operator* (int a, expr const &b)
 
expr pw (expr const &a, expr const &b)
 
expr pw (expr const &a, int b)
 
expr pw (int a, expr const &b)
 
expr mod (expr const &a, expr const &b)
 
expr mod (expr const &a, int b)
 
expr mod (int a, expr const &b)
 
expr rem (expr const &a, expr const &b)
 
expr rem (expr const &a, int b)
 
expr rem (int a, expr const &b)
 
expr is_int (expr const &e)
 
expr operator/ (expr const &a, expr const &b)
 
expr operator/ (expr const &a, int b)
 
expr operator/ (int a, expr const &b)
 
expr operator- (expr const &a)
 
expr operator- (expr const &a, expr const &b)
 
expr operator- (expr const &a, int b)
 
expr operator- (int a, expr const &b)
 
expr operator<= (expr const &a, expr const &b)
 
expr operator<= (expr const &a, int b)
 
expr operator<= (int a, expr const &b)
 
expr operator>= (expr const &a, expr const &b)
 
expr operator>= (expr const &a, int b)
 
expr operator>= (int a, expr const &b)
 
expr operator< (expr const &a, expr const &b)
 
expr operator< (expr const &a, int b)
 
expr operator< (int a, expr const &b)
 
expr operator> (expr const &a, expr const &b)
 
expr operator> (expr const &a, int b)
 
expr operator> (int a, expr const &b)
 
expr pble (expr_vector const &es, int const *coeffs, int bound)
 
expr pbge (expr_vector const &es, int const *coeffs, int bound)
 
expr pbeq (expr_vector const &es, int const *coeffs, int bound)
 
expr atmost (expr_vector const &es, unsigned bound)
 
expr atleast (expr_vector const &es, unsigned bound)
 
expr operator& (expr const &a, expr const &b)
 
expr operator& (expr const &a, int b)
 
expr operator& (int a, expr const &b)
 
expr operator^ (expr const &a, expr const &b)
 
expr operator^ (expr const &a, int b)
 
expr operator^ (int a, expr const &b)
 
expr operator| (expr const &a, expr const &b)
 
expr operator| (expr const &a, int b)
 
expr operator| (int a, expr const &b)
 
expr nand (expr const &a, expr const &b)
 
expr nor (expr const &a, expr const &b)
 
expr xnor (expr const &a, expr const &b)
 
expr min (expr const &a, expr const &b)
 
expr max (expr const &a, expr const &b)
 
expr bv2int (expr const &a, bool is_signed)
 bit-vector and integer conversions. More...
 
expr int2bv (unsigned n, expr const &a)
 
expr bvadd_no_overflow (expr const &a, expr const &b, bool is_signed)
 bit-vector overflow/underflow checks More...
 
expr bvadd_no_underflow (expr const &a, expr const &b)
 
expr bvsub_no_overflow (expr const &a, expr const &b)
 
expr bvsub_no_underflow (expr const &a, expr const &b, bool is_signed)
 
expr bvsdiv_no_overflow (expr const &a, expr const &b)
 
expr bvneg_no_overflow (expr const &a)
 
expr bvmul_no_overflow (expr const &a, expr const &b, bool is_signed)
 
expr bvmul_no_underflow (expr const &a, expr const &b)
 
expr abs (expr const &a)
 
expr sqrt (expr const &a, expr const &rm)
 
expr operator~ (expr const &a)
 
expr fma (expr const &a, expr const &b, expr const &c, expr const &rm)
 FloatingPoint fused multiply-add. More...
 
expr range (expr const &lo, expr const &hi)
 

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

Constructor & Destructor Documentation

◆ expr() [1/3]

expr ( context c)
inline

◆ expr() [2/3]

expr ( context c,
Z3_ast  n 
)
inline

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

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

◆ expr() [3/3]

expr ( expr const &  n)
inline

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

741 :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 899 of file z3++.h.

899  {
900  assert(is_algebraic());
901  unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
902  check_error();
903  return i;
904  }

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

872  {
873  assert(is_algebraic());
874  Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
875  check_error();
876  return expr(ctx(), r);
877  }

◆ algebraic_poly()

expr_vector algebraic_poly ( ) const
inline

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

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

889  {
890  assert(is_algebraic());
891  Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
892  check_error();
893  return expr_vector(ctx(), r);
894  }

◆ algebraic_upper()

expr algebraic_upper ( unsigned  precision) const
inline

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

879  {
880  assert(is_algebraic());
881  Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
882  check_error();
883  return expr(ctx(), r);
884  }

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

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

Referenced by AstRef::__bool__().

◆ at()

expr at ( expr const &  index) const
inline

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

1291  {
1292  check_context(*this, index);
1293  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1294  check_error();
1295  return expr(ctx(), r);
1296  }

◆ body()

expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

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

985  {
986  return Z3_get_bool_value(ctx(), m_ast);
987  }

◆ contains()

expr contains ( expr const &  s)
inline

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

1285  {
1286  check_context(*this, s);
1287  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1288  check_error();
1289  return expr(ctx(), r);
1290  }

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

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

997  {
998  assert(is_numeral());
999  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
1000  check_error();
1001  return expr(ctx(),r);
1002  }

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

1270  {
1271  check_context(*this, offset); check_context(offset, length);
1272  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1273  }

◆ extract() [2/2]

expr extract ( unsigned  hi,
unsigned  lo 
) const
inline

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

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

◆ fpa_rounding_mode()

sort fpa_rounding_mode ( )
inline

Return a RoundingMode sort.

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

1036  {
1037  assert(is_fpa());
1038  Z3_sort s = ctx().fpa_rounding_mode();
1039  check_error();
1040  return sort(ctx(), s);
1041  }

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

864  {
865  assert(is_numeral() || is_algebraic());
866  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
867  }

◆ get_escaped_string()

std::string get_escaped_string ( ) const
inline

for a string value expression return an escaped or unescaped string value.

Precondition
expression is for a string value.

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

1016  {
1017  assert(is_string_value());
1018  char const* s = Z3_get_string(ctx(), m_ast);
1019  check_error();
1020  return std::string(s);
1021  }

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

921  {
922  int result = 0;
923  if (!is_numeral_i(result)) {
924  assert(ctx().enable_exceptions());
925  if (!ctx().enable_exceptions()) return 0;
926  Z3_THROW(exception("numeral does not fit in machine int"));
927  }
928  return result;
929  }

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

957  {
958  assert(is_numeral());
959  int64_t result = 0;
960  if (!is_numeral_i64(result)) {
961  assert(ctx().enable_exceptions());
962  if (!ctx().enable_exceptions()) return 0;
963  Z3_THROW(exception("numeral does not fit in machine int64_t"));
964  }
965  return result;
966  }

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

940  {
941  assert(is_numeral());
942  unsigned result = 0;
943  if (!is_numeral_u(result)) {
944  assert(ctx().enable_exceptions());
945  if (!ctx().enable_exceptions()) return 0;
946  Z3_THROW(exception("numeral does not fit in machine uint"));
947  }
948  return result;
949  }

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

974  {
975  assert(is_numeral());
976  uint64_t result = 0;
977  if (!is_numeral_u64(result)) {
978  assert(ctx().enable_exceptions());
979  if (!ctx().enable_exceptions()) return 0;
980  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
981  }
982  return result;
983  }

◆ get_sort()

sort get_sort ( ) const
inline

◆ get_string()

std::string get_string ( ) const
inline

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

1023  {
1024  assert(is_string_value());
1025  unsigned n;
1026  char const* s = Z3_get_lstring(ctx(), m_ast, &n);
1027  check_error();
1028  return std::string(s, n);
1029  }

◆ hi()

unsigned hi ( ) const
inline

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

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

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

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

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

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

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

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

Referenced by solver::add(), optimize::add(), z3::implies(), z3::ite(), z3::operator!(), z3::operator&&(), and z3::operator||().

◆ is_bv()

bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

768 { return get_sort().is_bv(); }

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

◆ is_const()

bool is_const ( ) const
inline

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

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

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

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

◆ is_distinct()

bool is_distinct ( ) const
inline

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

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

◆ is_eq()

bool is_eq ( ) const
inline

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

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

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

◆ is_false()

bool is_false ( ) const
inline

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

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

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

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

◆ is_fpa()

bool is_fpa ( ) const
inline

Return true if this is a FloatingPoint expression. .

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

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

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

◆ is_implies()

bool is_implies ( ) const
inline

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

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

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

Referenced by z3::abs().

◆ is_ite()

bool is_ite ( ) const
inline

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

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

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

◆ is_not()

bool is_not ( ) const
inline

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

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

809 { return kind() == Z3_NUMERAL_AST; }

Referenced by 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 816 of file z3++.h.

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

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

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

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

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

Referenced by expr::get_numeral_int64().

◆ is_numeral_u()

bool is_numeral_u ( unsigned &  i) const
inline

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

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

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

Referenced by expr::get_numeral_uint64().

◆ is_or()

bool is_or ( ) const
inline

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

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

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

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

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

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

◆ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

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

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

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

◆ is_true()

bool is_true ( ) const
inline

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

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

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

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

◆ is_xor()

bool is_xor ( ) const
inline

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

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

◆ itos()

expr itos ( ) const
inline

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

1313  {
1314  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1315  check_error();
1316  return expr(ctx(), r);
1317  }

◆ length()

expr length ( ) const
inline

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

1303  {
1304  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1305  check_error();
1306  return expr(ctx(), r);
1307  }

Referenced by expr::extract().

◆ lo()

unsigned lo ( ) const
inline

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

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

1323  {
1324  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1325  check_error();
1326  return expr(ctx(), r);
1327  }

◆ loop() [2/2]

expr loop ( unsigned  lo,
unsigned  hi 
)
inline

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

1328  {
1329  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1330  check_error();
1331  return expr(ctx(), r);
1332  }

◆ nth()

expr nth ( expr const &  index) const
inline

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

1297  {
1298  check_context(*this, index);
1299  Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1300  check_error();
1301  return expr(ctx(), r);
1302  }

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

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

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

◆ numerator()

expr numerator ( ) const
inline

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

989  {
990  assert(is_numeral());
991  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
992  check_error();
993  return expr(ctx(),r);
994  }

◆ operator Z3_app()

operator Z3_app ( ) const
inline

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

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

◆ operator=()

expr& operator= ( expr const &  n)
inline

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

742 { return static_cast<expr&>(ast::operator=(n)); }

◆ operator[]() [1/2]

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

index operator defined on arrays and sequences.

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

1337  {
1338  assert(is_array() || is_seq());
1339  if (is_array()) {
1340  return select(*this, index);
1341  }
1342  return nth(index);
1343  }

◆ operator[]() [2/2]

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

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

1345  {
1346  return select(*this, index);
1347  }

◆ repeat()

expr repeat ( unsigned  i)
inline

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

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

1274  {
1275  check_context(*this, src); check_context(src, dst);
1276  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1277  check_error();
1278  return expr(ctx(), r);
1279  }

◆ rotate_left()

expr rotate_left ( unsigned  i)
inline

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

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

◆ rotate_right()

expr rotate_right ( unsigned  i)
inline

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

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

◆ simplify() [1/2]

expr simplify ( ) const
inline

Return a simplified version of this expression.

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

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

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

◆ stoi()

expr stoi ( ) const
inline

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

1308  {
1309  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1310  check_error();
1311  return expr(ctx(), r);
1312  }

◆ substitute() [1/2]

expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

3558  {
3559  array<Z3_ast> _dst(dst.size());
3560  for (unsigned i = 0; i < dst.size(); ++i) {
3561  _dst[i] = dst[i];
3562  }
3563  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
3564  check_error();
3565  return expr(ctx(), r);
3566  }

◆ substitute() [2/2]

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

Apply substitution. Replace src expressions by dst.

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

3545  {
3546  assert(src.size() == dst.size());
3547  array<Z3_ast> _src(src.size());
3548  array<Z3_ast> _dst(dst.size());
3549  for (unsigned i = 0; i < src.size(); ++i) {
3550  _src[i] = src[i];
3551  _dst[i] = dst[i];
3552  }
3553  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
3554  check_error();
3555  return expr(ctx(), r);
3556  }

◆ unit()

expr unit ( ) const
inline

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

1280  {
1281  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1282  check_error();
1283  return expr(ctx(), r);
1284  }

Friends And Related Function Documentation

◆ abs

expr abs ( expr const &  a)
friend

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

1722  {
1723  Z3_ast r;
1724  if (a.is_int()) {
1725  expr zero = a.ctx().int_val(0);
1726  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1727  }
1728  else if (a.is_real()) {
1729  expr zero = a.ctx().real_val(0);
1730  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1731  }
1732  else {
1733  r = Z3_mk_fpa_abs(a.ctx(), a);
1734  }
1735  a.check_error();
1736  return expr(a.ctx(), r);
1737  }

◆ atleast

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

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

2087  {
2088  assert(es.size() > 0);
2089  context& ctx = es[0].ctx();
2090  array<Z3_ast> _es(es);
2091  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2092  ctx.check_error();
2093  return expr(ctx, r);
2094  }

◆ atmost

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

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

2079  {
2080  assert(es.size() > 0);
2081  context& ctx = es[0].ctx();
2082  array<Z3_ast> _es(es);
2083  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2084  ctx.check_error();
2085  return expr(ctx, r);
2086  }

◆ bv2int

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

bit-vector and integer conversions.

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

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

1894  {
1895  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);
1896  }

◆ bvadd_no_underflow

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

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

1897  {
1898  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1899  }

◆ bvmul_no_overflow

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

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

1912  {
1913  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);
1914  }

◆ bvmul_no_underflow

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

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

1915  {
1916  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1917  }

◆ bvneg_no_overflow

expr bvneg_no_overflow ( expr const &  a)
friend

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

1909  {
1910  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
1911  }

◆ bvsdiv_no_overflow

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

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

1906  {
1907  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1908  }

◆ bvsub_no_overflow

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

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

1900  {
1901  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1902  }

◆ bvsub_no_underflow

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

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

1903  {
1904  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);
1905  }

◆ concat [1/2]

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

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

2113  {
2114  check_context(a, b);
2115  Z3_ast r;
2116  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2117  Z3_ast _args[2] = { a, b };
2118  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2119  }
2120  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2121  Z3_ast _args[2] = { a, b };
2122  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2123  }
2124  else {
2125  r = Z3_mk_concat(a.ctx(), a, b);
2126  }
2127  a.ctx().check_error();
2128  return expr(a.ctx(), r);
2129  }

◆ concat [2/2]

expr concat ( expr_vector const &  args)
friend

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

2131  {
2132  Z3_ast r;
2133  assert(args.size() > 0);
2134  if (args.size() == 1) {
2135  return args[0];
2136  }
2137  context& ctx = args[0].ctx();
2138  array<Z3_ast> _args(args);
2139  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
2140  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2141  }
2142  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
2143  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2144  }
2145  else {
2146  r = _args[args.size()-1];
2147  for (unsigned i = args.size()-1; i > 0; ) {
2148  --i;
2149  r = Z3_mk_concat(ctx, _args[i], r);
2150  ctx.check_error();
2151  }
2152  }
2153  ctx.check_error();
2154  return expr(ctx, r);
2155  }

◆ distinct

expr distinct ( expr_vector const &  args)
friend

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

2104  {
2105  assert(args.size() > 0);
2106  context& ctx = args[0].ctx();
2107  array<Z3_ast> _args(args);
2108  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2109  ctx.check_error();
2110  return expr(ctx, r);
2111  }

◆ fma

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

FloatingPoint fused multiply-add.

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

1747  {
1748  check_context(a, b); check_context(a, c); check_context(a, rm);
1749  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1750  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
1751  a.check_error();
1752  return expr(a.ctx(), r);
1753  }

◆ implies [1/3]

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

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

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

◆ implies [2/3]

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

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

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

◆ implies [3/3]

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

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

1377  {
1378  assert(a.is_bool() && b.is_bool());
1379  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1380  }

◆ int2bv

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

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

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

1425 { _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 1761 of file z3++.h.

1761  {
1762  check_context(c, t); check_context(c, e);
1763  assert(c.is_bool());
1764  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1765  c.check_error();
1766  return expr(c.ctx(), r);
1767  }

◆ max

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

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

1707  {
1708  check_context(a, b);
1709  Z3_ast r;
1710  if (a.is_arith()) {
1711  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1712  }
1713  else if (a.is_bv()) {
1714  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1715  }
1716  else {
1717  assert(a.is_fpa());
1718  r = Z3_mk_fpa_max(a.ctx(), a, b);
1719  }
1720  return expr(a.ctx(), r);
1721  }

◆ min

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

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

1692  {
1693  check_context(a, b);
1694  Z3_ast r;
1695  if (a.is_arith()) {
1696  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1697  }
1698  else if (a.is_bv()) {
1699  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1700  }
1701  else {
1702  assert(a.is_fpa());
1703  r = Z3_mk_fpa_min(a.ctx(), a, b);
1704  }
1705  return expr(a.ctx(), r);
1706  }

◆ mk_and

expr mk_and ( expr_vector const &  args)
friend

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

2163  {
2164  array<Z3_ast> _args(args);
2165  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2166  args.check_error();
2167  return expr(args.ctx(), r);
2168  }

◆ mk_or

expr mk_or ( expr_vector const &  args)
friend

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

2157  {
2158  array<Z3_ast> _args(args);
2159  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2160  args.check_error();
2161  return expr(args.ctx(), r);
2162  }

◆ mod [1/3]

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

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

1389  {
1390  if (a.is_bv()) {
1391  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1392  }
1393  else {
1394  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1395  }
1396  }

◆ mod [2/3]

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

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

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

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

◆ nand

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

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

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

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

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

1463  {
1464  check_context(a, b);
1465  Z3_ast args[2] = { a, b };
1466  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1467  a.check_error();
1468  return expr(a.ctx(), r);
1469  }

◆ operator!= [2/3]

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

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

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

◆ operator!= [3/3]

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

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

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

◆ operator& [1/3]

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

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

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

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

◆ operator& [3/3]

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

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

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

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

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

1429  {
1430  check_context(a, b);
1431  assert(a.is_bool() && b.is_bool());
1432  Z3_ast args[2] = { a, b };
1433  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1434  a.check_error();
1435  return expr(a.ctx(), r);
1436  }

◆ operator* [1/3]

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

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

1503  {
1504  check_context(a, b);
1505  Z3_ast r = 0;
1506  if (a.is_arith() && b.is_arith()) {
1507  Z3_ast args[2] = { a, b };
1508  r = Z3_mk_mul(a.ctx(), 2, args);
1509  }
1510  else if (a.is_bv() && b.is_bv()) {
1511  r = Z3_mk_bvmul(a.ctx(), a, b);
1512  }
1513  else if (a.is_fpa() && b.is_fpa()) {
1514  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1515  }
1516  else {
1517  // operator is not supported by given arguments.
1518  assert(false);
1519  }
1520  a.check_error();
1521  return expr(a.ctx(), r);
1522  }

◆ operator* [2/3]

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

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

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

◆ operator* [3/3]

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

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

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

1473  {
1474  check_context(a, b);
1475  Z3_ast r = 0;
1476  if (a.is_arith() && b.is_arith()) {
1477  Z3_ast args[2] = { a, b };
1478  r = Z3_mk_add(a.ctx(), 2, args);
1479  }
1480  else if (a.is_bv() && b.is_bv()) {
1481  r = Z3_mk_bvadd(a.ctx(), a, b);
1482  }
1483  else if (a.is_seq() && b.is_seq()) {
1484  return concat(a, b);
1485  }
1486  else if (a.is_re() && b.is_re()) {
1487  Z3_ast _args[2] = { a, b };
1488  r = Z3_mk_re_union(a.ctx(), 2, _args);
1489  }
1490  else if (a.is_fpa() && b.is_fpa()) {
1491  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1492  }
1493  else {
1494  // operator is not supported by given arguments.
1495  assert(false);
1496  }
1497  a.check_error();
1498  return expr(a.ctx(), r);
1499  }

◆ operator+ [2/3]

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

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

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

◆ operator+ [3/3]

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

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

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

◆ operator- [1/4]

expr operator- ( expr const &  a)
friend

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

1566  {
1567  Z3_ast r = 0;
1568  if (a.is_arith()) {
1569  r = Z3_mk_unary_minus(a.ctx(), a);
1570  }
1571  else if (a.is_bv()) {
1572  r = Z3_mk_bvneg(a.ctx(), a);
1573  }
1574  else if (a.is_fpa()) {
1575  r = Z3_mk_fpa_neg(a.ctx(), a);
1576  }
1577  else {
1578  // operator is not supported by given arguments.
1579  assert(false);
1580  }
1581  a.check_error();
1582  return expr(a.ctx(), r);
1583  }

◆ operator- [2/4]

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

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

1585  {
1586  check_context(a, b);
1587  Z3_ast r = 0;
1588  if (a.is_arith() && b.is_arith()) {
1589  Z3_ast args[2] = { a, b };
1590  r = Z3_mk_sub(a.ctx(), 2, args);
1591  }
1592  else if (a.is_bv() && b.is_bv()) {
1593  r = Z3_mk_bvsub(a.ctx(), a, b);
1594  }
1595  else if (a.is_fpa() && b.is_fpa()) {
1596  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1597  }
1598  else {
1599  // operator is not supported by given arguments.
1600  assert(false);
1601  }
1602  a.check_error();
1603  return expr(a.ctx(), r);
1604  }

◆ operator- [3/4]

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

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

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

◆ operator- [4/4]

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

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

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

1544  {
1545  check_context(a, b);
1546  Z3_ast r = 0;
1547  if (a.is_arith() && b.is_arith()) {
1548  r = Z3_mk_div(a.ctx(), a, b);
1549  }
1550  else if (a.is_bv() && b.is_bv()) {
1551  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1552  }
1553  else if (a.is_fpa() && b.is_fpa()) {
1554  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1555  }
1556  else {
1557  // operator is not supported by given arguments.
1558  assert(false);
1559  }
1560  a.check_error();
1561  return expr(a.ctx(), r);
1562  }

◆ operator/ [2/3]

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

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

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

◆ operator/ [3/3]

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

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

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

1633  {
1634  check_context(a, b);
1635  Z3_ast r = 0;
1636  if (a.is_arith() && b.is_arith()) {
1637  r = Z3_mk_lt(a.ctx(), a, b);
1638  }
1639  else if (a.is_bv() && b.is_bv()) {
1640  r = Z3_mk_bvslt(a.ctx(), a, b);
1641  }
1642  else if (a.is_fpa() && b.is_fpa()) {
1643  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1644  }
1645  else {
1646  // operator is not supported by given arguments.
1647  assert(false);
1648  }
1649  a.check_error();
1650  return expr(a.ctx(), r);
1651  }

◆ operator< [2/3]

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

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

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

◆ operator< [3/3]

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

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

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

1608  {
1609  check_context(a, b);
1610  Z3_ast r = 0;
1611  if (a.is_arith() && b.is_arith()) {
1612  r = Z3_mk_le(a.ctx(), a, b);
1613  }
1614  else if (a.is_bv() && b.is_bv()) {
1615  r = Z3_mk_bvsle(a.ctx(), a, b);
1616  }
1617  else if (a.is_fpa() && b.is_fpa()) {
1618  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1619  }
1620  else {
1621  // operator is not supported by given arguments.
1622  assert(false);
1623  }
1624  a.check_error();
1625  return expr(a.ctx(), r);
1626  }

◆ operator<= [2/3]

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

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

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

◆ operator<= [3/3]

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

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

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

1454  {
1455  check_context(a, b);
1456  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1457  a.check_error();
1458  return expr(a.ctx(), r);
1459  }

◆ operator== [2/3]

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

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

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

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

1655  {
1656  check_context(a, b);
1657  Z3_ast r = 0;
1658  if (a.is_arith() && b.is_arith()) {
1659  r = Z3_mk_gt(a.ctx(), a, b);
1660  }
1661  else if (a.is_bv() && b.is_bv()) {
1662  r = Z3_mk_bvsgt(a.ctx(), a, b);
1663  }
1664  else if (a.is_fpa() && b.is_fpa()) {
1665  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1666  }
1667  else {
1668  // operator is not supported by given arguments.
1669  assert(false);
1670  }
1671  a.check_error();
1672  return expr(a.ctx(), r);
1673  }

◆ operator> [2/3]

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

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

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

◆ operator> [3/3]

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

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

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

1527  {
1528  check_context(a, b);
1529  Z3_ast r = 0;
1530  if (a.is_arith() && b.is_arith()) {
1531  r = Z3_mk_ge(a.ctx(), a, b);
1532  }
1533  else if (a.is_bv() && b.is_bv()) {
1534  r = Z3_mk_bvsge(a.ctx(), a, b);
1535  }
1536  else {
1537  // operator is not supported by given arguments.
1538  assert(false);
1539  }
1540  a.check_error();
1541  return expr(a.ctx(), r);
1542  }

◆ operator>= [2/3]

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

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

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

◆ operator>= [3/3]

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

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

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

1681 { check_context(a, b); Z3_ast r = 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 1682 of file z3++.h.

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

◆ operator^ [3/3]

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

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

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

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

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

◆ operator| [3/3]

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

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

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

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

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

1441  {
1442  check_context(a, b);
1443  assert(a.is_bool() && b.is_bool());
1444  Z3_ast args[2] = { a, b };
1445  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1446  a.check_error();
1447  return expr(a.ctx(), r);
1448  }

◆ operator~

expr operator~ ( expr const &  a)
friend

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

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

2071  {
2072  assert(es.size() > 0);
2073  context& ctx = es[0].ctx();
2074  array<Z3_ast> _es(es);
2075  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2076  ctx.check_error();
2077  return expr(ctx, r);
2078  }

◆ pbge

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

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

2063  {
2064  assert(es.size() > 0);
2065  context& ctx = es[0].ctx();
2066  array<Z3_ast> _es(es);
2067  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2068  ctx.check_error();
2069  return expr(ctx, r);
2070  }

◆ pble

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

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

2055  {
2056  assert(es.size() > 0);
2057  context& ctx = es[0].ctx();
2058  array<Z3_ast> _es(es);
2059  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2060  ctx.check_error();
2061  return expr(ctx, r);
2062  }

◆ pw [1/3]

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

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

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

◆ pw [2/3]

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

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

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

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

◆ range

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

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

3488  {
3489  check_context(lo, hi);
3490  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3491  lo.check_error();
3492  return expr(lo.ctx(), r);
3493  }

◆ rem [1/3]

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

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

1405  {
1406  if (a.is_fpa() && b.is_fpa()) {
1407  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1408  } else {
1409  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1410  }
1411  }

◆ rem [2/3]

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

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

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

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

◆ sqrt

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

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

1738  {
1739  check_context(a, rm);
1740  assert(a.is_fpa());
1741  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1742  a.check_error();
1743  return expr(a.ctx(), r);
1744  }

◆ sum

expr sum ( expr_vector const &  args)
friend

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

2095  {
2096  assert(args.size() > 0);
2097  context& ctx = args[0].ctx();
2098  array<Z3_ast> _args(args);
2099  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2100  ctx.check_error();
2101  return expr(ctx, r);
2102  }

◆ xnor

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

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

1691 { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
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::expr::lo
unsigned lo() const
Definition: z3++.h:1257
z3::ast::kind
Z3_ast_kind kind() const
Definition: z3++.h:498
z3::sort::is_fpa
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:659
Z3_OP_XOR
@ Z3_OP_XOR
Definition: z3_api.h:1017
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::sort::is_relation
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:643
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_bvslt
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
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_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_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_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_BIN_
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1370
Z3_OP_FALSE
@ Z3_OP_FALSE
Definition: z3_api.h:1010
z3::expr::is_numeral_i
bool is_numeral_i(int &i) const
Definition: z3++.h:812
z3::sort::is_re
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:651
Z3_mk_seq_concat
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_APP_AST
@ Z3_APP_AST
Definition: z3_api.h:180
Z3_mk_gt
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
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_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_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_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_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...
Z3_get_lstring
Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the unescaped string constant stored in s.
Z3_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_mk_fpa_sqrt
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.
Z3_THROW
#define Z3_THROW(x)
Definition: z3++.h:99
z3::expr::is_numeral_u
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:813
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_OP_IMPLIES
@ Z3_OP_IMPLIES
Definition: z3_api.h:1019
z3::select
expr select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3313
z3::expr::rem
friend expr rem(expr const &a, expr const &b)
Definition: z3++.h:1405
z3::sort::is_array
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:635
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_bvmul
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
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_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::expr::hi
unsigned hi() const
Definition: z3++.h:1258
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_simplify_ex
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_mk_bvnor
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
Z3_OP_DISTINCT
@ Z3_OP_DISTINCT
Definition: z3_api.h:1012
Z3_get_numeral_string
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
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:1057
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_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::sort::is_bv
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:631
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_OP_AND
@ Z3_OP_AND
Definition: z3_api.h:1014
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_is_string
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
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_mk_concat
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
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::ast::operator=
ast & operator=(ast const &s)
Definition: z3++.h:497
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_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_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_seq_unit
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
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_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_UN_
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1417
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_bvnot
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
z3::expr::is_quantifier
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:829
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_OP_TRUE
@ Z3_OP_TRUE
Definition: z3_api.h:1009
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.
z3::expr::is_seq
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:784
Z3_OP_ITE
@ Z3_OP_ITE
Definition: z3_api.h:1013
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_get_string
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s.
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_mk_fpa_neg
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
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_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::object::m_ctx
context * m_ctx
Definition: z3++.h:405
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::ast::m_ast
Z3_ast m_ast
Definition: z3++.h:489
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::func_decl::decl_kind
Z3_decl_kind decl_kind() const
Definition: z3++.h:706
Z3_mk_bvneg
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
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::sort::is_datatype
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:639
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_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_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_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_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_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::expr::implies
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:1377
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::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:809
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_OP_EQ
@ Z3_OP_EQ
Definition: z3_api.h:1011
Z3_VAR_AST
@ Z3_VAR_AST
Definition: z3_api.h:181
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_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_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_lt
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
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_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition: z3_api.h:179
z3::expr::expr
expr(context &c)
Definition: z3++.h:739
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_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_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_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::expr::pw
friend expr pw(expr const &a, expr const &b)
Definition: z3++.h:1385
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::sort::is_finite_domain
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:655
z3::expr::is_algebraic
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:851
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:1050
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::sort::is_int
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:619
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::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:72
z3::sort::is_seq
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:647
z3::expr::concat
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:2113
Z3_is_lambda
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
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_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_is_seq_sort
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
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_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_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_bvnand
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
z3::sort::is_arith
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:627
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_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_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::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:413
Z3_simplify
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_OP_OR
@ Z3_OP_OR
Definition: z3_api.h:1015
z3::expr::mod
friend expr mod(expr const &a, expr const &b)
Definition: z3++.h:1389
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_mk_bvsub
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
z3::context::fpa_rounding_mode
sort fpa_rounding_mode()
Return a RoundingMode sort.
Definition: z3++.h:2986
z3::expr::is_array
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:772
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_bvand
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
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_mk_bvxnor
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
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::sort::is_real
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:623
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::expr::nth
expr nth(expr const &index) const
Definition: z3++.h:1297
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_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::ast::ast
ast(context &c)
Definition: z3++.h:491
z3::sort::is_bool
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:615
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_not
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
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_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_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::is_numeral_i64
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:810
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_abs
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
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_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_bvuge
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_get_numeral_double
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
Z3_get_sort
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
z3::expr::length
expr length() const
Definition: z3++.h:1303
Z3_get_quantifier_body
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
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_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_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::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:410
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:181
z3::expr::is_fpa
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:802
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_bvsgt
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
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_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::object::ctx
context & ctx() const
Definition: z3++.h:409
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_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:182
Z3_OP_NOT
@ Z3_OP_NOT
Definition: z3_api.h:1018
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_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_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::expr::is_app
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:821
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:1009
z3::expr::is_numeral_u64
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:811
z3::expr::get_sort
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:747
Z3_mk_bvor
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.