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 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::extract(), 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.

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

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.
expr extract ( unsigned  hi,
unsigned  lo 
) const
inline

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

869 { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); return expr(ctx(), r); }
expr(context &c)
Definition: z3++.h:462
unsigned lo() const
Definition: z3++.h:870
context & ctx() const
Definition: z3++.h:272
Z3_ast Z3_API Z3_mk_extract(__in Z3_context c, __in unsigned high, __in unsigned low, __in Z3_ast t1)
Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n...
unsigned hi() const
Definition: z3++.h:871
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
unsigned hi ( ) const
inline

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

871 { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
int Z3_API Z3_get_decl_int_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
unsigned Z3_API Z3_get_decl_num_parameters(__in Z3_context c, __in Z3_func_decl d)
Return the number of parameters associated with a declaration.
context & ctx() const
Definition: z3++.h:272
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:548
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:521
bool is_app ( ) const
inline

Return true if this expression is an application.

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

Referenced by expr::hi(), expr::is_const(), expr::lo(), 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 lo ( ) const
inline

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

870 { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
int Z3_API Z3_get_decl_int_parameter(__in Z3_context c, __in Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
unsigned Z3_API Z3_get_decl_num_parameters(__in Z3_context c, __in Z3_func_decl d)
Return the number of parameters associated with a declaration.
context & ctx() const
Definition: z3++.h:272
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition: z3++.h:548
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:521
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 876 of file z3++.h.

876 { 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 880 of file z3++.h.

880 { 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 1813 of file z3++.h.

1813  {
1814  assert(src.size() == dst.size());
1815  array<Z3_ast> _src(src.size());
1816  array<Z3_ast> _dst(dst.size());
1817  for (unsigned i = 0; i < src.size(); ++i) {
1818  _src[i] = src[i];
1819  _dst[i] = dst[i];
1820  }
1821  Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
1822  check_error();
1823  return expr(ctx(), r);
1824  }
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 1826 of file z3++.h.

1826  {
1827  array<Z3_ast> _dst(dst.size());
1828  for (unsigned i = 0; i < dst.size(); ++i) {
1829  _dst[i] = dst[i];
1830  }
1831  Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
1832  check_error();
1833  return expr(ctx(), r);
1834  }
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 1103 of file z3++.h.

1103  {
1104  assert(args.size() > 0);
1105  context& ctx = args[0].ctx();
1106  array<Z3_ast> _args(args);
1107  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1108  ctx.check_error();
1109  return expr(ctx, r);
1110  }
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 894 of file z3++.h.

894 { 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 895 of file z3++.h.

895 { 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 917 of file z3++.h.

917  {
918  check_context(c, t); check_context(c, e);
919  assert(c.is_bool());
920  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
921  c.check_error();
922  return expr(c.ctx(), r);
923  }
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 897 of file z3++.h.

897  {
898  assert(a.is_arith() && b.is_arith());
899  check_context(a, b);
900  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
901  a.check_error();
902  return expr(a.ctx(), r);
903  }
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 904 of file z3++.h.

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

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

905 { 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:897