From: Enrico Tassi Date: Wed, 28 Jun 2006 10:28:58 +0000 (+0000) Subject: superposition_left not performed if the input goal is an identity X-Git-Tag: make_still_working~7132 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a0cb7cf4ac234997157aac20a1a68a4a88e805e1;p=helm.git superposition_left not performed if the input goal is an identity --- diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index e7166324d..c74abe27d 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/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/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 81c2a15f1..e7ef6fa7c 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/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