Crate z3

Z3

Z3 is a theorem prover from Microsoft Research.

Modules

• ast
  Abstract syntax tree (AST).
• datatype_builder
  Helpers for building custom datatype sorts.

Structs

• ApplyResult
  Collection of subgoals resulting from applying of a tactic to a goal.
• Config
  Configuration used to initialize logical contexts.
• Context
  Manager of all other Z3 objects, global configuration options, etc.
• ContextHandle
  Handle that can be used to interrupt a computation from another thread.
• DatatypeBuilder
  Build a custom datatype sort.
• DatatypeSort
  A custom datatype sort.
• DatatypeVariant
  Inner variant for a custom datatype sort.
• FuncDecl
  Function declaration. Every constant and function have an associated declaration.
• FuncEntry
  Store the value of the interpretation of a function in a particular point. https://z3prover.github.io/api/html/classz3py_1_1_func_entry.html
• FuncInterp
  Stores the interpretation of a function in a Z3 model. https://z3prover.github.io/api/html/classz3py_1_1_func_interp.html
• Goal
  Set of formulas that can be solved and/or transformed using tactics and solvers.
• IsNotApp
  A struct to represent when an ast is not a function application.
• Model
  Model for the constraints inserted into the logical context.
• Optimize
  Context for solving optimization queries.
• Params
  Parameter set used to configure many components (simplifiers, tactics, solvers, etc).
• Pattern
  A pattern for quantifier instantiation, used to guide quantifier instantiation.
• Probe
  Function/predicate used to inspect a goal and collect information that may be used to decide which solver and/or preprocessing step will be used.
• RecFuncDecl
  Recursive function declaration. Every function has an associated declaration.
• Solver
  (Incremental) solver, possibly specialized by a particular tactic or logic.
• Sort
  Sorts represent the various ‘types’ of Asts.
• SortDiffers
  A struct to represent when two sorts are of different types.
• Statistics
  Statistical data about a solver.
• StatisticsEntry
  A key, value entry within Statistics.
• Tactic
  Basic building block for creating custom solvers for specific problem domains.

Enums

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

Functions

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