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	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

Enumerations
enum	check_result { unsat, sat, unknown }

Detailed Description

Enumeration Type Documentation

enum check_result

Enumerator
unsat
sat
unknown

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

                      {
        unsat, sat, unknown
    };