|  | import Data.Map (Map) | 
        
          |  | import qualified Data.Map as Map | 
        
          |  |  | 
        
          |  | import Data.Set (Set) | 
        
          |  | import qualified Data.Set as Set | 
        
          |  | import Data.List (minimumBy) | 
        
          |  |  | 
        
          |  | type Var = String | 
        
          |  | type Values = Set Int | 
        
          |  |  | 
        
          |  | data Ast = | 
        
          |  | In Var Values | 
        
          |  | | And Ast Ast | 
        
          |  | | Not Ast | 
        
          |  | | Lit Bool | 
        
          |  | deriving (Show, Eq) | 
        
          |  |  | 
        
          |  | data Constraint = | 
        
          |  | Prohibited Values | 
        
          |  | | Permitted Values | 
        
          |  | deriving (Show) | 
        
          |  |  | 
        
          |  | type Env = Map Var Constraint | 
        
          |  |  | 
        
          |  | empty = Map.empty | 
        
          |  |  | 
        
          |  | combineConstraints :: Constraint -> Constraint -> Constraint | 
        
          |  | combineConstraints (Prohibited a) (Prohibited b) = Prohibited $ Set.union a b | 
        
          |  | combineConstraints (Permitted a)  (Permitted b)  = Permitted  $ Set.intersection a b | 
        
          |  | combineConstraints (Permitted a)  (Prohibited b) = Permitted  $ Set.difference a b | 
        
          |  | combineConstraints (Prohibited a) (Permitted b)  = Permitted  $ Set.difference b a | 
        
          |  |  | 
        
          |  | permit :: String -> Values -> Env | 
        
          |  | permit k set = Map.singleton k rule | 
        
          |  | where rule = Permitted set | 
        
          |  |  | 
        
          |  | prohibit k set = Map.singleton k rule | 
        
          |  | where rule = Prohibited set | 
        
          |  |  | 
        
          |  | invert' :: Constraint -> Constraint | 
        
          |  | invert' (Permitted a)  = Prohibited a | 
        
          |  | invert' (Prohibited a) = Permitted a | 
        
          |  |  | 
        
          |  | invert :: Env -> Env | 
        
          |  | invert = fmap invert' | 
        
          |  |  | 
        
          |  | merge :: Env -> Env -> Env | 
        
          |  | merge = Map.unionWith combineConstraints | 
        
          |  |  | 
        
          |  | extract :: Env -> Ast -> Env | 
        
          |  | extract env (Lit _)          = env | 
        
          |  | extract env (Not x)          = invert $ extract env x | 
        
          |  | extract env (In var set)     = merge env $ permit var set | 
        
          |  | extract env (And left right) = let l = extract env left | 
        
          |  | r = extract env right | 
        
          |  | in merge l r | 
        
          |  |  | 
        
          |  | test' :: Maybe Constraint -> Values -> Maybe Bool | 
        
          |  | test' (Just (Prohibited a)) b = | 
        
          |  | if Set.isSubsetOf b a then Just False | 
        
          |  | else Nothing | 
        
          |  |  | 
        
          |  | test' (Just (Permitted a)) b = | 
        
          |  | if Set.isSubsetOf b a then Nothing | 
        
          |  | else Just False | 
        
          |  |  | 
        
          |  | test' con vals = Nothing | 
        
          |  |  | 
        
          |  | test :: Env -> Var -> Values -> Maybe Bool | 
        
          |  | test env var values = test' con values | 
        
          |  | where con = Map.lookup var env | 
        
          |  |  | 
        
          |  | minimize :: Env -> Ast -> [Ast] | 
        
          |  | minimize env (Lit t)         = [Lit t] | 
        
          |  | minimize env (Not (Not ast)) = minimize env ast | 
        
          |  | minimize env (Not v)         = do | 
        
          |  | ast <- minimize env v | 
        
          |  | case ast of | 
        
          |  | (Lit v) -> return $ Lit (not v) | 
        
          |  | _       -> return $ Not ast | 
        
          |  |  | 
        
          |  | minimize env (In v s) = | 
        
          |  | case proof of | 
        
          |  | Just x  -> [Lit x] | 
        
          |  | Nothing -> [In v s] | 
        
          |  |  | 
        
          |  | where proof = test env v s | 
        
          |  |  | 
        
          |  | minimize env (And a b) = | 
        
          |  | minimizeAnd env a b ++ minimizeAnd env b a | 
        
          |  |  | 
        
          |  | minimizeAnd env a b = do | 
        
          |  | let env' = extract env a | 
        
          |  | left  <- minimize env a | 
        
          |  | right <- minimize env' b | 
        
          |  |  | 
        
          |  | return (minimizeAnd' left right) | 
        
          |  |  | 
        
          |  | minimizeAnd' (Lit True) right = right | 
        
          |  | minimizeAnd' left (Lit True)  = left | 
        
          |  | minimizeAnd' (Lit False) _    = Lit False | 
        
          |  | minimizeAnd' _ (Lit False)    = Lit False | 
        
          |  | minimizeAnd' left right       = And left right | 
        
          |  |  | 
        
          |  | depth (Lit _)   = 1 | 
        
          |  | depth (And l r) = 1 + depth l + depth r | 
        
          |  | depth (Not ast) = 1 + depth ast | 
        
          |  | depth (In _ _)  = 3 | 
        
          |  | deeper a b = depth a `compare` depth b | 
        
          |  | optimize ast = minimumBy deeper $ minimize empty ast |