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