Z3 |

Data Structures | Namespaces | Macros | Typedefs | Enumerations | Functions
z3++.h File Reference

Go to the source code of this file.

## Data Structures
class | exception
| Exception used to sign API usage errors. More...
class | config
| Z3 global configuration object. More...
class | context
| A Context manages all other Z3 objects, global configuration options, etc. More...
class | scoped_context
class | array< T >
class | object
class | symbol
class | param_descrs
class | params
class | ast
class | ast_vector_tpl< T >
class | ast_vector_tpl< T >::iterator
class | sort
| A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...
class | func_decl
| Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application. More...
class | expr
| 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...
class | cast_ast< ast >
class | cast_ast< expr >
class | cast_ast< sort >
class | cast_ast< func_decl >
class | func_entry
class | func_interp
class | model
struct | model::translate
class | stats
class | solver
struct | solver::simple
struct | solver::translate
class | solver::cube_iterator
class | solver::cube_generator
class | goal
class | apply_result
class | tactic
class | probe
class | optimize
class | optimize::handle
class | fixedpoint
class | user_propagator_base

## Namespaces
namespace | z3
| Z3 C++ namespace.

## Macros
#define | Z3_THROW(x) {}
#define | _Z3_MK_BIN_(a, b, binop)
#define | _Z3_MK_UN_(a, mkun)
#define | MK_EXPR1(_fn, _arg)
#define | MK_EXPR2(_fn, _arg1, _arg2)

## Typedefs
typedef ast_vector_tpl< ast > | ast_vector
typedef ast_vector_tpl< expr > | expr_vector
typedef ast_vector_tpl< sort > | sort_vector
typedef ast_vector_tpl< func_decl > | func_decl_vector

## Enumerations
enum | check_result { unsat , sat , unknown }
enum | rounding_mode { RNA , RNE , RTP , RTN , RTZ }

## Functions
void | set_param (char const *param, char const *value)
void | set_param (char const *param, bool value)
void | set_param (char const *param, int value)
void | reset_params ()
std::ostream & | operator<< (std::ostream &out, exception const &e)
check_result | to_check_result (Z3_lbool l)
void | check_context (object const &a, object const &b)
std::ostream & | operator<< (std::ostream &out, symbol const &s)
std::ostream & | operator<< (std::ostream &out, param_descrs const &d)
std::ostream & | operator<< (std::ostream &out, params const &p)
std::ostream & | operator<< (std::ostream &out, ast const &n)
bool | eq (ast const &a, ast const &b)
expr | select (expr const &a, expr const &i)
| forward declarations More...
expr | select (expr const &a, expr_vector const &i)
expr | implies (expr const &a, expr const &b)
expr | implies (expr const &a, bool b)
expr | implies (bool a, expr const &b)
expr | pw (expr const &a, expr const &b)
expr | pw (expr const &a, int b)
expr | pw (int a, expr const &b)
expr | mod (expr const &a, expr const &b)
expr | mod (expr const &a, int b)
expr | mod (int a, expr const &b)
expr | operator% (expr const &a, expr const &b)
expr | operator% (expr const &a, int b)
expr | operator% (int a, expr const &b)
expr | rem (expr const &a, expr const &b)
expr | rem (expr const &a, int b)
expr | rem (int a, expr const &b)
expr | operator! (expr const &a)
expr | is_int (expr const &e)
expr | operator&& (expr const &a, expr const &b)
expr | operator&& (expr const &a, bool b)
expr | operator&& (bool a, expr const &b)
expr | operator|| (expr const &a, expr const &b)
expr | operator|| (expr const &a, bool b)
expr | operator|| (bool 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, double b)
expr | operator== (double 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, double b)
expr | operator!= (double 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, 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, 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 | nand (expr const &a, expr const &b)
expr | nor (expr const &a, expr const &b)
expr | xnor (expr const &a, expr const &b)
expr | min (expr const &a, expr const &b)
expr | max (expr const &a, expr const &b)
expr | bvredor (expr const &a)
expr | bvredand (expr const &a)
expr | abs (expr const &a)
expr | sqrt (expr const &a, expr const &rm)
expr | fp_eq (expr const &a, expr const &b)
expr | operator~ (expr const &a)
expr | fma (expr const &a, expr const &b, expr const &c, expr const &rm)
expr | fpa_fp (expr const &sgn, expr const &exp, expr const &sig)
expr | fpa_to_sbv (expr const &t, unsigned sz)
expr | fpa_to_ubv (expr const &t, unsigned sz)
expr | sbv_to_fpa (expr const &t, sort s)
expr | ubv_to_fpa (expr const &t, sort s)
expr | fpa_to_fpa (expr const &t, sort s)
expr | round_fpa_to_closest_integer (expr const &t)
expr | ite (expr const &c, expr const &t, expr const &e)
| Create the if-then-else expression `ite(c, t, e)` More...
expr | to_expr (context &c, Z3_ast a)
| Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the whole C API with the C++ layer defined in this file. More...
sort | to_sort (context &c, Z3_sort s)
func_decl | to_func_decl (context &c, Z3_func_decl f)
expr | sle (expr const &a, expr const &b)
| signed less than or equal to operator for bitvectors. More...
expr | sle (expr const &a, int b)
expr | sle (int a, expr const &b)
expr | slt (expr const &a, expr const &b)
| signed less than operator for bitvectors. More...
expr | slt (expr const &a, int b)
expr | slt (int a, expr const &b)
expr | sge (expr const &a, expr const &b)
| signed greater than or equal to operator for bitvectors. More...
expr | sge (expr const &a, int b)
expr | sge (int a, expr const &b)
expr | sgt (expr const &a, expr const &b)
| signed greater than operator for bitvectors. More...
expr | sgt (expr const &a, int b)
expr | sgt (int a, expr const &b)
expr | ule (expr const &a, expr const &b)
| unsigned less than or equal to operator for bitvectors. More...
expr | ule (expr const &a, int b)
expr | ule (int a, expr const &b)
expr | ult (expr const &a, expr const &b)
| unsigned less than operator for bitvectors. More...
expr | ult (expr const &a, int b)
expr | ult (int a, expr const &b)
expr | uge (expr const &a, expr const &b)
| unsigned greater than or equal to operator for bitvectors. More...
expr | uge (expr const &a, int b)
expr | uge (int a, expr const &b)
expr | ugt (expr const &a, expr const &b)
| unsigned greater than operator for bitvectors. More...
expr | ugt (expr const &a, int b)
expr | ugt (int a, expr const &b)
expr | udiv (expr const &a, expr const &b)
| unsigned division operator for bitvectors. More...
expr | udiv (expr const &a, int b)
expr | udiv (int a, expr const &b)
expr | srem (expr const &a, expr const &b)
| signed remainder operator for bitvectors More...
expr | srem (expr const &a, int b)
expr | srem (int a, expr const &b)
expr | smod (expr const &a, expr const &b)
| signed modulus operator for bitvectors More...
expr | smod (expr const &a, int b)
expr | smod (int a, expr const &b)
expr | urem (expr const &a, expr const &b)
| unsigned reminder operator for bitvectors More...
expr | urem (expr const &a, int b)
expr | urem (int a, expr const &b)
expr | shl (expr const &a, expr const &b)
| shift left operator for bitvectors More...
expr | shl (expr const &a, int b)
expr | shl (int a, expr const &b)
expr | lshr (expr const &a, expr const &b)
| logic shift right operator for bitvectors More...
expr | lshr (expr const &a, int b)
expr | lshr (int a, expr const &b)
expr | ashr (expr const &a, expr const &b)
| arithmetic shift right operator for bitvectors More...
expr | ashr (expr const &a, int b)
expr | ashr (int a, expr const &b)
expr | zext (expr const &a, unsigned i)
| Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector. More...
expr | bv2int (expr const &a, bool is_signed)
| bit-vector and integer conversions. More...
expr | int2bv (unsigned n, expr const &a)
expr | bvadd_no_overflow (expr const &a, expr const &b, bool is_signed)
| bit-vector overflow/underflow checks More...
expr | bvadd_no_underflow (expr const &a, expr const &b)
expr | bvsub_no_overflow (expr const &a, expr const &b)
expr | bvsub_no_underflow (expr const &a, expr const &b, bool is_signed)
expr | bvsdiv_no_overflow (expr const &a, expr const &b)
expr | bvneg_no_overflow (expr const &a)
expr | bvmul_no_overflow (expr const &a, expr const &b, bool is_signed)
expr | bvmul_no_underflow (expr const &a, expr const &b)
expr | sext (expr const &a, unsigned i)
| Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector. More...
func_decl | linear_order (sort const &a, unsigned index)
func_decl | partial_order (sort const &a, unsigned index)
func_decl | piecewise_linear_order (sort const &a, unsigned index)
func_decl | tree_order (sort const &a, unsigned index)
expr | forall (expr const &x, expr const &b)
expr | forall (expr const &x1, expr const &x2, expr const &b)
expr | forall (expr const &x1, expr const &x2, expr const &x3, expr const &b)
expr | forall (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
expr | forall (expr_vector const &xs, expr const &b)
expr | exists (expr const &x, expr const &b)
expr | exists (expr const &x1, expr const &x2, expr const &b)
expr | exists (expr const &x1, expr const &x2, expr const &x3, expr const &b)
expr | exists (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
expr | exists (expr_vector const &xs, expr const &b)
expr | lambda (expr const &x, expr const &b)
expr | lambda (expr const &x1, expr const &x2, expr const &b)
expr | lambda (expr const &x1, expr const &x2, expr const &x3, expr const &b)
expr | lambda (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
expr | lambda (expr_vector const &xs, expr const &b)
expr | pble (expr_vector const &es, int const *coeffs, int bound)
expr | pbge (expr_vector const &es, int const *coeffs, int bound)
expr | pbeq (expr_vector const &es, int const *coeffs, int bound)
expr | atmost (expr_vector const &es, unsigned bound)
expr | atleast (expr_vector const &es, unsigned bound)
expr | sum (expr_vector const &args)
expr | distinct (expr_vector const &args)
expr | concat (expr const &a, expr const &b)
expr | concat (expr_vector const &args)
expr | mk_or (expr_vector const &args)
expr | mk_and (expr_vector const &args)
std::ostream & | operator<< (std::ostream &out, model const &m)
std::ostream & | operator<< (std::ostream &out, stats const &s)
std::ostream & | operator<< (std::ostream &out, check_result r)
std::ostream & | operator<< (std::ostream &out, solver const &s)
std::ostream & | operator<< (std::ostream &out, goal const &g)
std::ostream & | operator<< (std::ostream &out, apply_result const &r)
tactic | operator& (tactic const &t1, tactic const &t2)
tactic | operator| (tactic const &t1, tactic const &t2)
tactic | repeat (tactic const &t, unsigned max=UINT_MAX)
tactic | with (tactic const &t, params const &p)
tactic | try_for (tactic const &t, unsigned ms)
tactic | par_or (unsigned n, tactic const *tactics)
tactic | par_and_then (tactic const &t1, tactic const &t2)
probe | operator<= (probe const &p1, probe const &p2)
probe | operator<= (probe const &p1, double p2)
probe | operator<= (double p1, probe const &p2)
probe | operator>= (probe const &p1, probe const &p2)
probe | operator>= (probe const &p1, double p2)
probe | operator>= (double p1, probe const &p2)
probe | operator< (probe const &p1, probe const &p2)
probe | operator< (probe const &p1, double p2)
probe | operator< (double p1, probe const &p2)
probe | operator> (probe const &p1, probe const &p2)
probe | operator> (probe const &p1, double p2)
probe | operator> (double p1, probe const &p2)
probe | operator== (probe const &p1, probe const &p2)
probe | operator== (probe const &p1, double p2)
probe | operator== (double p1, probe const &p2)
probe | operator&& (probe const &p1, probe const &p2)
probe | operator|| (probe const &p1, probe const &p2)
probe | operator! (probe const &p)
std::ostream & | operator<< (std::ostream &out, optimize const &s)
std::ostream & | operator<< (std::ostream &out, fixedpoint const &f)
tactic | fail_if (probe const &p)
tactic | when (probe const &p, tactic const &t)
tactic | cond (probe const &p, tactic const &t1, tactic const &t2)
expr | to_real (expr const &a)
func_decl | function (symbol const &name, unsigned arity, sort const *domain, sort const &range)
func_decl | function (char const *name, unsigned arity, sort const *domain, sort const &range)
func_decl | function (char const *name, sort const &domain, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range)
func_decl | function (char const *name, sort_vector const &domain, sort const &range)
func_decl | function (std::string const &name, sort_vector const &domain, sort const &range)
func_decl | recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range)
func_decl | recfun (char const *name, unsigned arity, sort const *domain, sort const &range)
func_decl | recfun (char const *name, sort const &d1, sort const &range)
func_decl | recfun (char const *name, sort const &d1, sort const &d2, sort const &range)
expr | select (expr const &a, int i)
expr | store (expr const &a, expr const &i, expr const &v)
expr | store (expr const &a, int i, expr const &v)
expr | store (expr const &a, expr i, int v)
expr | store (expr const &a, int i, int v)
expr | store (expr const &a, expr_vector const &i, expr const &v)
expr | as_array (func_decl &f)
expr | const_array (sort const &d, expr const &v)
expr | empty_set (sort const &s)
expr | full_set (sort const &s)
expr | set_add (expr const &s, expr const &e)
expr | set_del (expr const &s, expr const &e)
expr | set_union (expr const &a, expr const &b)
expr | set_intersect (expr const &a, expr const &b)
expr | set_difference (expr const &a, expr const &b)
expr | set_complement (expr const &a)
expr | set_member (expr const &s, expr const &e)
expr | set_subset (expr const &a, expr const &b)
expr | empty (sort const &s)
expr | suffixof (expr const &a, expr const &b)
expr | prefixof (expr const &a, expr const &b)
expr | indexof (expr const &s, expr const &substr, expr const &offset)
expr | last_indexof (expr const &s, expr const &substr)
expr | to_re (expr const &s)
expr | in_re (expr const &s, expr const &re)
expr | plus (expr const &re)
expr | option (expr const &re)
expr | star (expr const &re)
expr | re_empty (sort const &s)
expr | re_full (sort const &s)
expr | re_intersect (expr_vector const &args)
expr | re_complement (expr const &a)
expr | range (expr const &lo, expr const &hi)

## Macro Definition Documentation

## ◆ _Z3_MK_BIN_

#define _Z3_MK_BIN_ | ( |  | a,
|  |  | b,
|  |  | binop
| ) |  |

Value:
check_context(a, b); \
Z3_ast r = binop(a.ctx(), a, b); \
a.check_error(); \
return expr(a.ctx(), r); \
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:426

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

## ◆ _Z3_MK_UN_

#define _Z3_MK_UN_ | ( |  | a,
|  |  | mkun
| ) |  |

Value:
Z3_ast r = mkun(a.ctx(), a); \
a.check_error(); \
return expr(a.ctx(), r); \

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

## ◆ MK_EXPR1

#define MK_EXPR1 | ( |  | _fn,
|  |  | _arg
| ) |  |

Value:
Z3_ast r = _fn(_arg.ctx(), _arg); \
_arg.check_error(); \
return expr(_arg.ctx(), r);

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

## ◆ MK_EXPR2

#define MK_EXPR2 | ( |  | _fn,
|  |  | _arg1,
|  |  | _arg2
| ) |  |

Value:
check_context(_arg1, _arg2); \
Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
_arg1.check_error(); \
return expr(_arg1.ctx(), r);

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

## ◆ Z3_THROW

#define Z3_THROW | ( |  | x | ) | {}

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