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.