Crate z3[][src]


Abstract syntax tree (AST).

Helpers for building custom datatype sorts.


Collection of subgoals resulting from applying of a tactic to a goal.

Configuration used to initialize logical contexts.

Manager of all other Z3 objects, global configuration options, etc.

Handle that can be used to interrupt a computation from another thread.

Build a custom datatype sort.

A custom datatype sort.

Inner variant for a custom datatype sort.

Function declaration. Every constant and function have an associated declaration.

Set of formulas that can be solved and/or transformed using tactics and solvers.

A struct to represent when an ast is not a function application.

Model for the constraints inserted into the logical context.

Context for solving optimization queries.

Parameter set used to configure many components (simplifiers, tactics, solvers, etc).

A pattern for quantifier instantiation, used to guide quantifier instantiation.

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.

Recursive function declaration. Every function has an associated declaration.

(Incremental) solver, possibly specialized by a particular tactic or logic.

Sorts represent the various ‘types’ of Asts.

A struct to represent when two sorts are of different types.

Basic building block for creating custom solvers for specific problem domains.


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.

Symbols are used to name several term and type constructors.