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

open Util;;

(* 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;;
type color = int;;

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) ());
 )
;;

print_endline "Three example encodings:";;

(* 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]
);;

(******************************************************************************)

print_endline "\nIt will now run some problems and decode the solutions";;
print_endline "Press ENTER to continue.";;
let _ = read_line ();;

let strip_lambda_matches =
 let getvar = function
  | `Var(n,_) -> n
  | _ -> assert false in
 let rec aux n = function
  | `Lam(_,t) -> aux (n+1) t
  | `Match(_,_,_,bs,_) -> Some (n, List.map (getvar ++ snd) !bs)
  | _ -> None
 in aux 0
;;

let next_candidates sigma cands =
 let sigma = Util.filter_map
  (fun x -> try Some (List.assoc x sigma) with Not_found -> None) cands in
 match Util.find_opt strip_lambda_matches sigma with
 | None -> -1, []
 | Some x -> x
;;

let fix_numbers l =
 let rec aux n = function
 | [] -> []
 | x::xs -> (x - 2*n - 1) :: (aux (n+1) xs)
 in aux 0 l
;;

let color (g:graph) =
 let p = encode_graph g in
 let (_, _, _, _, vars as p) = Parser.problem_of_string p in
 let _, result = Lambda4.solve (Lambda4.problem_of p) in
 match result with
 | `Unseparable _ -> prerr_endline "Graph not colorable"; None
 | `Separable sigma -> (
  (* start from variable x *)
  let x = Util.index_of "x" vars in
  (* List.iter (fun x -> prerr_endline (string_of_int (fst x) ^ ":" ^ Num.print ~l:vars (snd x))) sigma; *)
  let rec iter f x =
   let n, x = f x in if x = [] then [] else n :: iter f x in
  let numbers = iter (next_candidates sigma) [x] in
  let numbers = fix_numbers numbers in
  (* display solution *)
  let colors = ["r"; "g"; "b"] in
  prerr_endline ("\nSolution found:\n " ^ String.concat "\n "
   (List.mapi (fun i x ->
     string_of_int i ^ " := " ^ List.nth colors x) numbers));
  assert (List.for_all (fun (a,b) -> List.nth numbers a <> List.nth numbers b) g);
  Some numbers)
;;

let bruteforce g =
 let nodes_no = 1+
  List.fold_left (fun acc (a,b) -> Pervasives.max acc (Pervasives.max a b)) 0 g in
 let check x = if List.for_all (fun (a,b) -> List.nth x a <> List.nth x b) g
  then failwith "bruteforce: sat" in
 let rec guess l = prerr_string "+";
  if List.length l = nodes_no
   then check l
    else (guess (0::l); guess (1::l); guess (2::l)) in
 guess [];
 prerr_endline "bruteforce: unsat"
;;

assert (color [0,1;0,2;1,2;2,3;3,0] <> None);;
assert (color [0,1;0,2;1,2;2,3;3,0;0,4;4,2] <> None);;

(* assert (color [
 1,2; 1,4; 1,7; 1,9; 2,3; 2,6; 2,8; 3,5;
 3,7; 3,0; 4,5; 4,6; 4,0; 5,8; 5,9; 6,11;
 7,11; 8,11; 9,11; 0,11;
] = None);; *)

(* https://turing.cs.hbg.psu.edu/txn131/file_instances/coloring/graph_color/queen5_5.col *)
color [1,7
; 1,13
; 1,19
; 1,25
; 1,2
; 1,3
; 1,4
; 1,5
; 1,6
; 1,11
; 1,16
; 1,21
; 2,8
; 2,14
; 2,20
; 2,6
; 2,3
; 2,4
; 2,5
; 2,7
; 2,12
; 2,17
; 2,22
; 2,1
; 3,9
; 3,15
; 3,7
; 3,11
; 3,4
; 3,5
; 3,8
; 3,13
; 3,18
; 3,23
; 3,2
; 3,1
; 4,10
; 4,8
; 4,12
; 4,16
; 4,5
; 4,9
; 4,14
; 4,19
; 4,24
; 4,3
; 4,2
; 4,1
; 5,9
; 5,13
; 5,17
; 5,21
; 5,10
; 5,15
; 5,20
; 5,25
; 5,4
; 5,3
; 5,2
; 5,1
; 6,12
; 6,18
; 6,24
; 6,7
; 6,8
; 6,9
; 6,10
; 6,11
; 6,16
; 6,21
; 6,2
; 6,1
; 7,13
; 7,19
; 7,25
; 7,11
; 7,8
; 7,9
; 7,10
; 7,12
; 7,17
; 7,22
; 7,6
; 7,3
; 7,2
; 7,1
; 8,14
; 8,20
; 8,12
; 8,16
; 8,9
; 8,10
; 8,13
; 8,18
; 8,23
; 8,7
; 8,6
; 8,4
; 8,3
; 8,2
; 9,15
; 9,13
; 9,17
; 9,21
; 9,10
; 9,14
; 9,19
; 9,24
; 9,8
; 9,7
; 9,6
; 9,5
; 9,4
; 9,3
; 10,14
; 10,18
; 10,22
; 10,15
; 10,20
; 10,25
; 10,9
; 10,8
; 10,7
; 10,6
; 10,5
; 10,4
; 11,17
; 11,23
; 11,12
; 11,13
; 11,14
; 11,15
; 11,16
; 11,21
; 11,7
; 11,6
; 11,3
; 11,1
; 12,18
; 12,24
; 12,16
; 12,13
; 12,14
; 12,15
; 12,17
; 12,22
; 12,11
; 12,8
; 12,7
; 12,6
; 12,4
; 12,2
; 13,19
; 13,25
; 13,17
; 13,21
; 13,14
; 13,15
; 13,18
; 13,23
; 13,12
; 13,11
; 13,9
; 13,8
; 13,7
; 13,5
; 13,3
; 13,1
; 14,20
; 14,18
; 14,22
; 14,15
; 14,19
; 14,24
; 14,13
; 14,12
; 14,11
; 14,10
; 14,9
; 14,8
; 14,4
; 14,2
; 15,19
; 15,23
; 15,20
; 15,25
; 15,14
; 15,13
; 15,12
; 15,11
; 15,10
; 15,9
; 15,5
; 15,3
; 16,22
; 16,17
; 16,18
; 16,19
; 16,20
; 16,21
; 16,12
; 16,11
; 16,8
; 16,6
; 16,4
; 16,1
; 17,23
; 17,21
; 17,18
; 17,19
; 17,20
; 17,22
; 17,16
; 17,13
; 17,12
; 17,11
; 17,9
; 17,7
; 17,5
; 17,2
; 18,24
; 18,22
; 18,19
; 18,20
; 18,23
; 18,17
; 18,16
; 18,14
; 18,13
; 18,12
; 18,10
; 18,8
; 18,6
; 18,3
; 19,25
; 19,23
; 19,20
; 19,24
; 19,18
; 19,17
; 19,16
; 19,15
; 19,14
; 19,13
; 19,9
; 19,7
; 19,4
; 19,1
; 20,24
; 20,25
; 20,19
; 20,18
; 20,17
; 20,16
; 20,15
; 20,14
; 20,10
; 20,8
; 20,5
; 20,2
; 21,22
; 21,23
; 21,24
; 21,25
; 21,17
; 21,16
; 21,13
; 21,11
; 21,9
; 21,6
; 21,5
; 21,1
; 22,23
; 22,24
; 22,25
; 22,21
; 22,18
; 22,17
; 22,16
; 22,14
; 22,12
; 22,10
; 22,7
; 22,2
; 23,24
; 23,25
; 23,22
; 23,21
; 23,19
; 23,18
; 23,17
; 23,15
; 23,13
; 23,11
; 23,8
; 23,3
; 24,25
; 24,23
; 24,22
; 24,21
; 24,20
; 24,19
; 24,18
; 24,14
; 24,12
; 24,9
; 24,6
; 24,4
; 25,24
; 25,23
; 25,22
; 25,21
; 25,20
; 25,19
; 25,15
; 25,13
; 25,10
; 25,7
; 25,5
; 25,1];;