let simplify ~(print: bool) (clauses: clause list) : clause list =
  if print then begin
    print_endline ("Preprocessing: Unit");
  end;

  (* first build index of unit clauses *)
  let index =
    Discrimination_tree.create_literal_index false
  in
    List.iter
      (fun clause ->
         match clause with
           | literal :: [] ->
               (index#find literal)#add literal.Term.atom literal

           | _ ->
               ()
      )
      clauses;

  (* simplify *)
  let clauses', simplified =
    simplify' ~print:print [] clauses index false
  in
    if print then begin
      print_newline ();
    end;

  (* get original order of clauses back *)
  if simplified then
    List.rev clauses'
  else
    clauses