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_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 &i) const
 
bool is_numeral_u64 (__uint64 &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_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_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...
 
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 get_numeral_int64 () const
 Return __int64 value of numeral, throw if result cannot fit in __int64. More...
 
__uint64 get_numeral_uint64 () const
 Return __uint64 value of numeral, throw if result cannot fit in __uint64. More...
 
Z3_lbool bool_value () const
 
expr numerator () const
 
expr denominator () const
 
 operator Z3_app () const
 
func_decl decl () const
 Return the declaration associated with this application. This method assumes the expression is an application. More...
 
unsigned num_args () const
 Return the number of arguments in this application. This method assumes the expression is an application. More...
 
expr arg (unsigned i) const
 Return the i-th argument of this application. This method assumes the expression is an application. More...
 
expr body () const
 Return the 'body' of this quantifier. More...
 
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 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 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 operator~ (expr const &a)
 
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 594 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 597 of file z3++.h.

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

◆ expr() [3/3]

expr ( expr const &  n)
inline

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

598 :ast(n) {}
ast(context &c)
Definition: z3++.h:445

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

Referenced by AstRef::__bool__().

822 { 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:365
expr(context &c)
Definition: z3++.h:596
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:364

◆ at()

expr at ( expr const &  index) const
inline

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

1016  {
1017  check_context(*this, index);
1018  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1019  check_error();
1020  return expr(ctx(), r);
1021  }
Z3_error_code check_error() const
Definition: z3++.h:365
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.
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ body()

expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

829 { 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:365
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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:680

◆ bool_value()

Z3_lbool bool_value ( ) const
inline

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

780  {
781  return Z3_get_bool_value(ctx(), m_ast);
782  }
context & ctx() const
Definition: z3++.h:364
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:443

◆ contains()

expr contains ( expr const &  s)
inline

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

1010  {
1011  check_context(*this, s);
1012  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1013  check_error();
1014  return expr(ctx(), r);
1015  }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
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 807 of file z3++.h.

Referenced by expr::hi(), and expr::lo().

807 { 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:365
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:364

◆ denominator()

expr denominator ( ) const
inline

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

792  {
793  assert(is_numeral());
794  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
795  check_error();
796  return expr(ctx(),r);
797  }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
Z3_ast m_ast
Definition: z3++.h:443
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:662
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 986 of file z3++.h.

986 { 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:170
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
unsigned lo() const
Definition: z3++.h:987
unsigned hi() const
Definition: z3++.h:988
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 overloaeded as sequence concatenation and regular expression union. concat is overloaded to handle sequences and regular expressions

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

995  {
996  check_context(*this, offset); check_context(offset, length);
997  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
998  }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
expr length() const
Definition: z3++.h:1022
context & ctx() const
Definition: z3++.h:364
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
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.

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

701  {
702  assert(is_numeral() || is_algebraic());
703  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
704  }
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:688
context & ctx() const
Definition: z3++.h:364
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:443
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:662

◆ 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 the is_numeral_i function.

Precondition
is_numeral()

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

716  {
717  int result = 0;
718  if (!is_numeral_i(result)) {
719  assert(ctx().enable_exceptions());
720  if (!ctx().enable_exceptions()) return 0;
721  Z3_THROW(exception("numeral does not fit in machine int"));
722  }
723  return result;
724  }
#define Z3_THROW(x)
Definition: z3++.h:93
context & ctx() const
Definition: z3++.h:364
bool is_numeral_i(int &i) const
Definition: z3++.h:665

◆ get_numeral_int64()

__int64 get_numeral_int64 ( ) const
inline

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

Precondition
is_numeral()

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

752  {
753  assert(is_numeral());
754  __int64 result = 0;
755  if (!is_numeral_i64(result)) {
756  assert(ctx().enable_exceptions());
757  if (!ctx().enable_exceptions()) return 0;
758  Z3_THROW(exception("numeral does not fit in machine __int64"));
759  }
760  return result;
761  }
#define Z3_THROW(x)
Definition: z3++.h:93
context & ctx() const
Definition: z3++.h:364
#define __int64
Definition: z3_api.h:40
bool is_numeral_i64(__int64 &i) const
Definition: z3++.h:663
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:662

◆ 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 the is_numeral_u function.

Precondition
is_numeral()

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

735  {
736  assert(is_numeral());
737  unsigned result = 0;
738  if (!is_numeral_u(result)) {
739  assert(ctx().enable_exceptions());
740  if (!ctx().enable_exceptions()) return 0;
741  Z3_THROW(exception("numeral does not fit in machine uint"));
742  }
743  return result;
744  }
#define Z3_THROW(x)
Definition: z3++.h:93
context & ctx() const
Definition: z3++.h:364
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:666
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:662

◆ get_numeral_uint64()

__uint64 get_numeral_uint64 ( ) const
inline

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

Precondition
is_numeral()

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

769  {
770  assert(is_numeral());
771  __uint64 result = 0;
772  if (!is_numeral_u64(result)) {
773  assert(ctx().enable_exceptions());
774  if (!ctx().enable_exceptions()) return 0;
775  Z3_THROW(exception("numeral does not fit in machine __uint64"));
776  }
777  return result;
778  }
#define Z3_THROW(x)
Definition: z3++.h:93
#define __uint64
Definition: z3_api.h:44
context & ctx() const
Definition: z3++.h:364
bool is_numeral_u64(__uint64 &i) const
Definition: z3++.h:664
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:662

◆ get_sort()

sort get_sort ( ) const
inline

◆ hi()

unsigned hi ( ) const
inline

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

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

988 { 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:807
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:364
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:672
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.

◆ is_algebraic()

bool is_algebraic ( ) const
inline

Return true if expression is an algebraic number.

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

Referenced by expr::get_decimal_string().

688 { return 0 != Z3_is_algebraic_number(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:364
Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the give AST is a real algebraic number.
Z3_ast m_ast
Definition: z3++.h:443

◆ is_app()

bool is_app ( ) const
inline

Return true if this expression is an application.

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

Referenced by expr::hi(), expr::is_const(), expr::lo(), and expr::operator Z3_app().

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

◆ is_arith()

bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

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

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

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

◆ is_array()

bool is_array ( ) const
inline

Return true if this is a Array expression.

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

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

◆ is_bool()

bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

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

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

◆ is_bv()

bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

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

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

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

Referenced by solver::add().

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

◆ is_datatype()

bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

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

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

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

◆ is_int()

bool is_int ( ) const
inline

Return true if this is an integer expression.

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

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

◆ is_numeral() [1/3]

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

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

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

◆ is_numeral() [2/3]

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

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

Referenced by expr::is_numeral().

667 { 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:365
context & ctx() const
Definition: z3++.h:364
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:443
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:662

◆ is_numeral() [3/3]

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

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

Referenced by expr::is_numeral().

668 { 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:365
context & ctx() const
Definition: z3++.h:364
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:443
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:662

◆ is_numeral_i()

bool is_numeral_i ( int &  i) const
inline

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

Referenced by expr::get_numeral_int().

665 { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:365
context & ctx() const
Definition: z3++.h:364
Z3_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:443

◆ is_numeral_i64()

bool is_numeral_i64 ( __int64 i) const
inline

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

Referenced by expr::get_numeral_int64().

663 { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:365
context & ctx() const
Definition: z3++.h:364
Z3_ast m_ast
Definition: z3++.h:443
Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, __int64 *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine __int64 int...

◆ is_numeral_u()

bool is_numeral_u ( unsigned &  i) const
inline

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

Referenced by expr::get_numeral_uint().

666 { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:365
context & ctx() const
Definition: z3++.h:364
Z3_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_ast m_ast
Definition: z3++.h:443

◆ is_numeral_u64()

bool is_numeral_u64 ( __uint64 i) const
inline

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

Referenced by expr::get_numeral_uint64().

664 { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:365
context & ctx() const
Definition: z3++.h:364
Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, __uint64 *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine __uint64 int...
Z3_ast m_ast
Definition: z3++.h:443

◆ is_quantifier()

bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

Referenced by expr::body().

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

◆ is_re()

bool is_re ( ) const
inline

Return true if this is a regular expression.

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

Referenced by z3::operator+().

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

◆ is_real()

bool is_real ( ) const
inline

Return true if this is a real expression.

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

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

◆ is_relation()

bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

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

◆ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

Referenced by z3::operator+().

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

◆ is_var()

bool is_var ( ) const
inline

Return true if this expression is a variable.

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

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

◆ is_well_sorted()

bool is_well_sorted ( ) const
inline

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

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

693 { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:365
context & ctx() const
Definition: z3++.h:364
Z3_ast m_ast
Definition: z3++.h:443
Z3_bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.

◆ itos()

expr itos ( ) const
inline

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

1032  {
1033  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1034  check_error();
1035  return expr(ctx(), r);
1036  }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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 1022 of file z3++.h.

Referenced by expr::extract().

1022  {
1023  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1024  check_error();
1025  return expr(ctx(), r);
1026  }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
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:364

◆ lo()

unsigned lo ( ) const
inline

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

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

987 { 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:807
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:364
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:672
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.

◆ loop() [1/2]

expr loop ( unsigned  lo)
inline

create a looping regular expression.

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

1042  {
1043  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1044  check_error();
1045  return expr(ctx(), r);
1046  }
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 repated between lo and hi time...
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
unsigned lo() const
Definition: z3++.h:987
Z3_ast m_ast
Definition: z3++.h:443

◆ loop() [2/2]

expr loop ( unsigned  lo,
unsigned  hi 
)
inline

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

1047  {
1048  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1049  check_error();
1050  return expr(ctx(), r);
1051  }
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 repated between lo and hi time...
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
unsigned lo() const
Definition: z3++.h:987
unsigned hi() const
Definition: z3++.h:988
Z3_ast m_ast
Definition: z3++.h:443

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

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

814 { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:365
context & ctx() const
Definition: z3++.h:364
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...

◆ numerator()

expr numerator ( ) const
inline

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

784  {
785  assert(is_numeral());
786  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
787  check_error();
788  return expr(ctx(),r);
789  }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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:443
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:662

◆ operator Z3_app()

operator Z3_app ( ) const
inline

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

799 { 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:672
Z3_ast m_ast
Definition: z3++.h:443

◆ operator=()

expr& operator= ( expr const &  n)
inline

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

599 { return static_cast<expr&>(ast::operator=(n)); }
expr(context &c)
Definition: z3++.h:596
ast & operator=(ast const &s)
Definition: z3++.h:451

◆ repeat()

expr repeat ( unsigned  i)
inline

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

983 { 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:170
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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 999 of file z3++.h.

999  {
1000  check_context(*this, src); check_context(src, dst);
1001  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1002  check_error();
1003  return expr(ctx(), r);
1004  }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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:368

◆ rotate_left()

expr rotate_left ( unsigned  i)
inline

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

981 { 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:170
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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 982 of file z3++.h.

982 { 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:170
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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 1057 of file z3++.h.

1057 { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_ast m_ast
Definition: z3++.h:443

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

1061 { 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:365
expr(context &c)
Definition: z3++.h:596
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:364
Z3_ast m_ast
Definition: z3++.h:443

◆ stoi()

expr stoi ( ) const
inline

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

1027  {
1028  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1029  check_error();
1030  return expr(ctx(), r);
1031  }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
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:364

◆ substitute() [1/2]

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

Apply substitution. Replace src expressions by dst.

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

2893  {
2894  assert(src.size() == dst.size());
2895  array<Z3_ast> _src(src.size());
2896  array<Z3_ast> _dst(dst.size());
2897  for (unsigned i = 0; i < src.size(); ++i) {
2898  _src[i] = src[i];
2899  _dst[i] = dst[i];
2900  }
2901  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
2902  check_error();
2903  return expr(ctx(), r);
2904  }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
context & ctx() const
Definition: z3++.h:364
Z3_ast m_ast
Definition: z3++.h:443

◆ substitute() [2/2]

expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

2906  {
2907  array<Z3_ast> _dst(dst.size());
2908  for (unsigned i = 0; i < dst.size(); ++i) {
2909  _dst[i] = dst[i];
2910  }
2911  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
2912  check_error();
2913  return expr(ctx(), r);
2914  }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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:443

◆ unit()

expr unit ( ) const
inline

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

1005  {
1006  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1007  check_error();
1008  return expr(ctx(), r);
1009  }
Z3_error_code check_error() const
Definition: z3++.h:365
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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

◆ atleast

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

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

1667  {
1668  assert(es.size() > 0);
1669  context& ctx = es[0].ctx();
1670  array<Z3_ast> _es(es);
1671  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
1672  ctx.check_error();
1673  return expr(ctx, r);
1674  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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 1659 of file z3++.h.

1659  {
1660  assert(es.size() > 0);
1661  context& ctx = es[0].ctx();
1662  array<Z3_ast> _es(es);
1663  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
1664  ctx.check_error();
1665  return expr(ctx, r);
1666  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ concat [1/2]

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

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

1693  {
1694  check_context(a, b);
1695  Z3_ast r;
1696  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
1697  Z3_ast _args[2] = { a, b };
1698  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
1699  }
1700  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
1701  Z3_ast _args[2] = { a, b };
1702  r = Z3_mk_re_concat(a.ctx(), 2, _args);
1703  }
1704  else {
1705  r = Z3_mk_concat(a.ctx(), a, b);
1706  }
1707  a.ctx().check_error();
1708  return expr(a.ctx(), r);
1709  }
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:596
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.
Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
Z3_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 1711 of file z3++.h.

1711  {
1712  Z3_ast r;
1713  assert(args.size() > 0);
1714  if (args.size() == 1) {
1715  return args[0];
1716  }
1717  context& ctx = args[0].ctx();
1718  array<Z3_ast> _args(args);
1719  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
1720  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
1721  }
1722  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
1723  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
1724  }
1725  else {
1726  r = _args[args.size()-1];
1727  for (unsigned i = args.size()-1; i > 0; ) {
1728  --i;
1729  r = Z3_mk_concat(ctx, _args[i], r);
1730  ctx.check_error();
1731  }
1732  }
1733  ctx.check_error();
1734  return expr(ctx, r);
1735  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
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:596
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.
Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
context & ctx() const
Definition: z3++.h:364
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:604
Z3_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 1684 of file z3++.h.

1684  {
1685  assert(args.size() > 0);
1686  context& ctx = args[0].ctx();
1687  array<Z3_ast> _args(args);
1688  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1689  ctx.check_error();
1690  return expr(ctx, r);
1691  }
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:170
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364

◆ implies [1/3]

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

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

1082  {
1083  assert(a.is_bool() && b.is_bool());
1084  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1085  }
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:1075

◆ implies [2/3]

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

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

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

◆ implies [3/3]

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

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

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

◆ is_int

expr is_int ( expr const &  e)
friend

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

1112 { _Z3_MK_UN_(e, Z3_mk_is_int); }
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1104
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 1366 of file z3++.h.

1366  {
1367  check_context(c, t); check_context(c, e);
1368  assert(c.is_bool());
1369  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1370  c.check_error();
1371  return expr(c.ctx(), r);
1372  }
expr(context &c)
Definition: z3++.h:596
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
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).

◆ mk_and

expr mk_and ( expr_vector const &  args)
friend

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

1743  {
1744  array<Z3_ast> _args(args);
1745  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
1746  args.check_error();
1747  return expr(args.ctx(), r);
1748  }
expr(context &c)
Definition: z3++.h:596
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 1737 of file z3++.h.

1737  {
1738  array<Z3_ast> _args(args);
1739  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
1740  args.check_error();
1741  return expr(args.ctx(), r);
1742  }
expr(context &c)
Definition: z3++.h:596
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 1094 of file z3++.h.

1094 { _Z3_MK_BIN_(a, b, Z3_mk_mod); }
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1075

◆ mod [2/3]

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

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

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

◆ mod [3/3]

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

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

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

◆ nand

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

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

1352 { 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:596
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:368

◆ nor

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

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

1353 { 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:596
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ operator & [1/3]

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

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

1340 { 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:596
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
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 1341 of file z3++.h.

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

◆ operator & [3/3]

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

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

1342 { 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 1116 of file z3++.h.

1116  {
1117  check_context(a, b);
1118  assert(a.is_bool() && b.is_bool());
1119  Z3_ast args[2] = { a, b };
1120  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1121  a.check_error();
1122  return expr(a.ctx(), r);
1123  }
expr(context &c)
Definition: z3++.h:596
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:368

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

1125 { 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 1126 of file z3++.h.

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

◆ operator!

expr operator! ( expr const &  a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

1110 { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1104
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 1150 of file z3++.h.

1150  {
1151  check_context(a, b);
1152  Z3_ast args[2] = { a, b };
1153  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1154  a.check_error();
1155  return expr(a.ctx(), r);
1156  }
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:596
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ operator!= [2/3]

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

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

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

◆ operator!= [3/3]

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

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

1158 { assert(b.is_arith() || b.is_bv()); 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 1187 of file z3++.h.

1187  {
1188  check_context(a, b);
1189  Z3_ast r = 0;
1190  if (a.is_arith() && b.is_arith()) {
1191  Z3_ast args[2] = { a, b };
1192  r = Z3_mk_mul(a.ctx(), 2, args);
1193  }
1194  else if (a.is_bv() && b.is_bv()) {
1195  r = Z3_mk_bvmul(a.ctx(), a, b);
1196  }
1197  else {
1198  // operator is not supported by given arguments.
1199  assert(false);
1200  }
1201  a.check_error();
1202  return expr(a.ctx(), r);
1203  }
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:596
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement multiplication.

◆ operator* [2/3]

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

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

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

◆ operator* [3/3]

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

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

1205 { 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 1160 of file z3++.h.

1160  {
1161  check_context(a, b);
1162  Z3_ast r = 0;
1163  if (a.is_arith() && b.is_arith()) {
1164  Z3_ast args[2] = { a, b };
1165  r = Z3_mk_add(a.ctx(), 2, args);
1166  }
1167  else if (a.is_bv() && b.is_bv()) {
1168  r = Z3_mk_bvadd(a.ctx(), a, b);
1169  }
1170  else if (a.is_seq() && b.is_seq()) {
1171  return concat(a, b);
1172  }
1173  else if (a.is_re() && b.is_re()) {
1174  Z3_ast _args[2] = { a, b };
1175  r = Z3_mk_re_union(a.ctx(), 2, _args);
1176  }
1177  else {
1178  // operator is not supported by given arguments.
1179  assert(false);
1180  }
1181  a.check_error();
1182  return expr(a.ctx(), r);
1183  }
expr(context &c)
Definition: z3++.h:596
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:1693
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:368
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&#39;s complement addition.

◆ operator+ [2/3]

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

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

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

◆ operator+ [3/3]

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

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

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

◆ operator- [1/4]

expr operator- ( expr const &  a)
friend

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

1244  {
1245  Z3_ast r = 0;
1246  if (a.is_arith()) {
1247  r = Z3_mk_unary_minus(a.ctx(), a);
1248  }
1249  else if (a.is_bv()) {
1250  r = Z3_mk_bvneg(a.ctx(), a);
1251  }
1252  else {
1253  // operator is not supported by given arguments.
1254  assert(false);
1255  }
1256  a.check_error();
1257  return expr(a.ctx(), r);
1258  }
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:596
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two&#39;s complement unary minus.

◆ operator- [2/4]

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

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

1260  {
1261  check_context(a, b);
1262  Z3_ast r = 0;
1263  if (a.is_arith() && b.is_arith()) {
1264  Z3_ast args[2] = { a, b };
1265  r = Z3_mk_sub(a.ctx(), 2, args);
1266  }
1267  else if (a.is_bv() && b.is_bv()) {
1268  r = Z3_mk_bvsub(a.ctx(), a, b);
1269  }
1270  else {
1271  // operator is not supported by given arguments.
1272  assert(false);
1273  }
1274  a.check_error();
1275  return expr(a.ctx(), r);
1276  }
expr(context &c)
Definition: z3++.h:596
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
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&#39;s complement subtraction.

◆ operator- [3/4]

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

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

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

◆ operator- [4/4]

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

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

1278 { 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 1225 of file z3++.h.

1225  {
1226  check_context(a, b);
1227  Z3_ast r = 0;
1228  if (a.is_arith() && b.is_arith()) {
1229  r = Z3_mk_div(a.ctx(), a, b);
1230  }
1231  else if (a.is_bv() && b.is_bv()) {
1232  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1233  }
1234  else {
1235  // operator is not supported by given arguments.
1236  assert(false);
1237  }
1238  a.check_error();
1239  return expr(a.ctx(), r);
1240  }
expr(context &c)
Definition: z3++.h:596
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;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:368

◆ operator/ [2/3]

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

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

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

◆ operator/ [3/3]

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

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

1242 { 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 1302 of file z3++.h.

1302  {
1303  check_context(a, b);
1304  Z3_ast r = 0;
1305  if (a.is_arith() && b.is_arith()) {
1306  r = Z3_mk_lt(a.ctx(), a, b);
1307  }
1308  else if (a.is_bv() && b.is_bv()) {
1309  r = Z3_mk_bvslt(a.ctx(), a, b);
1310  }
1311  else {
1312  // operator is not supported by given arguments.
1313  assert(false);
1314  }
1315  a.check_error();
1316  return expr(a.ctx(), r);
1317  }
expr(context &c)
Definition: z3++.h:596
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;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:368

◆ operator< [2/3]

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

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

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

◆ operator< [3/3]

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

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

1319 { 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 1280 of file z3++.h.

1280  {
1281  check_context(a, b);
1282  Z3_ast r = 0;
1283  if (a.is_arith() && b.is_arith()) {
1284  r = Z3_mk_le(a.ctx(), a, b);
1285  }
1286  else if (a.is_bv() && b.is_bv()) {
1287  r = Z3_mk_bvsle(a.ctx(), a, b);
1288  }
1289  else {
1290  // operator is not supported by given arguments.
1291  assert(false);
1292  }
1293  a.check_error();
1294  return expr(a.ctx(), r);
1295  }
expr(context &c)
Definition: z3++.h:596
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&#39;s complement signed less than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ operator<= [2/3]

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

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

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

◆ operator<= [3/3]

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

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

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

1141  {
1142  check_context(a, b);
1143  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1144  a.check_error();
1145  return expr(a.ctx(), r);
1146  }
expr(context &c)
Definition: z3++.h:596
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
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 1147 of file z3++.h.

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

◆ operator== [3/3]

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

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

1148 { assert(b.is_arith() || b.is_bv()); 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 1321 of file z3++.h.

1321  {
1322  check_context(a, b);
1323  Z3_ast r = 0;
1324  if (a.is_arith() && b.is_arith()) {
1325  r = Z3_mk_gt(a.ctx(), a, b);
1326  }
1327  else if (a.is_bv() && b.is_bv()) {
1328  r = Z3_mk_bvsgt(a.ctx(), a, b);
1329  }
1330  else {
1331  // operator is not supported by given arguments.
1332  assert(false);
1333  }
1334  a.check_error();
1335  return expr(a.ctx(), r);
1336  }
expr(context &c)
Definition: z3++.h:596
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed greater than.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.

◆ operator> [2/3]

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

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

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

◆ operator> [3/3]

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

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

1338 { 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 1208 of file z3++.h.

1208  {
1209  check_context(a, b);
1210  Z3_ast r = 0;
1211  if (a.is_arith() && b.is_arith()) {
1212  r = Z3_mk_ge(a.ctx(), a, b);
1213  }
1214  else if (a.is_bv() && b.is_bv()) {
1215  r = Z3_mk_bvsge(a.ctx(), a, b);
1216  }
1217  else {
1218  // operator is not supported by given arguments.
1219  assert(false);
1220  }
1221  a.check_error();
1222  return expr(a.ctx(), r);
1223  }
expr(context &c)
Definition: z3++.h:596
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&#39;s complement signed greater than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ operator>= [2/3]

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

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

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

◆ operator>= [3/3]

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

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

1300 { 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 1344 of file z3++.h.

1344 { 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:596
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
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 1345 of file z3++.h.

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

◆ operator^ [3/3]

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

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

1346 { 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 1348 of file z3++.h.

1348 { 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:596
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
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 1349 of file z3++.h.

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

◆ operator| [3/3]

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

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

1350 { 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 1128 of file z3++.h.

1128  {
1129  check_context(a, b);
1130  assert(a.is_bool() && b.is_bool());
1131  Z3_ast args[2] = { a, b };
1132  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1133  a.check_error();
1134  return expr(a.ctx(), r);
1135  }
expr(context &c)
Definition: z3++.h:596
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:368

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

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

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

◆ operator~

expr operator~ ( expr const &  a)
friend

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

1356 { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:596
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 1651 of file z3++.h.

1651  {
1652  assert(es.size() > 0);
1653  context& ctx = es[0].ctx();
1654  array<Z3_ast> _es(es);
1655  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
1656  ctx.check_error();
1657  return expr(ctx, r);
1658  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
expr(context &c)
Definition: z3++.h:596
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:364

◆ pbge

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

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

1643  {
1644  assert(es.size() > 0);
1645  context& ctx = es[0].ctx();
1646  array<Z3_ast> _es(es);
1647  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
1648  ctx.check_error();
1649  return expr(ctx, r);
1650  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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 1635 of file z3++.h.

1635  {
1636  assert(es.size() > 0);
1637  context& ctx = es[0].ctx();
1638  array<Z3_ast> _es(es);
1639  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
1640  ctx.check_error();
1641  return expr(ctx, r);
1642  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
expr(context &c)
Definition: z3++.h:596
context & ctx() const
Definition: z3++.h:364
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 1090 of file z3++.h.

1090 { _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:1075

◆ pw [2/3]

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

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

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

◆ pw [3/3]

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

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

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

◆ range

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

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

2813  {
2814  check_context(lo, hi);
2815  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
2816  lo.check_error();
2817  return expr(lo.ctx(), r);
2818  }
expr(context &c)
Definition: z3++.h:596
unsigned lo() const
Definition: z3++.h:987
friend void check_context(object const &a, object const &b)
Definition: z3++.h:368
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:988

◆ rem [1/3]

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

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

1098 { _Z3_MK_BIN_(a, b, Z3_mk_rem); }
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1075

◆ rem [2/3]

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

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

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

◆ rem [3/3]

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

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

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

◆ sum

expr sum ( expr_vector const &  args)
friend

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

1675  {
1676  assert(args.size() > 0);
1677  context& ctx = args[0].ctx();
1678  array<Z3_ast> _args(args);
1679  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
1680  ctx.check_error();
1681  return expr(ctx, r);
1682  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:170
expr(context &c)
Definition: z3++.h:596
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:364

◆ xnor

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

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

1354 { 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:596
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:368