{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
--------------------------------------------------------------------
-- |
-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Ersatz.Solution
  ( Solution(..), solutionFrom
  , Result(..)
  , Solver
  ) where

#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
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 Data.Typeable
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
  } deriving Typeable

solutionFrom :: HasSAT s => IntMap Bool -> s -> Solution
solutionFrom :: 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0    = Int -> IntMap Bool -> Maybe Bool
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Bool
litMap
                | Bool
otherwise = Bool -> Bool
not (Bool -> Bool) -> Maybe Bool -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> IntMap Bool -> Maybe Bool
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 (Literal -> Maybe Bool) -> Maybe Literal -> Maybe Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< StableName () -> HashMap (StableName ()) Literal -> Maybe Literal
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
qbfs
-> Getting
     (HashMap (StableName ()) Literal)
     s
     (HashMap (StableName ()) Literal)
-> HashMap (StableName ()) Literal
forall s a. s -> Getting a s a -> a
^.Getting
  (HashMap (StableName ()) Literal)
  s
  (HashMap (StableName ()) Literal)
forall s. HasSAT s => Lens' s (HashMap (StableName ()) Literal)
stableMap

data Result
  = Unsolved
  | Unsatisfied
  | Satisfied
  deriving (Result -> Result -> Bool
(Result -> Result -> Bool)
-> (Result -> Result -> Bool) -> Eq Result
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
Eq Result
-> (Result -> Result -> Ordering)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Result)
-> (Result -> Result -> Result)
-> Ord 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
$cp1Ord :: Eq Result
Ord,Ord Result
Ord Result
-> ((Result, Result) -> [Result])
-> ((Result, Result) -> Result -> Int)
-> ((Result, Result) -> Result -> Int)
-> ((Result, Result) -> Result -> Bool)
-> ((Result, Result) -> Int)
-> ((Result, Result) -> Int)
-> Ix 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]
$cp1Ix :: Ord Result
Ix,Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
(Int -> Result -> ShowS)
-> (Result -> String) -> ([Result] -> ShowS) -> Show Result
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]
(Int -> ReadS Result)
-> ReadS [Result]
-> ReadPrec Result
-> ReadPrec [Result]
-> Read 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
_ = String -> Result
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

-- | A @'Solver' s m@ is responsible for invoking a solver and
-- returning a 'Result' and a map of determined results.
--
-- * @s@ is typically 'SAT' or 'QSAT'
--
-- * @m@ is typically 'IO'
type Solver s m = s -> m (Result, IntMap Bool)