content: {-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TemplateHaskell #-}
  module Test.QBF (qbfTestGroup) where
  
  import Control.Monad
  import qualified Data.IntSet as IntSet
  import Data.IntMap (IntMap)
  import qualified Data.IntMap as IntMap
  import Data.Maybe (catMaybes)
  
  import Test.Tasty
  import Test.Tasty.QuickCheck hiding ((.&&.), (.||.))
  import Test.Tasty.TH
  import qualified Test.QuickCheck.Monadic as QM
  
  import ToySolver.Data.Boolean
  import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
  import qualified ToySolver.QBF as QBF
  
  import Test.SAT.Utils (arbitraryLit)
  
  -- -------------------------------------------------------------------
  
  prop_solveCEGAR :: Property
  prop_solveCEGAR = QM.monadicIO $ do
    (nv, prefix@(_ : prefix'), matrix) <- QM.pick arbitrarySmallQBF
    (sat, cert) <- QM.run $ QBF.solveCEGAR nv prefix matrix
    QM.assert $ sat == evalQBFNaive prefix matrix
    case cert of
      Nothing -> return ()
      Just ls ->
        QM.assert $ sat == evalQBFNaive' (IntMap.fromList [(abs lit, lit > 0) | lit <- IntSet.toList ls]) prefix' matrix
  
  prop_solveCEGARIncremental :: Property
  prop_solveCEGARIncremental = QM.monadicIO $ do
    (nv, prefix@(_ : prefix'), matrix) <- QM.pick arbitrarySmallQBF
    (sat, cert) <- QM.run $ QBF.solveCEGARIncremental nv prefix matrix
    QM.assert $ sat == evalQBFNaive prefix matrix
    case cert of
      Nothing -> return ()
      Just ls ->
        QM.assert $ sat == evalQBFNaive' (IntMap.fromList [(abs lit, lit > 0) | lit <- IntSet.toList ls]) prefix' matrix
  
  prop_solveQE :: Property
  prop_solveQE = QM.monadicIO $ do
    (nv, prefix@(_ : prefix'), matrix) <- QM.pick arbitrarySmallQBF
    (sat, cert) <- QM.run $ QBF.solveQE nv prefix matrix
    QM.assert $ sat == evalQBFNaive prefix matrix
    case cert of
      Nothing -> return ()
      Just ls ->
        QM.assert $ sat == evalQBFNaive' (IntMap.fromList [(abs lit, lit > 0) | lit <- IntSet.toList ls]) prefix' matrix
  
  {-
  If the innermost quantifier is a universal quantifier,
  we can remove the bound variable v from the clauses that
  do not contain v and ¬v simultaneously.
  -}
  prop_eliminate_last_universal_quantifier :: Property
  prop_eliminate_last_universal_quantifier = QM.monadicIO $ do
    (nv, prefix, matrix1) <- QM.pick gen
    let (QBF.A, xs) = last prefix
        matrix2 = [[lit | lit <- clause, abs lit `IntSet.notMember` xs] | clause <- matrix1]
        matrix1' = andB [orB [f lit | lit <- clause] | clause <- matrix1]
        matrix2' = andB [orB [f lit | lit <- clause] | clause <- matrix2]
        f lit = if lit > 0
                then QBF.litToMatrix lit
                else notB (QBF.litToMatrix (abs lit))
    (sat1, _cert1) <- QM.run $ QBF.solveCEGAR nv prefix matrix1'
    (sat2, _cert2) <- QM.run $ QBF.solveCEGAR nv (init prefix) matrix2'
    QM.assert $ sat1 == sat2
    where
      gen :: Gen (Int, QBF.Prefix, [[Int]])
      gen = do
        nv <- choose (0,10)
        nc <- choose (0,50)
        let vs = [1..nv]
        q1 <- arbitrary
        q2 <- arbitrary
        vs1 <- IntSet.fromList <$> subsetof vs
        vs2 <- IntSet.fromList <$> subsetof vs
        matrix <- replicateM nc $ do
          if nv == 0 then
            return []
          else do
            mapM (\v -> elements [v, -v]) =<< subsetof vs
        return
          ( nv
          , [(q1,vs1), (q2, vs2 IntSet.\\ vs1), (QBF.A, IntSet.fromList vs IntSet.\\ (vs1 `IntSet.union` vs2))]
          , matrix
          )
  
  -- -------------------------------------------------------------------
  
  evalQBFNaive :: QBF.Prefix -> QBF.Matrix -> Bool
  evalQBFNaive prefix = evalQBFNaive' IntMap.empty prefix
  
  evalQBFNaive' :: IntMap Bool -> QBF.Prefix -> QBF.Matrix -> Bool
  evalQBFNaive' env prefix = f env [(q,v) | (q,vs) <- prefix, v <- IntSet.toList vs]
    where
      f env [] matrix = Tseitin.fold (env IntMap.!) matrix
      f env ((QBF.A,x) : prefix) matrix =
        f (IntMap.insert x True  env) prefix matrix &&
        f (IntMap.insert x False env) prefix matrix
      f env ((QBF.E,x) : prefix) matrix =
        f (IntMap.insert x True  env) prefix matrix ||
        f (IntMap.insert x False env) prefix matrix
  
  -- -------------------------------------------------------------------
  
  subsetof :: [a] -> Gen [a]
  subsetof xs = catMaybes <$> sequence [elements [Just x, Nothing] | x <- xs]
  
  arbitrarySmallQBF :: Gen (Int, QBF.Prefix, QBF.Matrix)
  arbitrarySmallQBF = do
    (nv, prefix, matrix') <- arbitrarySmallQBF'
    let f lit = if lit > 0
                then QBF.litToMatrix lit
                else notB (QBF.litToMatrix (abs lit))
        matrix = andB [orB [f lit | lit <- clause] | clause <- matrix']
    return (nv, prefix, matrix)
  
  arbitrarySmallQBF' :: Gen (Int, QBF.Prefix, [[Int]])
  arbitrarySmallQBF' = do
    nv <- choose (0,10)
    nc <- choose (0,50)
  
    let vs = [1..nv]
    q1 <- arbitrary
    q2 <- arbitrary
    q3 <- arbitrary
    vs1 <- IntSet.fromList <$> subsetof vs
    vs2 <- IntSet.fromList <$> subsetof vs
  
    matrix <- replicateM nc $ do
      len <- choose (0,10)
      if nv == 0 then
        return []
      else
        replicateM len $ arbitraryLit nv
  
    return
      ( nv
      , [(q1,vs1), (q2, vs2 IntSet.\\ vs1), (q3, IntSet.fromList vs IntSet.\\ (vs1 `IntSet.union` vs2))]
      , matrix
      )
  
  instance Arbitrary QBF.Quantifier where
    arbitrary = arbitraryBoundedEnum
  
  -- -------------------------------------------------------------------
  -- Test harness
  
  qbfTestGroup :: TestTree
  qbfTestGroup = $(testGroupGenerator)
  