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...
 
expr substitute (func_decl_vector const &funs, expr_vector const &bodies)
 Apply function substitution by macro definitions. 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 810 of file z3++.h.

Constructor & Destructor Documentation

expr ( context c)
inline
expr ( context c,
Z3_ast  n 
)
inline

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

813 :ast(c, reinterpret_cast<Z3_ast>(n)) {}
ast(context &c)
Definition: z3++.h:554

Member Function Documentation

unsigned algebraic_i ( ) const
inline

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

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

1046  {
1047  assert(is_algebraic());
1048  unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
1049  check_error();
1050  return i;
1051  }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:928
Z3_ast m_ast
Definition: z3++.h:552
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.
expr algebraic_lower ( unsigned  precision) const
inline

Retrieve lower and upper bounds for algebraic numerals based on a decimal precision

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

1019  {
1020  assert(is_algebraic());
1021  Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
1022  check_error();
1023  return expr(ctx(), r);
1024  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:928
Z3_ast m_ast
Definition: z3++.h:552
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...
expr_vector algebraic_poly ( ) const
inline

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

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

1036  {
1037  assert(is_algebraic());
1038  Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
1039  check_error();
1040  return expr_vector(ctx(), r);
1041  }
Z3_error_code check_error() const
Definition: z3++.h:474
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
context & ctx() const
Definition: z3++.h:473
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:928
Z3_ast m_ast
Definition: z3++.h:552
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:76
expr algebraic_upper ( unsigned  precision) const
inline

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

1026  {
1027  assert(is_algebraic());
1028  Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
1029  check_error();
1030  return expr(ctx(), r);
1031  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:928
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_ast m_ast
Definition: z3++.h:552
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 1207 of file z3++.h.

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

1207 { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
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.
context & ctx() const
Definition: z3++.h:473
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 1214 of file z3++.h.

1214  {
1215  expr_vector vec(ctx());
1216  unsigned argCnt = num_args();
1217  for (unsigned i = 0; i < argCnt; i++)
1218  vec.push_back(arg(i));
1219  return vec;
1220  }
context & ctx() const
Definition: z3++.h:473
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:1199
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application...
Definition: z3++.h:1207
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:76
bool as_binary ( std::string &  s) const
inline

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

888 { if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:880
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_ast m_ast
Definition: z3++.h:552
double as_double ( ) const
inline

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

890 { double d = 0; is_numeral(d); return d; }
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:880
int64_t as_int64 ( ) const
inline

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

892 { int64_t r = 0; is_numeral_i64(r); return r; }
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:881
uint64_t as_uint64 ( ) const
inline

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

891 { uint64_t r = 0; is_numeral_u64(r); return r; }
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:882
expr at ( expr const &  index) const
inline

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

1487  {
1488  check_context(*this, index);
1489  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1490  check_error();
1491  return expr(ctx(), r);
1492  }
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...
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
iterator begin ( )
inline

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

1616 { return iterator(*this, 0); }
expr bit2bool ( unsigned  i) const
inline

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

1417 { Z3_ast r = Z3_mk_bit2bool(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:812
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.
context & ctx() const
Definition: z3++.h:473
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

1227 { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:906
Z3_lbool bool_value ( ) const
inline

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

1132  {
1133  return Z3_get_bool_value(ctx(), m_ast);
1134  }
context & ctx() const
Definition: z3++.h:473
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_ast m_ast
Definition: z3++.h:552
expr char_from_bv ( ) const
inline

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

1534  {
1535  Z3_ast r = Z3_mk_char_from_bv(ctx(), *this);
1536  check_error();
1537  return expr(ctx(), r);
1538  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv)
Create a character from a bit-vector (code point).
context & ctx() const
Definition: z3++.h:473
expr char_to_bv ( ) const
inline

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

1529  {
1530  Z3_ast r = Z3_mk_char_to_bv(ctx(), *this);
1531  check_error();
1532  return expr(ctx(), r);
1533  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch)
Create a bit-vector (code point) from character.
context & ctx() const
Definition: z3++.h:473
expr char_to_int ( ) const
inline

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

1524  {
1525  Z3_ast r = Z3_mk_char_to_int(ctx(), *this);
1526  check_error();
1527  return expr(ctx(), r);
1528  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)
Create an integer (code point) from character.
expr contains ( expr const &  s) const
inline

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

1481  {
1482  check_context(*this, s);
1483  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1484  check_error();
1485  return expr(ctx(), r);
1486  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
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 1192 of file z3++.h.

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

1192 { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
Z3_error_code check_error() const
Definition: z3++.h:474
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
context & ctx() const
Definition: z3++.h:473
expr denominator ( ) const
inline

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

1144  {
1145  assert(is_numeral());
1146  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
1147  check_error();
1148  return expr(ctx(),r);
1149  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:880
Z3_ast m_ast
Definition: z3++.h:552
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.
iterator end ( )
inline

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

1617 { return iterator(*this, is_app() ? num_args() : 0); }
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:1199
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
expr extract ( unsigned  hi,
unsigned  lo 
) const
inline

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

1416 { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:812
unsigned lo() const
Definition: z3++.h:1418
context & ctx() const
Definition: z3++.h:473
unsigned hi() const
Definition: z3++.h:1419
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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 1466 of file z3++.h.

1466  {
1467  check_context(*this, offset); check_context(offset, length);
1468  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1469  }
expr length() const
Definition: z3++.h:1499
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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.
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 1011 of file z3++.h.

1011  {
1012  assert(is_numeral() || is_algebraic());
1013  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
1014  }
context & ctx() const
Definition: z3++.h:473
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:880
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places...
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:928
Z3_ast m_ast
Definition: z3++.h:552
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 1068 of file z3++.h.

1068  {
1069  int result = 0;
1070  if (!is_numeral_i(result)) {
1071  assert(ctx().enable_exceptions());
1072  if (!ctx().enable_exceptions()) return 0;
1073  Z3_THROW(exception("numeral does not fit in machine int"));
1074  }
1075  return result;
1076  }
#define Z3_THROW(x)
Definition: z3++.h:103
context & ctx() const
Definition: z3++.h:473
bool is_numeral_i(int &i) const
Definition: z3++.h:883
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 1104 of file z3++.h.

1104  {
1105  assert(is_numeral());
1106  int64_t result = 0;
1107  if (!is_numeral_i64(result)) {
1108  assert(ctx().enable_exceptions());
1109  if (!ctx().enable_exceptions()) return 0;
1110  Z3_THROW(exception("numeral does not fit in machine int64_t"));
1111  }
1112  return result;
1113  }
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:881
#define Z3_THROW(x)
Definition: z3++.h:103
context & ctx() const
Definition: z3++.h:473
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:880
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 1087 of file z3++.h.

1087  {
1088  assert(is_numeral());
1089  unsigned result = 0;
1090  if (!is_numeral_u(result)) {
1091  assert(ctx().enable_exceptions());
1092  if (!ctx().enable_exceptions()) return 0;
1093  Z3_THROW(exception("numeral does not fit in machine uint"));
1094  }
1095  return result;
1096  }
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:884
#define Z3_THROW(x)
Definition: z3++.h:103
context & ctx() const
Definition: z3++.h:473
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:880
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 1121 of file z3++.h.

1121  {
1122  assert(is_numeral());
1123  uint64_t result = 0;
1124  if (!is_numeral_u64(result)) {
1125  assert(ctx().enable_exceptions());
1126  if (!ctx().enable_exceptions()) return 0;
1127  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
1128  }
1129  return result;
1130  }
#define Z3_THROW(x)
Definition: z3++.h:103
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:882
context & ctx() const
Definition: z3++.h:473
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:880
sort get_sort ( ) const
inline
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 1163 of file z3++.h.

1163  {
1164  assert(is_string_value());
1165  char const* s = Z3_get_string(ctx(), m_ast);
1166  check_error();
1167  return std::string(s);
1168  }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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:1156
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s. Characters outside the basic printable ASCII range are esca...
Z3_ast m_ast
Definition: z3++.h:552
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 1175 of file z3++.h.

1175  {
1176  assert(is_string_value());
1177  unsigned n = Z3_get_string_length(ctx(), m_ast);
1178  std::u32string s;
1179  s.resize(n);
1180  Z3_get_string_contents(ctx(), m_ast, n, (unsigned*)s.data());
1181  return s;
1182  }
unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s)
Retrieve the length of the unescaped string constant stored in s.
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.
context & ctx() const
Definition: z3++.h:473
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:1156
Z3_ast m_ast
Definition: z3++.h:552
unsigned hi ( ) const
inline

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

1419 { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
context & ctx() const
Definition: z3++.h:473
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
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.
unsigned id ( ) const
inline

retrieve unique identifier for expression.

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

1056 { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.
Z3_ast m_ast
Definition: z3++.h:552
bool is_algebraic ( ) const
inline

Return true if expression is an algebraic number.

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

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

928 { return Z3_is_algebraic_number(ctx(), m_ast); }
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
bool is_and ( ) const
inline

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

1296 { return is_app() && Z3_OP_AND == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:774
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
bool is_app ( ) const
inline

Return true if this expression is an application.

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

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

898 { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:568
bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

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

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

835 { return get_sort().is_arith(); }
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:691
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_array ( ) const
inline

Return true if this is a Array expression.

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

Referenced by expr::operator[]().

843 { return get_sort().is_array(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:699
bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

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

823 { return get_sort().is_bool(); }
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:679
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

Referenced by z3::bvredand(), z3::bvredor(), z3::fpa_fp(), z3::max(), z3::min(), expr::mk_from_ieee_bv(), z3::mod(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::sbv_to_fpa(), and z3::ubv_to_fpa().

839 { return get_sort().is_bv(); }
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:695
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_const ( ) const
inline

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

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

Referenced by solver::add().

902 { return is_app() && num_args() == 0; }
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition: z3++.h:1199
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

847 { return get_sort().is_datatype(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:703
expr is_digit ( ) const
inline

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

1539  {
1540  Z3_ast r = Z3_mk_char_is_digit(ctx(), *this);
1541  check_error();
1542  return expr(ctx(), r);
1543  }
Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch)
Create a check if the character is a digit.
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
bool is_distinct ( ) const
inline

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

1302 { return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:774
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
bool is_eq ( ) const
inline

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

1300 { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:774
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
bool is_exists ( ) const
inline

Return true if this expression is an existential quantifier.

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

915 { return Z3_is_quantifier_exists(ctx(), m_ast); }
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
bool is_false ( ) const
inline

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

1294 { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:774
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
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 869 of file z3++.h.

869 { return get_sort().is_finite_domain(); }
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:719
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_forall ( ) const
inline

Return true if this expression is a universal quantifier.

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

911 { return Z3_is_quantifier_forall(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:473
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
Z3_ast m_ast
Definition: z3++.h:552
bool is_fpa ( ) const
inline

Return true if this is a FloatingPoint expression. .

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

Referenced by z3::fma(), z3::fp_eq(), z3::fpa_to_fpa(), z3::fpa_to_sbv(), z3::fpa_to_ubv(), z3::max(), z3::min(), expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), expr::mk_to_ieee_bv(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::rem(), z3::round_fpa_to_closest_integer(), and z3::sqrt().

873 { return get_sort().is_fpa(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:723
bool is_implies ( ) const
inline

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

1299 { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:774
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
bool is_int ( ) const
inline

Return true if this is an integer expression.

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

Referenced by z3::abs().

827 { return get_sort().is_int(); }
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:683
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_ite ( ) const
inline

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

1301 { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:774
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
bool is_lambda ( ) const
inline

Return true if this expression is a lambda expression.

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

919 { return Z3_is_lambda(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
bool is_not ( ) const
inline

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

1295 { return is_app() && Z3_OP_NOT == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:774
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
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 880 of file z3++.h.

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

880 { return kind() == Z3_NUMERAL_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:568
bool is_numeral ( std::string &  s) const
inline

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

Referenced by expr::is_numeral().

885 { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:880
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_ast m_ast
Definition: z3++.h:552
bool is_numeral ( std::string &  s,
unsigned  precision 
) const
inline

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

Referenced by expr::is_numeral().

886 { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:880
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_ast m_ast
Definition: z3++.h:552
bool is_numeral ( double &  d) const
inline

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

Referenced by expr::is_numeral().

887 { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:880
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
Z3_ast m_ast
Definition: z3++.h:552
bool is_numeral_i ( int &  i) const
inline

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

Referenced by expr::get_numeral_int().

883 { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int...
Z3_ast m_ast
Definition: z3++.h:552
bool is_numeral_i64 ( int64_t &  i) const
inline

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

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

881 { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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_ast m_ast
Definition: z3++.h:552
bool is_numeral_u ( unsigned &  i) const
inline

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

Referenced by expr::get_numeral_uint().

884 { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int...
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
bool is_numeral_u64 ( uint64_t &  i) const
inline

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

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

882 { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int...
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
bool is_or ( ) const
inline

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

1297 { return is_app() && Z3_OP_OR == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:774
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

Referenced by expr::body().

906 { return kind() == Z3_QUANTIFIER_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:568
bool is_re ( ) const
inline

Return true if this is a regular expression.

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

Referenced by z3::operator+().

859 { return get_sort().is_re(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:715
bool is_real ( ) const
inline

Return true if this is a real expression.

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

Referenced by z3::abs().

831 { return get_sort().is_real(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:687
bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

851 { return get_sort().is_relation(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:707
bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

Referenced by z3::operator+(), and expr::operator[]().

855 { return get_sort().is_seq(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:711
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 1156 of file z3++.h.

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

1156 { return Z3_is_string(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:473
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
Z3_ast m_ast
Definition: z3++.h:552
bool is_true ( ) const
inline

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

1293 { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:774
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
bool is_var ( ) const
inline

Return true if this expression is a variable.

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

924 { return kind() == Z3_VAR_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:568
bool is_well_sorted ( ) const
inline

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

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

933 { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
bool is_xor ( ) const
inline

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

1298 { return is_app() && Z3_OP_XOR == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:774
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
expr itos ( ) const
inline

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

1509  {
1510  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1511  check_error();
1512  return expr(ctx(), r);
1513  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
expr length ( ) const
inline

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

1499  {
1500  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1501  check_error();
1502  return expr(ctx(), r);
1503  }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
unsigned lo ( ) const
inline

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

1418 { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
context & ctx() const
Definition: z3++.h:473
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:1192
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
expr loop ( unsigned  lo)
inline

create a looping regular expression.

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

1549  {
1550  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1551  check_error();
1552  return expr(ctx(), r);
1553  }
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...
expr(context &c)
Definition: z3++.h:812
unsigned lo() const
Definition: z3++.h:1418
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
expr loop ( unsigned  lo,
unsigned  hi 
)
inline

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

1554  {
1555  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1556  check_error();
1557  return expr(ctx(), r);
1558  }
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...
expr(context &c)
Definition: z3++.h:812
unsigned lo() const
Definition: z3++.h:1418
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
unsigned hi() const
Definition: z3++.h:1419
Z3_ast m_ast
Definition: z3++.h:552
expr mk_from_ieee_bv ( sort const &  s) const
inline

Convert this IEEE BV into a fpa.

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

998  {
999  assert(is_bv());
1000  Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
1001  check_error();
1002  return expr(ctx(), r);
1003  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
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.
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:839
expr mk_is_inf ( ) const
inline

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

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

938  {
939  assert(is_fpa());
940  Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast);
941  check_error();
942  return expr(ctx(), r);
943  }
expr(context &c)
Definition: z3++.h:812
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:873
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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_ast m_ast
Definition: z3++.h:552
expr mk_is_nan ( ) const
inline

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

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

948  {
949  assert(is_fpa());
950  Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast);
951  check_error();
952  return expr(ctx(), r);
953  }
expr(context &c)
Definition: z3++.h:812
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:873
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t)
Predicate indicating whether t is a NaN.
Z3_ast m_ast
Definition: z3++.h:552
expr mk_is_normal ( ) const
inline

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

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

958  {
959  assert(is_fpa());
960  Z3_ast r = Z3_mk_fpa_is_normal(ctx(), m_ast);
961  check_error();
962  return expr(ctx(), r);
963  }
expr(context &c)
Definition: z3++.h:812
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:873
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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_ast m_ast
Definition: z3++.h:552
expr mk_is_subnormal ( ) const
inline

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

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

968  {
969  assert(is_fpa());
970  Z3_ast r = Z3_mk_fpa_is_subnormal(ctx(), m_ast);
971  check_error();
972  return expr(ctx(), r);
973  }
expr(context &c)
Definition: z3++.h:812
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.
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:873
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
expr mk_is_zero ( ) const
inline

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

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

978  {
979  assert(is_fpa());
980  Z3_ast r = Z3_mk_fpa_is_zero(ctx(), m_ast);
981  check_error();
982  return expr(ctx(), r);
983  }
expr(context &c)
Definition: z3++.h:812
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...
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:873
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
expr mk_to_ieee_bv ( ) const
inline

Convert this fpa into an IEEE BV.

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

988  {
989  assert(is_fpa());
990  Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast);
991  check_error();
992  return expr(ctx(), r);
993  }
expr(context &c)
Definition: z3++.h:812
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:873
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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_ast m_ast
Definition: z3++.h:552
expr nth ( expr const &  index) const
inline

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

Referenced by expr::operator[]().

1493  {
1494  check_context(*this, index);
1495  Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1496  check_error();
1497  return expr(ctx(), r);
1498  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
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...
context & ctx() const
Definition: z3++.h:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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 1199 of file z3++.h.

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

1199 { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
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...
expr numerator ( ) const
inline

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

1136  {
1137  assert(is_numeral());
1138  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1139  check_error();
1140  return expr(ctx(),r);
1141  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:880
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
Z3_ast m_ast
Definition: z3++.h:552
operator Z3_app ( ) const
inline

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

1184 { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:898
Z3_ast m_ast
Definition: z3++.h:552
expr operator[] ( expr const &  index) const
inline

index operator defined on arrays and sequences.

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

1563  {
1564  assert(is_array() || is_seq());
1565  if (is_array()) {
1566  return select(*this, index);
1567  }
1568  return nth(index);
1569  }
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:843
expr nth(expr const &index) const
Definition: z3++.h:1493
expr select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3903
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:855
expr operator[] ( expr_vector const &  index) const
inline

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

1571  {
1572  return select(*this, index);
1573  }
expr select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3903
expr repeat ( unsigned  i) const
inline

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

1406 { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:812
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr replace ( expr const &  src,
expr const &  dst 
) const
inline

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

1470  {
1471  check_context(*this, src); check_context(src, dst);
1472  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1473  check_error();
1474  return expr(ctx(), r);
1475  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
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.
context & ctx() const
Definition: z3++.h:473
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
expr rotate_left ( unsigned  i) const
inline

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

1404 { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:812
context & ctx() const
Definition: z3++.h:473
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
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.
expr rotate_right ( unsigned  i) const
inline

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

1405 { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:812
context & ctx() const
Definition: z3++.h:473
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_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:192
expr sbvtos ( ) const
inline

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

1519  {
1520  Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this);
1521  check_error();
1522  return expr(ctx(), r);
1523  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s)
Signed bit-vector to string conversion.
expr simplify ( ) const
inline

Return a simplified version of this expression.

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

1578 { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_ast m_ast
Definition: z3++.h:552
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 1582 of file z3++.h.

1582 { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
expr stoi ( ) const
inline

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

1504  {
1505  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1506  check_error();
1507  return expr(ctx(), r);
1508  }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
expr substitute ( expr_vector const &  src,
expr_vector const &  dst 
)
inline

Apply substitution. Replace src expressions by dst.

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

4178  {
4179  assert(src.size() == dst.size());
4180  array<Z3_ast> _src(src.size());
4181  array<Z3_ast> _dst(dst.size());
4182  for (unsigned i = 0; i < src.size(); ++i) {
4183  _src[i] = src[i];
4184  _dst[i] = dst[i];
4185  }
4186  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
4187  check_error();
4188  return expr(ctx(), r);
4189  }
expr(context &c)
Definition: z3++.h:812
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. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

4191  {
4192  array<Z3_ast> _dst(dst.size());
4193  for (unsigned i = 0; i < dst.size(); ++i) {
4194  _dst[i] = dst[i];
4195  }
4196  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
4197  check_error();
4198  return expr(ctx(), r);
4199  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the variables in a with the expressions in to. For every i smaller than num_exprs...
Z3_ast m_ast
Definition: z3++.h:552
expr substitute ( func_decl_vector const &  funs,
expr_vector const &  bodies 
)
inline

Apply function substitution by macro definitions.

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

4201  {
4202  array<Z3_ast> _dst(dst.size());
4203  array<Z3_func_decl> _funs(funs.size());
4204  if (dst.size() != funs.size()) {
4205  Z3_THROW(exception("length of argument lists don't align"));
4206  return expr(ctx(), nullptr);
4207  }
4208  for (unsigned i = 0; i < dst.size(); ++i) {
4209  _dst[i] = dst[i];
4210  _funs[i] = funs[i];
4211  }
4212  Z3_ast r = Z3_substitute_funs(ctx(), m_ast, dst.size(), _funs.ptr(), _dst.ptr());
4213  check_error();
4214  return expr(ctx(), r);
4215  }
#define Z3_THROW(x)
Definition: z3++.h:103
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast m_ast
Definition: z3++.h:552
Z3_ast Z3_API Z3_substitute_funs(Z3_context c, Z3_ast a, unsigned num_funs, Z3_func_decl const from[], Z3_ast const to[])
Substitute functions in from with new expressions in to.
expr ubvtos ( ) const
inline

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

1514  {
1515  Z3_ast r = Z3_mk_ubv_to_str(ctx(), *this);
1516  check_error();
1517  return expr(ctx(), r);
1518  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s)
Unsigned bit-vector to string conversion.
expr unit ( ) const
inline

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

1476  {
1477  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1478  check_error();
1479  return expr(ctx(), r);
1480  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.

Friends And Related Function Documentation

expr abs ( expr const &  a)
friend

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

1994  {
1995  Z3_ast r;
1996  if (a.is_int()) {
1997  expr zero = a.ctx().int_val(0);
1998  expr ge = a >= zero;
1999  expr na = -a;
2000  r = Z3_mk_ite(a.ctx(), ge, a, na);
2001  }
2002  else if (a.is_real()) {
2003  expr zero = a.ctx().real_val(0);
2004  expr ge = a >= zero;
2005  expr na = -a;
2006  r = Z3_mk_ite(a.ctx(), ge, a, na);
2007  }
2008  else {
2009  r = Z3_mk_fpa_abs(a.ctx(), a);
2010  }
2011  a.check_error();
2012  return expr(a.ctx(), r);
2013  }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
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).
expr atleast ( expr_vector const &  es,
unsigned  bound 
)
friend

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

2429  {
2430  assert(es.size() > 0);
2431  context& ctx = es[0u].ctx();
2432  array<Z3_ast> _es(es);
2433  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2434  ctx.check_error();
2435  return expr(ctx, r);
2436  }
expr(context &c)
Definition: z3++.h:812
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
expr atmost ( expr_vector const &  es,
unsigned  bound 
)
friend

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

2421  {
2422  assert(es.size() > 0);
2423  context& ctx = es[0u].ctx();
2424  array<Z3_ast> _es(es);
2425  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2426  ctx.check_error();
2427  return expr(ctx, r);
2428  }
expr(context &c)
Definition: z3++.h:812
context & ctx() const
Definition: z3++.h:473
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
expr bv2int ( expr const &  a,
bool  is_signed 
)
friend

bit-vector and integer conversions.

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

2232 { Z3_ast r = Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error(); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:812
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...
expr bvadd_no_overflow ( expr const &  a,
expr const &  b,
bool  is_signed 
)
friend

bit-vector overflow/underflow checks

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

2238  {
2239  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);
2240  }
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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.
expr bvadd_no_underflow ( expr const &  a,
expr const &  b 
)
friend

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

2241  {
2242  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2243  }
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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...
expr bvmul_no_overflow ( expr const &  a,
expr const &  b,
bool  is_signed 
)
friend

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

2256  {
2257  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);
2258  }
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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...
expr bvmul_no_underflow ( expr const &  a,
expr const &  b 
)
friend

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

2259  {
2260  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2261  }
expr(context &c)
Definition: z3++.h:812
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...
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
expr bvneg_no_overflow ( expr const &  a)
friend

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

2253  {
2254  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2255  }
expr(context &c)
Definition: z3++.h:812
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...
expr bvredand ( expr const &  a)
friend

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

1988  {
1989  assert(a.is_bv());
1990  Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
1991  a.check_error();
1992  return expr(a.ctx(), r);
1993  }
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
expr(context &c)
Definition: z3++.h:812
expr bvredor ( expr const &  a)
friend

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

1982  {
1983  assert(a.is_bv());
1984  Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1985  a.check_error();
1986  return expr(a.ctx(), r);
1987  }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
expr bvsdiv_no_overflow ( expr const &  a,
expr const &  b 
)
friend

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

2250  {
2251  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2252  }
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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...
expr bvsub_no_overflow ( expr const &  a,
expr const &  b 
)
friend

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

2244  {
2245  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2246  }
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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...
expr bvsub_no_underflow ( expr const &  a,
expr const &  b,
bool  is_signed 
)
friend

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

2247  {
2248  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);
2249  }
expr(context &c)
Definition: z3++.h:812
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...
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
expr concat ( expr const &  a,
expr const &  b 
)
friend

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

2455  {
2456  check_context(a, b);
2457  Z3_ast r;
2458  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2459  Z3_ast _args[2] = { a, b };
2460  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2461  }
2462  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2463  Z3_ast _args[2] = { a, b };
2464  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2465  }
2466  else {
2467  r = Z3_mk_concat(a.ctx(), a, b);
2468  }
2469  a.ctx().check_error();
2470  return expr(a.ctx(), r);
2471  }
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
expr concat ( expr_vector const &  args)
friend

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

2473  {
2474  Z3_ast r;
2475  assert(args.size() > 0);
2476  if (args.size() == 1) {
2477  return args[0u];
2478  }
2479  context& ctx = args[0u].ctx();
2480  array<Z3_ast> _args(args);
2481  if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
2482  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2483  }
2484  else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
2485  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2486  }
2487  else {
2488  r = _args[args.size()-1];
2489  for (unsigned i = args.size()-1; i > 0; ) {
2490  --i;
2491  r = Z3_mk_concat(ctx, _args[i], r);
2492  ctx.check_error();
2493  }
2494  }
2495  ctx.check_error();
2496  return expr(ctx, r);
2497  }
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
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:1214
context & ctx() const
Definition: z3++.h:473
unsigned size() const
Definition: z3++.h:597
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:818
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
expr distinct ( expr_vector const &  args)
friend

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

2446  {
2447  assert(args.size() > 0);
2448  context& ctx = args[0u].ctx();
2449  array<Z3_ast> _args(args);
2450  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2451  ctx.check_error();
2452  return expr(ctx, r);
2453  }
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]).
expr(context &c)
Definition: z3++.h:812
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:1214
context & ctx() const
Definition: z3++.h:473
unsigned size() const
Definition: z3++.h:597
expr fma ( expr const &  a,
expr const &  b,
expr const &  c,
expr const &  rm 
)
friend

FloatingPoint fused multiply-add.

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

2030  {
2031  check_context(a, b); check_context(a, c); check_context(a, rm);
2032  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2033  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
2034  a.check_error();
2035  return expr(a.ctx(), r);
2036  }
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.
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
expr fp_eq ( expr const &  a,
expr const &  b 
)
friend

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

2021  {
2022  check_context(a, b);
2023  assert(a.is_fpa());
2024  Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
2025  a.check_error();
2026  return expr(a.ctx(), r);
2027  }
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.
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 2038 of file z3++.h.

2038  {
2039  check_context(sgn, exp); check_context(exp, sig);
2040  assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2041  Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
2042  sgn.check_error();
2043  return expr(sgn.ctx(), r);
2044  }
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.
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
expr fpa_to_fpa ( expr const &  t,
sort  s 
)
friend

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

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

2074  {
2075  assert(t.is_fpa());
2076  Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2077  t.check_error();
2078  return expr(t.ctx(), r);
2079  }
expr(context &c)
Definition: z3++.h:812
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.
expr fpa_to_sbv ( expr const &  t,
unsigned  sz 
)
friend

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

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

2046  {
2047  assert(t.is_fpa());
2048  Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2049  t.check_error();
2050  return expr(t.ctx(), r);
2051  }
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.
expr(context &c)
Definition: z3++.h:812
expr fpa_to_ubv ( expr const &  t,
unsigned  sz 
)
friend

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

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

2053  {
2054  assert(t.is_fpa());
2055  Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2056  t.check_error();
2057  return expr(t.ctx(), r);
2058  }
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.
expr(context &c)
Definition: z3++.h:812
expr implies ( expr const &  a,
expr const &  b 
)
friend

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

1628  {
1629  assert(a.is_bool() && b.is_bool());
1630  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1631  }
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1621
expr implies ( expr const &  a,
bool  b 
)
friend

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

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

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

1633 { return implies(b.ctx().bool_val(a), b); }
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:1628
expr int2bv ( unsigned  n,
expr const &  a 
)
friend

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

2233 { Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:812
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.
expr is_int ( expr const &  e)
friend

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

1676 { _Z3_MK_UN_(e, Z3_mk_is_int); }
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1668
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 2093 of file z3++.h.

2093  {
2094  check_context(c, t); check_context(c, e);
2095  assert(c.is_bool());
2096  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
2097  c.check_error();
2098  return expr(c.ctx(), r);
2099  }
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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).
expr max ( expr const &  a,
expr const &  b 
)
friend

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

1966  {
1967  check_context(a, b);
1968  Z3_ast r;
1969  if (a.is_arith()) {
1970  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1971  }
1972  else if (a.is_bv()) {
1973  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1974  }
1975  else {
1976  assert(a.is_fpa());
1977  r = Z3_mk_fpa_max(a.ctx(), a, b);
1978  }
1979  a.check_error();
1980  return expr(a.ctx(), r);
1981  }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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).
expr min ( expr const &  a,
expr const &  b 
)
friend

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

1950  {
1951  check_context(a, b);
1952  Z3_ast r;
1953  if (a.is_arith()) {
1954  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1955  }
1956  else if (a.is_bv()) {
1957  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1958  }
1959  else {
1960  assert(a.is_fpa());
1961  r = Z3_mk_fpa_min(a.ctx(), a, b);
1962  }
1963  a.check_error();
1964  return expr(a.ctx(), r);
1965  }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
expr mk_and ( expr_vector const &  args)
friend

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

2505  {
2506  array<Z3_ast> _args(args);
2507  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2508  args.check_error();
2509  return expr(args.ctx(), r);
2510  }
expr(context &c)
Definition: z3++.h:812
Z3_error_code check_error() const
Definition: z3++.h:474
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:1214
context & ctx() const
Definition: z3++.h:473
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].
expr mk_or ( expr_vector const &  args)
friend

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

2499  {
2500  array<Z3_ast> _args(args);
2501  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2502  args.check_error();
2503  return expr(args.ctx(), r);
2504  }
expr(context &c)
Definition: z3++.h:812
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_error_code check_error() const
Definition: z3++.h:474
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:1214
context & ctx() const
Definition: z3++.h:473
expr mk_xor ( expr_vector const &  args)
friend

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

2511  {
2512  if (args.empty())
2513  return args.ctx().bool_val(false);
2514  expr r = args[0u];
2515  for (unsigned i = 1; i < args.size(); ++i)
2516  r = r ^ args[i];
2517  return r;
2518  }
expr(context &c)
Definition: z3++.h:812
bool empty() const
Definition: z3++.h:603
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:1214
context & ctx() const
Definition: z3++.h:473
unsigned size() const
Definition: z3++.h:597
expr bool_val(bool b)
Definition: z3++.h:3740
expr mod ( expr const &  a,
expr const &  b 
)
friend

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

1640  {
1641  if (a.is_bv()) {
1642  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1643  }
1644  else {
1645  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1646  }
1647  }
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1621
expr mod ( expr const &  a,
int  b 
)
friend

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

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

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

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

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

1947 { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
expr nor ( expr const &  a,
expr const &  b 
)
friend

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

1948 { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
expr operator! ( expr const &  a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

1674 { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1668
expr operator!= ( expr const &  a,
expr const &  b 
)
friend

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

1716  {
1717  check_context(a, b);
1718  Z3_ast args[2] = { a, b };
1719  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1720  a.check_error();
1721  return expr(a.ctx(), r);
1722  }
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]).
expr(context &c)
Definition: z3++.h:812
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:1214
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
expr operator!= ( expr const &  a,
int  b 
)
friend

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

1723 { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a != a.ctx().num_val(b, a.get_sort()); }
expr operator!= ( int  a,
expr const &  b 
)
friend

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

1724 { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) != b; }
expr operator& ( expr const &  a,
expr const &  b 
)
friend

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

1935 { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
expr operator& ( expr const &  a,
int  b 
)
friend

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

1936 { return a & a.ctx().num_val(b, a.get_sort()); }
expr operator& ( int  a,
expr const &  b 
)
friend

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

1937 { return b.ctx().num_val(a, b.get_sort()) & b; }
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 1680 of file z3++.h.

1680  {
1681  check_context(a, b);
1682  assert(a.is_bool() && b.is_bool());
1683  Z3_ast args[2] = { a, b };
1684  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1685  a.check_error();
1686  return expr(a.ctx(), r);
1687  }
expr(context &c)
Definition: z3++.h:812
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:1214
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].
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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 1689 of file z3++.h.

1689 { return a && a.ctx().bool_val(b); }
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 1690 of file z3++.h.

1690 { return b.ctx().bool_val(a) && b; }
expr operator* ( expr const &  a,
expr const &  b 
)
friend

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

1758  {
1759  check_context(a, b);
1760  Z3_ast r = 0;
1761  if (a.is_arith() && b.is_arith()) {
1762  Z3_ast args[2] = { a, b };
1763  r = Z3_mk_mul(a.ctx(), 2, args);
1764  }
1765  else if (a.is_bv() && b.is_bv()) {
1766  r = Z3_mk_bvmul(a.ctx(), a, b);
1767  }
1768  else if (a.is_fpa() && b.is_fpa()) {
1769  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1770  }
1771  else {
1772  // operator is not supported by given arguments.
1773  assert(false);
1774  }
1775  a.check_error();
1776  return expr(a.ctx(), r);
1777  }
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].
expr(context &c)
Definition: z3++.h:812
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:1214
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
expr operator* ( expr const &  a,
int  b 
)
friend

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

1778 { return a * a.ctx().num_val(b, a.get_sort()); }
expr operator* ( int  a,
expr const &  b 
)
friend

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

1779 { return b.ctx().num_val(a, b.get_sort()) * b; }
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_add(a.ctx(), 2, args);
1734  }
1735  else if (a.is_bv() && b.is_bv()) {
1736  r = Z3_mk_bvadd(a.ctx(), a, b);
1737  }
1738  else if (a.is_seq() && b.is_seq()) {
1739  return concat(a, b);
1740  }
1741  else if (a.is_re() && b.is_re()) {
1742  Z3_ast _args[2] = { a, b };
1743  r = Z3_mk_re_union(a.ctx(), 2, _args);
1744  }
1745  else if (a.is_fpa() && b.is_fpa()) {
1746  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1747  }
1748  else {
1749  // operator is not supported by given arguments.
1750  assert(false);
1751  }
1752  a.check_error();
1753  return expr(a.ctx(), r);
1754  }
expr(context &c)
Definition: z3++.h:812
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:2455
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].
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:1214
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
expr operator+ ( expr const &  a,
int  b 
)
friend

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

1755 { return a + a.ctx().num_val(b, a.get_sort()); }
expr operator+ ( int  a,
expr const &  b 
)
friend

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

1756 { return b.ctx().num_val(a, b.get_sort()) + b; }
expr operator- ( expr const &  a)
friend

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

1824  {
1825  Z3_ast r = 0;
1826  if (a.is_arith()) {
1827  r = Z3_mk_unary_minus(a.ctx(), a);
1828  }
1829  else if (a.is_bv()) {
1830  r = Z3_mk_bvneg(a.ctx(), a);
1831  }
1832  else if (a.is_fpa()) {
1833  r = Z3_mk_fpa_neg(a.ctx(), a);
1834  }
1835  else {
1836  // operator is not supported by given arguments.
1837  assert(false);
1838  }
1839  a.check_error();
1840  return expr(a.ctx(), r);
1841  }
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
expr operator- ( expr const &  a,
expr const &  b 
)
friend

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

1843  {
1844  check_context(a, b);
1845  Z3_ast r = 0;
1846  if (a.is_arith() && b.is_arith()) {
1847  Z3_ast args[2] = { a, b };
1848  r = Z3_mk_sub(a.ctx(), 2, args);
1849  }
1850  else if (a.is_bv() && b.is_bv()) {
1851  r = Z3_mk_bvsub(a.ctx(), a, b);
1852  }
1853  else if (a.is_fpa() && b.is_fpa()) {
1854  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1855  }
1856  else {
1857  // operator is not supported by given arguments.
1858  assert(false);
1859  }
1860  a.check_error();
1861  return expr(a.ctx(), r);
1862  }
expr(context &c)
Definition: z3++.h:812
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:1214
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
expr operator- ( expr const &  a,
int  b 
)
friend

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

1863 { return a - a.ctx().num_val(b, a.get_sort()); }
expr operator- ( int  a,
expr const &  b 
)
friend

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

1864 { return b.ctx().num_val(a, b.get_sort()) - b; }
expr operator/ ( expr const &  a,
expr const &  b 
)
friend

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

1802  {
1803  check_context(a, b);
1804  Z3_ast r = 0;
1805  if (a.is_arith() && b.is_arith()) {
1806  r = Z3_mk_div(a.ctx(), a, b);
1807  }
1808  else if (a.is_bv() && b.is_bv()) {
1809  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1810  }
1811  else if (a.is_fpa() && b.is_fpa()) {
1812  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1813  }
1814  else {
1815  // operator is not supported by given arguments.
1816  assert(false);
1817  }
1818  a.check_error();
1819  return expr(a.ctx(), r);
1820  }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
expr operator/ ( expr const &  a,
int  b 
)
friend

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

1821 { return a / a.ctx().num_val(b, a.get_sort()); }
expr operator/ ( int  a,
expr const &  b 
)
friend

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

1822 { return b.ctx().num_val(a, b.get_sort()) / b; }
expr operator< ( expr const &  a,
expr const &  b 
)
friend

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

1891  {
1892  check_context(a, b);
1893  Z3_ast r = 0;
1894  if (a.is_arith() && b.is_arith()) {
1895  r = Z3_mk_lt(a.ctx(), a, b);
1896  }
1897  else if (a.is_bv() && b.is_bv()) {
1898  r = Z3_mk_bvslt(a.ctx(), a, b);
1899  }
1900  else if (a.is_fpa() && b.is_fpa()) {
1901  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1902  }
1903  else {
1904  // operator is not supported by given arguments.
1905  assert(false);
1906  }
1907  a.check_error();
1908  return expr(a.ctx(), r);
1909  }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
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()); }
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; }
expr operator<= ( expr const &  a,
expr const &  b 
)
friend

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

1866  {
1867  check_context(a, b);
1868  Z3_ast r = 0;
1869  if (a.is_arith() && b.is_arith()) {
1870  r = Z3_mk_le(a.ctx(), a, b);
1871  }
1872  else if (a.is_bv() && b.is_bv()) {
1873  r = Z3_mk_bvsle(a.ctx(), a, b);
1874  }
1875  else if (a.is_fpa() && b.is_fpa()) {
1876  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1877  }
1878  else {
1879  // operator is not supported by given arguments.
1880  assert(false);
1881  }
1882  a.check_error();
1883  return expr(a.ctx(), r);
1884  }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
expr operator<= ( expr const &  a,
int  b 
)
friend

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

1885 { return a <= a.ctx().num_val(b, a.get_sort()); }
expr operator<= ( int  a,
expr const &  b 
)
friend

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

1886 { return b.ctx().num_val(a, b.get_sort()) <= b; }
expr operator== ( expr const &  a,
expr const &  b 
)
friend

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

1705  {
1706  check_context(a, b);
1707  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1708  a.check_error();
1709  return expr(a.ctx(), r);
1710  }
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
expr operator== ( expr const &  a,
int  b 
)
friend

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

1711 { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a == a.ctx().num_val(b, a.get_sort()); }
expr operator== ( int  a,
expr const &  b 
)
friend

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

1712 { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) == b; }
expr operator> ( expr const &  a,
expr const &  b 
)
friend

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

1913  {
1914  check_context(a, b);
1915  Z3_ast r = 0;
1916  if (a.is_arith() && b.is_arith()) {
1917  r = Z3_mk_gt(a.ctx(), a, b);
1918  }
1919  else if (a.is_bv() && b.is_bv()) {
1920  r = Z3_mk_bvsgt(a.ctx(), a, b);
1921  }
1922  else if (a.is_fpa() && b.is_fpa()) {
1923  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1924  }
1925  else {
1926  // operator is not supported by given arguments.
1927  assert(false);
1928  }
1929  a.check_error();
1930  return expr(a.ctx(), r);
1931  }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
expr operator> ( expr const &  a,
int  b 
)
friend

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

1932 { return a > a.ctx().num_val(b, a.get_sort()); }
expr operator> ( int  a,
expr const &  b 
)
friend

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

1933 { return b.ctx().num_val(a, b.get_sort()) > b; }
expr operator>= ( expr const &  a,
expr const &  b 
)
friend

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

1782  {
1783  check_context(a, b);
1784  Z3_ast r = 0;
1785  if (a.is_arith() && b.is_arith()) {
1786  r = Z3_mk_ge(a.ctx(), a, b);
1787  }
1788  else if (a.is_bv() && b.is_bv()) {
1789  r = Z3_mk_bvsge(a.ctx(), a, b);
1790  }
1791  else if (a.is_fpa() && b.is_fpa()) {
1792  r = Z3_mk_fpa_geq(a.ctx(), a, b);
1793  }
1794  else {
1795  // operator is not supported by given arguments.
1796  assert(false);
1797  }
1798  a.check_error();
1799  return expr(a.ctx(), r);
1800  }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.
expr operator>= ( expr const &  a,
int  b 
)
friend

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

1888 { return a >= a.ctx().num_val(b, a.get_sort()); }
expr operator>= ( int  a,
expr const &  b 
)
friend

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

1889 { return b.ctx().num_val(a, b.get_sort()) >= b; }
expr operator^ ( expr const &  a,
expr const &  b 
)
friend

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

1939 { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
expr operator^ ( expr const &  a,
int  b 
)
friend

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

1940 { return a ^ a.ctx().num_val(b, a.get_sort()); }
expr operator^ ( int  a,
expr const &  b 
)
friend

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

1941 { return b.ctx().num_val(a, b.get_sort()) ^ b; }
expr operator| ( expr const &  a,
expr const &  b 
)
friend

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

1943 { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
expr operator| ( expr const &  a,
int  b 
)
friend

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

1944 { return a | a.ctx().num_val(b, a.get_sort()); }
expr operator| ( int  a,
expr const &  b 
)
friend

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

1945 { return b.ctx().num_val(a, b.get_sort()) | b; }
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 1692 of file z3++.h.

1692  {
1693  check_context(a, b);
1694  assert(a.is_bool() && b.is_bool());
1695  Z3_ast args[2] = { a, b };
1696  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1697  a.check_error();
1698  return expr(a.ctx(), r);
1699  }
expr(context &c)
Definition: z3++.h:812
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].
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:1214
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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 1701 of file z3++.h.

1701 { return a || a.ctx().bool_val(b); }
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 1703 of file z3++.h.

1703 { return b.ctx().bool_val(a) || b; }
expr operator~ ( expr const &  a)
friend

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

2028 { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
expr pbeq ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
friend

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

2413  {
2414  assert(es.size() > 0);
2415  context& ctx = es[0u].ctx();
2416  array<Z3_ast> _es(es);
2417  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2418  ctx.check_error();
2419  return expr(ctx, r);
2420  }
expr(context &c)
Definition: z3++.h:812
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.
context & ctx() const
Definition: z3++.h:473
expr pbge ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
friend

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

2405  {
2406  assert(es.size() > 0);
2407  context& ctx = es[0u].ctx();
2408  array<Z3_ast> _es(es);
2409  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2410  ctx.check_error();
2411  return expr(ctx, r);
2412  }
expr(context &c)
Definition: z3++.h:812
context & ctx() const
Definition: z3++.h:473
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.
expr pble ( expr_vector const &  es,
int const *  coeffs,
int  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_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2402  ctx.check_error();
2403  return expr(ctx, r);
2404  }
expr(context &c)
Definition: z3++.h:812
context & ctx() const
Definition: z3++.h:473
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.
expr pw ( expr const &  a,
expr const &  b 
)
friend

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

1636 { _Z3_MK_BIN_(a, b, Z3_mk_power); }
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1621
expr pw ( expr const &  a,
int  b 
)
friend

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

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

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

1638 { return pw(b.ctx().num_val(a, b.get_sort()), b); }
friend expr pw(expr const &a, expr const &b)
Definition: z3++.h:1636
expr range ( expr const &  lo,
expr const &  hi 
)
friend

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

4085  {
4086  check_context(lo, hi);
4087  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
4088  lo.check_error();
4089  return expr(lo.ctx(), r);
4090  }
expr(context &c)
Definition: z3++.h:812
unsigned lo() const
Definition: z3++.h:1418
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
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.
unsigned hi() const
Definition: z3++.h:1419
expr rem ( expr const &  a,
expr const &  b 
)
friend

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

1656  {
1657  if (a.is_fpa() && b.is_fpa()) {
1658  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1659  } else {
1660  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1661  }
1662  }
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1621
expr rem ( expr const &  a,
int  b 
)
friend

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

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

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

1664 { return rem(b.ctx().num_val(a, b.get_sort()), b); }
friend expr rem(expr const &a, expr const &b)
Definition: z3++.h:1656
expr round_fpa_to_closest_integer ( expr const &  t)
friend

Round a floating-point term into its closest integer.

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

2081  {
2082  assert(t.is_fpa());
2083  Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
2084  t.check_error();
2085  return expr(t.ctx(), r);
2086  }
expr(context &c)
Definition: z3++.h:812
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, again represented as a floating-point number.
expr sbv_to_fpa ( expr const &  t,
sort  s 
)
friend

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

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

2060  {
2061  assert(t.is_bv());
2062  Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2063  t.check_error();
2064  return expr(t.ctx(), r);
2065  }
expr(context &c)
Definition: z3++.h:812
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...
expr sqrt ( expr const &  a,
expr const &  rm 
)
friend

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

2014  {
2015  check_context(a, rm);
2016  assert(a.is_fpa());
2017  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
2018  a.check_error();
2019  return expr(a.ctx(), r);
2020  }
expr(context &c)
Definition: z3++.h:812
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.
expr sum ( expr_vector const &  args)
friend

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

2437  {
2438  assert(args.size() > 0);
2439  context& ctx = args[0u].ctx();
2440  array<Z3_ast> _args(args);
2441  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2442  ctx.check_error();
2443  return expr(ctx, r);
2444  }
expr(context &c)
Definition: z3++.h:812
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].
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:1214
context & ctx() const
Definition: z3++.h:473
unsigned size() const
Definition: z3++.h:597
expr ubv_to_fpa ( expr const &  t,
sort  s 
)
friend

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

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

2067  {
2068  assert(t.is_bv());
2069  Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2070  t.check_error();
2071  return expr(t.ctx(), r);
2072  }
expr(context &c)
Definition: z3++.h:812
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...
expr xnor ( expr const &  a,
expr const &  b 
)
friend

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

1949 { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:812
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477