Z3
Namespaces | Data Structures | Enumerations
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  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 >::iterator
 
class  ast_vector_tpl< T >
 
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
 

Enumerations

enum  check_result { unsat, sat, unknown }
 
enum  rounding_mode {
  RNA, RNE, RTP, RTN,
  RTZ
}
 

Detailed Description

Enumeration Type Documentation

enum check_result
Enumerator
unsat 
sat 
unknown 

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

129  {
130  unsat, sat, unknown
131  };
Definition: z3++.h:130
enum rounding_mode
Enumerator
RNA 
RNE 
RTP 
RTN 
RTZ 

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

133  {
134  RNA,
135  RNE,
136  RTP,
137  RTN,
138  RTZ
139  };
Definition: z3++.h:134
Definition: z3++.h:136
Definition: z3++.h:135
Definition: z3++.h:137
Definition: z3++.h:138