let scc_list g =
  let components = C.scc_list g in
  let components = List.filter (fun l ->
    match l with
    | [ a ] -> G.mem_edge g a a
    | _ -> true
  ) components in
  let components = List.map (List.map G.V.label) components in
  List.map (induced g) components

let not_eps =  List.filter (fun s -> s <> "")

let rec constraints_composante g =
  let vertices = G.fold_vertex (fun v l -> v :: l) g [] in
  let nodes = G.fold_vertex (fun v l -> G.V.label v :: l) g [] in
  let nodes_constraints = List.map (fun (s,t) ->
    sprintf "%s >= %s" (pprint_term s) (pprint_term t)
  ) nodes in
  let uts = RuleSet.elements (ut_composante nodes) in
  let uts_constraints = List.map (fun (s,t) ->
    sprintf "%s >= %s" (pprint_term s) (pprint_term t)
  ) uts in
  let uts_conjuct = String.concat " /\\ " uts_constraints in
  let nodes_conjuct = String.concat " /\\ " nodes_constraints in

  let cime_disjunctions = List.map (fun v ->
    let (s,t) = G.V.label v in
    let ineq = sprintf "%s > %s" (pprint_term s) (pprint_term t) in
    let sccs = scc_list (G.remove_vertex g v) in
    let resursive_constraints = List.map constraints_composante sccs in
    let resursive_constraints = not_eps resursive_constraints in
    let root = String.concat " /\\ " (ineq :: not_eps [nodes_conjuct;uts_conjuct]) in
    let root = sprintf "ordering_solve (order_constraints R_trs_0_algebra \"%s\")" root in
(*     printf "%d sccs when removing %s\n%!" (List.length sccs) (pprint_rule (s,t)); *)
    sprintf "( %s )" (String.concat " and\n" (root :: resursive_constraints))
  ) vertices in

(*   printf "\n"; *)
  sprintf "( %s )" (String.concat " or\n\n" cime_disjunctions)

let constraints g =
  let components = scc_list g in
(*   printf "root: %d sccs\n%!" (List.length components); *)
  let components_constraints = List.map constraints_composante components in
  String.concat " and\n\n\n" components_constraints