(* debugging ****************************************************************)
-let string_of_entry (inverse, b) =
- if I.S.mem 0 inverse then begin if b then "CF" else "C" end else
+let string_of_entry synth (inverse, b) =
+ if I.overlaps synth inverse then begin if b then "CF" else "C" end else
if I.S.is_empty inverse then "I" else "P"
-let to_string (classes, rc) =
- let linearize = String.concat " " (List.map string_of_entry classes) in
+let to_string synth (classes, rc) =
+ let linearize =
+ String.concat " " (List.map (string_of_entry synth) classes)
+ in
match rc with
| None -> linearize
| Some (i, j, _, _) -> Printf.sprintf "%s %u %u" linearize i j
Array.iteri map b;
prerr_newline ()
+(* dummy dependences ********************************************************)
+
+let make l =
+ let map _ = I.S.empty, false in
+ List.rev_map map l
+
(* classification ***********************************************************)
let classify_conclusion vs =
let rc = classify_conclusion vs in
let map (b, h) (c, v) =
let _, argsno = PEH.split_with_whd (c, v) in
- let isf = argsno > 0 || H.is_sort v in
+ let isf = argsno > 0 (* || H.is_sort v *) in
let iu = H.is_unsafe h (List.hd vs) in
(I.get_rels_from_premise h v, I.S.empty, isf && iu) :: b, succ h
in