Z3Config
public class Z3Config
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 use Z3GlobalParameters.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 init()
-
Declaration
Swift
public func setParameter(name: String, value: String)