From d8c8060ad0cfc9b93ce919b6662383a230192840 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Sun, 15 May 2005 12:08:59 +0000 Subject: [PATCH] fixes (mainly) to demodulation and meta_convertibility --- helm/ocaml/paramodulation/.cvsignore | 1 + helm/ocaml/paramodulation/inference.ml | 368 ++++++++++++++---------- helm/ocaml/paramodulation/inference.mli | 5 +- helm/ocaml/paramodulation/saturation.ml | 209 ++++++++------ helm/ocaml/paramodulation/utils.ml | 7 +- helm/ocaml/paramodulation/utils.mli | 2 +- 6 files changed, 339 insertions(+), 253 deletions(-) diff --git a/helm/ocaml/paramodulation/.cvsignore b/helm/ocaml/paramodulation/.cvsignore index 9ef1b560e..6f54c3772 100644 --- a/helm/ocaml/paramodulation/.cvsignore +++ b/helm/ocaml/paramodulation/.cvsignore @@ -1,2 +1,3 @@ *.cm[iaox] *.cmxa .depend +saturatio.opt diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index c4b0a842f..987c17cc8 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -9,11 +9,18 @@ let meta_convertibility_aux table t1 t2 = match t1, t2 with | t1, t2 when t1 = t2 -> table | C.Meta (m1, tl1), C.Meta (m2, tl2) -> - let m1_binding, table = - try List.assoc m1 table, table - with Not_found -> m2, (m1, m2)::table + let m1_binding, m2_binding, table = + let m1b, table = + try List.assoc m1 table, table + with Not_found -> m2, (m1, m2)::table + in + let m2b, table = + try List.assoc m2 table, table + with Not_found -> m1, (m2, m1)::table + in + m1b, m2b, table in - if m1_binding <> m2 then + if m1_binding <> m2 || m2_binding <> m1 then raise NotMetaConvertible else ( try @@ -105,17 +112,18 @@ let meta_convertibility_eq eq1 eq2 = in try let table = meta_convertibility_aux [] left left' in -(* print_table table "before"; *) let _ = meta_convertibility_aux table right right' in -(* print_table table "after"; *) +(* Printf.printf "meta_convertibility_eq, ok:\n%s\n%s\n" *) +(* (string_of_equality eq1) (string_of_equality eq2); *) +(* print_newline (); *) true with NotMetaConvertible -> -(* Printf.printf "NotMetaConvertible:\n%s = %s\n%s = %s\n\n" *) -(* (CicPp.ppterm left) (CicPp.ppterm right) *) -(* (CicPp.ppterm left') (CicPp.ppterm right'); *) try let table = meta_convertibility_aux [] left right' in let _ = meta_convertibility_aux table right left' in +(* Printf.printf "meta_convertibility_eq, ok:\n%s\n%s\n" *) +(* (string_of_equality eq1) (string_of_equality eq2); *) +(* print_newline (); *) true with NotMetaConvertible -> false @@ -135,6 +143,13 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) what type_of_what where context metasenv ugraph = let module S = CicSubstitution in let module C = Cic in +(* let _ = *) +(* let names = names_of_context context in *) +(* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *) +(* (CicPp.pp what names) (CicPp.ppterm what) *) +(* (CicPp.pp where names) (CicPp.ppterm where); *) +(* print_newline (); *) +(* in *) (* return value: ((list of all possible beta expansions, subst, metasenv, ugraph), @@ -381,6 +396,8 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) | _ -> try let subst', metasenv', ugraph' = +(* Printf.printf "provo a unificare %s e %s\n" *) +(* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *) CicUnification.fo_unif metasenv context (S.lift lift_amount what) term ugraph in @@ -390,11 +407,11 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *) (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *) if match_only then - let term' = CicMetaSubst.apply_subst subst' term in - if not (meta_convertibility term term') then ( -(* let names = names_of_context context in *) -(* Printf.printf "\nterm e term' sono diversi!:\n%s\n%s\n\n" *) -(* (CicPp.pp term names) (CicPp.pp term' names); *) + let t' = CicMetaSubst.apply_subst subst' term in + if not (meta_convertibility term t') then ( + let names = names_of_context context in +(* Printf.printf "\nbeta_expand: term e t' sono diversi!:\n%s\n%s\n\n" *) +(* (CicPp.pp term names) (CicPp.pp t' names); *) res, lifted_term ) else @@ -403,7 +420,8 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) else ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, lifted_term) - with _ -> + with e -> +(* print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e)); *) res, lifted_term in (* Printf.printf "exit aux\n"; *) @@ -514,11 +532,14 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) = + let table = Hashtbl.create (List.length args) in let newargs, _ = List.fold_right (fun t (newargs, index) -> match t with - | Cic.Meta (i, l) -> ((Cic.Meta (index, l))::newargs, index+1) + | Cic.Meta (i, l) -> + Hashtbl.add table i index; + ((Cic.Meta (index, l))::newargs, index+1) | _ -> assert false) args ([], newmeta) in @@ -526,11 +547,15 @@ let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) = ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs ~where in - let menv', _ = + let menv' = List.fold_right - (fun (i, context, term) (menv, index) -> - ((index, context, term)::menv, index+1)) - menv ([], newmeta) + (fun (i, context, term) menv -> + try + let index = Hashtbl.find table i in + (index, context, term)::menv + with Not_found -> + (i, context, term)::menv) + menv [] in (newmeta + (List.length newargs) + 1, (repl proof, (repl ty, repl left, repl right), menv', newargs)) @@ -562,62 +587,66 @@ let superposition_left (metasenv, context, ugraph) target source = let eqproof, (ty, t1, t2), newmetas, args = source in (* ALB: TODO check that ty and eq_ty are indeed equal... *) - assert (eq_ty = ty); - - let where, is_left = - match nonrec_kbo left right with - | Lt -> right, false - | Gt -> left, true - | _ -> ( - Printf.printf "????????? %s = %s" (CicPp.ppterm left) - (CicPp.ppterm right); - print_newline (); - assert false (* again, for ground terms this shouldn't happen... *) - ) - in - let metasenv' = newmetas @ metasenv in - let res1 = - List.filter - (fun (t, s, m, ug) -> - nonrec_kbo (M.apply_subst s t1) (M.apply_subst s t2) = Gt) - (beta_expand t1 ty where context metasenv' ugraph) - and res2 = - List.filter - (fun (t, s, m, ug) -> - nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt) - (beta_expand t2 ty where context metasenv' ugraph) - in -(* let what, other = *) -(* if is_left then left, right *) -(* else right, left *) -(* in *) - let build_new what other eq_URI (t, s, m, ug) = - let newgoal, newgoalproof = - match t with - | C.Lambda (nn, ty, bo) -> - let bo' = S.subst (M.apply_subst s other) bo in - let bo'' = - C.Appl ( - [C.MutInd (HL.Logic.eq_URI, 0, []); - S.lift 1 eq_ty] @ - if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo']) - in - let t' = C.Lambda (nn, ty, bo'') in - S.subst (M.apply_subst s other) bo, - M.apply_subst s - (C.Appl [C.Const (eq_URI, []); ty; what; t'; - proof; other; eqproof]) - | _ -> assert false + (* assert (eq_ty = ty); *) + + if eq_ty <> ty then + [] + else + let where, is_left = + match nonrec_kbo left right with + | Lt -> right, false + | Gt -> left, true + | _ -> ( + Printf.printf "????????? %s = %s" (CicPp.ppterm left) + (CicPp.ppterm right); + print_newline (); + assert false (* again, for ground terms this shouldn't happen... *) + ) in - let equation = - if is_left then (eq_ty, newgoal, right) - else (eq_ty, left, newgoal) + let metasenv' = newmetas @ metasenv in + let res1 = + List.filter + (fun (t, s, m, ug) -> + nonrec_kbo (M.apply_subst s t1) (M.apply_subst s t2) = Gt) + (beta_expand t1 ty where context metasenv' ugraph) + and res2 = + List.filter + (fun (t, s, m, ug) -> + nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt) + (beta_expand t2 ty where context metasenv' ugraph) in - (eqproof, equation, [], []) - in - let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1 - and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in - new1 @ new2 + (* let what, other = *) + (* if is_left then left, right *) + (* else right, left *) + (* in *) + let build_new what other eq_URI (t, s, m, ug) = + let newgoal, newgoalproof = + match t with + | C.Lambda (nn, ty, bo) -> + let bo' = S.subst (M.apply_subst s other) bo in + let bo'' = + C.Appl ( + [C.MutInd (HL.Logic.eq_URI, 0, []); + S.lift 1 eq_ty] @ + if is_left then [bo'; S.lift 1 right] + else [S.lift 1 left; bo']) + in + let t' = C.Lambda (nn, ty, bo'') in + S.subst (M.apply_subst s other) bo, + M.apply_subst s + (C.Appl [C.Const (eq_URI, []); ty; what; t'; + proof; other; eqproof]) + | _ -> assert false + in + let equation = + if is_left then (eq_ty, newgoal, right) + else (eq_ty, left, newgoal) + in + (eqproof, equation, [], []) + in + let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1 + and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in + new1 @ new2 ;; @@ -632,84 +661,103 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = let maxmeta = ref newmeta in (* TODO check if ty and ty' are equal... *) - assert (eq_ty = ty'); - -(* let ok term subst other other_eq_side ugraph = *) -(* match term with *) -(* | C.Lambda (nn, ty, bo) -> *) -(* let bo' = S.subst (M.apply_subst subst other) bo in *) -(* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *) -(* not res *) -(* | _ -> assert false *) -(* in *) - let condition left right what other (t, s, m, ug) = - let subst = M.apply_subst s in - let cmp1 = nonrec_kbo (subst what) (subst other) in - let cmp2 = nonrec_kbo (subst left) (subst right) in -(* cmp1 = Gt && cmp2 = Gt *) - cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le -(* && (ok t s other right ug) *) - in - let metasenv' = metasenv @ newmetas @ newm' in - let beta_expand = beta_expand ~metas_ok:false in - let res1 = - List.filter - (condition left right t1 t2) - (beta_expand t1 eq_ty left context metasenv' ugraph) - and res2 = - List.filter - (condition left right t2 t1) - (beta_expand t2 eq_ty left context metasenv' ugraph) - and res3 = - List.filter - (condition right left t1 t2) - (beta_expand t1 eq_ty right context metasenv' ugraph) - and res4 = - List.filter - (condition right left t2 t1) - (beta_expand t2 eq_ty right context metasenv' ugraph) - in - let newmetas = newmetas @ newm' in - let newargs = args @ args' in - let build_new what other is_left eq_URI (t, s, m, ug) = -(* let what, other = *) -(* if is_left then left, right *) -(* else right, left *) -(* in *) - let newterm, neweqproof = - match t with - | C.Lambda (nn, ty, bo) -> - let bo' = M.apply_subst s (S.subst other bo) in - let bo'' = - C.Appl ( - [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ - if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo']) - in - let t' = C.Lambda (nn, ty, bo'') in - bo', - M.apply_subst s - (C.Appl [C.Const (eq_URI, []); ty; what; t'; eqproof; other; eqp']) - | _ -> assert false + (* assert (eq_ty = ty'); *) + + if eq_ty <> ty' then + newmeta, [] + else + (* let ok term subst other other_eq_side ugraph = *) + (* match term with *) + (* | C.Lambda (nn, ty, bo) -> *) + (* let bo' = S.subst (M.apply_subst subst other) bo in *) + (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *) + (* not res *) + (* | _ -> assert false *) + (* in *) + let condition left right what other (t, s, m, ug) = + let subst = M.apply_subst s in + let cmp1 = nonrec_kbo (subst what) (subst other) in + let cmp2 = nonrec_kbo (subst left) (subst right) in + (* cmp1 = Gt && cmp2 = Gt *) + cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le + (* && (ok t s other right ug) *) in - let newmeta, newequality = - let left, right = - if is_left then (newterm, M.apply_subst s right) - else (M.apply_subst s left, newterm) in - fix_metas !maxmeta - (neweqproof, (eq_ty, left, right), newmetas, newargs) + let metasenv' = metasenv @ newmetas @ newm' in + let beta_expand = beta_expand ~metas_ok:false in + let res1 = + List.filter + (condition left right t1 t2) + (beta_expand t1 eq_ty left context metasenv' ugraph) + and res2 = + List.filter + (condition left right t2 t1) + (beta_expand t2 eq_ty left context metasenv' ugraph) + and res3 = + List.filter + (condition right left t1 t2) + (beta_expand t1 eq_ty right context metasenv' ugraph) + and res4 = + List.filter + (condition right left t2 t1) + (beta_expand t2 eq_ty right context metasenv' ugraph) in - maxmeta := newmeta; - newequality - in - let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1 - and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2 - and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3 - and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in - let ok = function - | _, (_, left, right), _, _ -> - not (fst (CR.are_convertible context left right ugraph)) - in - !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4)) + let newmetas = newmetas @ newm' in + let newargs = args @ args' in + let build_new what other is_left eq_URI (t, s, m, ug) = + (* let what, other = *) + (* if is_left then left, right *) + (* else right, left *) + (* in *) + let newterm, neweqproof = + match t with + | C.Lambda (nn, ty, bo) -> + let bo' = M.apply_subst s (S.subst other bo) in + let bo'' = + C.Appl ( + [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ + if is_left then [bo'; S.lift 1 right] + else [S.lift 1 left; bo']) + in + let t' = C.Lambda (nn, ty, bo'') in + bo', + M.apply_subst s + (C.Appl [C.Const (eq_URI, []); ty; what; t'; + eqproof; other; eqp']) + | _ -> assert false + in + let newmeta, newequality = + let left, right = + if is_left then (newterm, M.apply_subst s right) + else (M.apply_subst s left, newterm) in + fix_metas !maxmeta + (neweqproof, (eq_ty, left, right), newmetas, newargs) + in + maxmeta := newmeta; + newequality + in + let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1 + and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2 + and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3 + and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in + let ok = function + | _, (_, left, right), _, _ -> + not (fst (CR.are_convertible context left right ugraph)) + in + !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4)) +;; + + +let is_identity ((_, context, ugraph) as env) = function + | ((_, (ty, left, right), _, _) as equality) -> + let res = + (left = right || + (fst (CicReduction.are_convertible context left right ugraph))) + in +(* if res then ( *) +(* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *) +(* print_newline (); *) +(* ); *) + res ;; @@ -743,7 +791,7 @@ let demodulation newmeta (metasenv, context, ugraph) target source = (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *) (* (string_of_equality ~env target) (CicPp.pp what names) *) (* (CicPp.pp other names) (string_of_bool is_left); *) -(* Printf.printf "step: %d\n" step; *) +(* Printf.printf "step: %d" step; *) (* print_newline (); *) let ok (t, s, m, ug) = @@ -756,6 +804,9 @@ let demodulation newmeta (metasenv, context, ugraph) target source = in (* print_endline "res:"; *) (* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *) +(* print_newline (); *) +(* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *) +(* print_newline (); *) List.filter ok r in match res with @@ -790,12 +841,15 @@ let demodulation newmeta (metasenv, context, ugraph) target source = fix_metas newmeta (newproof, (eq_ty, left, right), newmetasenv, newargs) in -(* Printf.printf *) -(* "demodulate, newtarget: %s\ntarget was: %s\n" *) -(* (string_of_equality ~env newtarget) *) -(* (string_of_equality ~env target); *) -(* print_newline (); *) - demodulate newmeta step metasenv newtarget + Printf.printf + "demodulate, newtarget: %s\ntarget was: %s\n" + (string_of_equality ~env newtarget) + (string_of_equality ~env target); + print_newline (); + if is_identity env newtarget then + newmeta, newtarget + else + demodulate newmeta step metasenv newtarget in demodulate newmeta 3 (metasenv @ metas') target ;; diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index a895340c5..4e1fe2c0a 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -59,7 +59,8 @@ val superposition_right: val demodulation: int -> environment -> equality -> equality -> int * equality -val meta_convertibility: Cic.term -> Cic.term -> bool - val meta_convertibility_eq: equality -> equality -> bool +val is_identity: environment -> equality -> bool + + diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 6508e75da..a0148fb35 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -22,32 +22,84 @@ struct let compare eq1 eq2 = match meta_convertibility_eq eq1 eq2 with | true -> 0 - | false -> Pervasives.compare eq1 eq2 + | false -> + let _, (ty, left, right), _, _ = eq1 + and _, (ty', left', right'), _, _ = eq2 in + let weight_of t = fst (weight_of_term ~consider_metas:false t) in + let w1 = (weight_of ty) + (weight_of left) + (weight_of right) + and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in + match Pervasives.compare w1 w2 with + | 0 -> Pervasives.compare eq1 eq2 + | res -> res end module EqualitySet = Set.Make(OrderedEquality);; - +let weight_age_ratio = ref 0;; (* settable by the user from the command line *) +let weight_age_counter = ref !weight_age_ratio;; + +let set_selection = ref (fun set -> EqualitySet.min_elt set);; + let select env passive = - match passive with - | hd::tl, pos -> (Negative, hd), (tl, pos) - | [], hd::tl -> (Positive, hd), ([], tl) - | _, _ -> assert false + let (neg_list, neg_set), (pos_list, pos_set) = passive in + if !weight_age_ratio > 0 then + weight_age_counter := !weight_age_counter - 1; + match !weight_age_counter with + | 0 -> ( + weight_age_counter := !weight_age_ratio; + match neg_list, pos_list with + | hd::tl, pos -> + (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set)) + | [], hd::tl -> + (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set)) + | _, _ -> assert false + ) + | _ -> + let remove eq l = + List.filter (fun e -> not (e = eq)) l + in + if EqualitySet.is_empty neg_set then + let current = !set_selection pos_set in + let passive = + (neg_list, neg_set), + (remove current pos_list, EqualitySet.remove current pos_set) + in + (Positive, current), passive + else + let current = !set_selection neg_set in + let passive = + (remove current neg_list, EqualitySet.remove current neg_set), + (pos_list, pos_set) + in + (Negative, current), passive ;; -(* -let select env passive = - match passive with - | neg, pos when EqualitySet.is_empty neg -> - let elem = EqualitySet.min_elt pos in - (Positive, elem), (neg, EqualitySet.remove elem pos) - | neg, pos -> - let elem = EqualitySet.min_elt neg in - (Negative, elem), (EqualitySet.remove elem neg, pos) +let make_passive neg pos = + let set_of equalities = + List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities + in + (neg, set_of neg), (pos, set_of pos) +;; + + +let add_to_passive passive (new_neg, new_pos) = + let (neg_list, neg_set), (pos_list, pos_set) = passive in + let ok set equality = not (EqualitySet.mem equality set) in + let neg = List.filter (ok neg_set) new_neg + and pos = List.filter (ok pos_set) new_pos in + let add set equalities = + List.fold_left (fun s e -> EqualitySet.add e s) set equalities + in + (neg @ neg_list, add neg_set neg), (pos_list @ pos, add pos_set pos) +;; + + +let passive_is_empty = function + | ([], _), ([], _) -> true + | _ -> false ;; -*) (* TODO: find a better way! *) @@ -104,54 +156,32 @@ let contains_empty env (negative, positive) = ;; -let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) = - let find sign eq1 eq2 = - if meta_convertibility_eq eq1 eq2 then ( -(* Printf.printf "Trovato equazione duplicata di segno %s\n%s\n\n" *) -(* (string_of_sign sign) (string_of_equality eq1); *) - true - ) else - false - in - let ok sign equalities equality = - not (List.exists (find sign equality) equalities) - in - let neg = List.filter (ok Negative passive_neg) new_neg in - let pos = List.filter (ok Positive passive_pos) new_pos in -(* let neg, pos = new_neg, new_pos in *) - (neg @ passive_neg, passive_pos @ pos) -;; - - -let is_identity ((_, context, ugraph) as env) = function - | ((_, (ty, left, right), _, _) as equality) -> - let res = - (left = right || - (fst (CicReduction.are_convertible context left right ugraph))) - in -(* if res then ( *) -(* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *) -(* print_newline (); *) -(* ); *) - res -;; - - let forward_simplify env (sign, current) active = -(* if sign = Negative then *) -(* Some (sign, current) *) -(* else *) - let rec aux env (sign, current) = - function - | [] -> Some (sign, current) - | (Negative, _)::tl -> aux env (sign, current) tl - | (Positive, equality)::tl -> - let newmeta, current = demodulation !maxmeta env current equality in - maxmeta := newmeta; - if is_identity env current then - None - else - aux env (sign, current) tl + (* first step, remove already present equalities *) + let duplicate = + let rec aux = function + | [] -> false + | (s, eq)::tl when s = sign -> + if meta_convertibility_eq current eq then true + else aux tl + | _::tl -> aux tl + in + aux active + in + if duplicate then + None + else + let rec aux env (sign, current) = function + | [] -> Some (sign, current) + | (Negative, _)::tl -> aux env (sign, current) tl + | (Positive, equality)::tl -> + let newmeta, current = + demodulation !maxmeta env current equality in + maxmeta := newmeta; + if is_identity env current then + None + else + aux env (sign, current) tl in aux env (sign, current) active ;; @@ -204,22 +234,12 @@ let backward_simplify env (sign, current) active = (fun (s, eq) res -> if find eq res then res else (s, eq)::res) active [] ;; - - -(* -let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) = - let add_all = List.fold_left (fun res eq -> EqualitySet.add eq res) in - add_all passive_neg new_neg, add_all passive_pos new_pos -;; -*) let rec given_clause env passive active = - match passive with -(* | s1, s2 when (EqualitySet.is_empty s1) && (EqualitySet.is_empty s2) -> *) -(* Failure *) - | [], [] -> Failure - | passive -> + match passive_is_empty passive with + | true -> Failure + | false -> (* Printf.printf "before select\n"; *) let (sign, current), passive = select env passive in (* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *) @@ -232,17 +252,19 @@ let rec given_clause env passive active = let proof, _, _, _ = current in Success (Some proof, env) | None -> - Printf.printf "avanti... %s %s" (string_of_sign sign) - (string_of_equality ~env current); - print_newline (); +(* Printf.printf "avanti... %s %s" (string_of_sign sign) *) +(* (string_of_equality ~env current); *) +(* print_newline (); *) given_clause env passive active | Some (sign, current) -> -(* Printf.printf "sign: %s\ncurrent: %s\n" *) +(* Printf.printf "selected: %s %s" *) (* (string_of_sign sign) (string_of_equality ~env current); *) (* print_newline (); *) let new' = infer env sign current active in + let new' = forward_simplify_new env new' active in + let active = backward_simplify env (sign, current) active (* match new' with *) @@ -250,8 +272,6 @@ let rec given_clause env passive active = (* | _ -> active *) in - let new' = forward_simplify_new env new' active in - print_endline "\n================================================"; let _ = Printf.printf "active:\n%s\n" @@ -261,6 +281,7 @@ let rec given_clause env passive active = (string_of_equality ~env e)) active))); print_newline (); in + (* let _ = *) (* match new' with *) (* | neg, pos -> *) @@ -323,12 +344,7 @@ let main () = let term_equality = equality_of_term meta_proof goal in let meta_proof, (eq_ty, left, right), _, _ = term_equality in let active = [] in -(* let passive = *) -(* (EqualitySet.singleton term_equality, *) -(* List.fold_left *) -(* (fun res eq -> EqualitySet.add eq res) EqualitySet.empty equalities) *) -(* in *) - let passive = [term_equality], equalities in + let passive = make_passive [term_equality] equalities in Printf.printf "\ncurrent goal: %s ={%s} %s\n" (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right); Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); @@ -362,8 +378,21 @@ let main () = ;; +let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";; + let _ = - let configuration_file = "../../gTopLevel/gTopLevel.conf.xml" in - Helm_registry.load_from configuration_file + let set_ratio v = weight_age_ratio := v; weight_age_counter := v + and set_sel () = set_selection := (fun s -> EqualitySet.max_elt s) + and set_conf f = configuration_file := f + in + Arg.parse [ + "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio"; + + "-i", Arg.Unit set_sel, + "Inverse selection (select heaviest equalities before)"; + + "-c", Arg.String set_conf, "Configuration file (for the db connection)"; + ] (fun a -> ()) "Usage:" in +Helm_registry.load_from !configuration_file; main () diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 8d97e0c4b..7f0a8ba55 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -27,20 +27,21 @@ let string_of_weight (cw, mw) = Printf.sprintf "[%d; %s]" cw s -let weight_of_term term = +let weight_of_term ?(consider_metas=true) term = (* ALB: what to consider as a variable? I think "variables" in our case are Metas and maybe Rels... *) let module C = Cic in let vars_dict = Hashtbl.create 5 in let rec aux = function - | C.Meta (metano, _) -> + | C.Meta (metano, _) when consider_metas -> (try let oldw = Hashtbl.find vars_dict metano in Hashtbl.replace vars_dict metano (oldw+1) with Not_found -> Hashtbl.add vars_dict metano 1); 0 - + | C.Meta _ -> 0 (* "variables" are lighter than constants and functions...*) + | C.Var (_, ens) | C.Const (_, ens) | C.MutInd (_, _, ens) diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index 164d4f303..235085ab1 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -9,7 +9,7 @@ val print_subst: Cic.substitution -> string val string_of_weight: weight -> string -val weight_of_term: Cic.term -> weight +val weight_of_term: ?consider_metas:bool -> Cic.term -> weight val normalize_weight: int -> weight -> weight -- 2.39.2