{-# LANGUAGE CPP #-}

-- |
-- Module    : Z3.Opts
-- 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>
--
-- 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.
--

module Z3.Opts
  ( -- * Z3 configuration
    Opts
  , setOpts
  , stdOpts
  , (+?)
    -- * Z3 options
  , opt
  , OptValue
  )
  where

import qualified Z3.Base as Base

import           Data.Fixed  ( Fixed )
import qualified Data.Fixed as Fixed
import           Data.Monoid ( Monoid(..) )

#if MIN_VERSION_base(4,9,0)
import           Data.Semigroup ( Semigroup (..) )
#endif

---------------------------------------------------------------------
-- Configuration

-- | Z3 configuration.
newtype Opts = Opts [Opt]

#if MIN_VERSION_base(4,9,0)
instance Semigroup Opts where
  Opts ps1 :: [Opt]
ps1 <> :: Opts -> Opts -> Opts
<> Opts ps2 :: [Opt]
ps2 = [Opt] -> Opts
Opts ([Opt]
ps1 [Opt] -> [Opt] -> [Opt]
forall a. [a] -> [a] -> [a]
++ [Opt]
ps2)
#endif

instance Monoid Opts where
  mempty :: Opts
mempty = [Opt] -> Opts
Opts []
#if MIN_VERSION_base(4,9,0)
  mappend :: Opts -> Opts -> Opts
mappend = Opts -> Opts -> Opts
forall a. Semigroup a => a -> a -> a
(<>)
#else
  Opts ps1 `mappend` Opts ps2 = Opts (ps1 ++ ps2)
#endif

singleton :: Opt -> Opts
singleton :: Opt -> Opts
singleton o :: Opt
o = [Opt] -> Opts
Opts [Opt
o]

-- | Default configuration.
stdOpts :: Opts
stdOpts :: Opts
stdOpts = Opts
forall a. Monoid a => a
mempty

-- | Append configurations.
(+?) :: Opts -> Opts -> Opts
+? :: Opts -> Opts -> Opts
(+?) = Opts -> Opts -> Opts
forall a. Monoid a => a -> a -> a
mappend

-- | Set a configuration option.
opt :: OptValue val => String -> val -> Opts
opt :: String -> val -> Opts
opt oid :: String
oid val :: val
val = Opt -> Opts
singleton (Opt -> Opts) -> Opt -> Opts
forall a b. (a -> b) -> a -> b
$ String -> val -> Opt
forall val. OptValue val => String -> val -> Opt
option String
oid val
val

-- | Set configuration.
--
-- If you are using the 'Z3.Monad' interface, you don't need to
-- call this function directly, just pass your 'Opts' to /evalZ3*/
-- functions.
setOpts :: Base.Config -> Opts -> IO ()
setOpts :: Config -> Opts -> IO ()
setOpts baseCfg :: Config
baseCfg (Opts params :: [Opt]
params) = (Opt -> IO ()) -> [Opt] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Config -> Opt -> IO ()
setOpt Config
baseCfg) [Opt]
params

-------------------------------------------------
-- Options

-- | Pair option-value.
data Opt = Opt String  -- id
               String  -- value

-- | Set an option.
setOpt :: Base.Config -> Opt -> IO ()
setOpt :: Config -> Opt -> IO ()
setOpt baseCfg :: Config
baseCfg (Opt oid :: String
oid val :: String
val) = Config -> String -> String -> IO ()
Base.setParamValue Config
baseCfg String
oid String
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.
class OptValue val where
  option :: String -> val -> Opt

instance OptValue Bool where
  option :: String -> Bool -> Opt
option oid :: String
oid = String -> String -> Opt
Opt String
oid (String -> Opt) -> (Bool -> String) -> Bool -> Opt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
boolVal

instance OptValue Int where
  option :: String -> Int -> Opt
option oid :: String
oid = String -> String -> Opt
Opt String
oid (String -> Opt) -> (Int -> String) -> Int -> Opt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show

instance OptValue Integer where
  option :: String -> Integer -> Opt
option oid :: String
oid = String -> String -> Opt
Opt String
oid (String -> Opt) -> (Integer -> String) -> Integer -> Opt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show

instance Fixed.HasResolution a => OptValue (Fixed a) where
  option :: String -> Fixed a -> Opt
option oid :: String
oid = String -> String -> Opt
Opt String
oid (String -> Opt) -> (Fixed a -> String) -> Fixed a -> Opt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Fixed a -> String
forall a. HasResolution a => Bool -> Fixed a -> String
Fixed.showFixed Bool
True

instance OptValue [Char] where
  option :: String -> String -> Opt
option = String -> String -> Opt
Opt

-------------------------------------------------
-- Utils

boolVal :: Bool -> String
boolVal :: Bool -> String
boolVal True  = "true"
boolVal False = "false"