module Params:sig
..end
A Params objects represents a configuration in the form of Symbol.symbol/value pairs.
type
params
module ParamDescrs:sig
..end
val add_bool : params -> Symbol.symbol -> bool -> unit
val add_int : params -> Symbol.symbol -> int -> unit
val add_float : params -> Symbol.symbol -> float -> unit
val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit
val mk_params : context -> params
val to_string : params -> string
val update_param_value : context -> string -> string -> unit
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
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