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

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))"

    (* Some DL98-Testcases *)
    ]


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 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
    ]

let main =
    let success = ref 0 in
    let failed = ref 0 in
    foreach_l testcases (fun (name,table) ->
        Printf.printf "==== Testing %s ====\n" name;
        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