Classes

The abstract syntax tree (AST) class for Expression syntaxes.

An expression abstract syntax tree (AST) class that is typed with a sort to allow for compile-time static type checking of expressions.

An algebraic number that can be used in the Z3 real algebraic number package.

A numeral value belonging to a specific finite domain.

An AST class for Z3 regular expression sorts with a given base element sort.

An AST class for Z3 sequence sorts with a given base element sort.

A named finite domain.

A function declaration node.

Kind of AST used to represent pattern and multi-patterns used to guide quantifier instantiation.

Z3ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.

Abstract syntax tree node. That is, the data-structure used in Z3 to represent terms, formulas and types. Base class for Z3Sort, Z3FuncDecl, Z3Pattern, and AnyZ3Ast.

Map of Z3AstBase objects.

Vector of Z3AstBase objects.

A configuration object for the Z3 context object.

Configurations are created in order to assign parameters prior to creating contexts for Z3 interaction. For example, if the users wishes to use proof generation, then call:

Z3Config.setParameter("proof", "true")

The following parameters can be set:

• proof: (Boolean) Enable proof generation
• debug_ref_count: (Boolean) Enable debug support for Z3_ast reference counting
• trace: (Boolean) Tracing support for VCC
• trace_file_name: (String) Trace out file for VCC traces
• timeout: (unsigned) default timeout (in milliseconds) used for solvers
• well_sorted_check: type checker
• auto_config: use heuristics to automatically select solver and configure it
• model: model generation for solvers, this parameter can be overwritten when creating a solver
• model_validate: validate models produced by solvers
• unsat_core: unsat-core generation for solvers, this parameter can be overwritten when creating a solver
• encoding: the string encoding used internally (must be either “unicode” - 18 bit, “bmp” - 16 bit or “ascii” - 8 bit)

Type constructor for a (recursive) datatype.

List of constructors for a (recursive) datatype.

Main interaction point to Z3.

Context for the recursive predicate solver.

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

Model for the constraints asserted into the logical context.

Object for managing optimization context.

Provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters.

Parameter set used to configure many components such as: simplifiers, tactics, solvers, etc.

Context for incrementally parsing strings. Declarations can be added incrementally to the parser state.

A class describing a probe in Z3. Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used.

Base class for Z3 objects that support reference counting.

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

Provides statistical data for a solver.

Lisp-like symbol used to name types, constants, and functions. A symbol can be created using string or integers.

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