let split ~(print:bool) (clauses: clause list) : clause list =
if print then begin
print_endline ("Preprocessing: Ground Splitting");
end;
let labels =
Labels.create 64
in
let counter =
Counter.create_with 0
in
let rec split' to_split already_split split_done =
match to_split with
| [] ->
if print then begin
print_endline ("Performed " ^ string_of_int (Counter.value counter) ^ " non-ground splits.");
print_newline ();
end;
if split_done then
List.rev already_split
else
clauses
| clause :: tail ->
begin
let clause' =
List.map
(fun literal ->
literal, Term.vars_of_literal literal
)
clause
in
match split_clause labels counter clause' with
| None ->
split' tail (clause :: already_split) split_done
| Some [] ->
failwith "Preprocessing_split_ground.split: empty clause"
| Some split ->
if print then begin
print_endline ("Non-ground split: " ^ Term.clause_to_string clause);
List.iter
(fun clause ->
print_endline ("-> " ^ Term.clause_to_string clause)
)
split;
print_newline ();
end;
split' tail (split @ already_split) true
end
in
split' clauses [] false