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