module Ersatz.Solution
( Solution(..), solutionFrom
, Result(..)
, Solver
) where
import Control.Lens
import qualified Data.HashMap.Lazy as HashMap
import Data.IntMap (IntMap)
import qualified Data.IntMap.Strict as IntMap
import Data.Ix
import Ersatz.Internal.Literal
import Ersatz.Problem
import System.Mem.StableName (StableName)
data Solution = Solution
{ Solution -> Literal -> Maybe Bool
solutionLiteral :: Literal -> Maybe Bool
, Solution -> StableName () -> Maybe Bool
solutionStableName :: StableName () -> Maybe Bool
}
solutionFrom :: HasSAT s => IntMap Bool -> s -> Solution
solutionFrom :: forall s. HasSAT s => IntMap Bool -> s -> Solution
solutionFrom IntMap Bool
litMap s
qbf = (Literal -> Maybe Bool)
-> (StableName () -> Maybe Bool) -> Solution
Solution Literal -> Maybe Bool
lookupLit StableName () -> Maybe Bool
lookupSN
where
lookupLit :: Literal -> Maybe Bool
lookupLit Literal
l | Int
i forall a. Ord a => a -> a -> Bool
>= Int
0 = forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Bool
litMap
| Bool
otherwise = Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (-Int
i) IntMap Bool
litMap
where i :: Int
i = Literal -> Int
literalId Literal
l
lookupSN :: StableName () -> Maybe Bool
lookupSN StableName ()
sn = Literal -> Maybe Bool
lookupLit forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup StableName ()
sn HashMap (StableName ()) Literal
snMap
snMap :: HashMap (StableName ()) Literal
snMap = s
qbfforall s a. s -> Getting a s a -> a
^.forall s. HasSAT s => Lens' s (HashMap (StableName ()) Literal)
stableMap
data Result
= Unsolved
| Unsatisfied
| Satisfied
deriving (Result -> Result -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Result -> Result -> Bool
$c/= :: Result -> Result -> Bool
== :: Result -> Result -> Bool
$c== :: Result -> Result -> Bool
Eq,Eq Result
Result -> Result -> Bool
Result -> Result -> Ordering
Result -> Result -> Result
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Result -> Result -> Result
$cmin :: Result -> Result -> Result
max :: Result -> Result -> Result
$cmax :: Result -> Result -> Result
>= :: Result -> Result -> Bool
$c>= :: Result -> Result -> Bool
> :: Result -> Result -> Bool
$c> :: Result -> Result -> Bool
<= :: Result -> Result -> Bool
$c<= :: Result -> Result -> Bool
< :: Result -> Result -> Bool
$c< :: Result -> Result -> Bool
compare :: Result -> Result -> Ordering
$ccompare :: Result -> Result -> Ordering
Ord,Ord Result
(Result, Result) -> Int
(Result, Result) -> [Result]
(Result, Result) -> Result -> Bool
(Result, Result) -> Result -> Int
forall a.
Ord a
-> ((a, a) -> [a])
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Bool)
-> ((a, a) -> Int)
-> ((a, a) -> Int)
-> Ix a
unsafeRangeSize :: (Result, Result) -> Int
$cunsafeRangeSize :: (Result, Result) -> Int
rangeSize :: (Result, Result) -> Int
$crangeSize :: (Result, Result) -> Int
inRange :: (Result, Result) -> Result -> Bool
$cinRange :: (Result, Result) -> Result -> Bool
unsafeIndex :: (Result, Result) -> Result -> Int
$cunsafeIndex :: (Result, Result) -> Result -> Int
index :: (Result, Result) -> Result -> Int
$cindex :: (Result, Result) -> Result -> Int
range :: (Result, Result) -> [Result]
$crange :: (Result, Result) -> [Result]
Ix,Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Result] -> ShowS
$cshowList :: [Result] -> ShowS
show :: Result -> String
$cshow :: Result -> String
showsPrec :: Int -> Result -> ShowS
$cshowsPrec :: Int -> Result -> ShowS
Show,ReadPrec [Result]
ReadPrec Result
Int -> ReadS Result
ReadS [Result]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Result]
$creadListPrec :: ReadPrec [Result]
readPrec :: ReadPrec Result
$creadPrec :: ReadPrec Result
readList :: ReadS [Result]
$creadList :: ReadS [Result]
readsPrec :: Int -> ReadS Result
$creadsPrec :: Int -> ReadS Result
Read)
instance Enum Result where
fromEnum :: Result -> Int
fromEnum Result
Unsolved = -Int
1
fromEnum Result
Unsatisfied = Int
0
fromEnum Result
Satisfied = Int
1
toEnum :: Int -> Result
toEnum (-1) = Result
Unsolved
toEnum Int
0 = Result
Unsatisfied
toEnum Int
1 = Result
Satisfied
toEnum Int
_ = forall a. HasCallStack => String -> a
error String
"Enum.toEnum {Ersatz.Solution.Result}: argument of out range"
instance Bounded Result where
minBound :: Result
minBound = Result
Unsolved
maxBound :: Result
maxBound = Result
Satisfied
type Solver s m = s -> m (Result, IntMap Bool)