z3++.h File Reference

Go to the source code of this file.

Data Structures
class	ast_vector_tpl< T >
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< T >
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
	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) 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	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	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)