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 (Lazy.force 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     type state
  30     val empty_state : state
  31     val bag_of_state : state -> bag
  32     val replace_bag: state -> bag -> state
  33     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
  34     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
  35     val forward_infer_step :
  36       state ->
  37       t Terms.unit_clause ->
  38       int ->
  39       state
  40     val goal_narrowing :
  41       int
  42       -> int
  43       -> float option
  44       -> state
  45       -> state
  46     val paramod :
  47       useage:bool ->
  48       max_steps:int ->
  49       ?timeout:float ->
  50       bag ->
  51       g_passives:t Terms.unit_clause list ->
  52       passives:t Terms.unit_clause list -> szsontology
  53     val fast_eq_check :
  54       state -> input* input -> szsontology
  55   end
  56
  57 module Paramod (B : Orderings.Blob) = struct
  58   module Pp = Pp.Pp (B)
  59   module FU = FoUnif.Founif(B)
  60   module IDX = Index.Index(B)
  61   module Sup = Superposition.Superposition(B)
  62   module Utils = FoUtils.Utils(B)
  63   module Order = B
  64   module WeightOrderedPassives =
  65       struct
  66         type t = B.t Terms.passive_clause
  67         let compare = Utils.compare_passive_clauses_weight
  68       end
  69
  70   module AgeOrderedPassives =
  71       struct
  72         type t = B.t Terms.passive_clause
  73         let compare = Utils.compare_passive_clauses_age
  74       end
  75
  76   module WeightPassiveSet = Set.Make(WeightOrderedPassives)
  77   module AgePassiveSet = Set.Make(AgeOrderedPassives)
  78
  79   type t = B.t
  80   type input = B.input
  81   type bag = B.t Terms.bag * int
  82   type szsontology =
  83     | Unsatisfiable of (B.t Terms.bag * int * int list) list
  84     | GaveUp
  85     | Error of string
  86     | Timeout of int * B.t Terms.bag
  87   exception Stop of szsontology
  88   type state =
  89       t Terms.bag
  90       * int
  91       * Index.Index(B).active_set
  92       * (IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t)
  93       * B.t Terms.unit_clause list
  94       * (WeightPassiveSet.t * AgePassiveSet.t)
  95
  96   let empty_state =
  97     Terms.empty_bag,
  98     0,
  99     ([],IDX.DT.empty),
 100     (IDX.DT.empty,WeightPassiveSet.empty,AgePassiveSet.empty),
 101     [],
 102     (WeightPassiveSet.empty,AgePassiveSet.empty)
 103   ;;
 104
 105   let bag_of_state (bag,n,_,_,_,_) = bag,n
 106   ;;
 107
 108   let replace_bag (_,_,a,b,c,d) (bag,n) = bag,n,a,b,c,d
 109   ;;
 110
 111   let add_passive_clause ?(no_weight=false)
 112       (passive_t,passives_w,passives_a) cl =
 113     let pcl = if no_weight then (0,cl)
 114     else Utils.mk_passive_clause cl in
 115     IDX.index_unit_clause passive_t cl,
 116     WeightPassiveSet.add pcl passives_w,
 117     AgePassiveSet.add pcl passives_a
 118   ;;
 119
 120   let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g =
 121     let g = if no_weight then (0,g)
 122     else Utils.mk_passive_goal g in
 123     WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
 124   ;;
 125
 126   let remove_passive_clause (passive_t,passives_w,passives_a) cl =
 127     let passive_t = IDX.remove_unit_clause passive_t (snd cl) in
 128     let passives_w = WeightPassiveSet.remove cl passives_w in
 129     let passives_a = AgePassiveSet.remove cl passives_a in
 130       passive_t,passives_w,passives_a
 131   ;;
 132
 133   let add_passive_clauses ?(no_weight=false) =
 134     List.fold_left (add_passive_clause ~no_weight)
 135   ;;
 136
 137   let add_passive_goals ?(no_weight=false)
 138       (passives_w,passives_a) new_clauses =
 139     let new_clauses_w,new_clauses_a =
 140       List.fold_left (add_passive_goal ~no_weight)
 141       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
 142     in
 143       (WeightPassiveSet.union new_clauses_w passives_w,
 144        AgePassiveSet.union new_clauses_a passives_a)
 145   ;;
 146
 147   let remove_passive_goal (passives_w,passives_a) cl =
 148     let passives_w = WeightPassiveSet.remove cl passives_w in
 149     let passives_a = AgePassiveSet.remove cl passives_a in
 150       passives_w,passives_a
 151   ;;
 152
 153   let is_passive_set_empty (_,passives_w,passives_a) =
 154     if (WeightPassiveSet.is_empty passives_w) then begin
 155       assert (AgePassiveSet.is_empty passives_a); true
 156     end else begin
 157       assert (not (AgePassiveSet.is_empty passives_a)); false
 158     end
 159   ;;
 160
 161   let is_passive_g_set_empty (passives_w,passives_a) =
 162     if (WeightPassiveSet.is_empty passives_w) then begin
 163       assert (AgePassiveSet.is_empty passives_a); true
 164     end else begin
 165       assert (not (AgePassiveSet.is_empty passives_a)); false
 166     end
 167   ;;
 168
 169   let passive_set_cardinal (_,passives_w,_)
 170       = WeightPassiveSet.cardinal passives_w
 171   ;;
 172
 173   let g_passive_set_cardinal (passives_w,_)
 174       = WeightPassiveSet.cardinal passives_w
 175   ;;
 176
 177   let passive_empty_set =
 178     (IDX.DT.empty,WeightPassiveSet.empty,AgePassiveSet.empty)
 179   ;;
 180
 181   let g_passive_empty_set =
 182     (WeightPassiveSet.empty,AgePassiveSet.empty)
 183   ;;
 184
 185   let pick_min_passive ~use_age (_,passives_w,passives_a) =
 186     if use_age then AgePassiveSet.min_elt passives_a
 187     else WeightPassiveSet.min_elt passives_w
 188   ;;
 189
 190   let pick_min_g_passive ~use_age (passives_w,passives_a) =
 191     if use_age then AgePassiveSet.min_elt passives_a
 192     else WeightPassiveSet.min_elt passives_w
 193   ;;
 194
 195   let mk_clause bag maxvar (t,ty) =
 196     let (proof,ty) = B.saturate t ty in
 197     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
 198     let bag, c = Terms.add_to_bag c bag in
 199     (bag, maxvar), c
 200   ;;
 201
 202   let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
 203   let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
 204   let initialize_goal (bag,maxvar,actives,passives,_,_) t =
 205     let (bag,maxvar), g = mk_goal (bag,maxvar) t in
 206     let g_passives = g_passive_empty_set in
 207     (* if the goal is not an equation we returns an empty
 208        passive set *)
 209     let g_passives =
 210       if Terms.is_eq_clause g then add_passive_goal g_passives g
 211       else g_passives
 212     in
 213       (bag,maxvar,actives,passives,[],g_passives)
 214
 215
 216   (* TODO : global age over facts and goals (without comparing weights) *)
 217   let select ~use_age passives g_passives =
 218     if is_passive_set_empty passives then begin
 219       if (is_passive_g_set_empty g_passives) then
 220         raise (Stop GaveUp) (* we say we are incomplete *)
 221       else
 222        let g_cl = pick_min_g_passive ~use_age:use_age g_passives in
 223         (true,g_cl,passives,remove_passive_goal g_passives g_cl)
 224     end
 225     else let cl = pick_min_passive ~use_age:use_age passives in
 226       if is_passive_g_set_empty g_passives then
 227         (false,cl,remove_passive_clause passives cl,g_passives)
 228       else
 229         let g_cl = pick_min_g_passive ~use_age:use_age g_passives in
 230         let (id1,_,_,_),(id2,_,_,_) = snd cl, snd g_cl in
 231         let cmp = if use_age then id1 <= id2
 232         else fst cl <= fst g_cl
 233         in
 234           if cmp then
 235             (false,cl,remove_passive_clause passives cl,g_passives)
 236           else
 237             (true,g_cl,passives,remove_passive_goal g_passives g_cl)
 238   ;;
 239
 240   let backward_infer_step bag maxvar actives passives
 241                           g_actives g_passives g_current iterno =
 242     (* superposition left, simplifications on goals *)
 243       debug (lazy "infer_left step...");
 244       let bag, maxvar, new_goals =
 245         Sup.infer_left bag maxvar g_current actives
 246       in
 247         debug (lazy "Performed infer_left step");
 248         let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
 249         bag, maxvar, actives, passives, g_current::g_actives,
 250     (add_passive_goals g_passives new_goals)
 251   ;;
 252
 253   let forward_infer_step
 254       ((bag,maxvar,actives,passives,g_actives,g_passives) as s)
 255       current iterno =
 256     (* forward step *)
 257
 258     (* e = select P           *
 259      * e' = demod A e         *
 260      * A' = demod [e'] A      *
 261      * A'' = A' + e'          *
 262      * e'' = fresh e'         *
 263      * new = supright e'' A'' *
 264      * new'= demod A'' new    *
 265      * P' = P + new'          *)
 266     debug (lazy "Forward infer step...");
 267     debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
 268     let id,_,_,_ = current in
 269     let _ = Terms.get_from_bag id bag in
 270
 271     match Sup.keep_simplified current actives bag maxvar
 272     with
 273       | _,None -> s
 274       | bag,Some (current,actives) ->
 275     debug (lazy "simplified...");
 276     let bag, maxvar, actives, new_clauses =
 277       Sup.infer_right bag maxvar current actives
 278     in
 279       debug (lazy "Demodulating goals with actives...");
 280       (* keep goals demodulated w.r.t. actives and check if solved *)
 281       let bag, g_actives =
 282         List.fold_left
 283           (fun (bag,acc) c ->
 284              match
 285                Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c
 286              with
 287                | None -> bag, acc
 288                | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
 289           (bag,[]) g_actives
 290       in
 291       let ctable = IDX.index_unit_clause IDX.DT.empty current in
 292       let bag, maxvar, new_goals =
 293         List.fold_left
 294           (fun (bag,m,acc) g ->
 295              let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in
 296                bag,m,ng@acc)
 297           (bag,maxvar,[]) g_actives
 298       in
 299       let bag = Terms.replace_in_bag (current,false,iterno) bag in
 300         (* prerr_endline (Pp.pp_bag bag); *)
 301     bag, maxvar, actives,
 302     add_passive_clauses passives new_clauses, g_actives,
 303     add_passive_goals g_passives new_goals
 304   ;;
 305
 306   let debug_status (_,_,actives,passives,g_actives,g_passives) =
 307     lazy
 308       ((Printf.sprintf "Number of active goals : %d\n"
 309           (List.length g_actives)) ^
 310        (Printf.sprintf "Number of passive goals : %d\n"
 311           (g_passive_set_cardinal g_passives)) ^
 312        (Printf.sprintf "Number of actives : %d\n"
 313           (List.length (fst actives))) ^
 314        (Printf.sprintf "Number of passives : %d\n"
 315          (passive_set_cardinal passives)))
 316   ;;
 317
 318
 319   (* we just check if any of the active goals is subsumed by a
 320      passive clause, or if any of the passive goal is subsumed
 321      by an active or passive clause *)
 322   let last_chance (bag,maxvar,actives,passives,g_actives,g_passives) =
 323     debug (lazy("Last chance " ^ string_of_float
 324                   (Unix.gettimeofday())));
 325     let active_t = snd actives in
 326     let passive_t,wset,_ = passives in
 327     let _ = debug
 328       (lazy
 329          ("Passive set :" ^ (String.concat ";\n"
 330             (List.map (fun _,cl -> Pp.pp_unit_clause cl)
 331                (WeightPassiveSet.elements wset))))) in
 332     let wset = IDX.elems passive_t in
 333     let _ = debug
 334       (lazy
 335          ("Passive table :" ^(String.concat ";\n"
 336             (List.map (fun _,cl -> Pp.pp_unit_clause cl)
 337                (IDX.ClauseSet.elements wset))))) in
 338     let g_passives =
 339       WeightPassiveSet.fold
 340         (fun (_,x) acc ->
 341           if List.exists (Sup.are_alpha_eq x) g_actives then acc
 342           else x::acc)
 343           (fst g_passives) []
 344     in
 345       ignore
 346       (List.iter
 347         (fun x ->
 348             ignore
 349               (Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
 350        g_passives);
 351       ignore
 352       (List.iter
 353          (fun x ->
 354             ignore
 355               (Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
 356         (g_actives@g_passives));
 357     raise (Stop (Timeout (maxvar,bag)))
 358
 359   let check_timeout = function
 360     | None -> false
 361     | Some timeout -> Unix.gettimeofday () > timeout
 362
 363   let rec given_clause ~useage
 364     bag maxvar iterno weight_picks max_steps timeout
 365     actives passives g_actives g_passives
 366   =
 367     let iterno = iterno + 1 in
 368     if iterno = max_steps || check_timeout timeout then
 369       last_chance (bag,maxvar,actives,passives,g_actives,g_passives)
 370     else
 371     let use_age = useage && (weight_picks = (iterno / 6 + 1)) in
 372     let weight_picks = if use_age then 0 else weight_picks+1
 373     in
 374
 375     let rec aux_select bag
 376         (passives:IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t)
 377         g_passives =
 378       let backward,(weight,current),passives,g_passives =
 379         select ~use_age passives g_passives
 380       in
 381         if use_age && weight > monster then
 382           let bag,cl = Terms.add_to_bag current bag in
 383             if backward then
 384               aux_select bag passives (add_passive_goal g_passives cl)
 385             else
 386               aux_select bag (add_passive_clause passives cl) g_passives
 387         else
 388           let bag = Terms.replace_in_bag (current,false,iterno) bag in
 389         if backward then
 390           let _ = debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) in
 391          match
 392            Sup.simplify_goal
 393              ~no_demod:false maxvar (snd actives) bag g_actives current
 394          with
 395            | None -> aux_select bag passives g_passives
 396            | Some (bag,g_current) ->
 397                backward_infer_step bag maxvar actives passives
 398                  g_actives g_passives g_current iterno
 399         else
 400           let _ = debug (lazy("Selected fact : " ^ Pp.pp_unit_clause current))
 401           in
 402             if Sup.orphan_murder bag (fst actives) current then
 403               let _ = debug (lazy "Orphan murdered") in
 404               let bag = Terms.replace_in_bag (current,true,iterno) bag in
 405                 aux_select bag passives g_passives
 406             else
 407               let s = bag,maxvar,actives,passives,g_actives,g_passives in
 408               let s1 = forward_infer_step s current iterno
 409               in
 410                 if s == s1 then aux_select bag passives g_passives
 411                 else s1
 412     in
 413       (*prerr_endline "Active table :";
 414        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
 415           (fst actives)); *)
 416
 417     let (bag,maxvar,actives,passives,g_actives,g_passives) as status  =
 418       aux_select bag passives g_passives
 419     in
 420       debug (debug_status status);
 421       given_clause ~useage
 422         bag maxvar iterno weight_picks max_steps timeout
 423         actives passives g_actives g_passives
 424   ;;
 425
 426   (* similar to given_clause, but it merely works on goals,
 427      in parallel, at each iteration *)
 428   let rec goal_narrowing iterno max_steps timeout status
 429   =
 430     debug (debug_status status);
 431     let iterno = iterno + 1 in
 432     if iterno = max_steps || check_timeout timeout then
 433       last_chance status
 434     else
 435     let _,_,_,_,_,g_passives = status in
 436     let passive_goals = WeightPassiveSet.elements (fst g_passives) in
 437     let newstatus =
 438       List.fold_left
 439         (fun acc g ->
 440            let bag,maxvar,actives,passives,g_actives,g_passives = acc in
 441            let g_passives =
 442              remove_passive_goal g_passives g in
 443            let current = snd g in
 444            let _ =
 445              debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current))
 446            in
 447            match
 448              Sup.simplify_goal
 449                ~no_demod:false maxvar (snd actives) bag g_actives current
 450            with
 451              | None -> acc
 452              | Some (bag,g_current) ->
 453                  let _ =
 454                    debug (lazy("Demodulated goal : "
 455                                ^ Pp.pp_unit_clause g_current))
 456                  in
 457                  backward_infer_step bag maxvar actives passives
 458                   g_actives g_passives g_current iterno)
 459            status passive_goals
 460     in
 461       goal_narrowing iterno max_steps timeout newstatus
 462
 463     let compute_result bag i =
 464       let l =
 465         let rec traverse ongoal (accg,acce) i =
 466           match Terms.get_from_bag i bag with
 467             | (id,_,_,Terms.Exact _),_,_ ->
 468                 if ongoal then [i],acce else
 469                   if (List.mem i acce) then accg,acce else accg,acce@[i]
 470             | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ ->
 471                 if (not ongoal) && (List.mem i acce) then accg,acce
 472                 else
 473                   let accg,acce =
 474                     traverse false (traverse ongoal (accg,acce) i1) i2
 475                   in
 476                     if ongoal then i::accg,acce else accg,i::acce
 477         in
 478         let gsteps,esteps = traverse true ([],[]) i in
 479           (List.rev esteps)@gsteps
 480       in
 481       debug (lazy ("steps: " ^ (string_of_int (List.length l))));
 482       let max_w =
 483         List.fold_left
 484           (fun acc i ->
 485              let (cl,_,_) = Terms.get_from_bag i bag in
 486                max acc (Order.compute_unit_clause_weight cl)) 0 l in
 487         debug (lazy ("Max weight : " ^ (string_of_int max_w)));
 488 (*        List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) =
 489             Terms.get_from_bag id bag in
 490               if d then
 491                 prerr_endline
 492                 (Printf.sprintf "Id : %d, selected at %d, weight %d,disc, by %s"
 493                    id it (Order.compute_unit_clause_weight cl)
 494                    (Pp.pp_proof_step proof))
 495               else
 496                prerr_endline
 497                 (Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
 498                    id it (Order.compute_unit_clause_weight cl)
 499                    (Pp.pp_proof_step proof))) l;*)
 500         debug (lazy ("Proof:" ^
 501           (String.concat "\n"
 502              (List.map
 503                 (fun x ->
 504                    let cl,_,_ = Terms.get_from_bag x bag in
 505                      Pp.pp_unit_clause cl) l))));
 506         Unsatisfiable [ bag, i, l ]
 507
 508   let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
 509     let _initial_timestamp = Unix.gettimeofday () in
 510     let passives =
 511       add_passive_clauses ~no_weight:true passive_empty_set passives
 512     in
 513     let g_passives =
 514       add_passive_goals ~no_weight:true g_passive_empty_set g_passives
 515     in
 516     let g_actives = [] in
 517     let actives = [], IDX.DT.empty in
 518     try
 519      given_clause ~useage ~noinfer:false
 520       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
 521     with
 522     | Sup.Success (bag, _, (i,_,_,_)) ->
 523         compute_result bag i
 524     | Stop (Unsatisfiable _) -> Error "solution found!"
 525     | Stop o -> o
 526   ;;
 527
 528 let fast_eq_check s goal =
 529   let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
 530   if is_passive_g_set_empty g_passives then Error "not an equation"
 531   else
 532   try
 533     goal_narrowing 0 2 None s
 534   with
 535     | Sup.Success (bag, _, (i,_,_,_)) ->
 536         compute_result bag i
 537     | Stop (Unsatisfiable _) -> Error "solution found!"
 538     | Stop o -> o
 539   ;;
 540
 541 end