--------------------------------------------------------------------
-- |
-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Ersatz.Solver
  ( module Ersatz.Solver.DepQBF
  , module Ersatz.Solver.Kissat
  , module Ersatz.Solver.Lingeling
  , module Ersatz.Solver.Minisat
  , module Ersatz.Solver.Z3
  , solveWith
  ) where

import Control.Monad.State
import Data.Default
import Ersatz.Codec
import Ersatz.Problem
import Ersatz.Solution
import Ersatz.Solver.DepQBF
import Ersatz.Solver.Kissat
import Ersatz.Solver.Lingeling
import Ersatz.Solver.Minisat
import Ersatz.Solver.Z3

-- | @'solveWith' solver prob@ solves a SAT problem @prob@ with the given
-- @solver@. It returns a pair consisting of:
--
-- 1. A 'Result' that indicates if @prob@ is satisfiable ('Satisfied'),
--    unsatisfiable ('Unsatisfied'), or if the solver could not determine any
--    results ('Unsolved').
--
-- 2. A 'Decoded' answer that was decoded using the solution to @prob@. Note
--    that this answer is only meaningful if the 'Result' is 'Satisfied' and
--    the answer value is in a 'Just'.
--
-- Here is a small example of how to use 'solveWith':
--
-- @
-- import Ersatz
--
-- main :: IO ()
-- main = do
--   res <- 'solveWith' minisat $ do
--     (b1 :: Bit) <- exists
--     (b2 :: Bit) <- exists
--     assert (b1 === b2)
--     pure [b1, b2]
--   case res of
--     (Satisfied, Just answer) -> print answer
--     _ -> fail "Could not solve problem"
-- @
--
-- Depending on the whims of @minisat@, this program may print either
-- @[False, False]@ or @[True, True]@.
solveWith ::
  (Monad m, HasSAT s, Default s, Codec a) =>
  Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
solveWith :: forall (m :: * -> *) s a.
(Monad m, HasSAT s, Default s, Codec a) =>
Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
solveWith Solver s m
solver StateT s m a
m = do
  (a
a, s
problem) <- StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT s m a
m s
forall a. Default a => a
def
  (Result
res, IntMap Bool
litMap) <- Solver s m
solver s
problem
  (Result, Maybe (Decoded a)) -> m (Result, Maybe (Decoded a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
res, Solution -> a -> Maybe (Decoded a)
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode (IntMap Bool -> s -> Solution
forall s. HasSAT s => IntMap Bool -> s -> Solution
solutionFrom IntMap Bool
litMap s
problem) a
a)