{-# OPTIONS_GHC -Wall #-}
module ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
(
areDualDNFs
, checkDuality
, checkDualityA
, checkDualityB
, isRedundant
, deleteRedundancy
, isCounterExampleOf
, occurFreq
, condition_1_1
, condition_1_2
, condition_1_3
, condition_2_1
, condition_1_1_solve
, condition_1_2_solve
, condition_1_3_solve
, condition_2_1_solve
) where
import Prelude hiding (all, any)
import Control.Arrow ((***))
import Control.Exception (assert)
import Control.Monad
import Data.Foldable (all, any)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.List hiding (all, any, intersect)
import Data.Maybe
import Data.Ratio
import Data.Set (Set)
import qualified Data.Set as Set
xhi :: Double -> Double
xhi :: Double -> Double
xhi Double
n = forall a. (a -> a) -> a -> [a]
iterate Double -> Double
f Double
m forall a. [a] -> Int -> a
!! Int
30
where
m :: Double
m = Double
logn forall a. Fractional a => a -> a -> a
/ forall a. Floating a => a -> a -> a
logBase Double
2 Double
logn
where
logn :: Double
logn = forall a. Floating a => a -> a -> a
logBase Double
2 Double
n
f :: Double -> Double
f Double
x = Double
m forall a. Num a => a -> a -> a
* ((Double
logx forall a. Num a => a -> a -> a
+ forall a. Floating a => a -> a -> a
logBase Double
2 Double
logx) forall a. Fractional a => a -> a -> a
/ Double
logx)
where
logx :: Double
logx = forall a. Floating a => a -> a -> a
logBase Double
2 Double
x
disjoint :: IntSet -> IntSet -> Bool
disjoint :: IntSet -> IntSet -> Bool
disjoint IntSet
xs IntSet
ys = IntSet -> Bool
IntSet.null forall a b. (a -> b) -> a -> b
$ IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.intersection` IntSet
ys
intersect :: IntSet -> IntSet -> Bool
intersect :: IntSet -> IntSet -> Bool
intersect IntSet
xs IntSet
ys = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ IntSet -> IntSet -> Bool
disjoint IntSet
xs IntSet
ys
isHittingSetOf :: IntSet -> Set IntSet -> Bool
isHittingSetOf :: IntSet -> Set IntSet -> Bool
isHittingSetOf IntSet
xs Set IntSet
yss = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (IntSet
xs IntSet -> IntSet -> Bool
`intersect`) Set IntSet
yss
isCounterExampleOf :: IntSet -> (Set IntSet, Set IntSet) -> Bool
isCounterExampleOf :: IntSet -> (Set IntSet, Set IntSet) -> Bool
isCounterExampleOf IntSet
xs (Set IntSet
f,Set IntSet
g) = Bool
lhs forall a. Eq a => a -> a -> Bool
== Bool
rhs
where
lhs :: Bool
lhs = forall (t :: * -> *). Foldable t => t Bool -> Bool
or [IntSet
is IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` IntSet
xs | IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
f]
rhs :: Bool
rhs = forall (t :: * -> *). Foldable t => t Bool -> Bool
or [IntSet
xs IntSet -> IntSet -> Bool
`disjoint` IntSet
js | IntSet
js <- forall a. Set a -> [a]
Set.toList Set IntSet
g]
_volume :: Set IntSet -> Set IntSet -> Int
_volume :: Set IntSet -> Set IntSet -> Int
_volume Set IntSet
f Set IntSet
g = forall a. Set a -> Int
Set.size Set IntSet
f forall a. Num a => a -> a -> a
* forall a. Set a -> Int
Set.size Set IntSet
g
condition_1_1 :: Set IntSet -> Set IntSet -> Bool
condition_1_1 :: Set IntSet -> Set IntSet -> Bool
condition_1_1 Set IntSet
f Set IntSet
g = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\IntSet
is -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\IntSet
js -> IntSet
is IntSet -> IntSet -> Bool
`intersect` IntSet
js) Set IntSet
g) Set IntSet
f
condition_1_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_1_solve Set IntSet
f Set IntSet
g = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ do
IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
f
IntSet
js <- forall a. Set a -> [a]
Set.toList Set IntSet
g
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ IntSet
is IntSet -> IntSet -> Bool
`disjoint` IntSet
js
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
is
condition_1_2 :: Set IntSet -> Set IntSet -> Bool
condition_1_2 :: Set IntSet -> Set IntSet -> Bool
condition_1_2 Set IntSet
f Set IntSet
g = Set IntSet -> IntSet
h Set IntSet
f forall a. Eq a => a -> a -> Bool
== Set IntSet -> IntSet
h Set IntSet
g
where
h :: Set IntSet -> IntSet
h = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList
condition_1_2_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_2_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_2_solve Set IntSet
f Set IntSet
g
| Just (Int
v1,IntSet
_) <- IntSet -> Maybe (Int, IntSet)
IntSet.minView IntSet
d1 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [Int -> IntSet -> IntSet
IntSet.delete Int
v1 IntSet
is | IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
f, Int
v1 Int -> IntSet -> Bool
`IntSet.member` IntSet
is]
| Just (Int
v2,IntSet
_) <- IntSet -> Maybe (Int, IntSet)
IntSet.minView IntSet
d2 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [(IntSet
vs IntSet -> IntSet -> IntSet
`IntSet.difference` (Int -> IntSet -> IntSet
IntSet.delete Int
v2 IntSet
js)) | IntSet
js <- forall a. Set a -> [a]
Set.toList Set IntSet
g, Int
v2 Int -> IntSet -> Bool
`IntSet.member` IntSet
js]
| Bool
otherwise = forall a. Maybe a
Nothing
where
f_vs :: IntSet
f_vs = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set IntSet
f
g_vs :: IntSet
g_vs = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set IntSet
g
vs :: IntSet
vs = IntSet
f_vs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
g_vs
d1 :: IntSet
d1 = IntSet
f_vs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
g_vs
d2 :: IntSet
d2 = IntSet
g_vs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
f_vs
condition_1_3 :: Set IntSet -> Set IntSet -> Bool
condition_1_3 :: Set IntSet -> Set IntSet -> Bool
condition_1_3 Set IntSet
f Set IntSet
g = Set IntSet -> Int
maxSize Set IntSet
f forall a. Ord a => a -> a -> Bool
<= forall a. Set a -> Int
Set.size Set IntSet
g Bool -> Bool -> Bool
&& Set IntSet -> Int
maxSize Set IntSet
g forall a. Ord a => a -> a -> Bool
<= forall a. Set a -> Int
Set.size Set IntSet
f
where
maxSize :: Set IntSet -> Int
maxSize Set IntSet
xs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Ord a => a -> a -> a
max Int
0 [IntSet -> Int
IntSet.size IntSet
i | IntSet
i <- forall a. Set a -> [a]
Set.toList Set IntSet
xs]
condition_1_3_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_3_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_3_solve Set IntSet
f Set IntSet
g = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$
[forall a. [a] -> a
head [IntSet
is' | Int
i <- IntSet -> [Int]
IntSet.toList IntSet
is, let is' :: IntSet
is' = Int -> IntSet -> IntSet
IntSet.delete Int
i IntSet
is, IntSet
is' IntSet -> Set IntSet -> Bool
`isHittingSetOf` Set IntSet
g] | IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
f, IntSet -> Int
IntSet.size IntSet
is forall a. Ord a => a -> a -> Bool
> Int
g_size] forall a. [a] -> [a] -> [a]
++
[IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` forall a. [a] -> a
head [IntSet
js' | Int
j <- IntSet -> [Int]
IntSet.toList IntSet
js, let js' :: IntSet
js' = Int -> IntSet -> IntSet
IntSet.delete Int
j IntSet
js, IntSet
js' IntSet -> Set IntSet -> Bool
`isHittingSetOf` Set IntSet
f] | IntSet
js <- forall a. Set a -> [a]
Set.toList Set IntSet
g, IntSet -> Int
IntSet.size IntSet
js forall a. Ord a => a -> a -> Bool
> Int
f_size]
where
xs :: IntSet
xs = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.union Set IntSet
f Set IntSet
g
f_size :: Int
f_size = forall a. Set a -> Int
Set.size Set IntSet
f
g_size :: Int
g_size = forall a. Set a -> Int
Set.size Set IntSet
g
e :: Set IntSet -> Set IntSet -> Rational
e :: Set IntSet -> Set IntSet -> Rational
e Set IntSet
f Set IntSet
g = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
1 forall a. Integral a => a -> a -> Ratio a
% (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ IntSet -> Int
IntSet.size IntSet
i) | IntSet
i <- forall a. Set a -> [a]
Set.toList Set IntSet
f] forall a. Num a => a -> a -> a
+
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
1 forall a. Integral a => a -> a -> Ratio a
% (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ IntSet -> Int
IntSet.size IntSet
j) | IntSet
j <- forall a. Set a -> [a]
Set.toList Set IntSet
g]
condition_2_1 :: Set IntSet -> Set IntSet -> Bool
condition_2_1 :: Set IntSet -> Set IntSet -> Bool
condition_2_1 Set IntSet
f Set IntSet
g = Set IntSet -> Set IntSet -> Rational
e Set IntSet
f Set IntSet
g forall a. Ord a => a -> a -> Bool
>= Rational
1
condition_2_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_2_1_solve :: Set IntSet -> Set IntSet -> Maybe IntSet
condition_2_1_solve Set IntSet
f Set IntSet
g =
if Set IntSet -> Set IntSet -> Bool
condition_2_1 Set IntSet
f Set IntSet
g
then forall a. Maybe a
Nothing
else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Int] -> Set IntSet -> Set IntSet -> IntSet -> IntSet
loop (IntSet -> [Int]
IntSet.toList IntSet
vs) Set IntSet
f Set IntSet
g IntSet
IntSet.empty
where
vs :: IntSet
vs = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.union Set IntSet
f Set IntSet
g
loop :: [Int] -> Set IntSet -> Set IntSet -> IntSet -> IntSet
loop :: [Int] -> Set IntSet -> Set IntSet -> IntSet -> IntSet
loop [] Set IntSet
_ Set IntSet
_ IntSet
ret = IntSet
ret
loop (Int
v:[Int]
vs) Set IntSet
f Set IntSet
g IntSet
ret =
if Set IntSet -> Set IntSet -> Rational
e Set IntSet
f1 Set IntSet
g1 forall a. Ord a => a -> a -> Bool
<= Set IntSet -> Set IntSet -> Rational
e Set IntSet
f2 Set IntSet
g2
then [Int] -> Set IntSet -> Set IntSet -> IntSet -> IntSet
loop [Int]
vs Set IntSet
f1 Set IntSet
g1 (Int -> IntSet -> IntSet
IntSet.insert Int
v IntSet
ret)
else [Int] -> Set IntSet -> Set IntSet -> IntSet -> IntSet
loop [Int]
vs Set IntSet
f2 Set IntSet
g2 IntSet
ret
where
f1 :: Set IntSet
f1 = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
v) Set IntSet
f
g1 :: Set IntSet
g1 = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Int
v Int -> IntSet -> Bool
`IntSet.notMember`) Set IntSet
g
f2 :: Set IntSet
f2 = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Int
v Int -> IntSet -> Bool
`IntSet.notMember`) Set IntSet
f
g2 :: Set IntSet
g2 = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
v) Set IntSet
g
isRedundant :: Set IntSet -> Bool
isRedundant :: Set IntSet -> Bool
isRedundant = [IntSet] -> Bool
loop forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn IntSet -> Int
IntSet.size forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList
where
loop :: [IntSet] -> Bool
loop :: [IntSet] -> Bool
loop [] = Bool
False
loop (IntSet
xs:[IntSet]
yss) = forall (t :: * -> *). Foldable t => t Bool -> Bool
or [IntSet
xs IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` IntSet
ys | IntSet
ys <- [IntSet]
yss] Bool -> Bool -> Bool
|| [IntSet] -> Bool
loop [IntSet]
yss
isIrredundant :: Set IntSet -> Bool
isIrredundant :: Set IntSet -> Bool
isIrredundant = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set IntSet -> Bool
isRedundant
deleteRedundancy :: Set IntSet -> Set IntSet
deleteRedundancy :: Set IntSet -> Set IntSet
deleteRedundancy = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Set IntSet -> IntSet -> Set IntSet
f forall a. Set a
Set.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn IntSet -> Int
IntSet.size forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList
where
f :: Set IntSet -> IntSet -> Set IntSet
f :: Set IntSet -> IntSet -> Set IntSet
f Set IntSet
xss IntSet
ys =
if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` IntSet
ys) Set IntSet
xss
then Set IntSet
xss
else forall a. Ord a => a -> Set a -> Set a
Set.insert IntSet
ys Set IntSet
xss
occurFreq
:: Fractional a
=> Int
-> Set IntSet
-> a
occurFreq :: forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
f = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int
1 | IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
f, Int
x Int -> IntSet -> Bool
`IntSet.member` IntSet
is] :: Int) forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Set a -> Int
Set.size Set IntSet
f)
areDualDNFs
:: Set IntSet
-> Set IntSet
-> Bool
areDualDNFs :: Set IntSet -> Set IntSet -> Bool
areDualDNFs Set IntSet
f Set IntSet
g = forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB Set IntSet
f Set IntSet
g
checkDuality :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDuality :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDuality = Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB
checkDualityA
:: Set IntSet
-> Set IntSet
-> Maybe IntSet
checkDualityA :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA Set IntSet
f Set IntSet
g
| Just IntSet
xs <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_1_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
xs
| Bool
otherwise = Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
f) (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
g)
checkDualityA' :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' Set IntSet
f Set IntSet
g
| forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Set IntSet -> Bool
isIrredundant Set IntSet
f Bool -> Bool -> Bool
&& Set IntSet -> Bool
isIrredundant Set IntSet
g) Bool
False = forall a. (?callStack::CallStack) => a
undefined
| Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_2_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
| Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_3_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
| Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_2_1_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
| Int
v forall a. Ord a => a -> a -> Bool
<= Int
1 = Set IntSet -> Set IntSet -> Maybe IntSet
solveSmall Set IntSet
f Set IntSet
g
| Bool
otherwise = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[
Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' Set IntSet
f1 (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
g0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g1))
,
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> IntSet -> IntSet
IntSet.insert Int
x) forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
f0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
f1)) Set IntSet
g1
]
where
size_f :: Int
size_f = forall a. Set a -> Int
Set.size Set IntSet
f
size_g :: Int
size_g = forall a. Set a -> Int
Set.size Set IntSet
g
n :: Int
n = Int
size_f forall a. Num a => a -> a -> a
+ Int
size_g
v :: Int
v = Int
size_f forall a. Num a => a -> a -> a
* Int
size_g
xs :: IntSet
xs = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set IntSet
f forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g
epsilon :: Double
epsilon :: Double
epsilon = Double
1 forall a. Fractional a => a -> a -> a
/ forall a. Floating a => a -> a -> a
logBase Double
2 (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n)
x :: Int
x = forall a. [a] -> a
head [Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs, forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
f forall a. Ord a => a -> a -> Bool
>= Double
epsilon Bool -> Bool -> Bool
|| forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
g forall a. Ord a => a -> a -> Bool
>= Double
epsilon]
(Set IntSet
f0, Set IntSet
f1) = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Int
x Int -> IntSet -> Bool
`IntSet.member`) Set IntSet
f
(Set IntSet
g0, Set IntSet
g1) = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Int
x Int -> IntSet -> Bool
`IntSet.member`) Set IntSet
g
solveSmall :: Set IntSet -> Set IntSet -> Maybe IntSet
solveSmall :: Set IntSet -> Set IntSet -> Maybe IntSet
solveSmall Set IntSet
f Set IntSet
g
| forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Set IntSet -> Bool
isIrredundant Set IntSet
f Bool -> Bool -> Bool
&& Set IntSet -> Bool
isIrredundant Set IntSet
g) Bool
False = forall a. (?callStack::CallStack) => a
undefined
| forall a. Set a -> Bool
Set.null Set IntSet
f Bool -> Bool -> Bool
&& forall a. Set a -> Bool
Set.null Set IntSet
g = forall a. a -> Maybe a
Just IntSet
IntSet.empty
| forall a. Set a -> Bool
Set.null Set IntSet
f = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bool -> Bool
not (forall a. Set a -> Bool
Set.null Set IntSet
g)) forall a b. (a -> b) -> a -> b
$
if IntSet
IntSet.empty forall a. Ord a => a -> Set a -> Bool
`Set.member` Set IntSet
g
then forall a. Maybe a
Nothing
else forall a. a -> Maybe a
Just (forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions (forall a. Set a -> [a]
Set.toList Set IntSet
g))
| forall a. Set a -> Bool
Set.null Set IntSet
g = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bool -> Bool
not (forall a. Set a -> Bool
Set.null Set IntSet
f)) forall a b. (a -> b) -> a -> b
$
if IntSet
IntSet.empty forall a. Ord a => a -> Set a -> Bool
`Set.member` Set IntSet
f
then forall a. Maybe a
Nothing
else forall a. a -> Maybe a
Just IntSet
IntSet.empty
| Int
size_f forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Int
size_g forall a. Eq a => a -> a -> Bool
== Int
1 =
let
is :: IntSet
is = forall a. Set a -> a
Set.findMin Set IntSet
f
js :: IntSet
js = forall a. Set a -> a
Set.findMin Set IntSet
g
is_size :: Int
is_size = IntSet -> Int
IntSet.size IntSet
is
js_size :: Int
js_size = IntSet -> Int
IntSet.size IntSet
js
in if Int
is_size forall a. Eq a => a -> a -> Bool
== Int
1 then
if Int
js_size forall a. Eq a => a -> a -> Bool
== Int
1 then
forall a. Maybe a
Nothing
else
forall a. a -> Maybe a
Just (IntSet
js IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
is)
else
forall a. a -> Maybe a
Just (IntSet
is IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
js)
| Bool
otherwise = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"should not happen"
where
size_f :: Int
size_f = forall a. Set a -> Int
Set.size Set IntSet
f
size_g :: Int
size_g = forall a. Set a -> Int
Set.size Set IntSet
g
checkDualityB
:: Set IntSet
-> Set IntSet
-> Maybe IntSet
checkDualityB :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB Set IntSet
f Set IntSet
g
| Just IntSet
xs <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_1_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
xs
| Bool
otherwise = Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
f) (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
g)
checkDualityB' :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' Set IntSet
f Set IntSet
g
| forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Set IntSet -> Bool
isIrredundant Set IntSet
f Bool -> Bool -> Bool
&& Set IntSet -> Bool
isIrredundant Set IntSet
g) Bool
False = forall a. (?callStack::CallStack) => a
undefined
| Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_2_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
| Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_1_3_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
| Just IntSet
s <- Set IntSet -> Set IntSet -> Maybe IntSet
condition_2_1_solve Set IntSet
f Set IntSet
g = forall a. a -> Maybe a
Just IntSet
s
| Int
v forall a. Ord a => a -> a -> Bool
<= Int
1 = Set IntSet -> Set IntSet -> Maybe IntSet
solveSmall Set IntSet
f Set IntSet
g
| Bool
otherwise =
let x :: Int
x = forall a. [a] -> a
head [Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs, forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
f forall a. Ord a => a -> a -> Bool
> (Rational
0::Rational), forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
g forall a. Ord a => a -> a -> Bool
> (Rational
0::Rational)]
(Set IntSet
f0, Set IntSet
f1) = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Int
x Int -> IntSet -> Bool
`IntSet.member`) Set IntSet
f
(Set IntSet
g0, Set IntSet
g1) = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Int
x Int -> IntSet -> Bool
`IntSet.member`) Set IntSet
g
epsilon_x_f :: Double
epsilon_x_f :: Double
epsilon_x_f = forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
f
epsilon_x_g :: Double
epsilon_x_g :: Double
epsilon_x_g = forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
g
in if Double
epsilon_x_f forall a. Ord a => a -> a -> Bool
<= Double
epsilon_v then
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[
Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' Set IntSet
f1 (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
g0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g1))
,
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum forall a b. (a -> b) -> a -> b
$ do
IntSet
js <- forall a. Set a -> [a]
Set.toList Set IntSet
g0
let f' :: Set IntSet
f' = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (IntSet
js IntSet -> IntSet -> Bool
`disjoint`) Set IntSet
f0
g' :: Set IntSet
g' = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
js) Set IntSet
g1
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
IntSet
ys <- Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
g') (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
f')
let ys2 :: IntSet
ys2 = Int -> IntSet -> IntSet
IntSet.insert Int
x forall a b. (a -> b) -> a -> b
$ IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` (IntSet
js IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
ys)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (IntSet
ys2 IntSet -> (Set IntSet, Set IntSet) -> Bool
`isCounterExampleOf` (Set IntSet
f,Set IntSet
g)) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
ys2
]
else if Double
epsilon_x_g forall a. Ord a => a -> a -> Bool
<= Double
epsilon_v then
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> IntSet -> IntSet
IntSet.insert Int
x) forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
f0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
f1)) Set IntSet
g1
,
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum forall a b. (a -> b) -> a -> b
$ do
IntSet
is <- forall a. Set a -> [a]
Set.toList Set IntSet
f0
let f' :: Set IntSet
f' = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
is) Set IntSet
f1
g' :: Set IntSet
g' = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (IntSet
is IntSet -> IntSet -> Bool
`disjoint`) Set IntSet
g0
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
IntSet
ys <- Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
f') (Set IntSet -> Set IntSet
deleteRedundancy Set IntSet
g')
let ys2 :: IntSet
ys2 = IntSet
is IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
ys
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (IntSet
ys2 IntSet -> (Set IntSet, Set IntSet) -> Bool
`isCounterExampleOf` (Set IntSet
f,Set IntSet
g)) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
ys2
]
else
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[
Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' Set IntSet
f1 (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
g0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g1))
,
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> IntSet -> IntSet
IntSet.insert Int
x) forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
f0 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
f1)) Set IntSet
g1
]
where
size_f :: Int
size_f = forall a. Set a -> Int
Set.size Set IntSet
f
size_g :: Int
size_g = forall a. Set a -> Int
Set.size Set IntSet
g
v :: Int
v = Int
size_f forall a. Num a => a -> a -> a
* Int
size_g
epsilon_v :: Double
epsilon_v = Double
1 forall a. Fractional a => a -> a -> a
/ Double -> Double
xhi (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
v)
xs :: IntSet
xs = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Set IntSet
f forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g