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 |
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 Monoid
s,
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.
Z3 configuration
Z3 options
Values for Z3 options.
Any OptValue
type can be passed to a Z3 option (and values will be
converted into an appropriate String
).
Since 0.4 the Double
instance has been replaced by a new Fixed
instance.
option