All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Namespaces | Data Structures | Enumerations


 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


enum  check_result { unsat, sat, unknown }

Detailed Description

Enumeration Type Documentation

enum check_result

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

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