{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Provers.Z3(z3) where
import Data.SBV.Core.Data
import Data.SBV.SMT.SMT
z3 :: SMTSolver
z3 :: SMTSolver
z3 = SMTSolver :: Solver
-> String
-> (String -> String)
-> (SMTConfig -> [String])
-> SMTEngine
-> SolverCapabilities
-> SMTSolver
SMTSolver {
name :: Solver
name = Solver
Z3
, executable :: String
executable = "z3"
, preprocess :: String -> String
preprocess = String -> String
forall a. a -> a
id
, options :: SMTConfig -> [String]
options = [String] -> SMTConfig -> [String]
modConfig ["-nw", "-in", "-smt2"]
, engine :: SMTEngine
engine = String -> String -> SMTEngine
standardEngine "SBV_Z3" "SBV_Z3_OPTIONS"
, capabilities :: SolverCapabilities
capabilities = SolverCapabilities :: Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Maybe [String]
-> SolverCapabilities
SolverCapabilities {
supportsQuantifiers :: Bool
supportsQuantifiers = Bool
True
, supportsUninterpretedSorts :: Bool
supportsUninterpretedSorts = Bool
True
, supportsUnboundedInts :: Bool
supportsUnboundedInts = Bool
True
, supportsReals :: Bool
supportsReals = Bool
True
, supportsApproxReals :: Bool
supportsApproxReals = Bool
True
, supportsIEEE754 :: Bool
supportsIEEE754 = Bool
True
, supportsSets :: Bool
supportsSets = Bool
True
, supportsOptimization :: Bool
supportsOptimization = Bool
True
, supportsPseudoBooleans :: Bool
supportsPseudoBooleans = Bool
True
, supportsCustomQueries :: Bool
supportsCustomQueries = Bool
True
, supportsGlobalDecls :: Bool
supportsGlobalDecls = Bool
True
, supportsDataTypes :: Bool
supportsDataTypes = Bool
True
, supportsFlattenedModels :: Maybe [String]
supportsFlattenedModels = [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ "(set-option :pp.max_depth 4294967295)"
, "(set-option :pp.min_alias_size 4294967295)"
, "(set-option :model.inline_def true )"
]
}
}
where modConfig :: [String] -> SMTConfig -> [String]
modConfig :: [String] -> SMTConfig -> [String]
modConfig opts :: [String]
opts _cfg :: SMTConfig
_cfg = [String]
opts