Source file magic.ml

open UtilsLib.Focused_list
(** Module to handle the General magic set rewriting.

see 13.6 General magic set p 861-865 of Principles of Database and
Knowledge-Base Systems II, Ullman

 *)

open DatalogLib
open Datalog
module ASPred = Datalog_AbstractSyntax.AbstractSyntax.Predicate
module ASRule = Datalog_AbstractSyntax.AbstractSyntax.Rule
module ASProg = Datalog_AbstractSyntax.AbstractSyntax.Program
module RuleIdMap = Datalog_AbstractSyntax.RuleIdMap

module Log = UtilsLib.Xlog.Make (struct
  let name = "Magic"
end)

type extra_pred_type =
  | Magic
  | Supp_zero
  | Supp_k



exception Out_of_Bound

type dot = NoDot | InExt | InInt

type dotted_rule = {
  drule_id : int;
  head : ASPred.predicate;
  head_args : ASPred.TermSet.t;
  previous_args : ASPred.TermSet.t;
  (* cont the argument of the goal pred under focust *)
  focused_e_rhs :
    (ASPred.predicate * int * ASPred.TermSet.t) Focused_list.t option;
      (** represents the extensionnal predicates of the
       rule. The [int] represents the position in the rule *)
  focused_i_rhs :
    (ASPred.predicate * int * ASPred.TermSet.t) Focused_list.t option;
  next_args : ASPred.TermSet.t;
  dot : dot;
  rhs_size : int;
  i_preds : ASPred.PredIds.t;
}

let init_opt l =
  try Some (Focused_list.init l) with Focused_list.Empty_list -> None

let get_args acc preds =
  List.fold_left
    (fun args (p, _) ->
      List.fold_left
        (fun acc arg -> ASPred.TermSet.add arg acc)
        args p.ASPred.arguments)
    acc preds

let init_rule r =
  let dot, previous_args, next_args =
    match (r.ASRule.e_rhs, r.ASRule.i_rhs) with
    | [], [] -> (NoDot, ASPred.TermSet.empty, ASPred.TermSet.empty)
    | [], (g, _) :: tl ->
        ( InInt,
          ASPred.(TermSet.of_list g.arguments),
          get_args ASPred.TermSet.empty tl )
    | (g, _) :: tl, i_rhs ->
        ( InExt,
          ASPred.(TermSet.of_list g.arguments),
          get_args (get_args ASPred.TermSet.empty tl) i_rhs )
  in
  (* We ensure that the rhs predicates are ordered according to their position *)
  let () =
    assert (
      List.sort (fun (_, p1) (_, p2) -> p1 - p2) r.ASRule.e_rhs = r.ASRule.e_rhs)
  in
  let () =
    assert (
      List.sort (fun (_, p1) (_, p2) -> p1 - p2) r.ASRule.i_rhs = r.ASRule.i_rhs)
  in
  {
    drule_id = r.ASRule.id;
    head = r.ASRule.lhs;
    head_args = ASPred.TermSet.of_list r.ASRule.lhs.ASPred.arguments;
    previous_args;
    focused_e_rhs =
      init_opt
        (List.map
           (fun (pred, pos) ->
             (pred, pos, ASPred.TermSet.of_list pred.ASPred.arguments))
           r.ASRule.e_rhs);
    focused_i_rhs =
      init_opt
        (List.map
           (fun (pred, pos) ->
             (pred, pos, ASPred.TermSet.of_list pred.ASPred.arguments))
           r.ASRule.i_rhs);
    next_args;
    dot;
    rhs_size = r.ASRule.rhs_num;
    i_preds =
      List.fold_left
        (fun acc (pred, _) -> ASPred.(PredIds.add pred.p_id acc))
        ASPred.PredIds.empty r.ASRule.i_rhs;
  }

let right r =
  match (r.dot, r.focused_e_rhs, r.focused_i_rhs) with
  | NoDot, _, _ -> raise Out_of_Bound
  | InExt, None, _ -> failwith "Bug: InExt should not be set if e_rhs is empty"
  | InExt, Some e_rhs, None -> (
      try
        let e_rhs' = Focused_list.forward e_rhs in
        {
          r with
          dot = InExt;
          focused_e_rhs = Some e_rhs';
          previous_args =
            (let _, _, args = Focused_list.focus e_rhs' in
             ASPred.TermSet.union args r.previous_args);
          next_args =
            Focused_list.fold_forward ~include_focus:false
              (fun acc (_, _, args) -> ASPred.TermSet.union args acc)
              ASPred.TermSet.empty e_rhs';
        }
      with Focused_list.End_of_list -> raise Out_of_Bound)
  | InExt, Some e_rhs, Some i_rhs -> (
      try
        let e_rhs' = Focused_list.forward e_rhs in
        {
          r with
          dot = InExt;
          focused_e_rhs = Some e_rhs';
          previous_args =
            (let _, _, args = Focused_list.focus e_rhs' in
             ASPred.TermSet.union args r.previous_args);
          next_args =
            Focused_list.fold_forward
              (fun acc (_, _, args) -> ASPred.TermSet.union args acc)
              (Focused_list.fold_forward ~include_focus:false
                 (fun acc (_, _, args) -> ASPred.TermSet.union args acc)
                 ASPred.TermSet.empty e_rhs')
              i_rhs;
        }
      with Focused_list.End_of_list ->
        {
          r with
          dot = InInt;
          focused_i_rhs = Some i_rhs;
          previous_args =
            (let _, _, args = Focused_list.focus i_rhs in
             ASPred.TermSet.union args r.previous_args);
          next_args =
            Focused_list.fold_forward ~include_focus:false
              (fun acc (_, _, args) -> ASPred.TermSet.union args acc)
              ASPred.TermSet.empty i_rhs;
        })
  | InInt, _, None -> failwith "Bug: InInt should not be set if i_rhs is empty"
  | InInt, _, Some i_rhs -> (
      try
        let i_rhs' = Focused_list.forward i_rhs in
        {
          r with
          dot = InInt;
          focused_i_rhs = Some i_rhs';
          previous_args =
            (let _, _, args = Focused_list.focus i_rhs' in
             ASPred.TermSet.union args r.previous_args);
          next_args =
            Focused_list.fold_forward ~include_focus:false
              (fun acc (_, _, args) -> ASPred.TermSet.union args acc)
              ASPred.TermSet.empty i_rhs';
        }
      with Focused_list.End_of_list -> raise Out_of_Bound)

let focus r =
  match r.dot with
  | NoDot -> raise Out_of_Bound
  | InExt -> (
      match r.focused_e_rhs with
      | None -> failwith "Bug: an extensional predicate should be focused on"
      | Some e_rhs -> Focused_list.focus e_rhs)
  | InInt -> (
      match r.focused_i_rhs with
      | None -> failwith "Bug: an intensional predicate should be focused on"
      | Some i_rhs -> Focused_list.focus i_rhs)

let supplementary_name_pattern rule_id position =
  Printf.sprintf "sup_%d_%d" rule_id position

let magic_name_pattern s = Printf.sprintf "m_%s" s

(* CHECK: revoir la doc *)

(** [add_sup_rule ~previous_sup_pred r magic_prog] returns a pair
   [magic_prog',new_sup_pred] where [magic_prog'] is [magic_prog]
   updated by adding a new supplementary rule as follows: if [r] is a
   dotted rule focusing on [P_k^{ador_k}], the rule
   [sup_r_id_k(x'_k):-previous_sup_pred,P_k_ador] where
   [previous_sup_pred] is [sup_r_id_{k-1}(x'_{k-1}]. [x'_k] is defined
   as the union of the variables occurring in the head of [r] and
   variables that appear both in predicates at position between [1]
   and [k-1] and variables occuring as args of predicates at position
   between [k] and [n] ([P_n] being the last predicate of the rule,
   and [P_1] the first one). [new_sup_pred] is the new supplementary
   predicate.

   See
   https://gitlab.inria.fr/ACG/student-projects/2018-2019-m1/-/blob/master/project_report.pdf
   p19, paragraph "Création de règles pour les autres prédicats
   supplémentaires"

 *)
let add_sup_rule ~previous_sup_pred r (magic_prog, extra_preds, rule_to_rule_map)
  =
  let pp_args fmt args = ASPred.pp_terms magic_prog.ASProg.const_table fmt args in
  let () =
    Log.debug (fun m ->
        m "The position of the focused pred in add_sup_rule is: %d"
          (let _focused_pred, pos, _ = focus r in
           pos))
  in
  let () = Log.debug (fun m -> m "Head arguments are: @[%a@]" pp_args r.head_args) in
  let () = Log.debug (fun m -> m "Previous arguments are: @[%a@]" pp_args r.previous_args) in
  let () = Log.debug (fun m -> m "Next arguments are: @[%a@]" pp_args r.next_args) in
  let new_sup_pred_args =
    ASPred.TermSet.(union r.head_args (inter r.previous_args r.next_args))
  in
  let () = Log.debug (fun m -> m "Resulting arguments are: @[%a@]" pp_args new_sup_pred_args) in
  let new_sup_pred_args, arity =
    ASPred.TermSet.fold
      (fun arg (args, card) -> (arg :: args, card + 1))
      new_sup_pred_args ([], 0)
  in
  let new_sup_pred_args = List.rev new_sup_pred_args in
  let focused_pred, pos, _ = focus r in
  let sup_rule_id, id_gen' =
    UtilsLib.IdGenerator.IntIdGen.get_fresh_id magic_prog.ASProg.rule_id_gen
  in
  let new_sup_pred_id, pred_table' =
    ASPred.PredIdTable.add_sym
      (supplementary_name_pattern r.drule_id pos)
      magic_prog.ASProg.pred_table
  in
  let new_sup_pred =
    ASPred.{ p_id = new_sup_pred_id; arity; arguments = new_sup_pred_args }
  in
  let extra_preds = ASPred.PredIdMap.add new_sup_pred_id Supp_k extra_preds
  in
  let () =
    Log.debug (fun m ->
        m "New supplementary predicate: %a"
          (ASPred.pp pred_table'
             magic_prog.ASProg.const_table) new_sup_pred)
  in
  let e_rhs, i_rhs, i_rhs_num, is_extensional =
    if ASPred.(PredIds.mem focused_pred.p_id r.i_preds) then
      ([], [ (previous_sup_pred, 1); (focused_pred, 2) ], 2, false)
    else ([ (focused_pred, 1) ], [ (previous_sup_pred, 2) ], 1, true)
  in
  let sup_rule =
    ASRule.
      {
        id = sup_rule_id;
        lhs = new_sup_pred;
        e_rhs;
        i_rhs;
        i_rhs_num;
        rhs_num = 2;
      }
  in
  let magic_prog' =
    ASProg.
      {
        rules = ASRule.Rules.add sup_rule magic_prog.rules;
        pred_table = pred_table';
        const_table = magic_prog.const_table;
        i_preds = ASPred.PredIds.add new_sup_pred_id magic_prog.i_preds;
        rule_id_gen = id_gen';
        head_to_rules =
          ASRule.extend_head_id_map_to_rules new_sup_pred_id sup_rule
            magic_prog.head_to_rules;
        e_pred_to_rules =
          (if is_extensional then
             ASRule.extend_head_id_map_to_rules focused_pred.ASPred.p_id sup_rule
               magic_prog.e_pred_to_rules
           else magic_prog.e_pred_to_rules);
      }
  in
  let rule_to_rule_map' =
    RuleIdMap.add sup_rule_id r.drule_id rule_to_rule_map
  in
  (magic_prog', extra_preds, rule_to_rule_map', new_sup_pred)

(** [add_magic_rule ~previous_sup_pred r magic_prog] returns
   [magic_prog'] where [magic_prog'] is [magic_prog] updated by adding
   a new supplementary rule as follows: if [r] is a dotted rule
   focusing on [P_k^{ador_k}], the rule
   [m_P_k^{ador_k}:-previous_sup_pred] where [previous_sup_pred] is
   [sup_r_id_{k-1}(x'_{k-1}]. [x'_k] is defined as the union of the
   variables occurring in the head of [r] and variables that appear
   both in predicates at position between [1] and [k-1] and variables
   occuring as args of predicates at position between [k] and [n]
   ([P_n] being the last predicate of the rule, and [P_1] the first
   one). It is assumed that [P_k^{ador_k}] is an intensional
   predicate.

   See
   https://gitlab.inria.fr/ACG/student-projects/2018-2019-m1/-/blob/master/project_report.pdf
   p18, paragraph "Création des règles magiques"

 *)
let add_magic_rule ~previous_sup_pred r
    (magic_prog, extra_preds, rule_to_rule_map) =
  let focused_pred, _, _ = focus r in
  let magic_rule_id, id_gen' =
    UtilsLib.IdGenerator.IntIdGen.get_fresh_id magic_prog.ASProg.rule_id_gen
  in
  let magic_rule_head_id, pred_table' =
    ASPred.PredIdTable.add_sym
      (magic_name_pattern
         ASPred.(
           PredIdTable.find_sym_from_id focused_pred.p_id
             magic_prog.ASProg.pred_table))
      magic_prog.ASProg.pred_table
  in
  let magic_rule =
    ASRule.
      {
        id = magic_rule_id;
        lhs = ASPred.{ focused_pred with p_id = magic_rule_head_id };
        e_rhs = [];
        i_rhs = [ (previous_sup_pred, 1) ];
        i_rhs_num = 1;
        rhs_num = 1;
      }
  in
  let extra_preds = ASPred.PredIdMap.add magic_rule_head_id Magic extra_preds
  in
  let () =
    Log.debug (fun m ->
        m "Generating rule: %a"
          (ASRule.pp pred_table' magic_prog.ASProg.const_table)  magic_rule)
  in
  let rule_to_rule_map' =
    RuleIdMap.add magic_rule_id r.drule_id rule_to_rule_map
  in
  let magic_prog' =
    ASProg.
      {
        rules = ASRule.Rules.add magic_rule magic_prog.rules;
        pred_table = pred_table';
        const_table = magic_prog.const_table;
        i_preds = ASPred.PredIds.add magic_rule_head_id magic_prog.i_preds;
        rule_id_gen = id_gen';
        head_to_rules =
          ASRule.extend_head_id_map_to_rules magic_rule_head_id magic_rule
            magic_prog.head_to_rules;
        e_pred_to_rules = magic_prog.e_pred_to_rules;
      }
  in
  (magic_prog', extra_preds, rule_to_rule_map')

(** [extend_prog ~previous_sup_pred r magic_prog] returns a pair
   [magic_prog',next_data] where [magic_prog'] is [magic_prog] updated
   by adding a new magic rule and a new supplementary rule
   corresponding to the focused predicate [P_k^{ador_k}]. The magic
   rule is added only if [P_k^{ador_k}] is intensional. The
   supplementary rule is added only if [k<n] where [n] is the size ot
   the rhs of [r]. In this latter case, [next_data] is [Some
   (new_sup_pred,r')]. Otherwise it is [None].

   See
   https://gitlab.inria.fr/ACG/student-projects/2018-2019-m1/-/blob/master/project_report.pdf
   p18-19.

 *)

let extend_prog_aux ~previous_sup_pred r
    (magic_prog, extra_preds, rule_to_rule_map) =
  let focused_pred, _pos, _ = focus r in
  let () =
    Log.debug (fun m ->
        m "In extend_prog, the position of the focused pred is: %d" _pos)
  in
  let magic_prog', extra_preds', rule_to_rule_map' =
    if ASPred.(PredIds.mem focused_pred.p_id r.i_preds) then
      add_magic_rule ~previous_sup_pred r
        (magic_prog, extra_preds, rule_to_rule_map)
    else (magic_prog, extra_preds, rule_to_rule_map)
  in
  try
    let r' = right r in
    let magic_prog'', extra_preds'', rule_to_rule_map'', new_sup_pred =
      add_sup_rule ~previous_sup_pred r
        (magic_prog', extra_preds', rule_to_rule_map')
    in
    (magic_prog'', extra_preds'', rule_to_rule_map'', Some (new_sup_pred, r'))
  with Out_of_Bound -> (magic_prog', extra_preds', rule_to_rule_map', None)

let rec extend_prog ~previous_sup_pred r
    (magic_prog, extra_preds, rule_to_rule_map) =
  let focused_pred, _, _ = focus r in
  match
    extend_prog_aux ~previous_sup_pred r
      (magic_prog, extra_preds, rule_to_rule_map)
  with
  | new_prog, new_extra_preds, new_rule_to_rule_map, None ->
      ( new_prog,
        new_extra_preds,
        new_rule_to_rule_map,
        focused_pred,
        previous_sup_pred )
  | new_prog, new_extra_preds, new_rule_to_rule_map, Some (new_sup_pred, r') ->
      extend_prog ~previous_sup_pred:new_sup_pred r'
        (new_prog, new_extra_preds, new_rule_to_rule_map)

(* VÉRIFIER si nécessaire de prendre les pred map comme paramètres :
   peut-être pas car effacé lors de la réécriture des dérivations *)
let first_sup_rule r (magic_prog, extra_preds, rule_to_rule_map) =
  let () = Log.debug (fun m -> m "Generating the first supplementary rule") in
  let sup_rule_id, id_gen' =
    UtilsLib.IdGenerator.IntIdGen.get_fresh_id magic_prog.ASProg.rule_id_gen
  in
  let new_sup_pred_id, pred_table' =
    ASPred.PredIdTable.add_sym
      (supplementary_name_pattern r.drule_id 0)
      magic_prog.ASProg.pred_table
  in
  (* The arguments of the first supplementary predicate are the same
     as the head of the rule *)
  let new_sup_pred_args = ASPred.TermSet.of_list r.head.ASPred.arguments in
  let new_sup_pred_args, arity =
    ASPred.TermSet.fold
      (fun elt (args, length) -> (elt :: args, length + 1))
      new_sup_pred_args ([], 0)
  in
  let new_sup_pred =
    ASPred.
      { p_id = new_sup_pred_id; arguments = List.rev new_sup_pred_args; arity }
  in
  let extra_preds = ASPred.PredIdMap.add new_sup_pred_id Supp_zero extra_preds
  in
  let () =
    Log.debug (fun m ->
        m "Supplementary predicate: %a"
          (ASPred.pp pred_table'
             magic_prog.ASProg.const_table)  new_sup_pred)
  in
  let head_adorned_pred_sym =
    ASPred.(PredIdTable.find_sym_from_id r.head.p_id pred_table')
  in
  let first_magic_pred_id, pred_table'' =
    ASPred.PredIdTable.add_sym
      (magic_name_pattern head_adorned_pred_sym)
      pred_table'
  in
  (* The arguments of the magic predicate corresponding to the head of
     the rule are the same as the head of the rule *)
  let first_magic_pred = ASPred.{ r.head with p_id = first_magic_pred_id } in
  let extra_preds = ASPred.PredIdMap.add first_magic_pred_id Magic extra_preds
  in
  let () =
    Log.debug (fun m ->
        m "First magic predicate: %a"
          (ASPred.pp pred_table''
             magic_prog.ASProg.const_table)  first_magic_pred)
  in
  let sup_rule =
    ASRule.
      {
        id = sup_rule_id;
        lhs = new_sup_pred;
        e_rhs = [];
        i_rhs = [ (first_magic_pred, 1) ];
        i_rhs_num = 1;
        rhs_num = 1;
      }
  in
  let () =
    Log.debug (fun m ->
        m "Generating rule: %a"
          (ASRule.pp pred_table'' magic_prog.ASProg.const_table) sup_rule)
  in
  let rule_to_rule_map' =
    RuleIdMap.add sup_rule_id r.drule_id rule_to_rule_map
  in
  let magic_prog' =
    ASProg.
      {
        rules = ASRule.Rules.add sup_rule magic_prog.rules;
        pred_table = pred_table'';
        const_table = magic_prog.const_table;
        i_preds =
          ASPred.PredIds.(
            add new_sup_pred_id (add first_magic_pred_id magic_prog.i_preds));
        rule_id_gen = id_gen';
        head_to_rules =
          ASRule.extend_head_id_map_to_rules new_sup_pred_id sup_rule
            magic_prog.head_to_rules;
        e_pred_to_rules = magic_prog.e_pred_to_rules;
      }
  in
  (magic_prog', extra_preds, rule_to_rule_map', new_sup_pred)

(* ub_pred_to_original_pred means unique binding predicate to original predicate mapping *)
let derive_rules ~from:r prog (magic_prog, extra_preds, rule_to_rule_map) =
  let () =
    Log.debug (fun m ->
        m "Generating supplementary and magic predicates and rules from: %a"
          (ASRule.pp ~with_position:true magic_prog.ASProg.pred_table
             magic_prog.ASProg.const_table) r)
  in

  let dotted_rule = init_rule r in

  (* The rule head should be a new predicate in magic_prog *)
  let rule_head_sym =
    ASPred.(
      PredIdTable.find_sym_from_id dotted_rule.head.p_id prog.ASProg.pred_table)
  in
  let new_rule_head_id, new_table =
    ASPred.PredIdTable.add_sym rule_head_sym magic_prog.ASProg.pred_table
  in
  let new_head_pred =
    ASPred.{ dotted_rule.head with p_id = new_rule_head_id }
  in

  (* Generate the id for the rule P_x(x_0):-sup_r.0(x_0) (if no rhs)
     or P_x(x_0):-sup_r.{n-1}(x'_{n-1},P_n(x'_n) (otherwise) in order
     to get the same rule order as in MG & GR algo *)
  let new_rule_id, id_gen' =
    UtilsLib.IdGenerator.IntIdGen.get_fresh_id magic_prog.ASProg.rule_id_gen
  in

  (* In any case, the first supplementary rule has to be created *)
  let magic_prog', extra_preds', rule_to_rule_map', first_sup_pred =
    first_sup_rule dotted_rule
      ( ASProg.{ magic_prog with pred_table = new_table; rule_id_gen = id_gen' },
        extra_preds,
        rule_to_rule_map )
  in

  (* Check if the rule has a non empty rhs *)
  if dotted_rule.rhs_size = 0 then
    (* no other supplementary predicate is to be created, and one new rule is added *)
    let new_rule =
      ASRule.
        {
          id = new_rule_id;
          lhs = new_head_pred;
          e_rhs = [];
          i_rhs = [ (first_sup_pred, 1) ];
          i_rhs_num = 1;
          rhs_num = 1;
        }
    in
    let () =
      Log.debug (fun m ->
          m " Generating rule: %a"
            (ASRule.pp magic_prog'.ASProg.pred_table
               magic_prog'.ASProg.const_table) new_rule)
    in
    let magic_prog'' =
      ASProg.
        {
          magic_prog' with
          rules = ASRule.Rules.add new_rule magic_prog'.rules;
          i_preds =
            ASPred.PredIds.add new_rule.ASRule.lhs.ASPred.p_id
              magic_prog'.ASProg.i_preds;
          head_to_rules =
            ASRule.extend_head_id_map_to_rules new_head_pred.ASPred.p_id
              new_rule magic_prog'.head_to_rules;
        }
    in
    let rule_to_rule_map'' =
      RuleIdMap.add new_rule_id r.ASRule.id rule_to_rule_map'
    in
    (magic_prog'', extra_preds', rule_to_rule_map'')
  else
    (* We can process the goals of the rule *)
    (* TODO: rajouter la prise en compte du mapping magic_pred -> original pred *)
    let ( magic_prog'',
          extra_preds'',
          rule_to_rule_map'',
          last_pred,
          last_sup_pred ) =
      extend_prog ~previous_sup_pred:first_sup_pred dotted_rule
        (magic_prog', extra_preds', rule_to_rule_map')
    in
    let e_rhs, i_rhs, i_rhs_num, is_extensional =
      if ASPred.(PredIds.mem last_pred.p_id prog.ASProg.i_preds) then
        ([], [ (last_sup_pred, 1); (last_pred, 2) ], 2, false)
      else ([ (last_pred, 1) ], [ (last_sup_pred, 2) ], 1, true)
    in
    let new_rule =
      ASRule.
        {
          id = new_rule_id;
          lhs = new_head_pred;
          e_rhs;
          i_rhs;
          i_rhs_num;
          rhs_num = 2;
        }
    in
    let () =
      Log.debug (fun m ->
          m " Generating rule: %a"
            (ASRule.pp magic_prog''.ASProg.pred_table
               magic_prog''.ASProg.const_table) new_rule)
    in
    let magic_prog''' =
      ASProg.
        {
          magic_prog'' with
          rules = ASRule.Rules.add new_rule magic_prog''.rules;
          i_preds =
            ASPred.PredIds.add new_rule.ASRule.lhs.ASPred.p_id
              magic_prog''.ASProg.i_preds;
          head_to_rules =
            ASRule.extend_head_id_map_to_rules new_head_pred.ASPred.p_id
              new_rule magic_prog''.head_to_rules;
          e_pred_to_rules =
            (if is_extensional then
             ASRule.extend_head_id_map_to_rules last_pred.ASPred.p_id new_rule
               magic_prog''.e_pred_to_rules
            else magic_prog''.e_pred_to_rules);
        }
    in
    let rule_to_rule_map''' =
      RuleIdMap.add new_rule_id r.ASRule.id rule_to_rule_map''
    in
    (magic_prog''', extra_preds'', rule_to_rule_map''')

let make_magic prog (*unique_binding_pred_to_original_pred_map*) =
  ASRule.Rules.fold
    (fun r acc -> derive_rules ~from:r prog acc)
    prog.ASProg.rules
    ( ASProg.
        {
          prog with
          rules = ASRule.Rules.empty;
          rule_id_gen = UtilsLib.IdGenerator.IntIdGen.init ();
          head_to_rules = ASPred.PredIdMap.empty;
          e_pred_to_rules = ASPred.PredIdMap.empty;
        },
      ASPred.PredIdMap.empty,
      RuleIdMap.empty )

let query_to_seed query program =
  (*We build the adornment of term*)
  let bfs, _ = Adornment.adornment ~bound_variables:ASPred.TermSet.empty query in
  (* p_alpha *)
  let adorn_name = Adornment.adorned_predicate_to_string ~pred_table:program.ASProg.pred_table (query, bfs) in
(*    Adorned_predicate.string_of_ad_pred (query, bfs) program.ASProg.pred_table
      in *)
  (* the adorned query should already be in the magic program *)
  let () = assert
    (match ASPred.PredIdTable.find_id_of_sym_opt adorn_name program.ASProg.pred_table with
     | None -> false
     | Some _ -> true) in
  (* the corresponding magic predicate as well *)
  let magic_pred_id = ASPred.PredIdTable.find_id_of_sym (magic_name_pattern adorn_name) program.ASProg.pred_table in
  let magic_pred = ASPred.({query with p_id = magic_pred_id }) in
  let new_id, new_gen =
    UtilsLib.IdGenerator.IntIdGen.get_fresh_id program.ASProg.rule_id_gen
  in
  let seed =
    ASRule.
      {
        id = new_id;
        lhs = magic_pred;
        e_rhs = [];
        i_rhs = [];
        i_rhs_num = 0;
        rhs_num = 0;
      }
  in
  ASProg.
    {
      rules = ASRule.Rules.add seed program.rules;
      pred_table = program.pred_table;
      const_table = program.const_table;
      i_preds = program.i_preds;
      rule_id_gen = new_gen;
      head_to_rules =
        ASRule.extend_head_id_map_to_rules magic_pred.ASPred.p_id seed
          program.head_to_rules;
      e_pred_to_rules = program.e_pred_to_rules;
    }

(* We now assume that query is already a magic predicate *)
let query_to_seed_concrete query program =
  let query_name =
    ASPred.PredIdTable.find_sym_from_id query.ASPred.p_id
      program.Datalog.Program.pred_table
  in
  let magic_pred  =
    let magic_name = magic_name_pattern query_name in
    try
      let id_of_magic_name =
        ASPred.PredIdTable.find_id_of_sym magic_name
          program.Datalog.Program.pred_table
      in
      { query with ASPred.p_id = id_of_magic_name }
    with ASPred.PredIdTable.CT_Not_found ->
      failwith
        (Printf.sprintf
           "Bug: The magic adorned predicate '%s' (adorn name: '%s') for the \
            query should already be in the table of intensional predicates"
           magic_name query_name)
  in
  let new_id, new_gen =
    UtilsLib.IdGenerator.IntIdGen.get_fresh_id
      program.Datalog.Program.rule_id_gen
  in
  let seed =
    ASRule.
      {
        id = new_id;
        lhs = magic_pred;
        e_rhs = [];
        i_rhs = [];
        i_rhs_num = 0;
        rhs_num = 0;
      }
  in
  Datalog.Program.(
    add_rule ~intensional:true seed { program with rule_id_gen = new_gen })