{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
-- Copyright   :  (c) Masahiro Sakai 2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-- This modules provides functions to check whether two monotone boolean
-- functions /f/ and /g/ given in DNFs are mutually dual (/i.e./ f(x1,…,xn) = ¬g(¬x1,…,¬xn)).
--
-- References:
--
-- * [FredmanKhachiyan1996] Michael L. Fredman and Leonid Khachiyan,
--   On the Complexicy of Dualization of Monotone Disjunctifve Normal Forms,
--   Journal of Algorithms, vol. 21, pp. 618-628, 1996.
--   <http://www.sciencedirect.com/science/article/pii/S0196677496900620>
--   <http://www.cs.tau.ac.il/~fiat/dmsem03/On%20the%20complexity%20of%20Dualization%20of%20monotone%20Disjunctive%20Normal%20Forms%20-%201996.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
  (
  -- * Main functions
    areDualDNFs
  , checkDuality
  , checkDualityA
  , checkDualityB

  -- * Redundancy
  -- $Redundancy
  , isRedundant
  , deleteRedundancy

  -- * Utilities for testing
  , isCounterExampleOf
  , occurFreq

  -- * Internal functions exported only for testing purpose
  , 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 n ** xhi n == n
xhi :: Double -> Double
xhi :: Double -> Double
xhi Double
n = (Double -> Double) -> Double -> [Double]
forall a. (a -> a) -> a -> [a]
iterate Double -> Double
f Double
m [Double] -> Int -> Double
forall a. (?callStack::CallStack) => [a] -> Int -> a
!! Int
30
  where
    m :: Double
m = Double
logn Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double -> Double -> Double
forall a. Floating a => a -> a -> a
logBase Double
2 Double
logn
      where
        logn :: Double
logn = Double -> Double -> Double
forall a. Floating a => a -> a -> a
logBase Double
2 Double
n
    f :: Double -> Double
f Double
x = Double
m Double -> Double -> Double
forall a. Num a => a -> a -> a
* ((Double
logx Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double -> Double -> Double
forall a. Floating a => a -> a -> a
logBase Double
2 Double
logx) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
logx)
      where
        logx :: Double
logx = Double -> Double -> Double
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 (IntSet -> Bool) -> IntSet -> Bool
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 (Bool -> Bool) -> Bool -> Bool
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 = (IntSet -> Bool) -> Set IntSet -> Bool
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 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
rhs
  where
    lhs :: Bool
lhs = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [IntSet
is IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` IntSet
xs | IntSet
is <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
f]
    rhs :: Bool
rhs = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [IntSet
xs IntSet -> IntSet -> Bool
`disjoint` IntSet
js | IntSet
js <- Set IntSet -> [IntSet]
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 = Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
f Int -> Int -> Int
forall a. Num a => a -> a -> a
* Set IntSet -> Int
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 = (IntSet -> Bool) -> Set IntSet -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\IntSet
is -> (IntSet -> Bool) -> Set IntSet -> Bool
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 = [IntSet] -> Maybe IntSet
forall a. [a] -> Maybe a
listToMaybe ([IntSet] -> Maybe IntSet) -> [IntSet] -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ do
  IntSet
is <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
f
  IntSet
js <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
g
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ IntSet
is IntSet -> IntSet -> Bool
`disjoint` IntSet
js
  IntSet -> [IntSet]
forall a. a -> [a]
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 IntSet -> IntSet -> Bool
forall a. Eq a => a -> a -> Bool
== Set IntSet -> IntSet
h Set IntSet
g
  where
    h :: Set IntSet -> IntSet
h = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions ([IntSet] -> IntSet)
-> (Set IntSet -> [IntSet]) -> Set IntSet -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList

-- | Find @xs@ such that @xs `isCounterExampleOf` (f,g)@ unless @'condition_1_2' f g@.
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 = IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [IntSet] -> IntSet
forall a. (?callStack::CallStack) => [a] -> a
head [Int -> IntSet -> IntSet
IntSet.delete Int
v1 IntSet
is | IntSet
is <- Set IntSet -> [IntSet]
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 = IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [IntSet] -> IntSet
forall a. (?callStack::CallStack) => [a] -> a
head [(IntSet
vs IntSet -> IntSet -> IntSet
`IntSet.difference` (Int -> IntSet -> IntSet
IntSet.delete Int
v2 IntSet
js)) | IntSet
js <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
g, Int
v2 Int -> IntSet -> Bool
`IntSet.member` IntSet
js]
  | Bool
otherwise = Maybe IntSet
forall a. Maybe a
Nothing
  where
    f_vs :: IntSet
f_vs = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$ Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
f
    g_vs :: IntSet
g_vs = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$ Set IntSet -> [IntSet]
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
g Bool -> Bool -> Bool
&& Set IntSet -> Int
maxSize Set IntSet
g Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
f
  where
    maxSize :: Set IntSet -> Int
maxSize Set IntSet
xs = (Int -> Int -> Int) -> Int -> [Int] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 [IntSet -> Int
IntSet.size IntSet
i | IntSet
i <- Set IntSet -> [IntSet]
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 = [IntSet] -> Maybe IntSet
forall a. [a] -> Maybe a
listToMaybe ([IntSet] -> Maybe IntSet) -> [IntSet] -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$
  [[IntSet] -> IntSet
forall a. (?callStack::CallStack) => [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 <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
f, IntSet -> Int
IntSet.size IntSet
is Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
g_size] [IntSet] -> [IntSet] -> [IntSet]
forall a. [a] -> [a] -> [a]
++
  [IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` [IntSet] -> IntSet
forall a. (?callStack::CallStack) => [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 <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
g, IntSet -> Int
IntSet.size IntSet
js Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
f_size]
  where
    xs :: IntSet
xs = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$ Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList (Set IntSet -> [IntSet]) -> Set IntSet -> [IntSet]
forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set IntSet
f Set IntSet
g
    f_size :: Int
f_size = Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
f
    g_size :: Int
g_size = Set IntSet -> Int
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 = [Rational] -> Rational
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
1 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% (Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ IntSet -> Int
IntSet.size IntSet
i) | IntSet
i <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
f] Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+
        [Rational] -> Rational
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
1 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% (Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ IntSet -> Int
IntSet.size IntSet
j) | IntSet
j <- Set IntSet -> [IntSet]
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 Rational -> Rational -> Bool
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 Maybe IntSet
forall a. Maybe a
Nothing
  else IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
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 = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$ Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList (Set IntSet -> [IntSet]) -> Set IntSet -> [IntSet]
forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Set IntSet
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 Rational -> Rational -> Bool
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
        -- f = x f1 ∨ f2
        -- g = x g2 ∨ g1
        f1 :: Set IntSet
f1 = (IntSet -> IntSet) -> Set IntSet -> Set IntSet
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 = (IntSet -> Bool) -> Set IntSet -> Set IntSet
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Int
v Int -> IntSet -> Bool
`IntSet.notMember`) Set IntSet
g
        f2 :: Set IntSet
f2 = (IntSet -> Bool) -> Set IntSet -> Set IntSet
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Int
v Int -> IntSet -> Bool
`IntSet.notMember`) Set IntSet
f
        g2 :: Set IntSet
g2 = (IntSet -> IntSet) -> Set IntSet -> Set IntSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
v) Set IntSet
g

-- | @'isRedundant' F@ tests whether /F/ contains redundant implicants.
isRedundant :: Set IntSet -> Bool
isRedundant :: Set IntSet -> Bool
isRedundant = [IntSet] -> Bool
loop ([IntSet] -> Bool)
-> (Set IntSet -> [IntSet]) -> Set IntSet -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntSet -> Int) -> [IntSet] -> [IntSet]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn IntSet -> Int
IntSet.size ([IntSet] -> [IntSet])
-> (Set IntSet -> [IntSet]) -> Set IntSet -> [IntSet]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList
  where
    loop :: [IntSet] -> Bool
    loop :: [IntSet] -> Bool
loop [] = Bool
False
    loop (IntSet
xs:[IntSet]
yss) = [Bool] -> Bool
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 (Bool -> Bool) -> (Set IntSet -> Bool) -> Set IntSet -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set IntSet -> Bool
isRedundant

-- | Removes redundant implicants from a given DNF.
deleteRedundancy :: Set IntSet -> Set IntSet
deleteRedundancy :: Set IntSet -> Set IntSet
deleteRedundancy = (Set IntSet -> IntSet -> Set IntSet)
-> Set IntSet -> [IntSet] -> Set IntSet
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Set IntSet -> IntSet -> Set IntSet
f Set IntSet
forall a. Set a
Set.empty ([IntSet] -> Set IntSet)
-> (Set IntSet -> [IntSet]) -> Set IntSet -> Set IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntSet -> Int) -> [IntSet] -> [IntSet]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn IntSet -> Int
IntSet.size ([IntSet] -> [IntSet])
-> (Set IntSet -> [IntSet]) -> Set IntSet -> [IntSet]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set IntSet -> [IntSet]
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 (IntSet -> Bool) -> Set IntSet -> Bool
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 IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => a -> Set a -> Set a
Set.insert IntSet
ys Set IntSet
xss

-- | @occurFreq  x F@ computes /|{I∈F | x∈I}| \/ |F|/
occurFreq
  :: Fractional a
  => Int -- ^ a variable /x/
  -> Set IntSet -- ^ a DNF /F/
  -> a
occurFreq :: forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
f = Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int
1 | IntSet
is <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
f, Int
x Int -> IntSet -> Bool
`IntSet.member` IntSet
is] :: Int) a -> a -> a
forall a. Fractional a => a -> a -> a
/ Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
f)

-- | @areDualDNFs f g@ checks whether two monotone boolean functions /f/
-- and /g/ are mutually dual (/i.e./ f(x1,…,xn) = ¬g(¬x1,…,xn)).
--
-- Note that this function does not care about redundancy of DNFs.
--
-- Complexity: /O(n^o(log n))/ where @n = 'IntSet.size' f + 'IntSet.size' g@.
areDualDNFs
  :: Set IntSet -- ^ a monotone boolean function /f/ given in DNF
  -> Set IntSet -- ^ a monotone boolean function /g/ given in DNF
  -> Bool
areDualDNFs :: Set IntSet -> Set IntSet -> Bool
areDualDNFs Set IntSet
f Set IntSet
g = Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe IntSet -> Bool) -> Maybe IntSet -> Bool
forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB Set IntSet
f Set IntSet
g

-- | Synonym for 'checkDualityB'.
checkDuality :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDuality :: Set IntSet -> Set IntSet -> Maybe IntSet
checkDuality = Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB

-- | @checkDualityA f g@ checks whether two monotone boolean functions /f/
-- and /g/ are mutually dual (/i.e./ f(x1,…,xn) = ¬g(¬x1,…,¬xn)) using
-- “Algorithm A” of [FredmanKhachiyan1996].
--
-- If they are indeed mutually dual it returns @Nothing@, otherwise
-- it returns @Just cs@ such that {xi ↦ (if xi∈cs then True else False) | i∈{1…n}}
-- is a solution of f(x1,…,xn) = g(¬x1,…,¬xn)).
--
-- Note that this function does not care about redundancy of DNFs.
--
-- Complexity: /O(n^O(log^2 n))/ where @n = 'IntSet.size' f + 'IntSet.size' g@.
checkDualityA
  :: Set IntSet -- ^ a monotone boolean function /f/ given in DNF
  -> Set IntSet -- ^ a monotone boolean function /g/ given in DNF
  -> 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 = IntSet -> Maybe IntSet
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
  | Bool -> Bool -> Bool
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 = Maybe IntSet
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 = IntSet -> Maybe IntSet
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 = IntSet -> Maybe IntSet
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 = IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
s
  | Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = Set IntSet -> Set IntSet -> Maybe IntSet
solveSmall Set IntSet
f Set IntSet
g
  | Bool
otherwise = [Maybe IntSet] -> Maybe IntSet
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
      [ -- If x=0 then f(xs)=g(¬xs) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs)
        Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' Set IntSet
f1 (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
g0 Set IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g1))
      , -- If x=1 then f(xs)=g(¬xs) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs)
        (IntSet -> IntSet) -> Maybe IntSet -> Maybe IntSet
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> IntSet -> IntSet
IntSet.insert Int
x) (Maybe IntSet -> Maybe IntSet) -> Maybe IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityA' (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
f0 Set IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
f1)) Set IntSet
g1
      ]
  where
    size_f :: Int
size_f = Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
f
    size_g :: Int
size_g = Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
g
    n :: Int
n = Int
size_f Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
size_g
    v :: Int
v = Int
size_f Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
size_g
    xs :: IntSet
xs = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$ Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList (Set IntSet -> [IntSet]) -> Set IntSet -> [IntSet]
forall a b. (a -> b) -> a -> b
$ Set IntSet
f Set IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g
    epsilon :: Double
    epsilon :: Double
epsilon = Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double -> Double -> Double
forall a. Floating a => a -> a -> a
logBase Double
2 (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n)
    x :: Int
x = [Int] -> Int
forall a. (?callStack::CallStack) => [a] -> a
head [Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs, Int -> Set IntSet -> Double
forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
f Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
>= Double
epsilon Bool -> Bool -> Bool
|| Int -> Set IntSet -> Double
forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
g Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
>= Double
epsilon]
    -- f = x f0 ∨ f1
    (Set IntSet
f0, Set IntSet
f1) = (IntSet -> IntSet) -> Set IntSet -> Set IntSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) (Set IntSet -> Set IntSet)
-> (Set IntSet -> Set IntSet)
-> (Set IntSet, Set IntSet)
-> (Set IntSet, Set IntSet)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Set IntSet -> Set IntSet
forall a. a -> a
id ((Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet))
-> (Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet)
forall a b. (a -> b) -> a -> b
$ (IntSet -> Bool) -> Set IntSet -> (Set IntSet, Set IntSet)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Int
x Int -> IntSet -> Bool
`IntSet.member`) Set IntSet
f
    -- g = x g0 ∨ g1
    (Set IntSet
g0, Set IntSet
g1) = (IntSet -> IntSet) -> Set IntSet -> Set IntSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) (Set IntSet -> Set IntSet)
-> (Set IntSet -> Set IntSet)
-> (Set IntSet, Set IntSet)
-> (Set IntSet, Set IntSet)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Set IntSet -> Set IntSet
forall a. a -> a
id ((Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet))
-> (Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet)
forall a b. (a -> b) -> a -> b
$ (IntSet -> Bool) -> Set IntSet -> (Set IntSet, Set IntSet)
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
  | Bool -> Bool -> Bool
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 = Maybe IntSet
forall a. (?callStack::CallStack) => a
undefined
  | Set IntSet -> Bool
forall a. Set a -> Bool
Set.null Set IntSet
f Bool -> Bool -> Bool
&& Set IntSet -> Bool
forall a. Set a -> Bool
Set.null Set IntSet
g = IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
IntSet.empty
  | Set IntSet -> Bool
forall a. Set a -> Bool
Set.null Set IntSet
f = Bool -> Maybe IntSet -> Maybe IntSet
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bool -> Bool
not (Set IntSet -> Bool
forall a. Set a -> Bool
Set.null Set IntSet
g)) (Maybe IntSet -> Maybe IntSet) -> Maybe IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$
      if IntSet
IntSet.empty IntSet -> Set IntSet -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set IntSet
g
      then Maybe IntSet
forall a. Maybe a
Nothing
      else IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just ([IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions (Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
g))
  | Set IntSet -> Bool
forall a. Set a -> Bool
Set.null Set IntSet
g = Bool -> Maybe IntSet -> Maybe IntSet
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bool -> Bool
not (Set IntSet -> Bool
forall a. Set a -> Bool
Set.null Set IntSet
f)) (Maybe IntSet -> Maybe IntSet) -> Maybe IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$
      if IntSet
IntSet.empty IntSet -> Set IntSet -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set IntSet
f
      then Maybe IntSet
forall a. Maybe a
Nothing
      else IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
IntSet.empty
  | Int
size_f Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Int
size_g Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 =
      let
        is :: IntSet
is = Set IntSet -> IntSet
forall a. Set a -> a
Set.findMin Set IntSet
f
        js :: IntSet
js = Set IntSet -> IntSet
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then
           if Int
js_size Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then
             Maybe IntSet
forall a. Maybe a
Nothing
           else
             IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet
js IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
is)
         else
           IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet
is IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
js)
  | Bool
otherwise = [Char] -> Maybe IntSet
forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"should not happen"
  where
    size_f :: Int
size_f = Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
f
    size_g :: Int
size_g = Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
g

-- | @checkDualityB f g@ checks whether two monotone boolean functions /f/
-- and /g/ are mutually dual (i.e. f(x1,…,xn) = ¬g(¬x1,…,xn)) using
-- “Algorithm B” of [FredmanKhachiyan1996].
--
-- If they are indeed mutually dual it returns @Nothing@, otherwise
-- it returns @Just cs@ such that {xi ↦ (if xi∈cs then True else False) | i∈{1…n}}
-- is a solution of f(x1,…,xn) = g(¬x1,…,xn)).
--
-- Note that this function does not care about redundancy of DNFs.
--
-- Complexity: /O(n^o(log n))/ where @n = 'Set.size' f + 'Set.size' g@.
checkDualityB
  :: Set IntSet -- ^ a monotone boolean function /f/ given in DNF
  -> Set IntSet -- ^ a monotone boolean function /g/ given in DNF
  -> 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 = IntSet -> Maybe IntSet
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
  | Bool -> Bool -> Bool
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 = Maybe IntSet
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 = IntSet -> Maybe IntSet
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 = IntSet -> Maybe IntSet
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 = IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
s
  | Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = Set IntSet -> Set IntSet -> Maybe IntSet
solveSmall Set IntSet
f Set IntSet
g
--  | min size_f size_g <= 2 = undefined
  | Bool
otherwise =
      let x :: Int
x = [Int] -> Int
forall a. (?callStack::CallStack) => [a] -> a
head [Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs, Int -> Set IntSet -> Rational
forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
f Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> (Rational
0::Rational), Int -> Set IntSet -> Rational
forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
g Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> (Rational
0::Rational)]
          -- f = x f0 ∨ f1
          (Set IntSet
f0, Set IntSet
f1) = (IntSet -> IntSet) -> Set IntSet -> Set IntSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) (Set IntSet -> Set IntSet)
-> (Set IntSet -> Set IntSet)
-> (Set IntSet, Set IntSet)
-> (Set IntSet, Set IntSet)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Set IntSet -> Set IntSet
forall a. a -> a
id ((Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet))
-> (Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet)
forall a b. (a -> b) -> a -> b
$ (IntSet -> Bool) -> Set IntSet -> (Set IntSet, Set IntSet)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (Int
x Int -> IntSet -> Bool
`IntSet.member`) Set IntSet
f
          -- g = x g0 ∨ g1
          (Set IntSet
g0, Set IntSet
g1) = (IntSet -> IntSet) -> Set IntSet -> Set IntSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> IntSet -> IntSet
IntSet.delete Int
x) (Set IntSet -> Set IntSet)
-> (Set IntSet -> Set IntSet)
-> (Set IntSet, Set IntSet)
-> (Set IntSet, Set IntSet)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Set IntSet -> Set IntSet
forall a. a -> a
id ((Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet))
-> (Set IntSet, Set IntSet) -> (Set IntSet, Set IntSet)
forall a b. (a -> b) -> a -> b
$ (IntSet -> Bool) -> Set IntSet -> (Set IntSet, Set IntSet)
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 = Int -> Set IntSet -> Double
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 = Int -> Set IntSet -> Double
forall a. Fractional a => Int -> Set IntSet -> a
occurFreq Int
x Set IntSet
g
      in if Double
epsilon_x_f Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
epsilon_v then
           [Maybe IntSet] -> Maybe IntSet
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
           [ {- f(xs ∪ {x↦0})=g(¬xs ∪ {x↦1}) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs). -}
             Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' Set IntSet
f1 (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
g0 Set IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g1))
           , {- f(¬xs ∪ {x↦1}) = g(xs ∪ {x↦0})
                ⇔ f0(¬xs) ∨ f1(¬xs) = g1(xs)
                ⇔ f0(¬xs) ∨ (¬g0(xs)∧¬g1(xs)) = g1(xs) {- duality of f1 and g0∨g1 -}
                ⇔ f0(¬xs) = g1(xs) and g0(xs) = 1
                   {- g0(xs)=0 is impossible, because
                      it implies f0(¬xs)∨¬g1(xs)=g1(xs) and then
                      f0(¬xs)=g1(xs)=1 which contradicts condition (1.1) -}
              -}
             [Maybe IntSet] -> Maybe IntSet
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Maybe IntSet] -> Maybe IntSet) -> [Maybe IntSet] -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ do
               IntSet
js <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
g0
               let f' :: Set IntSet
f' = (IntSet -> Bool) -> Set IntSet -> Set IntSet
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (IntSet
js IntSet -> IntSet -> Bool
`disjoint`) Set IntSet
f0
                   g' :: Set IntSet
g' = (IntSet -> IntSet) -> Set IntSet -> Set IntSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
js) Set IntSet
g1
               Maybe IntSet -> [Maybe IntSet]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> [Maybe IntSet]) -> Maybe IntSet -> [Maybe IntSet]
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 (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` (IntSet
js IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
ys)
                 Bool -> Maybe () -> Maybe ()
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (IntSet
ys2 IntSet -> (Set IntSet, Set IntSet) -> Bool
`isCounterExampleOf` (Set IntSet
f,Set IntSet
g)) (Maybe () -> Maybe ()) -> Maybe () -> Maybe ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 IntSet -> Maybe IntSet
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
ys2
           ]
         else if Double
epsilon_x_g Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
epsilon_v then
           [Maybe IntSet] -> Maybe IntSet
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
           [ {- f(xs ∪ {x↦1}) = g(¬xs ∪ {x↦0})) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs). -}
             (IntSet -> IntSet) -> Maybe IntSet -> Maybe IntSet
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> IntSet -> IntSet
IntSet.insert Int
x) (Maybe IntSet -> Maybe IntSet) -> Maybe IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
f0 Set IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
f1)) Set IntSet
g1
           , {- f(xs ∪ {x↦0}) = g(¬xs ∪ {x↦1})
                ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs)
                ⇔ f1(xs) = g0(¬xs) ∨ (¬f0(xs)∧¬f1(xs))  {- duality of g1 and f0∨f1 -}
                ⇔ f1(xs) = g0(¬xs) and f0(xs) = 1
                   {- f0(xs)=0 is impossible, because
                      it implies f1(xs)=g0(¬xs)∨¬f1(xs) and then
                      f1(xs)=g0(¬xs)=1 which contradicts condition (1.1) -}
              -}
             [Maybe IntSet] -> Maybe IntSet
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Maybe IntSet] -> Maybe IntSet) -> [Maybe IntSet] -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ do
               IntSet
is <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
f0
               let f' :: Set IntSet
f' = (IntSet -> IntSet) -> Set IntSet -> Set IntSet
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' = (IntSet -> Bool) -> Set IntSet -> Set IntSet
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (IntSet
is IntSet -> IntSet -> Bool
`disjoint`) Set IntSet
g0
               Maybe IntSet -> [Maybe IntSet]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> [Maybe IntSet]) -> Maybe IntSet -> [Maybe IntSet]
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
                 Bool -> Maybe () -> Maybe ()
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (IntSet
ys2 IntSet -> (Set IntSet, Set IntSet) -> Bool
`isCounterExampleOf` (Set IntSet
f,Set IntSet
g)) (Maybe () -> Maybe ()) -> Maybe () -> Maybe ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 IntSet -> Maybe IntSet
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
ys2
           ]
         else -- epsilon_v < min epsilon_x_f epsilon_x_g
           [Maybe IntSet] -> Maybe IntSet
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
           [ -- If x=0 then f(xs)=g(¬xs) ⇔ f1(xs) = g0(¬xs) ∨ g1(¬xs)
             Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' Set IntSet
f1 (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
g0 Set IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g1))
           , -- If x=1 then f(xs)=g(¬xs) ⇔ f0(xs) ∨ f1(xs) = g1(¬xs)
             (IntSet -> IntSet) -> Maybe IntSet -> Maybe IntSet
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> IntSet -> IntSet
IntSet.insert Int
x) (Maybe IntSet -> Maybe IntSet) -> Maybe IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ Set IntSet -> Set IntSet -> Maybe IntSet
checkDualityB' (Set IntSet -> Set IntSet
deleteRedundancy (Set IntSet
f0 Set IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
f1)) Set IntSet
g1
           ]
  where
    size_f :: Int
size_f = Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
f
    size_g :: Int
size_g = Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
g
    v :: Int
v = Int
size_f Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
size_g
    epsilon_v :: Double
epsilon_v = Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double -> Double
xhi (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
v)
    xs :: IntSet
xs = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$ Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList (Set IntSet -> [IntSet]) -> Set IntSet -> [IntSet]
forall a b. (a -> b) -> a -> b
$ Set IntSet
f Set IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set IntSet
g

-- $Redundancy
-- An implicant /I∈F/ of a DNF /F/ is redundant if /F/ contains proper subset of /I/.
-- A DNF /F/ is called redundant if it contains redundant implicants.
-- The main functions of this modules does not care about redundancy of DNFs.