Module Z3.Params

module Params: sig .. end

Parameter sets (of Solvers, Tactics, ...)

A Params objects represents a configuration in the form of Symbol.symbol/value pairs.

type params

module ParamDescrs: sig .. end

ParamDescrs describe sets of parameters (of Solvers, Tactics, ...)

val add_bool : params -> Symbol.symbol -> bool -> unit

Adds a parameter setting.

val add_int : params -> Symbol.symbol -> int -> unit

Adds a parameter setting.

val add_float : params -> Symbol.symbol -> float -> unit

Adds a parameter setting.

val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit

Adds a parameter setting.

val mk_params : context -> params

Creates a new parameter set

val to_string : params -> string

A string representation of the parameter set.

val update_param_value : context -> string -> string -> unit

Update a mutable configuration parameter.

The list of all configuration parameters can be obtained using the Z3 executable: z3.exe -p Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.

val set_print_mode : context -> Z3enums.ast_print_mode -> unit

Selects the format used for pretty-printing expressions.

The default mode for pretty printing expressions is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called PRINT_SMTLIB_FULL. To print shared common subexpressions only once, use the PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use PRINT_SMTLIB_COMPLIANT. AST.to_string Quantifier.Pattern.to_string FuncDecl.to_string Sort.to_string