(*----------------------------------------------------------------*)
open General
open Qbf_10
exception Not_NNF
exception SHOULD_NOT_HAPPEN
module Var_set = Set.Make(String)
type qbf = Literal of var
  | N_Literal of var
  | Quantifier of q_type * var list * qbf
  | BiOP of bi_op * qbf list * Var_set.t
  | EXOP of equ_xor_op * qbf * qbf * Var_set.t
(*------------------------------------------------------------------*)

(* get_var_set : qbf -> Var.set.t 
 * qbf를 받아서, 해당 qbf 전체가 가지고 있는 variable들의 집합을 반환한다. *)
let rec get_var_set (q: qbf) : Var_set.t = 
  match q with
    Literal x -> Var_set.singleton x
  | N_Literal x -> Var_set.singleton x
  | Quantifier(_, _, q) -> get_var_set q
  | BiOP (_, _, set) -> set
  | EXOP (_, _, _, set) -> set
      
(* convert_from_qbf_10_to_qbf : qbf_10 -> qbf
 * 
 * 각각의 노드에 해당 노드 아래의 variable들을 간직하는 set을 할당한다.
 * 
 * 1. 우선 NNF로 변환한다. => nnfed_q_10
 * 2. Literal은 그대로 둔다.
 * 3. Quantifier인 경우, 내부 qbf를 처리한다.
 * 4. BiOP인 경우, List item 각각을 convert한 이후에, 각각의 variable들을 모두 합한다.
 *) 
let rec convert_from_qbf_10_to_qbf (q_10: qbf_10) : qbf =
   let 
       nnfed_q_10 = nnf_qbf_10 q_10 
   in
   match nnfed_q_10 with 
   Qbf_10.Neg (Qbf_10.Var x) -> N_Literal x
   | Qbf_10.Neg(_) -> raise Not_NNF
   | Qbf_10.Var x -> Literal x
   | Qbf_10.Quantifier (t, l, q_sub) -> 
       Quantifier(t , l, convert_from_qbf_10_to_qbf q_sub)
   | Qbf_10.BiOP(bt, l) ->
   let
       new_list : qbf list = List.map convert_from_qbf_10_to_qbf l
   in
   BiOP (bt,
	 new_list,
	 List.fold_left 
	   Var_set.union 
	   Var_set.empty
	   (List.map get_var_set new_list))
   | Qbf_10.EXOP(t, q1, q2) -> 
       let qbf1 = convert_from_qbf_10_to_qbf q1 in
       let qbf2 = convert_from_qbf_10_to_qbf q2 in
	 EXOP(t, qbf1, qbf2, Var_set.union (get_var_set qbf1) (get_var_set qbf2))
  (*
     * push_into : qbf -> var -> q_type -> qbf
     * Push q_type v into QBF q.
  *)
let rec
    push_into (q:qbf) (v:var) (qt:q_type) : qbf = 
  match q with
    Literal _ -> Quantifier(qt, [v], q)
  | N_Literal _ -> Quantifier(qt, [v], q)
  | BiOP((bt:bi_op), (qbf_list:qbf list), (set:Var_set.t)) -> 
      let
	  (partition_o, partition_x) = 
	(List.partition
	   (fun q_i -> 
	     (Var_set.mem
		v
		(get_var_set q_i))
	       )
	   qbf_list)
      in
      (
      match partition_o with
       (* In case there is no partition_o in here *)
	[] -> print_string v; raise SHOULD_NOT_HAPPEN
       (* In case that partition_o has only one member *)
      | one::[] -> 
	  BiOP
	    (bt,
	     (push_into one v qt)::partition_x,
	     Var_set.add v set)
       (* In case that partition_o has more than one member *)
      | _ -> 
	  let new_q = 
	    Quantifier
	      (qt,
	       [v], 
	       BiOP
		 (bt, 
		  partition_o, 
		  List.fold_left 
		    Var_set.union 
		    Var_set.empty
		    (List.map get_var_set partition_o)))
	  in
	  if List.length partition_x = 0 then
	    new_q
	  else
	    BiOP 
	      (bt,
	       (new_q:: partition_x),
	       Var_set.add v set)
	      )
  | Quantifier(qt', var_list, q') -> 
	(* 서로 다른 quantifier 이면 stop *)
      if qt != qt' then
	  Quantifier(qt, [v], q)
	(* 서로 같은 quantifier 이면 파고 든다. 파고든 이후에 같은 quantifier가 연속 되면 합쳐줘야 한다. *)
      else 
	let 
	    pushed_result_of_q' = push_into q' v qt
	in
	(match pushed_result_of_q' with
	    (* 파고든 결과가 바깥의 quantifier와 동일한 type인 경우, 합친다. *)
	  Quantifier(result_qt, l, q) -> 
	    if result_qt = qt 
	    then 
	      Quantifier(qt', var_list@l, q)
	    else
	      Quantifier(qt', var_list, pushed_result_of_q')
	    (* 바깥의 quantifier와 다른 경우는 그냥 붙인다. *)	
	| _ -> Quantifier(qt', var_list, pushed_result_of_q'))
  | EXOP(t, q1, q2, var_set) -> 
      let v_in_q1 = Var_set.mem v (get_var_set q1) in
      let v_in_q2 = Var_set.mem v (get_var_set q2) in
	(match (v_in_q1, v_in_q2) with
	    (true, true) -> Quantifier(qt, [v], q)
	  | (true, false) -> EXOP(t, push_into q1 v qt, q2, Var_set.add v var_set)
	  | (false, true) -> EXOP(t, q1, push_into q2 v qt, Var_set.add v var_set)
	  | _ -> raise SHOULD_NOT_HAPPEN)
            
(* push_quantifier : qbf -> qbf
   *
   * qbf q를 받아서, 이것을 quantifier를 더 이상 밀어넣을 수 없는 상태로 만든다. 
   * push_into를 이용하게 된다.
*)
and push_quantifier (q:qbf) :qbf = 
  match q with
    Literal _ -> q
  | N_Literal _ -> q
  | BiOP(bt, qbf_list, var_set) ->
      let
	  pushed_qbf_list = List.map push_quantifier qbf_list
      in
      BiOP (bt, pushed_qbf_list, var_set)
  | Quantifier(qt, var_list, q') ->
      let 
	  pushed_q' = push_quantifier q'
      in
      List.fold_left
	(fun old_q v -> push_into old_q v qt)
	pushed_q'
	var_list
  | EXOP(t, q1, q2, var_set) -> EXOP(t, push_quantifier q1, push_quantifier q2, var_set)

(*let rec print_qbf2dot (q:qbf) : unit = 
  let print_header () :unit = 
    print_string 
      ("digraph G {\n"^
       "graph [concentrate=true, fontsize=\"14.00\", ordering=out, rankdir=TB, ranksep=\"0.30\", ratio=\"1.80\", size=\"4,4\"];")
  in
  let print_footer () :unit = print_string "}\n" in
  let and_c = ref 0 in
  let or_c = ref 0 in
  let forall_c = ref 0 in
  let exists_c = ref 0 in
  let node2string (q:qbf) =
    match q with
    Literal x -> x
    | N_Literal x -> ("!"^x)
    | Quantifier(qt, var_list, _) -> 
	let qt_string = 
	  if qt = Forall then 
	    (incr forall_c;("U"^(string_of_int (!forall_c))))
          else 
	    (incr exists_c;("E"^(string_of_int (!exists_c))))
	in
	let var_list_string = 
	  List.fold_left (fun s v -> (s^" "^v)) "" var_list 
	in
	qt_string^"["^var_list_string^"]"
    | BiOP(bt, _, _) -> 
	if bt = And then
	  (incr and_c;("AND "^(string_of_int (!and_c))))
	else 
	  (incr or_c;("OR "^(string_of_int (!or_c))))
  in
  let draw_line (from_str:string) (to_str:string) : unit = 
    print_string ("\""^from_str^"\" -> \""^to_str^"\";\n")
  in
  let rec print_qbf2dot_aux (q_name:string) (q: qbf) : unit = 
    match q with 
      Literal x -> ()
    | N_Literal x -> ()
    | Quantifier(qt, var_list, q') -> 
	let
	    q'_name = node2string q'
	in
	(draw_line q_name q'_name;
	 print_qbf2dot_aux q'_name q') 
    | BiOP(bt, q_list, _) -> 
	List.iter 
	  (fun q' -> 
	    let
		q'_name = node2string q'
	    in
	    (draw_line q_name q'_name; 
	     print_qbf2dot_aux q'_name q')
	      ) 
	  q_list
  in
  (print_header ();print_qbf2dot_aux (node2string q) q;print_footer ())
*)

let rec print (out:out_channel) (q:qbf) : unit = match q with
    Literal v -> output_string out v
  | N_Literal v -> output_string out ("!"^v)
  | Quantifier(qt, var_list, qbf) ->
      let
	  qt_string = if qt = Forall then General.forall_string else General.exists_string
      in
      (output_string out "(";
       output_string out qt_string;
       output_string out " [";
       List.iter (fun var -> output_string out var;output_string out " ") var_list;
       output_string out "]";
       print out qbf;
       output_string out ")")
  | BiOP(bt, qbf_list, _) -> 
      let
	  bt_string = (if bt = And then General.and_string else General.or_string)
      in
	(output_string out "(";
	 output_string out bt_string;
	 output_string out " "; 
	 List.iter (fun qbf -> print out qbf;output_string out " ") qbf_list;
	 output_string out ")")
  | EXOP(ex_type, qbf1, qbf2, _) ->
      let
	  ex_string = (if ex_type = Equ then General.equ_string else General.xor_string)
      in      
	(output_string out "(";
	 output_string out ex_string;
	 output_string out " "; 
	 print out qbf1;
	 output_string out " ";
	 print out qbf2;
	 output_string out ")")

    
