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 and simplify with
 104      * just new_clauses *)
 105     let bag, g_actives =
 106       List.fold_left
 107         (fun (bag,acc) c ->
 108            let bag, c = Sup.backward_simplify maxvar (snd actives) bag c in
 109              bag, c::acc)
 110         (bag,[]) g_actives
 111     in
 112
 113       (* backward step : superposition left, simplifications on goals *)
 114       debug "Backward infer step...";
 115       let bag, maxvar, g_actives, g_passives =
 116         match select g_passives with
 117       | None -> bag, maxvar, g_actives, g_passives
 118       | Some (g_current, g_passives) ->
 119           debug ("Selected goal : " ^ Pp.pp_unit_clause g_current);
 120           let bag, g_current =
 121             Sup.backward_simplify maxvar (snd actives) bag g_current
 122           in
 123           let bag, maxvar, new_goals =
 124             Sup.infer_left bag maxvar g_current actives
 125           in
 126           let new_goals = List.fold_left add_passive_clause
 127             PassiveSet.empty new_goals
 128           in
 129           bag, maxvar, g_current::g_actives,
 130           (PassiveSet.union new_goals g_passives)
 131     in
 132       prerr_endline
 133         (Printf.sprintf "Number of active goals : %d"
 134            (List.length g_actives));
 135       prerr_endline
 136         (Printf.sprintf "Number of passive goals : %d"
 137            (PassiveSet.cardinal g_passives));
 138
 139       (* forward step *)
 140
 141       (* e = select P           *
 142        * e' = demod A e         *
 143        * A' = demod [e'] A      *
 144        * A'' = A' + e'          *
 145        * e'' = fresh e'         *
 146        * new = supright e'' A'' *
 147        * new'= demod A'' new    *
 148        * P' = P + new'          *)
 149       debug "Forward infer step...";
 150     let bag, maxvar, actives, passives, g_passives =
 151       match select passives with
 152       | None -> bag, maxvar, actives, passives, g_passives
 153       | Some (current, passives) ->
 154           debug ("Selected fact : " ^ Pp.pp_unit_clause current);
 155           match Sup.forward_simplify (snd actives) bag current with
 156           | None -> debug ("Discarded fact");
 157               bag, maxvar, actives, passives, g_passives
 158           | Some (bag, current) ->
 159               debug ("Fact after simplification :" ^ Pp.pp_unit_clause current);
 160               let bag, maxvar, actives, new_clauses =
 161                 Sup.infer_right bag maxvar current actives
 162               in
 163               let ctable = IDX.index_unit_clause IDX.DT.empty current in
 164               let bag, maxvar, new_goals =
 165                 List.fold_left
 166                   (fun (bag,m,acc) g ->
 167                      let bag, m, ng = Sup.infer_left bag maxvar g
 168                        ([current],ctable) in
 169                        bag,m,ng@acc)
 170                   (bag,maxvar,[]) g_actives
 171               in
 172               let new_clauses = List.fold_left add_passive_clause
 173                 PassiveSet.empty new_clauses in
 174               let new_goals = List.fold_left add_passive_clause
 175                 PassiveSet.empty new_goals in
 176                 bag, maxvar, actives,
 177               PassiveSet.union new_clauses passives,
 178               PassiveSet.union new_goals g_passives
 179     in
 180       prerr_endline
 181         (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
 182       prerr_endline
 183         (Printf.sprintf "Number of passives : %d"
 184            (PassiveSet.cardinal passives));
 185       given_clause bag maxvar actives passives g_actives g_passives
 186   in
 187
 188   let mk_clause bag maxvar (t,ty) =
 189     let (proof,ty) = B.saturate t ty in
 190     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
 191     let bag, c = Utils.add_to_bag bag c in
 192     bag, maxvar, c
 193   in
 194   let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
 195   let g_actives = [] in
 196   let g_passives = PassiveSet.singleton (Utils.mk_passive_clause goal) in
 197   let passives, bag, maxvar =
 198     List.fold_left
 199       (fun (cl, bag, maxvar) t ->
 200          let bag, maxvar, c = mk_clause bag maxvar t in
 201          (add_passive_clause cl c), bag, maxvar)
 202       (PassiveSet.empty, bag, maxvar) table
 203   in
 204   let actives = [], IDX.DT.empty in
 205   try given_clause bag maxvar actives passives g_actives g_passives
 206   with Sup.Success (bag, _, mp) ->
 207     prerr_endline "YES!";
 208     prerr_endline "Meeting point :"; prerr_endline (Pp.pp_unit_clause mp);
 209     (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag) *)
 210 ;;