helm/software/components/ng_paramodulation/paramod.ml

   1 (*let nparamod metasenv subst context t table =
   2   prerr_endline "========================================";
   3   let module C = struct
   4     let metasenv = metasenv
   5     let subst = subst
   6     let context = context
   7   end
   8   in
   9   let module B = NCicBlob.NCicBlob(C) in
  10   let module Pp = Pp.Pp (B) in
  11   let module FU = FoUnif.Founif(B) in
  12   let module IDX = Index.Index(B) in
  13   let module Sup = Superposition.Superposition(B) in
  14   let module Utils = FoUtils.Utils(B) in*)
  15 (*
  16   let test_unification _ = function
  17     | Terms.Node [_; _; lhs; rhs] ->
  18         prerr_endline "Unification test :";
  19         prerr_endline (Pp.pp_foterm lhs);
  20         prerr_endline (Pp.pp_foterm rhs);
  21         FU.unification [] [] lhs rhs
  22     | _ -> assert false
  23   in
  24   let subst,vars = test_unification [] res in
  25     prerr_endline "Result :";
  26     prerr_endline (Pp.pp_foterm res);
  27     prerr_endline "Substitution :";
  28     prerr_endline (Pp.pp_substitution subst)
  29 *)
  30 (*
  31
  32   let mk_clause maxvar t =
  33     let ty = B.embed t in
  34     let proof = B.embed (NCic.Rel ~-1) in
  35     Utils.mk_unit_clause maxvar ty proof
  36   in
  37   let clause, maxvar = mk_clause 0 t in
  38   prerr_endline "Input clause :";
  39   prerr_endline (Pp.pp_unit_clause clause);
  40   let bag = Utils.empty_bag in
  41   let active_clauses, maxvar =
  42     List.fold_left
  43       (fun (cl,maxvar) t ->
  44          let c, m = mk_clause maxvar t in
  45          c::cl, m)
  46       ([],maxvar) table
  47   in
  48   let table =
  49     List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
  50   in
  51   prerr_endline "Active table:";
  52   List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
  53   let bag, maxvar, _, newclauses =
  54     Sup.infer_right bag maxvar clause (active_clauses, table)
  55   in
  56   prerr_endline "Output clauses :";
  57   List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
  58   (* prerr_endline "Proofs: ";
  59   prerr_endline (Pp.pp_bag bag); *)
  60   prerr_endline "========================================";
  61 ;;
  62 *)
  63 let debug s =
  64   prerr_endline s
  65 ;;
  66
  67 let nparamod metasenv subst context t table =
  68   prerr_endline "========================================";
  69   let module C = struct
  70     let metasenv = metasenv
  71     let subst = subst
  72     let context = context
  73   end
  74   in
  75   let module B = NCicBlob.NCicBlob(C) in
  76   let module Pp = Pp.Pp (B) in
  77   let module FU = FoUnif.Founif(B) in
  78   let module IDX = Index.Index(B) in
  79   let module Sup = Superposition.Superposition(B) in
  80   let module Utils = FoUtils.Utils(B) in
  81
  82   let module OrderedPassives =
  83       struct
  84         type t = B.t Terms.passive_clause
  85
  86         let compare = Utils.compare_passive_clauses
  87       end
  88   in
  89   let module PassiveSet = Set.Make(OrderedPassives)
  90   in
  91   let add_passive_clause passives cl =
  92     PassiveSet.add (Utils.mk_passive_clause cl) passives
  93   in
  94     (* TODO : fairness condition *)
  95   let select passives =
  96     if PassiveSet.is_empty passives then None
  97     else let cl = PassiveSet.min_elt passives in
  98       Some (snd cl,PassiveSet.remove cl passives)
  99   in
 100   let rec given_clause bag maxvar actives passives g_actives g_passives =
 101
 102     (* keep goals demodulated w.r.t. actives and check if solved *)
 103     (* we may move this at the end of infer_right *)
 104     let bag, g_actives =
 105       List.fold_left
 106         (fun (bag,acc) c ->
 107            let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
 108              bag, c::acc)
 109         (bag,[]) g_actives
 110     in
 111
 112       (* superposition left, simplifications on goals *)
 113       debug "infer_left step...";
 114       let bag, maxvar, g_actives, g_passives =
 115         match select g_passives with
 116       | None -> bag, maxvar, g_actives, g_passives
 117       | Some (g_current, g_passives) ->
 118           debug ("Selected goal : " ^ Pp.pp_unit_clause g_current);
 119           let bag, g_current =
 120             Sup.simplify_goal maxvar (snd actives) bag g_current
 121           in
 122           let bag, maxvar, new_goals =
 123             Sup.infer_left bag maxvar g_current actives
 124           in
 125           let new_goals = List.fold_left add_passive_clause
 126             PassiveSet.empty new_goals
 127           in
 128           bag, maxvar, g_current::g_actives,
 129           (PassiveSet.union new_goals g_passives)
 130     in
 131       prerr_endline
 132         (Printf.sprintf "Number of active goals : %d"
 133            (List.length g_actives));
 134       prerr_endline
 135         (Printf.sprintf "Number of passive goals : %d"
 136            (PassiveSet.cardinal g_passives));
 137
 138       (* forward step *)
 139
 140       (* e = select P           *
 141        * e' = demod A e         *
 142        * A' = demod [e'] A      *
 143        * A'' = A' + e'          *
 144        * e'' = fresh e'         *
 145        * new = supright e'' A'' *
 146        * new'= demod A'' new    *
 147        * P' = P + new'          *)
 148       debug "Forward infer step...";
 149     let bag, maxvar, actives, passives, g_passives =
 150       match select passives with
 151       | None -> bag, maxvar, actives, passives, g_passives
 152       | Some (current, passives) ->
 153           debug ("Selected fact : " ^ Pp.pp_unit_clause current);
 154           match Sup.simplify (snd actives) bag current with
 155           | None -> debug ("Discarded fact");
 156               bag, maxvar, actives, passives, g_passives
 157           | Some (bag, current) ->
 158               debug ("Fact after simplification :" ^ Pp.pp_unit_clause current);
 159               let bag, maxvar, actives, new_clauses =
 160                 Sup.infer_right bag maxvar current actives
 161               in
 162               let ctable = IDX.index_unit_clause IDX.DT.empty current in
 163               let bag, maxvar, new_goals =
 164                 List.fold_left
 165                   (fun (bag,m,acc) g ->
 166                      let bag, m, ng = Sup.infer_left bag maxvar g
 167                        ([current],ctable) in
 168                        bag,m,ng@acc)
 169                   (bag,maxvar,[]) g_actives
 170               in
 171               let new_clauses = List.fold_left add_passive_clause
 172                 PassiveSet.empty new_clauses in
 173               let new_goals = List.fold_left add_passive_clause
 174                 PassiveSet.empty new_goals in
 175                 bag, maxvar, actives,
 176               PassiveSet.union new_clauses passives,
 177               PassiveSet.union new_goals g_passives
 178     in
 179       prerr_endline
 180         (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
 181       prerr_endline
 182         (Printf.sprintf "Number of passives : %d"
 183            (PassiveSet.cardinal passives));
 184       given_clause bag maxvar actives passives g_actives g_passives
 185   in
 186
 187   let mk_clause bag maxvar (t,ty) =
 188     let (proof,ty) = B.saturate t ty in
 189     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
 190     let bag, c = Utils.add_to_bag bag c in
 191     bag, maxvar, c
 192   in
 193   let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
 194   let g_actives = [] in
 195   let g_passives = PassiveSet.singleton (Utils.mk_passive_clause goal) in
 196   let passives, bag, maxvar =
 197     List.fold_left
 198       (fun (cl, bag, maxvar) t ->
 199          let bag, maxvar, c = mk_clause bag maxvar t in
 200          (add_passive_clause cl c), bag, maxvar)
 201       (PassiveSet.empty, bag, maxvar) table
 202   in
 203   let actives = [], IDX.DT.empty in
 204   try given_clause bag maxvar actives passives g_actives g_passives
 205   with Sup.Success (bag, _, mp) ->
 206     prerr_endline "YES!";
 207     prerr_endline "Meeting point :"; prerr_endline (Pp.pp_unit_clause mp);
 208     (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag) *)
 209 ;;