{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Provers.Boolector(boolector) where
import Data.SBV.Core.Data
import Data.SBV.SMT.SMT
boolector :: SMTSolver
boolector :: SMTSolver
boolector = SMTSolver :: Solver
-> String
-> (String -> String)
-> (SMTConfig -> [String])
-> SMTEngine
-> SolverCapabilities
-> SMTSolver
SMTSolver {
name :: Solver
name = Solver
Boolector
, executable :: String
executable = "boolector"
, preprocess :: String -> String
preprocess = String -> String
forall a. a -> a
id
, options :: SMTConfig -> [String]
options = [String] -> SMTConfig -> [String]
forall a b. a -> b -> a
const ["--smt2", "--smt2-model", "--no-exit-codes", "--incremental"]
, engine :: SMTEngine
engine = String -> String -> SMTEngine
standardEngine "SBV_BOOLECTOR" "SBV_BOOLECTOR_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
False
, supportsUninterpretedSorts :: Bool
supportsUninterpretedSorts = Bool
False
, supportsUnboundedInts :: Bool
supportsUnboundedInts = Bool
False
, supportsReals :: Bool
supportsReals = Bool
False
, supportsApproxReals :: Bool
supportsApproxReals = Bool
False
, supportsIEEE754 :: Bool
supportsIEEE754 = Bool
False
, 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
False
, supportsFlattenedModels :: Maybe [String]
supportsFlattenedModels = Maybe [String]
forall a. Maybe a
Nothing
}
}