open CoolUtils
open Testsuite
module DL98 = DL98TestCases
module CF = CoAlgFormula
module CR = CoAlgReasoner
module CM = CoAlgMisc
module L = List
module FP = FunctorParsing

let k   = [| (CM.MultiModalK,  [0]) |]
let kd  = [| (CM.MultiModalKD, [0]) |]
let cl  = [| (CM.CoalitionLogic, [0]) |]
let gml = [| (CM.GML, [0]) |]

let k_testcases: satCheck list =
    let c a b = (a,k,b) in
    [ c Sat   "True"
    ; c Unsat "False"
    ; c ParseError  "{Fsdf"
    (*; c ParseError  "Fsdf}" *)
    ; c Unsat "<R> True & [R] False"
    ; c Unsat "C |- <R> ~C"
    ; c Sat   "C |- [R] ~C"
    ; c Unsat "<R> ((<R> C) & (<S> False))"
    ; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
    ; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
    ; c Sat   "<R> A & <R> B |- [R] C"
    ; c Unsat "<R> A & <R> B |- [R] (~A & ~B)"
    ; c Unsat "<R> A & <R> B |- [R] ~B"
    ; c Sat   "<R> A & <R> ~A |- [R] B"
    ; c Unsat "<R> A & <R> ~A & (B => [R] ~A) |- [R] B"
    ; c Sat   "<R> A & <R> ~A & (B => [R] ~A) & (C => ~D) & (D => ~E) & <R> C & <R> D & <R> E |- True"
    ; c Unsat "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
    ; c Sat   "(<R> D | <R> E) & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
    ; c Sat   "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & (D & E => <R> ~(D&E)) |- True"
    ]


let nominal_testcases =
    let c a b = (a,k,b) in
    [ c Sat "@ i' <r> p"
    ; c Sat "@ i' <r>  i'"
    ; c Unsat "@ i' <r>  i' & @i' [r] ~ i'"
    ; c Sat "@ i' [r] (@ i' (~i')) "
    ]

let kd_testcases =
    let c a b = (a,kd,b) in
    [ c Sat   "True"
    ; c Unsat "False"
    ; c ParseError  "{Fsdf"
    (*; c ParseError  "Fsdf}" *)
    ; c Unsat "<R> True & [R] False"
    ; c Unsat "C |- <R> ~C"
    ; c Unsat "C |- [R] ~C"
    ]

let cl_testcases : satCheck list =
    let c a b = (a,cl,b) in
    [ c Unsat "[{1}] C & [{ 2 }] ~C"
    ; c Sat   "[{1}] C & <{ 2 }> ~C"
    ; c Unsat "[{1}] C & <{ 1 2 }> ~C"
    ; c Sat   "<{ 1 2 }> C & <{ 1 2 }> ~C"
    ; c Unsat "<{ 1 2 }> C & [{ 1 2 }] ~C"
    ; c Sat   "([{1 3}] C) & ([{ 2 3 }] ~C )"
    ]

let kAndKd = FunctorParsing.sortTableFromString "K * KD"

let kAndKd_testcases : satCheck list =
    let c a b = (a,kAndKd,b) in
    [ c Sat   "[pi1]True"
    ; c Sat   "[pi1][R]False"
    ; c Unsat "[pi2][R]False"
    ; c Sat   "i' => [pi1][R] i'"
    ; c Sat   "i' & [pi1][R] i'"
    ; c Unsat "i' => [pi2][R] (~i') |- i' & [pi2] [R] i'"
    ]

let kOrKd = [| (CoAlgMisc.Choice, [1; 2]);
               (CoAlgMisc.MultiModalK, [0]);
               (CoAlgMisc.MultiModalKD, [0])
            |]
let kOrKd_testcases : satCheck list =
    let c a b = (a,kOrKd,b) in
    [ c Sat   "( True + False )"
    ; c Sat   "(([R] False) + ([R] False))"
    ; c Unsat "((False) + ([R] False))"
    ]

let testcases =
    let c name table = (name,table) in
    [ c "DL98 (Sat)"    DL98.satCasesList
    ; c "DL98 (Unsat)"  DL98.unsatCasesList
    ; c "K"  k_testcases
    ; c "Nominals" nominal_testcases
    ; c "KD" kd_testcases
    ; c "CL" cl_testcases
    ; c "K*KD" kAndKd_testcases
    ; c "K+KD" kOrKd_testcases
    ]

let main =
    let success = ref 0 in
    let failed = ref 0 in
    foreach_l testcases (fun (name,table) ->
        Printf.printf "==== Testing %s ====\n" name;
        let (_,sorts,_) = List.hd table in
        Printf.printf "sortTable = %s\n" (FP.stringFromSortTable sorts);
        foreach_l table (fun sc ->
            let (expected,_,_) = sc in
            let actual = runSatCheckVerbose sc in
            (* compare the expected and the actual result *)
            if actual = expected
            then success := !success + 1
            else failed := !failed + 1
        );
        Printf.printf "\n"
    );
    let s n = if n = 1 then "testcase" else "testcases" in
    Printf.printf "=> %d %s succeeded, %d %s failed.\n"
        !success (s !success)
        !failed (s !failed)

let _ = main