content: {-# 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 <> Opts ps2 = Opts (ps1 ++ ps2)
  #endif
  
  instance Monoid Opts where
    mempty = Opts []
  #if MIN_VERSION_base(4,9,0)
    mappend = (<>)
  #else
    Opts ps1 `mappend` Opts ps2 = Opts (ps1 ++ ps2)
  #endif
  
  singleton :: Opt -> Opts
  singleton o = Opts [o]
  
  -- | Default configuration.
  stdOpts :: Opts
  stdOpts = mempty
  
  -- | Append configurations.
  (+?) :: Opts -> Opts -> Opts
  (+?) = mappend
  
  -- | Set a configuration option.
  opt :: OptValue val => String -> val -> Opts
  opt oid val = singleton $ option oid 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 baseCfg (Opts params) = mapM_ (setOpt baseCfg) params
  
  -------------------------------------------------
  -- Options
  
  -- | Pair option-value.
  data Opt = Opt String  -- id
                 String  -- value
  
  -- | Set an option.
  setOpt :: Base.Config -> Opt -> IO ()
  setOpt baseCfg (Opt oid val) = Base.setParamValue baseCfg oid 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 oid = Opt oid . boolVal
  
  instance OptValue Int where
    option oid = Opt oid . show
  
  instance OptValue Integer where
    option oid = Opt oid . show
  
  instance Fixed.HasResolution a => OptValue (Fixed a) where
    option oid = Opt oid . Fixed.showFixed True
  
  instance OptValue [Char] where
    option = Opt
  
  -------------------------------------------------
  -- Utils
  
  boolVal :: Bool -> String
  boolVal True  = "true"
  boolVal False = "false"
  