helm/software/components/ng_paramodulation/paramod.ml

   1 let debug s =
   2    () (*prerr_endline s*)
   3 ;;
   4
   5 let nparamod rdb metasenv subst context t table =
   6   let max_nb_iter = 999999999 in
   7   let amount_of_time = 300.0 in
   8   let module C = struct
   9     let metasenv = metasenv
  10     let subst = subst
  11     let context = context
  12   end
  13   in
  14   let nb_iter = ref 0 in
  15   let module B = NCicBlob.NCicBlob(C) in
  16   let module Pp = Pp.Pp (B) in
  17   let module FU = FoUnif.Founif(B) in
  18   let module IDX = Index.Index(B) in
  19   let module Sup = Superposition.Superposition(B) in
  20   let module Utils = FoUtils.Utils(B) in
  21
  22   let module WeightOrderedPassives =
  23       struct
  24         type t = B.t Terms.passive_clause
  25
  26         let compare = Utils.compare_passive_clauses_weight
  27       end
  28   in
  29   let module AgeOrderedPassives =
  30       struct
  31         type t = B.t Terms.passive_clause
  32
  33         let compare = Utils.compare_passive_clauses_age
  34       end
  35   in
  36   let module WeightPassiveSet = Set.Make(WeightOrderedPassives) in
  37   let module AgePassiveSet = Set.Make(AgeOrderedPassives) in
  38   let add_passive_clause ?(no_weight=true) (passives_w,passives_a) cl =
  39     let cl = if no_weight then (0,cl)
  40     else Utils.mk_passive_clause cl in
  41     WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
  42   in
  43   let remove_passive_clause (passives_w,passives_a) cl =
  44     let passives_w = WeightPassiveSet.remove cl passives_w in
  45     let passives_a = AgePassiveSet.remove cl passives_a in
  46       passives_w,passives_a
  47   in
  48   let add_passive_clauses (passives_w,passives_a) new_clauses =
  49     let new_clauses_w,new_clauses_a = List.fold_left add_passive_clause
  50       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
  51     in
  52       (WeightPassiveSet.union new_clauses_w passives_w,
  53        AgePassiveSet.union new_clauses_a passives_a)
  54   in
  55   let is_passive_set_empty (passives_w,passives_a) =
  56     if (WeightPassiveSet.is_empty passives_w) then begin
  57       assert (AgePassiveSet.is_empty passives_a); true
  58     end else begin
  59       assert (not (AgePassiveSet.is_empty passives_a)); false
  60     end
  61   in
  62   let passive_set_cardinal (passives_w,_) =
  63     WeightPassiveSet.cardinal passives_w
  64   in
  65   let passive_singleton cl =
  66     (WeightPassiveSet.singleton cl,AgePassiveSet.singleton cl)
  67   in
  68   let passive_empty_set =
  69     (WeightPassiveSet.empty,AgePassiveSet.empty)
  70   in
  71   let pick_min_passive use_age (passives_w,passives_a) =
  72     if use_age then AgePassiveSet.min_elt passives_a
  73     else WeightPassiveSet.min_elt passives_w
  74   in
  75   let timeout = Unix.gettimeofday () +. amount_of_time in
  76
  77     (* TODO : global age over facts and goals (without comparing weights) *)
  78   let select passives g_passives =
  79     if is_passive_set_empty passives then begin
  80       assert (not (is_passive_set_empty g_passives));
  81       let g_cl = pick_min_passive false g_passives in
  82         (true,snd g_cl,passives,remove_passive_clause g_passives g_cl)
  83     end
  84     else let cl = pick_min_passive false passives in
  85       if is_passive_set_empty g_passives then
  86         (false,snd cl,remove_passive_clause passives cl,g_passives)
  87       else
  88         let g_cl = pick_min_passive false g_passives in
  89           if (fst cl <= fst g_cl) then
  90             (false,snd cl,remove_passive_clause passives cl,g_passives)
  91           else
  92             (true,snd g_cl,passives,remove_passive_clause g_passives g_cl)
  93   in
  94
  95   let backward_infer_step bag maxvar actives passives
  96                           g_actives g_passives g_current =
  97     (* superposition left, simplifications on goals *)
  98       debug "infer_left step...";
  99       let bag, maxvar, new_goals =
 100         Sup.infer_left bag maxvar g_current actives
 101       in
 102         debug "Performed infer_left step";
 103         bag, maxvar, actives, passives, g_current::g_actives,
 104     (add_passive_clauses g_passives new_goals)
 105   in
 106
 107   let forward_infer_step bag maxvar actives passives g_actives
 108                          g_passives current =
 109     (* forward step *)
 110
 111     (* e = select P           *
 112      * e' = demod A e         *
 113      * A' = demod [e'] A      *
 114      * A'' = A' + e'          *
 115      * e'' = fresh e'         *
 116      * new = supright e'' A'' *
 117      * new'= demod A'' new    *
 118      * P' = P + new'          *)
 119     debug "Forward infer step...";
 120     debug "Selected and simplified";
 121     (* debug ("Fact after simplification :"
 122        ^ Pp.pp_unit_clause current); *)
 123     let bag, maxvar, actives, new_clauses =
 124       Sup.infer_right bag maxvar current actives
 125     in
 126       debug "Demodulating goals with actives...";
 127       (* keep goals demodulated w.r.t. actives and check if solved *)
 128       let bag, g_actives =
 129         List.fold_left
 130           (fun (bag,acc) c ->
 131              match Sup.simplify_goal maxvar (snd actives) bag acc c with
 132                | None -> bag, acc
 133                | Some (bag,c) -> bag,c::acc)
 134           (bag,[]) g_actives
 135       in
 136       let ctable = IDX.index_unit_clause IDX.DT.empty current in
 137       let bag, maxvar, new_goals =
 138         List.fold_left
 139           (fun (bag,m,acc) g ->
 140              let bag, m, ng = Sup.infer_left bag m g
 141                ([current],ctable) in
 142                bag,m,ng@acc)
 143           (bag,maxvar,[]) g_actives
 144       in
 145         bag, maxvar, actives,
 146     add_passive_clauses passives new_clauses, g_actives,
 147     add_passive_clauses g_passives new_goals
 148   in
 149
 150   let rec given_clause bag maxvar actives passives g_actives g_passives =
 151     (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
 152       prerr_endline "Active table :";
 153        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
 154           (fst actives)); *)
 155     incr nb_iter; if !nb_iter = max_nb_iter then
 156       raise (Failure "No iterations left !");
 157     if Unix.gettimeofday () > timeout then
 158       raise (Failure "Timeout !");
 159
 160
 161     let rec aux_select passives g_passives =
 162       let backward,current,passives,g_passives = select passives g_passives in
 163         if backward then
 164          match Sup.simplify_goal maxvar (snd actives) bag g_actives current with
 165             | None -> aux_select passives g_passives
 166             | Some x -> let bag,g_current = x in
 167                 backward_infer_step bag maxvar actives passives
 168                   g_actives g_passives g_current
 169         else
 170           (* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *)
 171           match Sup.keep_simplified current actives bag maxvar with
 172         (*  match Sup.one_pass_simplification current actives bag maxvar with*)
 173               | None -> aux_select passives g_passives
 174               | Some x -> let (current, bag, actives) = x in
 175                   forward_infer_step bag maxvar actives passives
 176                                      g_actives g_passives current
 177     in
 178
 179     let bag,maxvar,actives,passives,g_actives,g_passives =
 180       aux_select passives g_passives
 181     in
 182       debug
 183         (Printf.sprintf "Number of active goals : %d"
 184            (List.length g_actives));
 185       debug
 186         (Printf.sprintf "Number of passive goals : %d"
 187            (passive_set_cardinal g_passives));
 188       debug
 189         (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
 190       debug
 191         (Printf.sprintf "Number of passives : %d"
 192            (passive_set_cardinal passives));
 193       given_clause bag maxvar actives passives g_actives g_passives
 194   in
 195
 196   let mk_clause ?(no_weight=false) bag maxvar (t,ty) =
 197     let (proof,ty) = B.saturate t ty in
 198     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
 199     let bag, c = Utils.add_to_bag bag c in
 200     bag, maxvar, c
 201   in
 202   let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
 203   let g_actives = [] in
 204   let g_passives =
 205     passive_singleton (0,goal)
 206   in
 207   let passives, bag, maxvar =
 208     List.fold_left
 209       (fun (cl, bag, maxvar) t ->
 210          let bag, maxvar, c = mk_clause bag maxvar t in
 211          (add_passive_clause cl c), bag, maxvar)
 212       (passive_empty_set, bag, maxvar) table
 213   in
 214   let actives = [], IDX.DT.empty in
 215   try given_clause bag maxvar actives passives g_actives g_passives
 216   with
 217   | Sup.Success (bag, _, (i,_,_,_)) ->
 218       let l =
 219         let rec traverse ongoal (accg,acce) i =
 220           match Terms.M.find i bag with
 221             | (id,_,_,Terms.Exact _) ->
 222                 if ongoal then [i],acce else
 223                   if (List.mem i acce) then accg,acce else accg,acce@[i]
 224             | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
 225                 if (not ongoal) && (List.mem i acce) then accg,acce
 226                 else
 227                   let accg,acce =
 228                     traverse false (traverse ongoal (accg,acce) i1) i2
 229                   in
 230                     if ongoal then i::accg,acce else accg,i::acce
 231         in
 232         let gsteps,esteps = traverse true ([],[]) i in
 233           (List.rev esteps)@gsteps
 234       in
 235         prerr_endline (Printf.sprintf "Found proof in %d iterations, %fs"
 236                          !nb_iter
 237                          (Unix.gettimeofday() -. timeout +. amount_of_time));
 238       (* prerr_endline "Proof:";
 239       List.iter (fun x -> prerr_endline (string_of_int x);
 240               prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;*)
 241       let proofterm = B.mk_proof bag i l in
 242         prerr_endline (Printf.sprintf "Got proof term, %fs"
 243                          (Unix.gettimeofday() -. timeout +. amount_of_time));
 244       let metasenv, proofterm =
 245         let rec aux k metasenv = function
 246           | NCic.Meta _ as t -> metasenv, t
 247           | NCic.Implicit _ ->
 248               let metasenv,i,_,_=NCicMetaSubst.mk_meta metasenv context `Term in
 249               metasenv, NCic.Meta (i,(k,NCic.Irl (List.length context)))
 250           | t -> NCicUntrusted.map_term_fold_a
 251                   (fun _ k -> k+1) k aux metasenv t
 252         in
 253          aux 0 metasenv proofterm
 254       in
 255       let metasenv, subst, proofterm, _prooftype =
 256         NCicRefiner.typeof
 257           (rdb#set_coerc_db NCicCoercion.empty_db)
 258           metasenv subst context proofterm None
 259       in
 260       proofterm, metasenv, subst
 261   | Failure s ->
 262       prerr_endline s;
 263       prerr_endline
 264       (Printf.sprintf "FAILURE in %d iterations" !nb_iter); assert false
 265 ;;