Dynamically changing Z3 timeouts at runtime

Learning
1

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.

2

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 Symbol.

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";;
Exception:
Z3.Error("unknown parameter 'nonexist'\n Legal parameters are:\n ...)
2 Likes
3

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.

1 Like
4

Thanks for the responses, yes, managed to solve the problem.