open General
exception SHOULD_NOT_HAPPEN
type qbf_10 = Neg of qbf_10
  | Var of var
  | Quantifier of q_type * var list * qbf_10
  | BiOP of bi_op * qbf_10 list
  | EXOP of equ_xor_op * qbf_10 * qbf_10
(*
 *  nnf_qbf : qbf_10 -> qbf_10
 *  qbf_10을 입력 받아서 NNF(Negation Normal Form)으로 변환한다.
 *)
let rec nnf_qbf_10 (q:qbf_10) : qbf_10 = match q with
  Neg (Quantifier(t, var_list, q)) -> 
    Quantifier
      ((if t = Forall then Exists else Forall),
       var_list, 
       nnf_qbf_10(Neg q))
| Neg (BiOP(t, l)) -> 
    BiOP
      ((if t = And then Or else And),
       List.map (fun x -> (nnf_qbf_10 (Neg x))) l)
| Neg (Var x) -> q
| Neg (EXOP(t, q1, q2)) -> 
    let new_t = if t = Equ then Xor else Equ in
      EXOP(new_t, nnf_qbf_10 q1, nnf_qbf_10 q2)
| Neg (Neg q) -> nnf_qbf_10 q
| Quantifier(t, l, q) -> Quantifier(t, l, nnf_qbf_10 q)
| BiOP(t, l) -> BiOP(t, List.map nnf_qbf_10 l)
| Var(x) -> Var(x)
| EXOP(t, q1, q2) -> EXOP(t, nnf_qbf_10 q1, nnf_qbf_10 q2)

(* 
  let rec print_qbf_10 (q:qbf_10) : unit = match q with
    Neg q -> (print_string "!(";
	      print_qbf_10 q;
	      print_string ")")
  | Var v -> print_string v
  | Quantifier(q_t, var_head::var_list, q) ->
      (print_string "(";
       if q_t = General.Forall then 
	 print_string "forall " 
       else
	 print_string "exists ";
       print_string "[";
       print_string var_head;
       List.iter (fun var -> print_string (", "^var)) var_list;
       print_string "] ";
       print_qbf_10 q;
       print_string ")")
  | Quantifier(_, [], _) -> raise SHOULD_NOT_HAPPEN
  | BiOP(b_t, q_list) -> 
      let b_type2string b = if b = And then "&" else "|" in
      let rec print_qbf_list b_t qbf_list = match qbf_list with
	  [q1;q2] -> (print_string "(";
		      print_qbf_10 q1;
		      print_string (" "^(b_type2string b_t)^" ");
		      print_qbf_10 q2;
		      print_string ")")
	| q_head::tail_list -> (print_string "(";
				print_qbf_10 q_head;
				print_string (" "^(b_type2string b_t)^" ");
				print_qbf_list b_t tail_list;
				print_string ")";)
	| [] -> raise SHOULD_NOT_HAPPEN
      in
	print_qbf_list b_t q_list
*)
