Copyright | © Edward Kmett 2010-2014 Johan Kiviniemi 2013 |
---|---|
License | BSD3 |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- module Ersatz.Solver.DepQBF
- module Ersatz.Solver.Minisat
- module Ersatz.Solver.Z3
- solveWith :: (Monad m, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
Documentation
module Ersatz.Solver.DepQBF
module Ersatz.Solver.Minisat
module Ersatz.Solver.Z3
solveWith :: (Monad m, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a)) Source #
solves a SAT problem solveWith
solver probprob
with the given
solver
. It returns a pair consisting of:
- A
Result
that indicates ifprob
is satisfiable (Satisfied
), unsatisfiable (Unsatisfied
), or if the solver could not determine any results (Unsolved
). - A
Decoded
answer that was decoded using the solution toprob
. Note that this answer is only meaningful if theResult
isSatisfied
and the answer value is in aJust
.
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]
.