Solution.hs

--------------------------------------------------------------------
-- |
-- 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

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
  { solutionLiteral    :: Literal -> Maybe Bool
    -- ^ If a 'Literal' is uniquely assigned to a particular value, this will
    -- return 'Just' of that value. If a 'Literal' is unconstrained (i.e., it
    -- can be assigned either 'True' or 'False'), this will return 'Nothing'.
  , solutionStableName :: StableName () -> Maybe Bool
  }

solutionFrom :: HasSAT s => IntMap Bool -> s -> Solution
solutionFrom litMap qbf = Solution lookupLit lookupSN
  where
    lookupLit l | i >= 0    = IntMap.lookup i litMap
                | otherwise = not <$> IntMap.lookup (-i) litMap
      where i = literalId l

    lookupSN sn = lookupLit =<< HashMap.lookup sn snMap

    snMap = qbf^.stableMap

data Result
  = Unsolved
  | Unsatisfied
  | Satisfied
  deriving (Eq,Ord,Ix,Show,Read)

instance Enum Result where
  fromEnum Unsolved = -1
  fromEnum Unsatisfied = 0
  fromEnum Satisfied = 1

  toEnum (-1) = Unsolved
  toEnum 0 = Unsatisfied
  toEnum 1 = Satisfied
  toEnum _ = error "Enum.toEnum {Ersatz.Solution.Result}: argument of out range"

instance Bounded Result where
  minBound = Unsolved
  maxBound = 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)