From 975da98810a335a759a3b5e5f96b1beb96c932d2 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Thu, 19 May 2005 13:11:06 +0000 Subject: [PATCH] various optimizations (to paramodulation and passive clause selection) --- helm/ocaml/paramodulation/inference.ml | 500 ++++++++++++++++++------ helm/ocaml/paramodulation/inference.mli | 3 + helm/ocaml/paramodulation/saturation.ml | 421 ++++++++++++++++---- 3 files changed, 741 insertions(+), 183 deletions(-) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 987c17cc8..999666bca 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1,26 +1,87 @@ open Utils;; +let string_of_equality ?env = + match env with + | None -> ( + function + | _, (ty, left, right), _, _ -> + Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty) + (CicPp.ppterm left) (CicPp.ppterm right) + ) + | Some (_, context, _) -> ( + let names = names_of_context context in + function + | _, (ty, left, right), _, _ -> + Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names) + (CicPp.pp left names) (CicPp.pp right names) + ) +;; + + +let rec metas_of_term = function + | Cic.Meta (i, c) -> [i] + | Cic.Var (_, ens) + | Cic.Const (_, ens) + | Cic.MutInd (_, _, ens) + | Cic.MutConstruct (_, _, _, ens) -> + List.flatten (List.map (fun (u, t) -> metas_of_term t) ens) + | Cic.Cast (s, t) + | Cic.Prod (_, s, t) + | Cic.Lambda (_, s, t) + | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t) + | Cic.Appl l -> List.flatten (List.map metas_of_term l) + | Cic.MutCase (uri, i, s, t, l) -> + (metas_of_term s) @ (metas_of_term t) @ + (List.flatten (List.map metas_of_term l)) + | Cic.Fix (i, il) -> + List.flatten + (List.map (fun (s, i, t1, t2) -> + (metas_of_term t1) @ (metas_of_term t2)) il) + | Cic.CoFix (i, il) -> + List.flatten + (List.map (fun (s, t1, t2) -> + (metas_of_term t1) @ (metas_of_term t2)) il) + | _ -> [] +;; + + exception NotMetaConvertible;; let meta_convertibility_aux table t1 t2 = let module C = Cic in - let rec aux table t1 t2 = + let print_table t = + String.concat ", " + (List.map + (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t) + in + let rec aux ((table_l, table_r) as table) t1 t2 = +(* Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *) +(* (CicPp.ppterm t1) (CicPp.ppterm t2) *) +(* (print_table table_l) (print_table table_r); *) match t1, t2 with - | t1, t2 when t1 = t2 -> table | C.Meta (m1, tl1), C.Meta (m2, tl2) -> - 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 + let m1_binding, table_l = + try List.assoc m1 table_l, table_l + with Not_found -> m2, (m1, m2)::table_l + and m2_binding, table_r = + try List.assoc m2 table_r, table_r + with Not_found -> m1, (m2, m1)::table_r in - if m1_binding <> m2 || m2_binding <> m1 then +(* 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 *) +(* Printf.printf "table_l: %s\ntable_r: %s\n\n" *) +(* (print_table table_l) (print_table table_r); *) + if (m1_binding <> m2) || (m2_binding <> m1) then raise NotMetaConvertible else ( try @@ -30,7 +91,7 @@ let meta_convertibility_aux table t1 t2 = | None, Some _ | Some _, None -> raise NotMetaConvertible | None, None -> res | Some t1, Some t2 -> (aux res t1 t2)) - table tl1 tl2 + (table_l, table_r) tl1 tl2 with Invalid_argument _ -> raise NotMetaConvertible ) @@ -77,6 +138,7 @@ let meta_convertibility_aux table t1 t2 = table il1 il2 with Invalid_argument _ -> raise NotMetaConvertible ) + | t1, t2 when t1 = t2 -> table | _, _ -> raise NotMetaConvertible and aux_ens table ens1 ens2 = @@ -102,28 +164,19 @@ let meta_convertibility_eq eq1 eq2 = and _, (ty', left', right'), _, _ = eq2 in if ty <> ty' then false + else if (left = left') && (right = right') then + true + else if (left = right') && (right = left') then + true else - let print_table t w = - Printf.printf "table %s is:\n" w; - List.iter - (fun (k, v) -> Printf.printf "?%d: ?%d\n" k v) - t; - print_newline (); - in try - let table = meta_convertibility_aux [] left left' in + let table = meta_convertibility_aux ([], []) left left' in let _ = meta_convertibility_aux table right right' 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 -> try - let table = meta_convertibility_aux [] left right' in + 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 @@ -131,18 +184,122 @@ let meta_convertibility_eq eq1 eq2 = let meta_convertibility t1 t2 = - try - let _ = meta_convertibility_aux [] t1 t2 in + let f t = + String.concat ", " + (List.map + (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t) + in + if t1 = t2 then true - with NotMetaConvertible -> - false + else + try + let l, r = meta_convertibility_aux ([], []) t1 t2 in + (* Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *) + true + with NotMetaConvertible -> + false ;; +let replace_metas (* context *) term = + let module C = Cic in + let rec aux = function + | C.Meta (i, c) -> +(* let irl = *) +(* CicMkImplicit.identity_relocation_list_for_metavariable context *) +(* in *) +(* if c = irl then *) +(* C.Implicit (Some (`MetaIndex i)) *) +(* else ( *) +(* Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *) +(* (String.concat "\n" *) +(* (List.map *) +(* (function None -> "" | Some t -> CicPp.ppterm t) c)); *) +(* C.Meta (i, c) *) +(* ) *) + C.Implicit (Some (`MetaInfo (i, c))) + | C.Var (u, ens) -> C.Var (u, aux_ens ens) + | C.Const (u, ens) -> C.Const (u, aux_ens ens) + | C.Cast (s, t) -> C.Cast (aux s, aux t) + | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t) + | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t) + | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t) + | C.Appl l -> C.Appl (List.map aux l) + | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens) + | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens) + | C.MutCase (uri, i, s, t, l) -> + C.MutCase (uri, i, aux s, aux t, List.map aux l) + | C.Fix (i, il) -> + let il' = + List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in + C.Fix (i, il') + | C.CoFix (i, il) -> + let il' = + List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in + C.CoFix (i, il') + | t -> t + and aux_ens ens = + List.map (fun (u, t) -> (u, aux t)) ens + in + aux term +;; + + +let restore_metas (* context *) term = + let module C = Cic in + let rec aux = function + | C.Implicit (Some (`MetaInfo (i, c))) -> +(* let c = *) +(* CicMkImplicit.identity_relocation_list_for_metavariable context *) +(* in *) +(* C.Meta (i, c) *) +(* let local_context:(C.term option) list = *) +(* Marshal.from_string mc 0 *) +(* in *) +(* C.Meta (i, local_context) *) + C.Meta (i, c) + | C.Var (u, ens) -> C.Var (u, aux_ens ens) + | C.Const (u, ens) -> C.Const (u, aux_ens ens) + | C.Cast (s, t) -> C.Cast (aux s, aux t) + | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t) + | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t) + | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t) + | C.Appl l -> C.Appl (List.map aux l) + | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens) + | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens) + | C.MutCase (uri, i, s, t, l) -> + C.MutCase (uri, i, aux s, aux t, List.map aux l) + | C.Fix (i, il) -> + let il' = + List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in + C.Fix (i, il') + | C.CoFix (i, il) -> + let il' = + List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in + C.CoFix (i, il') + | t -> t + and aux_ens ens = + List.map (fun (u, t) -> (u, aux t)) ens + in + aux term +;; + + +let rec restore_subst (* context *) subst = + List.map + (fun (i, (c, t, ty)) -> + i, (c, restore_metas (* context *) t, ty)) + subst +;; + + 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 print_info = false in + (* let _ = *) (* let names = names_of_context context in *) (* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *) @@ -394,6 +551,10 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) | C.Meta _ when (not metas_ok) -> res, lifted_term | _ -> +(* let term' = *) +(* if match_only then replace_metas context term *) +(* else term *) +(* in *) try let subst', metasenv', ugraph' = (* Printf.printf "provo a unificare %s e %s\n" *) @@ -409,19 +570,42 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) if match_only then 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); *) +(* 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 + ) 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 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, lifted_term) with e -> -(* print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e)); *) + if print_info then ( + print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e)); + ); res, lifted_term in (* Printf.printf "exit aux\n"; *) @@ -455,14 +639,30 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) ) exp_named_subst ([], []) in - let expansions, _ = aux 0 where context metasenv [] ugraph in - List.map - (fun (term, subst, metasenv, ugraph) -> - let term' = C.Lambda (C.Anonymous, type_of_what, term) in -(* Printf.printf "term is: %s\nsubst is:\n%s\n\n" *) -(* (CicPp.ppterm term') (print_subst subst); *) - (term', subst, metasenv, ugraph)) - expansions + let expansions, _ = +(* let where = *) +(* if match_only then replace_metas (\* context *\) where *) +(* else where *) +(* in *) + if print_info then ( + Printf.printf "searching %s inside %s\n" + (CicPp.ppterm what) (CicPp.ppterm where); + ); + aux 0 where context metasenv [] ugraph + in + let mapfun = +(* if match_only then *) +(* (fun (term, subst, metasenv, ugraph) -> *) +(* let term' = *) +(* C.Lambda (C.Anonymous, type_of_what, restore_metas term) *) +(* and subst = restore_subst subst in *) +(* (term', subst, metasenv, ugraph)) *) +(* else *) + (fun (term, subst, metasenv, ugraph) -> + let term' = C.Lambda (C.Anonymous, type_of_what, term) in + (term', subst, metasenv, ugraph)) + in + List.map mapfun expansions ;; @@ -557,8 +757,17 @@ let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) = (i, context, term)::menv) menv [] in + let ty = repl ty + and left = repl left + and right = repl right in + let metas = (metas_of_term left) @ (metas_of_term right) in + let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' + and newargs = + List.filter + (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs + in (newmeta + (List.length newargs) + 1, - (repl proof, (repl ty, repl left, repl right), menv', newargs)) + (repl proof, (ty, left, right), menv', newargs)) ;; @@ -586,14 +795,13 @@ let superposition_left (metasenv, context, ugraph) target source = let proof, (eq_ty, left, right), _, _ = target in 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 compare_terms = !Utils.compare_terms in if eq_ty <> ty then [] else let where, is_left = - match nonrec_kbo left right with + match compare_terms left right with | Lt -> right, false | Gt -> left, true | _ -> ( @@ -604,16 +812,24 @@ let superposition_left (metasenv, context, ugraph) target source = ) 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) + let result = compare_terms t1 t2 in + let res1, res2 = + match result with + | Gt -> (beta_expand t1 ty where context metasenv' ugraph), [] + | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph) + | _ -> + let res1 = + List.filter + (fun (t, s, m, ug) -> + compare_terms (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) -> + compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt) + (beta_expand t2 ty where context metasenv' ugraph) + in + res1, res2 in (* let what, other = *) (* if is_left then left, right *) @@ -660,8 +876,7 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = let eqp', (ty', t1, t2), newm', args' = source in let maxmeta = ref newmeta in - (* TODO check if ty and ty' are equal... *) - (* assert (eq_ty = ty'); *) + let compare_terms = !Utils.compare_terms in if eq_ty <> ty' then newmeta, [] @@ -676,30 +891,53 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = (* 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 + let cmp1 = compare_terms (subst what) (subst other) in + let cmp2 = compare_terms (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) + let cmp1 = compare_terms left right + and cmp2 = compare_terms t1 t2 in + let res1, res2, res3, res4 = + let res l r s t = + List.filter + (condition l r s t) + (beta_expand s eq_ty l context metasenv' ugraph) + in + match cmp1, cmp2 with + | Gt, Gt -> + (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], [] + | Gt, Lt -> + [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], [] + | Lt, Gt -> + [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), [] + | Lt, Lt -> + [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph) + | Gt, _ -> + let res1 = res left right t1 t2 + and res2 = res left right t2 t1 in + res1, res2, [], [] + | Lt, _ -> + let res3 = res right left t1 t2 + and res4 = res right left t2 t1 in + [], [], res3, res4 + | _, Gt -> + let res1 = res left right t1 t2 + and res3 = res right left t1 t2 in + res1, [], res3, [] + | _, Lt -> + let res2 = res left right t2 t1 + and res4 = res right left t2 t1 in + [], res2, [], res4 + | _, _ -> + let res1 = res left right t1 t2 + and res2 = res left right t2 t1 + and res3 = res right left t1 t2 + and res4 = res right left t2 t1 in + res1, res2, res3, res4 in let newmetas = newmetas @ newm' in let newargs = args @ args' in @@ -770,16 +1008,33 @@ let demodulation newmeta (metasenv, context, ugraph) target source = let proof, (eq_ty, left, right), metas, args = target and proof', (ty, t1, t2), metas', args' = source in + + let compare_terms = !Utils.compare_terms in + if eq_ty <> ty then newmeta, target else - let get_params step = - match step with - | 3 -> true, t1, t2, HL.Logic.eq_ind_URI - | 2 -> false, t1, t2, HL.Logic.eq_ind_URI - | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI - | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI - | _ -> assert false + let first_step, get_params = + match compare_terms t1 t2 with + | Gt -> 1, (function + | 1 -> true, t1, t2, HL.Logic.eq_ind_URI + | 0 -> false, t1, t2, HL.Logic.eq_ind_URI + | _ -> assert false) + | Lt -> 1, (function + | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI + | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI + | _ -> assert false) + | _ -> + let first_step = 3 in + let get_params step = + match step with + | 3 -> true, t1, t2, HL.Logic.eq_ind_URI + | 2 -> false, t1, t2, HL.Logic.eq_ind_URI + | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI + | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI + | _ -> assert false + in + first_step, get_params in let rec demodulate newmeta step metasenv target = let proof, (eq_ty, left, right), metas, args = target in @@ -795,18 +1050,28 @@ let demodulation newmeta (metasenv, context, ugraph) target source = (* print_newline (); *) let ok (t, s, m, ug) = - nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt + compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt in let res = let r = (beta_expand ~metas_ok:false ~match_only:true what ty (if is_left then left else right) context (metasenv @ metas) ugraph) 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 (); *) +(* let m' = metas_of_term what *) +(* and m'' = metas_of_term (if is_left then left else right) in *) +(* if (List.mem 527 m'') && (List.mem 6 m') then ( *) +(* Printf.printf *) +(* "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" step; *) +(* print_newline (); *) +(* 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 @@ -817,7 +1082,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source = let newterm, newproof = match t with | C.Lambda (nn, ty, bo) -> - let bo' = M.apply_subst s (S.subst other bo) in +(* let bo' = M.apply_subst s (S.subst other bo) in *) + let bo' = S.subst (M.apply_subst s other) bo in let bo'' = C.Appl ( [C.MutInd (HL.Logic.eq_URI, 0, []); @@ -826,7 +1092,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source = else [S.lift 1 left; bo']) in let t' = C.Lambda (nn, ty, bo'') in - M.apply_subst s (S.subst other bo), +(* M.apply_subst s (S.subst other bo), *) + bo', M.apply_subst s (C.Appl [C.Const (eq_URI, []); ty; what; t'; proof; other; proof']) @@ -834,24 +1101,39 @@ let demodulation newmeta (metasenv, context, ugraph) target source = in let newmeta, newtarget = let left, right = - if is_left then (newterm, M.apply_subst s right) - else (M.apply_subst s left, newterm) in - let newmetasenv = metasenv @ metas in - let newargs = args @ args' in - fix_metas newmeta - (newproof, (eq_ty, left, right), newmetasenv, newargs) +(* if is_left then (newterm, M.apply_subst s right) *) +(* else (M.apply_subst s left, newterm) in *) + if is_left then newterm, right + else left, newterm + in +(* let newmetasenv = metasenv @ metas in *) +(* let newargs = args @ args' in *) +(* fix_metas newmeta *) +(* (newproof, (eq_ty, left, right), newmetasenv, newargs) *) + let m = (metas_of_term left) @ (metas_of_term right) in + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas + and newargs = + List.filter + (function C.Meta (i, _) -> List.mem i m | _ -> assert false) + args + in + 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 (); +(* Printf.printf *) +(* "demodulate, newtarget: %s\ntarget was: %s\n" *) +(* (string_of_equality ~env newtarget) *) +(* (string_of_equality ~env target); *) +(* (\* let _, _, newm, newa = newtarget in *\) *) +(* (\* Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *) +(* (\* (print_metasenv newm) *\) *) +(* (\* (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *) +(* print_newline (); *) if is_identity env newtarget then newmeta, newtarget else - demodulate newmeta step metasenv newtarget + demodulate newmeta first_step metasenv newtarget in - demodulate newmeta 3 (metasenv @ metas') target + demodulate newmeta first_step (metasenv @ metas') target ;; diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 4e1fe2c0a..bc37d1a64 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -63,4 +63,7 @@ val meta_convertibility_eq: equality -> equality -> bool val is_identity: environment -> equality -> bool +val string_of_equality: ?env:environment -> equality -> string + + diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index a0148fb35..dbc85261b 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -15,6 +15,32 @@ let string_of_sign = function ;; +(* +let symbols_of_equality (_, (_, left, right), _, _) = + TermSet.union (symbols_of_term left) (symbols_of_term right) +;; +*) + +let symbols_of_equality ((_, (_, left, right), _, _) as equality) = + let m1 = symbols_of_term left in + let m = + TermMap.fold + (fun k v res -> + try + let c = TermMap.find k res in + TermMap.add k (c+v) res + with Not_found -> + TermMap.add k v res) + (symbols_of_term right) m1 + in +(* Printf.printf "symbols_of_equality %s:\n" *) +(* (string_of_equality equality); *) +(* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *) +(* print_newline (); *) + m +;; + + module OrderedEquality = struct type t = Inference.equality @@ -39,10 +65,15 @@ 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 symbols_ratio = ref 0;; +let symbols_counter = ref 0;; + -let select env passive = +let select env passive active = let (neg_list, neg_set), (pos_list, pos_set) = passive in + let remove eq l = + List.filter (fun e -> not (e = eq)) l + in if !weight_age_ratio > 0 then weight_age_counter := !weight_age_counter - 1; match !weight_age_counter with @@ -55,19 +86,76 @@ let select env passive = (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set)) | _, _ -> assert false ) - | _ -> - let remove eq l = - List.filter (fun e -> not (e = eq)) l + | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> ( + symbols_counter := !symbols_counter - 1; + let cardinality map = + TermMap.fold (fun k v res -> res + v) map 0 in + match active with + | (Negative, e)::_ -> + let symbols = symbols_of_equality e in + let card = cardinality symbols in + let f equality (i, e) = + let common, others = + TermMap.fold + (fun k v (r1, r2) -> + if TermMap.mem k symbols then + let c = TermMap.find k symbols in + let c1 = abs (c - v) in + let c2 = v - c1 in + r1 + c2, r2 + c1 + else + r1, r2 + v) + (symbols_of_equality equality) (0, 0) + in +(* Printf.printf "equality: %s, common: %d, others: %d\n" *) +(* (string_of_equality ~env equality) common others; *) + let c = others + (abs (common - card)) in + if c < i then (c, equality) + else (i, e) + in + let e1 = EqualitySet.min_elt pos_set in + let initial = + let common, others = + TermMap.fold + (fun k v (r1, r2) -> + if TermMap.mem k symbols then + let c = TermMap.find k symbols in + let c1 = abs (c - v) in + let c2 = v - (abs (c - v)) in + r1 + c1, r2 + c2 + else + r1, r2 + v) + (symbols_of_equality e1) (0, 0) + in + (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); + (Positive, current), + (([], neg_set), + (remove current pos_list, EqualitySet.remove current pos_set)) + | _ -> + let current = EqualitySet.min_elt pos_set in + let passive = + (neg_list, neg_set), + (remove current pos_list, EqualitySet.remove current pos_set) + in + (Positive, current), passive + ) + | _ -> + symbols_counter := !symbols_ratio; + let set_selection set = EqualitySet.min_elt set in if EqualitySet.is_empty neg_set then - let current = !set_selection pos_set in + 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 current = set_selection neg_set in let passive = (remove current neg_list, EqualitySet.remove current neg_set), (pos_list, pos_set) @@ -156,8 +244,16 @@ let contains_empty env (negative, positive) = ;; -let forward_simplify env (sign, current) active = +let forward_simplify env ?(active=[]) ?passive (sign, current) = (* first step, remove already present equalities *) + let pn, pp = + match passive with + | None -> [], [] + | Some ((pn, _), (pp, _)) -> + (List.map (fun e -> Negative, e) pn), + (List.map (fun e -> Positive, e) pp) + in + let all = active @ pn @ pp in let duplicate = let rec aux = function | [] -> false @@ -166,7 +262,7 @@ let forward_simplify env (sign, current) active = else aux tl | _::tl -> aux tl in - aux active + aux all in if duplicate then None @@ -175,40 +271,61 @@ let forward_simplify env (sign, current) active = | [] -> Some (sign, current) | (Negative, _)::tl -> aux env (sign, current) tl | (Positive, equality)::tl -> - let newmeta, current = + let newmeta, newcurrent = demodulation !maxmeta env current equality in maxmeta := newmeta; - if is_identity env current then + if is_identity env newcurrent then None + else if newcurrent <> current then + aux env (sign, newcurrent) active else - aux env (sign, current) tl + aux env (sign, newcurrent) tl in - aux env (sign, current) active + aux env (sign, current) all ;; -let forward_simplify_new env (new_neg, new_pos) active = +let forward_simplify_new env ?(active=[]) ?passive (new_neg, new_pos) = + let pn, pp = + match passive with + | None -> [], [] + | Some ((pn, _), (pp, _)) -> + (List.map (fun e -> Negative, e) pn), + (List.map (fun e -> Positive, e) pp) + in + let all = active @ pn @ pp in let remove_identities equalities = let ok eq = not (is_identity env eq) in List.filter ok equalities in - let rec simpl active target = - match active with + let rec simpl all' target = + match all' with | [] -> target | (Negative, _)::tl -> simpl tl target | (Positive, source)::tl -> - let newmeta, target = demodulation !maxmeta env target source in + let newmeta, newtarget = demodulation !maxmeta env target source in maxmeta := newmeta; - if is_identity env target then target - else simpl tl target + if is_identity env newtarget then newtarget + else if newtarget <> target then ( +(* Printf.printf "OK:\n%s\n%s\n" *) +(* (string_of_equality ~env target) *) +(* (string_of_equality ~env newtarget); *) +(* print_newline (); *) + simpl all newtarget + ) + else simpl tl newtarget + in + let new_neg = List.map (simpl all) new_neg + and new_pos = remove_identities (List.map (simpl all) new_pos) in + let new_pos_set = + List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos in - let new_neg = List.map (simpl active) new_neg - and new_pos = List.map (simpl active) new_pos in - new_neg, remove_identities new_pos + new_neg, EqualitySet.elements new_pos_set ;; -let backward_simplify env (sign, current) active = +(* +let backward_simplify_active env (sign, current) active = match sign with | Negative -> active | Positive -> @@ -234,17 +351,75 @@ let backward_simplify env (sign, current) active = (fun (s, eq) res -> if find eq res then res else (s, eq)::res) active [] ;; +*) + + +let backward_simplify_active env (new_neg, new_pos) active = + let new_pos = List.map (fun e -> Positive, e) new_pos in + let active = + List.fold_right + (fun (s, equality) res -> + match forward_simplify env ~active:new_pos (s, equality) with + | None -> res + | Some e -> e::res) + 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 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 + | None -> resl, EqualitySet.remove equality ress, newn + | Some (s, e) -> + if equality = e then + equality::resl, ress, newn + else + let ress = EqualitySet.remove equality ress in + resl, ress, e::newn + in + let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, []) + and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in + match newn, newp with + | [], [] -> ((nl, ns), (pl, ps)), None + | _, _ -> ((nl, ns), (pl, ps)), Some (newn, newp) +;; + + +let backward_simplify env ?(active=[]) ?passive new' = + let active = backward_simplify_active env new' active in + match passive with + | None -> + active, (([], EqualitySet.empty), ([], EqualitySet.empty)), None + | Some passive -> + let passive, new' = + backward_simplify_passive env new' passive in + active, passive, new' +;; + 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 in + 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 with + 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); @@ -257,56 +432,148 @@ let rec given_clause env passive active = (* print_newline (); *) given_clause env passive active | Some (sign, current) -> -(* Printf.printf "selected: %s %s" *) -(* (string_of_sign sign) (string_of_equality ~env current); *) -(* print_newline (); *) + 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 new' = forward_simplify_new env new' active in - - let active = - backward_simplify env (sign, current) active -(* match new' with *) -(* | [], [] -> backward_simplify env (sign, current) active *) -(* | _ -> 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 active = + match sign with + | Negative -> active + | Positive -> + let active, _, _ = + backward_simplify env ([], [current]) ~active + in + active + 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) +;; - print_endline "\n================================================"; - let _ = - Printf.printf "active:\n%s\n" + +(* +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 (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) active))); + (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 _ = *) -(* 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 - given_clause env passive active - | true, proof -> - Success (proof, env) + 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 () = @@ -354,17 +621,17 @@ let main () = (function (_, (ty, t1, t2), _, _) -> let w1 = weight_of_term t1 in let w2 = weight_of_term t2 in - let res = nonrec_kbo t1 t2 in + let res = !compare_terms t1 t2 in Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty) (PP.ppterm t1) (string_of_weight w1) (string_of_comparison res) (PP.ppterm t2) (string_of_weight w2)) equalities; print_endline "--------------------------------------------------"; - let start = Sys.time () in + let start = Unix.gettimeofday () in print_endline "GO!"; let res = given_clause env passive active in - let finish = Sys.time () in + let finish = Unix.gettimeofday () in match res with | Failure -> Printf.printf "NO proof found! :-(\n\n" @@ -381,17 +648,23 @@ let main () = let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";; let _ = - let set_ratio v = weight_age_ratio := v; weight_age_counter := v - and set_sel () = set_selection := (fun s -> EqualitySet.max_elt s) + let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1) + and set_sel v = symbols_ratio := v; symbols_counter := v; and set_conf f = configuration_file := f + and set_lpo () = Utils.compare_terms := lpo + and set_kbo () = Utils.compare_terms := nonrec_kbo in Arg.parse [ - "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio"; + "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)"; - "-i", Arg.Unit set_sel, - "Inverse selection (select heaviest equalities before)"; + "-s", Arg.Int set_sel, + "symbols-based selection ratio (relative to the weight ratio)"; "-c", Arg.String set_conf, "Configuration file (for the db connection)"; + + "-lpo", Arg.Unit set_lpo, "Use lpo term ordering"; + + "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)"; ] (fun a -> ()) "Usage:" in Helm_registry.load_from !configuration_file; -- 2.39.2