superposition_left not performed if the input goal is an identity

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index e7166324de60d735480374a21595b3c9b1af8318..c74abe27d4605b8cf7b2638b826b8181d2bf77ca 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -1049,6 +1049,7 @@ let build_newgoal context goal posu rule expansion =
    the negative equation "target" and one of the positive equations in "table"
 *)
 let superposition_left (metasenv, context, ugraph) table goal = 
+  let names = Utils.names_of_context context in
   let proof,menv,eq,ty,l,r = open_goal goal in
   let c = !Utils.compare_terms l r in
   if c = Utils.Incomparable then
@@ -1064,14 +1065,24 @@ let superposition_left (metasenv, context, ugraph) table goal =
     List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
     end
   else
-    let big,small,possmall = 
       match c with 
-        Utils.Gt -> (* prerr_endline "GT"; *) l,r,Utils.Right 
-      | Utils.Lt -> (* prerr_endline "LT"; *) r,l,Utils.Left
-      | _ -> assert false
-    in
-    let expansions, _ = betaexpand_term menv context ugraph table 0 big in
-    List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
+      | Utils.Gt -> (* prerr_endline "GT"; *) 
+          let big,small,possmall = l,r,Utils.Right in
+          let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+          List.map 
+            (build_newgoal context goal possmall Equality.SuperpositionLeft) 
+            expansions
+      | Utils.Lt -> (* prerr_endline "LT"; *) 
+          let big,small,possmall = r,l,Utils.Left in
+          let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+          List.map 
+            (build_newgoal context goal possmall Equality.SuperpositionLeft) 
+            expansions
+      | Utils.Eq -> []
+      | _ ->
+          prerr_endline 
+            ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
+          assert false
 ;;
 
 (** demodulation, when the target is a goal *)

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 81c2a15f1920d2cd7e496643cf912d6042432bc3..e7ef6fa7c2b9def7764a18273fef1981eaf91baa 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -1188,6 +1188,15 @@ let given_clause
                   let new' = infer eq_uri env current active in
                   prerr_endline "infer goal";
                   let goals = infer_goal_set_with_current env current goals in
+(*
+      match check_if_goals_set_is_solved env active goals with
+      | Some p -> 
+          prerr_endline 
+            (Printf.sprintf "Found a proof in: %f\n" 
+              (Unix.gettimeofday() -. initial_time));
+          ParamodulationSuccess p
+      | None -> 
+*)
                   let active = 
                       let al, tbl = active in
                       al @ [current], Indexing.index tbl current
@@ -1555,7 +1564,7 @@ let saturate
 *)
       let goals = make_goal_set goal in
       let max_iterations = 10000 in
-      let max_time = Unix.gettimeofday () +.  600. (* minutes *) in
+      let max_time = Unix.gettimeofday () +.  300. (* minutes *) in
       given_clause 
         eq_uri env goals theorems passive active max_iterations max_time 
     in