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...
 
 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 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 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
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void 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 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)
 Power operator. More...
 
expr pw (expr const &a, int b)
 
expr pw (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 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 wasoperator (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 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)
 

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

Constructor & Destructor Documentation

§ expr() [1/3]

expr ( context c)
inline

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

562 :ast(c) {}
ast(context &c)
Definition: z3++.h:413

§ expr() [2/3]

expr ( context c,
Z3_ast  n 
)
inline

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

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

§ expr() [3/3]

expr ( expr const &  n)
inline

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

564 :ast(n) {}
ast(context &c)
Definition: z3++.h:413

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

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

755 { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:562
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ at()

expr at ( expr const &  index) const
inline

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

926  {
927  check_context(*this, index);
928  Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
929  check_error();
930  return expr(ctx(), r);
931  }
expr(context &c)
Definition: z3++.h:562
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
void check_error() const
Definition: z3++.h:333

§ body()

expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

Referenced by QuantifierRef::children().

762 { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:562
context & ctx() const
Definition: z3++.h:332
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:646
void check_error() const
Definition: z3++.h:333

§ contains()

expr contains ( expr const &  s)
inline

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

920  {
921  check_context(*this, s);
922  Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
923  check_error();
924  return expr(ctx(), r);
925  }
expr(context &c)
Definition: z3++.h:562
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
void check_error() const
Definition: z3++.h:333

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

740 { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ extract() [1/2]

expr extract ( unsigned  hi,
unsigned  lo 
) const
inline

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

896 { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:562
void check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:162
context & ctx() const
Definition: z3++.h:332
unsigned lo() const
Definition: z3++.h:897
unsigned hi() const
Definition: z3++.h:898
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 905 of file z3++.h.

905  {
906  check_context(*this, offset); check_context(offset, length);
907  Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
908  }
expr(context &c)
Definition: z3++.h:562
expr length() const
Definition: z3++.h:932
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
void check_error() const
Definition: z3++.h:333

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

667  {
668  assert(is_numeral() || is_algebraic());
669  return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
670  }
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:654
context & ctx() const
Definition: z3++.h:332
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:411
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:628

§ get_numeral_int()

int get_numeral_int ( ) const
inline

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

Precondition
is_numeral()

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

678  {
679  int result;
680  if (!is_numeral_i(result)) {
681  throw exception("numeral does not fit in machine int");
682  }
683  return result;
684  }
bool is_numeral_i(int &i) const
Definition: z3++.h:631

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

707  {
708  assert(is_numeral());
709  __int64 result;
710  if (!is_numeral_i64(result)) {
711  throw exception("numeral does not fit in machine __int64");
712  }
713  return result;
714  }
#define __int64
Definition: z3_api.h:40
bool is_numeral_i64(__int64 &i) const
Definition: z3++.h:629
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:628

§ get_numeral_uint()

unsigned get_numeral_uint ( ) const
inline

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

Precondition
is_numeral()

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

692  {
693  assert(is_numeral());
694  unsigned result;
695  if (!is_numeral_u(result)) {
696  throw exception("numeral does not fit in machine uint");
697  }
698  return result;
699  }
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:632
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:628

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

722  {
723  assert(is_numeral());
724  __uint64 result;
725  if (!is_numeral_u64(result)) {
726  throw exception("numeral does not fit in machine __uint64");
727  }
728  return result;
729  }
#define __uint64
Definition: z3_api.h:44
bool is_numeral_u64(__uint64 &i) const
Definition: z3++.h:630
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:628

§ get_sort()

sort get_sort ( ) const
inline

§ hi()

unsigned hi ( ) const
inline

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

898 { 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:740
context & ctx() const
Definition: z3++.h:332
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:638

§ is_algebraic()

bool is_algebraic ( ) const
inline

Return true if expression is an algebraic number.

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

654 { return 0 != Z3_is_algebraic_number(ctx(), m_ast); }
context & ctx() const
Definition: z3++.h:332
Z3_ast m_ast
Definition: z3++.h:411

§ is_app()

bool is_app ( ) const
inline

Return true if this expression is an application.

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

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

§ is_arith()

bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

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

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

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

§ is_array()

bool is_array ( ) const
inline

Return true if this is a Array expression.

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

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

§ is_bool()

bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

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

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

§ is_bv()

bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

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

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

Referenced by solver::add().

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

§ is_datatype()

bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

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

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

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

§ is_int()

bool is_int ( ) const
inline

Return true if this is an integer expression.

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

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

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

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

§ is_numeral() [2/3]

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

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

Referenced by expr::is_numeral().

633 { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
context & ctx() const
Definition: z3++.h:332
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:411
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:628
void check_error() const
Definition: z3++.h:333

§ is_numeral() [3/3]

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

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

Referenced by expr::is_numeral().

634 { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }
context & ctx() const
Definition: z3++.h:332
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:411
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition: z3++.h:628
void check_error() const
Definition: z3++.h:333

§ is_numeral_i()

bool is_numeral_i ( int &  i) const
inline

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

631 { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
context & ctx() const
Definition: z3++.h:332
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:411
void check_error() const
Definition: z3++.h:333

§ is_numeral_i64()

bool is_numeral_i64 ( __int64 i) const
inline

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

629 { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
context & ctx() const
Definition: z3++.h:332
Z3_ast m_ast
Definition: z3++.h:411
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...
void check_error() const
Definition: z3++.h:333

§ is_numeral_u()

bool is_numeral_u ( unsigned &  i) const
inline

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

632 { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
context & ctx() const
Definition: z3++.h:332
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:411
void check_error() const
Definition: z3++.h:333

§ is_numeral_u64()

bool is_numeral_u64 ( __uint64 i) const
inline

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

630 { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned __int64 *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned __int6...
context & ctx() const
Definition: z3++.h:332
Z3_ast m_ast
Definition: z3++.h:411
void check_error() const
Definition: z3++.h:333

§ is_quantifier()

bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

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

§ is_re()

bool is_re ( ) const
inline

Return true if this is a regular expression.

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

Referenced by z3::operator+().

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

§ is_real()

bool is_real ( ) const
inline

Return true if this is a real expression.

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

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

§ is_relation()

bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

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

§ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

Referenced by z3::operator+().

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

§ is_var()

bool is_var ( ) const
inline

Return true if this expression is a variable.

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

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

§ is_well_sorted()

bool is_well_sorted ( ) const
inline

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

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

659 { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
context & ctx() const
Definition: z3++.h:332
Z3_ast m_ast
Definition: z3++.h:411
void check_error() const
Definition: z3++.h:333

§ length()

expr length ( ) const
inline

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

932  {
933  Z3_ast r = Z3_mk_seq_length(ctx(), *this);
934  check_error();
935  return expr(ctx(), r);
936  }
expr(context &c)
Definition: z3++.h:562
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ lo()

unsigned lo ( ) const
inline

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

897 { 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:740
context & ctx() const
Definition: z3++.h:332
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:638

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

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

747 { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ operator Z3_app()

operator Z3_app ( ) const
inline

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

732 { 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:638
Z3_ast m_ast
Definition: z3++.h:411

§ operator=()

expr& operator= ( expr const &  n)
inline

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

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

§ replace()

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

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

909  {
910  check_context(*this, src); check_context(src, dst);
911  Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
912  check_error();
913  return expr(ctx(), r);
914  }
expr(context &c)
Definition: z3++.h:562
context & ctx() const
Definition: z3++.h:332
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
void check_error() const
Definition: z3++.h:333

§ simplify() [1/2]

expr simplify ( ) const
inline

Return a simplified version of this expression.

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

943 { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:562
context & ctx() const
Definition: z3++.h:332
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_ast m_ast
Definition: z3++.h:411
void check_error() const
Definition: z3++.h:333

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

947 { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:562
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:332
Z3_ast m_ast
Definition: z3++.h:411
void check_error() const
Definition: z3++.h:333

§ substitute() [1/2]

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

Apply substitution. Replace src expressions by dst.

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

2535  {
2536  assert(src.size() == dst.size());
2537  array<Z3_ast> _src(src.size());
2538  array<Z3_ast> _dst(dst.size());
2539  for (unsigned i = 0; i < src.size(); ++i) {
2540  _src[i] = src[i];
2541  _dst[i] = dst[i];
2542  }
2543  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
2544  check_error();
2545  return expr(ctx(), r);
2546  }
expr(context &c)
Definition: z3++.h:562
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:332
Z3_ast m_ast
Definition: z3++.h:411
void check_error() const
Definition: z3++.h:333

§ substitute() [2/2]

expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

2548  {
2549  array<Z3_ast> _dst(dst.size());
2550  for (unsigned i = 0; i < dst.size(); ++i) {
2551  _dst[i] = dst[i];
2552  }
2553  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
2554  check_error();
2555  return expr(ctx(), r);
2556  }
expr(context &c)
Definition: z3++.h:562
context & ctx() const
Definition: z3++.h:332
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:411
void check_error() const
Definition: z3++.h:333

§ unit()

expr unit ( ) const
inline

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

915  {
916  Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
917  check_error();
918  return expr(ctx(), r);
919  }
expr(context &c)
Definition: z3++.h:562
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

Friends And Related Function Documentation

§ concat [1/2]

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

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

1478  {
1479  check_context(a, b);
1480  Z3_ast r;
1481  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
1482  Z3_ast _args[2] = { a, b };
1483  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
1484  }
1485  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
1486  Z3_ast _args[2] = { a, b };
1487  r = Z3_mk_re_concat(a.ctx(), 2, _args);
1488  }
1489  else {
1490  r = Z3_mk_concat(a.ctx(), a, b);
1491  }
1492  a.ctx().check_error();
1493  return expr(a.ctx(), r);
1494  }
expr(context &c)
Definition: z3++.h:562
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ concat [2/2]

expr concat ( expr_vector const &  args)
friend

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

1496  {
1497  Z3_ast r;
1498  assert(args.size() > 0);
1499  if (args.size() == 1) {
1500  return args[0];
1501  }
1502  context& ctx = args[0].ctx();
1503  array<Z3_ast> _args(args);
1504  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
1505  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
1506  }
1507  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
1508  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
1509  }
1510  else {
1511  r = _args[args.size()-1];
1512  for (unsigned i = args.size()-1; i > 0; ) {
1513  --i;
1514  r = Z3_mk_concat(ctx, _args[i], r);
1515  ctx.check_error();
1516  }
1517  }
1518  ctx.check_error();
1519  return expr(ctx, r);
1520  }
expr(context &c)
Definition: z3++.h:562
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
context & ctx() const
Definition: z3++.h:332
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:570

§ distinct

expr distinct ( expr_vector const &  args)
friend

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

1469  {
1470  assert(args.size() > 0);
1471  context& ctx = args[0].ctx();
1472  array<Z3_ast> _args(args);
1473  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1474  ctx.check_error();
1475  return expr(ctx, r);
1476  }
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:562
context & ctx() const
Definition: z3++.h:332

§ implies [1/3]

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

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

961  {
962  check_context(a, b);
963  assert(a.is_bool() && b.is_bool());
964  Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
965  a.check_error();
966  return expr(a.ctx(), r);
967  }
expr(context &c)
Definition: z3++.h:562
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.

§ implies [2/3]

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

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

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

§ implies [3/3]

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

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

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

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

1237  {
1238  check_context(c, t); check_context(c, e);
1239  assert(c.is_bool());
1240  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1241  c.check_error();
1242  return expr(c.ctx(), r);
1243  }
expr(context &c)
Definition: z3++.h:562
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
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 1528 of file z3++.h.

1528  {
1529  array<Z3_ast> _args(args);
1530  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
1531  args.check_error();
1532  return expr(args.ctx(), r);
1533  }
expr(context &c)
Definition: z3++.h:562
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 1522 of file z3++.h.

1522  {
1523  array<Z3_ast> _args(args);
1524  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
1525  args.check_error();
1526  return expr(args.ctx(), r);
1527  }
expr(context &c)
Definition: z3++.h:562
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].

§ operator & [1/3]

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

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

1214 { 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:562
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
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 1215 of file z3++.h.

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

§ operator & [3/3]

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

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

1216 { 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 990 of file z3++.h.

990  {
991  check_context(a, b);
992  assert(a.is_bool() && b.is_bool());
993  Z3_ast args[2] = { a, b };
994  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
995  a.check_error();
996  return expr(a.ctx(), r);
997  }
expr(context &c)
Definition: z3++.h:562
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:336

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

999 { 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 1000 of file z3++.h.

1000 { 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 983 of file z3++.h.

983  {
984  assert(a.is_bool());
985  Z3_ast r = Z3_mk_not(a.ctx(), a);
986  a.check_error();
987  return expr(a.ctx(), r);
988  }
expr(context &c)
Definition: z3++.h:562
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 1024 of file z3++.h.

1024  {
1025  check_context(a, b);
1026  Z3_ast args[2] = { a, b };
1027  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1028  a.check_error();
1029  return expr(a.ctx(), r);
1030  }
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:562
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator!= [2/3]

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

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

1031 { 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 1032 of file z3++.h.

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

1061  {
1062  check_context(a, b);
1063  Z3_ast r = 0;
1064  if (a.is_arith() && b.is_arith()) {
1065  Z3_ast args[2] = { a, b };
1066  r = Z3_mk_mul(a.ctx(), 2, args);
1067  }
1068  else if (a.is_bv() && b.is_bv()) {
1069  r = Z3_mk_bvmul(a.ctx(), a, b);
1070  }
1071  else {
1072  // operator is not supported by given arguments.
1073  assert(false);
1074  }
1075  a.check_error();
1076  return expr(a.ctx(), r);
1077  }
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:562
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
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 1078 of file z3++.h.

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

§ operator* [3/3]

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

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

1079 { 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 1034 of file z3++.h.

1034  {
1035  check_context(a, b);
1036  Z3_ast r = 0;
1037  if (a.is_arith() && b.is_arith()) {
1038  Z3_ast args[2] = { a, b };
1039  r = Z3_mk_add(a.ctx(), 2, args);
1040  }
1041  else if (a.is_bv() && b.is_bv()) {
1042  r = Z3_mk_bvadd(a.ctx(), a, b);
1043  }
1044  else if (a.is_seq() && b.is_seq()) {
1045  return concat(a, b);
1046  }
1047  else if (a.is_re() && b.is_re()) {
1048  Z3_ast _args[2] = { a, b };
1049  r = Z3_mk_re_union(a.ctx(), 2, _args);
1050  }
1051  else {
1052  // operator is not supported by given arguments.
1053  assert(false);
1054  }
1055  a.check_error();
1056  return expr(a.ctx(), r);
1057  }
expr(context &c)
Definition: z3++.h:562
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:1478
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:336
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 1058 of file z3++.h.

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

§ operator+ [3/3]

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

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

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

§ operator- [1/4]

expr operator- ( expr const &  a)
friend

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

1118  {
1119  Z3_ast r = 0;
1120  if (a.is_arith()) {
1121  r = Z3_mk_unary_minus(a.ctx(), a);
1122  }
1123  else if (a.is_bv()) {
1124  r = Z3_mk_bvneg(a.ctx(), a);
1125  }
1126  else {
1127  // operator is not supported by given arguments.
1128  assert(false);
1129  }
1130  a.check_error();
1131  return expr(a.ctx(), r);
1132  }
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:562
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 1134 of file z3++.h.

1134  {
1135  check_context(a, b);
1136  Z3_ast r = 0;
1137  if (a.is_arith() && b.is_arith()) {
1138  Z3_ast args[2] = { a, b };
1139  r = Z3_mk_sub(a.ctx(), 2, args);
1140  }
1141  else if (a.is_bv() && b.is_bv()) {
1142  r = Z3_mk_bvsub(a.ctx(), a, b);
1143  }
1144  else {
1145  // operator is not supported by given arguments.
1146  assert(false);
1147  }
1148  a.check_error();
1149  return expr(a.ctx(), r);
1150  }
expr(context &c)
Definition: z3++.h:562
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
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 1151 of file z3++.h.

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

§ operator- [4/4]

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

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

1152 { 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 1099 of file z3++.h.

1099  {
1100  check_context(a, b);
1101  Z3_ast r = 0;
1102  if (a.is_arith() && b.is_arith()) {
1103  r = Z3_mk_div(a.ctx(), a, b);
1104  }
1105  else if (a.is_bv() && b.is_bv()) {
1106  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1107  }
1108  else {
1109  // operator is not supported by given arguments.
1110  assert(false);
1111  }
1112  a.check_error();
1113  return expr(a.ctx(), r);
1114  }
expr(context &c)
Definition: z3++.h:562
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:336

§ operator/ [2/3]

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

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

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

§ operator/ [3/3]

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

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

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

1176  {
1177  check_context(a, b);
1178  Z3_ast r = 0;
1179  if (a.is_arith() && b.is_arith()) {
1180  r = Z3_mk_lt(a.ctx(), a, b);
1181  }
1182  else if (a.is_bv() && b.is_bv()) {
1183  r = Z3_mk_bvslt(a.ctx(), a, b);
1184  }
1185  else {
1186  // operator is not supported by given arguments.
1187  assert(false);
1188  }
1189  a.check_error();
1190  return expr(a.ctx(), r);
1191  }
expr(context &c)
Definition: z3++.h:562
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:336

§ operator< [2/3]

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

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

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

§ operator< [3/3]

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

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

1193 { 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 1154 of file z3++.h.

1154  {
1155  check_context(a, b);
1156  Z3_ast r = 0;
1157  if (a.is_arith() && b.is_arith()) {
1158  r = Z3_mk_le(a.ctx(), a, b);
1159  }
1160  else if (a.is_bv() && b.is_bv()) {
1161  r = Z3_mk_bvsle(a.ctx(), a, b);
1162  }
1163  else {
1164  // operator is not supported by given arguments.
1165  assert(false);
1166  }
1167  a.check_error();
1168  return expr(a.ctx(), r);
1169  }
expr(context &c)
Definition: z3++.h:562
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:336

§ operator<= [2/3]

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

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

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

§ operator<= [3/3]

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

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

1171 { 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 1015 of file z3++.h.

1015  {
1016  check_context(a, b);
1017  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1018  a.check_error();
1019  return expr(a.ctx(), r);
1020  }
expr(context &c)
Definition: z3++.h:562
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
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 1021 of file z3++.h.

1021 { 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 1022 of file z3++.h.

1022 { 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 1195 of file z3++.h.

1195  {
1196  check_context(a, b);
1197  Z3_ast r = 0;
1198  if (a.is_arith() && b.is_arith()) {
1199  r = Z3_mk_gt(a.ctx(), a, b);
1200  }
1201  else if (a.is_bv() && b.is_bv()) {
1202  r = Z3_mk_bvsgt(a.ctx(), a, b);
1203  }
1204  else {
1205  // operator is not supported by given arguments.
1206  assert(false);
1207  }
1208  a.check_error();
1209  return expr(a.ctx(), r);
1210  }
expr(context &c)
Definition: z3++.h:562
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:336
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 1211 of file z3++.h.

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

§ operator> [3/3]

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

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

1212 { 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 1082 of file z3++.h.

1082  {
1083  check_context(a, b);
1084  Z3_ast r = 0;
1085  if (a.is_arith() && b.is_arith()) {
1086  r = Z3_mk_ge(a.ctx(), a, b);
1087  }
1088  else if (a.is_bv() && b.is_bv()) {
1089  r = Z3_mk_bvsge(a.ctx(), a, b);
1090  }
1091  else {
1092  // operator is not supported by given arguments.
1093  assert(false);
1094  }
1095  a.check_error();
1096  return expr(a.ctx(), r);
1097  }
expr(context &c)
Definition: z3++.h:562
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:336

§ operator>= [2/3]

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

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

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

§ operator>= [3/3]

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

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

1174 { 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 1218 of file z3++.h.

1218 { 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:562
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
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 1219 of file z3++.h.

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

§ operator^ [3/3]

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

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

1220 { 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 1222 of file z3++.h.

1222 { 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:562
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
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 1223 of file z3++.h.

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

§ operator| [3/3]

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

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

1224 { 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 1002 of file z3++.h.

1002  {
1003  check_context(a, b);
1004  assert(a.is_bool() && b.is_bool());
1005  Z3_ast args[2] = { a, b };
1006  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1007  a.check_error();
1008  return expr(a.ctx(), r);
1009  }
expr(context &c)
Definition: z3++.h:562
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:336

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

1011 { 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 1013 of file z3++.h.

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

§ operator~

expr operator~ ( expr const &  a)
friend

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

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

§ pw [1/3]

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

Power operator.

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

972  {
973  assert(a.is_arith() && b.is_arith());
974  check_context(a, b);
975  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
976  a.check_error();
977  return expr(a.ctx(), r);
978  }
expr(context &c)
Definition: z3++.h:562
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.

§ pw [2/3]

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

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

979 { return pw(a, a.ctx().num_val(b, a.get_sort())); }
friend expr pw(expr const &a, expr const &b)
Power operator.
Definition: z3++.h:972

§ pw [3/3]

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

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

980 { return pw(b.ctx().num_val(a, b.get_sort()), b); }
friend expr pw(expr const &a, expr const &b)
Power operator.
Definition: z3++.h:972

§ wasoperator

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