From 2443423198327d5c301bba64d370458a04ae5560 Mon Sep 17 00:00:00 2001 From: Visa Date: Wed, 20 Mar 2024 20:17:16 +0100 Subject: [PATCH] Add variable dependencies to term while propagating to substitution to block multishift degenerating simplifications. --- src/prover_phases/RecurrencePolynomial.ml | 18 ++- src/prover_phases/summation_equality.ml | 127 +++++++++++++++++----- 2 files changed, 114 insertions(+), 31 deletions(-) diff --git a/src/prover_phases/RecurrencePolynomial.ml b/src/prover_phases/RecurrencePolynomial.ml index c77ddea36..cc02f5289 100644 --- a/src/prover_phases/RecurrencePolynomial.ml +++ b/src/prover_phases/RecurrencePolynomial.ml @@ -114,12 +114,10 @@ let ( *.) c m = Z.(if equal c zero then [C zero] else match m with let ( *:)c = map(( *.)c) let const_op_poly n = Z.(if equal n zero then [] else if equal n one then [[]] else [[C n]]) let const_eq_poly n = Z.(if equal n zero then [] else if equal n one then [[A I]] else [[C n; A I]]) -(* Other safe constructors except that one for X comes after ordering and general compositions after arithmetic. *) +(* Other safe constructors, except that one for X comes after ordering and general compositions after arithmetic, and A-T-constructor comes after variable and embedding accessors. *) let var_poly i = [A(V i)] let shift i = O[i,[var_poly i; [A I]]] let mul_var i = X(var_poly i) -(* Embed term into polynomial argument. See also poly_of_term to reverse embedding of polynomial in a term. *) -let of_term~vars t = [[A(T(t, sort_uniq~cmp:(-) vars)) |@ (match !debug_poly_of_term t with None->true|Some p-> !debug_free_variables p = vars)]] (* Distinguishes standard shift indeterminates from general substitutions. *) let is1shift = function O[i,[[A(V j)];[A I]]] -> i=j | _ -> false @@ -690,6 +688,13 @@ let isMatrix1 i = Array.for_all((=)[||])i let (@.) m (i,j) = if i >= Array.length m or m.(i)=[||] then if i=j then 1 else 0 else try m.(i).(j) with Invalid_argument(*"index out of bounds"*)_ -> 0 + +(* Basic A-T-constructor: embed term into polynomial argument. See also poly_of_term to reverse embedding of polynomial in a term. The desire to compute default for vars forces this to appear late in this file. *) +let of_term ?(vars=[-1]) t = [[A(T(t, sort_uniq~cmp:(-) ( + if vars=[-1] then match poly_of_term t with + | None -> failwith("of_term: missing ~vars for non-polynomial-embedding term "^ Term.to_string t) + | Some p -> free_variables' p + else vars)))]] (* The input function produces polynomials, and its mapped version is linear. *) let map_monomials f = fold_left (++) _0 % map f @@ -701,6 +706,13 @@ let map_outer_indeterminates f = map_monomials(let rec loop_f m = match m with | [x] -> snd(f m x) | x::n -> match f m x with `End,p -> p | `Go,p -> p >< loop_f n in loop_f) +(* Map by given f monomials of the form n·m to n·f(m), where m is maximal s.t. f m is not None, or to n·m itself otherwise. *) +let map_submonomials f = map_monomials( + let rec search_sub m = match f m, m with + | Some fm, _ -> fm + | _, [] -> [[]] (* default action: id *) + | _, x::n -> [[x]] >< search_sub n + in search_sub) (* Replace every term that embeds some polynomial p by p if act_on p. *) let unembed act_on = map_indeterminates(function A(T(t,_)) as x -> ( diff --git a/src/prover_phases/summation_equality.ml b/src/prover_phases/summation_equality.ml index 10a897b1b..b042ad2a2 100755 --- a/src/prover_phases/summation_equality.ml +++ b/src/prover_phases/summation_equality.ml @@ -22,7 +22,8 @@ open CCList open CCFun open Type open Term -open Stdlib +open Stdlib +module R = RecurrencePolynomial module B = Builtin module HS = Hashtbl (* H̲ashtable for S̲tructural equality *) module HT = Hashtbl.Make(struct @@ -36,8 +37,8 @@ module HV = Hashtbl.Make(struct let hash = HVar.hash end) -let (=) = RecurrencePolynomial.(=) -let todo = RecurrencePolynomial.todo +let (=) = R.(=) +let todo = R.todo let (~=) x _ = x let (@@) = CCPair.map_same let (%%>) = compose_binop @@ -59,7 +60,7 @@ let lex_array c = to_list %%> lex_list c let sum_list = fold_left (+) 0 let sum_array = Array.fold_left (+) 0 -let index_of = RecurrencePolynomial.index_of +let index_of = R.index_of (* Search hash table by value instead of by key. The equality relation of keys does not matter. *) let search_hash ?(eq=(=)) table value = HS.fold (fun k v found -> if found=None & eq value v then Some k else found) table None @@ -176,7 +177,6 @@ let add_simplify_in_context module MakeSumSolver(MainEnv: Env.S) = struct module C = MainEnv.C -module R = RecurrencePolynomial (* In general parent clauses of an inference also track applied substitutions but with polynomials these substitutions are almost always identities. *) let parents_as_such = map(fun p -> C.proof_parent_subst (Subst.Renaming.create()) (p,0) Subst.empty) @@ -315,7 +315,7 @@ and propagate_oper_affine p's_on_f's = |> map(fun a -> get_or~default:a R.(poly_of_term(term_of_arg a))) |> flat_map propagate_recurrences_to |> Iter.of_list - |> Iter.cons(definitional_poly_clause R.(of_term~vars:(free_variables' p's_on_f's) result -- pf_sum)) + |> Iter.cons(definitional_poly_clause R.(of_term result -- pf_sum)) |> saturate_with_order R.(elim_oper_args((result,1) :: map(fun f -> f,2) (terms_in pf_sum))) |> filter_recurrences_of[p's_on_f's] @@ -343,9 +343,9 @@ and propagate_sum i f = |`O[u, R.[[A(V v)];[A I]]] when v=u -> [] | _ -> [1] in - let sumf = R.(let _,sumf,_ = poly_as_lit_term_id([[S i]]>< of_term~vars:(free_variables' f) f_term) -- sumf) in + let embed_sumf_rewriter = definitional_poly_clause R.(([[S i]]>< of_term f_term) -- sumf) in Iter.of_list(propagate_recurrences_to f) |> saturate_with_order(R.elim_indeterminate' sum_blocker) |> Iter.map(map_poly_in_clause R.((><)[[S i]])) @@ -364,9 +364,13 @@ and propagate_subst s f = (* 3. saturate *) (* 4. replace each compound shift by a 1-shift, and substitute multipliers *) let _,f_term,_ = R.poly_as_lit_term_id f in - let _,sf_term,_ = R.(poly_as_lit_term_id([o s]> Iter.empty @@ -388,8 +392,10 @@ and propagate_subst s f = ) in (* We must eliminate all domain shifts except ones skipped above: dom\( rangeO s \ {j | ∃ ss_j} ) *) let elimIndices = Int_set.(diff dom (diff (R.rangeO s) (of_list(List.map(snd%fst) multishifts_and_equations)))) in - (* * * * Clause prosessing chain: to f's recurrences, add 𝕊=∏S, eliminate S, push ∘s i.e. map 𝕊ⱼ↦Sⱼ, and filter *) - Iter.of_list(propagate_recurrences_to f) + (* * * * Clause prosessing chain: turn recurrences of f to ones of “s'f”, add 𝕊=∏S, eliminate S, push ∘s i.e. map 𝕊ⱼ↦Sⱼ, and filter *) + propagate_recurrences_to f + |> map(map_poly_in_clause R.(map_submonomials(fun n -> CCOpt.if_~=(poly_eq f [n]) s'f))) + |> Iter.of_list (* Above is undone via s'f_term ↦ sf_term at substitution push. *) |> Iter.append(Iter.of_list(map (definitional_poly_clause % snd) multishifts_and_equations)) |> saturate_with_order(fun m' -> function |`O[i,R.[[A(V j)];[A I]]] when i=j & Int_set.mem i elimIndices -> @@ -400,10 +406,9 @@ and propagate_subst s f = |_->false) |_->false) then [] else [1] | _ -> []) - |>(|<)"kylläinen" |> Iter.filter_map(fun c -> try Some(c |> map_poly_in_clause R.(fun p -> let cache_t_to_st = HT.create 4 in - let p = if equational p then p else p>< of_term~vars:(free_variables' f) f_term in + let p = if equational p then p else p>< of_term s'f_term in p |> map_monomials(fun m' -> [m']|> (* If the substitution does not change variables in the monomial m, then m can be kept as is, even if m contains shifts that were to be eliminated. This is not robust because generally the essence is that m is constant (or even satisfies more recurrences compared to f) w.r.t. some variables, while the effect of the substitution plays no rôle. *) if Int_set.inter effect_dom (free_variables[m']) = Int_set.empty then id @@ -412,12 +417,11 @@ and propagate_subst s f = (* Apply substitution to terminal indeterminates. *) | A I -> `Go, const_eq_poly Z.one | A(V i) as x -> CCPair.map_snd((><)(const_eq_poly Z.one)) (transf upcoming (hd(hd(mul_indet[[x]])))) - | A(T(f',vars)) when CCOpt.equal poly_eq (Some f) (poly_of_term f') -> `Go, of_term~vars:(free_variables'(get_exn(poly_of_term sf_term))) sf_term + | A(T(s'f,vars)) when s'f==s'f_term -> `Go, of_term sf_term | A(T(t,vars)) when HT.mem cache_t_to_st t -> `Go, HT.find cache_t_to_st t | A(T(t,vars)) -> - let st_poly = [o s] >< get_or~default:(of_term~vars t) (poly_of_term t) in - let _,st,_ = poly_as_lit_term_id st_poly in - let st = of_term~vars:(free_variables' st_poly) st in + let _,st,_ = poly_as_lit_term_id([o s] >< get_or~default:(of_term~vars t) (poly_of_term t)) in + let st = of_term st in HT.add cache_t_to_st t st; `Go,st (* Replace Mᵢ=X[A(V i)] by ∑ⱼmᵢⱼMⱼ. *) | X[A(V i)] -> `Go, fold_left (++) _0 (map(fun j -> const_op_poly(Z.of_int(m@.(i,j))) >< [[mul_var j]]) (Int_set.to_list(rangeO s))) @@ -431,7 +435,6 @@ and propagate_subst s f = | _ -> `End, [o s]><[upcoming] in transf)))) with Exit -> None) - |>Iter.persistent|>(|<)"muunnettu" |> filter_recurrences_of~lead:false [get_exn(R.poly_of_term sf_term)(* safe by definition of sf_term *)] @@ -488,17 +491,28 @@ let sum_equality_inference clause = try "0 - {ᵐm-1-x}g ";(*9 debug *) |]in(* (p,)r,e,i: ✓ - F: leviää jo {ᵐn+1}fₘ kohdalla - c,b,A,S: leviää etenkin bₘₙ kanssa, ja useille sijoituksille jää kaavoja löytymättä + c,b,A,F,S: leviää etenkin bₘₙ kanssa (? ja sijoituksille jäi aikoinaan kaavoja löytymättä ?) *) let rec go() = print_string"tutki: "; init_rec_table(); - let p = (!)tests.(read_int()) in - print_endline("Tutkitaan " ^ R.poly_to_string p); - ctrl_C_stoppable(fun()-> - propagate_recurrences_to p; - ~ + propagate_recurrences_to p; + ~ + let p,p' = poly_of_string@@(p,p') in + print_endline(match lead_unifiers p p' with + | None -> "Samastumattomat "^ poly_to_string p ^", "^ poly_to_string p' + | Some(u,u') -> "Unify "^poly_to_string[u]^", "^poly_to_string[u']^"\n" + ^"p̲p̲. "^poly_to_string(hd(superpose p p'))^"\n" + ^match CCOpt.or_~else_:(leadrewrite p p')(leadrewrite p' p) with + | Some r -> "rw. "^ poly_to_string r + | None -> "") + | x -> print_endline("Paloja jaettaessa pilkusta pitää tulla 2 eikä " ^ string_of_int(length x))); go() in go(); exit 1; @@ -527,8 +541,65 @@ let sum_equality_inference clause = try ]; exit 1 (* tl(tl[clause;clause]) *) -with e -> print_endline Printexc.((*get_backtrace() ^"\n"^ *)match e with Failure m -> m | e -> to_string e); exit 1 - +with e -> print_endline Printexc.((*get_backtrace() ^"\n"^ *)match e with Failure m -> m | e -> to_string e); exit 1 + +(* Fibonacci ongelmatulosteotos: +summation_equality line 292 ≣̲̇26 propagating to {ᵐn＋１͘}fₘ +CCOption.pp line 9 ≣̲̇49 rw.M－N + NMfₘ－Mfₘ－fₘ +CCOption.pp line 9 ≣̲̇50 rw.M－N + -Mfₘ＋N²fₘ－fₘ +CCOption.pp line 9 ≣̲̇50 rw.M－N + N²fₘ－Nfₘ－fₘ +RecurrencePolynomial line 605 ≣̲̇48 p̲p̲. -NMfₘ－Mfₘ＋N³fₘ +CCOption.pp line 9 ≣̲̇48 rw.M－N + -Mfₘ＋N³fₘ－N²fₘ +CCOption.pp line 9 ≣̲̇48 rw.M－N + N³fₘ－N²fₘ－Nfₘ +CCOption.pp line 9 ≣̲̇49 rw.N²fₘ－Nfₘ－fₘ + ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ ‽ -Nfₘ＋fₘ +CCOption.pp line 9 ≣̲̇49 rw.-Nfₘ＋fₘ + -Nfₘ +CCOption.pp line 9 ≣̲̇49 rw.-Nfₘ＋fₘ + -fₘ +RecurrencePolynomial line 605 ≣̲̇48 p̲p̲. Mfₘ－N²fₘ +CCOption.pp line 9 ≣̲̇47 rw.M－N + -N²fₘ＋Nfₘ +CCOption.pp line 9 ≣̲̇48 rw.-Nfₘ＋fₘ + Nfₘ－fₘ +CCOption.pp line 9 ≣̲̇49 rw.-fₘ + -Nfₘ＋２fₘ +CCOption.pp line 9 ≣̲̇49 rw.-Nfₘ＋fₘ + fₘ +CCOption.pp line 9 ≣̲̇50 rw.-fₘ + 0 +RecurrencePolynomial line 605 ≣̲̇48 p̲p̲. -Nfₘ +CCOption.pp line 9 ≣̲̇47 rw.-fₘ + -Nfₘ＋fₘ +CCOption.pp line 9 ≣̲̇48 rw.-fₘ + -Nfₘ＋２fₘ +CCOption.pp line 9 ≣̲̇49 rw.-fₘ + -Nfₘ＋３fₘ +CCOption.pp line 9 ≣̲̇50 rw.-fₘ + -Nfₘ＋４fₘ +*) + +(* Stirling ongelmatulosteotos: +summation_equality line 292 ≣̲̇28 propagating to {ⁿx}cₙₘ +CCOption.pp line 9 ≣̲̇51 rw.N－X + XMcₙₘ－nNcₙₘ－Ncₙₘ－cₙₘ +RecurrencePolynomial line 605 ≣̲̇50 p̲p̲. -nN²cₙₘ－２N²cₙₘ＋X²Mcₙₘ－Ncₙₘ +CCOption.pp line 9 ≣̲̇50 rw.N－X + -２N²cₙₘ＋X²Mcₙₘ－nXNcₙₘ－Ncₙₘ +CCOption.pp line 9 ≣̲̇51 rw.N－X + X²Mcₙₘ－nXNcₙₘ－２XNcₙₘ－Ncₙₘ +CCOption.pp line 9 ≣̲̇51 rw.XMcₙₘ－nNcₙₘ－Ncₙₘ－cₙₘ + -XNcₙₘ－Ncₙₘ＋cₙₘ +CCOption.pp line 9 ≣̲̇52 rw.N－X + -Ncₙₘ－X²cₙₘ＋cₙₘ +CCOption.pp line 9 ≣̲̇52 rw.N－X + -X²cₙₘ－Xcₙₘ＋cₙₘ +*) (* Setup to do when MakeSumSolver(...) is called. *);; MainEnv.add_unary_inf "recurrences for ∑" sum_equality_inference @@ -538,7 +609,7 @@ end let sum_by_recurrences = ref false (* Define name and setup actions required to registration of this extension in libzipperposition_phases.ml *) -let extension = RecurrencePolynomial.{ +let extension = R.{ Extensions.default with name = "∑"; env_actions = [fun env -> if !sum_by_recurrences then