From b70ba6ed73955d60b9b8556055ee3004b083d444 Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Sun, 16 Jun 2024 20:07:49 -0400 Subject: [PATCH] Update doc for `mk_context`. --- src/api/ml/z3.mli | 32 +++++++++++++++++++++++++++++--- 1 file changed, 29 insertions(+), 3 deletions(-) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 5320fc38e..0b31874e1 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -42,9 +42,10 @@ type context - 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 + - model (Boolean) model generation for solvers, this parameter can be overwritten when creating a solver + - model_validate (Boolean) validate models produced by solvers + - unsat_core (Boolean) 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) *) val mk_context : (string * string) list -> context @@ -3712,6 +3713,31 @@ end For example: (set_global_param "pp.decimal" "true") will set the parameter "decimal" in the module "pp" to true. + + Legal parameters are: + auto_config (bool) (default: true) + debug_ref_count (bool) (default: false) + dot_proof_file (string) (default: proof.dot) + dump_models (bool) (default: false) + encoding (string) (default: unicode) + memory_high_watermark (unsigned int) (default: 0) + memory_high_watermark_mb (unsigned int) (default: 0) + memory_max_alloc_count (unsigned int) (default: 0) + memory_max_size (unsigned int) (default: 0) + model (bool) (default: true) + model_validate (bool) (default: false) + proof (bool) (default: false) + rlimit (unsigned int) (default: 0) + smtlib2_compliant (bool) (default: false) + stats (bool) (default: false) + timeout (unsigned int) (default: 4294967295) + trace (bool) (default: false) + trace_file_name (string) (default: z3.log) + type_check (bool) (default: true) + unsat_core (bool) (default: false) + verbose (unsigned int) (default: 0) + warning (bool) (default: true) + well_sorted_check (bool) (default: false) *) val set_global_param : string -> string -> unit