From a200ab05cafa2e2b1075d04235042ee8e99f046e Mon Sep 17 00:00:00 2001 From: denes Date: Mon, 22 Jun 2009 16:51:14 +0000 Subject: [PATCH] Corrected proof visiting (topological sort) --- .../components/ng_paramodulation/nCicBlob.ml | 7 +- .../components/ng_paramodulation/paramod.ml | 71 ++++++++----------- .../components/ng_paramodulation/pp.ml | 12 +++- .../ng_paramodulation/superposition.ml | 37 ++++++---- 4 files changed, 71 insertions(+), 56 deletions(-) diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index 46710db21..dcc2aba30 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -217,8 +217,11 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct aux ongoal ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) | Terms.Step (_, id1, id2, dir, pos, subst) -> - let id, id1 = if ongoal then id1,id else id,id1 in - let lit,vl,_ = get_literal id in + let id, id1,(lit,vl,proof) = + if ongoal then id1,id,get_literal id1 + else id,id1,(lit,vl,proof) + in + let vl = if ongoal then Subst.filter subst vl else vl in let proof_of_id id = let vars = List.rev (vars_of id seen) in let args = List.map (Subst.apply_subst subst) vars in diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 5f75fb3aa..8530be3e8 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -1,16 +1,19 @@ +(* LOOPING : COL057-1.ma *) + let debug s = - () (* prerr_endline s *) + prerr_endline s ;; let nparamod rdb metasenv subst context t table = - let nb_iter = ref 200 in - let amount_of_time = 20.0 in + let max_nb_iter = 999999999 in + let amount_of_time = 10.0 in let module C = struct let metasenv = metasenv let subst = subst let context = context end in + let nb_iter = ref 0 in let module B = NCicBlob.NCicBlob(C) in let module Pp = Pp.Pp (B) in let module FU = FoUnif.Founif(B) in @@ -40,7 +43,7 @@ let nparamod rdb metasenv subst context t table = let rec given_clause bag maxvar actives passives g_actives g_passives = - decr nb_iter; if !nb_iter = 0 then + incr nb_iter; if !nb_iter = max_nb_iter then (*(prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag); prerr_endline "Active table :"; (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x)) @@ -61,9 +64,11 @@ let nparamod rdb metasenv subst context t table = 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 @@ -94,8 +99,8 @@ let nparamod rdb metasenv subst context t table = | 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 + 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 @@ -161,43 +166,28 @@ let nparamod rdb metasenv subst context t table = with | Sup.Success (bag, _, (i,_,_,_)) -> let l = - let module S = - HTopoSort.Make(struct type t=int let compare=Pervasives.compare end) - in - let module C : Set.S with type elt = int = - Set.Make(struct type t=int let compare=Pervasives.compare end) - in - let all id = - let rec traverse ongoal (accg,acce) i = - match Terms.M.find i bag with - | (_,_,_,Terms.Exact _) -> accg, acce - | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) -> - let accg, acce = - if ongoal then C.add i1 accg, acce - else accg, C.add i1 acce - in - let acce = C.add i2 acce in - traverse false (traverse ongoal (accg,acce) i1) i2 - in - traverse true (C.empty,C.empty) id - in - let esteps = - S.topological_sort (C.elements (snd (all i))) - (fun i -> C.elements (C.union (snd (all i)) (fst (all i)) )) - in - let gsteps = - S.topological_sort (C.elements (fst (all i))) - (fun i -> C.elements (fst (all i))) + let rec traverse ongoal (accg,acce) i = + match Terms.M.find 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 = List.rev gsteps in - esteps@(i::gsteps) + let gsteps,esteps = traverse true ([],[]) i in + (List.rev esteps)@gsteps in -(* - prerr_endline "Proof:"; + prerr_endline (Printf.sprintf "Found proof in %d iterations" !nb_iter); + (* prerr_endline "Proof:"; List.iter (fun x -> prerr_endline (string_of_int x); - prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l; -*) + prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;*) let proofterm = B.mk_proof bag i l in + prerr_endline "Got proof term"; let metasenv, proofterm = let rec aux k metasenv = function | NCic.Meta _ as t -> metasenv, t @@ -215,5 +205,6 @@ let nparamod rdb metasenv subst context t table = metasenv subst context proofterm None in proofterm, metasenv, subst - | Failure _ -> prerr_endline "FAILURE"; assert false + | Failure _ -> prerr_endline + (Printf.sprintf "FAILURE in %d iterations" !nb_iter); assert false ;; diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index 29f257697..2e95e7a95 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -89,7 +89,17 @@ let pp_unit_clause ~formatter:f c = Format.fprintf f "Id : %3d, " id ; match l with | Terms.Predicate t -> - pp_foterm f t + Format.fprintf f "@[{"; + pp_foterm f t; + Format.fprintf f "@;[%s] by %s@]" + (String.concat ", " (List.map string_of_int vars)) + (match proof with + | Terms.Exact _ -> "axiom" + | Terms.Step (rule, id1, id2, _, p, _) -> + Printf.sprintf "%s %d with %d at %s" + (string_of_rule rule) + id1 id2 (String.concat + "," (List.map string_of_int p))) | Terms.Equation (lhs, rhs, ty, comp) -> Format.fprintf f "@[{"; pp_foterm f ty; diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index d823c5a53..0fc1f750a 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -23,7 +23,7 @@ module Superposition (B : Terms.Blob) = exception Success of B.t Terms.bag * int * B.t Terms.unit_clause let debug s = - () (* prerr_endline s *) + () (* prerr_endline s *) ;; let rec list_first f = function @@ -35,7 +35,7 @@ module Superposition (B : Terms.Blob) = let rec aux pos ctx = function | Terms.Leaf _ as t -> f t pos ctx | Terms.Var _ -> None - | Terms.Node l as t-> + | Terms.Node l as t-> match f t pos ctx with | Some _ as x -> x | None -> @@ -137,16 +137,25 @@ module Superposition (B : Terms.Blob) = * in normal form we should not traverse it again *) let demodulate_once bag (id, literal, vl, pr) table = (* debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));*) - let t = - match literal with - | Terms.Predicate t -> t - | Terms.Equation (l,r,ty,_) -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] - in - match first_position [] (fun x -> x) t (demod table vl) with - | None -> None - | Some (newt, subst, varlist, id2, pos, dir) -> - build_clause bag (fun _ -> true) Terms.Demodulation - newt subst varlist id id2 pos dir + match literal with + | Terms.Predicate t -> assert false + | Terms.Equation (l,r,ty,_) -> + match first_position [2] + (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l + (demod table vl) + with + | Some (newt, subst, varlist, id2, pos, dir) -> + build_clause bag (fun _ -> true) Terms.Demodulation + newt subst varlist id id2 pos dir + | None -> + match first_position + [3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) r + (demod table vl) + with + | None -> None + | Some (newt, subst, varlist, id2, pos, dir) -> + build_clause bag (fun _ -> true) Terms.Demodulation + newt subst varlist id id2 pos dir ;; let rec demodulate bag clause table = @@ -438,9 +447,10 @@ module Superposition (B : Terms.Blob) = let infer_left bag maxvar goal (_alist, atable) = (* We superpose the goal with active clauses *) - let bag, maxvar, new_goals = + let bag, maxvar, new_goals = superposition_with_table bag maxvar goal atable in + prerr_endline "Superposed goal with active clauses"; (* We demodulate the goal with active clauses *) let bag, new_goals = List.fold_left @@ -449,6 +459,7 @@ module Superposition (B : Terms.Blob) = bag, g :: acc) (bag, []) new_goals in + prerr_endline "Demodulated goal with active clauses"; bag, maxvar, List.rev new_goals ;; -- 2.39.2