(*
 Reductions from SAT and 3-colorability of graphs to separation
 of lambda-terms. Commented out the encoding from SAT.
*)

(* type cnf = int list list;;

let (++) f g x = f (g x);;

let maxvar : cnf -> int =
 let aux f = List.fold_left (fun acc x -> max acc (f x)) 0 in
 aux (aux abs)
;; *)

type graph = (int * int) list;;

let arc x y = min x y, max x y;;
let mem g x y = List.mem (arc x y) g;;

(* let reduction_sat_3col p =
 let triangle a0 a1 a2 = [arc a0 a1; arc a0 a2; arc a1 a2] in
 let init0 = triangle 0 1 2 in
 (* 0false; 1true; 2base*)
 let n = maxvar p in
 let init1 = Array.to_list (Array.mapi (fun i () -> triangle (2*i+1) (2*(i+1)) 2) (Array.make n ())) in
 let freshno = ref (2 * n + 3) in
 let mk_triangle () =
  let i = !freshno in
  freshno := i+3; i, i+1, i+2 in
 let rec translate = function
 | [] -> assert false
 | x::[] -> [triangle 0 2 x]
 | x::y::l ->
    let a,b,c = mk_triangle () in
    triangle a b c :: [arc x a; arc y b] :: translate (c::l) in
 let p = List.map (List.map (fun x ->
   if x = 0 then assert false
    else if x < 0 then 2 * (abs x + 1)
    else 2 * x + 1
  )) p in
 let init2 = List.map (List.concat ++ translate) p in
 !freshno, init0 @ List.concat (init1 @ init2)
;;

let string_of_graph g =
 String.concat " " (List.map (fun (x,y) -> string_of_int x ^ "<>" ^ string_of_int y) g)
;; *)

(* let main p =
 let mv = maxvar p in
 prerr_endline (string_of_int mv);
 let _, g = reduction_sat_3col p in
 prerr_endline (string_of_graph g);
 generate ;;

prerr_endline (main[
 [1; -2; 3];
 [2; 4; -5]
]);; *)

let p_ = "BOMB ";;
let x_ = "x ";;
(* y, z dummies *)
let y_ = "y ";;
let z_ = "z ";;
(* a, b endline separators *)
let a_ = "a ";;
let b_ = "b ";;

let generate g n max =
 (* 0 <= n <= max+1 *)
 let three f sep =
  String.concat sep (List.map f [0;1;2]) in
 let rec aux' n m color =
  if m = -1 then x_
  else aux' n (m-1) color ^
   if n = m then
     (if List.mem (n,n) g then p_^p_^p_ (* cappio nel grafo *)
      else three (fun c -> if color = c then y_ else p_) "")
   else if n < m then y_^y_^y_
   else if List.mem (m,n) g then
    three (fun c -> if color = c then p_ else y_) ""
   else y_^y_^y_ in
 let rec aux m =
  if m = -1 then x_
   else aux (m-1) ^
    if n < m then p_^p_^p_
    else if n = m then
      "(_." ^ three (aux' n max) "b) (_." ^ "b) "
    else y_^y_^y_
 in aux max ^ a_
;;

let generate2 g n max =
 let rec aux m =
  if m = -1 then x_
   else aux (m-1) ^
    if n < m then p_^p_^p_
    else if n = m
    then z_^z_^z_
    else y_^y_^y_
 in aux max ^ p_
;;


let encode_graph g =
 let g = List.map (fun (x,y) -> min x y, max x y) g in
 let mapi f a = Array.to_list (Array.mapi f a) in
 let nodex_no =
  List.fold_left (fun acc (a,b) -> Pervasives.max acc (Pervasives.max a b)) 0 in
 String.concat "\n" ("\n$ problem from 3-colorability" ::
  let no = nodex_no g in
  mapi (fun i () ->
    (if i = no+1 then "D " else "C ") ^ generate g i no
  ) (Array.make (no+2) ()) @
  mapi (fun i () ->
    "C " ^ generate2 g i no
  ) (Array.make (no+1) ());
 )
;;

(* easy one *)
prerr_endline (encode_graph [0,1;]);;

(* two imopssible problems *)
prerr_endline (
 encode_graph [0,1; 1,1]
);;
prerr_endline (
 encode_graph [0,1; 0,2; 1,2; 0,3; 1,3; 2,3]
);;