Z3
Public Member Functions | Friends
expr Class Reference

A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More...

+ Inheritance diagram for expr:

Public Member Functions

 expr (context &c)
 
 expr (context &c, Z3_ast n)
 
 expr (expr const &n)
 
exproperator= (expr const &n)
 
sort get_sort () const
 Return the sort of this expression. More...
 
bool is_bool () const
 Return true if this is a Boolean expression. More...
 
bool is_int () const
 Return true if this is an integer expression. More...
 
bool is_real () const
 Return true if this is a real expression. More...
 
bool is_arith () const
 Return true if this is an integer or real expression. More...
 
bool is_bv () const
 Return true if this is a Bit-vector expression. More...
 
bool is_array () const
 Return true if this is a Array expression. More...
 
bool is_datatype () const
 Return true if this is a Datatype expression. More...
 
bool is_relation () const
 Return true if this is a Relation expression. More...
 
bool is_seq () const
 Return true if this is a sequence expression. More...
 
bool is_re () const
 Return true if this is a regular expression. More...
 
bool is_finite_domain () const
 Return true if this is a Finite-domain expression. More...
 
bool is_fpa () const
 Return true if this is a FloatingPoint expression. . More...
 
bool is_numeral () const
 Return true if this expression is a numeral. Specialized functions also return representations for the numerals as small integers, 64 bit integers or rational or decimal strings. More...
 
bool is_numeral_i64 (int64_t &i) const
 
bool is_numeral_u64 (uint64_t &i) const
 
bool is_numeral_i (int &i) const
 
bool is_numeral_u (unsigned &i) const
 
bool is_numeral (std::string &s) const
 
bool is_numeral (std::string &s, unsigned precision) const
 
bool is_numeral (double &d) const
 
bool is_app () const
 Return true if this expression is an application. More...
 
bool is_const () const
 Return true if this expression is a constant (i.e., an application with 0 arguments). More...
 
bool is_quantifier () const
 Return true if this expression is a quantifier. More...
 
bool is_forall () const
 Return true if this expression is a universal quantifier. More...
 
bool is_exists () const
 Return true if this expression is an existential quantifier. More...
 
bool is_lambda () const
 Return true if this expression is a lambda expression. More...
 
bool is_var () const
 Return true if this expression is a variable. More...
 
bool is_algebraic () const
 Return true if expression is an algebraic number. More...
 
bool is_well_sorted () const
 Return true if this expression is well sorted (aka type correct). More...
 
std::string get_decimal_string (int precision) const
 Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic. More...
 
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
 
std::string get_escaped_string () const
 for a string value expression return an escaped or unescaped string value. More...
 
std::string get_string () const
 
 operator Z3_app () const
 
sort fpa_rounding_mode ()
 Return a RoundingMode sort. More...
 
func_decl decl () const
 Return the declaration associated with this application. This method assumes the expression is an application. More...
 
unsigned num_args () const
 Return the number of arguments in this application. This method assumes the expression is an application. More...
 
expr arg (unsigned i) const
 Return the i-th argument of this application. This method assumes the expression is an application. More...
 
expr body () const
 Return the 'body' of this quantifier. More...
 
bool is_true () const
 
bool is_false () const
 
bool is_not () const
 
bool is_and () const
 
bool is_or () const
 
bool is_xor () const
 
bool is_implies () const
 
bool is_eq () const
 
bool is_ite () const
 
bool is_distinct () const
 
expr rotate_left (unsigned i)
 
expr rotate_right (unsigned i)
 
expr repeat (unsigned i)
 
expr extract (unsigned hi, unsigned lo) const
 
unsigned lo () const
 
unsigned hi () const
 
expr extract (expr const &offset, expr const &length) const
 sequence and regular expression operations. More...
 
expr replace (expr const &src, expr const &dst) const
 
expr unit () const
 
expr contains (expr const &s)
 
expr at (expr const &index) const
 
expr nth (expr const &index) const
 
expr length () const
 
expr stoi () const
 
expr itos () const
 
expr loop (unsigned lo)
 create a looping regular expression. More...
 
expr loop (unsigned lo, unsigned hi)
 
expr operator[] (expr const &index) const
 
expr operator[] (expr_vector const &index) const
 
expr simplify () const
 Return a simplified version of this expression. More...
 
expr simplify (params const &p) const
 Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier. More...
 
expr substitute (expr_vector const &src, expr_vector const &dst)
 Apply substitution. Replace src expressions by dst. More...
 
expr substitute (expr_vector const &dst)
 Apply substitution. Replace bound variables by expressions. More...
 
- Public Member Functions inherited from ast
 ast (context &c)
 
 ast (context &c, Z3_ast n)
 
 ast (ast const &s)
 
 ~ast ()
 
 operator Z3_ast () const
 
 operator bool () const
 
astoperator= (ast const &s)
 
Z3_ast_kind kind () const
 
unsigned hash () const
 
std::string to_string () const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
Z3_error_code check_error () const
 

Friends

expr operator! (expr const &a)
 Return an expression representing not(a). More...
 
expr operator&& (expr const &a, expr const &b)
 Return an expression representing a and b. More...
 
expr operator&& (expr const &a, bool b)
 Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant. More...
 
expr operator&& (bool a, expr const &b)
 Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant. More...
 
expr operator|| (expr const &a, expr const &b)
 Return an expression representing a or b. More...
 
expr operator|| (expr const &a, bool b)
 Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant. More...
 
expr operator|| (bool a, expr const &b)
 Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant. More...
 
expr implies (expr const &a, expr const &b)
 
expr implies (expr const &a, bool b)
 
expr implies (bool a, expr const &b)
 
expr mk_or (expr_vector const &args)
 
expr mk_and (expr_vector const &args)
 
expr ite (expr const &c, expr const &t, expr const &e)
 Create the if-then-else expression ite(c, t, e) More...
 
expr distinct (expr_vector const &args)
 
expr concat (expr const &a, expr const &b)
 
expr concat (expr_vector const &args)
 
expr operator== (expr const &a, expr const &b)
 
expr operator== (expr const &a, int b)
 
expr operator== (int a, expr const &b)
 
expr operator!= (expr const &a, expr const &b)
 
expr operator!= (expr const &a, int b)
 
expr operator!= (int a, expr const &b)
 
expr operator+ (expr const &a, expr const &b)
 
expr operator+ (expr const &a, int b)
 
expr operator+ (int a, expr const &b)
 
expr sum (expr_vector const &args)
 
expr operator* (expr const &a, expr const &b)
 
expr operator* (expr const &a, int b)
 
expr operator* (int a, expr const &b)
 
expr pw (expr const &a, expr const &b)
 
expr pw (expr const &a, int b)
 
expr pw (int a, expr const &b)
 
expr mod (expr const &a, expr const &b)
 
expr mod (expr const &a, int b)
 
expr mod (int a, expr const &b)
 
expr rem (expr const &a, expr const &b)
 
expr rem (expr const &a, int b)
 
expr rem (int a, expr const &b)
 
expr is_int (expr const &e)
 
expr operator/ (expr const &a, expr const &b)
 
expr operator/ (expr const &a, int b)
 
expr operator/ (int a, expr const &b)
 
expr operator- (expr const &a)
 
expr operator- (expr const &a, expr const &b)
 
expr operator- (expr const &a, int b)
 
expr operator- (int a, expr const &b)
 
expr operator<= (expr const &a, expr const &b)
 
expr operator<= (expr const &a, int b)
 
expr operator<= (int a, expr const &b)
 
expr operator>= (expr const &a, expr const &b)
 
expr operator>= (expr const &a, int b)
 
expr operator>= (int a, expr const &b)
 
expr operator< (expr const &a, expr const &b)
 
expr operator< (expr const &a, int b)
 
expr operator< (int a, expr const &b)
 
expr operator> (expr const &a, expr const &b)
 
expr operator> (expr const &a, int b)
 
expr operator> (int a, expr const &b)
 
expr pble (expr_vector const &es, int const *coeffs, int bound)
 
expr pbge (expr_vector const &es, int const *coeffs, int bound)
 
expr pbeq (expr_vector const &es, int const *coeffs, int bound)
 
expr atmost (expr_vector const &es, unsigned bound)
 
expr atleast (expr_vector const &es, unsigned bound)
 
expr operator& (expr const &a, expr const &b)
 
expr operator& (expr const &a, int b)
 
expr operator& (int a, expr const &b)
 
expr operator^ (expr const &a, expr const &b)
 
expr operator^ (expr const &a, int b)
 
expr operator^ (int a, expr const &b)
 
expr operator| (expr const &a, expr const &b)
 
expr operator| (expr const &a, int b)
 
expr operator| (int a, expr const &b)
 
expr nand (expr const &a, expr const &b)
 
expr nor (expr const &a, expr const &b)
 
expr xnor (expr const &a, expr const &b)
 
expr min (expr const &a, expr const &b)
 
expr max (expr const &a, expr const &b)
 
expr bv2int (expr const &a, bool is_signed)
 bit-vector and integer conversions. More...
 
expr int2bv (unsigned n, expr const &a)
 
expr bvadd_no_overflow (expr const &a, expr const &b, bool is_signed)
 bit-vector overflow/underflow checks More...
 
expr bvadd_no_underflow (expr const &a, expr const &b)
 
expr bvsub_no_overflow (expr const &a, expr const &b)
 
expr bvsub_no_underflow (expr const &a, expr const &b, bool is_signed)
 
expr bvsdiv_no_overflow (expr const &a, expr const &b)
 
expr bvneg_no_overflow (expr const &a)
 
expr bvmul_no_overflow (expr const &a, expr const &b, bool is_signed)
 
expr bvmul_no_underflow (expr const &a, expr const &b)
 
expr abs (expr const &a)
 
expr sqrt (expr const &a, expr const &rm)
 
expr operator~ (expr const &a)
 
expr fma (expr const &a, expr const &b, expr const &c)
 FloatingPoint fused multiply-add. More...
 
expr range (expr const &lo, expr const &hi)
 

Additional Inherited Members

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

Detailed Description

A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort.

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

Constructor & Destructor Documentation

◆ expr() [1/3]

expr ( context c)
inline

◆ expr() [2/3]

expr ( context c,
Z3_ast  n 
)
inline

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

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

◆ expr() [3/3]

expr ( expr const &  n)
inline

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

671 :ast(n) {}
ast(context &c)
Definition: z3++.h:488

Member Function Documentation

◆ arg()

expr arg ( unsigned  i) const
inline

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

Precondition
is_app()
i < num_args()

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

949 { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
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:406

Referenced by AstRef::__bool__().

◆ at()

expr at ( expr const &  index) const
inline

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

1175  {
1176  check_context(*this, index);
1177  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1178  check_error();
1179  return expr(ctx(), r);
1180  }
Z3_error_code check_error() const
Definition: z3++.h:407
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:669
context & ctx() const
Definition: z3++.h:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410

◆ body()

expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

956 { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
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:758

◆ bool_value()

Z3_lbool bool_value ( ) const
inline

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

878  {
879  return Z3_get_bool_value(ctx(), m_ast);
880  }
context & ctx() const
Definition: z3++.h:406
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:486

◆ contains()

expr contains ( expr const &  s)
inline

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

1169  {
1170  check_context(*this, s);
1171  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1172  check_error();
1173  return expr(ctx(), r);
1174  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.

◆ decl()

func_decl decl ( ) const
inline

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

Precondition
is_app()

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

934 { 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:407
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:406

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

◆ denominator()

expr denominator ( ) const
inline

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

890  {
891  assert(is_numeral());
892  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
893  check_error();
894  return expr(ctx(),r);
895  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
Z3_ast m_ast
Definition: z3++.h:486
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:739
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.

◆ extract() [1/2]

expr extract ( unsigned  hi,
unsigned  lo 
) const
inline

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

1140 { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
unsigned lo() const
Definition: z3++.h:1141
unsigned hi() const
Definition: z3++.h:1142
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,...

◆ extract() [2/2]

expr extract ( expr const &  offset,
expr const &  length 
) const
inline

sequence and regular expression operations.

  • is overloaded as sequence concatenation and regular expression union. concat is overloaded to handle sequences and regular expressions

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

1154  {
1155  check_context(*this, offset); check_context(offset, length);
1156  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1157  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
expr length() const
Definition: z3++.h:1187
context & ctx() const
Definition: z3++.h:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
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.

◆ fpa_rounding_mode()

sort fpa_rounding_mode ( )
inline

Return a RoundingMode sort.

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

920  {
921  assert(is_fpa());
922  Z3_sort s = ctx().fpa_rounding_mode();
923  check_error();
924  return sort(ctx(), s);
925  }
Z3_error_code check_error() const
Definition: z3++.h:407
sort fpa_rounding_mode()
Return a RoundingMode sort.
Definition: z3++.h:2929
context & ctx() const
Definition: z3++.h:406
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:732

◆ get_decimal_string()

std::string get_decimal_string ( int  precision) const
inline

Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic.

Precondition
is_numeral() || is_algebraic()

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

793  {
794  assert(is_numeral() || is_algebraic());
795  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
796  }
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:780
context & ctx() const
Definition: z3++.h:406
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:486
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:739

◆ get_escaped_string()

std::string get_escaped_string ( ) const
inline

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

Precondition
expression is for a string value.

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

902  {
903  char const* s = Z3_get_string(ctx(), m_ast);
904  check_error();
905  return std::string(s);
906  }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s.
Z3_ast m_ast
Definition: z3++.h:486

◆ get_numeral_int()

int get_numeral_int ( ) const
inline

Return int value of numeral, throw if result cannot fit in machine int.

It only makes sense to use this function if the caller can ensure that the result is an integer or if exceptions are enabled. If exceptions are disabled, then use the is_numeral_i function.

Precondition
is_numeral()

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

814  {
815  int result = 0;
816  if (!is_numeral_i(result)) {
817  assert(ctx().enable_exceptions());
818  if (!ctx().enable_exceptions()) return 0;
819  Z3_THROW(exception("numeral does not fit in machine int"));
820  }
821  return result;
822  }
#define Z3_THROW(x)
Definition: z3++.h:96
context & ctx() const
Definition: z3++.h:406
bool is_numeral_i(int &i) const
Definition: z3++.h:742

◆ get_numeral_int64()

int64_t get_numeral_int64 ( ) const
inline

Return int64_t value of numeral, throw if result cannot fit in int64_t.

Precondition
is_numeral()

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

850  {
851  assert(is_numeral());
852  int64_t result = 0;
853  if (!is_numeral_i64(result)) {
854  assert(ctx().enable_exceptions());
855  if (!ctx().enable_exceptions()) return 0;
856  Z3_THROW(exception("numeral does not fit in machine int64_t"));
857  }
858  return result;
859  }
#define Z3_THROW(x)
Definition: z3++.h:96
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:740
context & ctx() const
Definition: z3++.h:406
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:739

◆ get_numeral_uint()

unsigned get_numeral_uint ( ) const
inline

Return uint value of numeral, throw if result cannot fit in machine uint.

It only makes sense to use this function if the caller can ensure that the result is an integer or if exceptions are enabled. If exceptions are disabled, then use the is_numeral_u function.

Precondition
is_numeral()

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

833  {
834  assert(is_numeral());
835  unsigned result = 0;
836  if (!is_numeral_u(result)) {
837  assert(ctx().enable_exceptions());
838  if (!ctx().enable_exceptions()) return 0;
839  Z3_THROW(exception("numeral does not fit in machine uint"));
840  }
841  return result;
842  }
#define Z3_THROW(x)
Definition: z3++.h:96
context & ctx() const
Definition: z3++.h:406
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:743
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:739

◆ get_numeral_uint64()

uint64_t get_numeral_uint64 ( ) const
inline

Return uint64_t value of numeral, throw if result cannot fit in uint64_t.

Precondition
is_numeral()

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

867  {
868  assert(is_numeral());
869  uint64_t result = 0;
870  if (!is_numeral_u64(result)) {
871  assert(ctx().enable_exceptions());
872  if (!ctx().enable_exceptions()) return 0;
873  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
874  }
875  return result;
876  }
#define Z3_THROW(x)
Definition: z3++.h:96
context & ctx() const
Definition: z3++.h:406
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:741
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:739

◆ get_sort()

sort get_sort ( ) const
inline

◆ get_string()

std::string get_string ( ) const
inline

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

908  {
909  unsigned n;
910  char const* s = Z3_get_lstring(ctx(), m_ast, &n);
911  check_error();
912  return std::string(s, n);
913  }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
Z3_string Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the unescaped string constant stored in s.
Z3_ast m_ast
Definition: z3++.h:486

◆ hi()

unsigned hi ( ) const
inline

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

1142 { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
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:406
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.

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

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for expression.

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

802 { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality....
Z3_ast m_ast
Definition: z3++.h:486

◆ is_algebraic()

bool is_algebraic ( ) const
inline

Return true if expression is an algebraic number.

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

780 { 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:406
Z3_ast m_ast
Definition: z3++.h:486

Referenced by expr::get_decimal_string().

◆ is_and()

bool is_and ( ) const
inline

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

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

◆ is_app()

bool is_app ( ) const
inline

Return true if this expression is an application.

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

750 { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:495

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

◆ is_arith()

bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

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

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

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

◆ is_array()

bool is_array ( ) const
inline

Return true if this is a Array expression.

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

702 { return get_sort().is_array(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:564

Referenced by expr::operator[]().

◆ is_bool()

bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

682 { return get_sort().is_bool(); }
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:544
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677

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

◆ is_bv()

bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

698 { return get_sort().is_bv(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:560

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

◆ is_const()

bool is_const ( ) const
inline

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

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

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

Referenced by solver::add().

◆ is_datatype()

bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

706 { return get_sort().is_datatype(); }
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:568
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677

◆ is_distinct()

bool is_distinct ( ) const
inline

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

1030 { return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
Z3_decl_kind decl_kind() const
Definition: z3++.h:635
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750

◆ is_eq()

bool is_eq ( ) const
inline

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

1028 { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
Z3_decl_kind decl_kind() const
Definition: z3++.h:635
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750

◆ is_exists()

bool is_exists ( ) const
inline

Return true if this expression is an existential quantifier.

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

767 { 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:406
Z3_ast m_ast
Definition: z3++.h:486

◆ is_false()

bool is_false ( ) const
inline

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

1022 { return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
Z3_decl_kind decl_kind() const
Definition: z3++.h:635
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750

◆ is_finite_domain()

bool is_finite_domain ( ) const
inline

Return true if this is a Finite-domain expression.

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

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

728 { return get_sort().is_finite_domain(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:584

◆ is_forall()

bool is_forall ( ) const
inline

Return true if this expression is a universal quantifier.

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

763 { return Z3_is_quantifier_forall(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:406
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:486

◆ is_fpa()

bool is_fpa ( ) const
inline

Return true if this is a FloatingPoint expression. .

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

732 { return get_sort().is_fpa(); }
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition: z3++.h:588
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677

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

◆ is_implies()

bool is_implies ( ) const
inline

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

1027 { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
Z3_decl_kind decl_kind() const
Definition: z3++.h:635
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750

◆ is_int()

bool is_int ( ) const
inline

Return true if this is an integer expression.

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

686 { return get_sort().is_int(); }
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:548
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677

Referenced by z3::abs().

◆ is_ite()

bool is_ite ( ) const
inline

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

1029 { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
Z3_decl_kind decl_kind() const
Definition: z3++.h:635
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750

◆ is_lambda()

bool is_lambda ( ) const
inline

Return true if this expression is a lambda expression.

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

771 { return Z3_is_lambda(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:406
Z3_ast m_ast
Definition: z3++.h:486
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.

◆ is_not()

bool is_not ( ) const
inline

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

1023 { return is_app() && Z3_OP_NOT == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
Z3_decl_kind decl_kind() const
Definition: z3++.h:635
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750

◆ is_numeral() [1/4]

bool is_numeral ( ) const
inline

Return true if this expression is a numeral. Specialized functions also return representations for the numerals as small integers, 64 bit integers or rational or decimal strings.

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

739 { return kind() == Z3_NUMERAL_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:495

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

◆ is_numeral() [2/4]

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

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

744 { 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:407
context & ctx() const
Definition: z3++.h:406
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.
Z3_ast m_ast
Definition: z3++.h:486
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:739

Referenced by expr::is_numeral().

◆ is_numeral() [3/4]

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

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

745 { 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:407
context & ctx() const
Definition: z3++.h:406
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:486
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:739

Referenced by expr::is_numeral().

◆ is_numeral() [4/4]

bool is_numeral ( double &  d) const
inline

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

746 { 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:407
context & ctx() const
Definition: z3++.h:406
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:486
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:739

Referenced by expr::is_numeral().

◆ is_numeral_i()

bool is_numeral_i ( int &  i) const
inline

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

742 { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
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:486

Referenced by expr::get_numeral_int().

◆ is_numeral_i64()

bool is_numeral_i64 ( int64_t &  i) const
inline

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

740 { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
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:486

Referenced by expr::get_numeral_int64().

◆ is_numeral_u()

bool is_numeral_u ( unsigned &  i) const
inline

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

743 { 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:407
context & ctx() const
Definition: z3++.h:406
Z3_ast m_ast
Definition: z3++.h:486

Referenced by expr::get_numeral_uint().

◆ is_numeral_u64()

bool is_numeral_u64 ( uint64_t &  i) const
inline

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

741 { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:407
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....
context & ctx() const
Definition: z3++.h:406
Z3_ast m_ast
Definition: z3++.h:486

Referenced by expr::get_numeral_uint64().

◆ is_or()

bool is_or ( ) const
inline

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

1025 { return is_app() && Z3_OP_OR == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
Z3_decl_kind decl_kind() const
Definition: z3++.h:635
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750

◆ is_quantifier()

bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

758 { return kind() == Z3_QUANTIFIER_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:495

Referenced by expr::body().

◆ is_re()

bool is_re ( ) const
inline

Return true if this is a regular expression.

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

718 { return get_sort().is_re(); }
bool is_re() const
Return true if this sort is a regular expression sort.
Definition: z3++.h:580
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677

Referenced by z3::operator+().

◆ is_real()

bool is_real ( ) const
inline

Return true if this is a real expression.

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

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

Referenced by z3::abs().

◆ is_relation()

bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

710 { return get_sort().is_relation(); }
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:572
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677

◆ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

714 { return get_sort().is_seq(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition: z3++.h:576

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

◆ is_true()

bool is_true ( ) const
inline

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

1021 { return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
Z3_decl_kind decl_kind() const
Definition: z3++.h:635
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750

◆ is_var()

bool is_var ( ) const
inline

Return true if this expression is a variable.

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

776 { return kind() == Z3_VAR_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:495

◆ is_well_sorted()

bool is_well_sorted ( ) const
inline

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

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

785 { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
Z3_ast m_ast
Definition: z3++.h:486
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.

◆ is_xor()

bool is_xor ( ) const
inline

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

1026 { return is_app() && Z3_OP_XOR == decl().decl_kind(); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
Z3_decl_kind decl_kind() const
Definition: z3++.h:635
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750

◆ itos()

expr itos ( ) const
inline

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

1197  {
1198  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1199  check_error();
1200  return expr(ctx(), r);
1201  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.

◆ length()

expr length ( ) const
inline

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

1187  {
1188  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1189  check_error();
1190  return expr(ctx(), r);
1191  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
context & ctx() const
Definition: z3++.h:406

Referenced by expr::extract().

◆ lo()

unsigned lo ( ) const
inline

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

1141 { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:934
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:406
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:750
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.

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

◆ loop() [1/2]

expr loop ( unsigned  lo)
inline

create a looping regular expression.

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

1207  {
1208  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1209  check_error();
1210  return expr(ctx(), r);
1211  }
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
unsigned lo() const
Definition: z3++.h:1141
Z3_ast m_ast
Definition: z3++.h:486

◆ loop() [2/2]

expr loop ( unsigned  lo,
unsigned  hi 
)
inline

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

1212  {
1213  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1214  check_error();
1215  return expr(ctx(), r);
1216  }
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
unsigned lo() const
Definition: z3++.h:1141
unsigned hi() const
Definition: z3++.h:1142
Z3_ast m_ast
Definition: z3++.h:486

◆ nth()

expr nth ( expr const &  index) const
inline

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

1181  {
1182  check_context(*this, index);
1183  Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1184  check_error();
1185  return expr(ctx(), r);
1186  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
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:406
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410

Referenced by expr::operator[]().

◆ num_args()

unsigned num_args ( ) const
inline

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

Precondition
is_app()

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

941 { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:407
context & ctx() const
Definition: z3++.h:406
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...

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

◆ numerator()

expr numerator ( ) const
inline

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

882  {
883  assert(is_numeral());
884  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
885  check_error();
886  return expr(ctx(),r);
887  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
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:486
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:739

◆ operator Z3_app()

operator Z3_app ( ) const
inline

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

915 { 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:750
Z3_ast m_ast
Definition: z3++.h:486

◆ operator=()

expr& operator= ( expr const &  n)
inline

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

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

◆ operator[]() [1/2]

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

index operator defined on arrays and sequences.

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

1221  {
1222  assert(is_array() || is_seq());
1223  if (is_array()) {
1224  return select(*this, index);
1225  }
1226  return nth(index);
1227  }
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:702
expr nth(expr const &index) const
Definition: z3++.h:1181
expr select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3256
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:714

◆ operator[]() [2/2]

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

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

1229  {
1230  return select(*this, index);
1231  }
expr select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3256

◆ repeat()

expr repeat ( unsigned  i)
inline

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

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

◆ replace()

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

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

1158  {
1159  check_context(*this, src); check_context(src, dst);
1160  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1161  check_error();
1162  return expr(ctx(), r);
1163  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
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.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410

◆ rotate_left()

expr rotate_left ( unsigned  i)
inline

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

1132 { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.

◆ rotate_right()

expr rotate_right ( unsigned  i)
inline

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

1133 { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
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.

◆ simplify() [1/2]

expr simplify ( ) const
inline

Return a simplified version of this expression.

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

1236 { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_ast m_ast
Definition: z3++.h:486

◆ simplify() [2/2]

expr simplify ( params const &  p) const
inline

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

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

1240 { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
context & ctx() const
Definition: z3++.h:406
Z3_ast m_ast
Definition: z3++.h:486

◆ stoi()

expr stoi ( ) const
inline

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

1192  {
1193  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1194  check_error();
1195  return expr(ctx(), r);
1196  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
context & ctx() const
Definition: z3++.h:406

◆ substitute() [1/2]

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

Apply substitution. Replace src expressions by dst.

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

3488  {
3489  assert(src.size() == dst.size());
3490  array<Z3_ast> _src(src.size());
3491  array<Z3_ast> _dst(dst.size());
3492  for (unsigned i = 0; i < src.size(); ++i) {
3493  _src[i] = src[i];
3494  _dst[i] = dst[i];
3495  }
3496  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
3497  check_error();
3498  return expr(ctx(), r);
3499  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
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....
context & ctx() const
Definition: z3++.h:406
Z3_ast m_ast
Definition: z3++.h:486

◆ substitute() [2/2]

expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

3501  {
3502  array<Z3_ast> _dst(dst.size());
3503  for (unsigned i = 0; i < dst.size(); ++i) {
3504  _dst[i] = dst[i];
3505  }
3506  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
3507  check_error();
3508  return expr(ctx(), r);
3509  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs,...
Z3_ast m_ast
Definition: z3++.h:486

◆ unit()

expr unit ( ) const
inline

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

1164  {
1165  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1166  check_error();
1167  return expr(ctx(), r);
1168  }
Z3_error_code check_error() const
Definition: z3++.h:407
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.

Friends And Related Function Documentation

◆ abs

expr abs ( expr const &  a)
friend

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

1606  {
1607  Z3_ast r;
1608  if (a.is_int()) {
1609  expr zero = a.ctx().int_val(0);
1610  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1611  }
1612  else if (a.is_real()) {
1613  expr zero = a.ctx().real_val(0);
1614  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1615  }
1616  else {
1617  r = Z3_mk_fpa_abs(a.ctx(), a);
1618  }
1619  a.check_error();
1620  return expr(a.ctx(), r);
1621  }
expr(context &c)
Definition: z3++.h:669
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
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_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).

◆ atleast

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

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

2040  {
2041  assert(es.size() > 0);
2042  context& ctx = es[0].ctx();
2043  array<Z3_ast> _es(es);
2044  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2045  ctx.check_error();
2046  return expr(ctx, r);
2047  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ atmost

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

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

2032  {
2033  assert(es.size() > 0);
2034  context& ctx = es[0].ctx();
2035  array<Z3_ast> _es(es);
2036  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2037  ctx.check_error();
2038  return expr(ctx, r);
2039  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ bv2int

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

bit-vector and integer conversions.

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

1772 { 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:669
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...

◆ bvadd_no_overflow

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

bit-vector overflow/underflow checks

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

1778  {
1779  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);
1780  }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

◆ bvadd_no_underflow

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

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

1781  {
1782  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1783  }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

◆ bvmul_no_overflow

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

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

1796  {
1797  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);
1798  }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

◆ bvmul_no_underflow

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

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

1799  {
1800  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1801  }
expr(context &c)
Definition: z3++.h:669
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:410

◆ bvneg_no_overflow

expr bvneg_no_overflow ( expr const &  a)
friend

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

1793  {
1794  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
1795  }
expr(context &c)
Definition: z3++.h:669
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.

◆ bvsdiv_no_overflow

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

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

1790  {
1791  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1792  }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

◆ bvsub_no_overflow

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

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

1784  {
1785  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1786  }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

◆ bvsub_no_underflow

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

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

1787  {
1788  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);
1789  }
expr(context &c)
Definition: z3++.h:669
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:410

◆ concat [1/2]

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

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

2066  {
2067  check_context(a, b);
2068  Z3_ast r;
2069  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2070  Z3_ast _args[2] = { a, b };
2071  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2072  }
2073  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2074  Z3_ast _args[2] = { a, b };
2075  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2076  }
2077  else {
2078  r = Z3_mk_concat(a.ctx(), a, b);
2079  }
2080  a.ctx().check_error();
2081  return expr(a.ctx(), r);
2082  }
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:669
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:410
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.

◆ concat [2/2]

expr concat ( expr_vector const &  args)
friend

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

2084  {
2085  Z3_ast r;
2086  assert(args.size() > 0);
2087  if (args.size() == 1) {
2088  return args[0];
2089  }
2090  context& ctx = args[0].ctx();
2091  array<Z3_ast> _args(args);
2092  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
2093  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2094  }
2095  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
2096  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2097  }
2098  else {
2099  r = _args[args.size()-1];
2100  for (unsigned i = args.size()-1; i > 0; ) {
2101  --i;
2102  r = Z3_mk_concat(ctx, _args[i], r);
2103  ctx.check_error();
2104  }
2105  }
2106  ctx.check_error();
2107  return expr(ctx, r);
2108  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
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:669
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.
context & ctx() const
Definition: z3++.h:406
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:677
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.

◆ distinct

expr distinct ( expr_vector const &  args)
friend

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

2057  {
2058  assert(args.size() > 0);
2059  context& ctx = args[0].ctx();
2060  array<Z3_ast> _args(args);
2061  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2062  ctx.check_error();
2063  return expr(ctx, r);
2064  }
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406

◆ fma

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

FloatingPoint fused multiply-add.

◆ implies [1/3]

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

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

1261  {
1262  assert(a.is_bool() && b.is_bool());
1263  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1264  }
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:1254

◆ implies [2/3]

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

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

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

◆ implies [3/3]

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

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

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

◆ int2bv

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

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

1773 { Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:669
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.

◆ is_int

expr is_int ( expr const &  e)
friend

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

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

◆ ite

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

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

Precondition
c.is_bool()

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

1645  {
1646  check_context(c, t); check_context(c, e);
1647  assert(c.is_bool());
1648  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1649  c.check_error();
1650  return expr(c.ctx(), r);
1651  }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
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).

◆ max

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

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

1591  {
1592  check_context(a, b);
1593  Z3_ast r;
1594  if (a.is_arith()) {
1595  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1596  }
1597  else if (a.is_bv()) {
1598  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1599  }
1600  else {
1601  assert(a.is_fpa());
1602  r = Z3_mk_fpa_max(a.ctx(), a, b);
1603  }
1604  return expr(a.ctx(), r);
1605  }
expr(context &c)
Definition: z3++.h:669
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:410
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).

◆ min

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

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

1576  {
1577  check_context(a, b);
1578  Z3_ast r;
1579  if (a.is_arith()) {
1580  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1581  }
1582  else if (a.is_bv()) {
1583  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1584  }
1585  else {
1586  assert(a.is_fpa());
1587  r = Z3_mk_fpa_min(a.ctx(), a, b);
1588  }
1589  return expr(a.ctx(), r);
1590  }
expr(context &c)
Definition: z3++.h:669
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:410
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.

◆ mk_and

expr mk_and ( expr_vector const &  args)
friend

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

2116  {
2117  array<Z3_ast> _args(args);
2118  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2119  args.check_error();
2120  return expr(args.ctx(), r);
2121  }
expr(context &c)
Definition: z3++.h:669
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].

◆ mk_or

expr mk_or ( expr_vector const &  args)
friend

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

2110  {
2111  array<Z3_ast> _args(args);
2112  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2113  args.check_error();
2114  return expr(args.ctx(), r);
2115  }
expr(context &c)
Definition: z3++.h:669
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].

◆ mod [1/3]

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

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

1273  {
1274  if (a.is_bv()) {
1275  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1276  }
1277  else {
1278  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1279  }
1280  }
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:1254

◆ mod [2/3]

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

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

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

◆ mod [3/3]

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

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

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

◆ nand

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

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

1573 { check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:669
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:410

◆ nor

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

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

1574 { check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); 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:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410

◆ operator!

expr operator! ( expr const &  a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

1307 { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1301
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).

◆ operator!= [1/3]

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

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

1347  {
1348  check_context(a, b);
1349  Z3_ast args[2] = { a, b };
1350  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1351  a.check_error();
1352  return expr(a.ctx(), r);
1353  }
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:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410

◆ operator!= [2/3]

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

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

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

◆ operator!= [3/3]

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

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

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

◆ operator& [1/3]

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

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

1561 { check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.

◆ operator& [2/3]

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

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

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

◆ operator& [3/3]

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

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

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

◆ operator&& [1/3]

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

Return an expression representing a and b.

Precondition
a.is_bool()
b.is_bool()

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

1313  {
1314  check_context(a, b);
1315  assert(a.is_bool() && b.is_bool());
1316  Z3_ast args[2] = { a, b };
1317  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1318  a.check_error();
1319  return expr(a.ctx(), r);
1320  }
expr(context &c)
Definition: z3++.h:669
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:410

◆ operator&& [2/3]

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

Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.

Precondition
a.is_bool()

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

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

◆ operator&& [3/3]

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

Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.

Precondition
b.is_bool()

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

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

◆ operator* [1/3]

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

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

1387  {
1388  check_context(a, b);
1389  Z3_ast r = 0;
1390  if (a.is_arith() && b.is_arith()) {
1391  Z3_ast args[2] = { a, b };
1392  r = Z3_mk_mul(a.ctx(), 2, args);
1393  }
1394  else if (a.is_bv() && b.is_bv()) {
1395  r = Z3_mk_bvmul(a.ctx(), a, b);
1396  }
1397  else if (a.is_fpa() && b.is_fpa()) {
1398  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1399  }
1400  else {
1401  // operator is not supported by given arguments.
1402  assert(false);
1403  }
1404  a.check_error();
1405  return expr(a.ctx(), r);
1406  }
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:669
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:410
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.

◆ operator* [2/3]

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

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

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

◆ operator* [3/3]

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

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

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

◆ operator+ [1/3]

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

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

1357  {
1358  check_context(a, b);
1359  Z3_ast r = 0;
1360  if (a.is_arith() && b.is_arith()) {
1361  Z3_ast args[2] = { a, b };
1362  r = Z3_mk_add(a.ctx(), 2, args);
1363  }
1364  else if (a.is_bv() && b.is_bv()) {
1365  r = Z3_mk_bvadd(a.ctx(), a, b);
1366  }
1367  else if (a.is_seq() && b.is_seq()) {
1368  return concat(a, b);
1369  }
1370  else if (a.is_re() && b.is_re()) {
1371  Z3_ast _args[2] = { a, b };
1372  r = Z3_mk_re_union(a.ctx(), 2, _args);
1373  }
1374  else if (a.is_fpa() && b.is_fpa()) {
1375  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1376  }
1377  else {
1378  // operator is not supported by given arguments.
1379  assert(false);
1380  }
1381  a.check_error();
1382  return expr(a.ctx(), r);
1383  }
expr(context &c)
Definition: z3++.h:669
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:2066
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].
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
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.

◆ operator+ [2/3]

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

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

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

◆ operator+ [3/3]

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

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

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

◆ operator- [1/4]

expr operator- ( expr const &  a)
friend

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

1450  {
1451  Z3_ast r = 0;
1452  if (a.is_arith()) {
1453  r = Z3_mk_unary_minus(a.ctx(), a);
1454  }
1455  else if (a.is_bv()) {
1456  r = Z3_mk_bvneg(a.ctx(), a);
1457  }
1458  else if (a.is_fpa()) {
1459  r = Z3_mk_fpa_neg(a.ctx(), a);
1460  }
1461  else {
1462  // operator is not supported by given arguments.
1463  assert(false);
1464  }
1465  a.check_error();
1466  return expr(a.ctx(), r);
1467  }
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:669
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.

◆ operator- [2/4]

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

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

1469  {
1470  check_context(a, b);
1471  Z3_ast r = 0;
1472  if (a.is_arith() && b.is_arith()) {
1473  Z3_ast args[2] = { a, b };
1474  r = Z3_mk_sub(a.ctx(), 2, args);
1475  }
1476  else if (a.is_bv() && b.is_bv()) {
1477  r = Z3_mk_bvsub(a.ctx(), a, b);
1478  }
1479  else if (a.is_fpa() && b.is_fpa()) {
1480  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1481  }
1482  else {
1483  // operator is not supported by given arguments.
1484  assert(false);
1485  }
1486  a.check_error();
1487  return expr(a.ctx(), r);
1488  }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
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.

◆ operator- [3/4]

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

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

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

◆ operator- [4/4]

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

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

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

◆ operator/ [1/3]

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

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

1428  {
1429  check_context(a, b);
1430  Z3_ast r = 0;
1431  if (a.is_arith() && b.is_arith()) {
1432  r = Z3_mk_div(a.ctx(), a, b);
1433  }
1434  else if (a.is_bv() && b.is_bv()) {
1435  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1436  }
1437  else if (a.is_fpa() && b.is_fpa()) {
1438  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1439  }
1440  else {
1441  // operator is not supported by given arguments.
1442  assert(false);
1443  }
1444  a.check_error();
1445  return expr(a.ctx(), r);
1446  }
expr(context &c)
Definition: z3++.h:669
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:410
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.

◆ operator/ [2/3]

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

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

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

◆ operator/ [3/3]

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

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

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

◆ operator< [1/3]

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

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

1517  {
1518  check_context(a, b);
1519  Z3_ast r = 0;
1520  if (a.is_arith() && b.is_arith()) {
1521  r = Z3_mk_lt(a.ctx(), a, b);
1522  }
1523  else if (a.is_bv() && b.is_bv()) {
1524  r = Z3_mk_bvslt(a.ctx(), a, b);
1525  }
1526  else if (a.is_fpa() && b.is_fpa()) {
1527  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1528  }
1529  else {
1530  // operator is not supported by given arguments.
1531  assert(false);
1532  }
1533  a.check_error();
1534  return expr(a.ctx(), r);
1535  }
expr(context &c)
Definition: z3++.h:669
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:410
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.

◆ operator< [2/3]

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

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

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

◆ operator< [3/3]

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

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

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

◆ operator<= [1/3]

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

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

1492  {
1493  check_context(a, b);
1494  Z3_ast r = 0;
1495  if (a.is_arith() && b.is_arith()) {
1496  r = Z3_mk_le(a.ctx(), a, b);
1497  }
1498  else if (a.is_bv() && b.is_bv()) {
1499  r = Z3_mk_bvsle(a.ctx(), a, b);
1500  }
1501  else if (a.is_fpa() && b.is_fpa()) {
1502  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1503  }
1504  else {
1505  // operator is not supported by given arguments.
1506  assert(false);
1507  }
1508  a.check_error();
1509  return expr(a.ctx(), r);
1510  }
expr(context &c)
Definition: z3++.h:669
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:410
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.

◆ operator<= [2/3]

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

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

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

◆ operator<= [3/3]

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

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

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

◆ operator== [1/3]

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

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

1338  {
1339  check_context(a, b);
1340  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1341  a.check_error();
1342  return expr(a.ctx(), r);
1343  }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.

◆ operator== [2/3]

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

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

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

◆ operator== [3/3]

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

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

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

◆ operator> [1/3]

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

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

1539  {
1540  check_context(a, b);
1541  Z3_ast r = 0;
1542  if (a.is_arith() && b.is_arith()) {
1543  r = Z3_mk_gt(a.ctx(), a, b);
1544  }
1545  else if (a.is_bv() && b.is_bv()) {
1546  r = Z3_mk_bvsgt(a.ctx(), a, b);
1547  }
1548  else if (a.is_fpa() && b.is_fpa()) {
1549  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1550  }
1551  else {
1552  // operator is not supported by given arguments.
1553  assert(false);
1554  }
1555  a.check_error();
1556  return expr(a.ctx(), r);
1557  }
expr(context &c)
Definition: z3++.h:669
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:410
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.

◆ operator> [2/3]

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

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

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

◆ operator> [3/3]

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

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

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

◆ operator>= [1/3]

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

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

1411  {
1412  check_context(a, b);
1413  Z3_ast r = 0;
1414  if (a.is_arith() && b.is_arith()) {
1415  r = Z3_mk_ge(a.ctx(), a, b);
1416  }
1417  else if (a.is_bv() && b.is_bv()) {
1418  r = Z3_mk_bvsge(a.ctx(), a, b);
1419  }
1420  else {
1421  // operator is not supported by given arguments.
1422  assert(false);
1423  }
1424  a.check_error();
1425  return expr(a.ctx(), r);
1426  }
expr(context &c)
Definition: z3++.h:669
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:410

◆ operator>= [2/3]

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

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

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

◆ operator>= [3/3]

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

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

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

◆ operator^ [1/3]

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

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

1565 { check_context(a, b); Z3_ast r = Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.

◆ operator^ [2/3]

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

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

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

◆ operator^ [3/3]

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

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

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

◆ operator| [1/3]

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

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

1569 { check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.

◆ operator| [2/3]

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

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

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

◆ operator| [3/3]

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

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

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

◆ operator|| [1/3]

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

Return an expression representing a or b.

Precondition
a.is_bool()
b.is_bool()

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

1325  {
1326  check_context(a, b);
1327  assert(a.is_bool() && b.is_bool());
1328  Z3_ast args[2] = { a, b };
1329  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1330  a.check_error();
1331  return expr(a.ctx(), r);
1332  }
expr(context &c)
Definition: z3++.h:669
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].
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410

◆ operator|| [2/3]

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

Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.

Precondition
a.is_bool()

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

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

◆ operator|| [3/3]

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

Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.

Precondition
b.is_bool()

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

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

◆ operator~

expr operator~ ( expr const &  a)
friend

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

1629 { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:669
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.

◆ pbeq

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

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

2024  {
2025  assert(es.size() > 0);
2026  context& ctx = es[0].ctx();
2027  array<Z3_ast> _es(es);
2028  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2029  ctx.check_error();
2030  return expr(ctx, r);
2031  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:669
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:406

◆ pbge

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

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

2016  {
2017  assert(es.size() > 0);
2018  context& ctx = es[0].ctx();
2019  array<Z3_ast> _es(es);
2020  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2021  ctx.check_error();
2022  return expr(ctx, r);
2023  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

◆ pble

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

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

2008  {
2009  assert(es.size() > 0);
2010  context& ctx = es[0].ctx();
2011  array<Z3_ast> _es(es);
2012  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2013  ctx.check_error();
2014  return expr(ctx, r);
2015  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:669
context & ctx() const
Definition: z3++.h:406
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

◆ pw [1/3]

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

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

1269 { _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:1254

◆ pw [2/3]

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

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

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

◆ pw [3/3]

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

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

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

◆ range

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

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

3431  {
3432  check_context(lo, hi);
3433  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3434  lo.check_error();
3435  return expr(lo.ctx(), r);
3436  }
expr(context &c)
Definition: z3++.h:669
unsigned lo() const
Definition: z3++.h:1141
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
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:1142

◆ rem [1/3]

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

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

1289  {
1290  if (a.is_fpa() && b.is_fpa()) {
1291  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1292  } else {
1293  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1294  }
1295  }
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:1254

◆ rem [2/3]

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

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

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

◆ rem [3/3]

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

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

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

◆ sqrt

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

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

1622  {
1623  check_context(a, rm);
1624  assert(a.is_fpa());
1625  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1626  a.check_error();
1627  return expr(a.ctx(), r);
1628  }
expr(context &c)
Definition: z3++.h:669
friend void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.

◆ sum

expr sum ( expr_vector const &  args)
friend

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

2048  {
2049  assert(args.size() > 0);
2050  context& ctx = args[0].ctx();
2051  array<Z3_ast> _args(args);
2052  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2053  ctx.check_error();
2054  return expr(ctx, r);
2055  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:178
expr(context &c)
Definition: z3++.h:669
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].
context & ctx() const
Definition: z3++.h:406

◆ xnor

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

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

1575 { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:669
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:410