Logic.hs

module Rec where

import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.List (nub)

data Logic = Logic :& Logic
           | Logic :| Logic
           | Not Logic
           | Logic :=> Logic
           | Var Int
           deriving (Eq, Ord, Show, Read)

evaluate :: Map Int Bool -> Logic -> Bool
evaluate env (Var n)   = fromMaybe False $ Map.lookup n env
evaluate env (l :& r)  = evaluate env l && evaluate env r
evaluate env (l :| r)  = evaluate env l || evaluate env r
evaluate env (Not t)   = not $ evaluate env t
evaluate env (l :=> r) = not (evaluate env l) || evaluate env r

compatible :: Map Int Bool -> Map Int Bool -> Bool
compatible l r = all cond $ Map.keys l
    where cond n = fromMaybe True $ (==) <$> Map.lookup n l <*> Map.lookup n r

satisfy :: Logic -> [Map Int Bool]
satisfy (Var n)   = [Map.singleton n True]
satisfy (l :& r)  = [Map.union a b | a <- satisfy l, b <- satisfy r, compatible a b]
satisfy (l :| r)  = nub $ satisfy l ++ satisfy r
satisfy (Not t)   = map (Map.map not) $ satisfy t
satisfy (l :=> r) = satisfy (Not l :| r)