From 94ec1bb0fcb0a82bfaaf965aed6993de3a9e658a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 29 Jun 2009 14:36:37 +0000 Subject: [PATCH] do not infer on closed goals --- .../components/ng_paramodulation/paramod.ml | 3 +-- .../ng_paramodulation/superposition.ml | 26 +++++++++++-------- .../components/syntax_extensions/.depend | 3 +++ 3 files changed, 19 insertions(+), 13 deletions(-) diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 435c95024..6c3c5118d 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -168,8 +168,7 @@ module Paramod (B : Terms.Blob) = struct 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 + let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in bag,m,ng@acc) (bag,maxvar,[]) g_actives in diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 8070b4b5d..84de696df 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -454,17 +454,19 @@ module Superposition (B : Terms.Blob) = then raise (Success (bag, maxvar, clause)) else let (id,lit,vl,_) = clause in - let l,r,ty = - match lit with - | Terms.Equation(l,r,ty,_) -> l,r,ty - | _ -> assert false - in - match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x) - table (Some(bag,maxvar,clause,Subst.id_subst)) with - | None -> Some (bag,clause) - | Some (bag,maxvar,cl,subst) -> - prerr_endline "Goal subsumed"; - raise (Success (bag,maxvar,cl)) + if vl = [] then Some (bag,clause) + else + let l,r,ty = + match lit with + | Terms.Equation(l,r,ty,_) -> l,r,ty + | _ -> assert false + in + match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x) + table (Some(bag,maxvar,clause,Subst.id_subst)) with + | None -> Some (bag,clause) + | Some (bag,maxvar,cl,subst) -> + prerr_endline "Goal subsumed"; + raise (Success (bag,maxvar,cl)) (* else match is_subsumed ~unify:true bag maxvar clause table with | None -> Some (bag, clause) @@ -590,6 +592,8 @@ module Superposition (B : Terms.Blob) = let infer_left bag maxvar goal (_alist, atable) = (* We superpose the goal with active clauses *) + if (match goal with (_,_,[],_) -> true | _ -> false) then bag, maxvar, [] + else let bag, maxvar, new_goals = superposition_with_table bag maxvar goal atable in diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index f3c6a8bd1..25e67131f 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,2 +1,5 @@ +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi -- 2.39.2