-- | @HUnit@-based unit tests for @ersatz@.
module Main where

import Prelude hiding ((||), (&&), not)

import Data.Default
import qualified Data.IntMap.Strict as IntMap

import Test.Tasty (TestTree, defaultMain, testGroup)
import Test.Tasty.HUnit (Assertion, (@?=), testCase)

import Ersatz
import Ersatz.Internal.Literal

main :: IO ()
main = defaultMain tests

tests :: TestTree
tests =
  testGroup "unit tests"
    [ testCase "unconstrained literals" case_unconstrained_literals
    ]

-- A regression test for #60 and #76.
case_unconstrained_literals :: Assertion
case_unconstrained_literals =
    decode sol [b1, not b1, b2, not b2, b1 || b2, b1 && b2] @?=
      Just [False, True, False, True, False, False]
      -- There are other valid answers, but in practice, ersatz will choose this
      -- one due to the convention that the Codec Literal instance always
      -- assigns non-negative unconstrained Literals to False and negative
      -- unconstrained Literals to True.
  where
    sol = solutionFrom (IntMap.fromList [(1, True)]) (def :: SAT)
    b1 = Var $ Literal 2
    b2 = Var $ Literal 3