module Ersatz.Solver
( module Ersatz.Solver.DepQBF
, module Ersatz.Solver.Minisat
, module Ersatz.Solver.Z3
, solveWith
) where
import Control.Monad
import Control.Monad.State
import Data.Default
import Ersatz.Codec
import Ersatz.Problem
import Ersatz.Solution
import Ersatz.Solver.DepQBF
import Ersatz.Solver.Minisat
import Ersatz.Solver.Z3
solveWith ::
(Monad m, MonadPlus n, HasSAT s, Default s, Codec a) =>
Solver s m -> StateT s m a -> m (Result, n (Decoded a))
solveWith :: Solver s m -> StateT s m a -> m (Result, n (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, n (Decoded a)) -> m (Result, n (Decoded a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
res, Solution -> a -> n (Decoded a)
forall a (f :: * -> *).
(Codec a, MonadPlus f) =>
Solution -> a -> f (Decoded a)
decode (IntMap Bool -> s -> Solution
forall s. HasSAT s => IntMap Bool -> s -> Solution
solutionFrom IntMap Bool
litMap s
problem) a
a)