{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Provers.MathSAT(mathSAT) where
import Data.SBV.Core.Data
import Data.SBV.SMT.SMT
import Data.SBV.Control.Types
mathSAT :: SMTSolver
mathSAT :: SMTSolver
mathSAT = SMTSolver :: Solver
-> String
-> (String -> String)
-> (SMTConfig -> [String])
-> SMTEngine
-> SolverCapabilities
-> SMTSolver
SMTSolver {
name :: Solver
name = Solver
MathSAT
, executable :: String
executable = "mathsat"
, preprocess :: String -> String
preprocess = String -> String
forall a. a -> a
id
, options :: SMTConfig -> [String]
options = [String] -> SMTConfig -> [String]
modConfig ["-input=smt2", "-theory.fp.minmax_zero_mode=4"]
, engine :: SMTEngine
engine = String -> String -> SMTEngine
standardEngine "SBV_MATHSAT" "SBV_MATHSAT_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
False
, supportsIEEE754 :: Bool
supportsIEEE754 = Bool
True
, supportsSets :: Bool
supportsSets = Bool
False
, supportsOptimization :: Bool
supportsOptimization = Bool
False
, supportsPseudoBooleans :: Bool
supportsPseudoBooleans = Bool
False
, supportsCustomQueries :: Bool
supportsCustomQueries = Bool
True
, supportsGlobalDecls :: Bool
supportsGlobalDecls = Bool
False
, supportsDataTypes :: Bool
supportsDataTypes = Bool
True
, supportsFlattenedModels :: Maybe [String]
supportsFlattenedModels = Maybe [String]
forall a. Maybe a
Nothing
}
}
where
modConfig :: [String] -> SMTConfig -> [String]
modConfig :: [String] -> SMTConfig -> [String]
modConfig opts :: [String]
opts cfg :: SMTConfig
cfg
| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool
b | ProduceUnsatCores b :: Bool
b <- SMTConfig -> [SMTOption]
solverSetOptions SMTConfig
cfg]
= [String]
opts [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["-unsat_core_generation=3"]
| Bool
True
= [String]
opts