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