Configuring Z3.

Z3 has plenty of configuration options and these had varied quite a lot from Z3 3.x to Z3 4.x. We decided to keep things simple.

Configurations are essentially sets of String pairs, assigning values to parameters. We just provide a thin layer of abstraction on top of this.

For instance, opt "proof" True creates a configuration where proof generation is enabled. The first argument of opt is the option name, the second is the option value. The same configuration is created by opt "proof" "true". We do not check option names, and we do not assign types to options ---any String is accepted as a value. The OptValue class is a specialization of Show to convert Haskell values into a proper String representation for Z3.

Configurations can be combined with the +? operator, for instance, opt "proof" True +? opt "model" True is a configuration with both proof and model generation enabled. Configurations are Monoids, and +? is just an alias for mappend.

Configurations are set by setOpts if you are using Z3.Base, or passing the configuration object (of type Opts) to a runner if you are using the Z3.Monad interface.