module Language.Hasmtlib.Solver.Bitwuzla where

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

-- | A 'SolverConfig' for Bitwuzla.
--   Requires binary @bitwuzla@ to be in path.
--
--   As of v0.5 Bitwuzla uses Cadical as SAT-Solver by default.
--   Make sure it's default SAT-Solver binary - probably @cadical@ - is in path too.
bitwuzla :: SolverConfig s
bitwuzla :: forall s. SolverConfig s
bitwuzla = Config -> Maybe Int -> Maybe (Debugger s) -> SolverConfig s
forall s.
Config -> Maybe Int -> Maybe (Debugger s) -> SolverConfig s
SolverConfig
  (Config
defaultConfig { exe = "bitwuzla", args = [] })
  Maybe Int
forall a. Maybe a
Nothing
  Maybe (Debugger s)
forall a. Maybe a
Nothing


-- | A 'SolverConfig' for Bitwuzla with Kissat as underlying sat-solver.
--
--   Requires binary @bitwuzla@ and to be in path.
--   Will use the @kissat@ shipped with @bitwuzla@.
--
--   It is recommended to build @bitwuzla@ from source for this to work as expected.
bitwuzlaKissat :: SolverConfig s
bitwuzlaKissat :: forall s. SolverConfig s
bitwuzlaKissat = Config -> Maybe Int -> Maybe (Debugger s) -> SolverConfig s
forall s.
Config -> Maybe Int -> Maybe (Debugger s) -> SolverConfig s
SolverConfig
  (Config
defaultConfig { exe = "bitwuzla", args = ["--sat-solver=kissat"] })
  Maybe Int
forall a. Maybe a
Nothing
  Maybe (Debugger s)
forall a. Maybe a
Nothing