-- Copyright (C) 2017 Red Hat, Inc.
--
-- This library is free software; you can redistribute it and/or
-- modify it under the terms of the GNU Lesser General Public
-- License as published by the Free Software Foundation; either
-- version 2.1 of the License, or (at your option) any later version.
--
-- This library is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-- Lesser General Public License for more details.
--
-- You should have received a copy of the GNU Lesser General Public
-- License along with this library; if not, see <http://www.gnu.org/licenses/>.

module BDCS.DepsolveSpec(spec)
 where

import           Control.Monad.Except(runExceptT)
import qualified Data.Map as Map
import qualified Data.Set as Set
import           Test.Hspec

import BDCS.Depsolve

{-# ANN module "HLint: ignore Reduce duplication" #-}

spec :: Spec
spec = do
    describe "BDCS.Depsolve.formulaToCNF tests" $ do
        it "atom" $
            formulaToCNF (Atom '1') `shouldBe` [[CNFAtom (CNFOriginal '1')]]

        it "not" $
            formulaToCNF (Not '1') `shouldBe` [[CNFNot (CNFOriginal '1')]]

        it "and" $
            formulaToCNF (And [Atom '1', Atom '2', Atom '3', Atom '4']) `shouldBe` [[CNFAtom (CNFOriginal '1')],
                                                                                    [CNFAtom (CNFOriginal '2')],
                                                                                    [CNFAtom (CNFOriginal '3')],
                                                                                    [CNFAtom (CNFOriginal '4')]]

        it "Or 0 items" $
            formulaToCNF (Or [] :: Formula ()) `shouldBe` ([[]] :: CNFFormula ())

        it "Or 1 item" $
            formulaToCNF (Or [Atom '1']) `shouldBe` [[CNFAtom (CNFOriginal '1')]]

        -- See the comment in formulaToCNF for more detail. In short, for 1 OR 2 OR 3:
        --    start with (1) OR (2 OR 3) ==> (sub 0 -> 1) AND (NOT(sub 0) -> (2 OR 3))
        --    the left half becomes (NOT(sub0) OR 1), which is the first part of the result
        --    the right half becomes (sub0 OR (2 OR 3))
        --    recurse on (2 OR 3), adding sub0 to the front of each result

        it "Or 2 items" $
            formulaToCNF (Or [Atom '1', Atom '2']) `shouldBe` [[CNFNot  (CNFSubstitute 0),
                                                                CNFAtom (CNFOriginal '1')],
                                                               [CNFAtom (CNFSubstitute 0),
                                                                CNFAtom (CNFOriginal '2')]]
        it "Or 3 items" $
            formulaToCNF (Or [Atom '1', Atom '2', Atom '3']) `shouldBe` [[CNFNot  (CNFSubstitute 0),
                                                                          CNFAtom (CNFOriginal '1')],
                                                                         [CNFAtom (CNFSubstitute 0),
                                                                          CNFNot  (CNFSubstitute 1),
                                                                          CNFAtom (CNFOriginal '2')],
                                                                         [CNFAtom (CNFSubstitute 0),
                                                                          CNFAtom (CNFSubstitute 1),
                                                                          CNFAtom (CNFOriginal '3')]]

    describe "BDCS.Depsolve.pureLiteralEliminate tests" $ do
        it "pureLiteralEliminate, empty list" $
            pureLiteralEliminate Set.empty Map.empty ([] :: CNFFormula Char) `shouldBe` Map.empty

        it "already assigned, matches" $ do
            let assignments = Map.singleton (CNFOriginal '1') True
            let formula = [[CNFAtom (CNFOriginal '1')]]
            let solution = assignments
            pureLiteralEliminate Set.empty assignments formula `shouldBe` solution

        it "already assigned, does not match" $ do
            let assignments = Map.singleton (CNFOriginal '1') True
            let formula = [[CNFNot (CNFOriginal '1')]]
            let solution = Map.empty
            pureLiteralEliminate Set.empty assignments formula `shouldBe` solution

        it "pureLiteralEliminate, pure, appears once" $ do
            let assignments = Map.empty
            let formula = [[CNFAtom (CNFOriginal '1')]]
            let solution = Map.singleton (CNFOriginal '1') True
            pureLiteralEliminate Set.empty assignments formula `shouldBe` solution

        it "pure, appears once negative" $ do
            let assignments = Map.empty
            let formula = [[CNFNot (CNFOriginal '1')]]
            let solution = Map.singleton (CNFOriginal '1') False
            pureLiteralEliminate Set.empty assignments formula `shouldBe` solution

        it "pure, appears multiple times" $ do
            let assignments = Map.empty
            let formula = [[CNFAtom (CNFOriginal '1')],
                           [CNFAtom (CNFOriginal '1'),
                            CNFAtom (CNFOriginal '2')],
                           [CNFNot  (CNFOriginal '2')]]
            let solution = Map.singleton (CNFOriginal '1') True
            pureLiteralEliminate Set.empty assignments formula `shouldBe` solution

        it "pure, appears multiple times negative" $ do
            let assignments = Map.empty
            let formula = [[CNFNot  (CNFOriginal '1')],
                           [CNFNot  (CNFOriginal '1'),
                            CNFAtom (CNFOriginal '2')],
                           [CNFNot  (CNFOriginal '2')]]
            let solution = Map.singleton (CNFOriginal '1') False
            pureLiteralEliminate Set.empty assignments formula `shouldBe` solution

        it "unpure" $ do
            let assignments = Map.empty
            let formula = [[CNFAtom (CNFOriginal '1')],
                           [CNFNot  (CNFOriginal '1')]]
            let solution = Map.empty
            pureLiteralEliminate Set.empty assignments formula `shouldBe` solution

        it "unpure 2" $ do
            let assignments = Map.empty
            let formula = [[CNFAtom (CNFOriginal '1'),
                            CNFNot  (CNFOriginal '1')],
                           [CNFNot  (CNFOriginal '1')]]
            let solution = Map.empty
            pureLiteralEliminate Set.empty assignments formula `shouldBe` solution

    describe "BDCS.Depsolve.unitPropagate tests" $ do
        it "empty list" $
            runExceptT (unitPropagate Map.empty ([] :: CNFFormula Char)) >>=
                (`shouldBe` Right (Map.empty, []))

        it "one thing" $
            runExceptT (unitPropagate Map.empty [[CNFAtom (CNFOriginal '1')]]) >>=
                (`shouldBe` Right (Map.singleton (CNFOriginal '1') True, []))

        it "unit then elimate clause" $ do
            let assignments = Map.empty
            let formula = [[CNFAtom (CNFOriginal '1')],
                           [CNFAtom (CNFOriginal '1'),
                            CNFNot  (CNFOriginal '2')]]
            let assignments' = Map.singleton (CNFOriginal '1') True
            let formula' = []
            runExceptT (unitPropagate assignments formula) >>= (`shouldBe` Right (assignments', formula'))

        it "unit then elimate impossible" $ do
            let assignments = Map.empty
            let formula = [[CNFAtom (CNFOriginal '1')],
                           [CNFAtom (CNFOriginal '2'),
                            CNFNot  (CNFOriginal '1')]]
            let assignments' = Map.singleton (CNFOriginal '1') True
            let formula' = [[CNFAtom (CNFOriginal '2')]]
            runExceptT (unitPropagate assignments formula) >>= (`shouldBe` Right (assignments', formula'))

        it "unit then repeated" $ do
            let assignments = Map.empty
            let formula = [[CNFAtom (CNFOriginal '1')],
                           [CNFAtom (CNFOriginal '1')]]
            let assignments' = Map.singleton (CNFOriginal '1') True
            let formula' = []
            runExceptT (unitPropagate assignments formula) >>= (`shouldBe` Right (assignments', formula'))

        it "unit then unsolvable unit" $ do
            let assignments = Map.empty
            let formula = [[CNFAtom (CNFOriginal '1')],
                           [CNFNot  (CNFOriginal '1')]]
            runExceptT (unitPropagate assignments formula) >>= (`shouldBe` Left "Unable to solve expression")

        it "units then unsolvable clause" $ do
            let assignments = Map.empty
            let formula = [[CNFAtom (CNFOriginal '1')],
                           [CNFAtom (CNFOriginal '2')],
                           [CNFNot  (CNFOriginal '1'),
                            CNFNot  (CNFOriginal '2')]]
            runExceptT (unitPropagate assignments formula) >>= (`shouldBe` Left "Unable to solve expression")

    describe "BDCS.Depsolve.solveCNF tests" $ do
        it "empty formula" $ do
            let formula = [] :: (CNFFormula Char)
            let solution = [] :: [DepAssignment Char]
            runExceptT (solveCNF formula) >>= (`shouldBe` Right solution)

        it "singleton" $ do
            let formula = [[CNFAtom (CNFOriginal '1')]]
            let solution = [('1', True)]
            runExceptT (solveCNF formula) >>= (`shouldBe` Right solution)