{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}
module Test.HittingSets (hittingSetsTestGroup) where

import Prelude hiding (all)

import Control.Arrow
import Control.Monad
import Data.Foldable (all)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Ratio
import Data.Set (Set)
import qualified Data.Set as Set
import Test.Tasty
import Test.Tasty.QuickCheck hiding ((.&&.), (.||.))
import Test.Tasty.HUnit
import Test.Tasty.TH
import qualified ToySolver.Combinatorial.HittingSet.Simple as HittingSet
import qualified ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996 as FredmanKhachiyan1996
import qualified ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999 as GurvichKhachiyan1999
import qualified ToySolver.Combinatorial.HittingSet.DAA as DAA
import qualified ToySolver.Combinatorial.HittingSet.MARCO as MARCO

-- ---------------------------------------------------------------------
-- Hitting sets

case_minimalHittingSets_1 :: Assertion
case_minimalHittingSets_1 = actual @?= expected
  where
    actual    = HittingSet.minimalHittingSets $ Set.fromList $ map IntSet.fromList [[1], [2,3,5], [2,3,6], [2,4,5], [2,4,6]]
    expected  = Set.fromList $ map IntSet.fromList [[1,2], [1,3,4], [1,5,6]]

-- an example from http://kuma-san.net/htcbdd.html
case_minimalHittingSets_2 :: Assertion
case_minimalHittingSets_2 = actual @?= expected
  where
    actual    = HittingSet.minimalHittingSets $ Set.fromList $ map IntSet.fromList [[2,4,7], [7,8], [9], [9,10]]
    expected  = Set.fromList $ map IntSet.fromList [[7,9], [4,8,9], [2,8,9]]

hyperGraph :: Gen (Set IntSet)
hyperGraph = do
  nv <- choose (0, 10)
  ne <- if nv==0 then return 0 else choose (0, 20)
  liftM Set.fromList $ replicateM ne $ do
    n <- choose (1,nv)
    liftM IntSet.fromList $ replicateM n $ choose (1, nv)

isHittingSetOf :: IntSet -> Set IntSet -> Bool
isHittingSetOf s g = all (\e -> not (IntSet.null (s `IntSet.intersection` e))) g

prop_minimalHittingSets_duality :: Property
prop_minimalHittingSets_duality =
  forAll hyperGraph $ \g ->
    let h = HittingSet.minimalHittingSets g
    in h == HittingSet.minimalHittingSets (HittingSet.minimalHittingSets h)

prop_minimalHittingSets_isHittingSet :: Property
prop_minimalHittingSets_isHittingSet =
  forAll hyperGraph $ \g ->
    all (`isHittingSetOf` g) (HittingSet.minimalHittingSets g)

prop_minimalHittingSets_minimality :: Property
prop_minimalHittingSets_minimality =
  forAll hyperGraph $ \g ->
    forAll (elements (Set.toList (HittingSet.minimalHittingSets g))) $ \s ->
      if IntSet.null s then
        property True
      else
        forAll (elements (IntSet.toList s)) $ \v ->
          not $ IntSet.delete v s `isHittingSetOf` g

mutuallyDualHypergraphs :: Gen (Set IntSet, Set IntSet)
mutuallyDualHypergraphs = do
  g <- liftM HittingSet.minimalHittingSets hyperGraph
  let f = HittingSet.minimalHittingSets g
  return (f,g)

mutuallyDualDNFs :: Gen (Set IntSet, Set IntSet)
mutuallyDualDNFs = do
  (f,g) <- mutuallyDualHypergraphs
  let xs = IntSet.unions $ Set.toList $ f `Set.union` g
  if IntSet.null xs then
    return (f,g)
  else do
    let xs' = IntSet.toList xs
    let mutate h = liftM Set.unions $ do
          forM (Set.toList h) $ \is -> oneof $
            [ return $ Set.singleton is
            , do i <- elements xs'
                 return $ Set.fromList [is, IntSet.insert i is]
            ]
    f' <- mutate f
    g' <- mutate g
    return (f',g')

-- Pair of DNFs that are nearly dual.
pairOfDNFs :: Gen (Set IntSet, Set IntSet)
pairOfDNFs = do
  (f,g) <- mutuallyDualDNFs
  let mutate h = liftM Set.unions $ do
        forM (Set.toList h) $ \is -> oneof $
          [return Set.empty, return (Set.singleton is)] ++
          [ do x <- elements (IntSet.toList is)
               return $ Set.singleton $ IntSet.delete x is
          | not (IntSet.null is)
          ]
  return (f,g)

prop_FredmanKhachiyan1996_checkDualityA_prop1 :: Property
prop_FredmanKhachiyan1996_checkDualityA_prop1 =
  forAll mutuallyDualDNFs $ \(f,g) ->
    FredmanKhachiyan1996.checkDualityA f g == Nothing

prop_FredmanKhachiyan1996_checkDualityA_prop2 :: Property
prop_FredmanKhachiyan1996_checkDualityA_prop2 =
  forAll pairOfDNFs $ \(f,g) ->
    case FredmanKhachiyan1996.checkDualityA f g of
      Nothing -> True
      Just xs -> xs `FredmanKhachiyan1996.isCounterExampleOf` (f,g)

prop_FredmanKhachiyan1996_checkDualityB_prop1 :: Property
prop_FredmanKhachiyan1996_checkDualityB_prop1 =
  forAll mutuallyDualDNFs $ \(f,g) ->
    FredmanKhachiyan1996.checkDualityA f g == Nothing

prop_FredmanKhachiyan1996_checkDualityB_prop2 :: Property
prop_FredmanKhachiyan1996_checkDualityB_prop2 =
  forAll pairOfDNFs $ \(f,g) ->
    case FredmanKhachiyan1996.checkDualityB f g of
      Nothing -> True
      Just xs -> xs `FredmanKhachiyan1996.isCounterExampleOf` (f,g)

prop_FredmanKhachiyan1996_lemma_1 :: Property
prop_FredmanKhachiyan1996_lemma_1 =
  forAll mutuallyDualHypergraphs $ \(f,g) ->
    let e :: Rational
        e = sum [1 % (2 ^ IntSet.size i) | i <- Set.toList f] +
            sum [1 % (2 ^ IntSet.size j) | j <- Set.toList g]
    in e >= 1

prop_FredmanKhachiyan1996_corollary_1 :: Property
prop_FredmanKhachiyan1996_corollary_1 =
  forAll mutuallyDualHypergraphs $ \(f,g) ->
    let n = Set.size f + Set.size g
        m = minimum [IntSet.size is | is <- Set.toList (f `Set.union` g)]
    in (fromIntegral m :: Double) <= logBase 2 (fromIntegral n)

prop_FredmanKhachiyan1996_lemma_2 :: Property
prop_FredmanKhachiyan1996_lemma_2 =
  forAll mutuallyDualHypergraphs $ \(f,g) ->
    let n = Set.size f + Set.size g
        epsilon :: Double
        epsilon = 1 / logBase 2 (fromIntegral n)
        vs = IntSet.unions $ Set.toList $ f `Set.union` g
    in (Set.size f * Set.size g >= 1)
       ==> any (\v -> FredmanKhachiyan1996.occurFreq v f >= epsilon || FredmanKhachiyan1996.occurFreq v g >= epsilon) (IntSet.toList vs)

prop_FredmanKhachiyan1996_lemma_3_a :: Property
prop_FredmanKhachiyan1996_lemma_3_a =
  forAll mutuallyDualHypergraphs $ \(f,g) ->
    let vs = IntSet.unions $ Set.toList $ f `Set.union` g
        x = IntSet.findMin vs
        -- f = x f0 ∨ f1
        (f0, f1) = Set.map (IntSet.delete x) *** id $ Set.partition (x `IntSet.member`) f
        -- g = x g0 ∨ g1
        (g0, g1) = Set.map (IntSet.delete x) *** id $ Set.partition (x `IntSet.member`) g
    in not (IntSet.null vs)
       ==>
         HittingSet.minimalHittingSets f1 == FredmanKhachiyan1996.deleteRedundancy (g0 `Set.union` g1) &&
         HittingSet.minimalHittingSets g1 == FredmanKhachiyan1996.deleteRedundancy (f0 `Set.union` f1)

prop_FredmanKhachiyan1996_to_selfDuality :: Property
prop_FredmanKhachiyan1996_to_selfDuality =
  forAll mutuallyDualHypergraphs $ \(f,g) ->
    let vs = IntSet.unions $ Set.toList $ f `Set.union` g
        y = if IntSet.null vs then 0 else IntSet.findMax vs + 1
        z = y + 1
        h = FredmanKhachiyan1996.deleteRedundancy $ Set.unions
              [ Set.map (IntSet.insert y) f
              , Set.map (IntSet.insert z) g
              , Set.singleton (IntSet.fromList [y,z])
              ] 
    in HittingSet.minimalHittingSets h == h

case_FredmanKhachiyan1996_condition_1_1_solve_L :: Assertion
case_FredmanKhachiyan1996_condition_1_1_solve_L = (xs `FredmanKhachiyan1996.isCounterExampleOf` (f,g)) @?= True
  where
    Just xs = FredmanKhachiyan1996.condition_1_1_solve f g
    f = Set.fromList $ map IntSet.fromList [[2,4,7], [7,8], [9], [4]]
    g = Set.fromList $ map IntSet.fromList [[7,9], [4,8,9], [2,8,9]]

case_FredmanKhachiyan1996_condition_1_1_solve_R :: Assertion
case_FredmanKhachiyan1996_condition_1_1_solve_R = (xs `FredmanKhachiyan1996.isCounterExampleOf` (f,g)) @?= True
  where
    Just xs = FredmanKhachiyan1996.condition_1_1_solve f g
    f = Set.fromList $ map IntSet.fromList [[2,4,7], [7,8], [9]]
    g = Set.fromList $ map IntSet.fromList [[7,9], [4,8,9], [2,8,9], [4,7,8]]

case_FredmanKhachiyan1996_condition_1_2_solve_L :: Assertion
case_FredmanKhachiyan1996_condition_1_2_solve_L = (xs `FredmanKhachiyan1996.isCounterExampleOf` (f,g)) @?= True
  where
    Just xs = FredmanKhachiyan1996.condition_1_2_solve f g
    f = Set.fromList $ map IntSet.fromList [[2,4,7], [7,8], [9,10]]
    g = Set.fromList $ map IntSet.fromList [[7,9], [4,8,9], [2,8,9]]

case_FredmanKhachiyan1996_condition_1_2_solve_R :: Assertion
case_FredmanKhachiyan1996_condition_1_2_solve_R = (xs `FredmanKhachiyan1996.isCounterExampleOf` (f,g)) @?= True
  where
    Just xs = FredmanKhachiyan1996.condition_1_2_solve f g
    f = Set.fromList $ map IntSet.fromList [[2,4,7], [7,8], [9]]
    g = Set.fromList $ map IntSet.fromList [[7,9], [4,8,9], [2,8,9,10]]

case_FredmanKhachiyan1996_condition_1_3_solve_L :: Assertion
case_FredmanKhachiyan1996_condition_1_3_solve_L = (xs `FredmanKhachiyan1996.isCounterExampleOf` (f,g)) @?= True
  where
    Just xs = FredmanKhachiyan1996.condition_1_3_solve f g
    f = Set.fromList $ map IntSet.fromList [[2,4,7,10], [7,8], [9]]
    g = Set.fromList $ map IntSet.fromList [[7,9,10], [4,8,9], [2,8,9]]

case_FredmanKhachiyan1996_condition_1_3_solve_R :: Assertion
case_FredmanKhachiyan1996_condition_1_3_solve_R = (xs `FredmanKhachiyan1996.isCounterExampleOf` (f,g)) @?= True
  where
    Just xs = FredmanKhachiyan1996.condition_1_3_solve f g
    f = Set.fromList $ map IntSet.fromList [[2,4,7], [7,8], [9,10]]
    g = Set.fromList $ map IntSet.fromList [[7,9], [4,8,9], [2,8,9,10]]

case_FredmanKhachiyan1996_condition_2_1_solve_L :: Assertion
case_FredmanKhachiyan1996_condition_2_1_solve_L = (xs `FredmanKhachiyan1996.isCounterExampleOf` (f,g)) @?= True
  where
    Just xs = FredmanKhachiyan1996.condition_2_1_solve f g
    f = Set.fromList $ map IntSet.fromList [[2,4,7], [4,7,9], [7,8,9]]
    g = Set.fromList $ map IntSet.fromList [[2,4,7], [2,8,9], [4,8,9]]

case_FredmanKhachiyan1996_condition_2_1_solve_R :: Assertion
case_FredmanKhachiyan1996_condition_2_1_solve_R = (xs `FredmanKhachiyan1996.isCounterExampleOf` (f,g)) @?= True
  where
    Just xs = FredmanKhachiyan1996.condition_2_1_solve f g
    g = Set.fromList $ map IntSet.fromList [[2,4,7], [4,7,9], [7,8,9]]
    f = Set.fromList $ map IntSet.fromList [[2,4,7], [2,8,9], [4,8,9]]

case_FredmanKhachiyan1996_checkDualityA :: Assertion
case_FredmanKhachiyan1996_checkDualityA = FredmanKhachiyan1996.checkDualityA f g @?= Nothing
  where
    f = Set.fromList $ map IntSet.fromList [[2,4,7], [7,8], [9]]
    g = Set.fromList $ map IntSet.fromList [[7,9], [4,8,9], [2,8,9]]

case_FredmanKhachiyan1996_checkDualityB :: Assertion
case_FredmanKhachiyan1996_checkDualityB = FredmanKhachiyan1996.checkDualityB f g @?= Nothing
  where
    f = Set.fromList $ map IntSet.fromList [[2,4,7], [7,8], [9]]
    g = Set.fromList $ map IntSet.fromList [[7,9], [4,8,9], [2,8,9]]

propGenerateCNFAndDNF
  :: (IntSet -> (IntSet -> Bool) -> Set IntSet -> Set IntSet -> (Set IntSet, Set IntSet))
  -> Property
propGenerateCNFAndDNF impl = 
  forAll hyperGraph $ \g ->
    let vs = IntSet.unions $ Set.toList g
        f xs = any (\is -> not $ IntSet.null $ xs `IntSet.intersection` is) (Set.toList g)
        dual f is = not $ f (vs `IntSet.difference` is)
        is `isImplicantOf` f = f is
        is `isImplicateOf` f = is `isImplicantOf` dual f
        is `isPrimeImplicantOf` f = is `isImplicantOf` f && all (\i -> not (IntSet.delete i is `isImplicantOf` f)) (IntSet.toList is)
        is `isPrimeImplicateOf` f = is `isImplicateOf` f && all (\i -> not (IntSet.delete i is `isImplicateOf` f)) (IntSet.toList is)
        (cnf,dnf) = impl vs f Set.empty Set.empty
    in all (`isPrimeImplicantOf` f) (Set.toList dnf) &&
       all (`isPrimeImplicateOf` f) (Set.toList cnf)

propMinimalHittingSetsMinimality :: (Set IntSet -> Set IntSet) -> Property
propMinimalHittingSetsMinimality minimalHittingSets =
  forAll hyperGraph $ \g ->
    forAll (elements (Set.toList (minimalHittingSets g))) $ \s ->
      if IntSet.null s then
        property True
      else
        forAll (elements (IntSet.toList s)) $ \v ->
          not $ IntSet.delete v s `isHittingSetOf` g

propMinimalHittingSetsDuality :: (Set IntSet -> Set IntSet) -> Property
propMinimalHittingSetsDuality minimalHittingSets =
  forAll hyperGraph $ \g ->
    let h = minimalHittingSets g
    in h == minimalHittingSets (minimalHittingSets h)

propMinimalHittingSetsIsHittingSet :: (Set IntSet -> Set IntSet) -> Property
propMinimalHittingSetsIsHittingSet minimalHittingSets =
  forAll hyperGraph $ \g ->
    all (`isHittingSetOf` g) (minimalHittingSets g)

prop_GurvichKhachiyan1999_generateCNFAndDNF :: Property
prop_GurvichKhachiyan1999_generateCNFAndDNF = propGenerateCNFAndDNF GurvichKhachiyan1999.generateCNFAndDNF

prop_GurvichKhachiyan1999_minimalHittingSets_duality :: Property
prop_GurvichKhachiyan1999_minimalHittingSets_duality =
  propMinimalHittingSetsDuality GurvichKhachiyan1999.minimalHittingSets

prop_GurvichKhachiyan1999_minimalHittingSets_isHittingSet :: Property
prop_GurvichKhachiyan1999_minimalHittingSets_isHittingSet =
  propMinimalHittingSetsIsHittingSet GurvichKhachiyan1999.minimalHittingSets

prop_GurvichKhachiyan1999_minimalHittingSets_minimality :: Property
prop_GurvichKhachiyan1999_minimalHittingSets_minimality =
  propMinimalHittingSetsIsHittingSet GurvichKhachiyan1999.minimalHittingSets

prop_DAA_generateCNFAndDNF :: Property
prop_DAA_generateCNFAndDNF = propGenerateCNFAndDNF DAA.generateCNFAndDNF

prop_MARCO_generateCNFAndDNF :: Property
prop_MARCO_generateCNFAndDNF = propGenerateCNFAndDNF MARCO.generateCNFAndDNF

prop_MARCO_minimalHittingSets_duality :: Property
prop_MARCO_minimalHittingSets_duality =
  propMinimalHittingSetsDuality MARCO.minimalHittingSets

prop_MARCO_minimalHittingSets_isHittingSet :: Property
prop_MARCO_minimalHittingSets_isHittingSet =
  propMinimalHittingSetsIsHittingSet MARCO.minimalHittingSets

prop_MARCO_minimalHittingSets_minimality :: Property
prop_MARCO_minimalHittingSets_minimality =
  propMinimalHittingSetsIsHittingSet MARCO.minimalHittingSets

------------------------------------------------------------------------
-- Test harness

hittingSetsTestGroup :: TestTree
hittingSetsTestGroup = $(testGroupGenerator)