CoAlgMisc.ml

(** Common types, functions, and data structures for the CoAlgebraic reasoner.
    @author Florian Widmann
 *)


module S = 
MiscSolver
module L = List
module C = CoAlgFormula
module HC = HashConsing


(** An instantiation of a set (of the standard library) for bitsets.
 *)
module BsSet = Set.Make(
  struct
    type t = S.bitset
    let (compare : t -> t -> int) = S.compareBS
  end
 )

(** An instantiation of a hash table (of the standard library) for bitsets.
 *)
module GHt = Hashtbl.Make(
  struct
    type t = S.bitset * S.bitset
    let equal ((bs1l, bs1r) : t) (bs2l, bs2r) =
      (S.compareBS bs1l bs2l = 0) && (S.compareBS bs1r bs2r = 0)
    let hash ((bsl, bsr) : t) = (S.hashBS bsl) lxor (S.hashBS bsr)
  end
 )

(** An instantiation of a hash table (of the standard library) for bitsets.
 *)
module GHtS = Hashtbl.Make(
  struct
    type t = S.bitset
    let equal (bs1 : t) bs2 = S.compareBS bs1 bs2 = 0
    let hash (bs : t) = S.hashBS bs
  end
 )

(** An instantiation of a hash table (of the standard library) for literals.
 *)
module LHt = Hashtbl.Make(
  struct
    type t = Minisat.lit
    let equal (l1 : t) l2 = l1 = l2
    let hash (l : t) = (l :> int)
  end
 )

(** An instantiation of a hash table (of the standard library) for formulae.
 *)
module FHt = Hashtbl.Make(
  struct
    type t = int
    let equal (f1 : t) f2 = f1 = f2
    let hash (f : t) = f
  end
 )

(** An instantiation of a hash table (of the standard library) for nominals.
 *)
module NHt = Hashtbl.Make(
  struct
    type t = int * int
    let equal ((s1, f1) : t) (s2, f2) = (s1 = s2) && (f1 = f2)
    let hash ((s, f) : t) = (((s+f)*(s+f+1)) / 2) + f
  end
)


(*****************************************************************************)
(*     Types that can be modified rather easily                              *)
(*     (of course you then have to modify the implementations below too)     *)
(*****************************************************************************)

(* This type must be extended for additional logics. *)
type functors =
  | MultiModalK
  | MultiModalKD
  | Monotone
  | MultiModalM
  | CoalitionLogic
  | GML
  | PML
  | Constant of string list
  | Identity
  | DefaultImplication
  | Choice
  | Fusion

(* functors whose constructor takes additional parameters *)
type parametricFunctorName =
  | NameConstant

(* this type should only be used in the following few helper functions *)
type functorName =
  | NPa of functors (* No Parameters = functor without parameters *)
  | Pa  of parametricFunctorName (* Parameters = functor with parameters *)

let unaryfunctor2name : (functorName*string) list =
  [ (NPa MultiModalK , "MultiModalK")
  ; (NPa MultiModalKD , "MultiModalKD")
  ; (NPa Monotone , "Monotone")
  ; (NPa MultiModalM , "MultiModalM")
  ; (NPa GML ,           "GML")
  ; (NPa PML ,           "PML")
  ; (NPa CoalitionLogic , "CoalitionLogic")
  ; (NPa MultiModalK , "K")
  ; (NPa MultiModalKD , "KD")
  ; (NPa MultiModalM , "M")
  ; (NPa CoalitionLogic , "CL")
  ; (Pa  NameConstant , "Const")
  ; (Pa  NameConstant , "Constant")
  ; (NPa Identity, "Id")
  ; (NPa Identity, "Identity")
  ]

let functor2name : (functorName*string) list =
  L.append unaryfunctor2name
  [ (NPa Choice , "Choice")
  ; (NPa Fusion , "Fusion")
  ]

let functor_apply_parameters (func : parametricFunctorName) (params: string list) : functors option =
    (* apply parameter list to the constructor, denoted by the functor name func *)
    (* return None, if the parameters somehow don't match the required parameters *)
    match func with
    | NameConstant -> Some (Constant params)


let functor_of_string str params : functors option =
    let fst (a,b) = a in
    try
        let functorName = fst (List.find (fun (f,name) -> name = str) functor2name) in
        match functorName with
        | NPa x -> Some x
        | Pa f -> functor_apply_parameters f params
    with Not_found -> None

let unaryfunctor_of_string str params =
    match (functor_of_string str params) with
    | Some Choice -> None
    | Some Fusion -> None
    | x -> x

let string_of_functor (f: functors) : string =
    (* replace f orrectly with possibly some Pa wrapper *)
    (* also put the parameters into some suffix which will be appended later *)
    let f,suffix = match f with
            | Constant params -> Pa NameConstant, " "^(String.concat " " params)
            | _ -> NPa f, ""
    in
    let snd (a,b) = b in
    try
        let name = snd (List.find (fun (f2,name) -> f = f2) functor2name) in
        name ^ suffix
    with Not_found -> assert false

(* This type may be extended for additional logics. *)
type formulaType =
  | Other
  | TrueFalseF (* constant true or false *)
  | AndF
  | OrF
  | AtF
  | NomF
  | ExF  (* Existential / diamond *)
  | AxF  (* Universal / box *)
  | EnforcesF (* diamond of CL *)
  | AllowsF   (* box of CL *)
  | MoreThanF (* more than n successors = diamond in gml *)
  | MaxExceptF(* at most n exceptions = box in gml *)
  | AtLeastProbF (* for PML *)
  | LessProbFailF (* box for PML *)
  | ConstF (* constant functor *)
  | ConstnF (* constant functor *)
  | IdF (* Identity functor *)
  | NormF (* Default Implication *)
  | NormnF (* negation normal form of default implication *)
  | ChcF (* Choice *)
  | FusF (* Fusion *)
  | MuF
  | NuF

type localFormula = int
type bset = S.bitset

type atFormula = int
type cset = S.bitset
type csetSet = BsSet.t

type lht = localFormula LHt.t
type fht = Minisat.lit FHt.t
type nht = bset NHt.t

type state = { sortS : sort;
               mutable bsS : bset; (* a set of formulas who are either literals or
                                      modalities (TODO: also @-formulas?).
                                      the state is satisfiable if /\bsS is satisfiable.
                                    *)
               mutable deferralS : bset; (* which formulas still have deferrals *)
               mutable statusS : nodeStatus;
               mutable parentsS : core list; mutable childrenS : (dependencies * core list) list;
               mutable constraintsS : csetSet; expandFkt : stateExpander;
               idx: int }

and core = { (* for details, see documentation of newCore *)
             sortC : sort;
             mutable bsC : bset; (* a set of arbitrary formulas.
                                    the present core is satisfiable if /\ bsC is satisfiable *)
             mutable deferralC : bset; (* which formulas still have deferrals *)
             mutable statusC : nodeStatus;
             mutable parentsC : (state * int) list;
             mutable childrenC : state list;
             mutable constraintsC : csetSet;
             mutable solver : Minisat.solver option; (* a solver to find satisfying assignemnts for bsC.
                                         the solver returns "satisfiable" iff
                                         there is a satisfying assignment of
                                         bsC which is not represented by some state from the
                                         childrenC yet.
                                       *)
             fht : fht; (* mapping of boolean subformulas of bsC to their corresponding literals
                           of the Minisat solver
                         *)
             mutable constraintParents : cset list;
             idx : int }

and setState = state GHt.t array

and setCore = core GHt.t array

and setCnstr = unit GHtS.t


(*****************************************************************************)
(*                Types that are hard coded into the algorithm               *)
(*****************************************************************************)

and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
                  | Conjunctive of 'a (*specifies that all of the 'a need  to be satifsfied *)

and stateExpander = rule lazylist

and sort = C.sort

and nodeStatus =
  | Expandable
  | Open
  | Sat
  | Unsat

(* In K, given the singleton list [bs] returns the list of all Ax'es
   responsible for the individual members of bs being part of the core
   as well as the Ex.

   So given the state { <>φ , []ψ , []η } and the core { φ , ψ , η },
   dependency would map { η } to { <>φ , []η } and { ψ } to { <>φ , []ψ }
*)
and dependencies = bset list -> bset

(* Note: sort * bset * bset is to be read as sort * formulas_in_core * deferrals_in_core *)
and rule = (dependencies * (sort * bset * bset) lazylist)

and 'a lazyliststep =
  | MultipleElements of 'a list
  | SingleElement    of 'a
  | NoMoreElements

and 'a lazylist = unit -> 'a lazyliststep

and ruleEnumeration = rule lazyliststep

let nodeStatusToString : nodeStatus -> string = function
  | Expandable -> "Expandable"
  | Open -> "Open"
  | Sat -> "Sat"
  | Unsat -> "Unsat"

let lazylistFromList a_list =
    let list_state = ref (Some a_list) in
    fun () -> begin match !list_state with
              | Some (a_list) -> begin
                    list_state := None;
                    MultipleElements a_list
                end
              | None -> NoMoreElements
              end

let rec listFromLazylist evalfunc =
    let step = evalfunc () in
    match step with
    | NoMoreElements -> []
    | SingleElement x -> x::(listFromLazylist evalfunc)
    | MultipleElements xs -> List.append xs (listFromLazylist evalfunc)

type nominal = sort * localFormula

type node =
  | State of state
  | Core of core

type constrnt =
  | UnsatC
  | SatC
  | OpenC of node list
  | UnexpandedC of node list

type propagateElement =
  | UState of state * int option
  | UCore of core * bool
  | UCnstr of cset

type queueElement =
  | QState of state
  | QCore of core
  | QCnstr of cset
  | QEmpty

type sortTable = (functors * int list) array

exception CoAlg_finished of bool


let sortTable = ref (Array.make 0 (MultiModalK, [1]))

let junctionEvalBool : (bool list junction) -> bool = function
    | Disjunctive l -> List.fold_right (||) l false
    | Conjunctive l -> List.fold_right (&&) l true

let junctionEval (f: 'a -> bool) : 'a list junction -> bool = function
    | Disjunctive l -> List.fold_right (fun x y -> (f x) || y) l false
    | Conjunctive l -> List.fold_right (fun x y -> (f x) && y) l true

let optionalizeOperator (f: 'a -> 'b -> 'c) (x: 'a option) (y: 'b option) : 'c option =
    match x with
    | None -> None
    | Some x -> (match y with
                 | None -> None
                 | Some y -> Some (f x y))

let junctionEvalBoolOption : bool option list junction -> bool option =
    let f extreme op x y = (* ensure that: (Some True) || None = Some True *)
        if x = extreme || y = extreme
        then extreme
        else optionalizeOperator op x y
    in function
    | Disjunctive l ->
        List.fold_right (f (Some true)  (||)) l (Some false)
    | Conjunctive l ->
        List.fold_right (f (Some false) (&&)) l (Some true)

let junctionExtract : 'a junction -> ('a * ('b -> 'b junction)) = function
    | Disjunctive l -> (l, fun x -> Disjunctive x)
    | Conjunctive l -> (l, fun x -> Conjunctive x)

(*****************************************************************************)
(*      "Module type" and a specific implementation of the main queue        *)
(*****************************************************************************)

let queueStates = ref ([] : state list)
let queueCores1 = ref ([] : core list)
let queueCores2 = ref ([] : core list)
let queueCnstrs = ref ([] : cset list)
let doPropagation = ref false
let doPropagationCounter = ref 0

let queueInit () =
  queueStates := [];
  queueCores1 := [];
  queueCores2 := [];
  queueCnstrs := [];
  doPropagation := false

let queueIsEmpty () =
  !queueStates = [] && !queueCores1 = [] && !queueCores2 = [] && !queueCnstrs = []

let queueInsertState state = queueStates := state::!queueStates

(* original version: breadth-first *)
let queueInsertCore core = queueCores2 := core::!queueCores2

(* experiment: depth first
let queueInsertCore core = queueCores1 := core::!queueCores1
*)

let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs

let queueGetElement () =
  if !queueCnstrs <> [] then
    let res = List.hd !queueCnstrs in
    queueCnstrs := List.tl !queueCnstrs;
    QCnstr res
  else if !queueStates <> [] then
    let res = List.hd !queueStates in
    queueStates := List.tl !queueStates;
    QState res
  else if !queueCores1 <> [] then
    let res = List.hd !queueCores1 in
    queueCores1 := List.tl !queueCores1;
    QCore res
  else if !queueCores2 = [] then QEmpty
  else
    let res = List.hd !queueCores2 in
    doPropagation := true;
    queueCores1 := List.tl !queueCores2;
    queueCores2 := [];
    QCore res

let doNominalPropagation () = !doPropagation

let setPropagationCounter count =
  doPropagationCounter := count

let doSatPropagation () =
  if !doPropagationCounter == 0
  then true
  else begin
      doPropagationCounter := !doPropagationCounter - 1;
      false
    end
  (* let res = !doPropagation in *)
  (* doPropagation := false; *)
  (* res *)

(*****************************************************************************)
(*        "Module type" and a specific implementation of the graph           *)
(*****************************************************************************)

let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t)
let graphRoot = ref (None : core option)

let graphInit () =
  let size = Array.length !sortTable in
  graphStates := Array.init size (fun _ -> GHt.create 128);
  graphCores := Array.init size (fun _ -> GHt.create 128);
  graphCnstrs := GHtS.create 128;
  graphRoot := None

let graphIterStates fkt =
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates

let graphIterCores fkt =
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores

let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs

let graphClearCnstr () =
  let newGraph = GHtS.create (GHtS.length !graphCnstrs) in
  let copyCnstr cset cnstr =
    match cnstr with
    | UnsatC
    | SatC -> GHtS.add newGraph cset cnstr
    | OpenC _ -> GHtS.add newGraph cset (OpenC [])
    | UnexpandedC _ -> GHtS.add newGraph cset (UnexpandedC [])
  in
  GHtS.iter copyCnstr !graphCnstrs;
  graphCnstrs := newGraph

let graphFindState sort bs =
  try
    Some (GHt.find !graphStates.(sort) bs)
  with Not_found -> None

let graphFindCore sort bs =
  try
    Some (GHt.find !graphCores.(sort) bs)
  with Not_found -> None

let graphFindCnstr cset =
  try
    Some (GHtS.find !graphCnstrs cset)
  with Not_found -> None

let graphInsertState sort bs state =
  assert (not (GHt.mem !graphStates.(sort) bs));
  GHt.add !graphStates.(sort) bs state

let graphDeleteState sort state =
  GHt.remove !graphStates.(sort) state

let graphInsertCore sort bs core =
  assert (not (GHt.mem !graphCores.(sort) bs));
  GHt.add !graphCores.(sort) bs core

let graphDeleteCore sort core =
  GHt.remove !graphCores.(sort) core

let graphInsertCnstr cset cnstr =
  assert (not (GHtS.mem !graphCnstrs cset));
  GHtS.add !graphCnstrs cset cnstr

let graphReplaceCnstr cset cnstr =
  GHtS.replace !graphCnstrs cset cnstr

let graphSizeState () =
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates
let graphSizeCore () =
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores
let graphSizeCnstr () = GHtS.length !graphCnstrs

let graphAddRoot core =
  if !graphRoot = None then graphRoot := Some core
  else raise (C.CoAlgException "Root of graph is already set.")

let graphGetRoot () =
  match !graphRoot with
  | None -> raise (C.CoAlgException "Root of graph is not set.")
  | Some core -> core


(*****************************************************************************)
(*     "Module type" and a specific implementation of sets of constraints    *)
(*****************************************************************************)

let cssEmpty = BsSet.empty
let cssExists fkt css = BsSet.exists fkt css
let cssForall fkt css = BsSet.for_all fkt css
let cssUnion css1 css2 = BsSet.union css1 css2
let cssAdd cset css = BsSet.add cset css
let cssFold fkt css init = BsSet.fold fkt css init
let cssSingleton cset = BsSet.singleton cset
let cssEqual css1 css2 = BsSet.equal css1 css2
let cssIter (action: cset -> unit) css =
    BsSet.iter action css


(*****************************************************************************)
(*      "Module type" and a specific implementation of state nodes           *)
(*****************************************************************************)
let nodeCounter = ref 0
let nextNodeIdx () : int =
    let oldVal = !nodeCounter in
    nodeCounter := oldVal + 1;
    oldVal

let stateMake sort bs defer exp =
  { sortS = sort; bsS = bs; deferralS = defer; statusS = Expandable; parentsS = []; childrenS = [];
    constraintsS = cssEmpty; expandFkt = exp;
    idx = nextNodeIdx ()
  }
let stateGetSort state = state.sortS
let stateGetBs state = state.bsS
let stateSetBs state bs = state.bsS <- bs
let stateGetDeferral state = state.deferralS
let stateSetDeferral state bs = state.deferralS <- bs
let stateGetStatus state = state.statusS
let stateSetStatus state status = state.statusS <- status
let stateGetParents state = state.parentsS
let stateAddParent state parent = state.parentsS <- parent::state.parentsS
let stateGetRule state idx = List.nth state.childrenS (List.length state.childrenS - idx)
let stateGetRules state = state.childrenS
let stateAddRule state dep children =
  state.childrenS <- (dep, children)::state.childrenS;
  List.length state.childrenS
let stateGetConstraints state = state.constraintsS
let stateSetConstraints state csets = state.constraintsS <- csets
let stateNextRule state = state.expandFkt ()
let stateGetIdx (state:state) = state.idx


(*****************************************************************************)
(*      "Module type" and a specific implementation of core nodes            *)
(*****************************************************************************)

let coreMake sort bs defer solver fht =
  { sortC = sort; bsC = bs; deferralC = defer; statusC = Expandable; parentsC = []; childrenC = [];
    constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = [];
    idx = nextNodeIdx ()
  }
let coreGetSort core = core.sortC
let coreGetBs core = core.bsC
let coreSetBs core bs = core.bsC <- bs
let coreGetDeferral core = core.deferralC
let coreSetDeferral core bs = core.deferralC <- bs
let coreGetStatus core = core.statusC
let coreSetStatus core status = core.statusC <- status
let coreGetParents core = core.parentsC
let coreAddParent core parent idx = core.parentsC <- (parent, idx)::core.parentsC
let coreSetParent core parent idx = core.parentsC <- [(parent, idx)]
let coreGetChildren core = core.childrenC
let coreAddChild core child = core.childrenC <- child::core.childrenC
let coreGetConstraints core = core.constraintsC
let coreSetConstraints core csets = core.constraintsC <- csets
let coreGetSolver core = core.solver
let coreDeallocateSolver core = core.solver <- None; FHt.reset core.fht
let coreGetFht core = core.fht
let coreGetIdx (core:core) = core.idx
let coreGetConstraintParents core = core.constraintParents
let coreAddConstraintParent core cset =
  core.constraintParents <- cset::core.constraintParents


(*****************************************************************************)
(*      "Module type" and a specific implementation of sets of               *)
(*      states, cores, and constraints for the sat propagation               *)
(*****************************************************************************)

let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
let setCopyState set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
let setCopyCore set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
let setEmptyCnstr () = GHtS.create 128
let setAddState set state =
  GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state
let setAddCore set core =
  GHt.add set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) core
let setAddCnstr set cset = GHtS.add set cset ()
let setMemState set state =
  GHt.mem set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
let setMemCore set core =
  GHt.mem set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
let setMemCnstr set cset = GHtS.mem set cset
let setRemoveState set state =
  GHt.remove set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
let setRemoveCore set core =
  GHt.remove set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
let setRemoveCnstr set cset = GHtS.remove set cset
let setIterState fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
let setIterCore fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set
let setLengthState seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
let setLengthCore seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta


(*****************************************************************************)
(*        "Module type" and a specific implementation of the mapping         *)
(*        between (local) formulae and literals of the sat solver,           *)
(*        and of a mapping of nominals to sets of formulae                   *)
(*****************************************************************************)

let lhtInit () = LHt.create 16
let lhtAdd lht lit f = LHt.add lht lit f
let lhtFind lht lit =
  try
    Some (LHt.find lht lit)
  with Not_found -> None

let fhtInit () = FHt.create 16
let fhtAdd fht f lit = FHt.add fht f lit
let fhtFind fht f =
  try
    Some (FHt.find fht f)
  with Not_found -> None

let nhtInit () = NHt.create 8
let nhtAdd nht nom bs = NHt.add nht nom bs
let nhtFind nht nom =
  try
    Some (NHt.find nht nom)
  with Not_found -> None
let nhtFold fkt nht init = NHt.fold fkt nht init

(*****************************************************************************)
(*         "Module type" and a specific implementation of sets of            *)
(*         local formulae and @-formulae                                     *)
(*****************************************************************************)

let tboxTable = ref (Array.make 0 S.dummyBS)
let negativeFormulas = ref (Array.make 0 S.dummyBS) (* negative Formulas *)
let tboxDefs  = ref (Array.make 0 (Hashtbl.create 0))  (* Definitions *)
let tboxExtensions  = ref (Array.make 0 (Hashtbl.create 0))	(* Extensions *)

let bsetMake () = S.makeBS ()
let bsetDummy () = S.dummyBS
let bsetAdd bs lf = S.addBSNoChk bs lf
let bsetMem bs lf = S.memBS bs lf
let bsetRem bs lf = S.remBS bs lf
let bsetCompare bs1 bs2 = S.compareBS bs1 bs2
let bsetUnion bs1 bs2 = S.unionBSNoChk bs1 bs2
let bsetMakeRealEmpty () =
    let res = bsetMake () in
    bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
    res
let bsetCopy bs = S.copyBS bs
let bsetFold fkt bs init = S.foldBS fkt bs init
let bsetReplace fkt bs init = S.foldBS fkt bs init
let bsetIter fkt bset = S.iterBS fkt bset
let bsetFilter (a: bset) (f: localFormula -> bool) : bset =
    let res = bsetMakeRealEmpty () in
    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
    res
let bsetPartition (f: localFormula -> bool) (a: bset) : (bset * bset) =
    let left = bsetMakeRealEmpty () in
    let right = bsetMakeRealEmpty () in
    bsetIter (fun form -> if (f form) then bsetAdd left form else bsetAdd right form) a;
    (left, right)

let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort)

let csetCompare cs1 cs2 = S.compareBS cs1 cs2
let csetMake () = S.makeBS ()
let csetAdd cs lf = S.addBSNoChk cs lf
let csetCopy cs = S.copyBS cs
let csetUnion cs1 cs2 = S.unionBSNoChk cs1 cs2
let csetHasDot cs = S.memBS cs !S.bsfalse
let csetAddDot cs = S.addBSNoChk cs !S.bsfalse
let csetRemDot cs = S.remBS cs !S.bsfalse
let csetAddTBox sort cs = S.unionBSNoChk cs !tboxTable.(sort)
let csetIter cs fkt =
  let fkt2 f = if not (f = !S.bstrue || f = !S.bsfalse) then fkt f else () in
  S.iterBS fkt2 cs


(*****************************************************************************)
(*            "Module type" and a specific implementation of                 *)
(*            local formulae and @-formulae                                  *)
(*****************************************************************************)

(** This table maps integers (representing formulae) to their corresponding formulae.
 *)
let arrayFormula = ref (Array.make 0 (Array.make 0 C.TRUE))

(** This table maps integers (representing formulae) to their corresponding type.
 *)
let arrayType = ref (Array.make 0 (Array.make 0 Other))

(** This lookup table maps formulae (represented as integers)
    to their negation (in negation normal form).
 *)
let arrayNeg = ref (Array.make 0 (Array.make 0 (-1)))

(** These lookup tables map formulae (represented as integers)
    to their decompositions (represented as integers).
    This is done according to the rules of the tableau procedure
    and depends on the type of the formulae.
 *)
 (*
    for PML: arrayDest1 = the subformula
             arrayNum  = the nominator of the probability
             arrayNum2 = the denominator of the probability
 *)
let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1)))  (* first subformula *)
let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1)))  (* second subformula *)
let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1)))  (* a role *)
let arrayDeferral = ref (Array.make 0 (Array.make 0 (-1)))  (* deferral at point *)
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1)))  (* an integer *)
let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1)))  (* another integer *)
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)

(** This lookup table maps formulae (represented as integers)
    to their @-wrapper.
 *)
let arrayAt = ref (Array.make 0 (Array.make 0 (FHt.create 64)))

let lfGetType sort f = !arrayType.(sort).(f)
let lfGetDest1 sort f = !arrayDest1.(sort).(f)
let lfGetDest2 sort f = !arrayDest2.(sort).(f)
let lfGetDest3 sort f = !arrayDest3.(sort).(f)
let lfGetDeferral sort f = !arrayDeferral.(sort).(f)
let lfGetDestNum sort f = !arrayDestNum.(sort).(f)
let lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f)
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
let lfGetNeg sort f =
  let nf = !arrayNeg.(sort).(f) in
  if nf >= 0 then Some nf else None
let lfGetAt (sort, nom) f =
  FHt.find !arrayAt.(sort).(f) nom
let lfToInt lf = lf
let lfFromInt num = num
let lfGetFormula sort f = !arrayFormula.(sort).(f)

let escapeHtml (input : string) : string =
  List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str)
    [("<", "&lt;") ; (">", "&gt;") ; ("&", "&amp;")]
    input

let bsetToString sort bset : string =
    let toFormula (lf:localFormula) (lst: string list) : string list =
        let formula: C.formula = lfGetFormula sort lf in
        (C.string_of_formula formula) :: lst
    in
    let formulaList = bsetFold toFormula bset [] in
    "{ "^(String.concat ", " formulaList)^" }"

let csetToString sort cset = bsetToString sort cset

let coreToString (core:core): string =
    let helper cset lst : string list =
        (csetToString core.sortC cset):: lst
    in
    let constraints = cssFold helper core.constraintsC [] in
    let children =
        List.map (fun (st:state) -> string_of_int st.idx) core.childrenC
    in
    let parents =
        List.map (fun (st,_:state*int) -> string_of_int st.idx) core.parentsC
    in
    "Core "^(string_of_int core.idx)^" {\n"^
    "  Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^
    "  " ^ bsetToString core.sortC core.bsC ^ "\n" ^
    "  Deferrals: \n" ^
    "    " ^ bsetToString core.sortC core.deferralC ^ "\n" ^
    "  Constraints: { "^(String.concat
                         "\n                 " constraints)^" }\n"^
    "  Children: { "^(String.concat
                         ", " children)^" }\n"^
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
    "}"

let stateToString (state:state): string =
    let helper cset lst : string list =
        (csetToString state.sortS cset):: lst
    in
    let constraints = cssFold helper state.constraintsS [] in
    let core2idx core = core.idx in
    let fst (a,b) = a in
    let conclusionList =
        List.map (fun (_,lst) ->
                  List.map (fun (core:core) -> string_of_int core.idx) lst
        ) state.childrenS
    in
    let conclusionList =
        List.map (fun x -> "{"^String.concat ", " x^"}") conclusionList
    in
    let parents =
        List.map (fun (co:core) -> string_of_int co.idx) state.parentsS
    in
    "State "^(string_of_int state.idx)^" {\n"^
    "  Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^
    "  " ^ bsetToString state.sortS state.bsS ^ "\n" ^
    "  Deferrals: \n" ^
    "    " ^ bsetToString state.sortS state.deferralS ^ "\n" ^
    "  Constraints: { "^(String.concat
                         "\n                 " constraints)^" }\n"^
    "  Children: { "^(String.concat
                         "\n              " conclusionList)^" }\n"^
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
    "}"

let stateToDot (state:state): string =
  let color = match state.statusS with
    | Sat -> "green"
    | Unsat -> "red"
    | Open -> "yellow"
    | Expandable -> "white"
  in
  let toFormula (lf:localFormula) (lst: string list) : string list =
    let formula: C.formula = lfGetFormula state.sortS lf in
    if (bsetMem state.deferralS lf)
    then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
    else (escapeHtml (C.string_of_formula formula)) :: lst
  in
  let formulaList = bsetFold toFormula state.bsS [] in
  let ownidx = (string_of_int state.idx) in
  let parents =
    List.map (fun (co:core) ->
              "Node"^string_of_int co.idx^" -> Node"^ownidx^";")
             state.parentsS
  in
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
  ^ ",label=<State "  ^ ownidx
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
  ^ ">];\n"
  ^ (String.concat "\n" parents)


let coreToDot (core:core): string =
  let color = match core.statusC with
    | Sat -> "green"
    | Unsat -> "red"
    | Open -> "yellow"
    | Expandable -> "white"
  in
  let toFormula (lf:localFormula) (lst: string list) : string list =
    let formula: C.formula = lfGetFormula core.sortC lf in
    if (bsetMem core.deferralC lf)
    then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
    else (escapeHtml (C.string_of_formula formula)) :: lst
  in
  let formulaList = bsetFold toFormula core.bsC [] in
  let ownidx = (string_of_int core.idx) in
  let parents =
    List.map (fun (st,_:state*int) ->
              "Node"^string_of_int st.idx^" -> Node"^ownidx^";")
             core.parentsC
  in
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
  ^ ",label=<Core "  ^ ownidx
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
  ^ ">];\n"
  ^ (String.concat "\n" parents)


let queuePrettyStatus () =
  let printList (sl : int list) : string =
    String.concat ", " (List.map string_of_int sl)
  in
  (* TODO: are atFormulas always look-up-able for sort 0? *)
  (Printf.sprintf "%d Constraints: " (List.length !queueCnstrs))
  ^(String.concat ", " (List.map (csetToString 0) !queueCnstrs))
  ^(Printf.sprintf "\n%d States: " (List.length !queueStates))
  ^(printList (List.map (fun (st:state) -> st.idx) !queueStates))
  ^(Printf.sprintf "\n%d Cores1: " (List.length !queueCores1))
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores1))
  ^(Printf.sprintf "\n%d Cores2: " (List.length !queueCores2))
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores2))
  ^"\n"




let atFormulaGetSubformula f = !arrayDest1.(0).(f)
let atFormulaGetNominal f =
  let s = !arrayDest3.(0).(f) in
  let n = !arrayDest2.(0).(f) in
  (s, n)

let lfToAt _ lf = lf

(* Calculate all possible formulae. This includes all subformulae and
   in the case of μ-Calculus the Fischer-Ladner closure.

   TODO: variable sort needs to match epected sort
 *)
let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
  let newvars = List.filter (fun (x) -> C.hc_freeIn x f) vars in
  let detClosure_ = detClosure newvars in
  let deferral = if List.length newvars > 0
                 then (List.hd newvars)
                 else "ε" in
  if s < 0 || s >= Array.length fset then
    let sstr = string_of_int s in
    raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr))
  else ();
  if C.HcFHt.mem vset.(s) f &&
    (compare (C.HcFHt.find vset.(s) f) deferral = 0 ||
        compare deferral "ε" = 0)
  then ()
  else
    let () = C.HcFHt.add vset.(s) f deferral in
    let () = C.HcFHt.add fset.(s) f () in
    let (func, sortlst) = !sortTable.(s) in
    match f.HC.node with
    | C.HCTRUE
    | C.HCFALSE
    | C.HCVAR _ -> ()
    | C.HCAP name ->
        if C.isNominal name then begin
          Hashtbl.replace nomset name s;
          match nomTbl name with
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
          | Some sort ->
              if sort <> s then
                let str1 = "Nominal: " ^ name ^ " of sort " ^ (string_of_int sort) in
                let str2 = " is used in sort " ^ (string_of_int s) ^ "." in
                raise (C.CoAlgException (str1 ^ str2))
              else ()
        end else ()
    | C.HCNOT _ -> ()
    | C.HCAT (name, f1) ->
        C.HcFHt.replace atset f ();
        let s1 =
          match nomTbl name with
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
          | Some sort -> sort
        in
        let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
        detClosure_ nomTbl hcF fset vset atset nomset s1 hcnom;
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
    | C.HCOR (f1, f2)
    | C.HCAND (f1, f2) ->
        detClosure_ nomTbl hcF fset vset atset nomset s f1;
        detClosure_ nomTbl hcF fset vset atset nomset s f2
    | C.HCEX (_, f1)
    | C.HCAX (_, f1) ->
        if (func <> MultiModalK && func <> MultiModalKD && func <> Monotone && func <> MultiModalM)
            || List.length sortlst <> 1
        then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
        else ();
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
    | C.HCENFORCES (_, f1)
    | C.HCALLOWS (_, f1) ->
        if func <> CoalitionLogic || List.length sortlst <> 1
        then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.")
        else ();
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
    | C.HCMORETHAN (_,_,f1)
    | C.HCMAXEXCEPT (_,_,f1) ->
        if func <> GML || List.length sortlst <> 1
        then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.")
        else ();
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
    | C.HCATLEASTPROB (_,f1)
    | C.HCLESSPROBFAIL (_,f1) ->
        if func <> PML || List.length sortlst <> 1
        then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.")
        else ();
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
        (*
            TODO: add ¬ f1 to the closure!
        detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde)
        *)
    | C.HCCONST color
    | C.HCCONSTN color ->
      begin match func with