[dt] heuristic on list length in paths

src/discrimination_tree.ml

@@ -87,21 +87,14 @@ let pp_cell fmt n =
   else Format.fprintf fmt "%o" k
 
 let show_cell n = Format.asprintf "%a" pp_cell n
-module Path : sig
-  type t
-  val pp : Format.formatter -> t -> unit
-  val get : t -> int -> cell
-  type builder
-  val make : int -> cell -> builder
-  val emit : builder -> cell -> unit
-  val stop : builder -> t
-  val of_list : cell list -> t
-
-end = struct
+
+module Path = struct
  type t = cell array [@@deriving show]
  let get a i = a.(i)
 
+
  type builder = { mutable pos : int; mutable path : cell array }
+ let get_builder_pos {pos} = pos
  let make size e = { pos = 0; path = Array.make size e }
  let rec emit p e = 
     let len = Array.length p.path in
@@ -285,17 +278,18 @@ let skip_listTailVariable ~pos path : int =
     In the example it is no needed to index the goal path to depth 100, but rather considering
     the maximal depth of the first argument, which 4 << 100
   *)
-type 'a t = {t: 'a Trie.t; max_size : int;  max_depths : int array } 
+type 'a t = {t: 'a Trie.t; max_size : int;  max_depths : int array; max_list_length: int } 
 
 let pp pp_a fmt { t } : unit = Trie.pp (fun fmt data -> pp_a fmt data) fmt t
 let show pp_a { t } : string = Trie.show (fun fmt data -> pp_a fmt data) t
 
-let index { t; max_size; max_depths } path data =
+let index { t; max_size; max_depths; max_list_length = mll } ~max_list_length path data =
   let t, m = Trie.add path data t in
-  { t; max_size = max max_size m; max_depths }
+  { t; max_size = max max_size m; max_depths; max_list_length = max max_list_length mll }
 
 let max_path { max_size } = max_size
 let max_depths { max_depths } = max_depths 
+let max_list_length { max_list_length } = max_list_length
 
 (* the equivalent of skip, but on the index, thus the list of trees
     that are rooted just after the term represented by the tree root
@@ -389,7 +383,7 @@ and on_all_children ~pos ~add_result mode path map =
 
 let empty_dt args_depth : 'a t =
   let max_depths = Array.make (List.length args_depth) 0 in
-  {t = Trie.empty; max_depths; max_size = 0}
+  {t = Trie.empty; max_depths; max_size = 0; max_list_length=0}
 
 let retrieve ~pos ~add_result path index =
   let mode = Path.get path pos in

src/discrimination_tree.mli

@@ -4,6 +4,7 @@ module Path : sig
   val pp : Format.formatter -> t -> unit
   val get : t -> int -> cell
   type builder
+  val get_builder_pos : builder -> int
   val make : int -> cell -> builder
   val emit : builder -> cell -> unit
   val stop : builder -> t
@@ -31,9 +32,10 @@ type 'a t
 
     @note: in the elpi runtime, there are no two rule having the same [~time]
 *)
-val index : 'a t -> Path.t -> 'a -> 'a t
+val index : 'a t -> max_list_length:int -> Path.t -> 'a -> 'a t
 
 val max_path : 'a t -> int
+val max_list_length : 'a t -> int
 val max_depths : 'a t -> int array
 
 val empty_dt : 'b list -> 'a t

src/runtime.ml

@@ -2507,8 +2507,33 @@ let hash_arg_list is_goal hd ~depth args mode spec =
 let hash_clause_arg_list = hash_arg_list false
 let hash_goal_arg_list = hash_arg_list true
 
+(*  returns the maximal length of any sub_list
+    this operation is done at compile time per each clause being index
+    for example the term (app['a','b',app['c','d','e'], 'f', app['a','b','c','d','e','f']])
+    has three lists L1 = ['a','b',app['c','d','e'], 'f', app['a','b','c','d','e','f']
+                    L2 = ['c','d','e']
+                    L3 = app['a','b','c','d','e','f']
+    and the longest one has length 6
+*)
+let rec max_list_length acc = function
+  | Nil -> acc
+  | Cons (a, (UVar (_, _, _) | AppUVar (_, _, _) | Arg (_, _)|AppArg (_, _))) -> 
+      let alen = max_list_length 0 a in
+      max (acc+2) alen
+  | Cons (a, b)-> 
+      let alen = max_list_length 0 a in
+      let blen = max_list_length (acc+1) b in 
+      max blen alen
+  | App (_,x,xs) -> List.fold_left (fun acc x -> max acc (max_list_length 0 x)) acc (x::xs)
+  | Builtin (_, xs) -> List.fold_left (fun acc x -> max acc (max_list_length 0 x)) acc xs
+  | Lam t -> max_list_length acc t
+  | Discard | Const _ |CData _ -> acc
+  | UVar (_, _, _) | AppUVar (_, _, _) | Arg (_, _)|AppArg (_, _) -> acc
+
+let max_lists_length = List.fold_left (fun acc e -> max (max_list_length 0 e) acc) 0
+
 (** 
-  [arg_to_trie_path ~safe ~depth ~is_goal args arg_depths arg_modes]
+  [arg_to_trie_path ~safe ~depth ~is_goal args arg_depths arg_modes mp max_list_length]
   returns the path represetation of a term to be used in indexing with trie.
   args, args_depths and arg_modes are the lists of respectively the arguments, the 
   depths and the modes of the current term to be indexed.
@@ -2517,10 +2542,14 @@ let hash_goal_arg_list = hash_arg_list true
   In the former case, each argument we add a special mkInputMode/mkOutputMode 
   node before each argument to be indexed. This special node is used during 
   instance retrival to know the mode of the current argument
+  - mp is the max_path size of any path in the index used to truncate the goal
+  - max_list_length is the length of the longest sublist in each term of args 
 *)
-let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode mp : Discrimination_tree.Path.t =
+let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode mp (max_list_length':int) : Discrimination_tree.Path.t =
   let open Discrimination_tree in
-  let path = Path.make (max mp 8) mkPathEnd in
+
+  let path_length = mp + Array.length args_depths_ar + 1 in
+  let path = Path.make path_length mkPathEnd in
 
   let current_ar_pos = ref 0 in
   let current_user_depth = ref 0 in
@@ -2537,7 +2566,7 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m
     end
   in
 
-  let rec list_to_trie_path ~safe ~depth ?(h=0) path_depth (len: int) (t: term) : unit =
+  let rec list_to_trie_path ~safe ~depth ~h path_depth (len: int) (t: term) : unit =
     match deref_head ~depth t with
     | Nil -> Path.emit path mkListEnd; update_current_min_depth path_depth
     | Cons (a, b) ->
@@ -2549,7 +2578,7 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m
         (*              has the node `app` with arity `1` as first*)
         (*              cell, then come the elment of the list    *)
         (*              up to the 30^th elemebt                   *)
-        if h > 30 then (Path.emit path mkListEnd; update_current_min_depth path_depth)
+        if is_goal && h >= max_list_length' then (Path.emit path mkListEnd; update_current_min_depth path_depth)
         else
           (main ~safe ~depth a path_depth;
           list_to_trie_path ~depth ~safe ~h:(h+1) path_depth (len+1) b)
@@ -2578,6 +2607,8 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m
   (** gives the path representation of a term *)
   and main ~safe ~depth t path_depth : unit =
     if path_depth = 0 then update_current_min_depth path_depth
+    else if Path.get_builder_pos path >= path_length then 
+      (Path.emit path mkVariable; update_current_min_depth path_depth)
     else
       let path_depth = path_depth - 1 in 
       match deref_head ~depth t with 
@@ -2601,7 +2632,7 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m
       | Cons (x,xs) ->
           Path.emit path mkListHead;
           main ~safe ~depth x (path_depth + 1);
-          list_to_trie_path ~safe ~depth (path_depth + 1) 0 xs
+          list_to_trie_path ~safe ~depth ~h:1 (path_depth + 1) 0 xs
 
   (** builds the sub-path of a sublist of arguments of the current clause  *)
   and make_sub_path arg_hd arg_tl arg_depth_hd arg_depth_tl mode_hd mode_tl = 
@@ -2689,9 +2720,10 @@ let add_clause_to_snd_lvl_idx ~depth ~insert predicate clause = function
 | IndexWithDiscriminationTree {mode; arg_depths; args_idx; } ->
     let max_depths = Discrimination_tree.max_depths args_idx in
     let max_path = Discrimination_tree.max_path args_idx in
-    let path = arg_to_trie_path ~depth ~safe:true ~is_goal:false clause.args arg_depths max_depths mode max_path in
+    let max_list_length = max_lists_length clause.args in
+    let path = arg_to_trie_path ~depth ~safe:true ~is_goal:false clause.args arg_depths max_depths mode max_path max_list_length in
     [%spy "dev:disc-tree:depth-path" ~rid pp_string "Inst: MaxDepths " (pplist pp_int "") (Array.to_list max_depths)];
-    let args_idx = Discrimination_tree.index args_idx path clause in
+    let args_idx = Discrimination_tree.index args_idx path clause ~max_list_length in
     IndexWithDiscriminationTree {
       mode; arg_depths;
       args_idx = args_idx
@@ -2899,8 +2931,9 @@ let get_clauses ~depth predicate goal { index = { idx = m } } =
      | IndexWithDiscriminationTree {arg_depths; mode; args_idx} ->
         let max_depths = Discrimination_tree.max_depths args_idx in
         let max_path = Discrimination_tree.max_path args_idx in
-        let (path: Discrimination_tree.Path.t) = arg_to_trie_path ~safe:false ~depth ~is_goal:true (trie_goal_args goal) arg_depths max_depths mode max_path in
-        [%spy "dev:disc-tree:depth-path" ~rid pp_string "Goal: MaxDepths " (pplist pp_int ";") (Array.to_list max_depths)];
+        let max_list_length = Discrimination_tree.max_list_length args_idx in
+        let path = arg_to_trie_path ~safe:false ~depth ~is_goal:true (trie_goal_args goal) arg_depths max_depths mode max_path max_list_length in
+        [%spy "dev:disc-tree:depth-path" ~rid pp_string "Goal: MaxDepths " (pplist pp_int ";") (Array.to_list max_depths) pp_int (max_path) pp_int max_list_length];
         (* Format.(printf "Goal: MaxDepth is %a\n" (pp_print_list ~pp_sep:(fun fmt _ -> pp_print_string fmt " ") pp_print_int) (Discrimination_tree.max_depths args_idx |> Array.to_list)); *)
         [%spy "dev:disc-tree:path" ~rid 
           Discrimination_tree.Path.pp path

src/test_discrimination_tree.ml

@@ -52,7 +52,7 @@ let () =
     (* Format.printf "%a\n" pp_path pathGoal; *)
     let pathInsts = List.map (fun (x,y) -> x @ [mkPathEnd], y) pathInsts in
     let add_to_trie t (key,value) = 
-      index t (Path.of_list key) value in
+      index t (Path.of_list key) ~max_list_length:1000 value in
     let trie = List.fold_left add_to_trie (empty_dt []) pathInsts in 
     let retrived = retrieve (fun x y -> y - x) pathGoal trie in
     let retrived_nb = Elpi.Internal.Bl.length retrived in