]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/paramod.ml
Rewrote the main loop for paramodulation
[helm.git] / helm / software / components / ng_paramodulation / paramod.ml
index d0129279065f1ec620d4aa9d824a6fa978f301b0..fc44be0486e990d399f1dd48a9e382fb0b0dea93 100644 (file)
@@ -1,7 +1,7 @@
 (* LOOPING : COL057-1.ma *)
 
 let debug s =
-  () (* prerr_endline s *)
+   prerr_endline s
 ;;
 
 let nparamod rdb metasenv subst context t table =
@@ -34,14 +34,97 @@ let nparamod rdb metasenv subst context t table =
     PassiveSet.add (Utils.mk_passive_clause cl) passives
   in
   let timeout = Unix.gettimeofday () +. amount_of_time in 
+
     (* TODO : fairness condition *)
-  let select passives =
-    if PassiveSet.is_empty passives then None
+  let select passives g_passives =
+    if PassiveSet.is_empty passives then begin
+      assert (not (PassiveSet.is_empty g_passives));
+      let g_cl = PassiveSet.min_elt g_passives in
+       (true,snd g_cl,passives,PassiveSet.remove g_cl g_passives)
+    end
     else let cl = PassiveSet.min_elt passives in
-      Some (snd cl,PassiveSet.remove cl passives)
+      if PassiveSet.is_empty g_passives then
+       (false,snd cl,PassiveSet.remove cl passives,g_passives)
+      else
+       let g_cl = PassiveSet.min_elt g_passives in
+         if (fst cl <= fst g_cl) then
+           (false,snd cl,PassiveSet.remove cl passives,g_passives)
+         else
+           (true,snd g_cl,passives,PassiveSet.remove g_cl g_passives)
+  in
+
+  let backward_infer_step bag maxvar actives passives g_actives g_passives g_current =
+    (* superposition left, simplifications on goals *)
+      debug "infer_left step...";
+    debug ("Selected goal : " ^ Pp.pp_unit_clause g_current);
+    let bag, g_current = 
+      Sup.simplify_goal maxvar (snd actives) bag g_current
+    in
+      debug "Simplified goal";
+      let bag, maxvar, new_goals = 
+        Sup.infer_left bag maxvar g_current actives 
+      in
+       debug "Performed infer_left step";
+       let new_goals = List.fold_left add_passive_clause
+         PassiveSet.empty new_goals
+       in
+          bag, maxvar, actives, passives, g_current::g_actives,
+    (PassiveSet.union new_goals g_passives)
+  in
+
+  let forward_infer_step bag maxvar actives passives g_actives
+                         g_passives current =
+    (* forward step *)
+    
+    (* 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 "Forward infer step...";
+    debug "Selected and simplified";
+    (* debug ("Fact after simplification :"
+       ^ Pp.pp_unit_clause current); *)
+    let bag, maxvar, actives, new_clauses = 
+      Sup.infer_right bag maxvar current actives 
+    in
+      debug "Demodulating goals with actives...";
+      debug ("Current : " ^ (Pp.pp_unit_clause current));
+      debug ("Active goal : " ^ (Pp.pp_unit_clause (List.hd g_actives)));
+      (* keep goals demodulated w.r.t. actives and check if solved *)
+      let bag, g_actives = 
+       List.fold_left 
+          (fun (bag,acc) c -> 
+            let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
+              bag, c::acc) 
+          (bag,[]) g_actives 
+      in
+      debug (Pp.pp_unit_clause current);
+      debug (Pp.pp_unit_clause (List.hd g_actives));
+      let ctable = IDX.index_unit_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 new_clauses = List.fold_left add_passive_clause
+       PassiveSet.empty new_clauses in
+      let new_goals = List.fold_left add_passive_clause
+       PassiveSet.empty new_goals in
+       debug (string_of_int (PassiveSet.cardinal new_goals));
+       debug (string_of_int (PassiveSet.cardinal g_passives));
+       bag, maxvar, actives,
+    PassiveSet.union new_clauses passives, g_actives,
+    PassiveSet.union new_goals g_passives
   in
-  let rec given_clause bag maxvar actives      
-      passives g_actives g_passives =
+
+  let rec given_clause bag maxvar actives passives g_actives g_passives =
     (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
       prerr_endline "Active table :"; 
        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
@@ -52,90 +135,31 @@ let nparamod rdb metasenv subst context t table =
       raise (Failure "Timeout !");
 
 
-      
-    (* superposition left, simplifications on goals *)
-      debug "infer_left 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) -> 
-         debug ("Selected goal : " ^ Pp.pp_unit_clause g_current);
-          let bag, g_current = 
-            Sup.simplify_goal maxvar (snd actives) bag g_current
-          in
-           debug "Simplified goal";
-          let bag, maxvar, new_goals = 
-            Sup.infer_left bag maxvar g_current actives 
-          in
-           debug "Performed infer_left step";
-         let new_goals = List.fold_left add_passive_clause
-           PassiveSet.empty new_goals
-         in
-          bag, maxvar, g_current::g_actives,
-         (PassiveSet.union new_goals g_passives)
+    let rec aux_select passives g_passives =
+      let backward,current,passives,g_passives = select passives g_passives in
+       if backward then
+         backward_infer_step bag maxvar actives passives
+                             g_actives g_passives current
+       else
+         (* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *)
+          match Sup.keep_simplified current actives bag maxvar with
+       (*  match Sup.one_pass_simplification current actives bag maxvar with*)
+             | None -> aux_select passives g_passives
+             | Some x -> let (current, bag, actives) = x in
+                 forward_infer_step bag maxvar actives passives
+                                    g_actives g_passives current
+    in
+
+    let bag,maxvar,actives,passives,g_actives,g_passives =      
+      aux_select passives g_passives
     in
+      assert (PassiveSet.cardinal g_passives < 2);
       debug
        (Printf.sprintf "Number of active goals : %d"
           (List.length g_actives));
       debug
        (Printf.sprintf "Number of passive goals : %d"
           (PassiveSet.cardinal g_passives));
-  
-      (* forward step *)
-      (* 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 "Forward infer step...";
-    let bag, maxvar, actives, passives, g_passives =
-      let rec aux_simplify passives =
-       match select passives with
-         | None -> assert false
-         | Some (current, passives) -> 
-             debug ("Selected fact : " ^ Pp.pp_unit_clause current);
-                match Sup.keep_simplified current actives bag maxvar with
-(*  match Sup.one_pass_simplification current actives bag maxvar with*)
-               | None -> aux_simplify passives
-               | Some x -> x,passives
-      in
-      let (current, bag, actives),passives = aux_simplify passives
-      in                   
-       debug ("Fact after simplification :"
-              ^ Pp.pp_unit_clause current);
-       let bag, maxvar, actives, new_clauses = 
-          Sup.infer_right bag maxvar current actives 
-       in
-  debug "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 -> 
-               let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
-                bag, c::acc) 
-            (bag,[]) g_actives 
-       in
-       let ctable = IDX.index_unit_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 new_clauses = List.fold_left add_passive_clause
-         PassiveSet.empty new_clauses in
-       let new_goals = List.fold_left add_passive_clause
-         PassiveSet.empty new_goals in
-         bag, maxvar, actives,
-      PassiveSet.union new_clauses passives,
-      PassiveSet.union new_goals g_passives
-    in
       debug
        (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
       debug