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_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. More...
 
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_well_sorted () const
 Return true if this expression is well sorted (aka type correct). 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 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 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 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 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 465 of file z3++.h.

Constructor & Destructor Documentation

expr ( context c)
inline

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

467 :ast(c) {}
ast(context &c)
Definition: z3++.h:330
expr ( context c,
Z3_ast  n 
)
inline

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

468 :ast(c, reinterpret_cast<Z3_ast>(n)) {}
ast(context &c)
Definition: z3++.h:330
expr ( expr const &  n)
inline

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

469 :ast(n) {}
ast(context &c)
Definition: z3++.h:330

Member Function Documentation

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

Referenced by ExprRef::children().

568 { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:467
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:277
void check_error() const
Definition: z3++.h:278
expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

Referenced by QuantifierRef::children().

575 { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:467
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
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:534
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 553 of file z3++.h.

553 { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
expr extract ( unsigned  hi,
unsigned  lo 
) const
inline

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

875 { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:467
unsigned lo() const
Definition: z3++.h:876
context & ctx() const
Definition: z3++.h:277
unsigned hi() const
Definition: z3++.h:877
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 bitvector of size m to yield a new bitvector of size n...
sort get_sort ( ) const
inline

Return the sort of this expression.

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

Referenced by z3::pw(), z3::select(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), and z3::ult().

475 { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
void check_error() const
Definition: z3++.h:278
Z3_ast m_ast
Definition: z3++.h:328
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:273
unsigned hi ( ) const
inline

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

877 { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
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:277
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:553
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:526
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.
bool is_app ( ) const
inline

Return true if this expression is an application.

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

526 { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:337
bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

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

Referenced by z3::pw().

492 { return get_sort().is_arith(); }
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition: z3++.h:385
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:475
bool is_array ( ) const
inline

Return true if this is a Array expression.

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

500 { return get_sort().is_array(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:475
bool is_array() const
Return true if this sort is a Array sort.
Definition: z3++.h:393
bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

Referenced by solver::add(), optimize::add(), and z3::ite().

480 { return get_sort().is_bool(); }
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition: z3++.h:373
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:475
bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

496 { return get_sort().is_bv(); }
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition: z3++.h:389
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:475
bool is_const ( ) const
inline

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

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

Referenced by solver::add().

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

Return true if this is a Datatype expression.

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

504 { return get_sort().is_datatype(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:475
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition: z3++.h:397
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 517 of file z3++.h.

517 { return get_sort().is_finite_domain(); }
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
Definition: z3++.h:405
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:475
bool is_int ( ) const
inline

Return true if this is an integer expression.

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

484 { return get_sort().is_int(); }
bool is_int() const
Return true if this sort is the Integer sort.
Definition: z3++.h:377
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:475
bool is_numeral ( ) const
inline

Return true if this expression is a numeral.

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

522 { return kind() == Z3_NUMERAL_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:337
bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

534 { return kind() == Z3_QUANTIFIER_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:337
bool is_real ( ) const
inline

Return true if this is a real expression.

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

488 { return get_sort().is_real(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:475
bool is_real() const
Return true if this sort is the Real sort.
Definition: z3++.h:381
bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

508 { return get_sort().is_relation(); }
sort get_sort() const
Return the sort of this expression.
Definition: z3++.h:475
bool is_relation() const
Return true if this sort is a Relation sort.
Definition: z3++.h:401
bool is_var ( ) const
inline

Return true if this expression is a variable.

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

538 { return kind() == Z3_VAR_AST; }
Z3_ast_kind kind() const
Definition: z3++.h:337
bool is_well_sorted ( ) const
inline

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

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

543 { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
Z3_ast m_ast
Definition: z3++.h:328
Z3_bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
unsigned lo ( ) const
inline

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

876 { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
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:277
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:553
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:526
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.
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 560 of file z3++.h.

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

560 { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
context & ctx() const
Definition: z3++.h:277
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...
void check_error() const
Definition: z3++.h:278
operator Z3_app ( ) const
inline

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

545 { 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:526
Z3_ast m_ast
Definition: z3++.h:328
expr& operator= ( expr const &  n)
inline

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

470 { return static_cast<expr&>(ast::operator=(n)); }
expr(context &c)
Definition: z3++.h:467
ast & operator=(ast const &s)
Definition: z3++.h:336
expr simplify ( ) const
inline

Return a simplified version of this expression.

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

882 { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:467
context & ctx() const
Definition: z3++.h:277
void check_error() const
Definition: z3++.h:278
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
Z3_ast m_ast
Definition: z3++.h:328
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 886 of file z3++.h.

886 { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:467
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:277
void check_error() const
Definition: z3++.h:278
Z3_ast m_ast
Definition: z3++.h:328
expr substitute ( expr_vector const &  src,
expr_vector const &  dst 
)
inline

Apply substitution. Replace src expressions by dst.

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

1889  {
1890  assert(src.size() == dst.size());
1891  array<Z3_ast> _src(src.size());
1892  array<Z3_ast> _dst(dst.size());
1893  for (unsigned i = 0; i < src.size(); ++i) {
1894  _src[i] = src[i];
1895  _dst[i] = dst[i];
1896  }
1897  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
1898  check_error();
1899  return expr(ctx(), r);
1900  }
expr(context &c)
Definition: z3++.h:467
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:277
void check_error() const
Definition: z3++.h:278
Z3_ast m_ast
Definition: z3++.h:328
expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

1902  {
1903  array<Z3_ast> _dst(dst.size());
1904  for (unsigned i = 0; i < dst.size(); ++i) {
1905  _dst[i] = dst[i];
1906  }
1907  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
1908  check_error();
1909  return expr(ctx(), r);
1910  }
expr(context &c)
Definition: z3++.h:467
context & ctx() const
Definition: z3++.h:277
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...
void check_error() const
Definition: z3++.h:278
Z3_ast m_ast
Definition: z3++.h:328

Friends And Related Function Documentation

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

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

1118  {
1119  check_context(a, b);
1120  Z3_ast r = Z3_mk_concat(a.ctx(), a, b);
1121  a.ctx().check_error();
1122  return expr(a.ctx(), r);
1123  }
expr(context &c)
Definition: z3++.h:467
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:281
expr distinct ( expr_vector const &  args)
friend

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

1109  {
1110  assert(args.size() > 0);
1111  context& ctx = args[0].ctx();
1112  array<Z3_ast> _args(args);
1113  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1114  ctx.check_error();
1115  return expr(ctx, r);
1116  }
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]).The distinct construct is us...
expr(context &c)
Definition: z3++.h:467
context & ctx() const
Definition: z3++.h:277
expr implies ( expr const &  a,
expr const &  b 
)
friend

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

650  {
651  check_context(a, b);
652  assert(a.is_bool() && b.is_bool());
653  Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
654  a.check_error();
655  return expr(a.ctx(), r);
656  }
expr(context &c)
Definition: z3++.h:467
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
expr implies ( expr const &  a,
bool  b 
)
friend

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

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

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

901 { return implies(b.ctx().bool_val(a), b); }
friend expr implies(expr const &a, expr const &b)
Definition: z3++.h:650
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 923 of file z3++.h.

923  {
924  check_context(c, t); check_context(c, e);
925  assert(c.is_bool());
926  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
927  c.check_error();
928  return expr(c.ctx(), r);
929  }
expr(context &c)
Definition: z3++.h:467
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
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).
expr operator! ( expr const &  a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

582  {
583  assert(a.is_bool());
584  Z3_ast r = Z3_mk_not(a.ctx(), a);
585  a.check_error();
586  return expr(a.ctx(), r);
587  }
expr(context &c)
Definition: z3++.h:467
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
expr operator!= ( expr const &  a,
expr const &  b 
)
friend

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

674  {
675  check_context(a, b);
676  Z3_ast args[2] = { a, b };
677  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
678  a.check_error();
679  return expr(a.ctx(), r);
680  }
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]).The distinct construct is us...
expr(context &c)
Definition: z3++.h:467
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr operator!= ( expr const &  a,
int  b 
)
friend

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

681 { assert(a.is_arith() || a.is_bv()); return a != a.ctx().num_val(b, a.get_sort()); }
expr operator!= ( int  a,
expr const &  b 
)
friend

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

682 { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) != b; }
expr operator& ( expr const &  a,
expr const &  b 
)
friend

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

862 { 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:467
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
expr operator& ( expr const &  a,
int  b 
)
friend

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

863 { return a & a.ctx().num_val(b, a.get_sort()); }
expr operator& ( int  a,
expr const &  b 
)
friend

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

864 { return b.ctx().num_val(a, b.get_sort()) & b; }
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 596 of file z3++.h.

596  {
597  check_context(a, b);
598  assert(a.is_bool() && b.is_bool());
599  Z3_ast args[2] = { a, b };
600  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
601  a.check_error();
602  return expr(a.ctx(), r);
603  }
expr(context &c)
Definition: z3++.h:467
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].The array args must have num_arg...
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
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 612 of file z3++.h.

612 { return a && a.ctx().bool_val(b); }
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 619 of file z3++.h.

619 { return b.ctx().bool_val(a) && b; }
expr operator* ( expr const &  a,
expr const &  b 
)
friend

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

704  {
705  check_context(a, b);
706  Z3_ast r = 0;
707  if (a.is_arith() && b.is_arith()) {
708  Z3_ast args[2] = { a, b };
709  r = Z3_mk_mul(a.ctx(), 2, args);
710  }
711  else if (a.is_bv() && b.is_bv()) {
712  r = Z3_mk_bvmul(a.ctx(), a, b);
713  }
714  else {
715  // operator is not supported by given arguments.
716  assert(false);
717  }
718  a.check_error();
719  return expr(a.ctx(), r);
720  }
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].The array args must have num_args el...
expr(context &c)
Definition: z3++.h:467
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement multiplication.
expr operator* ( expr const &  a,
int  b 
)
friend

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

721 { return a * a.ctx().num_val(b, a.get_sort()); }
expr operator* ( int  a,
expr const &  b 
)
friend

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

722 { return b.ctx().num_val(a, b.get_sort()) * b; }
expr operator+ ( expr const &  a,
expr const &  b 
)
friend

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

684  {
685  check_context(a, b);
686  Z3_ast r = 0;
687  if (a.is_arith() && b.is_arith()) {
688  Z3_ast args[2] = { a, b };
689  r = Z3_mk_add(a.ctx(), 2, args);
690  }
691  else if (a.is_bv() && b.is_bv()) {
692  r = Z3_mk_bvadd(a.ctx(), a, b);
693  }
694  else {
695  // operator is not supported by given arguments.
696  assert(false);
697  }
698  a.check_error();
699  return expr(a.ctx(), r);
700  }
expr(context &c)
Definition: z3++.h:467
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].The array args must have num_args el...
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement addition.
expr operator+ ( expr const &  a,
int  b 
)
friend

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

701 { return a + a.ctx().num_val(b, a.get_sort()); }
expr operator+ ( int  a,
expr const &  b 
)
friend

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

702 { return b.ctx().num_val(a, b.get_sort()) + b; }
expr operator- ( expr const &  a)
friend

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

750  {
751  Z3_ast r = 0;
752  if (a.is_arith()) {
753  r = Z3_mk_unary_minus(a.ctx(), a);
754  }
755  else if (a.is_bv()) {
756  r = Z3_mk_bvneg(a.ctx(), a);
757  }
758  else {
759  // operator is not supported by given arguments.
760  assert(false);
761  }
762  a.check_error();
763  return expr(a.ctx(), r);
764  }
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing -arg.The arguments must have int or real type.
expr(context &c)
Definition: z3++.h:467
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two&#39;s complement unary minus.
expr operator- ( expr const &  a,
expr const &  b 
)
friend

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

766  {
767  check_context(a, b);
768  Z3_ast r = 0;
769  if (a.is_arith() && b.is_arith()) {
770  Z3_ast args[2] = { a, b };
771  r = Z3_mk_sub(a.ctx(), 2, args);
772  }
773  else if (a.is_bv() && b.is_bv()) {
774  r = Z3_mk_bvsub(a.ctx(), a, b);
775  }
776  else {
777  // operator is not supported by given arguments.
778  assert(false);
779  }
780  a.check_error();
781  return expr(a.ctx(), r);
782  }
expr(context &c)
Definition: z3++.h:467
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
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].The array args must have num_args ...
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement subtraction.
expr operator- ( expr const &  a,
int  b 
)
friend

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

783 { return a - a.ctx().num_val(b, a.get_sort()); }
expr operator- ( int  a,
expr const &  b 
)
friend

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

784 { return b.ctx().num_val(a, b.get_sort()) - b; }
expr operator/ ( expr const &  a,
expr const &  b 
)
friend

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

731  {
732  check_context(a, b);
733  Z3_ast r = 0;
734  if (a.is_arith() && b.is_arith()) {
735  r = Z3_mk_div(a.ctx(), a, b);
736  }
737  else if (a.is_bv() && b.is_bv()) {
738  r = Z3_mk_bvsdiv(a.ctx(), a, b);
739  }
740  else {
741  // operator is not supported by given arguments.
742  assert(false);
743  }
744  a.check_error();
745  return expr(a.ctx(), r);
746  }
expr(context &c)
Definition: z3++.h:467
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.The arguments must either both have int type or both ha...
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr operator/ ( expr const &  a,
int  b 
)
friend

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

747 { return a / a.ctx().num_val(b, a.get_sort()); }
expr operator/ ( int  a,
expr const &  b 
)
friend

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

748 { return b.ctx().num_val(a, b.get_sort()) / b; }
expr operator< ( expr const &  a,
expr const &  b 
)
friend

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

824  {
825  check_context(a, b);
826  Z3_ast r = 0;
827  if (a.is_arith() && b.is_arith()) {
828  r = Z3_mk_lt(a.ctx(), a, b);
829  }
830  else if (a.is_bv() && b.is_bv()) {
831  r = Z3_mk_bvslt(a.ctx(), a, b);
832  }
833  else {
834  // operator is not supported by given arguments.
835  assert(false);
836  }
837  a.check_error();
838  return expr(a.ctx(), r);
839  }
expr(context &c)
Definition: z3++.h:467
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:281
expr operator< ( expr const &  a,
int  b 
)
friend

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

840 { return a < a.ctx().num_val(b, a.get_sort()); }
expr operator< ( int  a,
expr const &  b 
)
friend

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

841 { return b.ctx().num_val(a, b.get_sort()) < b; }
expr operator<= ( expr const &  a,
expr const &  b 
)
friend

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

786  {
787  check_context(a, b);
788  Z3_ast r = 0;
789  if (a.is_arith() && b.is_arith()) {
790  r = Z3_mk_le(a.ctx(), a, b);
791  }
792  else if (a.is_bv() && b.is_bv()) {
793  r = Z3_mk_bvsle(a.ctx(), a, b);
794  }
795  else {
796  // operator is not supported by given arguments.
797  assert(false);
798  }
799  a.check_error();
800  return expr(a.ctx(), r);
801  }
expr(context &c)
Definition: z3++.h:467
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:281
expr operator<= ( expr const &  a,
int  b 
)
friend

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

802 { return a <= a.ctx().num_val(b, a.get_sort()); }
expr operator<= ( int  a,
expr const &  b 
)
friend

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

803 { return b.ctx().num_val(a, b.get_sort()) <= b; }
expr operator== ( expr const &  a,
expr const &  b 
)
friend

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

665  {
666  check_context(a, b);
667  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
668  a.check_error();
669  return expr(a.ctx(), r);
670  }
expr(context &c)
Definition: z3++.h:467
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
expr operator== ( expr const &  a,
int  b 
)
friend

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

671 { assert(a.is_arith() || a.is_bv()); return a == a.ctx().num_val(b, a.get_sort()); }
expr operator== ( int  a,
expr const &  b 
)
friend

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

672 { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) == b; }
expr operator> ( expr const &  a,
expr const &  b 
)
friend

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

843  {
844  check_context(a, b);
845  Z3_ast r = 0;
846  if (a.is_arith() && b.is_arith()) {
847  r = Z3_mk_gt(a.ctx(), a, b);
848  }
849  else if (a.is_bv() && b.is_bv()) {
850  r = Z3_mk_bvsgt(a.ctx(), a, b);
851  }
852  else {
853  // operator is not supported by given arguments.
854  assert(false);
855  }
856  a.check_error();
857  return expr(a.ctx(), r);
858  }
expr(context &c)
Definition: z3++.h:467
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:281
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
expr operator> ( expr const &  a,
int  b 
)
friend

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

859 { return a > a.ctx().num_val(b, a.get_sort()); }
expr operator> ( int  a,
expr const &  b 
)
friend

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

860 { return b.ctx().num_val(a, b.get_sort()) > b; }
expr operator>= ( expr const &  a,
expr const &  b 
)
friend

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

805  {
806  check_context(a, b);
807  Z3_ast r = 0;
808  if (a.is_arith() && b.is_arith()) {
809  r = Z3_mk_ge(a.ctx(), a, b);
810  }
811  else if (a.is_bv() && b.is_bv()) {
812  r = Z3_mk_bvsge(a.ctx(), a, b);
813  }
814  else {
815  // operator is not supported by given arguments.
816  assert(false);
817  }
818  a.check_error();
819  return expr(a.ctx(), r);
820  }
expr(context &c)
Definition: z3++.h:467
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:281
expr operator>= ( expr const &  a,
int  b 
)
friend

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

821 { return a >= a.ctx().num_val(b, a.get_sort()); }
expr operator>= ( int  a,
expr const &  b 
)
friend

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

822 { return b.ctx().num_val(a, b.get_sort()) >= b; }
expr operator^ ( expr const &  a,
expr const &  b 
)
friend

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

866 { 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:467
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
expr operator^ ( expr const &  a,
int  b 
)
friend

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

867 { return a ^ a.ctx().num_val(b, a.get_sort()); }
expr operator^ ( int  a,
expr const &  b 
)
friend

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

868 { return b.ctx().num_val(a, b.get_sort()) ^ b; }
expr operator| ( expr const &  a,
expr const &  b 
)
friend

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

870 { 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:467
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
expr operator| ( expr const &  a,
int  b 
)
friend

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

871 { return a | a.ctx().num_val(b, a.get_sort()); }
expr operator| ( int  a,
expr const &  b 
)
friend

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

872 { return b.ctx().num_val(a, b.get_sort()) | b; }
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 627 of file z3++.h.

627  {
628  check_context(a, b);
629  assert(a.is_bool() && b.is_bool());
630  Z3_ast args[2] = { a, b };
631  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
632  a.check_error();
633  return expr(a.ctx(), r);
634  }
expr(context &c)
Definition: z3++.h:467
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].The array args must have num_args ...
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
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 641 of file z3++.h.

641 { return a || a.ctx().bool_val(b); }
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 648 of file z3++.h.

648 { return b.ctx().bool_val(a) || b; }
expr operator~ ( expr const &  a)
friend

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

874 { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
expr(context &c)
Definition: z3++.h:467
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
expr pw ( expr const &  a,
expr const &  b 
)
friend

Power operator.

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

903  {
904  assert(a.is_arith() && b.is_arith());
905  check_context(a, b);
906  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
907  a.check_error();
908  return expr(a.ctx(), r);
909  }
expr(context &c)
Definition: z3++.h:467
friend void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1^arg2.
expr pw ( expr const &  a,
int  b 
)
friend

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

910 { 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:903
expr pw ( int  a,
expr const &  b 
)
friend

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

911 { 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:903