let rec get_explanation (state: state) (literals: literal array) : explanation =
Array.fold_left
(fun acc literal ->
let literal_info =
try
LiteralTable.find state.st_literal_info literal
with
| Not_found ->
failwith ("State.get_explanation: " ^ Term.literal_to_string literal)
in
let explanation =
match literal_info.li_explanation with
| Some explanation ->
explanation
| None ->
let explanation =
get_explanation state literal_info.li_context_literals
in
literal_info.li_explanation <- Some explanation;
explanation
in
merge_explanations acc explanation
)
[]
literals