content: {-# OPTIONS_GHC -Wall #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TemplateHaskell #-}
  module Test.SAT.Types (satTypesTestGroup) where
  
  import Control.Monad
  import Data.Array.IArray
  import Data.List (sort)
  
  import Test.Tasty
  import Test.Tasty.QuickCheck
  import Test.Tasty.HUnit
  import Test.Tasty.TH
  
  import qualified ToySolver.SAT.Types as SAT
  
  import Test.SAT.Utils
  
  ------------------------------------------------------------------------
  
  -- -4*(not x1) + 3*x1 + 10*(not x2)
  -- = -4*(1 - x1) + 3*x1 + 10*(not x2)
  -- = -4 + 4*x1 + 3*x1 + 10*(not x2)
  -- = 7*x1 + 10*(not x2) - 4
  case_normalizePBLinSum_1 :: Assertion
  case_normalizePBLinSum_1 = do
    sort e @?= sort [(7,x1),(10,-x2)]
    c @?= -4
    where
      x1 = 1
      x2 = 2
      (e,c) = SAT.normalizePBLinSum ([(-4,-x1),(3,x1),(10,-x2)], 0)
  
  prop_normalizePBLinSum :: Property
  prop_normalizePBLinSum = forAll g $ \(nv, (s,n)) ->
      let (s2,n2) = SAT.normalizePBLinSum (s,n)
      in flip all (allAssignments nv) $ \m ->
           SAT.evalPBLinSum m s + n == SAT.evalPBLinSum m s2 + n2
    where
      g :: Gen (Int, (SAT.PBLinSum, Integer))
      g = do
        nv <- choose (0, 10)
        s <- forM [1..nv] $ \x -> do
          c <- arbitrary
          p <- arbitrary
          return (c, SAT.literal x p)
        n <- arbitrary
        return (nv, (s,n))
  
  -- -4*(not x1) + 3*x1 + 10*(not x2) >= 3
  -- ⇔ -4*(1 - x1) + 3*x1 + 10*(not x2) >= 3
  -- ⇔ -4 + 4*x1 + 3*x1 + 10*(not x2) >= 3
  -- ⇔ 7*x1 + 10*(not x2) >= 7
  -- ⇔ 7*x1 + 7*(not x2) >= 7
  -- ⇔ x1 + (not x2) >= 1
  case_normalizePBLinAtLeast_1 :: Assertion
  case_normalizePBLinAtLeast_1 = (sort lhs, rhs) @?= (sort [(1,x1),(1,-x2)], 1)
    where
      x1 = 1
      x2 = 2
      (lhs,rhs) = SAT.normalizePBLinAtLeast ([(-4,-x1),(3,x1),(10,-x2)], 3)
  
  prop_normalizePBLinAtLeast :: Property
  prop_normalizePBLinAtLeast = forAll g $ \(nv, c) ->
      let c2 = SAT.normalizePBLinAtLeast c
      in flip all (allAssignments nv) $ \m ->
           SAT.evalPBLinAtLeast m c == SAT.evalPBLinAtLeast m c2
    where
      g :: Gen (Int, SAT.PBLinAtLeast)
      g = do
        nv <- choose (0, 10)
        lhs <- forM [1..nv] $ \x -> do
          c <- arbitrary
          p <- arbitrary
          return (c, SAT.literal x p)
        rhs <- arbitrary
        return (nv, (lhs,rhs))
  
  case_normalizePBLinExactly_1 :: Assertion
  case_normalizePBLinExactly_1 = (sort lhs, rhs) @?= ([], 1)
    where
      x1 = 1
      x2 = 2
      (lhs,rhs) = SAT.normalizePBLinExactly ([(6,x1),(4,x2)], 2)
  
  case_normalizePBLinExactly_2 :: Assertion
  case_normalizePBLinExactly_2 = (sort lhs, rhs) @?= ([], 1)
    where
      x1 = 1
      x2 = 2
      x3 = 3
      (lhs,rhs) = SAT.normalizePBLinExactly ([(2,x1),(2,x2),(2,x3)], 3)
  
  prop_normalizePBLinExactly :: Property
  prop_normalizePBLinExactly = forAll g $ \(nv, c) ->
      let c2 = SAT.normalizePBLinExactly c
      in flip all (allAssignments nv) $ \m ->
           SAT.evalPBLinExactly m c == SAT.evalPBLinExactly m c2
    where
      g :: Gen (Int, SAT.PBLinExactly)
      g = do
        nv <- choose (0, 10)
        lhs <- forM [1..nv] $ \x -> do
          c <- arbitrary
          p <- arbitrary
          return (c, SAT.literal x p)
        rhs <- arbitrary
        return (nv, (lhs,rhs))
  
  prop_cutResolve :: Property
  prop_cutResolve =
    forAll (choose (1, 10)) $ \nv ->
      forAll (g nv True) $ \c1 ->
        forAll (g nv False) $ \c2 ->
          let c3 = SAT.cutResolve c1 c2 1
          in flip all (allAssignments nv) $ \m ->
               not (SAT.evalPBLinExactly m c1 && SAT.evalPBLinExactly m c2) || SAT.evalPBLinExactly m c3
    where
      g :: Int -> Bool -> Gen SAT.PBLinExactly
      g nv b = do
        lhs <- forM [1..nv] $ \x -> do
          if x==1 then do
            c <- liftM ((1+) . abs) arbitrary
            return (c, SAT.literal x b)
          else do
            c <- arbitrary
            p <- arbitrary
            return (c, SAT.literal x p)
        rhs <- arbitrary
        return (lhs, rhs)
  
  case_cutResolve_1 :: Assertion
  case_cutResolve_1 = (sort lhs, rhs) @?= (sort [(1,x3),(1,x4)], 1)
    where
      x1 = 1
      x2 = 2
      x3 = 3
      x4 = 4
      pb1 = ([(1,x1), (1,x2), (1,x3)], 1)
      pb2 = ([(2,-x1), (2,-x2), (1,x4)], 3)
      (lhs,rhs) = SAT.cutResolve pb1 pb2 x1
  
  case_cutResolve_2 :: Assertion
  case_cutResolve_2 = (sort lhs, rhs) @?= (sort lhs2, rhs2)
    where
      x1 = 1
      x2 = 2
      x3 = 3
      x4 = 4
      pb1 = ([(3,x1), (2,-x2), (1,x3), (1,x4)], 3)
      pb2 = ([(1,-x3), (1,x4)], 1)
      (lhs,rhs) = SAT.cutResolve pb1 pb2 x3
      (lhs2,rhs2) = ([(2,x1),(1,-x2),(1,x4)],2) -- ([(3,x1),(2,-x2),(2,x4)], 3)
  
  case_cardinalityReduction :: Assertion
  case_cardinalityReduction = (sort lhs, rhs) @?= ([1,2,3,4,5],4)
    where
      (lhs, rhs) = SAT.cardinalityReduction ([(6,1),(5,2),(4,3),(3,4),(2,5),(1,6)], 17)
  
  prop_pbLinUpperBound :: Property
  prop_pbLinUpperBound =
    forAll (choose (0,10)) $ \nv ->
      forAll (arbitraryPBLinSum nv) $ \s ->
        forAll (arbitraryAssignment nv) $ \m ->
          let ub = SAT.pbLinUpperBound s
           in counterexample (show ub) $ SAT.evalPBLinSum m s <= ub
  
  prop_pbLinLowerBound :: Property
  prop_pbLinLowerBound =
    forAll (choose (0,10)) $ \nv ->
      forAll (arbitraryPBLinSum nv) $ \s ->
        forAll (arbitraryAssignment nv) $ \m ->
          let lb = SAT.pbLinLowerBound s
           in counterexample (show lb) $ lb <= SAT.evalPBLinSum m s
  
  case_pbLinSubsume_clause :: Assertion
  case_pbLinSubsume_clause = SAT.pbLinSubsume ([(1,1),(1,-3)],1) ([(1,1),(1,2),(1,-3),(1,4)],1) @?= True
  
  case_pbLinSubsume_1 :: Assertion
  case_pbLinSubsume_1 = SAT.pbLinSubsume ([(1,1),(1,2),(1,-3)],2) ([(1,1),(2,2),(1,-3),(1,4)],1) @?= True
  
  case_pbLinSubsume_2 :: Assertion
  case_pbLinSubsume_2 = SAT.pbLinSubsume ([(1,1),(1,2),(1,-3)],2) ([(1,1),(2,2),(1,-3),(1,4)],3) @?= False
  
  prop_removeNegationFromPBSum :: Property
  prop_removeNegationFromPBSum =
    forAll (choose (0,10)) $ \nv ->
      forAll (arbitraryPBSum nv) $ \s ->
        let s' = SAT.removeNegationFromPBSum s
         in counterexample (show s') $
              forAll (arbitraryAssignment nv) $ \m -> SAT.evalPBSum m s === SAT.evalPBSum m s'
  
  prop_pbUpperBound :: Property
  prop_pbUpperBound =
    forAll (choose (0,10)) $ \nv ->
      forAll (arbitraryPBSum nv) $ \s ->
        forAll (arbitraryAssignment nv) $ \m ->
          let ub = SAT.pbUpperBound s
           in counterexample (show ub) $ SAT.evalPBSum m s <= ub
  
  prop_pbLowerBound :: Property
  prop_pbLowerBound =
    forAll (choose (0,10)) $ \nv ->
      forAll (arbitraryPBSum nv) $ \s ->
        forAll (arbitraryAssignment nv) $ \m ->
          let lb = SAT.pbLowerBound s
           in counterexample (show lb) $ lb <= SAT.evalPBSum m s
  
  ------------------------------------------------------------------------
  
  case_normalizeXORClause_False :: Assertion
  case_normalizeXORClause_False =
    SAT.normalizeXORClause ([],True) @?= ([],True)
  
  case_normalizeXORClause_True :: Assertion
  case_normalizeXORClause_True =
    SAT.normalizeXORClause ([],False) @?= ([],False)
  
  -- x ⊕ y ⊕ x = y
  case_normalizeXORClause_case1 :: Assertion
  case_normalizeXORClause_case1 =
    SAT.normalizeXORClause ([1,2,1],True) @?= ([2],True)
  
  -- x ⊕ ¬x = x ⊕ x ⊕ 1 = 1
  case_normalizeXORClause_case2 :: Assertion
  case_normalizeXORClause_case2 =
    SAT.normalizeXORClause ([1,-1],True) @?= ([],False)
  
  prop_normalizeXORClause :: Property
  prop_normalizeXORClause = forAll g $ \(nv, c) ->
      let c2 = SAT.normalizeXORClause c
      in flip all (allAssignments nv) $ \m ->
           SAT.evalXORClause m c == SAT.evalXORClause m c2
    where
      g :: Gen (Int, SAT.XORClause)
      g = do
        nv <- choose (0, 10)
        len <- choose (0, nv)
        lhs <- replicateM len $ arbitraryLit nv
        rhs <- arbitrary
        return (nv, (lhs,rhs))
  
  case_evalXORClause_case1 :: Assertion
  case_evalXORClause_case1 =
    SAT.evalXORClause (array (1,2) [(1,True),(2,True)] :: Array Int Bool) ([1,2], True) @?= False
  
  case_evalXORClause_case2 :: Assertion
  case_evalXORClause_case2 =
    SAT.evalXORClause (array (1,2) [(1,False),(2,True)] :: Array Int Bool) ([1,2], True) @?= True
  
  ------------------------------------------------------------------------
  
  satTypesTestGroup :: TestTree
  satTypesTestGroup = $(testGroupGenerator)
  