From: Alberto Griggio Date: Tue, 7 Jun 2005 07:53:30 +0000 (+0000) Subject: *** empty log message *** X-Git-Tag: PRE_INDEX_1~63 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c76c8c83852508d69e7765dc9e929cdcf34af57d;p=helm.git *** empty log message *** --- diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index fba57a593..85668aaf9 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -75,7 +75,7 @@ $(TOPLEVELOBJS): $(LIBRARIES) $(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT) clean: - rm -f *.cm[iox] *.o gTopLevel{,.opt} regtest{,.opt} testlibrary{,.opt} + rm -f *.cm[iox] *.o saturation{,.opt} regtest{,.opt} testlibrary{,.opt} install: cp gTopLevel gTopLevel.opt $(BIN_DIR) uninstall: diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 999666bca..4d56d30e9 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -292,7 +292,31 @@ let rec restore_subst (* context *) subst = subst ;; - + +exception MatchingFailure;; + +let matching metasenv context t1 t2 ugraph = + try + let subst, metasenv, ugraph = + CicUnification.fo_unif metasenv context t1 t2 ugraph + in + let t' = CicMetaSubst.apply_subst subst t1 in + if not (meta_convertibility t1 t') then + raise MatchingFailure + else + let metas = metas_of_term t1 in + let fix_subst = function + | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas -> + (j, (c, Cic.Meta (i, lc), ty)) + | s -> s + in + let subst = List.map fix_subst subst in + subst, metasenv, ugraph + with e -> + raise MatchingFailure +;; + + let beta_expand ?(metas_ok=true) ?(match_only=false) what type_of_what where context metasenv ugraph = let module S = CicSubstitution in @@ -559,47 +583,33 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) 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 + if match_only then + matching metasenv context term (S.lift lift_amount what)ugraph + else + CicUnification.fo_unif metasenv context + (S.lift lift_amount what) term ugraph in (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *) (* (CicPp.ppterm (S.lift lift_amount what)); *) (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *) (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *) (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *) - if match_only then - let t' = CicMetaSubst.apply_subst subst' term in - if not (meta_convertibility term t') then ( -(* if print_info 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 ( - let metas = metas_of_term term in -(* let ok = ref false in *) - let fix_subst = function - | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> -(* Printf.printf "fix_subst: scambio ?%d e ?%d\n" i j; *) -(* ok := true; *) - (j, (c, C.Meta (i, lc), ty)) - | s -> s - in - let subst' = List.map fix_subst subst' in -(* if !ok then ( *) -(* Printf.printf "aaa:\nterm: %s\nt'%s\n term subst': %s\n" *) -(* (CicPp.ppterm term) *) -(* (CicPp.ppterm t') *) -(* (CicPp.ppterm (CicMetaSubst.apply_subst subst' term)) *) -(* ); *) - ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, - lifted_term) - ) -(* ((C.Rel (1 + lift_amount), restore_subst context subst', *) -(* metasenv', ugraph')::res, lifted_term) *) - else +(* if match_only then *) +(* let t' = CicMetaSubst.apply_subst subst' term in *) +(* if not (meta_convertibility term t') then ( *) +(* res, lifted_term *) +(* ) else ( *) +(* let metas = metas_of_term term in *) +(* let fix_subst = function *) +(* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *) +(* (j, (c, C.Meta (i, lc), ty)) *) +(* | s -> s *) +(* in *) +(* let subst' = List.map fix_subst subst' in *) +(* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *) +(* lifted_term) *) +(* ) *) +(* else *) ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, lifted_term) with e -> @@ -1144,3 +1154,53 @@ let demodulation newmeta env target source = *) +let subsumption env target source = + let _, (ty, tl, tr), tmetas, _ = target + and _, (ty', sl, sr), smetas, _ = source in + if ty <> ty' then + false + else + let metasenv, context, ugraph = env in + let metasenv = metasenv @ tmetas @ smetas in + let names = names_of_context context in + let samesubst subst subst' = +(* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *) +(* (print_subst subst) (print_subst subst'); *) +(* print_newline (); *) + let tbl = Hashtbl.create (List.length subst) in + List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst; + List.for_all + (fun (m, (c, t1, t2)) -> + try + let c', t1', t2' = Hashtbl.find tbl m in + if (c = c') && (t1 = t1') && (t2 = t2') then true + else false + with Not_found -> + true) + subst' + in + let subsaux left right left' right' = + try + let subst, menv, ug = matching metasenv context left left' ugraph + and subst', menv', ug' = matching metasenv context right right' ugraph + in +(* Printf.printf "left = right: %s = %s\n" *) +(* (CicPp.pp left names) (CicPp.pp right names); *) +(* Printf.printf "left' = right': %s = %s\n" *) +(* (CicPp.pp left' names) (CicPp.pp right' names); *) + samesubst subst subst' + with e -> +(* print_endline (Printexc.to_string e); *) + false + in + let res = + if subsaux tl tr sl sr then true + else subsaux tl tr sr sl + in + if res then ( + Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n" + (string_of_equality ~env target) (string_of_equality ~env source); + print_newline (); + ); + res +;; diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index bc37d1a64..fab2026ad 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -65,5 +65,4 @@ val is_identity: environment -> equality -> bool val string_of_equality: ?env:environment -> equality -> string - - +val subsumption: environment -> equality -> equality -> bool diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index dbc85261b..4c1480d10 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -131,8 +131,8 @@ let select env passive active = (others + (abs (common - card))), e1 in let _, current = EqualitySet.fold f pos_set initial in - Printf.printf "\nsymbols-based selection: %s\n\n" - (string_of_equality ~env current); +(* Printf.printf "\nsymbols-based selection: %s\n\n" *) +(* (string_of_equality ~env current); *) (Positive, current), (([], neg_set), (remove current pos_list, EqualitySet.remove current pos_set)) @@ -244,8 +244,7 @@ let contains_empty env (negative, positive) = ;; -let forward_simplify env ?(active=[]) ?passive (sign, current) = - (* first step, remove already present equalities *) +let forward_simplify env (sign, current) ?passive active = let pn, pp = match passive with | None -> [], [] @@ -254,38 +253,51 @@ let forward_simplify env ?(active=[]) ?passive (sign, current) = (List.map (fun e -> Positive, e) pp) in let all = active @ pn @ pp in - 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 all + let rec find_duplicate sign current = function + | [] -> false + | (s, eq)::tl when s = sign -> + if meta_convertibility_eq current eq then true + else find_duplicate sign current tl + | _::tl -> find_duplicate sign current tl 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, newcurrent = - demodulation !maxmeta env current equality in - maxmeta := newmeta; - if is_identity env newcurrent then - None - else if newcurrent <> current then - aux env (sign, newcurrent) active +(* let duplicate = find_duplicate sign current all 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, newcurrent = + demodulation !maxmeta env current equality in + maxmeta := newmeta; + if is_identity env newcurrent then + if sign = Negative then + Some (sign, current) else - aux env (sign, newcurrent) tl - in - aux env (sign, current) all + None + else if newcurrent <> current then + aux env (sign, newcurrent) active + else + aux env (sign, newcurrent) tl + in + let res = aux env (sign, current) all in + match res with + | None -> None + | Some (s, c) -> + if find_duplicate s c all then + None + else + let pred (sign, eq) = + if sign <> s then false + else subsumption env c eq + in + if List.exists pred all then None + else res ;; -let forward_simplify_new env ?(active=[]) ?passive (new_neg, new_pos) = +let forward_simplify_new env (new_neg, new_pos) ?passive active = let pn, pp = match passive with | None -> [], [] @@ -320,60 +332,62 @@ let forward_simplify_new env ?(active=[]) ?passive (new_neg, new_pos) = let new_pos_set = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos in - new_neg, EqualitySet.elements new_pos_set -;; - - -(* -let backward_simplify_active env (sign, current) active = - match sign with - | Negative -> active - | Positive -> - let active = - List.map - (fun (s, equality) -> - (* match s with *) - (* | Negative -> s, equality *) - (* | Positive -> *) - let newmeta, equality = - demodulation !maxmeta env equality current in - maxmeta := newmeta; - s, equality) - active - in - let active = - List.filter (fun (s, eq) -> not (is_identity env eq)) active - in - let find eq1 where = - List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where - in - List.fold_right - (fun (s, eq) res -> if find eq res then res else (s, eq)::res) - active [] + let new_pos = EqualitySet.elements new_pos_set in + let f sign' target (sign, eq) = +(* Printf.printf "f %s <%s> (%s, <%s>)\n" *) +(* (string_of_sign sign') (string_of_equality ~env target) *) +(* (string_of_sign sign) (string_of_equality ~env eq); *) + if sign <> sign' then false + else subsumption env target eq + in +(* new_neg, new_pos *) + (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, + List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) ;; -*) let backward_simplify_active env (new_neg, new_pos) active = let new_pos = List.map (fun e -> Positive, e) new_pos in - let active = + let active, newa = List.fold_right - (fun (s, equality) res -> - match forward_simplify env ~active:new_pos (s, equality) with - | None -> res - | Some e -> e::res) - active [] + (fun (s, equality) (res, newn) -> + match forward_simplify env (s, equality) new_pos with + | None when s = Negative -> + Printf.printf "\nECCO QUI: %s\n" + (string_of_equality ~env equality); + print_newline (); + res, newn + | None -> res, newn + | Some (s, e) -> + if equality = e then + (s, e)::res, newn + else + res, (s, e)::newn) + active ([], []) in let find eq1 where = List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where in - List.fold_right - (fun (s, eq) res -> - if (is_identity env eq) || (find eq res) then - res - else - (s, eq)::res) - active [] + let active, newa = + let f (s, eq) res = + if (is_identity env eq) || (find eq res) then res else (s, eq)::res + in + List.fold_right + (fun (s, eq) res -> + if (is_identity env eq) || (find eq res) then res else (s, eq)::res) + active [], + List.fold_right + (fun (s, eq) (n, p) -> + if (s <> Negative) && (is_identity env eq) then + (n, p) + else + if s = Negative then eq::n, p + else n, eq::p) + newa ([], []) + in + match newa with + | [], [] -> active, None + | _ -> active, Some newa ;; @@ -381,7 +395,7 @@ let backward_simplify_passive env (new_neg, new_pos) passive = let new_pos = List.map (fun e -> Positive, e) new_pos in let (nl, ns), (pl, ps) = passive in let f sign equality (resl, ress, newn) = - match forward_simplify env ~active:new_pos (sign, equality) with + match forward_simplify env (sign, equality) new_pos with | None -> resl, EqualitySet.remove equality ress, newn | Some (s, e) -> if equality = e then @@ -398,15 +412,15 @@ let backward_simplify_passive env (new_neg, new_pos) passive = ;; -let backward_simplify env ?(active=[]) ?passive new' = - let active = backward_simplify_active env new' active in +let backward_simplify env new' ?passive active = + let active, newa = backward_simplify_active env new' active in match passive with | None -> - active, (([], EqualitySet.empty), ([], EqualitySet.empty)), None + active, (([], EqualitySet.empty), ([], EqualitySet.empty)), newa, None | Some passive -> - let passive, new' = + let passive, newp = backward_simplify_passive env new' passive in - active, passive, new' + active, passive, newa, newp ;; @@ -419,44 +433,159 @@ let rec given_clause env passive active = let (sign, current), passive = select env passive active in (* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *) (* (string_of_sign sign) (string_of_equality ~env current); *) - match forward_simplify env (sign, current) ~active ~passive with - | None when sign = Negative -> - Printf.printf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current); - print_newline (); - let proof, _, _, _ = current in - Success (Some proof, env) + match forward_simplify env (sign, current) ~passive active with +(* | None when sign = Negative -> *) +(* Printf.printf "OK!!! %s %s" (string_of_sign sign) *) +(* (string_of_equality ~env current); *) +(* print_newline (); *) +(* 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 (); *) given_clause env passive active | Some (sign, current) -> - print_endline "\n================================================"; - Printf.printf "selected: %s %s" - (string_of_sign sign) (string_of_equality ~env current); - print_newline (); + if (sign = Negative) && (is_identity env current) then ( + Printf.printf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current); + print_newline (); + let proof, _, _, _ = current in + Success (Some proof, env) + ) else ( + print_endline "\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 res, proof = contains_empty env new' in + if res then + Success (proof, env) + else + let new' = forward_simplify_new env new' active in + let active = + match sign with + | Negative -> active + | Positive -> + let active, _, newa, _ = + backward_simplify env ([], [current]) active + in + match newa with + | None -> active + | Some (n, p) -> + let nn = List.map (fun e -> Negative, e) n + and pp = List.map (fun e -> Positive, e) p in + nn @ active @ pp + in + let _ = + Printf.printf "active:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) active))); + print_newline (); + in + let _ = + match new' with + | neg, pos -> + Printf.printf "new':\n%s\n" + (String.concat "\n" + ((List.map + (fun e -> "Negative " ^ + (string_of_equality ~env e)) neg) @ + (List.map + (fun e -> "Positive " ^ + (string_of_equality ~env e)) pos))); + print_newline (); + in + match contains_empty env new' with + | false, _ -> + let active = + match sign with + | Negative -> (sign, current)::active + | Positive -> active @ [(sign, current)] + in + let passive = add_to_passive passive new' in + let (_, ns), (_, ps) = passive in + Printf.printf "passive:\n%s\n" + (String.concat "\n" + ((List.map (fun e -> "Negative " ^ + (string_of_equality ~env e)) + (EqualitySet.elements ns)) @ + (List.map (fun e -> "Positive " ^ + (string_of_equality ~env e)) + (EqualitySet.elements ps)))); + print_newline (); + given_clause env passive active + | true, proof -> + Success (proof, env) + ) +;; - let new' = infer env sign current active in - let res, proof = contains_empty env new' in - if res then - Success (proof, env) - else - let new' = forward_simplify_new env new' ~active in - - (* let active, passive, retained = *) - (* backward_simplify env [(sign, current)] ~active ~passive *) - (* in *) +let rec given_clause_fullred env passive active = + match passive_is_empty passive with + | true -> Failure + | false -> +(* Printf.printf "before select\n"; *) + let (sign, current), passive = select env passive active in +(* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *) +(* (string_of_sign sign) (string_of_equality ~env current); *) + match forward_simplify env (sign, current) ~passive active with + | None -> + given_clause_fullred env passive active + | Some (sign, current) -> + if (sign = Negative) && (is_identity env current) then ( + Printf.printf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current); + print_newline (); + let proof, _, _, _ = current in + Success (Some proof, env) + ) else ( + print_endline "\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 active = - match sign with - | Negative -> active - | Positive -> - let active, _, _ = - backward_simplify env ([], [current]) ~active - in - active + if is_identity env current then active + else + match sign with + | Negative -> (sign, current)::active + | Positive -> active @ [(sign, current)] + in +(* let _ = *) +(* match new' with *) +(* | neg, pos -> *) +(* Printf.printf "new' before simpl:\n%s\n" *) +(* (String.concat "\n" *) +(* ((List.map *) +(* (fun e -> "Negative " ^ *) +(* (string_of_equality ~env e)) neg) @ *) +(* (List.map *) +(* (fun e -> "Positive " ^ *) +(* (string_of_equality ~env e)) pos))); *) +(* print_newline (); *) +(* in *) + let rec simplify new' active passive = + let new' = forward_simplify_new env new' ~passive active in + let active, passive, newa, retained = + backward_simplify env new' ~passive active + in + match newa, retained with + | None, None -> active, passive, new' + | Some (n, p), None + | None, Some (n, p) -> + let nn, np = new' in + simplify (nn @ n, np @ p) active passive + | Some (n, p), Some (rn, rp) -> + let nn, np = new' in + simplify (nn @ n @ rn, np @ p @ rp) active passive in + let active, passive, new' = simplify new' active passive in let _ = Printf.printf "active:\n%s\n" (String.concat "\n" @@ -480,102 +609,24 @@ let rec given_clause env passive active = in match contains_empty env new' with | false, _ -> - let active = - match sign with - | Negative -> (sign, current)::active - | Positive -> active @ [(sign, current)] - in let passive = add_to_passive passive new' in - let (_, ns), (_, ps) = passive in - Printf.printf "passive:\n%s\n" - (String.concat "\n" - ((List.map (fun e -> "Negative " ^ - (string_of_equality ~env e)) - (EqualitySet.elements ns)) @ - (List.map (fun e -> "Positive " ^ - (string_of_equality ~env e)) - (EqualitySet.elements ps)))); - print_newline (); - given_clause env passive active +(* let (_, ns), (_, ps) = passive in *) +(* Printf.printf "passive:\n%s\n" *) +(* (String.concat "\n" *) +(* ((List.map (fun e -> "Negative " ^ *) +(* (string_of_equality ~env e)) *) +(* (EqualitySet.elements ns)) @ *) +(* (List.map (fun e -> "Positive " ^ *) +(* (string_of_equality ~env e)) *) +(* (EqualitySet.elements ps)))); *) +(* print_newline (); *) + given_clause_fullred env passive active | true, proof -> Success (proof, env) + ) ;; -(* -let rec given_clause env passive active = - match passive_is_empty passive with - | true -> Failure - | false -> -(* Printf.printf "before select\n"; *) - let (sign, current), passive = select env passive active in -(* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *) -(* (string_of_sign sign) (string_of_equality ~env current); *) - print_endline "\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 rec simplify new' active passive = - let new' = forward_simplify_new env new' ~active ~passive in - let active, passive, retained = - backward_simplify env new' ~active ~passive - in - match retained with - | None -> active, passive, new' - | Some (rn, rp) -> - let nn, np = new' in - simplify (nn @ rn, np @ rp) active passive - in - let active, passive, new' = simplify new' active passive in - let _ = - Printf.printf "active:\n%s\n" - (String.concat "\n" - ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) active))); - print_newline (); - in - let _ = - match new' with - | neg, pos -> - Printf.printf "new':\n%s\n" - (String.concat "\n" - ((List.map - (fun e -> "Negative " ^ - (string_of_equality ~env e)) neg) @ - (List.map - (fun e -> "Positive " ^ - (string_of_equality ~env e)) pos))); - print_newline (); - in - match contains_empty env new' with - | false, _ -> - let active = - match sign with - | Negative -> (sign, current)::active - | Positive -> active @ [(sign, current)] - in - let passive = add_to_passive passive new' in - let (_, ns), (_, ps) = passive in - Printf.printf "passive:\n%s\n" - (String.concat "\n" - ((List.map (fun e -> "Negative " ^ - (string_of_equality ~env e)) - (EqualitySet.elements ns)) @ - (List.map (fun e -> "Positive " ^ - (string_of_equality ~env e)) - (EqualitySet.elements ps)))); - print_newline (); - given_clause env passive active - | true, proof -> - Success (proof, env) -;; -*) - - let get_from_user () = let dbd = Mysql.quick_connect ~host:"localhost" ~user:"helm" ~database:"mowgli" () in @@ -592,6 +643,9 @@ let get_from_user () = ;; +let given_clause_ref = ref given_clause;; + + let main () = let module C = Cic in let module T = CicTypeChecker in @@ -630,7 +684,7 @@ let main () = print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in print_endline "GO!"; - let res = given_clause env passive active in + let res = !given_clause_ref env passive active in let finish = Unix.gettimeofday () in match res with | Failure -> @@ -653,8 +707,11 @@ let _ = and set_conf f = configuration_file := f and set_lpo () = Utils.compare_terms := lpo and set_kbo () = Utils.compare_terms := nonrec_kbo + and set_fullred () = given_clause_ref := given_clause_fullred in Arg.parse [ + "-f", Arg.Unit set_fullred, "Use full-reduction strategy"; + "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)"; "-s", Arg.Int set_sel,