open CoolUtils
open Testsuite
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]) |]

(* ============ multi modal K ============ *)
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"
    ]

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 testcases =
    let c name table = (name,table) in
    [ c "K"  k_testcases
    ; c "KD" kd_testcases
    ]

let main =
    foreach_l testcases (fun (name,table) ->
        Printf.printf "\n==== Testing logic %s ====\n" name;
        foreach_l table runSatCheckVerbose
    )

let _ = main