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