import Test.QuickCheck
import System.Random

import Rewriting hiding (Var)
import Logic.Formula
import Logic.Rules
import Logic.Strategies hiding (main)

{-
real    0m1.720s
user    0m1.569s
sys     0m0.077s
-}
killer1 = (Var "q" :<->: F) :||: (T :->: Var "p") :<->: ((Var "r" :<->: Var "p") :<->: (Var "q" :<->: Var "p"))

{-
real    0m2.704s
user    0m2.472s
sys     0m0.138s
-}
killer2 = ((Var "q" :<->: T) :<->: (T :<->: Var "q")) :<->: (Var "q" :||: Var "p" :<->: (Var "p" :<->: Var "q"))

{-
real    0m27.321s
user    0m25.806s
sys     0m1.189s
-}
killer3 = ((Var "r" :<->: Var "r") :<->: (Var "r" :<->: Var "r")) :<->: (Var "q" :&&: Var "p" :<->: Var "r")

main = do
  print (propSound killer3)

-- The samples below were obtained with |check custom propSound|

custom :: Config
custom = Config
  { configMaxTest = 10
  , configMaxFail = 1000
  , configSize    = (+ 3) . (`div` 2)
  , configEvery   = \n args -> show n ++ ":\n" ++ unlines args
  }

{-

0:
Var "q" :<->: Var "r"
1:
Var "r"
2:
Not (Var "p") :->: (T :<->: Var "r")
3:
(Var "q" :<->: F) :||: (T :->: Var "p") :<->: ((Var "r" :<->: Var "p") :<->: (Var "q" :<->: Var "p"))
4:
(T :||: Var "r") :||: (Var "p" :<->: T)
5:
Var "p"
6:
(Var "q" :<->: Var "p") :||: Var "p"
7:
Var "r" :&&: F
8:
(Var "q" :<->: F) :||: Var "q" :<->: (Var "r" :<->: Var "r") :||: F
9:
Not (Var "q") :||: T :&&: T :<->: Var "q" :||: (Var "q" :->: Var "p")
OK, passed 10 tests.

real    0m1.643s
user    0m1.562s
sys     0m0.068s
-}

{-
0:
Var "r"
1:
Var "p"
2:
((F :<->: T) :->: (Var "r" :<->: T)) :&&: Not (Var "q" :->: T)
3:
(Var "q" :||: Var "p") :&&: Not (Var "q")
4:
Var "q" :&&: Var "p" :||: (Var "p" :<->: Var "q") :<->: Not (Var "r" :&&: Var "p")
5:
(F :||: Var "p") :||: Not (Var "q")
6:
((Var "q" :<->: T) :<->: (T :<->: Var "q")) :<->: (Var "q" :||: Var "p" :<->: (Var "p" :<->: Var "q"))
7:
(T :<->: Var "p") :<->: (Var "r" :<->: Var "p")
8:
Var "q"
9:
Var "r"
OK, passed 10 tests.

real    0m2.683s
user    0m2.528s
sys     0m0.132s

-}

{-
0:
T
1:
(Var "q" :->: Var "p") :->: (Var "q" :<->: Var "p")
2:
((T :<->: Var "r") :<->: F) :&&: ((Var "r" :<->: T) :||: (Var "p" :||: T))
3:
Var "p" :&&: Var "r"
4:
T
5:
T :||: ((Var "q" :<->: Var "r") :||: Not (Var "p"))
6:
((Var "r" :<->: Var "r") :<->: (Var "r" :<->: Var "r")) :<->: (Var "q" :&&: Var "p" :<->: Var "r")
7:
Var "r" :||: Var "q" :->: (Var "p" :<->: T)
8:
Not (Not (Var "q") :<->: (Var "p" :<->: F))
9:
Var "q"
OK, passed 10 tests.

real    0m27.170s
user    0m25.710s
sys     0m1.173s
-}