Using Z3's configuration API

Question

Running z3 -p with the latest (unstable) Z3 shows a list of parameters grouped by module. The instructions read:

To set a module parameter, use <module-name>.<parameter-name>=value
Example:  pp.decimal=true

In general, how do these instructions translate to the C API? In the current documentation, there seems to be a set of API calls dealing with "global" configuration, e.g., Z3_set_param_value, and another object-specific set of calls built around the Z3_params type, such as Z3_solver_set_params.

In particular, I was wondering if I can use Z3_set_param_value to globally set any parameter in any module. Other StackOverflow answers advertise the use of Z3_params objects even for global parameters, like timeout (or is it :timeout?), but it's not clear to me how this API maps to the module.parameter=value syntax.

Answer 1

The module/name parameters are mainly for the command-line version of Z3.

Global parameters are meant to be set once in the beginning and will then be valid for all subsequent calls. We introduced this parameter setting scheme together with the new strategies/goals/solvers/tactics/probes interface because we needed different configurations of tactics and the Z3_params object is meant to be used mainly for that. For instance, Z3_tactic_using_params creates a new tactic that is a reconfiguration of another tactic based on the options in the Z3_params object.

Note however, when creating tactics through the API, there are no modules (the tactic you create doesn't live in a Z3-internal `parameter module'). For example, in the strategies tutorial (see here), a tactic is constructed and applied as follows:

(check-sat-using (then (using-params simplify :arith-lhs true :som true)
                        normalize-bounds
                        lia2pb  
                        pb2bv                       
                        bit-blast                       
                        sat))

So, the parameters "arith-lhs" and "som" are enabled for the simplifier. On the commandline, the same option is in the "rewriter" module, i.e., it would be rewriter.arith_lhs=true and if it is enabled on the commmand line, it will be enabled every time the simplifier is called.

A list of tactics and the list of parameters that it recognizes can be obtained by running (on Windows, Linux resp.)

echo (help-tactic) | z3 -in -smt2
echo "(help-tactic)" | z3 -in -smt2

Another thing to note is that parameters in a Z3_params object are not checked in any way, i.e., it is possible to provide a bogus parameter name and Z3 will not complain or issue a warning, the tactics will simply ignore that parameter.

The : in front of parameter names is a left-over of Lisp, which is the basis for the SMT2 format. See, e.g., here: Why colons precede variables in Common Lisp. They are only necessary when using the SMT2 input language. So, the SMT2 command

(set-option :timeout 2000)

is meant to be equivalent to the commandline parameter

timeout=2000

Since the question explicitly mentions the timeout parameter: We recently had some issues with timeout handling on OSX, it may be necessary to get the latest fixes, and of course there may be more bugs that we didn't find yet.

In the C API, the function Z3_global_param_set is used to set the global parameters, and also to set default module parameters. These parameters will be shared by all Z3_context objects created afterwards (i.e., pp.decimal) and they will be used if one of the built-in tactics is applied.