module Language.Hasmtlib.Solver.MathSAT where

import SMTLIB.Backends.Process
import Language.Hasmtlib.Type.Solver

-- | A 'SolverConfig' for MathSAT.
--   Requires binary @mathsat@ to be in path.
mathsat :: SolverConfig s
mathsat :: forall s. SolverConfig s
mathsat = Config -> Maybe Int -> Maybe (Debugger s) -> SolverConfig s
forall s.
Config -> Maybe Int -> Maybe (Debugger s) -> SolverConfig s
SolverConfig
  (Config
defaultConfig { exe = "mathsat", args = [] })
  Maybe Int
forall a. Maybe a
Nothing
  Maybe (Debugger s)
forall a. Maybe a
Nothing

-- | A 'SolverConfig' for OptiMathSAT.
--   Requires binary @optimathsat@ to be in path.
optimathsat :: SolverConfig s
optimathsat :: forall s. SolverConfig s
optimathsat = Config -> Maybe Int -> Maybe (Debugger s) -> SolverConfig s
forall s.
Config -> Maybe Int -> Maybe (Debugger s) -> SolverConfig s
SolverConfig
  (Config
defaultConfig { exe = "optimathsat", args = ["-optimization=true"] })
  Maybe Int
forall a. Maybe a
Nothing
  Maybe (Debugger s)
forall a. Maybe a
Nothing