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 connection_clauses =
ConnectionClauses.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) ^ " ground splits.");
print_newline ();
end;
if split_done then
List.rev already_split
else
clauses
| clause :: tail ->
begin
match split_clause labels counter connection_clauses clause with
| None ->
split' tail (clause :: already_split) split_done
| Some split ->
if print then begin
print_endline ("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