TacSplit.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2021                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Lang

module PartitionsQQ : sig
  val destructs_qq :
    Lang.F.pool -> is_forall:bool ->
    Lang.F.QED.term ->
    Lang.F.Vars.t * Lang.F.QED.term

  val get : vars:Lang.F.Vars.t -> Lang.F.term list ->
    int * Lang.F.Tset.t list
end
= struct
  let dkey = Wp_parameters.register_category "tac_split_quantifiers" (* debugging key *)
  let debug fmt = Wp_parameters.debug ~dkey fmt

  let destructs_qq pool ~is_forall t =
    let ctx,a = F.e_open ~pool ~forall:is_forall ~exists:(not is_forall) ~lambda:false t in
    let vars = List.fold_left (fun vars (_,var) -> F.Vars.add var vars) F.Vars.empty ctx
    in vars, a

  type kind_t = Root of F.Tset.t | Node of node_t
  and  node_t = { var: F.Var.t;
                  mutable rank: int;
                  mutable kind: kind_t
                }
  type var2node_t = node_t F.Vmap.t

  let is_root root = match root.kind with
    | Node _ -> false
    | Root _ -> true

  let find (map:var2node_t) var =
    let find_root var root = function
      | None -> (* adds an empty root partition for that [var] *)
          root := Some { var; rank=0; kind=(Root F.Tset.empty) };
          debug ". . find(%a)= %a (inserted)@." Lang.F.pp_var var Lang.F.pp_var var ;
          !root
      | (Some { kind=(Root _); var=debug_var }) as old ->
          debug ". . find(%a)= %a@." Lang.F.pp_var var Lang.F.pp_var debug_var ;
          root := old ;
          old
      | Some ({ kind=(Node _) } as node) ->
          debug ". . find(%a)=" Lang.F.pp_var var ;
          let rec find_aux node =
            debug " %a" Lang.F.pp_var node.var ;
            match node.kind with
            | Node y ->
                let r = find_aux y in