Z3
Namespaces | Data Structures
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  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  parameter
 class for auxiliary parameters associated with func_decl The class is initialized with a func_decl or application expression and an index The accessor get_expr, get_sort, ... is available depending on the value of kind(). The caller is responsible to check that the kind of the parameter aligns with the call (get_expr etc). More...
 
class  solver::cube_iterator
 
class  solver::cube_generator
 
class  solver
 
class  goal
 
class  apply_result
 
class  tactic
 
class  simplifier
 
class  probe
 
class  optimize::handle
 
class  optimize
 
class  fixedpoint
 
class  constructor_list
 
class  constructors
 
class  on_clause
 
class  user_propagator_base
 

Detailed Description