Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
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 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 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 460 of file z3++.h.

Constructor & Destructor Documentation

expr ( context c)
inline

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

Referenced by expr::arg(), expr::body(), expr::simplify(), and expr::substitute().

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

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

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

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

464 :ast(n) {}
ast(context &c)
Definition: z3++.h:325

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

Referenced by ExprRef::children().

563 { Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:462
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_ast Z3_API Z3_get_app_arg(__in Z3_context c, __in Z3_app a, __in unsigned i)
Return the i-th argument of the given application.
expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

Referenced by QuantifierRef::children().

570 { assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_get_quantifier_body(__in Z3_context c, __in Z3_ast a)
Return body of quantifier.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition: z3++.h:529
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 548 of file z3++.h.

548 { Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_func_decl Z3_API Z3_get_app_decl(__in Z3_context c, __in Z3_app a)
Return the declaration of a constant or function application.
sort get_sort ( ) const
inline

Return the sort of this expression.

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

Referenced by expr::is_arith(), expr::is_array(), expr::is_bool(), expr::is_bv(), expr::is_datatype(), expr::is_finite_domain(), expr::is_int(), expr::is_real(), expr::is_relation(), z3::pw(), z3::select(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), and z3::ult().

470 { Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
void check_error() const
Definition: z3++.h:273
Z3_sort Z3_API Z3_get_sort(__in Z3_context c, __in Z3_ast a)
Return the sort of an AST node.
Z3_ast m_ast
Definition: z3++.h:323
context * m_ctx
Definition: z3++.h:268
bool is_app ( ) const
inline

Return true if this expression is an application.

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

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

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

Return true if this is an integer or real expression.

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

Referenced by z3::pw().

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

Return true if this is a Array expression.

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

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

Return true if this is a Boolean expression.

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

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

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

Return true if this is a Bit-vector expression.

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

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

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

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

Referenced by solver::add().

525 { 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:555
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:521
bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

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

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

Return true if this is an integer expression.

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

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

Return true if this expression is a numeral.

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

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

Return true if this expression is a quantifier.

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

Referenced by expr::body().

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

Return true if this is a real expression.

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

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

Return true if this is a Relation expression.

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

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

Return true if this expression is a variable.

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

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

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

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

538 { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
Z3_bool Z3_API Z3_is_well_sorted(__in Z3_context c, __in Z3_ast t)
Return true if the given expression t is well sorted.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_ast m_ast
Definition: z3++.h:323
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 555 of file z3++.h.

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

555 { unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
unsigned Z3_API Z3_get_app_num_args(__in Z3_context c, __in Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
operator Z3_app ( ) const
inline

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

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

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

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

Return a simplified version of this expression.

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

873 { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_simplify(__in Z3_context c, __in Z3_ast a)
Interface to simplifier.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_ast m_ast
Definition: z3++.h:323
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 877 of file z3++.h.

877 { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:462
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_ast m_ast
Definition: z3++.h:323
Z3_ast Z3_API Z3_simplify_ex(__in Z3_context c, __in Z3_ast a, __in Z3_params p)
Interface to simplifier.
expr substitute ( expr_vector const &  src,
expr_vector const &  dst 
)
inline

Apply substitution. Replace src expressions by dst.

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

1790  {
1791  assert(src.size() == dst.size());
1792  array<Z3_ast> _src(src.size());
1793  array<Z3_ast> _dst(dst.size());
1794  for (unsigned i = 0; i < src.size(); ++i) {
1795  _src[i] = src[i];
1796  _dst[i] = dst[i];
1797  }
1798  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
1799  check_error();
1800  return expr(ctx(), r);
1801  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_substitute(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const from[], __in_ecount(num_exprs) 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:272
void check_error() const
Definition: z3++.h:273
Z3_ast m_ast
Definition: z3++.h:323
expr substitute ( expr_vector const &  dst)
inline

Apply substitution. Replace bound variables by expressions.

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

1803  {
1804  array<Z3_ast> _dst(dst.size());
1805  for (unsigned i = 0; i < dst.size(); ++i) {
1806  _dst[i] = dst[i];
1807  }
1808  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
1809  check_error();
1810  return expr(ctx(), r);
1811  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_substitute_vars(__in Z3_context c, __in Z3_ast a, __in unsigned num_exprs, __in_ecount(num_exprs) Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs...
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_ast m_ast
Definition: z3++.h:323

Friends And Related Function Documentation

expr distinct ( expr_vector const &  args)
friend

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

1100  {
1101  assert(args.size() > 0);
1102  context& ctx = args[0].ctx();
1103  array<Z3_ast> _args(args);
1104  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1105  ctx.check_error();
1106  return expr(ctx, r);
1107  }
expr(context &c)
Definition: z3++.h:462
context & ctx() const
Definition: z3++.h:272
Z3_ast Z3_API Z3_mk_distinct(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).The distinct construct is us...
expr implies ( expr const &  a,
expr const &  b 
)
friend

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

645  {
646  check_context(a, b);
647  assert(a.is_bool() && b.is_bool());
648  Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
649  a.check_error();
650  return expr(a.ctx(), r);
651  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_mk_implies(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create an AST node representing t1 implies t2.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
expr implies ( expr const &  a,
bool  b 
)
friend

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

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

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

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

914  {
915  check_context(c, t); check_context(c, e);
916  assert(c.is_bool());
917  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
918  c.check_error();
919  return expr(c.ctx(), r);
920  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_mk_ite(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
expr operator! ( expr const &  a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

577  {
578  assert(a.is_bool());
579  Z3_ast r = Z3_mk_not(a.ctx(), a);
580  a.check_error();
581  return expr(a.ctx(), r);
582  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_mk_not(__in Z3_context c, __in Z3_ast a)
Create an AST node representing not(a).
expr operator!= ( expr const &  a,
expr const &  b 
)
friend

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

668  {
669  check_context(a, b);
670  Z3_ast args[2] = { a, b };
671  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
672  a.check_error();
673  return expr(a.ctx(), r);
674  }
expr(context &c)
Definition: z3++.h:462
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_distinct(__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).The distinct construct is us...
expr operator!= ( expr const &  a,
int  b 
)
friend

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

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

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

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

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

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

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

858 { 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 591 of file z3++.h.

591  {
592  check_context(a, b);
593  assert(a.is_bool() && b.is_bool());
594  Z3_ast args[2] = { a, b };
595  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
596  a.check_error();
597  return expr(a.ctx(), r);
598  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_mk_and(__in Z3_context c, __in unsigned num_args, __in_ecount(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:276
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 607 of file z3++.h.

607 { 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 614 of file z3++.h.

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

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

698  {
699  check_context(a, b);
700  Z3_ast r;
701  if (a.is_arith() && b.is_arith()) {
702  Z3_ast args[2] = { a, b };
703  r = Z3_mk_mul(a.ctx(), 2, args);
704  }
705  else if (a.is_bv() && b.is_bv()) {
706  r = Z3_mk_bvmul(a.ctx(), a, b);
707  }
708  else {
709  // operator is not supported by given arguments.
710  assert(false);
711  }
712  a.check_error();
713  return expr(a.ctx(), r);
714  }
Z3_ast Z3_API Z3_mk_mul(__in Z3_context c, __in unsigned num_args, __in_ecount(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:462
Z3_ast Z3_API Z3_mk_bvmul(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement multiplication.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
expr operator* ( expr const &  a,
int  b 
)
friend

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

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

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

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

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

678  {
679  check_context(a, b);
680  Z3_ast r;
681  if (a.is_arith() && b.is_arith()) {
682  Z3_ast args[2] = { a, b };
683  r = Z3_mk_add(a.ctx(), 2, args);
684  }
685  else if (a.is_bv() && b.is_bv()) {
686  r = Z3_mk_bvadd(a.ctx(), a, b);
687  }
688  else {
689  // operator is not supported by given arguments.
690  assert(false);
691  }
692  a.check_error();
693  return expr(a.ctx(), r);
694  }
Z3_ast Z3_API Z3_mk_bvadd(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement addition.
expr(context &c)
Definition: z3++.h:462
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_add(__in Z3_context c, __in unsigned num_args, __in_ecount(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 operator+ ( expr const &  a,
int  b 
)
friend

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

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

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

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

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

744  {
745  Z3_ast r;
746  if (a.is_arith()) {
747  r = Z3_mk_unary_minus(a.ctx(), a);
748  }
749  else if (a.is_bv()) {
750  r = Z3_mk_bvneg(a.ctx(), a);
751  }
752  else {
753  // operator is not supported by given arguments.
754  assert(false);
755  }
756  a.check_error();
757  return expr(a.ctx(), r);
758  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_mk_bvneg(__in Z3_context c, __in Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_unary_minus(__in Z3_context c, __in Z3_ast arg)
Create an AST node representing -arg.The arguments must have int or real type.
expr operator- ( expr const &  a,
expr const &  b 
)
friend

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

760  {
761  check_context(a, b);
762  Z3_ast r;
763  if (a.is_arith() && b.is_arith()) {
764  Z3_ast args[2] = { a, b };
765  r = Z3_mk_sub(a.ctx(), 2, args);
766  }
767  else if (a.is_bv() && b.is_bv()) {
768  r = Z3_mk_bvsub(a.ctx(), a, b);
769  }
770  else {
771  // operator is not supported by given arguments.
772  assert(false);
773  }
774  a.check_error();
775  return expr(a.ctx(), r);
776  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_mk_sub(__in Z3_context c, __in unsigned num_args, __in_ecount(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(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Standard two's complement subtraction.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
expr operator- ( expr const &  a,
int  b 
)
friend

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

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

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

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

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

725  {
726  check_context(a, b);
727  Z3_ast r;
728  if (a.is_arith() && b.is_arith()) {
729  r = Z3_mk_div(a.ctx(), a, b);
730  }
731  else if (a.is_bv() && b.is_bv()) {
732  r = Z3_mk_bvsdiv(a.ctx(), a, b);
733  }
734  else {
735  // operator is not supported by given arguments.
736  assert(false);
737  }
738  a.check_error();
739  return expr(a.ctx(), r);
740  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_mk_bvsdiv(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed division.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_div(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Create an AST node representing arg1 div arg2.The arguments must either both have int type or both ha...
expr operator/ ( expr const &  a,
int  b 
)
friend

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

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

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

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

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

818  {
819  check_context(a, b);
820  Z3_ast r;
821  if (a.is_arith() && b.is_arith()) {
822  r = Z3_mk_lt(a.ctx(), a, b);
823  }
824  else if (a.is_bv() && b.is_bv()) {
825  r = Z3_mk_bvslt(a.ctx(), a, b);
826  }
827  else {
828  // operator is not supported by given arguments.
829  assert(false);
830  }
831  a.check_error();
832  return expr(a.ctx(), r);
833  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_mk_bvslt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed less than.
Z3_ast Z3_API Z3_mk_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create less than.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
expr operator< ( expr const &  a,
int  b 
)
friend

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

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

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

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

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

780  {
781  check_context(a, b);
782  Z3_ast r;
783  if (a.is_arith() && b.is_arith()) {
784  r = Z3_mk_le(a.ctx(), a, b);
785  }
786  else if (a.is_bv() && b.is_bv()) {
787  r = Z3_mk_bvsle(a.ctx(), a, b);
788  }
789  else {
790  // operator is not supported by given arguments.
791  assert(false);
792  }
793  a.check_error();
794  return expr(a.ctx(), r);
795  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_mk_bvsle(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed less than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_le(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create less than or equal to.
expr operator<= ( expr const &  a,
int  b 
)
friend

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

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

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

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

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

659  {
660  check_context(a, b);
661  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
662  a.check_error();
663  return expr(a.ctx(), r);
664  }
expr(context &c)
Definition: z3++.h:462
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_eq(__in Z3_context c, __in Z3_ast l, __in Z3_ast r)
Create an AST node representing l = r.
expr operator== ( expr const &  a,
int  b 
)
friend

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

665 { 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 666 of file z3++.h.

666 { 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 837 of file z3++.h.

837  {
838  check_context(a, b);
839  Z3_ast r;
840  if (a.is_arith() && b.is_arith()) {
841  r = Z3_mk_gt(a.ctx(), a, b);
842  }
843  else if (a.is_bv() && b.is_bv()) {
844  r = Z3_mk_bvsgt(a.ctx(), a, b);
845  }
846  else {
847  // operator is not supported by given arguments.
848  assert(false);
849  }
850  a.check_error();
851  return expr(a.ctx(), r);
852  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_mk_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create greater than.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_bvsgt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed greater than.
expr operator> ( expr const &  a,
int  b 
)
friend

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

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

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

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

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

799  {
800  check_context(a, b);
801  Z3_ast r;
802  if (a.is_arith() && b.is_arith()) {
803  r = Z3_mk_ge(a.ctx(), a, b);
804  }
805  else if (a.is_bv() && b.is_bv()) {
806  r = Z3_mk_bvsge(a.ctx(), a, b);
807  }
808  else {
809  // operator is not supported by given arguments.
810  assert(false);
811  }
812  a.check_error();
813  return expr(a.ctx(), r);
814  }
expr(context &c)
Definition: z3++.h:462
Z3_ast Z3_API Z3_mk_ge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Create greater than or equal to.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_bvsge(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Two's complement signed greater than or equal to.
expr operator>= ( expr const &  a,
int  b 
)
friend

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

866 { 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 622 of file z3++.h.

622  {
623  check_context(a, b);
624  assert(a.is_bool() && b.is_bool());
625  Z3_ast args[2] = { a, b };
626  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
627  a.check_error();
628  return expr(a.ctx(), r);
629  }
expr(context &c)
Definition: z3++.h:462
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_or(__in Z3_context c, __in unsigned num_args, __in_ecount(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 ...
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 636 of file z3++.h.

636 { 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 643 of file z3++.h.

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

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

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

Power operator.

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

894  {
895  assert(a.is_arith() && b.is_arith());
896  check_context(a, b);
897  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
898  a.check_error();
899  return expr(a.ctx(), r);
900  }
Z3_ast Z3_API Z3_mk_power(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Create an AST node representing arg1^arg2.
expr(context &c)
Definition: z3++.h:462
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
expr pw ( expr const &  a,
int  b 
)
friend

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

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

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

902 { 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:894