let create ~(print_transformation: bool) ~(print_sorts: bool) (problem: problem) : finite_domain =
  (* any preprocessing simplifications applied to the flattened clauses
     didn't do any good, so we just keep them as they are. *)
  if print_transformation then begin
    print_endline ("Finite domain flattening:");
    print_newline ();
  end;

  (* term definitions *)
  let definitions =
    create_term_definitions ~print:print_transformation problem
  in
  (* flatten *)
  let flattened =
    flatten ~print:print_transformation (definitions.new_definitions @ problem#getClauses) definitions
  in
  (* non-ground split - ground splitting didn't help in tests *)
  let flattened =
    Preprocessing_split_nonground.split ~print:false flattened
  in
  (* replace = by -diff to improve performance (less context unifiers with -v) *)
  let flattened =
    List.map to_diff_clause flattened
  in
  let flattened_problem =
    Problem.create ~equality:problem#containsEquality ~horn:false flattened []
  in

  (* do sort inference *)
  let sorts =
    Sort_inference.infer ~print:false problem#getClauses
  in
  (* add the skolem constants generated by the term definitions *)
    List.iter
      (fun (definition_symbol, term_symbol) ->
        Sort_inference.add_constant sorts definition_symbol term_symbol
      )
      definitions.constants;

    if print_sorts then
      Sort_inference.print sorts;


    {
      original = problem;
      flattened = flattened_problem;
      sorts = sorts;
      term_definitions = definitions;
    }