Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
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  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.

1238  {
1239  unsat, sat, unknown
1240  };
Definition: z3++.h:1239