cubetrie.ml

(**************************************************************************)
(*                                                                        *)
(*                              Cubicle                                   *)
(*                                                                        *)
(*                       Copyright (C) 2011-2014                          *)
(*                                                                        *)
(*                  Sylvain Conchon and Alain Mebsout                     *)
(*                       Universite Paris-Sud 11                          *)
(*                                                                        *)
(*                                                                        *)
(*  This file is distributed under the terms of the Apache Software       *)
(*  License version 2.0                                                   *)
(*                                                                        *)
(**************************************************************************)

open Options
open Util
open Types
open Ast

module H = Hstring

(* Trie, mapping cubes to value of type 'a *)
type 'a t = 
  | Empty
  | Full of 'a
  | Node of (Atom.t * 'a t) list

let empty = Empty

(* Test emptiness of a trie *)
let is_empty = function
  | Empty -> true
  | _ -> false

(* Add a mapping cube->v to trie *)
let rec add cube v trie = match trie with
  | Empty -> List.fold_right (fun a t -> Node [a,t]) cube (Full v)
  | Full _ -> trie
  | Node l -> match cube with
      | [] -> Full v
      | atom::cube -> Node (add_to_list atom cube v l)
and add_to_list atom cube v l = match l with
  | [] -> [atom, add cube v Empty]
  | (atom',t')::n ->
      let cmp = Atom.compare atom atom' in
      if cmp = 0 then (atom, add cube v t')::n
      else if cmp > 0 then (atom',t')::(add_to_list atom cube v n)
      else (atom, add cube v Empty)::l

(* Add a mapping cube->v to trie without checking for subsomption *)
let rec add_force cube v trie = match trie with
  | Empty -> List.fold_right (fun a t -> Node [a,t]) cube (Full v)
  | Full _ -> trie
  | Node l -> match cube with
      | [] -> Full v
      | atom::cube -> Node (add_force_to_list atom cube v l)
and add_force_to_list atom cube v l = match l with
  | [] -> [atom, add_force cube v Empty]
  | (atom',t')::n ->
      let cmp = Atom.compare atom atom' in
      if cmp > 0 then (atom',t')::(add_force_to_list atom cube v n)
      else (atom, add_force cube v Empty)::l

(* (\* Add a mapping cube->v to trie *\) *)
(* let rec add_array cube v trie = match trie with *)
(*   | Empty -> Array.fold_right (fun a t -> Node [a,t]) cube (Full v) *)
(*   | Full _ -> trie *)
(*   | Node l ->  *)
(*       if Array.length cube = 0 then Full v *)
(*       else Node (add_array_to_list  *)
(*                    cube.(0) (Array.sub cube 1 (Array.length cube - 1)) *)
(*                    v l) *)
(* and add_array_to_list atom cube v l = match l with *)
(*   | [] -> [atom, add_array cube v Empty] *)
(*   | (atom',t')::n -> *)
(*       let cmp = Atom.compare atom atom' in *)
(*       if cmp = 0 then (atom, add_array cube v t')::n *)
(*       else if cmp > 0 then (atom',t')::(add_array_to_list atom cube v n) *)
(*       else (atom, add_array cube v Empty)::l *)

(* (\* Add a mapping cube->v to trie without checking for subsomption *\) *)
(* let rec add_array_force cube v trie = match trie with *)
(*   | Empty -> Array.fold_right (fun a t -> Node [a,t]) cube (Full v) *)
(*   | Full _ -> trie *)
(*   | Node l ->  *)
(*       if Array.length cube = 0 then Full v *)
(*       else Node (add_array_force_to_list  *)
(*                    cube.(0) (Array.sub cube 1 (Array.length cube - 1)) *)
(*                    v l) *)
(* and add_array_force_to_list atom cube v l = match l with *)
(*   | [] -> [atom, add_array_force cube v Empty] *)
(*   | (atom',t')::n -> *)
(*       let cmp = Atom.compare atom atom' in *)
(*       if cmp > 0 then (atom',t')::(add_array_force_to_list atom cube v n) *)
(*       else (atom, add_array_force cube v Empty)::l *)


let add_array cube v trie = add (Array.to_list cube) v trie

let add_array_force cube v trie = add_force (Array.to_list cube) v trie

(* Is cube subsumed by some cube in the trie? *)
let rec mem cube trie = match trie with 
  | Empty -> None
  | Full { tag = id } -> Some [id]
  | Node l -> match cube with
      | [] -> None
      | atom::cube -> 
          mem_list atom cube l
and mem_list atom cube l = match l with
  | [] -> None
  | (atom',t')::n ->
      (* let cmp = Atom.compare atom atom' in *)
      let cmp = - (Atom.trivial_is_implied atom' atom) in
      if cmp = 0 then match mem cube t' with
        | Some _ as r -> r
        | None -> match cube with
            | [] -> None
            | atom::cube -> mem_list atom cube l
      else if cmp > 0 then mem_list atom cube n
      else match cube with
          | [] -> None
          | atom::cube -> mem_list atom cube l

let rec mem_poly cube trie = match trie with 
  | Empty -> false
  | Full _ -> true
  | Node l -> match cube with
      | [] -> false
      | atom::cube -> 
          mem_poly_list atom cube l
and mem_poly_list atom cube l = match l with
  | [] -> false
  | (atom',t')::n ->
      (* let cmp = Atom.compare atom atom' in *)
      let cmp = - (Atom.trivial_is_implied atom' atom) in
      if cmp = 0 then match mem_poly cube t' with
        | true -> true
        | false -> match cube with
            | [] -> false
            | atom::cube -> mem_poly_list atom cube l
      else if cmp > 0 then mem_poly_list atom cube n
      else match cube with
          | [] -> false
          | atom::cube -> mem_poly_list atom cube l

(* (\* Is cube subsumed by some cube in the trie? *\) *)
(* let rec mem_array cube trie =  *)
(*   match trie with  *)
(*   | Empty -> None *)
(*   | Full { tag = id } -> Some [id] *)
(*   | Node l -> *)
(*       if Array.length cube = 0 then None *)
(*       else mem_array_list *)
(*         cube.(0) (Array.sub cube 1 (Array.length cube - 1)) l *)
(* and mem_array_list atom cube l = match l with *)
(*   | [] -> None *)
(*   | (atom',t')::n -> *)
(*       (\* let cmp = Atom.compare atom atom' in *\) *)
(*       let cmp = - (Atom.trivial_is_implied atom' atom) in *)
(*       if cmp = 0 then  *)
(*         match mem_array cube t' with *)
(*           | None ->  *)
(*               if Array.length cube = 0 then None *)
(*               else mem_array_list *)
(*                 cube.(0) (Array.sub cube 1 (Array.length cube - 1)) l *)
(*           | Some _ as r -> r *)
(*       else if cmp > 0 then mem_array_list atom cube n *)
(*       else if Array.length cube = 0 then None *)
(*       else mem_array_list *)
(*         cube.(0) (Array.sub cube 1 (Array.length cube - 1)) l *)


let mem_array a trie = mem (Array.to_list a) trie

(* (\* Is cube subsumed by some cube in the trie? *\) *)
(* let rec mem_array_poly cube trie =  *)
(*   match trie with  *)
(*   | Empty -> false *)
(*   | Full _ -> true *)
(*   | Node l -> *)
(*       if Array.length cube = 0 then false *)
(*       else mem_array_poly_list *)
(*         cube.(0) (Array.sub cube 1 (Array.length cube - 1)) l *)
(* and mem_array_poly_list atom cube l = match l with *)
(*   | [] -> false *)
(*   | (atom',t')::n -> *)
(*       (\* let cmp = Atom.compare atom atom' in *\) *)
(*       let cmp = - (Atom.trivial_is_implied atom' atom) in *)
(*       if cmp = 0 then  *)
(*         mem_array_poly cube t' || *)
(*           (Array.length cube <> 0 && *)
(*              mem_array_poly_list *)
(*                cube.(0) (Array.sub cube 1 (Array.length cube - 1)) l *)
(*           ) *)
(*       else if cmp > 0 then mem_array_poly_list atom cube n *)
(*       else (Array.length cube <> 0 && *)
(*               mem_array_poly_list *)
(*                 cube.(0) (Array.sub cube 1 (Array.length cube - 1)) l) *)

let mem_array_poly a trie = mem_poly (Array.to_list a) trie

let mem c t =
  TimerSubset.start ();
  let res = mem c t in
  TimerSubset.pause ();
  res
   
(* Apply f to all values mapped to in the trie. *)
let rec iter f trie = match trie with
  | Empty -> ()
  | Full v -> f v
  | Node l -> List.iter (fun (_,t) -> iter f t) l

let mem_array c t =
  (* Format.eprintf "memarray %a in@." Pretty.print_array c; *)
  (* iter (fun s -> Format.eprintf ">>> %a\n@." Pretty.print_array s.t_arru) t; *)
  TimerSubset.start ();
  let res = mem_array c t in
  TimerSubset.pause ();
  res

(* Fold f to all values mapped to in the trie. *)
let rec fold f acc trie = match trie with
  | Empty -> acc
  | Full v -> f acc v
  | Node l -> List.fold_left (fun acc (_,t) -> fold f acc t) acc l

(* Apply f to all values whose keys (cubes) are subsumed by the given cube. *)
let rec iter_subsumed f cube trie = match cube, trie with
  | [], _ -> iter f trie
  | _, Empty 
  | _, Full _ -> () 
  | _, Node l -> iter_subsumed_list f cube l
and iter_subsumed_list f cube l = match l with
  | [] -> ()
  | (atom',t')::n ->
      let atom = List.hd cube in
      let cmp = Atom.compare atom atom' in
      if cmp=0 then 
        iter_subsumed f (List.tl cube) t'
      else if cmp>0 then begin
        iter_subsumed f cube t';
        iter_subsumed_list f cube n 
      end

(* Delete all values which satisfy the predicate p *)
let rec delete p trie = match trie with 
  | Empty -> Empty
  | Full v -> if p v then Empty else trie
  | Node l -> 
      let l' = delete_list p l in
      if l == l' then trie else Node l'
and delete_list p l = match l with
  | [] -> []
  | (atom, t):: n ->
      let t' = delete p t in
      let n' = delete_list p n in
      if t'==t && n'==n then l else (atom,t')::n'


(* List of all values mapped by the trie *)
let rec all_vals = function
  | Empty -> []
  | Full v -> [v]
  | Node l -> 
      List.flatten (List.fold_left (fun acc (_,t) -> (all_vals t)::acc) [] l)

(* All values whose keys (cubes) are not inconsistent with the given cube. *)
let rec consistent cube trie = match cube, trie with
  | [], _ -> all_vals trie
  | _, Empty -> []
  | _, Full v -> [v]
  | (atom::cube), Node l -> List.flatten (List.map (consistent_list atom cube) l)
and consistent_list atom cube ((atom', t') as n) = match (atom, atom') with
  | Atom.Comp (Elem (v1, Glob), Eq, Elem (x1, Constr)),
    Atom.Comp (Elem (v2, Glob), Eq, Elem (x2, Constr))
  | Atom.Comp (Elem (v1, Glob), Eq, Elem (x1, Var)),
    Atom.Comp (Elem (v2, Glob), Eq, Elem (x2, Var)) 
      when H.equal v1 v2 && not (H.equal x1 x2) ->
      []
  | Atom.Comp (Elem (v1, Glob), Eq, Elem (x1, Constr)),
    Atom.Comp (Elem (v2, Glob), (Neq|Lt), Elem (x2, Constr))
      when H.equal v1 v2 && H.equal x1 x2 ->
      []
  | Atom.Comp (Access (a1,li1), Eq, (Elem (_,(Constr|Glob)) | Arith _ as x1)),
    Atom.Comp (Access (a2,li2), Eq, (Elem (_,(Constr|Glob)) | Arith _ as x2))
      when H.equal a1 a2 && H.list_equal li1 li2 && Term.compare x1 x2 <> 0 ->
      []
  | Atom.Comp (Access (a1,li1), Eq,
               (Elem (_, (Constr|Glob)) | Arith _ as x1)),
    Atom.Comp (Access (a2,li2), (Neq | Lt), 
               (Elem (_, (Constr|Glob)) | Arith _ as x2))
      when H.equal a1 a2 && H.list_equal li1 li2 && Term.compare x1 x2 = 0 ->
      []
  | _, _ ->
      let cmp = Atom.compare atom atom' in
      if cmp = 0 then consistent cube t'
      else if cmp < 0 then match cube with
        | [] -> all_vals t'
        | atom::cube -> consistent_list atom cube n
      else consistent (atom::cube) t'


let rec add_and_resolve n visited =
  let visited =
    fold (fun visited nv ->
      match Cube.resolve_two n.cube nv.cube with
        | None -> visited
        | Some cube_res -> add_and_resolve (Node.create cube_res) visited
    ) visited visited in
  add_array (Node.array n) n visited

let delete_subsumed ?(cpt=ref 0) p nodes =
  let vars, ap = Node.variables p, Node.array p in
  let substs = Variable.all_permutations vars vars in
  List.iter (fun ss ->
    let u = ArrayAtom.apply_subst ss ap in
    iter_subsumed (fun n ->
      if Node.has_deleted_ancestor n || not (Node.ancestor_of n p) then begin
        n.deleted <- true;
        if dot then Dot.delete_node_by n p;
        incr cpt;
      end
    ) (Array.to_list u) nodes;
  ) substs;
  (* iter (fun n -> if Node.has_deleted_ancestor n then *)
  (*       n.deleted <- true; *)
  (*       ) nodes; *)
  delete (fun n -> n.deleted || Node.has_deleted_ancestor n) nodes


let add_node p trie = add_array (Node.array p) p trie