{-# LANGUAGE ScopedTypeVariables #-}
module Data.SBV.Provers.Z3(z3) where
import Data.Char (toLower)
import Data.SBV.Core.Data
import Data.SBV.SMT.SMT
import qualified System.Info as S(os)
optionPrefix :: Char
optionPrefix
| map toLower S.os `elem` ["linux", "darwin"] = '-'
| True = '/'
z3 :: SMTSolver
z3 = SMTSolver {
name = Z3
, executable = "z3"
, options = map (optionPrefix:) . modConfig ["nw", "in", "smt2"]
, engine = standardEngine "SBV_Z3" "SBV_Z3_OPTIONS"
, capabilities = SolverCapabilities {
supportsQuantifiers = True
, supportsUninterpretedSorts = True
, supportsUnboundedInts = True
, supportsReals = True
, supportsApproxReals = True
, supportsIEEE754 = True
, supportsOptimization = True
, supportsPseudoBooleans = True
, supportsCustomQueries = True
, supportsGlobalDecls = True
}
}
where modConfig :: [String] -> SMTConfig -> [String]
modConfig opts _cfg = opts