X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=8024dbba02e085fb8e730ab21a9cfc2ecc6a8368;hb=38c54dd8e2234836d5f3e8011c478daf7d59fa25;hp=9b5b1315719f845f0a86d7f0bc961839e3e44b68;hpb=96c91e470f670018df67c9cbff62fa06e3b57c5e;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 9b5b13157..8024dbba0 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,145 +1,413 @@
-let nparamod metasenv subst context t table =
-  prerr_endline "========================================";
-  let module C = struct
-    let metasenv = metasenv
-    let subst = subst
-    let context = context
-  end
-  in
-  let module B = NCicBlob.NCicBlob(C) in
-  let module Pp = Pp.Pp (B) in
-  let module FU = FoUnif.Founif(B) in
-  let module IDX = Index.Index(B) in
-  let module Sup = Superposition.Superposition(B) in
-  let module Utils = FoUtils.Utils(B) in
 (*
-  let test_unification _ = function
-    | Terms.Node [_; _; lhs; rhs] ->
-	prerr_endline "Unification test :";
-	prerr_endline (Pp.pp_foterm lhs);
-	prerr_endline (Pp.pp_foterm rhs);
-        FU.unification [] [] lhs rhs
-    | _ -> assert false
-  in
-  let subst,vars = test_unification [] res in
-    prerr_endline "Result :";
-    prerr_endline (Pp.pp_foterm res);
-    prerr_endline "Substitution :";
-    prerr_endline (Pp.pp_substitution subst)
-*)
-  let mk_clause maxvar t =
-    let ty = B.embed t in
-    let proof = B.embed (NCic.Rel ~-1) in
-    Utils.mk_unit_clause maxvar ty proof 
-  in
-  let clause, maxvar = mk_clause 0 t in
-  prerr_endline "Input clause :";
-  prerr_endline (Pp.pp_unit_clause clause);
-  let bag = Utils.empty_bag in
-  let active_clauses, maxvar = 
-    List.fold_left
-      (fun (cl,maxvar) t -> 
-         let c, m = mk_clause maxvar t in
-         c::cl, m)
-      ([],maxvar) table 
-  in
-  let table =  
-    List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
-  in
-  prerr_endline "Active table:";
-  List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
-  let bag, maxvar, _, newclauses = 
-    Sup.infer_right bag maxvar clause (active_clauses, table)
-  in
-  prerr_endline "Output clauses :";
-  List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
-  prerr_endline "Proofs: ";
-  prerr_endline (Pp.pp_bag bag);
-  prerr_endline "========================================";
-;;
-
-let select = function 
-  | [] -> None
-  | x::tl -> Some (x, tl)
-;;
-
-let nparamod metasenv subst context t table =
-  prerr_endline "========================================";
-  let module C = struct
-    let metasenv = metasenv
-    let subst = subst
-    let context = context
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
+
+let debug s = prerr_endline (Lazy.force s) ;;
+let debug _ = ();;
+
+let monster = 100;;
+    
+module type Paramod =
+  sig
+    type t
+    type szsontology = 
+      | Unsatisfiable of (t Terms.bag * int * int list) list
+      | GaveUp 
+      | Error of string 
+      | Timeout of int * t Terms.bag
+    val paramod :
+      useage:bool ->
+      max_steps:int ->
+      print_problem:bool ->
+      ?timeout:float ->
+      t Terms.foterm * (t Terms.foterm list * t Terms.foterm list) -> 
+      (t Terms.foterm * (t Terms.foterm list * t Terms.foterm list)) list -> szsontology
   end
-  in
-  let module B = NCicBlob.NCicBlob(C) in
-  let module Pp = Pp.Pp (B) in
-  let module FU = FoUnif.Founif(B) in
-  let module IDX = Index.Index(B) in
-  let module Sup = Superposition.Superposition(B) in
-  let module Utils = FoUtils.Utils(B) in
-
-  let rec given_clause bag maxvar actives passives g_actives g_passives =
-
-    (* keep goals demodulated w.r.t. actives and check if solved *)
-    (* we may move this at the end of infer_right and simplify with
-     * just new_clauses *) 
-    let bag, g_actives = 
-      List.fold_left 
-        (fun (bag,acc) c -> 
-          let bag, c = Sup.backward_simplify maxvar (snd actives) bag c in
-          bag, c::acc) 
-        (bag,[]) g_actives 
+
+module Paramod (B : Orderings.Blob) = struct
+  type t = B.t
+  type szsontology = 
+    | Unsatisfiable of (B.t Terms.bag * int * int list) list
+    | GaveUp 
+    | Error of string 
+    | Timeout of int * B.t Terms.bag
+  exception Stop of szsontology
+  type bag = B.t Terms.bag * int
+  module Pp = Pp.Pp (B) 
+  module FU = FoUnif.Founif(B) 
+  module IDX = Index.Index(B) 
+  module Sup = Superposition.Superposition(B) 
+  module Utils = FoUtils.Utils(B) 
+  module Order = B
+  module WeightOrderedPassives =
+      struct
+        type t = B.t Terms.passive_clause
+        let compare = Utils.compare_passive_clauses_weight
+      end
+
+  module AgeOrderedPassives =
+      struct
+        type t = B.t Terms.passive_clause
+        let compare = Utils.compare_passive_clauses_age
+      end
+  
+  module WeightPassiveSet = Set.Make(WeightOrderedPassives)
+  module AgePassiveSet = Set.Make(AgeOrderedPassives)
+
+  let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl =
+    let cl = if no_weight then (0,cl)
+    else Utils.mk_passive_clause cl in
+    WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
+  ;;
+
+  let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g =
+    let g = if no_weight then (0,g)
+    else Utils.mk_passive_goal g in
+    WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
+  ;;
+
+  let remove_passive_clause (passives_w,passives_a) cl =
+    let passives_w = WeightPassiveSet.remove cl passives_w in
+    let passives_a = AgePassiveSet.remove cl passives_a in
+      passives_w,passives_a
+  ;;
+
+  let add_passive_clauses ?(no_weight=false)
+      (passives_w,passives_a) new_clauses =
+    let new_clauses_w,new_clauses_a =
+      List.fold_left (add_passive_clause ~no_weight)
+      (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
     in
+      (WeightPassiveSet.union new_clauses_w passives_w,
+       AgePassiveSet.union new_clauses_a passives_a)
+  ;;
 
-    (* backward step *)
-    let bag, maxvar, g_actives, g_passives =
-      match select g_passives with
-      | None -> bag, maxvar, g_actives, g_passives
-      | Some (g_current, g_passives) -> 
-          let bag, g_current = 
-            Sup.backward_simplify maxvar (snd actives) bag g_current
-          in
-          let bag, maxvar, new_goals = 
-            Sup.infer_left bag maxvar g_current actives 
-          in
-          bag, maxvar, g_current::g_actives, g_passives @ new_goals
+  let add_passive_goals ?(no_weight=false)
+      (passives_w,passives_a) new_clauses =
+    let new_clauses_w,new_clauses_a =
+      List.fold_left (add_passive_goal ~no_weight)
+      (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
     in
+      (WeightPassiveSet.union new_clauses_w passives_w,
+       AgePassiveSet.union new_clauses_a passives_a)
+  ;;
+
+  let is_passive_set_empty (passives_w,passives_a) =
+    if (WeightPassiveSet.is_empty passives_w) then begin
+      assert (AgePassiveSet.is_empty passives_a); true
+    end else begin
+      assert (not (AgePassiveSet.is_empty passives_a)); false
+    end
+  ;;
+
+  let passive_set_cardinal (passives_w,_) = WeightPassiveSet.cardinal passives_w
   
+  let passive_empty_set =
+    (WeightPassiveSet.empty,AgePassiveSet.empty)
+  ;;
+
+  let pick_min_passive ~use_age (passives_w,passives_a) =
+    if use_age then AgePassiveSet.min_elt passives_a
+    else WeightPassiveSet.min_elt passives_w
+  ;;
+
+  (* TODO : global age over facts and goals (without comparing weights) *)
+  let select ~use_age passives g_passives =
+    if is_passive_set_empty passives then begin
+      if (is_passive_set_empty g_passives) then
+        raise (Stop GaveUp) (* we say we are incomplete *)
+      else
+       let g_cl = pick_min_passive ~use_age:use_age g_passives in
+        (true,g_cl,passives,remove_passive_clause g_passives g_cl)
+    end
+    else let cl = pick_min_passive ~use_age:use_age passives in
+      if is_passive_set_empty g_passives then
+        (false,cl,remove_passive_clause passives cl,g_passives)
+      else
+        let g_cl = pick_min_passive ~use_age:use_age g_passives in
+	let (id1,_,_,_,_),(id2,_,_,_,_) = snd cl, snd g_cl in
+	let cmp = if use_age then id1 <= id2
+	else fst cl <= fst g_cl
+	in
+          if cmp then
+            (false,cl,remove_passive_clause passives cl,g_passives)
+          else
+            (true,g_cl,passives,remove_passive_clause g_passives g_cl)
+  ;;
+
+  let backward_infer_step bag maxvar actives passives
+                          g_actives g_passives g_current iterno =
+    (* superposition left, simplifications on goals *)
+      debug (lazy "infer_left step...");
+      let bag, maxvar, new_goals = 
+        Sup.infer_left bag maxvar g_current actives 
+      in
+        debug (lazy "Performed infer_left step");
+	let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
+        bag, maxvar, actives, passives, g_current::g_actives,
+    (add_passive_goals g_passives new_goals)
+  ;;
+
+  let forward_infer_step bag maxvar actives passives g_actives
+                         g_passives current iterno =
     (* forward step *)
-    let bag, maxvar, actives, passives =
-      match select passives with
-      | None -> bag, maxvar, actives, passives
-      | Some (current, passives) -> 
-          match Sup.forward_simplify (snd actives) bag current with
-          | None -> bag, maxvar, actives, passives
-          | Some (bag, current) ->
-              let bag, maxvar, actives, new_clauses = 
-                Sup.infer_right bag maxvar current actives 
-              in
-              bag, maxvar, actives, passives @ new_clauses
+    
+    (* e = select P           *
+     * e' = demod A e         *
+     * A' = demod [e'] A      *
+     * A'' = A' + e'          *
+     * e'' = fresh e'         *
+     * new = supright e'' A'' *
+     * new'= demod A'' new    *
+     * P' = P + new'          *)
+    debug (lazy "Forward infer step...");
+    debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
+    let bag, maxvar, actives, new_clauses = 
+      Sup.infer_right bag maxvar current actives 
+    in
+      debug (lazy "Demodulating goals with actives...");
+      (* keep goals demodulated w.r.t. actives and check if solved *)
+      let bag, g_actives = 
+        List.fold_left 
+          (fun (bag,acc) c -> 
+             match 
+               Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c
+             with
+               | None -> bag, acc
+               | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
+          (bag,[]) g_actives 
+      in
+      let ctable = IDX.index_clause IDX.DT.empty current in
+      let bag, maxvar, new_goals = 
+        List.fold_left 
+          (fun (bag,m,acc) g -> 
+             let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in
+               bag,m,ng@acc) 
+          (bag,maxvar,[]) g_actives 
+      in
+      let bag = Terms.replace_in_bag (current,false,iterno) bag in
+    bag, maxvar, actives,
+    add_passive_clauses passives new_clauses, g_actives,
+    add_passive_goals g_passives new_goals
+  ;;
+ 
+  let rec given_clause ~useage ~noinfer 
+    bag maxvar iterno weight_picks max_steps timeout 
+    actives passives g_actives g_passives 
+  =
+    let iterno = iterno + 1 in
+    if iterno = max_steps then raise (Stop (Timeout (maxvar,bag)));
+    (* timeout check: gettimeofday called only if timeout set *)
+    if timeout <> None &&
+      (match timeout with
+      | None -> assert false
+      | Some timeout -> Unix.gettimeofday () > timeout) then
+        if noinfer then
+          begin
+            debug 
+              (lazy("Last chance: all is indexed " ^ string_of_float
+                (Unix.gettimeofday())));
+            let maxgoals = 100 in
+            ignore(List.fold_left 
+              (fun (acc,i) x -> 
+                 if i < maxgoals then
+                 ignore(Sup.simplify_goal ~no_demod:true 
+                          maxvar (snd actives) bag acc x)
+                 else
+                   ();
+                 x::acc,i+1)
+              ([],0) g_actives);
+            raise (Stop (Timeout (maxvar,bag)))
+          end
+        else if false then (* activates last chance strategy *)
+          begin
+           debug (lazy("Last chance: "^string_of_float (Unix.gettimeofday())));
+           given_clause ~useage ~noinfer:true bag maxvar iterno weight_picks max_steps 
+             (Some (Unix.gettimeofday () +. 20.))
+             actives passives g_actives g_passives;
+           raise (Stop (Timeout (maxvar,bag)));
+          end
+        else raise (Stop (Timeout (maxvar,bag)));
+
+    let use_age = useage && (weight_picks = (iterno / 6 + 1)) in
+    let weight_picks = if use_age then 0 else weight_picks+1
+    in
+
+    let rec aux_select bag passives g_passives =
+      let backward,(weight,current),passives,g_passives =
+        select ~use_age passives g_passives
+      in
+	if use_age && weight > monster then
+	  let bag,cl = Terms.add_to_bag current bag in
+	    if backward then
+	      aux_select bag passives (add_passive_clause g_passives cl)
+	    else
+	      aux_select bag (add_passive_clause passives cl) g_passives
+	else
+	  let bag = Terms.replace_in_bag (current,false,iterno) bag in
+        if backward then
+          let _ = debug (lazy("Selected goal : " ^ Pp.pp_clause current)) in
+         match 
+           if noinfer then 
+             if weight > monster then None else Some (bag,current)
+           else 
+             Sup.simplify_goal 
+               ~no_demod:false maxvar (snd actives) bag g_actives current 
+         with
+            | None -> aux_select bag passives g_passives
+            | Some (bag,g_current) ->
+               if noinfer then 
+                 let g_actives = g_current :: g_actives in 
+                 bag,maxvar,actives,passives,g_actives,g_passives
+               else
+                 backward_infer_step bag maxvar actives passives
+                   g_actives g_passives g_current iterno
+        else
+          let _ = debug (lazy("Selected fact : " ^ Pp.pp_clause current)) in
+	  (*let is_orphan = Sup.orphan_murder bag (fst actives) current in*)
+          match 
+            if noinfer then 
+              if weight > monster then bag,None 
+              else  bag, Some (current,actives)
+            else if Sup.orphan_murder bag (fst actives) current then
+	      let _ = debug (lazy "Orphan murdered") in
+              let bag = Terms.replace_in_bag (current,true,iterno) bag in
+                bag, None
+            else Sup.keep_simplified current actives bag maxvar
+          with
+        (*match Sup.one_pass_simplification current actives bag maxvar with*)
+              | bag,None -> aux_select bag passives g_passives
+              | bag,Some (current,actives) ->
+(*                    if is_orphan then prerr_endline
+                      ("WRONG discarded: " ^ (Pp.pp_unit_clause current));
+                  List.iter (fun x ->
+                               prerr_endline (Pp.pp_unit_clause x))
+                    (fst actives);*)
+
+(*                  List.iter (fun (id,_,_,_) -> let (cl,d) =
+                             Terms.M.find id bag in 
+                             if d then prerr_endline
+                               ("WRONG discarded: " ^ (Pp.pp_unit_clause cl)))
+                    (current::fst actives);*)
+                  if noinfer then
+                    let actives = 
+                      current::fst actives,
+                      IDX.index_clause (snd actives) current
+                    in
+                    bag,maxvar,actives,passives,g_actives,g_passives
+                  else
+                    forward_infer_step bag maxvar actives passives
+                      g_actives g_passives current iterno
     in
+    
+
+      (*prerr_endline "Active table :"; 
+       (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
+          (fst actives)); *)
+    let bag,maxvar,actives,passives,g_actives,g_passives =      
+      aux_select bag passives g_passives
+    in
+      debug
+        (lazy(Printf.sprintf "Number of active goals : %d"
+           (List.length g_actives)));
+      debug
+        (lazy(Printf.sprintf "Number of passive goals : %d"
+           (passive_set_cardinal g_passives)));
+      debug
+        (lazy(Printf.sprintf "Number of actives : %d" (List.length (fst actives))));
+      debug
+        (lazy(Printf.sprintf "Number of passives : %d"
+           (passive_set_cardinal passives)));
+      given_clause ~useage ~noinfer
+        bag maxvar iterno weight_picks max_steps timeout 
+        actives passives g_actives g_passives
+  ;;
+
+  let paramod ~useage ~max_steps ~print_problem ?timeout goal hypotheses =
+    let initial_timestamp = Unix.gettimeofday () in
+    let bag = Terms.empty_bag in
+    let maxvar = 0 in
+    let build_clause (bag,maxvar,l) (t,(nlit,plit)) =
+      let c,maxvar = Utils.mk_clause maxvar nlit plit t in
+      let bag,c = Terms.add_to_bag c bag in
+      (bag,maxvar,c::l)
+    in
+    let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in
+    let bag,maxvar,goals = build_clause (bag,maxvar,[]) goal in
+    let goal = match goals with | [g] -> g | _ -> assert false in
+    let passives =
+      add_passive_clauses ~no_weight:true passive_empty_set hypotheses
+    in
+    let g_passives =
+      add_passive_goal ~no_weight:true passive_empty_set goal
+    in
+    let g_actives = [] in
+    let actives = [], IDX.DT.empty in
+    if print_problem then begin
+       prerr_endline "Facts:";
+       List.iter (fun x -> prerr_endline (" " ^ Pp.pp_clause x)) hypotheses;
+       prerr_endline "Goal:";
+       prerr_endline (" " ^ Pp.pp_clause goal);
+    end;
+    try 
+     given_clause ~useage ~noinfer:false
+      bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
+    with 
+    | Sup.Success (bag, _, (i,_,_,_,_)) ->
+        let l =
+          let rec traverse ongoal (accg,acce) i =
+            match Terms.get_from_bag i bag with
+              | (id,_,_,_,Terms.Exact _),_,_ ->
+                  if ongoal then [i],acce else
+                    if (List.mem i acce) then accg,acce else accg,acce@[i]
+              | (_,_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ ->
+                  if (not ongoal) && (List.mem i acce) then accg,acce
+                  else
+                    let accg,acce = 
+                      traverse false (traverse ongoal (accg,acce) i1) i2
+                    in
+                      if ongoal then i::accg,acce else accg,i::acce
+          in
+          let gsteps,esteps = traverse true ([],[]) i in
+            (List.rev esteps)@gsteps
+        in
+	let max_w = List.fold_left (fun acc i ->
+		    let (cl,_,_) = Terms.get_from_bag i bag in
+		    max acc (Order.compute_clause_weight cl)) 0 l in
+	  prerr_endline "Statistics :";
+	  prerr_endline ("Max weight : " ^ (string_of_int max_w));
+(*	  List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) =
+	    Terms.get_from_bag id bag in
+	      if d then
+		prerr_endline
+		(Printf.sprintf "Id : %d, selected at %d, weight %d,disc, by %s"
+		   id it (Order.compute_unit_clause_weight cl) 
+		   (Pp.pp_proof_step proof))
+	      else
+	       prerr_endline
+		(Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
+		   id it (Order.compute_unit_clause_weight cl) 
+		   (Pp.pp_proof_step proof))) l;*)
+        prerr_endline 
+          (Printf.sprintf "Found proof, %fs" 
+            (Unix.gettimeofday() -. initial_timestamp));
+        (* 
+        prerr_endline "Proof:"; 
+        List.iter (fun x ->
+          prerr_endline (Pp.pp_unit_clause (fst(Terms.M.find x bag)))) l;
+        *)
+        Unsatisfiable [ bag, i, l ]
+    | Stop (Unsatisfiable _) -> Error "stop bug solution found!"
+    | Stop o -> o
+  ;;
 
-      given_clause bag maxvar actives passives g_actives g_passives
-  in
-
-  let mk_clause bag maxvar ty =
-    let ty = B.embed ty in
-    let proof = B.embed (NCic.Rel ~-1) in
-    let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
-    let bag, c = Utils.add_to_bag bag c in
-    bag, maxvar, c
-  in
-  let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
-  let g_actives = [] in
-  let g_passives = [goal] in
-  let passives, bag, maxvar = 
-    List.fold_left
-      (fun (cl, bag, maxvar) t -> 
-         let bag, maxvar, c = mk_clause bag maxvar t in
-         c::cl, bag, maxvar)
-      ([], bag, maxvar) table 
-  in
-  let actives = [], IDX.DT.empty in
-  try given_clause bag maxvar actives passives g_actives g_passives
-  with Sup.Success _ -> prerr_endline "YES!"
-;;
+end