| Copyright | (c) Iago Abal, 2013-2015 (c) David Castro, 2013 |
|---|---|
| License | BSD3 |
| Maintainer | Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com> |
| Safe Haskell | None |
| Language | Haskell98 |
Z3.Opts
Contents
Description
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.