Z3
Data Structures | Namespaces | Typedefs | Enumerations | Functions
src/api/c++/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  array< T >
class  object
class  symbol
class  params
class  ast
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  ast_vector_tpl< T >
class  func_entry
class  func_interp
class  model
class  stats
class  solver
class  goal
class  apply_result
class  tactic
class  probe

Namespaces

namespace  z3
 

Z3 C++ namespace.


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 }

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 ()
void check_context (object const &a, object const &b)
bool eq (ast const &a, ast 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 ite (expr const &c, expr const &t, expr const &e)
 Create the if-then-else expression ite(c, t, e)
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.
sort to_sort (context &c, Z3_sort s)
func_decl to_func_decl (context &c, Z3_func_decl f)
expr ule (expr const &a, expr const &b)
 unsigned less than or equal to operator for bitvectors.
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.
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.
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.
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.
expr udiv (expr const &a, int b)
expr udiv (int a, expr const &b)
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 distinct (expr_vector const &args)
std::ostream & operator<< (std::ostream &out, check_result r)
check_result to_check_result (Z3_lbool l)
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 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)
expr select (expr const &a, expr const &i)
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 const_array (sort const &d, expr const &v)
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines