Z3.Opts

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.

Z3 configuration

data Opts

Z3 configuration.

Instances

Semigroup Opts

Methods

(<>) :: Opts -> Opts -> Opts

sconcat :: NonEmpty Opts -> Opts

stimes :: Integral b => b -> Opts -> Opts

Monoid Opts

Methods

mempty :: Opts

mappend :: Opts -> Opts -> Opts

mconcat :: [Opts] -> Opts

setOpts :: Config -> Opts -> IO ()

Set configuration.

If you are using the Monad interface, you don't need to call this function directly, just pass your Opts to evalZ3* functions.

stdOpts :: Opts

Default configuration.

(+?) :: Opts -> Opts -> Opts

Append configurations.

Z3 options

opt :: OptValue val => String -> val -> Opts

Set a configuration option.

class OptValue val

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.

Minimal complete definition

option

Instances

OptValue Bool

Methods

option :: String -> Bool -> Opt

OptValue Int

Methods

option :: String -> Int -> Opt

OptValue Integer

Methods

option :: String -> Integer -> Opt

OptValue [Char]

Methods

option :: String -> [Char] -> Opt

HasResolution a => OptValue (Fixed a)

Methods

option :: String -> Fixed a -> Opt