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

Constructor & Destructor Documentation

§ expr() [1/3]

expr ( context c)
inline

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

605 :ast(c) {}
ast(context &c)
Definition: z3++.h:454

§ expr() [2/3]

expr ( context c,
Z3_ast  n 
)
inline

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

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

§ expr() [3/3]

expr ( expr const &  n)
inline

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

607 :ast(n) {}
ast(context &c)
Definition: z3++.h:454

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

Referenced by AstRef::__bool__().

831 { 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:374
expr(context &c)
Definition: z3++.h:605
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:373

§ at()

expr at ( expr const &  index) const
inline

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

1025  {
1026  check_context(*this, index);
1027  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1028  check_error();
1029  return expr(ctx(), r);
1030  }
Z3_error_code check_error() const
Definition: z3++.h:374
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:605
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

§ body()

expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

838 { 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:374
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
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:689

§ bool_value()

Z3_lbool bool_value ( ) const
inline

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

789  {
790  return Z3_get_bool_value(ctx(), m_ast);
791  }
context & ctx() const
Definition: z3++.h:373
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:452

§ contains()

expr contains ( expr const &  s)
inline

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

1019  {
1020  check_context(*this, s);
1021  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1022  check_error();
1023  return expr(ctx(), r);
1024  }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
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 816 of file z3++.h.

816 { 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:374
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:373

§ denominator()

expr denominator ( ) const
inline

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

801  {
802  assert(is_numeral());
803  Z3_ast r = Z3_get_denominator(ctx(), m_ast);
804  check_error();
805  return expr(ctx(),r);
806  }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
Z3_ast m_ast
Definition: z3++.h:452
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:671
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 995 of file z3++.h.

995 { 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:605
context & ctx() const
Definition: z3++.h:373
unsigned lo() const
Definition: z3++.h:996
unsigned hi() const
Definition: z3++.h:997
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n...

§ extract() [2/2]

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

sequence and regular expression operations.

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

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

1004  {
1005  check_context(*this, offset); check_context(offset, length);
1006  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1007  }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
expr length() const
Definition: z3++.h:1031
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
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 710 of file z3++.h.

710  {
711  assert(is_numeral() || is_algebraic());
712  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
713  }
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:697
context & ctx() const
Definition: z3++.h:373
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:452
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:671

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

725  {
726  int result = 0;
727  if (!is_numeral_i(result)) {
728  assert(ctx().enable_exceptions());
729  if (!ctx().enable_exceptions()) return 0;
730  Z3_THROW(exception("numeral does not fit in machine int"));
731  }
732  return result;
733  }
#define Z3_THROW(x)
Definition: z3++.h:93
context & ctx() const
Definition: z3++.h:373
bool is_numeral_i(int &i) const
Definition: z3++.h:674

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

761  {
762  assert(is_numeral());
763  int64_t result = 0;
764  if (!is_numeral_i64(result)) {
765  assert(ctx().enable_exceptions());
766  if (!ctx().enable_exceptions()) return 0;
767  Z3_THROW(exception("numeral does not fit in machine int64_t"));
768  }
769  return result;
770  }
#define Z3_THROW(x)
Definition: z3++.h:93
bool is_numeral_i64(int64_t &i) const
Definition: z3++.h:672
context & ctx() const
Definition: z3++.h:373
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:671

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

744  {
745  assert(is_numeral());
746  unsigned result = 0;
747  if (!is_numeral_u(result)) {
748  assert(ctx().enable_exceptions());
749  if (!ctx().enable_exceptions()) return 0;
750  Z3_THROW(exception("numeral does not fit in machine uint"));
751  }
752  return result;
753  }
#define Z3_THROW(x)
Definition: z3++.h:93
context & ctx() const
Definition: z3++.h:373
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:675
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:671

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

778  {
779  assert(is_numeral());
780  uint64_t result = 0;
781  if (!is_numeral_u64(result)) {
782  assert(ctx().enable_exceptions());
783  if (!ctx().enable_exceptions()) return 0;
784  Z3_THROW(exception("numeral does not fit in machine uint64_t"));
785  }
786  return result;
787  }
#define Z3_THROW(x)
Definition: z3++.h:93
context & ctx() const
Definition: z3++.h:373
bool is_numeral_u64(uint64_t &i) const
Definition: z3++.h:673
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:671

§ get_sort()

sort get_sort ( ) const
inline

Return the sort of this expression.

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

Referenced by z3::ashr(), z3::concat(), z3::lshr(), z3::mod(), z3::operator &(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::operator^(), z3::operator|(), z3::pw(), z3::rem(), z3::select(), z3::shl(), z3::smod(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().

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

§ hi()

unsigned hi ( ) const
inline

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

997 { 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:816
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:373
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:681
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 697 of file z3++.h.

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

§ is_app()

bool is_app ( ) const
inline

Return true if this expression is an application.

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

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

§ is_arith()

bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

Definition at line 630 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>=().

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

§ is_array()

bool is_array ( ) const
inline

Return true if this is a Array expression.

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

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

§ is_bool()

bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

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

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

§ is_bv()

bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

Definition at line 634 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>=().

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

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

Referenced by solver::add().

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

§ is_datatype()

bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

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

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

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

§ is_int()

bool is_int ( ) const
inline

Return true if this is an integer expression.

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

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

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

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

§ is_numeral() [2/3]

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

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

Referenced by expr::is_numeral().

676 { 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:374
context & ctx() const
Definition: z3++.h:373
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:452
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:671

§ is_numeral() [3/3]

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

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

Referenced by expr::is_numeral().

677 { 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:374
context & ctx() const
Definition: z3++.h:373
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:452
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:671

§ is_numeral_i()

bool is_numeral_i ( int &  i) const
inline

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

674 { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:374
context & ctx() const
Definition: z3++.h:373
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:452

§ is_numeral_i64()

bool is_numeral_i64 ( int64_t &  i) const
inline

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

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

§ is_numeral_u()

bool is_numeral_u ( unsigned &  i) const
inline

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

675 { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
Z3_error_code check_error() const
Definition: z3++.h:374
context & ctx() const
Definition: z3++.h:373
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:452

§ is_numeral_u64()

bool is_numeral_u64 ( uint64_t &  i) const
inline

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

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

§ is_quantifier()

bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

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

§ is_re()

bool is_re ( ) const
inline

Return true if this is a regular expression.

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

Referenced by z3::operator+().

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

§ is_real()

bool is_real ( ) const
inline

Return true if this is a real expression.

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

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

§ is_relation()

bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

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

§ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

Referenced by z3::operator+().

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

§ is_var()

bool is_var ( ) const
inline

Return true if this expression is a variable.

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

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

§ is_well_sorted()

bool is_well_sorted ( ) const
inline

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

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

702 { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:374
context & ctx() const
Definition: z3++.h:373
Z3_ast m_ast
Definition: z3++.h:452
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 1041 of file z3++.h.

1041  {
1042  Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1043  check_error();
1044  return expr(ctx(), r);
1045  }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
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 1031 of file z3++.h.

1031  {
1032  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1033  check_error();
1034  return expr(ctx(), r);
1035  }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
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:373

§ lo()

unsigned lo ( ) const
inline

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

996 { 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:816
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:373
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:681
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 1051 of file z3++.h.

1051  {
1052  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1053  check_error();
1054  return expr(ctx(), r);
1055  }
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
unsigned lo() const
Definition: z3++.h:996
Z3_ast m_ast
Definition: z3++.h:452

§ loop() [2/2]

expr loop ( unsigned  lo,
unsigned  hi 
)
inline

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

1056  {
1057  Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1058  check_error();
1059  return expr(ctx(), r);
1060  }
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
unsigned lo() const
Definition: z3++.h:996
unsigned hi() const
Definition: z3++.h:997
Z3_ast m_ast
Definition: z3++.h:452

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

Referenced by AstRef::__bool__().

823 { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
Z3_error_code check_error() const
Definition: z3++.h:374
context & ctx() const
Definition: z3++.h:373
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 793 of file z3++.h.

793  {
794  assert(is_numeral());
795  Z3_ast r = Z3_get_numerator(ctx(), m_ast);
796  check_error();
797  return expr(ctx(),r);
798  }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
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:452
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:671

§ operator Z3_app()

operator Z3_app ( ) const
inline

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

808 { 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:681
Z3_ast m_ast
Definition: z3++.h:452

§ operator=()

expr& operator= ( expr const &  n)
inline

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

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

§ repeat()

expr repeat ( unsigned  i)
inline

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

992 { 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:605
context & ctx() const
Definition: z3++.h:373
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 1008 of file z3++.h.

1008  {
1009  check_context(*this, src); check_context(src, dst);
1010  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1011  check_error();
1012  return expr(ctx(), r);
1013  }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
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:377

§ rotate_left()

expr rotate_left ( unsigned  i)
inline

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

990 { 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:605
context & ctx() const
Definition: z3++.h:373
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 991 of file z3++.h.

991 { 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:605
context & ctx() const
Definition: z3++.h:373
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 1066 of file z3++.h.

1066 { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_ast m_ast
Definition: z3++.h:452

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

1070 { 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:374
expr(context &c)
Definition: z3++.h:605
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:373
Z3_ast m_ast
Definition: z3++.h:452

§ stoi()

expr stoi ( ) const
inline

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

1036  {
1037  Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1038  check_error();
1039  return expr(ctx(), r);
1040  }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
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:373

§ substitute() [1/2]

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

Apply substitution. Replace src expressions by dst.

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

2948  {
2949  assert(src.size() == dst.size());
2950  array<Z3_ast> _src(src.size());
2951  array<Z3_ast> _dst(dst.size());
2952  for (unsigned i = 0; i < src.size(); ++i) {
2953  _src[i] = src[i];
2954  _dst[i] = dst[i];
2955  }
2956  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
2957  check_error();
2958  return expr(ctx(), r);
2959  }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
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:373
Z3_ast m_ast
Definition: z3++.h:452

§ substitute() [2/2]

expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

2961  {
2962  array<Z3_ast> _dst(dst.size());
2963  for (unsigned i = 0; i < dst.size(); ++i) {
2964  _dst[i] = dst[i];
2965  }
2966  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
2967  check_error();
2968  return expr(ctx(), r);
2969  }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
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:452

§ unit()

expr unit ( ) const
inline

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

1014  {
1015  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1016  check_error();
1017  return expr(ctx(), r);
1018  }
Z3_error_code check_error() const
Definition: z3++.h:374
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
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 1676 of file z3++.h.

1676  {
1677  assert(es.size() > 0);
1678  context& ctx = es[0].ctx();
1679  array<Z3_ast> _es(es);
1680  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
1681  ctx.check_error();
1682  return expr(ctx, r);
1683  }
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
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 1668 of file z3++.h.

1668  {
1669  assert(es.size() > 0);
1670  context& ctx = es[0].ctx();
1671  array<Z3_ast> _es(es);
1672  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
1673  ctx.check_error();
1674  return expr(ctx, r);
1675  }
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
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 1702 of file z3++.h.

1702  {
1703  check_context(a, b);
1704  Z3_ast r;
1705  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
1706  Z3_ast _args[2] = { a, b };
1707  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
1708  }
1709  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
1710  Z3_ast _args[2] = { a, b };
1711  r = Z3_mk_re_concat(a.ctx(), 2, _args);
1712  }
1713  else {
1714  r = Z3_mk_concat(a.ctx(), a, b);
1715  }
1716  a.ctx().check_error();
1717  return expr(a.ctx(), r);
1718  }
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:605
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:377
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 1720 of file z3++.h.

1720  {
1721  Z3_ast r;
1722  assert(args.size() > 0);
1723  if (args.size() == 1) {
1724  return args[0];
1725  }
1726  context& ctx = args[0].ctx();
1727  array<Z3_ast> _args(args);
1728  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
1729  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
1730  }
1731  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
1732  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
1733  }
1734  else {
1735  r = _args[args.size()-1];
1736  for (unsigned i = args.size()-1; i > 0; ) {
1737  --i;
1738  r = Z3_mk_concat(ctx, _args[i], r);
1739  ctx.check_error();
1740  }
1741  }
1742  ctx.check_error();
1743  return expr(ctx, r);
1744  }
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:605
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:373
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:613
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 1693 of file z3++.h.

1693  {
1694  assert(args.size() > 0);
1695  context& ctx = args[0].ctx();
1696  array<Z3_ast> _args(args);
1697  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1698  ctx.check_error();
1699  return expr(ctx, r);
1700  }
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:605
context & ctx() const
Definition: z3++.h:373

§ implies [1/3]

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

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

1091  {
1092  assert(a.is_bool() && b.is_bool());
1093  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1094  }
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:1084

§ implies [2/3]

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

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

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

§ implies [3/3]

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

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

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

§ is_int

expr is_int ( expr const &  e)
friend

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

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

1375  {
1376  check_context(c, t); check_context(c, e);
1377  assert(c.is_bool());
1378  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1379  c.check_error();
1380  return expr(c.ctx(), r);
1381  }
expr(context &c)
Definition: z3++.h:605
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
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 1752 of file z3++.h.

1752  {
1753  array<Z3_ast> _args(args);
1754  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
1755  args.check_error();
1756  return expr(args.ctx(), r);
1757  }
expr(context &c)
Definition: z3++.h:605
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 1746 of file z3++.h.

1746  {
1747  array<Z3_ast> _args(args);
1748  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
1749  args.check_error();
1750  return expr(args.ctx(), r);
1751  }
expr(context &c)
Definition: z3++.h:605
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 1103 of file z3++.h.

1103 { _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:1084

§ mod [2/3]

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

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

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

§ mod [3/3]

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

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

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

§ nand

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

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

1361 { 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:605
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:377

§ nor

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

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

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

§ operator & [1/3]

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

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

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

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

§ operator & [3/3]

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

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

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

1125  {
1126  check_context(a, b);
1127  assert(a.is_bool() && b.is_bool());
1128  Z3_ast args[2] = { a, b };
1129  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1130  a.check_error();
1131  return expr(a.ctx(), r);
1132  }
expr(context &c)
Definition: z3++.h:605
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:377

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

1134 { 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 1135 of file z3++.h.

1135 { 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 1119 of file z3++.h.

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

1159  {
1160  check_context(a, b);
1161  Z3_ast args[2] = { a, b };
1162  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1163  a.check_error();
1164  return expr(a.ctx(), r);
1165  }
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:605
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

§ operator!= [2/3]

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

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

1166 { 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 1167 of file z3++.h.

1167 { 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 1196 of file z3++.h.

1196  {
1197  check_context(a, b);
1198  Z3_ast r = 0;
1199  if (a.is_arith() && b.is_arith()) {
1200  Z3_ast args[2] = { a, b };
1201  r = Z3_mk_mul(a.ctx(), 2, args);
1202  }
1203  else if (a.is_bv() && b.is_bv()) {
1204  r = Z3_mk_bvmul(a.ctx(), a, b);
1205  }
1206  else {
1207  // operator is not supported by given arguments.
1208  assert(false);
1209  }
1210  a.check_error();
1211  return expr(a.ctx(), r);
1212  }
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:605
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
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 1213 of file z3++.h.

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

§ operator* [3/3]

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

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

1214 { 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 1169 of file z3++.h.

1169  {
1170  check_context(a, b);
1171  Z3_ast r = 0;
1172  if (a.is_arith() && b.is_arith()) {
1173  Z3_ast args[2] = { a, b };
1174  r = Z3_mk_add(a.ctx(), 2, args);
1175  }
1176  else if (a.is_bv() && b.is_bv()) {
1177  r = Z3_mk_bvadd(a.ctx(), a, b);
1178  }
1179  else if (a.is_seq() && b.is_seq()) {
1180  return concat(a, b);
1181  }
1182  else if (a.is_re() && b.is_re()) {
1183  Z3_ast _args[2] = { a, b };
1184  r = Z3_mk_re_union(a.ctx(), 2, _args);
1185  }
1186  else {
1187  // operator is not supported by given arguments.
1188  assert(false);
1189  }
1190  a.check_error();
1191  return expr(a.ctx(), r);
1192  }
expr(context &c)
Definition: z3++.h:605
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:1702
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:377
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 1193 of file z3++.h.

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

§ operator+ [3/3]

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

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

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

§ operator- [1/4]

expr operator- ( expr const &  a)
friend

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

1253  {
1254  Z3_ast r = 0;
1255  if (a.is_arith()) {
1256  r = Z3_mk_unary_minus(a.ctx(), a);
1257  }
1258  else if (a.is_bv()) {
1259  r = Z3_mk_bvneg(a.ctx(), a);
1260  }
1261  else {
1262  // operator is not supported by given arguments.
1263  assert(false);
1264  }
1265  a.check_error();
1266  return expr(a.ctx(), r);
1267  }
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:605
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 1269 of file z3++.h.

1269  {
1270  check_context(a, b);
1271  Z3_ast r = 0;
1272  if (a.is_arith() && b.is_arith()) {
1273  Z3_ast args[2] = { a, b };
1274  r = Z3_mk_sub(a.ctx(), 2, args);
1275  }
1276  else if (a.is_bv() && b.is_bv()) {
1277  r = Z3_mk_bvsub(a.ctx(), a, b);
1278  }
1279  else {
1280  // operator is not supported by given arguments.
1281  assert(false);
1282  }
1283  a.check_error();
1284  return expr(a.ctx(), r);
1285  }
expr(context &c)
Definition: z3++.h:605
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
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 1286 of file z3++.h.

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

§ operator- [4/4]

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

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

1287 { 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 1234 of file z3++.h.

1234  {
1235  check_context(a, b);
1236  Z3_ast r = 0;
1237  if (a.is_arith() && b.is_arith()) {
1238  r = Z3_mk_div(a.ctx(), a, b);
1239  }
1240  else if (a.is_bv() && b.is_bv()) {
1241  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1242  }
1243  else {
1244  // operator is not supported by given arguments.
1245  assert(false);
1246  }
1247  a.check_error();
1248  return expr(a.ctx(), r);
1249  }
expr(context &c)
Definition: z3++.h:605
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:377

§ operator/ [2/3]

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

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

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

§ operator/ [3/3]

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

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

1251 { 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 1311 of file z3++.h.

1311  {
1312  check_context(a, b);
1313  Z3_ast r = 0;
1314  if (a.is_arith() && b.is_arith()) {
1315  r = Z3_mk_lt(a.ctx(), a, b);
1316  }
1317  else if (a.is_bv() && b.is_bv()) {
1318  r = Z3_mk_bvslt(a.ctx(), a, b);
1319  }
1320  else {
1321  // operator is not supported by given arguments.
1322  assert(false);
1323  }
1324  a.check_error();
1325  return expr(a.ctx(), r);
1326  }
expr(context &c)
Definition: z3++.h:605
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:377

§ operator< [2/3]

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

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

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

§ operator< [3/3]

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

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

1328 { 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 1289 of file z3++.h.

1289  {
1290  check_context(a, b);
1291  Z3_ast r = 0;
1292  if (a.is_arith() && b.is_arith()) {
1293  r = Z3_mk_le(a.ctx(), a, b);
1294  }
1295  else if (a.is_bv() && b.is_bv()) {
1296  r = Z3_mk_bvsle(a.ctx(), a, b);
1297  }
1298  else {
1299  // operator is not supported by given arguments.
1300  assert(false);
1301  }
1302  a.check_error();
1303  return expr(a.ctx(), r);
1304  }
expr(context &c)
Definition: z3++.h:605
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:377

§ operator<= [2/3]

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

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

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

§ operator<= [3/3]

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

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

1306 { 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 1150 of file z3++.h.

1150  {
1151  check_context(a, b);
1152  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1153  a.check_error();
1154  return expr(a.ctx(), r);
1155  }
expr(context &c)
Definition: z3++.h:605
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
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 1156 of file z3++.h.

1156 { 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 1157 of file z3++.h.

1157 { 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 1330 of file z3++.h.

1330  {
1331  check_context(a, b);
1332  Z3_ast r = 0;
1333  if (a.is_arith() && b.is_arith()) {
1334  r = Z3_mk_gt(a.ctx(), a, b);
1335  }
1336  else if (a.is_bv() && b.is_bv()) {
1337  r = Z3_mk_bvsgt(a.ctx(), a, b);
1338  }
1339  else {
1340  // operator is not supported by given arguments.
1341  assert(false);
1342  }
1343  a.check_error();
1344  return expr(a.ctx(), r);
1345  }
expr(context &c)
Definition: z3++.h:605
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:377
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 1346 of file z3++.h.

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

§ operator> [3/3]

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

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

1347 { 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 1217 of file z3++.h.

1217  {
1218  check_context(a, b);
1219  Z3_ast r = 0;
1220  if (a.is_arith() && b.is_arith()) {
1221  r = Z3_mk_ge(a.ctx(), a, b);
1222  }
1223  else if (a.is_bv() && b.is_bv()) {
1224  r = Z3_mk_bvsge(a.ctx(), a, b);
1225  }
1226  else {
1227  // operator is not supported by given arguments.
1228  assert(false);
1229  }
1230  a.check_error();
1231  return expr(a.ctx(), r);
1232  }
expr(context &c)
Definition: z3++.h:605
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:377

§ operator>= [2/3]

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

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

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

§ operator>= [3/3]

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

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

1309 { 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 1353 of file z3++.h.

1353 { 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:605
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
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 1354 of file z3++.h.

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

§ operator^ [3/3]

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

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

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

§ operator| [1/3]

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

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

1357 { 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:605
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
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 1358 of file z3++.h.

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

§ operator| [3/3]

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

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

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

1137  {
1138  check_context(a, b);
1139  assert(a.is_bool() && b.is_bool());
1140  Z3_ast args[2] = { a, b };
1141  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1142  a.check_error();
1143  return expr(a.ctx(), r);
1144  }
expr(context &c)
Definition: z3++.h:605
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:377

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

1146 { 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 1148 of file z3++.h.

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

§ operator~

expr operator~ ( expr const &  a)
friend

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

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

1660  {
1661  assert(es.size() > 0);
1662  context& ctx = es[0].ctx();
1663  array<Z3_ast> _es(es);
1664  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
1665  ctx.check_error();
1666  return expr(ctx, r);
1667  }
expr(context &c)
Definition: z3++.h:605
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:373

§ pbge

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

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

1652  {
1653  assert(es.size() > 0);
1654  context& ctx = es[0].ctx();
1655  array<Z3_ast> _es(es);
1656  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
1657  ctx.check_error();
1658  return expr(ctx, r);
1659  }
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
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 1644 of file z3++.h.

1644  {
1645  assert(es.size() > 0);
1646  context& ctx = es[0].ctx();
1647  array<Z3_ast> _es(es);
1648  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
1649  ctx.check_error();
1650  return expr(ctx, r);
1651  }
expr(context &c)
Definition: z3++.h:605
context & ctx() const
Definition: z3++.h:373
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 1099 of file z3++.h.

1099 { _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:1084

§ pw [2/3]

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

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

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

§ pw [3/3]

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

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

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

§ range

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

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

2868  {
2869  check_context(lo, hi);
2870  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
2871  lo.check_error();
2872  return expr(lo.ctx(), r);
2873  }
expr(context &c)
Definition: z3++.h:605
unsigned lo() const
Definition: z3++.h:996
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
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:997

§ rem [1/3]

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

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

1107 { _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:1084

§ rem [2/3]

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

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

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

§ rem [3/3]

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

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

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

§ sum

expr sum ( 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_add(ctx, _args.size(), _args.ptr());
1689  ctx.check_error();
1690  return expr(ctx, r);
1691  }
expr(context &c)
Definition: z3++.h:605
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:373

§ xnor

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

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

1363 { 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:605
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:377