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
                 (* memoize *)
                 literal_info.li_explanation <- Some explanation;
                 explanation
       in
         merge_explanations acc explanation
    )
    []
    literals