Crate z3

source ·
Expand description


Z3 is a theorem prover from Microsoft Research.




  • The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
  • Wrapper which can point to a sort (by value) or to a custom datatype (by name).
  • The different kinds of interpreted function kinds.
  • Precision of a given goal. Some goals can be transformed using over/under approximations.
  • Result of a satisfiability query.
  • The different kinds of Z3 types.
  • The value for a key in Statistics.
  • Symbols are used to name several term and type constructors.


  • Get a global (or module) parameter.
  • Restore the value of all global (and module) parameters. This command will not affect already created objects (such as tactics and solvers).
  • Set a global (or module) parameter. This setting is shared by all Z3 contexts.