let usage_string = 
  ("QBF Transformer from QBF 1.0 format to the specific format for CMS solver\n"^
     "Microsoft Research Asia, Copyright (c) 2008 Microsoft Corporation\n"^
     "Usage: ./transformer [options] -input <Input QBF 1.0 Instance> -output <Output>\n")
let print_option = ("Options are:\n"^
		      "\t -no_push \t Don't push quantifiers inside.\n"^
		      "\t -push \t Push quantifiers inside as further as possible (default)\n")

let main () =
  let push_flag = ref 1 in
  let input_name = ref "" in
  let output_name = ref "" in
  let speclist = [("-no_push", Arg.Unit (fun () -> push_flag := 0), "\tDo not push quantifiers inside.");
      ("-push", Arg.Unit (fun () -> push_flag := 1), "\tPush quantifiers inside.");
      ("-input", Arg.String (fun s -> input_name := s), "\tinput filename of QBF 1.0 instance");
      ("-output", Arg.String (fun s -> output_name := s), "\toutput filename")] in
    Arg.parse speclist (fun s -> ()) usage_string;
    try
      if 
	!input_name = "" || !output_name = "" 
      then 
	(Arg.usage speclist usage_string; exit 10);
      let input_ch = open_in !input_name in
      let output_ch = open_out !output_name in
      let lexbuf = Lexing.from_channel input_ch in
      let given_qbf_10 = Parser.q Lexer.token lexbuf in
      let qbf = (Qbf.convert_from_qbf_10_to_qbf given_qbf_10) in
      let pushed_qbf = (Qbf.push_quantifier qbf) in
	if !push_flag = 1 then
	  Qbf.print output_ch pushed_qbf
	else
	  Qbf.print output_ch qbf
    with
	Sys_error s -> print_string ("File not found error : "^s^"\n")
      
let _ = main ()		  
let parse_error s = (* Called by the parser function on error *)
  print_endline s;
  flush stdout
