{-
How to use:

$ pakcs :load testSat.curry :add SatDef Sat
... if no error ...
testSat Sat SatDef> main
... it runs tests ...
-}

import Control.Search.SetFunctions
import qualified Data.Map as Map
import Data.Map (Map)
import System.IO.Unsafe (isVar)
import TestLib
import SatDef
import Sat

p0, p1 :: P String
a1 :: [[(String, Bool)]]

p0 = Not (Var "x") :&: Var "y" :&: (Var "x" :|: Not (Var "y")) 
-- Unsatisfiable.

p1 = (Var "x" :|: Var "y") :&: (Var "x" :|: Not (Var "y"))
-- Two ways to satisfy:
a1 = [[("x",True),("y",False)],[("x",True),("y",True)]]

valTests :: [Test]
valTests =
    [ "val p0" ~: val e p0 ~?= False
    , "val p1" ~: val e p1 ~?= True
    ]
  where
    e = Map.fromList [("x",True),("y",False)]

-- Like mkEnv but output [(var,bool)].
mkEnvList :: P String -> [(String,Bool)]
mkEnvList p = map inst (Map.toList (mkEnv p))

testMkEnv :: P String -> [[(String,Bool)]]
testMkEnv p = sortValues (set1 mkEnvList p)

mkEnvTests :: [Test]
mkEnvTests =
    [ "mkEnv p0" ~: testMkEnv p0 ~?= [[("x",False),("y",False)],
                                      [("x",False),("y",True)],
                                      [("x",True),("y",False)],
                                      [("x",True),("y",True)]]
    ]

-- Like sat but output [(var,bool)].
satList :: P String -> [(String,Bool)]
satList p = map inst (Map.toList (sat p))

-- Deeply magical instantiating unknowns to both False and True.
-- For testing mkEnv and sat, in case you use the smart way.
inst :: (a,Bool) -> (a,Bool)
inst a@(_,b) = seq (isVar b && b =:= (False ? True)) a

-- Like sat but collect all solutions for testing.
testSat :: P String -> [[(String,Bool)]]
testSat p = sortValues (set1 satList p)

satTests :: [Test]
satTests = [ "unsatisfiable" ~: testSat p0 ~?= []
           , "satisfiable" ~: testSat p1 ~?= a1
           ]

tests :: [Test]
tests = [Group valTests, Group mkEnvTests, Group satTests]

main :: IO ()
main = testlibMain tests