{-# language FlexibleContexts #-}
{-# LANGUAGE TupleSections #-}

module OBDD.Cube where

import Prelude hiding ((&&),(||),not,and,or)
import qualified Prelude
import OBDD

import qualified Data.Bool 
import Control.Monad (guard)
import Control.Applicative

import qualified Data.Map.Strict as M
import qualified Data.Set as S
import Data.List (partition, sortOn)

import Debug.Trace

type Cube v = M.Map v Bool

primes :: Ord v => OBDD v -> [Cube v]
primes :: OBDD v -> [Cube v]
primes OBDD v
d =
  let process :: Map (k, Check) a -> Map k a
process Map (k, Check) a
m = [(k, a)] -> Map k a
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(k, a)] -> Map k a) -> [(k, a)] -> Map k a
forall a b. (a -> b) -> a -> b
$ do
        ((k
v,Check
Sign), a
b) <- Map (k, Check) a -> [((k, Check), a)]
forall k a. Map k a -> [(k, a)]
M.toList Map (k, Check) a
m
        (k, a) -> [(k, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return (k
v, a
b)
  in (Map (v, Check) Bool -> Cube v)
-> [Map (v, Check) Bool] -> [Cube v]
forall a b. (a -> b) -> [a] -> [b]
map Map (v, Check) Bool -> Cube v
forall k a. Ord k => Map (k, Check) a -> Map k a
process ([Map (v, Check) Bool] -> [Cube v])
-> [Map (v, Check) Bool] -> [Cube v]
forall a b. (a -> b) -> a -> b
$ OBDD (v, Check) -> [Map (v, Check) Bool]
forall v. Ord v => OBDD v -> [Map v Bool]
paths (OBDD (v, Check) -> [Map (v, Check) Bool])
-> OBDD (v, Check) -> [Map (v, Check) Bool]
forall a b. (a -> b) -> a -> b
$ OBDD v -> OBDD (v, Check)
forall v. Ord v => OBDD v -> OBDD (v, Check)
prime OBDD v
d

nice :: Show v => Cube v -> String
nice :: Cube v -> String
nice Cube v
c = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ do
    (v
v,Bool
b) <- Cube v -> [(v, Bool)]
forall k a. Map k a -> [(k, a)]
M.toList Cube v
c
    (if Bool
b then String
" " else String
" -") String -> String -> String
forall a. [a] -> [a] -> [a]
++ v -> String
forall a. Show a => a -> String
show v
v
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

data Check = Sign | Occurs | Original
           deriving (Check -> Check -> Bool
(Check -> Check -> Bool) -> (Check -> Check -> Bool) -> Eq Check
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Check -> Check -> Bool
$c/= :: Check -> Check -> Bool
== :: Check -> Check -> Bool
$c== :: Check -> Check -> Bool
Eq, Eq Check
Eq Check
-> (Check -> Check -> Ordering)
-> (Check -> Check -> Bool)
-> (Check -> Check -> Bool)
-> (Check -> Check -> Bool)
-> (Check -> Check -> Bool)
-> (Check -> Check -> Check)
-> (Check -> Check -> Check)
-> Ord Check
Check -> Check -> Bool
Check -> Check -> Ordering
Check -> Check -> Check
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 :: Check -> Check -> Check
$cmin :: Check -> Check -> Check
max :: Check -> Check -> Check
$cmax :: Check -> Check -> Check
>= :: Check -> Check -> Bool
$c>= :: Check -> Check -> Bool
> :: Check -> Check -> Bool
$c> :: Check -> Check -> Bool
<= :: Check -> Check -> Bool
$c<= :: Check -> Check -> Bool
< :: Check -> Check -> Bool
$c< :: Check -> Check -> Bool
compare :: Check -> Check -> Ordering
$ccompare :: Check -> Check -> Ordering
$cp1Ord :: Eq Check
Ord, Int -> Check -> String -> String
[Check] -> String -> String
Check -> String
(Int -> Check -> String -> String)
-> (Check -> String) -> ([Check] -> String -> String) -> Show Check
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Check] -> String -> String
$cshowList :: [Check] -> String -> String
show :: Check -> String
$cshow :: Check -> String
showsPrec :: Int -> Check -> String -> String
$cshowsPrec :: Int -> Check -> String -> String
Show)

sign :: a -> OBDD (a, Check)
sign a
v = (a, Check) -> OBDD (a, Check)
forall v. Ord v => v -> OBDD v
variable (a
v, Check
Sign)
occurs :: a -> OBDD (a, Check)
occurs a
v = (a, Check) -> OBDD (a, Check)
forall v. Ord v => v -> OBDD v
variable (a
v, Check
Occurs)
original :: a -> OBDD (a, Check)
original a
v = (a, Check) -> OBDD (a, Check)
forall v. Ord v => v -> OBDD v
variable (a
v, Check
Original)

process :: Map (k, Check) Bool -> Map k Bool
process Map (k, Check) Bool
c = [(k, Bool)] -> Map k Bool
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(k, Bool)] -> Map k Bool) -> [(k, Bool)] -> Map k Bool
forall a b. (a -> b) -> a -> b
$ do
        ((k
v,Check
Occurs),Bool
True) <- Map (k, Check) Bool -> [((k, Check), Bool)]
forall k a. Map k a -> [(k, a)]
M.toList Map (k, Check) Bool
c
        (k, Bool) -> [(k, Bool)]
forall (m :: * -> *) a. Monad m => a -> m a
return (k
v, Map (k, Check) Bool
c Map (k, Check) Bool -> (k, Check) -> Bool
forall k a. Ord k => Map k a -> k -> a
M.! (k
v,Check
Sign))


-- | O. Coudert , J. C. Madre:
-- http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.3330

prime :: Ord v => OBDD v -> OBDD (v, Check)
prime :: OBDD v -> OBDD (v, Check)
prime = (OBDD v, OBDD (v, Check)) -> OBDD (v, Check)
forall a b. (a, b) -> b
snd
  ((OBDD v, OBDD (v, Check)) -> OBDD (v, Check))
-> (OBDD v -> (OBDD v, OBDD (v, Check)))
-> OBDD v
-> OBDD (v, Check)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> (OBDD v, OBDD (v, Check)))
-> (v
    -> (OBDD v, OBDD (v, Check))
    -> (OBDD v, OBDD (v, Check))
    -> (OBDD v, OBDD (v, Check)))
-> OBDD v
-> (OBDD v, OBDD (v, Check))
forall v a.
Ord v =>
(Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a
fold ( \ Bool
b -> ( Bool -> OBDD v
forall b. Boolean b => Bool -> b
bool Bool
b, Bool -> OBDD (v, Check)
forall b. Boolean b => Bool -> b
bool Bool
b ))
         ( \ v
v (OBDD v
fl,OBDD (v, Check)
pl) (OBDD v
fr,OBDD (v, Check)
pr) -> ( OBDD v -> OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b -> b
choose OBDD v
fl OBDD v
fr (v -> OBDD v
forall v. Ord v => v -> OBDD v
variable v
v)
               , let common :: OBDD (v, Check)
common = OBDD v -> OBDD (v, Check)
forall v. Ord v => OBDD v -> OBDD (v, Check)
prime (OBDD v
fl OBDD v -> OBDD v -> OBDD v
forall b. Boolean b => b -> b -> b
&& OBDD v
fr)
                 in      OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b
not (v -> OBDD (v, Check)
forall a. Ord a => a -> OBDD (a, Check)
occurs v
v) OBDD (v, Check) -> OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b -> b
&& OBDD (v, Check)
common
                     OBDD (v, Check) -> OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b -> b
|| v -> OBDD (v, Check)
forall a. Ord a => a -> OBDD (a, Check)
occurs v
v OBDD (v, Check) -> OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b -> b
&& OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b
not (v -> OBDD (v, Check)
forall a. Ord a => a -> OBDD (a, Check)
sign v
v) OBDD (v, Check) -> OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b -> b
&& OBDD (v, Check)
pl OBDD (v, Check) -> OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b -> b
&& OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b
not OBDD (v, Check)
common
                     OBDD (v, Check) -> OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b -> b
|| v -> OBDD (v, Check)
forall a. Ord a => a -> OBDD (a, Check)
occurs v
v OBDD (v, Check) -> OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b -> b
&&     (v -> OBDD (v, Check)
forall a. Ord a => a -> OBDD (a, Check)
sign v
v) OBDD (v, Check) -> OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b -> b
&& OBDD (v, Check)
pr OBDD (v, Check) -> OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b -> b
&& OBDD (v, Check) -> OBDD (v, Check)
forall b. Boolean b => b -> b
not OBDD (v, Check)
common
               )
         )


-- * naive way of finding a minimal set of clauses.

dnf :: OBDD v -> [Cube v]
dnf OBDD v
f =
  let ps :: [Cube v]
ps = OBDD v -> [Cube v]
forall v. Ord v => OBDD v -> [Map v Bool]
primes OBDD v
f
      ms :: [Cube v]
ms = Set v -> OBDD v -> [Cube v]
forall k. Ord k => Set k -> OBDD k -> [Map k Bool]
models (OBDD v -> Set v
forall v. Ord v => OBDD v -> Set v
variables OBDD v
f) OBDD v
f
      covering :: [Set Int]
covering = do
        Cube v
m <- [Cube v]
ms
        Set Int -> [Set Int]
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Int -> [Set Int]) -> Set Int -> [Set Int]
forall a b. (a -> b) -> a -> b
$ [Int] -> Set Int
forall a. Ord a => [a] -> Set a
S.fromList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$ do
                   (Int
i,Cube v
p) <- [Int] -> [Cube v] -> [(Int, Cube v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Cube v]
ps
                   Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Cube v -> Cube v -> Bool
forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
M.isSubmapOf Cube v
p Cube v
m
                   Int -> [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
      cost :: Map Int Int
cost = [(Int, Int)] -> Map Int Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Int, Int)] -> Map Int Int) -> [(Int, Int)] -> Map Int Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([Int] -> [(Int, Int)]) -> [Int] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ (Cube v -> Int) -> [Cube v] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Cube v -> Int
forall k a. Map k a -> Int
M.size [Cube v]
ps
      r :: Set Int
r = Map Int Int -> [Set Int] -> Set Int
forall a b. (Ord b, Ord a) => Map a b -> [Set a] -> Set a
greed Map Int Int
cost [Set Int]
covering
  in  (Int -> Cube v) -> [Int] -> [Cube v]
forall a b. (a -> b) -> [a] -> [b]
map ([Cube v]
ps [Cube v] -> Int -> Cube v
forall a. [a] -> Int -> a
!!) ([Int] -> [Cube v]) -> [Int] -> [Cube v]
forall a b. (a -> b) -> a -> b
$ Set Int -> [Int]
forall a. Set a -> [a]
S.toList Set Int
r


cnf :: OBDD k -> [Map k Bool]
cnf OBDD k
f = (Map k Bool -> Map k Bool) -> [Map k Bool] -> [Map k Bool]
forall a b. (a -> b) -> [a] -> [b]
map ((Bool -> Bool) -> Map k Bool -> Map k Bool
forall a b k. (a -> b) -> Map k a -> Map k b
M.map Bool -> Bool
Prelude.not) ([Map k Bool] -> [Map k Bool]) -> [Map k Bool] -> [Map k Bool]
forall a b. (a -> b) -> a -> b
$ OBDD k -> [Map k Bool]
forall v. Ord v => OBDD v -> [Map v Bool]
dnf (OBDD k -> [Map k Bool]) -> OBDD k -> [Map k Bool]
forall a b. (a -> b) -> a -> b
$ OBDD k -> OBDD k
forall b. Boolean b => b -> b
not OBDD k
f

greed :: Map a b -> [Set a] -> Set a
greed Map a b
cost [] = Set a
forall a. Set a
S.empty
greed Map a b
cost [Set a]
could =
  let count :: Map a Integer
count = (Integer -> Integer -> Integer) -> [Map a Integer] -> Map a Integer
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) ([Map a Integer] -> Map a Integer)
-> [Map a Integer] -> Map a Integer
forall a b. (a -> b) -> a -> b
$ do
        Set a
c <- [Set a]
could
        Map a Integer -> [Map a Integer]
forall (m :: * -> *) a. Monad m => a -> m a
return (Map a Integer -> [Map a Integer])
-> Map a Integer -> [Map a Integer]
forall a b. (a -> b) -> a -> b
$ [(a, Integer)] -> Map a Integer
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(a, Integer)] -> Map a Integer)
-> [(a, Integer)] -> Map a Integer
forall a b. (a -> b) -> a -> b
$ [a] -> [Integer] -> [(a, Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Set a -> [a]
forall a. Set a -> [a]
S.toList Set a
c) ([Integer] -> [(a, Integer)]) -> [Integer] -> [(a, Integer)]
forall a b. (a -> b) -> a -> b
$ Integer -> [Integer]
forall a. a -> [a]
repeat Integer
1
      this :: a
this = (a, (Integer, b)) -> a
forall a b. (a, b) -> a
fst
           ((a, (Integer, b)) -> a) -> (a, (Integer, b)) -> a
forall a b. (a -> b) -> a -> b
$ [(a, (Integer, b))] -> (a, (Integer, b))
forall a. [a] -> a
head
           ([(a, (Integer, b))] -> (a, (Integer, b)))
-> [(a, (Integer, b))] -> (a, (Integer, b))
forall a b. (a -> b) -> a -> b
$ ((a, (Integer, b)) -> (Integer, b))
-> [(a, (Integer, b))] -> [(a, (Integer, b))]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (a, (Integer, b)) -> (Integer, b)
forall a b. (a, b) -> b
snd
           ([(a, (Integer, b))] -> [(a, (Integer, b))])
-> [(a, (Integer, b))] -> [(a, (Integer, b))]
forall a b. (a -> b) -> a -> b
$ ((a, Integer) -> (a, (Integer, b)))
-> [(a, Integer)] -> [(a, (Integer, b))]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
k,Integer
v) -> (a
k, (Integer -> Integer
forall a. Num a => a -> a
negate Integer
v, Map a b
cost Map a b -> a -> b
forall k a. Ord k => Map k a -> k -> a
M.! a
k)))
           ([(a, Integer)] -> [(a, (Integer, b))])
-> [(a, Integer)] -> [(a, (Integer, b))]
forall a b. (a -> b) -> a -> b
$ Map a Integer -> [(a, Integer)]
forall k a. Map k a -> [(k, a)]
M.toList Map a Integer
count 
  in    a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
S.insert a
this
      (Set a -> Set a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
$ Map a b -> [Set a] -> Set a
greed Map a b
cost ([Set a] -> Set a) -> [Set a] -> Set a
forall a b. (a -> b) -> a -> b
$ (Set a -> Bool) -> [Set a] -> [Set a]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \Set a
p -> a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
S.notMember a
this Set a
p ) [Set a]
could

clause :: Map v Bool -> OBDD v
clause Map v Bool
c = [OBDD v] -> OBDD v
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and ([OBDD v] -> OBDD v) -> [OBDD v] -> OBDD v
forall a b. (a -> b) -> a -> b
$ do (v
v,Bool
b) <- Map v Bool -> [(v, Bool)]
forall k a. Map k a -> [(k, a)]
M.toList Map v Bool
c ; OBDD v -> [OBDD v]
forall (m :: * -> *) a. Monad m => a -> m a
return (OBDD v -> [OBDD v]) -> OBDD v -> [OBDD v]
forall a b. (a -> b) -> a -> b
$ v -> Bool -> OBDD v
forall v. Ord v => v -> Bool -> OBDD v
unit v
v Bool
b