helm/software/components/ng_paramodulation/paramod.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
  13
  14 let debug s = prerr_endline s ;;
  15 let debug _ = ();;
  16
  17 let monster = 100;;
  18
  19 module type Paramod =
  20   sig
  21     type t
  22     type input
  23     type szsontology =
  24       | Unsatisfiable of (t Terms.bag * int * int list) list
  25       | GaveUp
  26       | Error of string
  27       | Timeout of int * t Terms.bag
  28     type bag = t Terms.bag * int
  29     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
  30     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
  31     val paramod :
  32       max_steps:int ->
  33       ?timeout:float ->
  34       bag ->
  35       g_passives:t Terms.unit_clause list ->
  36       passives:t Terms.unit_clause list -> szsontology
  37   end
  38
  39 module Paramod (B : Orderings.Blob) = struct
  40   type t = B.t
  41   type input = B.input
  42   type szsontology =
  43     | Unsatisfiable of (B.t Terms.bag * int * int list) list
  44     | GaveUp
  45     | Error of string
  46     | Timeout of int * B.t Terms.bag
  47   exception Stop of szsontology
  48   type bag = B.t Terms.bag * int
  49   module Pp = Pp.Pp (B)
  50   module FU = FoUnif.Founif(B)
  51   module IDX = Index.Index(B)
  52   module Sup = Superposition.Superposition(B)
  53   module Utils = FoUtils.Utils(B)
  54   module Order = B
  55   module WeightOrderedPassives =
  56       struct
  57         type t = B.t Terms.passive_clause
  58         let compare = Utils.compare_passive_clauses_weight
  59       end
  60
  61   module AgeOrderedPassives =
  62       struct
  63         type t = B.t Terms.passive_clause
  64         let compare = Utils.compare_passive_clauses_age
  65       end
  66
  67   module WeightPassiveSet = Set.Make(WeightOrderedPassives)
  68   module AgePassiveSet = Set.Make(AgeOrderedPassives)
  69
  70   let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl =
  71     let cl = if no_weight then (0,cl)
  72     else Utils.mk_passive_clause cl in
  73     WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
  74   ;;
  75
  76   let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g =
  77     let g = if no_weight then (0,g)
  78     else Utils.mk_passive_goal g in
  79     WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
  80   ;;
  81
  82   let remove_passive_clause (passives_w,passives_a) cl =
  83     let passives_w = WeightPassiveSet.remove cl passives_w in
  84     let passives_a = AgePassiveSet.remove cl passives_a in
  85       passives_w,passives_a
  86   ;;
  87
  88   let add_passive_clauses ?(no_weight=false)
  89       (passives_w,passives_a) new_clauses =
  90     let new_clauses_w,new_clauses_a =
  91       List.fold_left (add_passive_clause ~no_weight)
  92       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
  93     in
  94       (WeightPassiveSet.union new_clauses_w passives_w,
  95        AgePassiveSet.union new_clauses_a passives_a)
  96   ;;
  97
  98   let add_passive_goals ?(no_weight=false)
  99       (passives_w,passives_a) new_clauses =
 100     let new_clauses_w,new_clauses_a =
 101       List.fold_left (add_passive_goal ~no_weight)
 102       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
 103     in
 104       (WeightPassiveSet.union new_clauses_w passives_w,
 105        AgePassiveSet.union new_clauses_a passives_a)
 106   ;;
 107
 108   let is_passive_set_empty (passives_w,passives_a) =
 109     if (WeightPassiveSet.is_empty passives_w) then begin
 110       assert (AgePassiveSet.is_empty passives_a); true
 111     end else begin
 112       assert (not (AgePassiveSet.is_empty passives_a)); false
 113     end
 114   ;;
 115
 116   let passive_set_cardinal (passives_w,_) = WeightPassiveSet.cardinal passives_w
 117
 118   let passive_empty_set =
 119     (WeightPassiveSet.empty,AgePassiveSet.empty)
 120   ;;
 121
 122   let pick_min_passive ~use_age (passives_w,passives_a) =
 123     if use_age then AgePassiveSet.min_elt passives_a
 124     else WeightPassiveSet.min_elt passives_w
 125   ;;
 126
 127   let mk_clause bag maxvar (t,ty) =
 128     let (proof,ty) = B.saturate t ty in
 129     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
 130     let bag, c = Terms.add_to_bag c bag in
 131     (bag, maxvar), c
 132   ;;
 133
 134   let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
 135   let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
 136
 137   (* TODO : global age over facts and goals (without comparing weights) *)
 138   let select ~use_age passives g_passives =
 139     if is_passive_set_empty passives then begin
 140       if (is_passive_set_empty g_passives) then
 141         raise (Stop GaveUp) (* we say we are incomplete *)
 142       else
 143        let g_cl = pick_min_passive ~use_age:use_age g_passives in
 144         (true,g_cl,passives,remove_passive_clause g_passives g_cl)
 145     end
 146     else let cl = pick_min_passive ~use_age:use_age passives in
 147       if is_passive_set_empty g_passives then
 148         (false,cl,remove_passive_clause passives cl,g_passives)
 149       else
 150         let g_cl = pick_min_passive ~use_age:use_age g_passives in
 151         let (id1,_,_,_),(id2,_,_,_) = snd cl, snd g_cl in
 152         let cmp = if use_age then id1 <= id2
 153         else fst cl <= fst g_cl
 154         in
 155           if cmp then
 156             (false,cl,remove_passive_clause passives cl,g_passives)
 157           else
 158             (true,g_cl,passives,remove_passive_clause g_passives g_cl)
 159   ;;
 160
 161   let backward_infer_step bag maxvar actives passives
 162                           g_actives g_passives g_current iterno =
 163     (* superposition left, simplifications on goals *)
 164       debug "infer_left step...";
 165       let bag, maxvar, new_goals =
 166         Sup.infer_left bag maxvar g_current actives
 167       in
 168         debug "Performed infer_left step";
 169         let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
 170         bag, maxvar, actives, passives, g_current::g_actives,
 171     (add_passive_goals g_passives new_goals)
 172   ;;
 173
 174   let forward_infer_step bag maxvar actives passives g_actives
 175                          g_passives current iterno =
 176     (* forward step *)
 177
 178     (* e = select P           *
 179      * e' = demod A e         *
 180      * A' = demod [e'] A      *
 181      * A'' = A' + e'          *
 182      * e'' = fresh e'         *
 183      * new = supright e'' A'' *
 184      * new'= demod A'' new    *
 185      * P' = P + new'          *)
 186     debug "Forward infer step...";
 187     let bag, maxvar, actives, new_clauses =
 188       Sup.infer_right bag maxvar current actives
 189     in
 190       debug "Demodulating goals with actives...";
 191       (* keep goals demodulated w.r.t. actives and check if solved *)
 192       let bag, g_actives =
 193         List.fold_left
 194           (fun (bag,acc) c ->
 195              match
 196                Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c
 197              with
 198                | None -> bag, acc
 199                | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
 200           (bag,[]) g_actives
 201       in
 202       let ctable = IDX.index_unit_clause IDX.DT.empty current in
 203       let bag, maxvar, new_goals =
 204         List.fold_left
 205           (fun (bag,m,acc) g ->
 206              let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in
 207                bag,m,ng@acc)
 208           (bag,maxvar,[]) g_actives
 209       in
 210       let bag = Terms.replace_in_bag (current,false,iterno) bag in
 211     bag, maxvar, actives,
 212     add_passive_clauses passives new_clauses, g_actives,
 213     add_passive_goals g_passives new_goals
 214   ;;
 215
 216   let rec given_clause ~noinfer
 217     bag maxvar iterno weight_picks max_steps timeout
 218     actives passives g_actives g_passives
 219   =
 220     let iterno = iterno + 1 in
 221     if iterno = max_steps then raise (Stop (Timeout (maxvar,bag)));
 222     (* timeout check: gettimeofday called only if timeout set *)
 223     if timeout <> None &&
 224       (match timeout with
 225       | None -> assert false
 226       | Some timeout -> Unix.gettimeofday () > timeout) then
 227         if noinfer then
 228           begin
 229             debug
 230               ("Last chance: all is indexed " ^ string_of_float
 231                 (Unix.gettimeofday()));
 232             let maxgoals = 100 in
 233             ignore(List.fold_left
 234               (fun (acc,i) x ->
 235                  if i < maxgoals then
 236                  ignore(Sup.simplify_goal ~no_demod:true
 237                           maxvar (snd actives) bag acc x)
 238                  else
 239                    ();
 240                  x::acc,i+1)
 241               ([],0) g_actives);
 242             raise (Stop (Timeout (maxvar,bag)))
 243           end
 244         else if false then (* activates last chance strategy *)
 245           begin
 246            debug("Last chance: "^string_of_float (Unix.gettimeofday()));
 247            given_clause ~noinfer:true bag maxvar iterno weight_picks max_steps
 248              (Some (Unix.gettimeofday () +. 20.))
 249              actives passives g_actives g_passives;
 250            raise (Stop (Timeout (maxvar,bag)));
 251           end
 252         else raise (Stop (Timeout (maxvar,bag)));
 253
 254     let use_age = weight_picks = (iterno / 6 + 1) in
 255     let weight_picks = if use_age then 0 else weight_picks+1
 256     in
 257
 258     let rec aux_select bag passives g_passives =
 259       let backward,(weight,current),passives,g_passives =
 260         select ~use_age passives g_passives
 261       in
 262         if use_age && weight > monster then
 263           let bag,cl = Terms.add_to_bag current bag in
 264             if backward then
 265               aux_select bag passives (add_passive_clause g_passives cl)
 266             else
 267               aux_select bag (add_passive_clause passives cl) g_passives
 268         else
 269           let bag = Terms.replace_in_bag (current,false,iterno) bag in
 270         if backward then
 271           let _ = debug ("Selected goal : " ^ Pp.pp_unit_clause current) in
 272          match
 273            if noinfer then
 274              if weight > monster then None else Some (bag,current)
 275            else
 276              Sup.simplify_goal
 277                ~no_demod:false maxvar (snd actives) bag g_actives current
 278          with
 279             | None -> aux_select bag passives g_passives
 280             | Some (bag,g_current) ->
 281                if noinfer then
 282                  let g_actives = g_current :: g_actives in
 283                  bag,maxvar,actives,passives,g_actives,g_passives
 284                else
 285                  backward_infer_step bag maxvar actives passives
 286                    g_actives g_passives g_current iterno
 287         else
 288           let _ = debug ("Selected fact : " ^ Pp.pp_unit_clause current) in
 289           (*let is_orphan = Sup.orphan_murder bag (fst actives) current in*)
 290           match
 291             if noinfer then
 292               if weight > monster then bag,None
 293               else  bag, Some (current,actives)
 294             else if Sup.orphan_murder bag (fst actives) current then
 295               let _ = debug "Orphan murdered" in
 296               let bag = Terms.replace_in_bag (current,true,iterno) bag in
 297                 bag, None
 298             else Sup.keep_simplified current actives bag maxvar
 299           with
 300         (*match Sup.one_pass_simplification current actives bag maxvar with*)
 301               | bag,None -> aux_select bag passives g_passives
 302               | bag,Some (current,actives) ->
 303 (*                    if is_orphan then prerr_endline
 304                       ("WRONG discarded: " ^ (Pp.pp_unit_clause current));
 305                   List.iter (fun x ->
 306                                prerr_endline (Pp.pp_unit_clause x))
 307                     (fst actives);*)
 308
 309 (*                  List.iter (fun (id,_,_,_) -> let (cl,d) =
 310                              Terms.M.find id bag in
 311                              if d then prerr_endline
 312                                ("WRONG discarded: " ^ (Pp.pp_unit_clause cl)))
 313                     (current::fst actives);*)
 314                   if noinfer then
 315                     let actives =
 316                       current::fst actives,
 317                       IDX.index_unit_clause (snd actives) current
 318                     in
 319                     bag,maxvar,actives,passives,g_actives,g_passives
 320                   else
 321                     forward_infer_step bag maxvar actives passives
 322                       g_actives g_passives current iterno
 323     in
 324
 325
 326       (*prerr_endline "Active table :";
 327        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
 328           (fst actives)); *)
 329
 330     let bag,maxvar,actives,passives,g_actives,g_passives =
 331       aux_select bag passives g_passives
 332     in
 333       debug
 334         (Printf.sprintf "Number of active goals : %d"
 335            (List.length g_actives));
 336       debug
 337         (Printf.sprintf "Number of passive goals : %d"
 338            (passive_set_cardinal g_passives));
 339       debug
 340         (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
 341       debug
 342         (Printf.sprintf "Number of passives : %d"
 343            (passive_set_cardinal passives));
 344       given_clause ~noinfer
 345         bag maxvar iterno weight_picks max_steps timeout
 346         actives passives g_actives g_passives
 347   ;;
 348
 349   let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
 350     let initial_timestamp = Unix.gettimeofday () in
 351     let passives =
 352       add_passive_clauses ~no_weight:true passive_empty_set passives
 353     in
 354     let g_passives =
 355       add_passive_goals ~no_weight:true passive_empty_set g_passives
 356     in
 357     let g_actives = [] in
 358     let actives = [], IDX.DT.empty in
 359     try
 360      given_clause ~noinfer:false
 361       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
 362     with
 363     | Sup.Success (bag, _, (i,_,_,_)) ->
 364         let l =
 365           let rec traverse ongoal (accg,acce) i =
 366             match Terms.get_from_bag i bag with
 367               | (id,_,_,Terms.Exact _),_,_ ->
 368                   if ongoal then [i],acce else
 369                     if (List.mem i acce) then accg,acce else accg,acce@[i]
 370               | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ ->
 371                   if (not ongoal) && (List.mem i acce) then accg,acce
 372                   else
 373                     let accg,acce =
 374                       traverse false (traverse ongoal (accg,acce) i1) i2
 375                     in
 376                       if ongoal then i::accg,acce else accg,i::acce
 377           in
 378           let gsteps,esteps = traverse true ([],[]) i in
 379             (List.rev esteps)@gsteps
 380         in
 381         let max_w = List.fold_left (fun acc i ->
 382                     let (cl,_,_) = Terms.get_from_bag i bag in
 383                     max acc (Order.compute_unit_clause_weight cl)) 0 l in
 384           prerr_endline "Statistics :";
 385           prerr_endline ("Max weight : " ^ (string_of_int max_w));
 386 (*        List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) =
 387             Terms.get_from_bag id bag in
 388               if d then
 389                 prerr_endline
 390                 (Printf.sprintf "Id : %d, selected at %d, weight %d,disc, by %s"
 391                    id it (Order.compute_unit_clause_weight cl)
 392                    (Pp.pp_proof_step proof))
 393               else
 394                prerr_endline
 395                 (Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
 396                    id it (Order.compute_unit_clause_weight cl)
 397                    (Pp.pp_proof_step proof))) l;*)
 398         prerr_endline
 399           (Printf.sprintf "Found proof, %fs"
 400             (Unix.gettimeofday() -. initial_timestamp));
 401         (*
 402         prerr_endline "Proof:";
 403         List.iter (fun x ->
 404           prerr_endline (Pp.pp_unit_clause (fst(Terms.M.find x bag)))) l;
 405         *)
 406         Unsatisfiable [ bag, i, l ]
 407     | Stop (Unsatisfiable _) -> Error "stop bug solution found!"
 408     | Stop o -> o
 409   ;;
 410
 411 end