Heyo all! Does anyone know if it is possible to dynamically change the runtime timeout allocated for a Z3 context at runtime.
The context here is that I’m sending multiple queries to Z3, but I know that certain ones are more challenging, and I’d like to allocate more time before giving up with a timeout.
I’ve tried the following:
let set_timeout solver timeout =
let params = Z3.Params.mk_params ctx in
Z3.Params.add_int params (Z3.Symbol.mk_string ctx "timeout") timeout;
Z3.Solver.set_parameters solver params
However, this doesn’t seem to actually change the timeout - it does correctly set the timeout the first time I call it, but then am unable to change the timeout at a later point in the execution.
I’ve had a look through the Z3 api bindings, but it doesn’t seem like there are any explanations of why this might not work, or what I should use instead.
The closest I could get was a function:
val Z3.Params.update_param_value : Z3.context -> string -> string -> unit
But I’m not sure what this does, and trying to use it to set the timeout doesn’t work either.
I have no experience to use this API yet, but the document of Z3.Params may suggest an OCaml string as a param, rather than a
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.
I can set it to other values in utop.
utop # #require "z3";;
utop # let ctx = Z3.mk_context ;;
val ctx : Z3.context = <abstr>
utop # Z3.Params.update_param_value ctx "timeout" "1";;
- : unit = ()
utop # Z3.Params.update_param_value ctx "nonexist" "1";;
Z3.Error("unknown parameter 'nonexist'\n Legal parameters are:\n ...)
I am using the
update_param_value, as @arbipher suggested, and it works for me as a charm, here’s my function,
let set_timeout ms =
Z3.Params.update_param_value ctxt "timeout" (string_of_int ms)
Note that the timeout is in milliseconds.
Thanks for the responses, yes, managed to solve the problem.