Classes
The following classes are available globally.
-
Z3ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.
See moreDeclaration
Swift
public class Z3ApplyResult : Z3RefCountedObject
-
Abstract syntax tree node. That is, the data-structure used in Z3 to represent terms, formulas and types. Base class for
See moreZ3Sort
,Z3FuncDecl
,Z3Pattern
, andAnyZ3Ast
.Declaration
Swift
public class Z3AstBase : Z3RefCountedObject
-
Declaration
-
Declaration
-
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")
Remark
In previous versions of Z3, theZ3_config
was used to store global and module configurations. Now, we should useZ3GlobalParameters.setParameter(id:value:)
.The following parameters can be set:
proof
: (Boolean) Enable proof generationdebug_ref_count
: (Boolean) Enable debug support for Z3_ast reference countingtrace
: (Boolean) Tracing support for VCCtrace_file_name
: (String) Trace out file for VCC tracestimeout
: (unsigned) default timeout (in milliseconds) used for solverswell_sorted_check
: type checkerauto_config
: use heuristics to automatically select solver and configure itmodel
: model generation for solvers, this parameter can be overwritten when creating a solvermodel_validate
: validate models produced by solversunsat_core
: unsat-core generation for solvers, this parameter can be overwritten when creating a solverencoding
: the string encoding used internally (must be either “unicode” - 18 bit, “bmp” - 16 bit or “ascii” - 8 bit)
Declaration
Swift
public class Z3Config
-
Type constructor for a (recursive) datatype.
See moreDeclaration
Swift
public class Z3Constructor
-
List of constructors for a (recursive) datatype.
See moreDeclaration
Swift
public class Z3ConstructorList
-
Main interaction point to Z3.
See moreDeclaration
Swift
public class Z3Context
-
Context for the recursive predicate solver.
See moreDeclaration
Swift
public class Z3FixedPoint : Z3RefCountedObject
-
Set of formulas that can be solved and/or transformed using tactics and solvers.
See moreDeclaration
Swift
public class Z3Goal : Z3RefCountedObject
-
Model for the constraints asserted into the logical context.
See moreDeclaration
Swift
public class Z3Model : Z3RefCountedObject
-
Object for managing optimization context.
See moreDeclaration
Swift
public class Z3Optimize : Z3RefCountedObject
-
Provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters.
See moreDeclaration
Swift
public class Z3ParamDescrs : Z3RefCountedObject
-
Parameter set used to configure many components such as: simplifiers, tactics, solvers, etc.
See moreDeclaration
Swift
public class Z3Params : Z3RefCountedObject
-
Context for incrementally parsing strings. Declarations can be added incrementally to the parser state.
See moreDeclaration
Swift
public class Z3ParserContext : Z3RefCountedObject
-
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.
See moreDeclaration
Swift
public class Z3Probe : Z3RefCountedObject
-
Base class for Z3 objects that support reference counting.
Declaration
Swift
public class Z3RefCountedObject
-
Incremental solver, possibly specialized by a particular tactic or logic.
See moreDeclaration
Swift
public class Z3Solver : Z3RefCountedObject
-
Provides statistical data for a solver.
See moreDeclaration
Swift
public class Z3Stats : Z3RefCountedObject
-
Lisp-like symbol used to name types, constants, and functions. A symbol can be created using string or integers.
See moreDeclaration
Swift
public class Z3Symbol
-
Basic building block for creating custom solvers for specific problem domains.
See moreDeclaration
Swift
public class Z3Tactic : Z3RefCountedObject