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 as_binary (std::string &s) const
 
bool is_app () const
 Return true if this expression is an application. More...
 
bool is_const () const
 Return true if this expression is a constant (i.e., an application with 0 arguments). More...
 
bool is_quantifier () const
 Return true if this expression is a quantifier. More...
 
bool is_forall () const
 Return true if this expression is a universal quantifier. More...
 
bool is_exists () const
 Return true if this expression is an existential quantifier. More...
 
bool is_lambda () const
 Return true if this expression is a lambda expression. More...
 
bool is_var () const
 Return true if this expression is a variable. More...
 
bool is_algebraic () const
 Return true if expression is an algebraic number. More...
 
bool is_well_sorted () const
 Return true if this expression is well sorted (aka type correct). More...
 
std::string get_decimal_string (int precision) const
 Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic. More...
 
expr algebraic_lower (unsigned precision) const
 
expr algebraic_upper (unsigned precision) const
 
expr_vector algebraic_poly () const
 Return coefficients for p of an algebraic number (root-obj p i) More...
 
unsigned algebraic_i () const
 Return i of an algebraic number (root-obj p i) More...
 
unsigned id () const
 retrieve unique identifier for expression. More...
 
int get_numeral_int () const
 Return int value of numeral, throw if result cannot fit in machine int. More...
 
unsigned get_numeral_uint () const
 Return uint value of numeral, throw if result cannot fit in machine uint. More...
 
int64_t get_numeral_int64 () const
 Return int64_t value of numeral, throw if result cannot fit in int64_t. More...
 
uint64_t get_numeral_uint64 () const
 Return uint64_t value of numeral, throw if result cannot fit in uint64_t. More...
 
Z3_lbool bool_value () const
 
expr numerator () const
 
expr denominator () const
 
bool is_string_value () const
 Return true if this expression is a string literal. The string can be accessed using get_string() and get_escaped_string() More...
 
std::string get_escaped_string () const
 for a string value expression return an escaped or unescaped string value. More...
 
std::string get_string () const
 
 operator Z3_app () const
 
sort fpa_rounding_mode ()
 Return a RoundingMode sort. More...
 
func_decl decl () const
 Return the declaration associated with this application. This method assumes the expression is an application. More...
 
unsigned num_args () const
 Return the number of arguments in this application. This method assumes the expression is an application. More...
 
expr arg (unsigned i) const
 Return the i-th argument of this application. This method assumes the expression is an application. More...
 
expr body () const
 Return the 'body' of this quantifier. More...
 
bool is_true () const
 
bool is_false () const
 
bool is_not () const
 
bool is_and () const
 
bool is_or () const
 
bool is_xor () const
 
bool is_implies () const
 
bool is_eq () const
 
bool is_ite () const
 
bool is_distinct () const
 
expr rotate_left (unsigned i)
 
expr rotate_right (unsigned i)
 
expr repeat (unsigned i)
 
expr extract (unsigned hi, unsigned lo) const
 
unsigned lo () const
 
unsigned hi () const
 
expr extract (expr const &offset, expr const &length) const
 sequence and regular expression operations. More...
 
expr replace (expr const &src, expr const &dst) const
 
expr unit () const
 
expr contains (expr const &s)
 
expr at (expr const &index) const
 
expr nth (expr const &index) const
 
expr length () const
 
expr stoi () const
 
expr itos () const
 
expr loop (unsigned lo)
 create a looping regular expression. More...
 
expr loop (unsigned lo, unsigned hi)
 
expr operator[] (expr const &index) const
 
expr operator[] (expr_vector const &index) const
 
expr simplify () const
 Return a simplified version of this expression. More...
 
expr simplify (params const &p) const
 Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier. More...
 
expr substitute (expr_vector const &src, expr_vector const &dst)
 Apply substitution. Replace src expressions by dst. More...
 
expr substitute (expr_vector const &dst)
 Apply substitution. Replace bound variables by expressions. More...
 
- Public Member Functions inherited from ast
 ast (context &c)
 
 ast (context &c, Z3_ast n)
 
 ast (ast const &s)
 
 ~ast ()
 
 operator Z3_ast () const
 
 operator bool () const
 
astoperator= (ast const &s)
 
Z3_ast_kind kind () const
 
unsigned hash () const
 
std::string to_string () const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
Z3_error_code check_error () const
 

Friends

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

Additional Inherited Members

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

Detailed Description

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

Definition at line 746 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 749 of file z3++.h.

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

◆ expr() [3/3]

expr ( expr const &  n)
inline

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

750 :ast(n) {}

Member Function Documentation

◆ algebraic_i()

unsigned algebraic_i ( ) const
inline

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

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

909  {
910  assert(is_algebraic());
911  unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
912  check_error();
913  return i;
914  }
Z3_ast m_ast
Definition: z3++.h:498
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:861
context & ctx() const
Definition: z3++.h:418
Z3_error_code check_error() const
Definition: z3++.h:419
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.

◆ algebraic_lower()

expr algebraic_lower ( unsigned  precision) const
inline

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

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

882  {
883  assert(is_algebraic());
884  Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
885  check_error();
886  return expr(ctx(), r);
887  }
expr(context &c)
Definition: z3++.h:748
Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision)
Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...

◆ algebraic_poly()

expr_vector algebraic_poly ( ) const
inline

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

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

899  {
900  assert(is_algebraic());
901  Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
902  check_error();
903  return expr_vector(ctx(), r);
904  }
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:72
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.

◆ algebraic_upper()

expr algebraic_upper ( unsigned  precision) const
inline

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

889  {
890  assert(is_algebraic());
891  Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
892  check_error();
893  return expr(ctx(), r);
894  }
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...

◆ arg()

expr arg ( unsigned  i) const
inline

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

Precondition
is_app()
i < num_args()

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

1075 { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.

Referenced by AstRef::__bool__(), and ExprRef::children().

◆ as_binary()

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

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

826 { if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:818
Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a)
Return numeral value, as a binary string of a numeric constant term.

◆ at()

expr at ( expr const &  index) const
inline

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

1301  {
1302  check_context(*this, index);
1303  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1304  check_error();
1305  return expr(ctx(), r);
1306  }
friend void check_context(object const &a, object const &b)
Definition: z3++.h:422
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...

◆ body()

expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

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

Referenced by QuantifierRef::children().

◆ bool_value()

Z3_lbool bool_value ( ) const
inline

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

995  {
996  return Z3_get_bool_value(ctx(), m_ast);
997  }
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.

◆ contains()

expr contains ( expr const &  s)
inline

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

1295  {
1296  check_context(*this, s);
1297  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1298  check_error();
1299  return expr(ctx(), r);
1300  }
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 1060 of file z3++.h.

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

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

◆ denominator()

expr denominator ( ) const
inline

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

1007  {
1008  assert(is_numeral());
1009  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
1010  check_error();
1011  return expr(ctx(),r);
1012  }
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.

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

◆ extract() [1/2]

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

sequence and regular expression operations.

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

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

1280  {
1281  check_context(*this, offset); check_context(offset, length);
1282  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1283  }
expr length() const
Definition: z3++.h:1313
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.

◆ extract() [2/2]

expr extract ( unsigned  hi,
unsigned  lo 
) const
inline

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

1266 { 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:187
unsigned hi() const
Definition: z3++.h:1268
unsigned lo() const
Definition: z3++.h:1267
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,...

◆ fpa_rounding_mode()

sort fpa_rounding_mode ( )
inline

Return a RoundingMode sort.

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

1046  {
1047  assert(is_fpa());
1048  Z3_sort s = ctx().fpa_rounding_mode();
1049  check_error();
1050  return sort(ctx(), s);
1051  }
sort fpa_rounding_mode()
Return a RoundingMode sort.
Definition: z3++.h:3013
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:811

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

874  {
875  assert(is_numeral() || is_algebraic());
876  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
877  }
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places.

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

1026  {
1027  assert(is_string_value());
1028  char const* s = Z3_get_string(ctx(), m_ast);
1029  check_error();
1030  return std::string(s);
1031  }
bool is_string_value() const
Return true if this expression is a string literal. The string can be accessed using get_string() and...
Definition: z3++.h:1019
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s.

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

931  {
932  int result = 0;
933  if (!is_numeral_i(result)) {
934  assert(ctx().enable_exceptions());
935  if (!ctx().enable_exceptions()) return 0;
936  Z3_THROW(exception("numeral does not fit in machine int"));
937  }
938  return result;
939  }
bool is_numeral_i(int &i) const
Definition: z3++.h:821
#define Z3_THROW(x)
Definition: z3++.h:99

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

967  {
968  assert(is_numeral());
969  int64_t result = 0;
970  if (!is_numeral_i64(result)) {
971  assert(ctx().enable_exceptions());
972  if (!ctx().enable_exceptions()) return 0;
973  Z3_THROW(exception("numeral does not fit in machine int64_t"));
974  }
975  return result;
976  }
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:819

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

950  {
951  assert(is_numeral());
952  unsigned result = 0;
953  if (!is_numeral_u(result)) {
954  assert(ctx().enable_exceptions());
955  if (!ctx().enable_exceptions()) return 0;
956  Z3_THROW(exception("numeral does not fit in machine uint"));
957  }
958  return result;
959  }
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:822

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

984  {
985  assert(is_numeral());
986  uint64_t result = 0;
987  if (!is_numeral_u64(result)) {
988  assert(ctx().enable_exceptions());
989  if (!ctx().enable_exceptions()) return 0;
990  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
991  }
992  return result;
993  }
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:820

◆ get_sort()

sort get_sort ( ) const
inline

Return the sort of this expression.

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

756 { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
context * m_ctx
Definition: z3++.h:414
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.

Referenced by z3::ashr(), expr::is_arith(), expr::is_array(), expr::is_bool(), expr::is_bv(), expr::is_datatype(), expr::is_finite_domain(), expr::is_fpa(), expr::is_int(), expr::is_re(), expr::is_real(), expr::is_relation(), expr::is_seq(), z3::lshr(), z3::select(), z3::shl(), z3::sle(), z3::slt(), z3::smod(), ModelRef::sorts(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().

◆ get_string()

std::string get_string ( ) const
inline

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

1033  {
1034  assert(is_string_value());
1035  unsigned n;
1036  char const* s = Z3_get_lstring(ctx(), m_ast, &n);
1037  check_error();
1038  return std::string(s, n);
1039  }
Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the unescaped string constant stored in s.

◆ hi()

unsigned hi ( ) const
inline

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

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

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

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for expression.

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

919 { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality....

◆ is_algebraic()

bool is_algebraic ( ) const
inline

Return true if expression is an algebraic number.

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

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

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

◆ is_and()

bool is_and ( ) const
inline

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

1150 { return is_app() && Z3_OP_AND == decl().decl_kind(); }
Z3_decl_kind decl_kind() const
Definition: z3++.h:715
@ Z3_OP_AND
Definition: z3_api.h:1007

◆ is_app()

bool is_app ( ) const
inline

Return true if this expression is an application.

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

831 { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:507
@ Z3_APP_AST
Definition: z3_api.h:182
@ Z3_NUMERAL_AST
Definition: z3_api.h:181

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

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

◆ is_array()

bool is_array ( ) const
inline

Return true if this is a Array expression.

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

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

Referenced by expr::operator[]().

◆ is_bool()

bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

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

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

◆ is_bv()

bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

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

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

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

Referenced by solver::add().

◆ is_datatype()

bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

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

◆ is_distinct()

bool is_distinct ( ) const
inline

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

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

◆ is_eq()

bool is_eq ( ) const
inline

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

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

◆ is_exists()

bool is_exists ( ) const
inline

Return true if this expression is an existential quantifier.

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

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

◆ is_false()

bool is_false ( ) const
inline

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

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

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

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

◆ is_forall()

bool is_forall ( ) const
inline

Return true if this expression is a universal quantifier.

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

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

◆ is_fpa()

bool is_fpa ( ) const
inline

Return true if this is a FloatingPoint expression. .

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

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

Referenced by expr::fpa_rounding_mode(), z3::operator!=(), and z3::operator==().

◆ is_implies()

bool is_implies ( ) const
inline

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

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

◆ is_int()

bool is_int ( ) const
inline

Return true if this is an integer expression.

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

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

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

◆ is_ite()

bool is_ite ( ) const
inline

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

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

◆ is_lambda()

bool is_lambda ( ) const
inline

Return true if this expression is a lambda expression.

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

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

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

◆ is_not()

bool is_not ( ) const
inline

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

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

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

818 { return kind() == Z3_NUMERAL_AST; }

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

◆ is_numeral() [2/4]

bool is_numeral ( double &  d) const
inline

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

825 { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.

Referenced by expr::is_numeral().

◆ is_numeral() [3/4]

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

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

823 { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a decimal string of a numeric constant term.

Referenced by expr::is_numeral().

◆ is_numeral() [4/4]

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

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

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

Referenced by expr::is_numeral().

◆ is_numeral_i()

bool is_numeral_i ( int &  i) const
inline

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

821 { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int....

Referenced by expr::get_numeral_int().

◆ is_numeral_i64()

bool is_numeral_i64 ( int64_t &  i) const
inline

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

819 { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int....

Referenced by expr::get_numeral_int64().

◆ is_numeral_u()

bool is_numeral_u ( unsigned &  i) const
inline

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

822 { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int....

Referenced by expr::get_numeral_uint().

◆ is_numeral_u64()

bool is_numeral_u64 ( uint64_t &  i) const
inline

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

820 { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int....

Referenced by expr::get_numeral_uint64().

◆ is_or()

bool is_or ( ) const
inline

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

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

◆ is_quantifier()

bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

839 { return kind() == Z3_QUANTIFIER_AST; }
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:184

Referenced by expr::body().

◆ is_re()

bool is_re ( ) const
inline

Return true if this is a regular expression.

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

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

◆ is_real()

bool is_real ( ) const
inline

Return true if this is a real expression.

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

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

◆ is_relation()

bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

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

◆ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

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

Referenced by expr::operator[]().

◆ is_string_value()

bool is_string_value ( ) const
inline

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

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

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

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

◆ is_true()

bool is_true ( ) const
inline

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

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

◆ is_var()

bool is_var ( ) const
inline

Return true if this expression is a variable.

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

857 { return kind() == Z3_VAR_AST; }
@ Z3_VAR_AST
Definition: z3_api.h:183

◆ is_well_sorted()

bool is_well_sorted ( ) const
inline

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

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

866 { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.

◆ is_xor()

bool is_xor ( ) const
inline

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

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

◆ itos()

expr itos ( ) const
inline

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

1323  {
1324  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1325  check_error();
1326  return expr(ctx(), r);
1327  }
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 1313 of file z3++.h.

1313  {
1314  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1315  check_error();
1316  return expr(ctx(), r);
1317  }
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.

Referenced by expr::extract().

◆ lo()

unsigned lo ( ) const
inline

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

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

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

◆ loop() [1/2]

expr loop ( unsigned  lo)
inline

create a looping regular expression.

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

1333  {
1334  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1335  check_error();
1336  return expr(ctx(), r);
1337  }
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...

◆ loop() [2/2]

expr loop ( unsigned  lo,
unsigned  hi 
)
inline

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

1338  {
1339  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1340  check_error();
1341  return expr(ctx(), r);
1342  }

◆ nth()

expr nth ( expr const &  index) const
inline

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

1307  {
1308  check_context(*this, index);
1309  Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1310  check_error();
1311  return expr(ctx(), r);
1312  }
Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the element positioned at position index. The function is under-specified if the inde...

Referenced by expr::operator[]().

◆ num_args()

unsigned num_args ( ) const
inline

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

Precondition
is_app()

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

1067 { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...

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

◆ numerator()

expr numerator ( ) const
inline

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

999  {
1000  assert(is_numeral());
1001  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1002  check_error();
1003  return expr(ctx(),r);
1004  }
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.

Referenced by RatNumRef::numerator_as_long().

◆ operator Z3_app()

operator Z3_app ( ) const
inline

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

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

◆ operator=()

expr& operator= ( expr const &  n)
inline

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

751 { return static_cast<expr&>(ast::operator=(n)); }
ast & operator=(ast const &s)
Definition: z3++.h:506

◆ operator[]() [1/2]

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

index operator defined on arrays and sequences.

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

1347  {
1348  assert(is_array() || is_seq());
1349  if (is_array()) {
1350  return select(*this, index);
1351  }
1352  return nth(index);
1353  }
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:781
expr nth(expr const &index) const
Definition: z3++.h:1307
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:793
expr select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3340

◆ operator[]() [2/2]

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

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

1355  {
1356  return select(*this, index);
1357  }

◆ repeat()

expr repeat ( unsigned  i)
inline

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

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

◆ replace()

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

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

1284  {
1285  check_context(*this, src); check_context(src, dst);
1286  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1287  check_error();
1288  return expr(ctx(), r);
1289  }
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.

◆ rotate_left()

expr rotate_left ( unsigned  i)
inline

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

1258 { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.

◆ rotate_right()

expr rotate_right ( unsigned  i)
inline

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

1259 { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the right i times.

◆ simplify() [1/2]

expr simplify ( ) const
inline

Return a simplified version of this expression.

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

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

◆ simplify() [2/2]

expr simplify ( params const &  p) const
inline

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

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

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

◆ stoi()

expr stoi ( ) const
inline

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

1318  {
1319  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1320  check_error();
1321  return expr(ctx(), r);
1322  }
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.

◆ substitute() [1/2]

expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

3585  {
3586  array<Z3_ast> _dst(dst.size());
3587  for (unsigned i = 0; i < dst.size(); ++i) {
3588  _dst[i] = dst[i];
3589  }
3590  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
3591  check_error();
3592  return expr(ctx(), r);
3593  }
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,...

◆ substitute() [2/2]

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

Apply substitution. Replace src expressions by dst.

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

3572  {
3573  assert(src.size() == dst.size());
3574  array<Z3_ast> _src(src.size());
3575  array<Z3_ast> _dst(dst.size());
3576  for (unsigned i = 0; i < src.size(); ++i) {
3577  _src[i] = src[i];
3578  _dst[i] = dst[i];
3579  }
3580  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
3581  check_error();
3582  return expr(ctx(), r);
3583  }
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....

◆ unit()

expr unit ( ) const
inline

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

1290  {
1291  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1292  check_error();
1293  return expr(ctx(), r);
1294  }
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 1739 of file z3++.h.

1739  {
1740  Z3_ast r;
1741  if (a.is_int()) {
1742  expr zero = a.ctx().int_val(0);
1743  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1744  }
1745  else if (a.is_real()) {
1746  expr zero = a.ctx().real_val(0);
1747  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1748  }
1749  else {
1750  r = Z3_mk_fpa_abs(a.ctx(), a);
1751  }
1752  a.check_error();
1753  return expr(a.ctx(), r);
1754  }
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).
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.

◆ atleast

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

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

2104  {
2105  assert(es.size() > 0);
2106  context& ctx = es[0].ctx();
2107  array<Z3_ast> _es(es);
2108  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2109  ctx.check_error();
2110  return expr(ctx, r);
2111  }
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 2096 of file z3++.h.

2096  {
2097  assert(es.size() > 0);
2098  context& ctx = es[0].ctx();
2099  array<Z3_ast> _es(es);
2100  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2101  ctx.check_error();
2102  return expr(ctx, r);
2103  }
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 1905 of file z3++.h.

1905 { Z3_ast r = Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...

◆ bvadd_no_overflow

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

bit-vector overflow/underflow checks

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

1911  {
1912  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);
1913  }
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 1914 of file z3++.h.

1914  {
1915  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1916  }
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 1929 of file z3++.h.

1929  {
1930  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);
1931  }
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 1932 of file z3++.h.

1932  {
1933  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1934  }
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...

◆ bvneg_no_overflow

expr bvneg_no_overflow ( expr const &  a)
friend

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

1926  {
1927  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
1928  }
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 1923 of file z3++.h.

1923  {
1924  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1925  }
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 1917 of file z3++.h.

1917  {
1918  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1919  }
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 1920 of file z3++.h.

1920  {
1921  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);
1922  }
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

◆ concat [1/2]

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

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

2130  {
2131  check_context(a, b);
2132  Z3_ast r;
2133  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2134  Z3_ast _args[2] = { a, b };
2135  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2136  }
2137  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2138  Z3_ast _args[2] = { a, b };
2139  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2140  }
2141  else {
2142  r = Z3_mk_concat(a.ctx(), a, b);
2143  }
2144  a.ctx().check_error();
2145  return expr(a.ctx(), r);
2146  }
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.

◆ concat [2/2]

expr concat ( expr_vector const &  args)
friend

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

2148  {
2149  Z3_ast r;
2150  assert(args.size() > 0);
2151  if (args.size() == 1) {
2152  return args[0];
2153  }
2154  context& ctx = args[0].ctx();
2155  array<Z3_ast> _args(args);
2156  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
2157  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2158  }
2159  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
2160  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2161  }
2162  else {
2163  r = _args[args.size()-1];
2164  for (unsigned i = args.size()-1; i > 0; ) {
2165  --i;
2166  r = Z3_mk_concat(ctx, _args[i], r);
2167  ctx.check_error();
2168  }
2169  }
2170  ctx.check_error();
2171  return expr(ctx, r);
2172  }

◆ distinct

expr distinct ( expr_vector const &  args)
friend

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

2121  {
2122  assert(args.size() > 0);
2123  context& ctx = args[0].ctx();
2124  array<Z3_ast> _args(args);
2125  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2126  ctx.check_error();
2127  return expr(ctx, r);
2128  }
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).

◆ fma

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

FloatingPoint fused multiply-add.

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

1764  {
1765  check_context(a, b); check_context(a, c); check_context(a, rm);
1766  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1767  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
1768  a.check_error();
1769  return expr(a.ctx(), r);
1770  }
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Floating-point fused multiply-add.

◆ implies [1/3]

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

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

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

◆ implies [2/3]

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

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

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

◆ implies [3/3]

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

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

1387  {
1388  assert(a.is_bool() && b.is_bool());
1389  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1390  }
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1380
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.

◆ int2bv

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

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

1906 { Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.

◆ is_int

expr is_int ( expr const &  e)
friend

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

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

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

◆ ite

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

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

Precondition
c.is_bool()

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

1778  {
1779  check_context(c, t); check_context(c, e);
1780  assert(c.is_bool());
1781  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1782  c.check_error();
1783  return expr(c.ctx(), r);
1784  }

◆ max

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

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

1724  {
1725  check_context(a, b);
1726  Z3_ast r;
1727  if (a.is_arith()) {
1728  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1729  }
1730  else if (a.is_bv()) {
1731  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1732  }
1733  else {
1734  assert(a.is_fpa());
1735  r = Z3_mk_fpa_max(a.ctx(), a, b);
1736  }
1737  return expr(a.ctx(), r);
1738  }
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.

◆ min

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

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

1709  {
1710  check_context(a, b);
1711  Z3_ast r;
1712  if (a.is_arith()) {
1713  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1714  }
1715  else if (a.is_bv()) {
1716  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1717  }
1718  else {
1719  assert(a.is_fpa());
1720  r = Z3_mk_fpa_min(a.ctx(), a, b);
1721  }
1722  return expr(a.ctx(), r);
1723  }
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 2180 of file z3++.h.

2180  {
2181  array<Z3_ast> _args(args);
2182  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2183  args.check_error();
2184  return expr(args.ctx(), r);
2185  }
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 2174 of file z3++.h.

2174  {
2175  array<Z3_ast> _args(args);
2176  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2177  args.check_error();
2178  return expr(args.ctx(), r);
2179  }
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 1399 of file z3++.h.

1399  {
1400  if (a.is_bv()) {
1401  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1402  }
1403  else {
1404  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1405  }
1406  }
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).

◆ mod [2/3]

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

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

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

◆ mod [3/3]

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

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

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

◆ nand

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

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

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

◆ nor

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

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

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

◆ operator!

expr operator! ( expr const &  a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

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

◆ operator!= [1/3]

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

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

1475  {
1476  check_context(a, b);
1477  Z3_ast args[2] = { a, b };
1478  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1479  a.check_error();
1480  return expr(a.ctx(), r);
1481  }

◆ operator!= [2/3]

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

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

1482 { 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 1483 of file z3++.h.

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

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

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

◆ operator& [3/3]

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

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

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

◆ operator&& [1/3]

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

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

Precondition
b.is_bool()

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

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

◆ operator&& [2/3]

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

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

Precondition
a.is_bool()

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

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

◆ operator&& [3/3]

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

Return an expression representing a and b.

Precondition
a.is_bool()
b.is_bool()

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

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

◆ 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  Z3_ast args[2] = { a, b };
1522  r = Z3_mk_mul(a.ctx(), 2, args);
1523  }
1524  else if (a.is_bv() && b.is_bv()) {
1525  r = Z3_mk_bvmul(a.ctx(), a, b);
1526  }
1527  else if (a.is_fpa() && b.is_fpa()) {
1528  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1529  }
1530  else {
1531  // operator is not supported by given arguments.
1532  assert(false);
1533  }
1534  a.check_error();
1535  return expr(a.ctx(), r);
1536  }
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.

◆ operator* [2/3]

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

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

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

◆ operator* [3/3]

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

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

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

1487  {
1488  check_context(a, b);
1489  Z3_ast r = 0;
1490  if (a.is_arith() && b.is_arith()) {
1491  Z3_ast args[2] = { a, b };
1492  r = Z3_mk_add(a.ctx(), 2, args);
1493  }
1494  else if (a.is_bv() && b.is_bv()) {
1495  r = Z3_mk_bvadd(a.ctx(), a, b);
1496  }
1497  else if (a.is_seq() && b.is_seq()) {
1498  return concat(a, b);
1499  }
1500  else if (a.is_re() && b.is_re()) {
1501  Z3_ast _args[2] = { a, b };
1502  r = Z3_mk_re_union(a.ctx(), 2, _args);
1503  }
1504  else if (a.is_fpa() && b.is_fpa()) {
1505  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1506  }
1507  else {
1508  // operator is not supported by given arguments.
1509  assert(false);
1510  }
1511  a.check_error();
1512  return expr(a.ctx(), r);
1513  }
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:2130
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
Z3_ast Z3_API Z3_mk_add(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_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.

◆ 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/4]

expr operator- ( expr const &  a)
friend

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

1583  {
1584  Z3_ast r = 0;
1585  if (a.is_arith()) {
1586  r = Z3_mk_unary_minus(a.ctx(), a);
1587  }
1588  else if (a.is_bv()) {
1589  r = Z3_mk_bvneg(a.ctx(), a);
1590  }
1591  else if (a.is_fpa()) {
1592  r = Z3_mk_fpa_neg(a.ctx(), a);
1593  }
1594  else {
1595  // operator is not supported by given arguments.
1596  assert(false);
1597  }
1598  a.check_error();
1599  return expr(a.ctx(), r);
1600  }
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.

◆ operator- [2/4]

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

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

1602  {
1603  check_context(a, b);
1604  Z3_ast r = 0;
1605  if (a.is_arith() && b.is_arith()) {
1606  Z3_ast args[2] = { a, b };
1607  r = Z3_mk_sub(a.ctx(), 2, args);
1608  }
1609  else if (a.is_bv() && b.is_bv()) {
1610  r = Z3_mk_bvsub(a.ctx(), a, b);
1611  }
1612  else if (a.is_fpa() && b.is_fpa()) {
1613  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1614  }
1615  else {
1616  // operator is not supported by given arguments.
1617  assert(false);
1618  }
1619  a.check_error();
1620  return expr(a.ctx(), r);
1621  }
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
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 1622 of file z3++.h.

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

◆ operator- [4/4]

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

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

1623 { 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  {
1562  check_context(a, b);
1563  Z3_ast r = 0;
1564  if (a.is_arith() && b.is_arith()) {
1565  r = Z3_mk_div(a.ctx(), a, b);
1566  }
1567  else if (a.is_bv() && b.is_bv()) {
1568  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1569  }
1570  else if (a.is_fpa() && b.is_fpa()) {
1571  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1572  }
1573  else {
1574  // operator is not supported by given arguments.
1575  assert(false);
1576  }
1577  a.check_error();
1578  return expr(a.ctx(), r);
1579  }
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.

◆ operator/ [2/3]

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

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

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

◆ operator/ [3/3]

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

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

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

1650  {
1651  check_context(a, b);
1652  Z3_ast r = 0;
1653  if (a.is_arith() && b.is_arith()) {
1654  r = Z3_mk_lt(a.ctx(), a, b);
1655  }
1656  else if (a.is_bv() && b.is_bv()) {
1657  r = Z3_mk_bvslt(a.ctx(), a, b);
1658  }
1659  else if (a.is_fpa() && b.is_fpa()) {
1660  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1661  }
1662  else {
1663  // operator is not supported by given arguments.
1664  assert(false);
1665  }
1666  a.check_error();
1667  return expr(a.ctx(), r);
1668  }
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.

◆ operator< [2/3]

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

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

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

◆ operator< [3/3]

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

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

1670 { 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 1625 of file z3++.h.

1625  {
1626  check_context(a, b);
1627  Z3_ast r = 0;
1628  if (a.is_arith() && b.is_arith()) {
1629  r = Z3_mk_le(a.ctx(), a, b);
1630  }
1631  else if (a.is_bv() && b.is_bv()) {
1632  r = Z3_mk_bvsle(a.ctx(), a, b);
1633  }
1634  else if (a.is_fpa() && b.is_fpa()) {
1635  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1636  }
1637  else {
1638  // operator is not supported by given arguments.
1639  assert(false);
1640  }
1641  a.check_error();
1642  return expr(a.ctx(), r);
1643  }
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.

◆ operator<= [2/3]

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

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

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

◆ operator<= [3/3]

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

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

1645 { 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 1464 of file z3++.h.

1464  {
1465  check_context(a, b);
1466  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1467  a.check_error();
1468  return expr(a.ctx(), r);
1469  }
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 1470 of file z3++.h.

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

◆ operator== [3/3]

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

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

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

◆ operator> [1/3]

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

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

1672  {
1673  check_context(a, b);
1674  Z3_ast r = 0;
1675  if (a.is_arith() && b.is_arith()) {
1676  r = Z3_mk_gt(a.ctx(), a, b);
1677  }
1678  else if (a.is_bv() && b.is_bv()) {
1679  r = Z3_mk_bvsgt(a.ctx(), a, b);
1680  }
1681  else if (a.is_fpa() && b.is_fpa()) {
1682  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1683  }
1684  else {
1685  // operator is not supported by given arguments.
1686  assert(false);
1687  }
1688  a.check_error();
1689  return expr(a.ctx(), r);
1690  }
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_ast Z3_API Z3_mk_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 1691 of file z3++.h.

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

◆ operator> [3/3]

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

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

1692 { 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 1541 of file z3++.h.

1541  {
1542  check_context(a, b);
1543  Z3_ast r = 0;
1544  if (a.is_arith() && b.is_arith()) {
1545  r = Z3_mk_ge(a.ctx(), a, b);
1546  }
1547  else if (a.is_bv() && b.is_bv()) {
1548  r = Z3_mk_bvsge(a.ctx(), a, b);
1549  }
1550  else if (a.is_fpa() && b.is_fpa()) {
1551  r = Z3_mk_fpa_geq(a.ctx(), a, b);
1552  }
1553  else {
1554  // operator is not supported by given arguments.
1555  assert(false);
1556  }
1557  a.check_error();
1558  return expr(a.ctx(), r);
1559  }
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.

◆ operator>= [2/3]

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

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

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

◆ operator>= [3/3]

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

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

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

◆ operator^ [1/3]

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

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

1698 { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.

◆ operator^ [2/3]

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

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

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

◆ operator^ [3/3]

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

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

1700 { 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 1702 of file z3++.h.

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

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

◆ operator| [3/3]

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

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

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

◆ operator|| [1/3]

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

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

Precondition
b.is_bool()

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

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

◆ operator|| [2/3]

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

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

Precondition
a.is_bool()

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

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

◆ operator|| [3/3]

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

Return an expression representing a or b.

Precondition
a.is_bool()
b.is_bool()

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

1451  {
1452  check_context(a, b);
1453  assert(a.is_bool() && b.is_bool());
1454  Z3_ast args[2] = { a, b };
1455  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1456  a.check_error();
1457  return expr(a.ctx(), r);
1458  }

◆ operator~

expr operator~ ( expr const &  a)
friend

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

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

◆ pbeq

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

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

2088  {
2089  assert(es.size() > 0);
2090  context& ctx = es[0].ctx();
2091  array<Z3_ast> _es(es);
2092  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2093  ctx.check_error();
2094  return expr(ctx, r);
2095  }
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

◆ pbge

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

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

2080  {
2081  assert(es.size() > 0);
2082  context& ctx = es[0].ctx();
2083  array<Z3_ast> _es(es);
2084  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2085  ctx.check_error();
2086  return expr(ctx, r);
2087  }
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 2072 of file z3++.h.

2072  {
2073  assert(es.size() > 0);
2074  context& ctx = es[0].ctx();
2075  array<Z3_ast> _es(es);
2076  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2077  ctx.check_error();
2078  return expr(ctx, r);
2079  }
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 1395 of file z3++.h.

1395 { _Z3_MK_BIN_(a, b, Z3_mk_power); }
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.

◆ pw [2/3]

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

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

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

◆ pw [3/3]

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

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

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

◆ range

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

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

3515  {
3516  check_context(lo, hi);
3517  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3518  lo.check_error();
3519  return expr(lo.ctx(), r);
3520  }
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.

◆ rem [1/3]

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

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

1415  {
1416  if (a.is_fpa() && b.is_fpa()) {
1417  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1418  } else {
1419  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1420  }
1421  }
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.

◆ rem [2/3]

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

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

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

◆ rem [3/3]

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

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

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

◆ sqrt

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

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

1755  {
1756  check_context(a, rm);
1757  assert(a.is_fpa());
1758  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1759  a.check_error();
1760  return expr(a.ctx(), r);
1761  }
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 2112 of file z3++.h.

2112  {
2113  assert(args.size() > 0);
2114  context& ctx = args[0].ctx();
2115  array<Z3_ast> _args(args);
2116  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2117  ctx.check_error();
2118  return expr(ctx, r);
2119  }

◆ xnor

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

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

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