let request_skolemized_clause (clause: clause) : clause =
let var_skolemization, par_normalization =
List.fold_left
(fun acc literal ->
request_skolemized_term' literal.atom acc
)
([], [])
clause
in
match var_skolemization with
| [] ->
(* no universal variables in term *)
clause
| _ ->
let mapping =
List.map
(fun (var, term) ->
request_var var, term
)
(par_normalization @ var_skolemization)
in
List.map
(fun literal ->
replace_terms_in_literal literal mapping
)
clause