C++ API

Namespaces
	z3
	Z3 C++ namespace.

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 >::iterator
class	ast_vector_tpl< T >
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::iterator
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
class	stats
class	solver::cube_iterator
class	solver::cube_generator
class	solver
class	goal
class	apply_result
class	tactic
class	probe
class	optimize::handle
class	optimize
class	fixedpoint
class	user_propagator_base

Detailed Description