diff --git a/src/prover_phases/RecurrencePolynomial.ml b/src/prover_phases/RecurrencePolynomial.ml index d1d0f91e0..42691a789 100644 --- a/src/prover_phases/RecurrencePolynomial.ml +++ b/src/prover_phases/RecurrencePolynomial.ml @@ -23,6 +23,9 @@ let (|@) x must = let msg = Obj.(if tag(repr must)=string_tag then magic must else if magic must then "" else "ERROR") in if msg="" then x else(print_string Printexc.(raw_backtrace_to_string(get_callstack 999)^"\n\n\t"^msg^" "^str x); exit 1) let todo msg = Obj.magic"TODO" |@ msg +(* let invalid_argument msg = invalid_argument msg) *) +let invalid_argument msg = Obj.magic"invalid_argument:" |@ msg +let (=) x y = try x=y with Invalid_argument m -> invalid_argument m let (~=) x _ = x let (@@) = map_same @@ -54,7 +57,7 @@ let length_lex_list c = (fun l -> length l, l) %%> (-) *** lex_list c let lex_array c = to_list %%> lex_list c let length_lex_array c = (fun l -> Array.length l, l) %%> (-) *** lex_array c -let fold_left_1 f = function x::l -> fold_left f x l | _->raise(Invalid_argument "fold_left_1: empty list") +let fold_left_1 f = function x::l -> fold_left f x l | _->invalid_argument "fold_left_1: empty list" let max_list ?(ord=compare) = fold_left_1(fun x y -> if ord x y < 0 then y else x) (* use e.g. max_list(⊥ :: ...) *) let min_list ?(ord=compare) = fold_left_1(fun x y -> if ord x y > 0 then y else x) (* use e.g. min_list(⊤ :: ...) *) let max_array ?(ord=compare) ?bottom l = max_list ~ord (CCOpt.to_list bottom @ to_list l) @@ -62,12 +65,12 @@ let min_array ?(ord=compare) ?top l = min_list ~ord (CCOpt.to_list top @ to_list let sum_list = fold_left (+) 0 let sum_array = Array.fold_left (+) 0 let index_of p l = match find_idx p l with Some(i,_) -> i |_-> - raise(Invalid_argument("index_of among "-^ length l)) + invalid_argument("index_of among "-^ length l) let index_of' a l = match find_idx ((=)a) l with Some(i,_) -> i |_-> - raise(Invalid_argument("index_of' among "-^ length l ^ + invalid_argument("index_of' among "-^ length l ^ let pp = atompp a in if pp == atomprinters 0 then "" - else ": "-^ a ^" ∉ ["^ concat_view"; " pp l ^"]")) + else ": "-^ a ^" ∉ ["^ concat_view"; " pp l ^"]") let with_cache_2 c f = curry(with_cache_rec c (uncurry % f % curry)) let with_cache_3 c f = curry(with_cache_2 c (uncurry % f % curry)) @@ -78,7 +81,7 @@ let subscript = String.to_seq %> List.of_seq %> concat_view "" (fun c -> match c | '('->"₍" | ')'->"₎" | '+'->"₊" | '-'->"₋" | '='->"₌" | '0'..'9' -> string_part_at "₀ ₁ ₂ ₃ ₄ ₅ ₆ ₇ ₈ ₉" (code c - code '0') | 'a'..'y' -> string_part_at "ₐ ᵦ ᵪ ᵨ ₑ ᵩ ₔ ₕ ᵢ ⱼ ₖ ₗ ₘ ₙ ₒ ₚ ᵩ ᵣ ₛ ₜ ᵤ ᵥ ᵥᵥ ₓ ᵧ" (code c - code 'a') - | c -> raise(Invalid_argument("subscript: " ^ String.make 1 c ^ " has no subscript form assigned to it"))) + | c -> invalid_argument("subscript: " ^ String.make 1 c ^ " has no subscript form assigned to it")) type var = int @@ -94,6 +97,9 @@ and op = | S of var | X of op list (* never X(X p · q) or X(C p · q) or X(A I); always X(_@[A _]) *) | O of (var*poly)list + +let debug_poly_of_term = ref(Obj.magic()) +let debug_free_variables = ref(Obj.magic()) (* Distinguish operator polynomials and recurrence equations: is A present in monomials or not. *) let equational = for_all(fun m -> m!=[] & match hd(rev m) with A _ -> true | C o -> is0 o | _ -> false) @@ -113,7 +119,7 @@ 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))]] +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 @@ -446,7 +452,8 @@ let poly_of_id id = id |> ID.payload_find ~f:(fun data -> match data with | _ -> None) (* Retrieve polynomial embedded into a term and make it conform to the current monomial order. See also of_term. *) -let poly_of_term t = match view t with Const id -> poly_of_id id |_->None +let poly_of_term t = match view t with Const id -> poly_of_id id |_->None +let _=debug_poly_of_term:=poly_of_term (* Retrieve polynomial embedded into a literal and make it conform to the current monomial order. *) let poly_of_lit = function Equation(o,p,true) when o==term0 -> poly_of_term p |_->None @@ -527,7 +534,7 @@ and indeterminate_product x y = | O f, A I -> const_eq_poly Z.one | O f, A(V n) -> get_or~default:[[y]] (assq_opt n f) | O f, A(T(_,v)) -> [o(filter(fun(i,_)-> mem i v) f) @ [y]] (* No recursive call to >< in order to avoid endless loop. *) - | A _, A _ -> raise(Invalid_argument("indeterminate_product ("^ indet_to_string x ^") ("^ indet_to_string y ^")")) + | A _, A _ -> invalid_argument("indeterminate_product ("^ indet_to_string x ^") ("^ indet_to_string y ^")") | A _, y -> [[y;x]] (* Push A from left to right. Caller must push A fully right before _,A multiplication! *) | x, y -> [[x;y]] @@ -636,6 +643,7 @@ and free_variables p' = Int_set.(let rec monoFV = function union_map monoFV p') let free_variables' = Int_set.to_list % free_variables +let _=debug_free_variables:=free_variables' (* Output ϱ,σ,raw. Renaming substitution indeterminate ϱ satisfies dom ϱ = vs\taken and img ϱ ∩ vs∪taken = ∅. Substitution indeterminate σ undoes ϱ meaning [σ]><[ϱ]>

map(fun(i,p) -> let put vs sh = (* i ↦ vs+sh = variable list + shift constant *) shift.(i) <- sh; - if vs<>[var_poly i] then (* identity variable mapping gets encoded by [||] always *) + if not(vs=[var_poly i]) then (* identity variable mapping gets encoded by [||] always *) matrix.(i) <- fold_left (fun row -> function | [A(V n)] -> row.(n) <- 1; row | [C a; A(V n)] -> row.(n) <- Z.to_int_exn a; row @@ -689,7 +697,7 @@ let unembed act_on = map_indeterminates(function A(T(t,_)) as x -> ( let to_poly_poly: (poly * op list) list -> poly = fold_left (++) _0 % map(fun(coef, arg) -> coef >< match arg with | [A(T _)] -> [arg] - | _ -> (* If arg is not term, pack it into such. Since the packing is not a true function, input is taken in the (poly * op list)list -form grouped by arg. *) + | _ -> (* If arg is not term, pack it into such. Since the packing is not a true function (actually it now is but the equality enforcing cache might be reworked), input is taken in the (poly * op list)list -form grouped by arg. *) let _,t,_ = poly_as_lit_term_id [arg] in of_term~vars:(free_variables'[arg]) t) (* Turn general formula into a recurrence in operator polynomial representation by embedding other parts into argument terms. *) @@ -711,15 +719,15 @@ let match_start(type r) ?(split=' ') patterns string = let exception Result of r in let rec apply_first = function (* Ocaml top-level (basic and utop) truncates error messages and it is not obvious how to avoid this. Hence to display important info from both of the long inputs, we manually truncate the matched string. This is unfortunate because without UTF-8 support, that we do not care to add as a dependency, the message easily ends up locally corrupted. *) - | [] -> raise(Invalid_argument String.( - "match_start: "^ sub string 0 (min (length string) (3 + max_list(List.map(length%fst) rules))) ^"... starts by none of patterns:\n"^ concat (make 1 split) (List.map fst rules))) + | [] -> invalid_argument String.( + "match_start: "^ sub string 0 (min (length string) (3 + max_list(List.map(length%fst) rules))) ^"... starts by none of patterns:\n"^ concat (make 1 split) (List.map fst rules)) | (p,act)::rest -> match if_start p act string with | Some ok -> raise(Result ok) | None -> apply_first rest in try apply_first rules with Result r -> r -let testterms = map (Term.const ~ty:Type.term % ID.make) ["b";"c";"f";"g";"q";"z"] +let testterms = map (Term.const ~ty:Type.term % ID.make) ["b";"c";"f";"g";"q";"z";"γ";"δ";"λ";"φ";"ψ";"ω";"ξ"] (* Usage example: Hashtbl.add "f" "xy" *) let variable_dependency = Hashtbl.create 6 @@ -732,37 +740,39 @@ let variable_dependency = Hashtbl.create 6 {ᵃₜb.Nb}{ᵉ2a}{ⁱ3e}{ʲ4i}{ᵏ5j}{ˡ1+k}{ᵐl+mn-2} {ⁿm-n}f + N{ˣm}∑ˣf *) -[@@@warning "-14"](* Regular expressions depend on UTF-8 encoding—did not work?! *) +[@@@warning "-14"](* Regular expressions depend on UTF-8 encoding—did not work => built it from character list. *) let rec poly_of_string s = - (* Workaround to add substitutions ({ᵛᵃʳpoly} == {var↦poly}) to unextensible setup: Replace {ᵛ...} by an encoding character c and add rule c->... for map_start_factor. *) - let delim = regexp(String.of_seq(to_seq['{';'.';'.';'[';chr 131;'-';chr 191;']';'?';'\\';'|';'}'])) in + (* Workaround to add substitutions ({ᵛᵃʳpoly} == {var↦poly}) to unextensible setup: Replace {ᵛ...} by an encoding character c and add rule c->... for map_start_factor. In Ocaml's regexp \| denotes alternatives while lonely | matches literal bar. Superscripts have UTF-8 length 2 or 3 bytes, and end-bytes are disjoint from start-bytes. *) + let delim = regexp("{..["^String.of_seq(to_seq[chr 131;'-';chr 191])^"]?\\|}") in let s', mapSubst = full_split delim s |> let rec packSubst = function | Delim"}" :: s' -> packSubst s' | Delim v :: Text p :: s' -> let r,m = packSubst s' in let codeSubst = String.make 1 (chr(length m)) in - if codeSubst=" " then raise(Failure("packSubst: Too many substitutions in "^s)); + if codeSubst=" " then failwith("packSubst: Too many substitutions in "^s); codeSubst ^ r, (codeSubst, fun i->String.[o[index_of' (sub v 1 (length v - 1)) (split_on_char ' ' "ʸ ˣ ᵛ ᵘ ᵗ ˢ ʳ ᵖ ᵒ ⁿ ᵐ ˡ ᵏ ʲ ⁱ ʰ ᵉ ᵃ"), poly_of_string p]]) :: m | Text p :: s' -> map_fst((^)p) (packSubst s') | [] -> "",[] - | s' -> raise(Invalid_argument("packSubst: "^ to_string(function Text t | Delim t -> t) s' ^" is ill-formed in "^s)) + | s' -> invalid_argument("packSubst: "^ to_string(function Text t | Delim t -> t) s' ^" is ill-formed in "^s) in packSubst in (* sanity check for operator vs. recurrence *) let check_mul_indet p = if equational p then mul_indet p else - raise(Invalid_argument("Operator polynomial " ^ poly_to_string p ^ " cannot become a multiplier indeterminate in " ^ s)) in + invalid_argument("Operator polynomial " ^ poly_to_string p ^ " cannot become a multiplier indeterminate in " ^ s) in + (* substitute string s onto every character c *) let replace c s = String.concat"" % map(fun a -> if a=c then s else String.make 1 a) % of_seq % String.to_seq in + (* convenience composition chain used twice right below *) let split_map_fold split fold mapper = String.split_on_char split %> map mapper %> fold_left_1 fold in let p = replace '-' "+-" s' |> split_map_fold '+' (++) ( split_map_fold '.' (fun n m -> check_mul_indet n >< m) - (poly_of_mono_string mapSubst % replace ' ' "")) in + (poly_of_mono_string mapSubst % replace ' ' "" % replace '\t' "")) in (* Make argument A I explicit for C and X monomials if A _ appears in any monomial. *) let p_eq = filter((function A _ :: _ -> true | _ -> false) % rev) p in let p_CX = filter(for_all(function C _ | X _ -> true | _ -> false)) p in if p_eq=[] then p else if length p_eq + length p_CX = length p then p_eq ++ (p_CX><[[A I]]) - else raise(Invalid_argument(poly_to_string p ^ " from " ^ s ^ " mixes operator and applied monomials")) + else invalid_argument(poly_to_string p ^ " from " ^ s ^ " mixes operator and applied monomials") and poly_of_mono_string base_rules s' = if s'="" then _0 (* neutral in splitting above *) else let map_start_factor rules = match_start (map (fun(p,f)-> p, @@ -788,6 +798,6 @@ and poly_of_mono_string base_rules s' = if s'="" then _0 (* neutral in splitting ("∂ d",fun i->[[D 1]]); ("0 1 2 3 4 5 6 7 8 9",fun i->const_op_poly(Z.of_int i)); ("-",fun i->const_op_poly(Z.minus_one)); - ("b c f g q z",fun i->embedded_term i); - ("B C F G Q Z",fun i->mul_indet(embedded_term i)); + ("b c f g q z γ δ λ φ ψ ω ξ",fun i->embedded_term i); + ("B C F G Q Z Γ Δ Λ Φ Ψ Ω Ξ",fun i->mul_indet(embedded_term i)); ]) \ No newline at end of file diff --git a/src/prover_phases/summation_equality.ml b/src/prover_phases/summation_equality.ml index 2dff36d95..50109e2de 100755 --- a/src/prover_phases/summation_equality.ml +++ b/src/prover_phases/summation_equality.ml @@ -35,7 +35,8 @@ module HV = Hashtbl.Make(struct let equal = HVar.equal(==) let hash = HVar.hash end) - + +let (=) = RecurrencePolynomial.(=) let todo = RecurrencePolynomial.todo let (~=) x _ = x let (@@) = CCPair.map_same @@ -246,11 +247,16 @@ let filter_map_recurrences map_poly = Iter.filter_map(fun c -> |> Iter.to_rev_list) ~=Proof.Step.trivial) with Invalid_argument _ -> None) -(* Filter those clauses that have eligible polynomial with leading term M f where some monomial M operates to a term f representing an expression in polylist. Then unembed all other polynomials outside polylist. *) -let filter_recurrences_of polylist = filter_map_recurrences R.(fun p -> if_~=(match terms_in[hd p] with - | [t] -> mem ~eq:(CCOpt.equal poly_eq) (poly_of_term t) (map CCOpt.pure polylist) - | _ -> false -) (unembed(fun p' -> not(mem~eq:poly_eq p' polylist)) p)) +(* Filter those clauses that have eligible polynomial whose every term M f, where term f represents an expression from polylist, has normal operator monomial M (that consist only of multipliers and 1-shifts). Moreover the leading term must have such form M f. After the filtering, unembed all other polynomials outside polylist. + Notes: The ordering of the embedded polynomial term f can be problematic. The polynomial structure of f does not automatically contribute to the ordering. Hence requiring, that M f leads, silently discards recurrences that forgot to take f into account in the ordering. However at least propagation to addition and affine forms relies to the presence of the requirement that M f leads. Now try making leading requirement optional via parameter. *) +let filter_recurrences_of ?(lead=true) polylist = filter_map_recurrences R.(fun p -> if_~= + (let wanted_terms = p |> map_monomials(fun m -> match terms_in[m] with + | [t] when mem ~eq:(CCOpt.equal poly_eq) (poly_of_term t) (map CCOpt.pure polylist) -> [m] + | _ -> _0) + in not(poly_eq _0 wanted_terms) + & (not lead or mono_eq (hd p) (hd wanted_terms)) + & poly_eq wanted_terms (oper_coef_view wanted_terms)) + (unembed(fun p' -> not(mem~eq:poly_eq p' polylist)) p)) (* Transform recurrence polynomial(s) of the clause by the given function. *) let map_poly_in_clause f ?(rule=Proof.Rule.mk"arithmetic on recurrence") c = @@ -259,13 +265,6 @@ let map_poly_in_clause f ?(rule=Proof.Rule.mk"arithmetic on recurrence") c = (Proof.Step.inference ~rule) -(* Associates index variables to terms. *) -let variable_table = HT.create 8 -(* Let an embedded term depend on a variable. Polynomial parameterized version of HT.add that'd works on terms like HT.find_all that retrieves the dependencies. *) -let add_dependence embedded_term = match embedded_term with - | [[R.A(T(t,_))]] -> HT.add variable_table t - | _ -> raise(Invalid_argument("add_dependence: Expected a polynomial embedding a term but got "^ R.poly_to_string embedded_term)) - (* Explicit cache for propagate_recurrences_to. We could also use with_cache_rec but its explicit recursive call functionparameter is slightly inconvenient in a long mutually recursive definition group. *) module PolyMap = Hashtbl.Make(struct type t = R.poly @@ -283,7 +282,7 @@ let add_new_rec p c = PolyMap.add recurrence_table p let rec propagate_recurrences_to f = match PolyMap.find_opt recurrence_table f with | Some r -> r | None -> - let r = Iter.to_rev_list(match f with + let r = Iter.to_rev_list(match "propagating to "| propagate_oper_affine f | [X q :: p] -> propagate_times [q] [p] | [S i :: p] -> propagate_sum i [p] @@ -330,15 +329,17 @@ and propagate_sum i f = in let sumf = R.(let _,sumf,_ = poly_as_lit_term_id([[S i]]>< of_term~vars:(free_variables' f) f_term) -- sumf) in Iter.of_list(propagate_recurrences_to f) - |> saturate_with_order sum_blocker + |> saturate_with_order sum_blocker |> Iter.map(map_poly_in_clause R.((><)[[S i]])) - (* Replace each ∑ᵢf by the embedding sumf by rewriting by polynomial ∑ᵢf-sumf. *) - |> Iter.cons(definitional_poly_clause R.(([[S i]]>< of_term~vars:(free_variables' f) f_term) -- sumf)) - |> saturate_with_order R.(elim_indeterminate(function`S _->1 | _->0)) (* orient the rewriter *) - (* Add the definitional N∑ᑉⁿf = ∑ᑉⁿf + fₙ with sumf embedded while f needs not to be. *) + (* Replace each ∑ᵢf by the embedding sumf by rewriting with temporary polynomial ∑ᵢf-sumf. *) + |> Iter.cons embed_sumf_rewriter + |> saturate_with_order R.(elim_indeterminate(function`S _->2 |`T sum_f when sum_f == hd(terms_in sumf) -> 1 | _->0)) (* orient the rewriter but keep sumf leading for filtering *) + |> Iter.filter((!=)embed_sumf_rewriter) (* perhaps filtered anyway in the end *) + (* Add the definitional N∑ᑉⁿf = ∑ᑉⁿf + fₙ with sumf embedded while f is not. *) |> Iter.cons(definitional_poly_clause R.(([[shift i]]> filter_recurrences_of R.[ [[S i]]> filter_recurrences_of R.[ [[S i]]> Int_set.mem v dom) s in (* => domain of s ⊆ dom ...necessary? *) + let effect_dom = Int_set.of_list(map fst s) in + let dom = R.free_variables f in + assert(Int_set.subset effect_dom dom); match R.view_affine s with | None -> Iter.empty | Some(m,a) -> @@ -359,43 +360,49 @@ and propagate_subst s f = let on_dom f = map f (Int_set.to_list dom) in (* 𝕊ⱼ = ∏ᵢ Sᵢ^mᵢⱼ = O[0,m₀ⱼ;...;i,mᵢⱼ;...] where j runs over range and i over domain *) let ss_j = hd(o(on_dom(fun i -> i, [var_poly i]++const_eq_poly(Z.of_int(m@.(i,j)))))) in - (* TODO Recurrence polynomial data structure needs an additional marker to distinguish compound shifts from ordinary ones in all corner cases. *) - if is1shift ss_j then failwith("Unimplemented: "^ string_of_int j^"ᵗʰ compound shift cannot be distinguished from 1-shift when propagating to substitution "^ poly_to_string[o s] ^" of "^ poly_to_string f); + (* TODO Recurrence polynomial data structure needs an additional marker to distinguish compound shifts from ordinary ones in all corner cases including permutations. +  We can tolerate a confusion between single and multi for a shift w.r.t. a new variable. This relaxation must be taken into account when transforming multishifts to 1-shifts. *) + if Int_set.mem j dom & is1shift ss_j then failwith("Unimplemented: "^ string_of_int j^"ᵗʰ compound shift cannot be distinguished from 1-shift when propagating to substitution "^ poly_to_string[o s] ^" of "^ poly_to_string f); let eq_j = product(on_dom(fun i -> pow' poly_alg [[shift i]] (max 0 (m@.(i,j))))) -- product([[ss_j]] :: on_dom(fun i -> pow' poly_alg [[shift i]] (- min 0 (m@.(i,j))))) in ((ss_j, shift j), j), eq_j ) in - (* We must eliminate all domain shifts except ones skipped above: dom\( rangeO s \ {j | ∃ ss_j} ) *) + (* 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(function((_,j),_)->j) 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) |> Iter.append(Iter.of_list(map (definitional_poly_clause % snd) multishifts_and_equations)) |> saturate_with_order(R.elim_indeterminate(function |`O[i,R.[[A I]]] -> if Int_set.mem i elimIndices then 1 else 0 - | _ -> 0)) + | _ -> 0)) |> Iter.filter_map(fun c -> try Some(c |> map_poly_in_clause R.(fun p -> - let cache_t_to_st = HT.create 1 in - let p = if equational p then p else p>< of_term~vars:(free_variables' f) f_term in - p |> map_indeterminates(let rec transf = function - | C a -> const_op_poly a - (* Apply substitution to terminal indeterminates. *) - | A I -> const_eq_poly Z.one - | A(V i) as x -> transf(hd(hd(mul_indet[[x]]))) >< const_eq_poly Z.one - | A(T(f',vars)) when CCOpt.equal poly_eq (Some f) (poly_of_term f') -> of_term~vars:(free_variables'(get_exn(poly_of_term sf_term))) sf_term - | A(T(t,vars)) when HT.mem cache_t_to_st t -> of_term~vars(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 - HT.add cache_t_to_st t st; of_term~vars:(free_variables' st_poly) st - (* Replace Mᵢ=X[A(V i)] by ∑ⱼmᵢⱼMⱼ. *) - | X[A(V i)] -> fold_left (++) _0 (map(fun j -> const_op_poly(Z.of_int(m@.(i,j))) >< [[mul_var j]]) (Int_set.to_list(R.rangeO s))) - (* Discard clauses still containing shifts that were to be eliminated. *) - | O[i,[[A(V j);A I]]] when i=j & Int_set.mem i elimIndices -> raise Exit - (* Replace 𝕊ⱼ by Sⱼ by looking it up from multishifts_and_equations. *) - | O _ as x -> [[get_or~default:x (CCList.assoc_opt ~eq:indet_eq x (map(fst%fst) multishifts_and_equations))]] - | _ -> raise Exit - in transf))) + 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 + 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 + else map_indeterminates(let rec transf = function + | C a -> const_op_poly a + (* Apply substitution to terminal indeterminates. *) + | A I -> const_eq_poly Z.one + | A(V i) as x -> transf(hd(hd(mul_indet[[x]]))) >< const_eq_poly Z.one + | A(T(f',vars)) when CCOpt.equal poly_eq (Some f) (poly_of_term f') -> of_term~vars:(free_variables'(get_exn(poly_of_term sf_term))) sf_term + | A(T(t,vars)) when HT.mem cache_t_to_st t -> 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 + HT.add cache_t_to_st t st; st + (* Replace Mᵢ=X[A(V i)] by ∑ⱼmᵢⱼMⱼ. *) + | X[A(V i)] -> fold_left (++) _0 (map(fun j -> const_op_poly(Z.of_int(m@.(i,j))) >< [[mul_var j]]) (Int_set.to_list(R.rangeO s))) + (* Discard clauses still containing shifts that were to be eliminated. Since elimIndices ⊆ dom, we keep shifts of new variables that the below case interpretates as multishifts. *) + | O[i,[[A(V j)];[A I]]] when i=j & Int_set.mem i elimIndices -> raise Exit + (* Replace 𝕊ⱼ by Sⱼ by looking it up from multishifts_and_equations. *) + | O _ as x -> [[get_or~default:x (CCList.assoc_opt ~eq:indet_eq x (map(fst%fst) multishifts_and_equations))]] + | _ -> raise Exit + in transf)))) with Exit -> None) - |> filter_recurrences_of[get_exn(R.poly_of_term sf_term)(* safe by definition of sf_term *)] + |> filter_recurrences_of~lead:false [get_exn(R.poly_of_term sf_term)(* safe by definition of sf_term *)] (* Make a polynomial into a new recurrence of its maximal term. Since polynomial is packed into a new clause, this function in this form is only suitable for testing. *) @@ -403,10 +410,10 @@ let declare_recurrence r = add_new_rec R.(max_list ~ord:(term_of_arg%%>Term.compare) (arg_terms_in r)) (definitional_poly_clause r) -let sum_equality_inference clause = +let sum_equality_inference clause = try (* for testing ↓ *) let (!) = R.poly_of_string in - let eq0' p = make_clause (map R.polyliteral p) ~=(Proof.Step.assert' ~file:"" ~name:"" ()) in + let eq0' p = make_clause (map R.polyliteral p) ~=Proof.Step.trivial in let split_or k d s = match String.split_on_char k s with | [a;b] -> a,b | [a] -> if k='.' then d,a else a,d | _ -> raise Exit in let eq0 ss = eq0' R.[fold_left (++) _0 (List.map(fun cmt -> @@ -414,9 +421,7 @@ let sum_equality_inference clause = let m,t = split_or '\'' "" mt in Z.of_string c *: poly_of_string m >< of_term~vars:(todo"vars in eq0")(have t [] int) ) (String.split_on_char '+' ss))] in - - add_dependence !"b" (match !"m" with [[X[A(V m)]]]->m |_->assert false); - HS.add R.variable_dependency "b" "m"; + (* declare_recurrence !"NNf-Nf-f"; declare_recurrence !"Ng-ng-g"; @@ -424,13 +429,48 @@ let sum_equality_inference clause = propagate_recurrences_to !"g+f"; (* OK *) propagate_recurrences_to !"g+nf"; (* diverge? *) propagate_recurrences_to !"∑ᵐb"; (* OK *) -*) + propagate_recurrences_to !"{ᵐm-n-1}b"; (* OK *) - propagate_recurrences_to !"∑ⁿ{ᵐm-n-1}b"; (* miss M-recurrence unless above is explicitly included—weird! *) - propagate_recurrences_to !"{ⁿm}∑ⁿ{ᵐm-n-1}b"; (* ok, extra rec. *) - propagate_recurrences_to !"{ⁿm}∑ⁿ{ᵐm-n-1}b - ∑ᵐb"; (* maybe ok *) - - ~ map(uncurry(HS.add R.variable_dependency)); + let init_rec_table() = PolyMap.clear recurrence_table; + declare_recurrence !"Nz-xz "; (* zₓₙ = xⁿ *) + declare_recurrence !"MMf-Mf-f "; (* fₘ = mᵗʰ Fibonacci *) + declare_recurrence !"xXq+Xq-q "; (* qₓ = x!⁻¹ *) + declare_recurrence !"mMb-nMb+Mb-mb-b "; (* binomial coefficient: *) + declare_recurrence !"nNb+Nb-mb-nb "; (* bₘₙ = (ₙͫ ) *) + declare_recurrence !"MNc-nNc-Nc-c "; (* Stirling cₘₙ = {ₙͫ } *) + declare_recurrence !"MMγ-γ-Mg-g "; (* double step γ=∑g *) + in let tests = [| + "{ᵐm+u}{ⁿh}b - {ⁿh+1}∑ⁿB{ᵐu}{ⁿh-n}b ";(*0 convolution *) + "∑ᵐ{ⁿm+1}∑ⁿg - {ⁿm}∑ⁿ∑ᵐg + {ⁿm}∑ⁿ{ᵐn}∑ᵐg ";(*1 interchange *) + "∑ᵐg - {ˣm}∑ˣ{ᵐm-1-x}g ";(*2 reverse *) + "∑ᵐg - γ ";(*3 elementary *) + "{ˣx+y}{ⁿm}z - {ⁿm+1}∑ⁿBx{ˣx-n}{ⁿn-1}Z{ˣy+n+1}{ⁿm-n-1}z ";(*4 Abel *) + "Q{ⁿm}z - {ⁿx+1}∑ⁿC{ˣx-n}q ";(*5 Stirling *) + "{ˣx+y}{ⁿm}z - {ⁿm+1}∑ⁿBZ{ˣy}{ⁿm-n}z ";(*6 binomial *) + "{ᵐn+1}f - {ᵐn+1}∑ᵐ{ⁿn-m}b ";(*7 Fibonacci *) + "γ - {ˣm}∑ˣ{ᵐm-1-x}g ";(*8 presented*) + |]in(* + (p,)r,e: ✓ + i: miss + S: loop final + c,b,F,A: cmp abstract with bₘₙ + *) + let rec go() = + print_string"tutki: "; + (* PolyMap.clear recurrence_table; *) + init_rec_table(); + let p = (!)tests.(read_int()) in + print_endline("Tutkitaan " ^ R.poly_to_string p); + propagate_recurrences_to p; + ~ print_endline x; exit 1 (* Setup to do when MakeSumSolver(...) is called. *);; -(* MainEnv.add_unary_inf "test" test_hook; *) MainEnv.add_unary_inf "recurrences for ∑" sum_equality_inference end (* Is this extension enabled? Set by a command line option. *) -let sum_by_recurrences = ref true +let sum_by_recurrences = ref false (* Define name and setup actions required to registration of this extension in libzipperposition_phases.ml *) let extension = RecurrencePolynomial.{