-------------------------------------------------------------------- -- | -- 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.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.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) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s) runStateT StateT s m a m forall a. Default a => a def (Result res, IntMap Bool litMap) <- Solver s m solver s problem forall (m :: * -> *) a. Monad m => a -> m a return (Result res, forall a. Codec a => Solution -> a -> Maybe (Decoded a) decode (forall s. HasSAT s => IntMap Bool -> s -> Solution solutionFrom IntMap Bool litMap s problem) a a)