From 47155f360f1b986e830a9b3d80e8989dd294fec2 Mon Sep 17 00:00:00 2001 From: Visa Date: Fri, 27 Oct 2023 17:24:10 +0300 Subject: [PATCH] Work with embedding of terms & polynomials. No shift simplification quick-fix. --- .ocamlinit | 55 ++- src/core/Util.ml | 11 +- src/core/Util.mli | 5 +- src/prover_phases/RecurrencePolynomial.ml | 193 +++++++--- src/prover_phases/TypeTests.ml | 68 ++-- src/prover_phases/summation_equality.ml | 440 +++------------------- 6 files changed, 270 insertions(+), 502 deletions(-) diff --git a/.ocamlinit b/.ocamlinit index 5d4bd0798..93c47229f 100644 --- a/.ocamlinit +++ b/.ocamlinit @@ -2,8 +2,6 @@ #use "topfind";; (* ## end of OPAM user-setup addition for ocamltop / base ## keep this line *) -let cmaPath = "/home/vnn490/Documents/Zipo/zipperposition/_build/default/src/";; - (* Steps to fix “Error: unbound module An_example” in Ocaml interpreter: 1. Find .ml file defining An_example (e.g. F12 opens definition in VSCode+Merlin). 2. #require an external dependency, or proceed to step 3 for Zipperposition specific An_example. @@ -13,7 +11,7 @@ let cmaPath = "/home/vnn490/Documents/Zipo/zipperposition/_build/default/src/";; 6. Restart. Other notes: -#mod_use "path/to/a_file.ml";; Wraps inside module A_file like the compiler. +#mod_use "path/to/a_file.ml";; wraps inside module A_file like the compiler. Program ocamlobjinfo or objinfo prints info about given .cma file. $OCAML_TOPLEVEL_PATH/autoload might be an alternative to this file. This file makes the toplevel slow to start. *) @@ -21,48 +19,52 @@ This file makes the toplevel slow to start. *) (* Zipperposition files: .cmi *) -#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/logtk";; -#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/logtk/proofs";; -#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/logtk/parsers";; -#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/logtk/solving";; -#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/logtk/arbitrary";; +#directory "./_build/install/default/lib/logtk";; +#directory "./_build/install/default/lib/logtk/proofs";; +#directory "./_build/install/default/lib/logtk/parsers";; +#directory "./_build/install/default/lib/logtk/solving";; +#directory "./_build/install/default/lib/logtk/arbitrary";; -#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition";; -#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition/avatar";; -#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition/arith";; -#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition/calculi";; -#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition/phases";; -#directory "/home/vnn490/Documents/Zipo/zipperposition/_build/install/default/lib/libzipperposition/induction";; +#directory "./_build/install/default/lib/libzipperposition";; +#directory "./_build/install/default/lib/libzipperposition/avatar";; +#directory "./_build/install/default/lib/libzipperposition/arith";; +#directory "./_build/install/default/lib/libzipperposition/calculi";; +#directory "./_build/install/default/lib/libzipperposition/phases";; +#directory "./_build/install/default/lib/libzipperposition/induction";; #directory ".";; (* Source .ml files may be duplicated in the .../_build/install/... directories so put the working directory into the search path as the last one to give it the precedence. *) -(* External dependencies *) +(* External dependencies—missing optional ones just print warnings and continue *) -#require "batteries";; (* If ∄ Batteries, this just prints warning and continues. *) -(* from src/{core,prover,solving}/dune files, (libraries ...) rows *) +#require "batteries";; +(* from src/{core,prover,...}/dune files, (libraries ...) rows *) #require "containers";; #require "containers-data";; #require "iter";; #require "oseq";; #require "zarith";; #require "unix";; -#require "str";; +#require "str";; +#require "mtime.clock.os";; #require "msat";; #require "msat.tseitin";; -#require "qcheck";; +#require "qcheck";; +#require "logtk.arith";; (* Zipperposition files: .cma *) - -let workingDirectory = Unix.getcwd();; -let inZipperpositionDirectory p = Unix.chdir(cmaPath^p);; + +let workingDirectory = Sys.getcwd();; +let cmaPath = "/_build/default/src/";; +let inZipperpositionDirectory p = try Sys.chdir(workingDirectory^cmaPath^p) +with Sys_error e -> print_string(e^" and so ");; inZipperpositionDirectory "core";; #load "logtk.cma";; (* dlllogtk.so is found from the set working directory *) - + inZipperpositionDirectory "proofs";; -#load "logtk_proofs.cma";; +#load "logtk_proofs.cma";; inZipperpositionDirectory "parsers";; #load "logtk_parsers.cma";; @@ -79,9 +81,6 @@ inZipperpositionDirectory "prover";; inZipperpositionDirectory "prover_calculi/avatar";; #load "libzipperposition_avatar.cma";; -inZipperpositionDirectory "prover_calculi/arith";; -#load "libzipperposition_arith.cma";; - inZipperpositionDirectory "prover_calculi/induction";; #load "libzipperposition_induction.cma";; @@ -194,5 +193,5 @@ open RecurrencePolynomial;; #mod_use "summation_equality.ml";; open Summation_equality;; -Unix.chdir workingDirectory;; (* restore original working directory *) +Sys.chdir workingDirectory;; (* restore original working directory *) open Batteries (* If ∄ Batteries, this crashes, so make it the last command. *) \ No newline at end of file diff --git a/src/core/Util.ml b/src/core/Util.ml index ad497f1df..86cf0e263 100755 --- a/src/core/Util.ml +++ b/src/core/Util.ml @@ -203,14 +203,13 @@ module UntypedPrint = struct let string_printers: ((any -> bool) * (any -> string)) list ref = ref[] let add_pp type_test to_string = string_printers := (type_test, to_string % magic) :: !string_printers + + let registered_types() = magic List.map fst !string_printers let str x = - let rec loop = function [] -> raise(Failure "Printers from TypeTests.ml are uninitialized!") - | (type_test, to_string)::printers -> - if is_int(repr x) then string_of_int(magic x) (* prioritize int's *) - else if type_test x then to_string x - else loop printers - in loop(magic !string_printers) + let _, to_string = try magic List.find (CCFun.flip fst x) !string_printers + with Not_found -> failwith "Printers from TypeTests.ml are uninitialized!" + in to_string x (* Print message msg preceded by FILE line LINE ≣̲̇CALL-DEPTH of the caller's caller. *) let print_with_caller msg = diff --git a/src/core/Util.mli b/src/core/Util.mli index 21494d5fb..c7c03d531 100755 --- a/src/core/Util.mli +++ b/src/core/Util.mli @@ -114,7 +114,10 @@ module UntypedPrint : sig val (~<) : 'a -> 'a val (|<) : string -> 'a -> 'a (** Prefix an expression with [~<] or [message|<] to trace it together with its location and call stack depth. Output can contain oddities due to inlining and lack of runtime types. *) - + + val registered_types : unit -> ('a -> bool) list + (** Retrieve the type tests used for polymorphic printing in order of priority. *) + val str : 'a -> string (** Adhoc polymorphic to_string *) diff --git a/src/prover_phases/RecurrencePolynomial.ml b/src/prover_phases/RecurrencePolynomial.ml index b0bee25ab..d1d0f91e0 100644 --- a/src/prover_phases/RecurrencePolynomial.ml +++ b/src/prover_phases/RecurrencePolynomial.ml @@ -19,13 +19,29 @@ open CCFun open Stdlib (* Utilities *) -let todo msg = print_string("TO‍‍D‍O "^msg^"\t"); assert false +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 (~=) x _ = x let (@@) = map_same let (%%>) = compose_binop let (%>>) f g x y = g(f x y) let (<:>) r f = r:=f!r let is0 = Z.(equal zero) +(* Simple polymorphic print helper independent of the heavyweight TypeTests.ml. Unknown typing can be tested as atompp _ == atomprinters 0 *) +let atomprinters = + let (!)p = p % Obj.magic in + let pps = [| ~="⁇"; !string_of_int; !id; !string_of_float; !(fun x -> !id(Obj.field x 0)) |] in + fun i -> !get pps i (* guarantee polymorphicity with constant printers *) +let atompp x : 'any->string = Obj.(let x = magic x in + if is_int x then 1 else + if tag x = string_tag then 2 else + if tag x = double_tag then 3 else + if tag x = object_tag then 4 else + 0) |> atomprinters +let (-^) s x = s ^ atompp x x (* Lexicographic product of comparison functions onto tuples. *) let ( *** ) c1 c2 (x1,x2) (y1,y2) = match c1 x1 y1 with 0 -> c2 x2 y2 | r -> r (* Example: lex_list(-) [1;4;2] [1;3;3;3] > 0 where (-) compares positive ints without overflow. *) @@ -45,8 +61,13 @@ let max_array ?(ord=compare) ?bottom l = max_list ~ord (CCOpt.to_list bottom @ t let min_array ?(ord=compare) ?top l = min_list ~ord (CCOpt.to_list top @ to_list l) let sum_list = fold_left (+) 0 let sum_array = Array.fold_left (+) 0 -let index_of p l = fst(get_exn(find_idx p l)) -let index_of' a = index_of((=)a) +let index_of p l = match find_idx p l with Some(i,_) -> i |_-> + raise(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 ^ + let pp = atompp a in + if pp == atomprinters 0 then "" + 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)) @@ -63,7 +84,7 @@ let subscript = String.to_seq %> List.of_seq %> concat_view "" (fun c -> match c type var = int let compare_var = (-) (* variables are positive *) (* Argument terms of operation: In principle they could be anything. However we need generic sorting and embedability to clauses. Second is biggest of many problems for an extra type variable, while first is problem for using the extensible exception type to hold the arguments. Instead we rely on that terms suffice as arguments—after all polynomials can be embedded to them. *) -type atom = I | V of var | T of Term.t +type atom = I | V of var | T of Term.t * var list type poly = op list list and op = | C of Z.t (* never C 1; unique if present *) @@ -88,10 +109,22 @@ 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. *) -let shift i = O[i,[[A(V i)];[A I]]] -let mul_var i = X[A(V i)] +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 t = [[A(T t)]] +let of_term~vars t = [[A(T(t, sort_uniq~cmp:(-) vars))]] + +(* Distinguishes standard shift indeterminates from general substitutions. *) +let is1shift = function O[i,[[A(V j)];[A I]]] -> i=j | _ -> false +(* Distinguishes multishift indeterminates from general substitutions. *) +let is_multishift = function O f -> f |> for_all(function + | i, [[A(V j)]; ([A I] | [C _; A I])] -> i=j + |_->false) |_->false +(* Unused. See view_affine *) +let is_affine = function O f -> f |> for_all(fun(_,f') -> f' |> for_all(function + | [A I] | [C _; A I] | [A(V _)] | [C _; A(V _)] -> true + |_->false)) |_->false (* Auxiliarity functions for general algebraic structures *) @@ -195,7 +228,7 @@ let total_weight w weight = let rec recW i=i|> fold_left(fun sum op -> w#plus sum (match op with | C _ | A I -> w#o | A(V i) -> weight(`V i) - | A(T t) -> weight(`T t) + | A(T(t,_)) -> weight(`T t) | D i -> weight(`D i) | S i -> weight(`S i) | O f -> weight(`O f) (* sum' w (map(fun(n,fn)-> weight(`O(n,fn))) f) *) @@ -231,7 +264,7 @@ and tiebreak_by weights = rev %%> lex_list(fun x y -> | D x, D y | S x, S y | XD x, XD y | A(V x), A(V y) -> compare x y | X x, X y -> compare_mono_by weights x y | O x, O y -> lex_list(compare_var *** compare_poly_by weights) x y - | A(T x), A(T y) -> Term.compare x y + | A(T(x,_)), A(T(y,_)) -> Term.compare x y | _ -> assert false (* If xw=yw, variant constructors of x,y must be equal and they are covered above. *)) (* Assign this to set the global monomial order. Old polynomials become invalid when the order changes (because they are sorted by the monomial order) and must not be used afterwards. However polynomials stored in clauses can still be reretrieved (see poly_as_lit_term_id and poly_of_{lit,term,id}). The weights are effectively 0-extended and compared as “signed ordinals”. Trailing zeros do not matter. @@ -267,7 +300,8 @@ let rec poly_eq p = CCList.equal mono_eq p and mono_eq m n = m==n or CCList.equal indet_eq m n and indet_eq x y = x==y or match x,y with | C a, C b -> Z.equal a b - | A(T t), A(T s) -> t==s + | A(T(t,tv)), A(T(s,sv)) -> t==s & if tv=sv then true else + failwith("Term "^ Term.to_string t ^" must not be associated with both variables ["^ concat_view "] and [" (CCList.to_string((-^)"")) [tv;sv] ^"]") | X f, X g -> mono_eq f g | O f, O g -> CCList.equal(CCPair.equal (=) poly_eq) f g | a, b -> a = b @@ -280,8 +314,15 @@ and mono_hash ?(depth=2) = fold_left (fun h x -> 31*h + indet_hash ~depth x) 0 and indet_hash ?(depth=2) = if depth=0 then ~=7 else function | X f -> mono_hash ~depth:(depth-1) f | O f -> fold_left (fun h (i,fi) -> bit_rotate_right i (h + poly_hash ~depth:(depth-1) fi)) 0 f - | A(T t) -> Term.hash t + | A(T(t,_)) -> Term.hash t | x -> Hashtbl.hash x + +(* Hash table with polynomial keys *) +module Hashtable = Hashtbl.Make(struct + type t = poly + let equal = poly_eq + let hash p = poly_hash p +end) (* Auxiliarity to below. Separate the predicated indeterminates to coefficient polynomials. Inverse is given by p: (poly * op list)list ↦ p |> map(fun(c,m) -> c><[m]) |> fold_left(++)_0 *) @@ -299,7 +340,7 @@ let lead_main_ops = snd % hd % mul_coef_view (* e.g. [Y] from above *) (* Allows to compute e.g. ∑ₙᑉᵐ s.t. ∑ₙᑉᵐ(M·P) = -Pₘ + M·∑ₙᑉᵐP and ∑ₙᑉᵐ(N·P) = Pₘ - P₀ + ∑ₙᑉᵐP *) let rec fold_indeterminates a f = function | [] | [A I] -> a `I -| [A(T t)] -> a(`T t) +| [A(T(t,_))] -> a(`T t) | [A(V i)] -> a(`V i) | x::m -> f (fold_indeterminates a f m) [m] x (* x last => anonymous pattern match is possible *) @@ -307,12 +348,13 @@ let rec fold_indeterminates a f = function (* Pretty-printing string conversion *) (* TODO provide an association in an environment *) -let var_name = string_part_at "y x v u t s r p o n m l k j i h e a" +let var_name = string_part_at "y x v u t s r p o n m l k j i h e a" +let var_of_name n = index_of' n (String.split_on_char ' ' "y x v u t s r p o n m l k j i h e a") (* Mostly Term.to_string but when polynomials are embedded into terms which are in turn embedded into polynomials, confusion could arise. Hence in one of these two embeddings the names have to be annotated.  Currently I annotate at the embedding. This has the trade-off of making all polynomials in terms/clauses “ugly” but an embedded polynomial in a term in a polynomial does not need nested annotation. *) let term_name t = Term.to_string t -(* E.g. ["-2x";"3y";"-4z"] becomes "-2x＋3y－4z". (On Ubuntu command line “＋” has width 2 which seems nice balance between 1 of “+” and 3 of “ + ”, some times.) *) +(* E.g. ["-2x";"3y";"-4z"] becomes "-2x＋3y－4z". (The “＋” has width 2 (in my Ubuntu and Cygwin terminals) which seems nice balance between 1 of “+” and 3 of “ + ”, some times.) *) let concat_plus_minus view = function | [] -> "0" | m::p -> map view p @@ -327,14 +369,14 @@ and poly_view_string p = mul_coef_view p |> concat_plus_minus(function | c, m -> "("^ poly_to_string c ^")"^ match mono_to_string m with "1"->"" | s->s) and mono_to_string m = group_succ ~eq:indet_eq m - |> concat_view "" (fun n -> indet_to_string(hd n) ^ match length n with 1->"" | l -> superscript(string_of_int l)) - |> function ""->"1" | "-"->"-1" | "͘"->"1͘" | s->s + |> concat_view "" (fun n -> indet_to_string(hd n) ^ match length n with 1->"" | l -> superscript(""-^l)) + |> function ""->"1" | "-"->"-1" | "͘"->"1͘" | "-͘"->"-1͘" | s->s and indet_to_string = function | C a -> (match Z.to_string a with "1"->assert false | "-1"->"-" | s->s) | A I -> "͘" | A(V i) -> var_name i -| A(T t) -> term_name t +| A(T(t,v)) -> term_name t ^ concat_view"" (subscript%var_name) v | D i -> subscript(var_name i) | XD i -> "ð"^subscript(var_name i) | S i -> "∑"^superscript(var_name i) @@ -346,36 +388,50 @@ let pp_poly = to_formatter poly_to_string (* Embedding polynomials into terms - Equality is not preserved! This embedding is a convenient point to make polynomials aware of the monomial order that is varied between computations. When a polynomial is retrieved from a clause, it is resorted to conform to the current order, if necessary. *) + Equality is preserved (at the cost of ever growing polynomial->id cache). This embedding is a convenient point to make polynomials aware of the monomial order that is varied between computations. When a polynomial is retrieved from a clause, it is resorted to conform to the current order, if necessary. *) +let term_of_arg = function [[A(T(t,_))]] -> t | _->assert false +(* List of argument term monomials that the given recurrence contains, without duplicates. *) +let arg_terms_in = + sort_uniq~cmp:(term_of_arg %%> Term.compare) + % flat_map(fun m -> match rev m with (A(T _) as a)::_ -> [ [[a]] ] | _->[]) (* List of terms that the given recurrence relates, without duplicates. *) -let terms_in = sort_uniq ~cmp:Term.compare % flat_map(fun m -> match rev m with A(T t)::_->[t] | _->[]) +let terms_in = map term_of_arg % arg_terms_in + +let poly_id_cache = Hashtable.create 4 let term0 = Term.const ~ty:term (ID.make "⬮") exception RepresentingPolynomial of poly * Precedence.Weight.t * (simple_indeterminate -> int list) -(* Given polynomial P<>0, embed P into a fresh ID idP, that idP into a Term termP, and it into a literal term0≈termP. Return all three. - ~name is the name given to the idP. If omitted, the name is (somewhat wastefully) taken to be the string representation of P, which is further annotated to support nesting the terms back into polynomials and into terms again. - ~weight becomes the weight of idP in KBO. Default weight ω is large because the polynomial literals are expected to be the most expensive literals of a clause to process. Note: the weight assignment is separately informed about the embedded polynomials because the weight of an ID is not assigned on construction, and precedence is fixed at the same time. *) +(* Given polynomial P!=0, embed P into an ID idP, that idP into a Term termP, and it into a literal term0≈termP. Return all three. + ~name is the name given to the idP, if fresh is created. If omitted, the name is (somewhat wastefully) taken to be the string representation of P, which is further annotated to support nesting the terms back into polynomials and into terms again. + ~weight becomes the weight of idP in KBO, if fresh idP is created. Default weight ω is large because the polynomial literals are expected to be the most expensive literals of a clause to process. Note: the weight assignment is separately informed about the embedded polynomials because the weight of an ID is not assigned on construction, and precedence is fixed at the same time. *) let poly_as_lit_term_id ?name ?(weight=omega) p = - let id = ID.make(name |> get_lazy(fun()-> - (* Compute default name only if none is given. *) - let replace = fold_left (%) id % map(fun(old,by) -> global_replace (regexp old) by) in - let _name = poly_to_string p - |> replace ["＋","˖"; "－","−"; "-","−"] (* avoid ' ' around name *) - |> flip String.iter - (* |> Iter.filter(fun c -> not(mem c [' ';'(';')'])) *) - (* |> Iter.take 20 *) - (* I annotate by overlining here that has the benefit of not increasing visual length but the down side of being problematic to iterate. As all pretty-printing, this can be changed to fit other needs, should such arise. *) - |> Iter.to_string ~sep:"" (fun c -> - (if code c lsr 6 != 2 then "̅" else "") ^ String.make 1 c) - in String.sub (_name ^ "̅") 2 (String.length _name))) + let id = match Hashtable.find_opt poly_id_cache p with + | Some id -> id + | None -> let id = + ID.make(name |> get_lazy(fun()-> + (* Compute default name only if none is given. *) + let replace = fold_left (%) id % map(fun(old,by) -> global_replace (regexp old) by) in + let _name = poly_to_string p + |> replace ["＋","˖"; "－","−"; "-","−"] (* avoid ' ' around name *) + |> flip String.iter + (* |> Iter.filter(fun c -> not(mem c [' ';'(';')'])) *) + (* |> Iter.take 20 *) + (* I annotate by overlining here that has the benefit of not increasing visual length but the down side of being problematic to iterate. As all pretty-printing, this can be changed to fit other needs, should such arise. *) + |> Iter.to_string ~sep:"" (fun c -> + (if code c lsr 6 != 2 then "̅" else "") ^ String.make 1 c) + |> replace["̅̅","̲"](*<-TODO fix this hack*) + in String.sub (_name ^ "̅") 2 (String.length _name))) + in + ID.set_payload id (RepresentingPolynomial(p, weight, !indeterminate_weights)); + Hashtable.add poly_id_cache p id; + id in - ID.set_payload id (RepresentingPolynomial(p, weight, !indeterminate_weights)); let term = Term.const ~ty:term id in Literal.mk_eq term0 term, term, id -(* Includes semantics of 0 giving tautology unlike poly_as_lit_term_id. (Repeated calls still give incomparable literals.) *) +(* Includes semantics of 0 giving tautology unlike poly_as_lit_term_id. *) let polyliteral p = if p = _0 then mk_tauto else (fun(l,_,_)->l) (poly_as_lit_term_id p) (* Retrieve polynomial that was embedded into an id by poly_as_lit_term_id (directly or indirectly). The retrieved polynomial conforms to the current monomial order. *) @@ -392,13 +448,10 @@ let poly_of_id id = id |> ID.payload_find ~f:(fun data -> match data with (* 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 -(* Polynomial representing the given term. If the term already embeds a polynomial, result is that embedded polynomial, in order to avoid multilayer embeddings. TODO we should not need 3 term->polynomial conversions! *) -(* let of_term' t = get_or~default:[[A(T t)]] (poly_of_term t) *) - (* 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 -(* Weight of polynomial id. Used when registering the extension in summation_equality.ml to update the weight assignment to be aware of the embedded polynomials. *) +(* Weight of polynomial id. This is used when registering the extension in summation_equality.ml to update the weight assignment to be aware of the embedded polynomials. *) let polyweight_of_id = ID.payload_find ~f:(function RepresentingPolynomial(_,w,_) -> Some w |_->None) @@ -448,10 +501,10 @@ and indeterminate_product x y = | x, C k -> [[y;x]] | D i, X f -> [[X f; D i]] ++ x_[f] | XD i, X f -> [[X f; XD i]] ++ x_[f] - | D i, O f -> (if mem_assq i f then f else (i,[[A(V i)]])::f) (* identity ∘'s in f are implicit *) + | D i, O f -> (if mem_assq i f then f else (i,[var_poly i])::f) (* identity ∘'s in f are implicit *) |> map(fun(n,fn)-> x_ fn >< [o f @[D n]]) (* coordinatewise chain rule *) |> fold_left (++) _0 (* sum *) - | XD i, O f -> fold_left(++)_0 (map(fun(n,fn)-> (todo"X fn⁻¹") >< x_ fn >< [o f @[XD n]]) (if mem_assq i f then f else (i,[[A(V i)]])::f)) (* like previous *) + | XD i, O f -> fold_left(++)_0 (map(fun(n,fn)-> (todo"X fn⁻¹") >< x_ fn >< [o f @[XD n]]) (if mem_assq i f then f else (i,[var_poly i])::f)) (* like previous *) | D i, XD j when i=j -> [[XD i; D i]; [D i]] | O f, X g -> x_[g] >< [[O f]] | X(S i ::f), S j when i=j -> let _Si_Xf = [[S i]]><[[S i]]) ++ [[S i; X(S i :: f)]] ++ _Si_Xf @@ -463,13 +516,17 @@ and indeterminate_product x y = | O[i,[[C c; A I]]], S l when i=l -> Z.(if c < zero then map(fun n -> eval_at~var:i (of_int n + c)) (range' 0 (Stdlib.abs(to_int_exn c))) else map(fun n -> eval_at~var:i (of_int n)) (range' 0 (to_int_exn c))) - | O[i,[[A(V j)];[A I]]], O[l,[[A(V k)];[A I]]] when i=j & l=k & i>l -> [[y;x]] (* TODO composite case *) + | O[i,[[A(V j)];[A I]]], O[l,[[A(V k)];[A I]]] when i=j & l=k & i>l -> [[y;x]] + | O f, O g when is_multishift x & is_multishift y & rev_cmp_mono [x] [y] <0 -> [[y;x]] + | O f, O g when not(is_multishift x) -> [o(map(map_snd((><)[[x]]))(*∘f*)g @ filter(fun(i,_) -> not(mem i (map fst g)))(*implicit defaults*)f)] | D i, D l | XD i, XD l | S i, S l | X[A(V i)], X[A(V l)] when i>l -> [[y;x]] | X f, X g when rev_cmp_mono f g < 0 -> [[y;x]] (* Assumes commutative product! *) | X f, A _ when rev_cmp_mono f [y] < 0 -> mul_indet[[y]]><[f] (* Assumes commutative product! *) | D _, A I -> [] | D i, A(V n) -> const_eq_poly Z.(if i=n then one else zero) + | 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 _, y -> [[y;x]] (* Push A from left to right. Caller must push A fully right before _,A multiplication! *) | x, y -> [[x;y]] @@ -479,8 +536,9 @@ and eval_at' ~var p = o[var, p] and eval_at ~var at = eval_at' ~var (const_eq_poly at) and o subst = match subst |> map(map_snd(fun p -> if equational p then p else p>< const_eq_poly Z.one)) - |> filter(function i,[[A(V j)]] -> i!=j | _-> true) -with []->[] | s-> assert(for_all (equational%snd) s); [O s] + |> filter(function i,[[A(V j)]] -> i!=j | _-> true) + |> fun s-> sort_uniq~cmp:(fst %%> (-)) s, length s (* sort and check nonduplication *) +with [],_->[] | s,l-> assert(for_all (equational%snd) s & l = length s); [O s] (* Does [[x;y]] represent x·y. Equivalently is x≯y in the internal indeterminate order. *) let join_normalizes x y = match x,y with @@ -528,7 +586,7 @@ let (|~>) general special = match lead_unifiers general special with let superpose p p' = if p==p' then [] else - match lead_unifiers ~

[([u]> [] @@ -544,7 +602,7 @@ module LeadRewriteIndex(P: View with type v=poly) = FV_tree.FV_IDX(struct let compute_feature f p = match P.view p with Some p when p!=_0 -> Some(FV_tree.N(f p)) | _->None end) -(* Features for a rewriting index testing various sums of operator degrees. Only for <>0 polynomials. *) +(* Features for a rewriting index testing various sums of operator degrees. Only for !=0 polynomials. *) let default_features() = (* () because of type variables *) let sum value = sum_list % map value % hd in [(* TODO double check that these are correctly increasing *) @@ -573,10 +631,12 @@ and free_variables p' = Int_set.(let rec monoFV = function (* Do operators make explicit all implicit dependencies in argument terms? If not, below is wrong! *) | A(V i) | S i | D i | XD i -> singleton i | X f -> monoFV f - | A(T t) -> map_or ~default:empty free_variables (poly_of_term t) (* TODO properly track variables of a term *) + | A(T(_,v)) -> of_list v (*map_or ~default:empty free_variables (poly_of_term t)*) ) in union_map monoFV p') +let free_variables' = Int_set.to_list % 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<>[[A(V i)]] then (* identity variable mapping gets encoded by [||] always *) + if 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 @@ -618,21 +678,24 @@ let (@.) m (i,j) = if i >= Array.length m or m.(i)=[||] then if i=j then 1 else (* The input function produces polynomials, and its mapped version is a homomorphism. *) let map_monomials f = fold_left (++) _0 % map f let map_indeterminates f = map_monomials(product % map f) -let map_terms f = map_indeterminates(function A(T t) -> of_term(f t) | x -> [[x]]) +let map_terms ?(vars=id) f = map_indeterminates(function A(T(t,v)) -> of_term~vars:(vars v) (f t) | x -> [[x]]) + +(* 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 -> ( + match poly_of_term t with Some p when act_on p -> p +| _ -> [[x]]) | x -> [[x]]) (* Applicable after (mul_)coef_view. Pack separated (op list)'s into argument terms of polynomial except when they are already packed that way. *) let to_poly_poly: (poly * op list) list -> poly = fold_left (++) _0 % map(fun(coef, arg) -> coef >< match arg with - | [A(T t)] -> [arg] + | [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. *) - let _,t,_ = poly_as_lit_term_id [arg] in of_term t) + 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. *) let oper_coef_view: poly -> poly = to_poly_poly % coef_view(function | C _ | X[A(V _)] -> true - | O f -> let var_or_const = function [A(V _)] | [A I] | [C _; A I] -> true | _ -> false - in for_all(for_all var_or_const) (map snd f) - | _ -> false) + | x -> is_multishift x) (* Parsing polynomials from strings—primarily for testing *) @@ -656,7 +719,9 @@ let match_start(type r) ?(split=' ') patterns string = 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 (* To generate test data. No multidigit numerals. Terms e.g. b,c,f,g and variables e.g. n,m,k,x,y (must be compatible with var_name). Examples: Xx+3x-2 @@ -703,6 +768,18 @@ and poly_of_mono_string base_rules s' = if s'="" then _0 (* neutral in splitting let map_start_factor rules = match_start (map (fun(p,f)-> p, fun i s -> f i >< if s="" then [[]] (* neutral in this recursion *) else poly_of_mono_string base_rules s ) rules) s' in + (* This split_string by GPT 3.5 is quite impressive, only the loop could be reversed, while web search came out empty handed. *) + let split_string str = + let rec aux i acc = + if i < String.length str then + aux (i + 1) ((String.sub str i 1) :: acc) + else + List.rev acc + in + aux 0 [] in + let embedded_term i = + let t = get_at_idx_exn i testterms in + of_term t ~vars:((map var_of_name %split_string %String.concat"" %Hashtbl.find_all variable_dependency %Term.to_string) t) in map_start_factor(base_rules@[ ("y x v u t s r p o n m l k j i h e a",fun i->[[mul_var i]]); ("Y X V U T S R P O N M L K J I H E A",fun i->[[shift i]]); @@ -711,6 +788,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->of_term(get_at_idx_exn i testterms)); - ("B C F G Q Z",fun i->mul_indet(of_term(get_at_idx_exn i testterms))); + ("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/TypeTests.ml b/src/prover_phases/TypeTests.ml index 2c97448fd..32296e93f 100755 --- a/src/prover_phases/TypeTests.ml +++ b/src/prover_phases/TypeTests.ml @@ -1,9 +1,9 @@ (* A dynamic type test is a predicate 'a->bool. They work by traversing the term structure. Since types are erased, same data can have multiple types. But if a type test T on data X is succesful, then at least X can be (magic) cast to T safely. Safety means no segmentation fault but risks custom invariants. The below tests are accure in this sense, or preserve accuracy, except the unsafe tests integer/Z.t, rational/Q.t and lazy_or. There's no test combinators for polymorphic variants and exceptions—they can be accurately tested by pattern matching. - Currently this file contains all definitions of type tests and their associations to string printers. It is hence easy to disable this debugging by never registering the corresponding extension. Another design would be to scatter the type tests next to the corresponding real type definitions. That'd reduce the risk of forgetting to update a test along side its corresponding type. *) + Currently this file contains all definitions of type tests and their associations to string printers. It is hence easy to disable this debugging by never registering the corresponding extension. Another design would be to scatter the type tests next to the corresponding real type definitions. That'd reduce the risk of forgetting to update a test along side its corresponding type. Moreover, assumptions about the order of the associations—easily enforced only in a single file—are made and documented. *) open Logtk open Libzipperposition -open List +open CCList open Obj (* OCaml's reflection module—powers all of this *) open Util open Util.UntypedPrint @@ -192,7 +192,15 @@ and indeterminate x = union 0 [ [int]; [monomial]; [list(tuple[int;polynomial])]] x -and op_atom x = union 1 [[int]; [term]] x +and op_atom x = union 1 [[int]; [term; list int]] x + +(* Makes a type test that searches possible types among add_pp registered types. The made type test outputs true until there's no common type for the given inputs (except any). *) +let search_type() = + let with_any = registered_types() in + let possible = ref(take (length with_any - 1) with_any) in + fun x -> match filter ((|>)x) !possible with + | [] -> false + | p -> possible:=p; true (* Define and register string converters *) @@ -213,14 +221,27 @@ let digits_in style = String.(to_seq %> List.of_seq %> concat_view "" (function | '0'..'9' as d -> (if style=wide then "\xEF\xBC" else "\xF0\x9D\x9F") ^ make 1 Char.(chr(style + code d)) | c -> make 1 c)) +type printer = Printer: ('any -> string) -> printer +let add_homogeneous_and_any polytypes_printers = + let _= polytypes_printers |> map(fun(t, Printer p)-> add_pp (t any) p) in + let _= polytypes_printers |> map(fun(t, Printer p)-> add_pp (t(search_type())) p) in() + +let generic_variant_pp x = + superscript(str(size x)) (* Prepend length of data tuple for easier exploration. *) + ^ (match tag x with 0-> "" | t-> "tag" ^ str t) (* Omit multipurpose default tag 0. *) + ^ "("^ clever_view "," str (fields x) ^")" + + let extension = {Extensions.default with name = "debug type tests"; env_actions = [fun env -> let module Env = (val env) in -add_pp clause (CCFormat.to_string Env.C.pp_tstp); +add_pp clause (CCFormat.to_string Env.C.pp_tstp); +(* Keep int last to prioritize it over 0-parameter variants. *) +add_pp int string_of_int; ]};; -(* Do overly general assignments first so they end up to the bottom of the printer stack. Above env_actions run of course after this file. *) +(* Do overly general assignments first so they end up to the bottom of the printer stack. Above env_actions run of course after below assignments. It is assumed that add_pp any is the first and add_pp int is the last registration which must be enforced separately if one plans to register a printer in another file. *) add_pp any (fun x -> (match tag x with | t when t=final_tag -> "final" @@ -229,26 +250,25 @@ add_pp any (fun x -> (match tag x with | _ -> "tag="^str(tag x) )^":size="^str(size x)); -add_pp (test 0 (fun(tag,_) -> tag < no_scan_tag)) (fun x -> - superscript(str(size x)) (* Prepend length of data tuple for easier exploration. *) - ^ (match tag x with 0-> "" | t-> "tag" ^ str t) (* Omit multipurpose default tag 0. *) - ^ "("^ clever_view "," str (fields x) ^")"); +add_pp (test 0 (fun(tag,_) -> tag < no_scan_tag)) generic_variant_pp; -add_pp (ccvector any) (CCVector.to_string ~start:"ᵛᵉᶜ⟨" ~stop:"⟩" str); +add_pp (lazy_or(fun _->false)) (fun _->"lazy"); +(* already evaluated lazy values *) +add_pp (test_tag forward_tag any) (str % Lazy.force); -add_pp (list any) (fun l -> "["^ clever_view ";" str l ^"]"); +add_homogeneous_and_any[ + array, Printer generic_variant_pp; + + ccvector, Printer(CCVector.to_string ~start:"ᵛᵉᶜ⟨" ~stop:"⟩" str); -add_pp (ccset any) ( - let rec to_list s = if s == repr 0 then [] else to_list(field s 0) @ field s 1 :: to_list(field s 2) in - fun s -> "{"^ clever_view "," str (to_list s) ^"}"); + list, Printer(fun l -> "["^ clever_view ";" str l ^"]"); -add_pp (hashtbl any any) Hashtbl.(fun t -> "{"^if length t = 0 then "↦̸ }" else - clever_view ";" (fun(k,v)-> str k ^"↦ "^ str v) (List.of_seq(to_seq t)) ^"}"); + ccset, Printer(let rec to_list s = if s == repr 0 then [] else to_list(field s 0) @ field s 1 :: to_list(field s 2) + in fun s -> "{"^ clever_view "," str (to_list s) ^"}"); -(* already evaluated lazy values *) -add_pp (test_tag forward_tag any) (str % Lazy.force); - -add_pp (lazy_or(fun _->false)) (fun _->"lazy"); + flip hashtbl any, Printer Hashtbl.(fun t -> "{"^if length t = 0 then "↦̸ }" else + clever_view ";" (fun(k,v)-> str k ^"↦ "^ str v) (List.of_seq(to_seq t)) ^"}"); +]; (* The infix_tag is for mutually recursive functions acording to a comment on https://github.com/ocaml/ocaml/issues/7810 *) add_pp (test 0 (fun(tag,_) -> tag=closure_tag or tag=infix_tag)) (fun f -> @@ -277,10 +297,10 @@ add_pp exception' Printexc.(fun e -> "("^ clever_view "," str (tl(fields e)) ^")" else ""); -add_pp decimal string_of_float; -(* Quote number and invisible strings. *) -add_pp string (fun s -> if None != int_of_string_opt(String.trim s ^ "0") then "“"^s^"”" else s); -(* Do not print list [term] as SLiteral ¬term. *) +add_pp decimal string_of_float; +(* Quote number and invisible strings. *) +add_pp string (fun s -> if None != int_of_string_opt(String.trim s ^ "0") then "“"^s^"”" else s); +(* Do not print a singleton list [term] as SLiteral ¬term. *) add_pp (fun x -> sliteral term x & not(list any x)) ((^)"ᔆᴸⁱᵗ" % SLiteral.to_string Term.pp); add_pp tvar HVar.to_string; add_pp subst Subst.to_string; diff --git a/src/prover_phases/summation_equality.ml b/src/prover_phases/summation_equality.ml index 8168df2ed..2dff36d95 100755 --- a/src/prover_phases/summation_equality.ml +++ b/src/prover_phases/summation_equality.ml @@ -58,7 +58,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 p l = fst(get_exn(find_idx p l)) +let index_of = RecurrencePolynomial.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 @@ -235,17 +235,22 @@ let make_polynomial_environment indeterminate_weights = let saturate_with_order = snd % make_polynomial_environment -(* Filter eligible non-trivial polynomial recurrences by the given condition. *) -let filter_recurrences ok_poly = Iter.filter(fun c -> - fold_lits ~eligible:(C.Eligible.res c) (C.lits c) - |> Iter.exists R.(fun(l,_) -> match poly_of_lit l with - | Some p -> p!=_0 & ok_poly p - | _ -> false)) +(* Drop None's after mapping eligible non-trivial polynomial recurrences by the given transformation. *) +let filter_map_recurrences map_poly = Iter.filter_map(fun c -> + try Some(make_clause~parents:[c] (fold_lits ~eligible:(C.Eligible.res c) (C.lits c) + |> Iter.map R.(fun(l,_) -> match poly_of_lit l with + | Some p when p!=_0 -> + let p' = get_exn(map_poly p) (* exception catched *) + in if poly_eq p' p then l else let l',_,_ = poly_as_lit_term_id p' in l' + | _ -> l) + |> 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. *) -let filter_recurrences_of polylist = filter_recurrences R.(fun p -> match terms_in[hd p] with +(* 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) + | _ -> false +) (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 = @@ -254,6 +259,13 @@ 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 @@ -281,16 +293,15 @@ let rec propagate_recurrences_to f = match PolyMap.find_opt recurrence_table f w PolyMap.add recurrence_table f r; r -(* Recurrences of term. If it embeds polynomial, apply propagation. *) -and recurrences_of_term t = propagate_recurrences_to R.(get_or~default:(of_term t) (poly_of_term t)) - and propagate_oper_affine p's_on_f's = let _,result,_ = R.poly_as_lit_term_id p's_on_f's in let pf_sum = R.oper_coef_view p's_on_f's in - let f's = R.terms_in pf_sum in - Iter.of_list(flat_map recurrences_of_term f's) - |> 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) f's)) + R.arg_terms_in pf_sum + |> 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)) + |> 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] and propagate_times f g = @@ -302,7 +313,7 @@ and propagate_times f g = map(map_poly_in_clause(fun r -> mul_indet f><[rename]> Iter.of_list disjoint_recurrences - (* 3. propagate to substitution σ(f·ϱg) when σ<>id *) + (* 3. propagate to substitution σ(f·ϱg) when σ!=id *) | [O m] -> let f_x_g' = R.(mul_indet f><[rename]>< g) in PolyMap.add recurrence_table f_x_g' disjoint_recurrences; @@ -317,14 +328,15 @@ and propagate_sum i f = |`O[u, R.[[A(V v)];[A I]]] when v=u -> [] | _ -> [1] in - let sumf = let _,sumf,_ = R.(poly_as_lit_term_id([[S i]]> 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]]> 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. *) + (* Add the definitional N∑ᑉⁿf = ∑ᑉⁿf + fₙ with sumf embedded while f needs not to be. *) |> Iter.cons(definitional_poly_clause R.(([[shift i]]> filter_recurrences_of R.[ [[S i]]> true | _ -> false in - let _,f_term,_ = R.(poly_as_lit_term_id f) in + let _,f_term,_ = R.poly_as_lit_term_id f in let _,sf_term,_ = R.(poly_as_lit_term_id([o s]> Int_set.mem v dom) s in (* => domain of s ⊆ dom ...necessary? - What'd be the variables of just a term? They'd have to be assigned somewhere (TODO) or maybe they are not needed so for now try to ignore them. *) + let s = filter (fun(v,_)-> Int_set.mem v dom) s in (* => domain of s ⊆ dom ...necessary? *) match R.view_affine s with | None -> Iter.empty | Some(m,a) -> @@ -348,7 +358,7 @@ and propagate_subst s f = let multishifts_and_equations = changedShift(Int_set.to_list(R.rangeO s)) |> map R.(fun j -> 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, const_eq_poly(Z.of_int(m@.(i,j)))))) in + 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); let eq_j = product(on_dom(fun i -> pow' poly_alg [[shift i]] (max 0 (m@.(i,j))))) @@ -364,16 +374,18 @@ and propagate_subst s f = | _ -> 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 f_term 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') when CCOpt.equal poly_eq (Some f) (poly_of_term f') -> of_term sf_term - | A(T t) when HT.mem cache_t_to_st t -> of_term(HT.find cache_t_to_st t) - | A(T t) -> let _,st,_ = poly_as_lit_term_id([o s] >< get_or~default:(of_term t) (poly_of_term t)) in - HT.add cache_t_to_st t st; of_term st + | 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. *) @@ -382,12 +394,13 @@ and propagate_subst s f = | 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) + with Exit -> None) + |> filter_recurrences_of[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. *) let declare_recurrence r = add_new_rec - R.(of_term(max_list ~ord:Term.compare (terms_in r))) + R.(max_list ~ord:(term_of_arg%%>Term.compare) (arg_terms_in r)) (definitional_poly_clause r) let sum_equality_inference clause = @@ -399,22 +412,24 @@ let sum_equality_inference clause = let eq0 ss = eq0' R.[fold_left (++) _0 (List.map(fun cmt -> let c,mt = split_or '.' "1" (String.trim cmt) in let m,t = split_or '\'' "" mt in - Z.of_string c *: poly_of_string m >< of_term(have t [] int) + 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"; propagate_recurrences_to !"nf"; (* OK *) propagate_recurrences_to !"g+f"; (* OK *) propagate_recurrences_to !"g+nf"; (* diverge? *) - propagate_recurrences_to !"{ⁿm}∑ⁿ{ᵐm-n}b - ∑ᵐb"; propagate_recurrences_to !"∑ᵐb"; (* OK *) *) - propagate_recurrences_to !"{ᵐm-n}b"; (* OK *) - propagate_recurrences_to !"∑ⁿ{ᵐm-n}b"; (* missing M-rule *) - (* propagate_recurrences_to !"{ⁿm}∑ⁿ{ᵐm-n}b"; (* errors: {ᵐm-n} vs {ᵐ-n+m}; rec. with N is very wrong *) - *) + 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 *) + ~ raise(Invalid_argument("var_index "^str term^" ∉ "^str!coords)) - -(* Try to separate non-trivial eligible recurrence and the rest of the literals from the given clause. *) -let view_poly_clause c = fold_lits ~eligible:(C.Eligible.res c) (C.lits c) - |> Iter.find R.(fun(l,_)-> match poly_of_lit l with - | Some p when p!=_0 -> Some(p, CCArray.filter((!=)l) (C.lits c)) - | _ -> None) - -(* Filter those clauses that have eligible polynomial with leading term M t where some monomial M operates on an OK term t. *) -let filter_recurrences_of ok_term = filter_recurrences R.(fun p -> match terms_in[hd p] with [t] -> ok_term t |_->false) - -let is_summation s = match view s with -| Const{name="sum"} -> true -| _ -> false - -let to_Z t = match view t with -| AppBuiltin(B.Int z, []) -> z -| AppBuiltin(B.Rat q, []) -> Q.(let z = to_bigint q in if equal q (of_bigint z) then z else raise Exit) -| _ -> raise Exit -let is_Z t = try snd(to_Z t, true) with Exit -> false -let to_int = Z.to_int_exn % to_Z - -type encoding_phase_info = {coords: term list; symbols: term list; specialise: term HV.t} - -let _Z a = app_builtin ~ty:int (Int a) [] -let _z = _Z % Z.of_int -let trivC = make_clause[Literal.mk_tauto] ~=Proof.Step.trivial -let feed = MainEnv.FormRename.get_skolem ~parent:trivC ~mode:`SkolemRecycle - -let rec ev t = match view t with -| AppBuiltin(B.Sum, [_; x; y]) -> - let x, y = ev x, ev y in - (try _Z Z.(to_Z x + to_Z y) - with Exit -> app_builtin ~ty:int B.Sum [of_ty int; x; y]) -| AppBuiltin(B.Difference, [_; x; y]) -> - let x, y = ev x, ev y in - (try _Z Z.(to_Z x - to_Z y) - with Exit -> app_builtin ~ty:int B.Difference [of_ty int; x; y]) -| AppBuiltin(B.Product, [_; x; y]) -> - let x, y = ev x, ev y in - (try _Z Z.(to_Z x * to_Z y) - with Exit -> app_builtin ~ty:int B.Product [of_ty int; x; y]) -| App(s,[m;f]) when is_summation s & is_Z(ev m) -> - ev R.(fold_left (fun adds j -> app_builtin ~ty:int B.Sum [of_ty int; adds; f@<[j]]) (_z 0) (init (1+to_int(ev m)) _z)) -| App(f,p) -> app (ev f) (map ev p) -| Fun(ty,b) -> fun_ ty (ev b) -| _ -> t -(* The only two uses of ev. *) -and (@<) g = ev % Lambda.whnf_list g -let (=:) by old = ev % replace ~old ~by - -let no_plus = map(fun s -> match view s with -| AppBuiltin(B.Sum, [_;x;y]) when is_Z x -> y -| AppBuiltin(B.Sum, [_;x;y]) when is_Z y -> x -| AppBuiltin(B.Difference, [_;x;y]) when is_Z y -> x -| _ -> s) - -(* Explicit integer constant or simple constant suitable as a coordinate variable. *) -let is_atom t = is_Z t or ty t == int & match view t with -| Const _ -> true -| App(f,x) -> for_all is_Z x -| _ -> false - -let is_free t = ty t ==int & is_var t - -let recurrence_table = HT.create 32 -let add_recurrence t r = HT.add recurrence_table t (r :: get_or ~default:[] (HT.find_opt recurrence_table t)) - -let rec term_to_poly info t = - if ty t != int then raise Exit; - match view t with - | AppBuiltin(B.(Sum|Difference) as op, [_;x;y]) -> - R.(if op=B.Sum then (++) else (--)) (term_to_poly info x) (term_to_poly info y) - | AppBuiltin(B.Product, [_;c;x]) -> R.(try const_op_poly(to_Z c) >< term_to_poly info x - with Exit -> if is_atom c - then [[mul_var(var_index c)]] >< term_to_poly info x - else R.of_term t) - | AppBuiltin(B.Int n, _) -> R.const_eq_poly n (* or const_op_poly? *) - | _ when memq t info.coords -> [[R.mul_var(var_index t)]] - | App(f,p) when exists (Unif.FO.matches ~pattern:(f @< no_plus p)) info.symbols -> - to_iter info.symbols (fun s -> try - Unif.FO.matching_same_scope ~scope:0 ~pattern:(f @< no_plus p) s - |> Subst.iter(fun (v,_) (b,_) -> HV.add info.specialise (cast_var_unsafe v) (of_term_unsafe b)) - with Unif.Fail -> ()); - R.of_term t - | App(f,p) when for_all(flip memq info.coords) p -> - R.of_term t - | _ -> raise Exit - -let equation_to_recpoly info literal = match to_form literal with SLiteral.Eq(t,s) -> - (try Some R.(term_to_poly info t -- term_to_poly info s) - with Exit -> None) -|_->None - -(* Associate the clause as a recurrence polynomial to appropriate terms. To be used in initialization. *) -let register_if_clause_is_recurrence info clause = - let v_id t = index_of ((==)t) info.coords in - fold_lits ~eligible:(C.Eligible.res clause) (C.lits clause) Subst.(fun(lit,place)-> - equation_to_recpoly info lit |> CCOpt.iter List.(fun p -> - let pair_with (v:Term.var) (x:Term.t) : var Scoped.t * term Scoped.t = ((v:>var),0), ((x:>term),0) in - let substs = HV.to_seq_keys info.specialise - |> of_seq_rev - |> sort_uniq(HVar.compare Type.compare) - |> map_product_l(fun v -> map(pair_with v) (sort_uniq Term.compare (HV.find_all info.specialise v))) - (* when specialising, do not duplicate variables *) - |> filter(fun l -> length l = length(sort_uniq(fst%snd %%> InnerTerm.compare) l)) - |> map of_list in - substs |> iter R.(fun s -> - let s' t = of_term_unsafe(apply (Renaming.create()) s ((t:Term.t:>term),0)) in - ignore(v_id,s'); (* silence unusedness *) - let sp = todo"substitution to shifts"(* R.map_terms s' p - |> map_monomials(fun(c,m,s)-> let m=copy m in [c, m, match s with - | Shift(z,g) -> - let z = copy z in - let rec correct_shift h = match view h with - | App(f,p) -> f @< (p |> map(fun t -> match view t with - | AppBuiltin(B.Sum, [_;x;y]) when is_Z x -> - z.(v_id y) <- to_int x; y - (* symmetric copy *) - | AppBuiltin(B.Sum, [_;y;x]) when is_Z x -> - z.(v_id y) <- to_int x; y - | AppBuiltin(B.Difference, [_;y;x]) when is_Z x -> - z.(v_id y) <- - to_int x; y - | _ -> t)) - (* TODO h is a possibly shifted term in polynomial. Just wish here that shifts are not present! *) - | AppBuiltin(B.Product, [_;c;x]) when is_Z c -> todo"" - | AppBuiltin(B.Product, [_;c;x]) when is_atom c -> - m.(v_id c) <- 1+m.(v_id c); - correct_shift x - | _ -> h in - Shift(z, correct_shift(s' g)) - | s -> s]) *)in - terms_in sp |> iter(flip add_recurrence (replace_lit_by_poly clause place sp))))) - - -(* * The structure following propagation steps—large mutually recursive block. * *) -let rec recurrences_of t = match HT.find_opt recurrence_table t with -| Some r -> r -| None -> - let r = Iter.to_rev_list(match view t with - | AppBuiltin(B.Sum, [_;x;y]) -> propagate_affine x y t - | AppBuiltin(B.Difference, [_;x;y]) -> propagate_affine x ~coef2:Z.minus_one y t - (* TODO symmetric copy *) - | AppBuiltin(B.Product, [_;x;y]) when is_Z x -> propagate_affine ~coef1:(to_Z x) x (_z 0) t - | AppBuiltin(B.Product, [_;x;y]) when is_atom x -> todo"atom" - | AppBuiltin(B.Product, [_;x;y]) -> propagate_times x y t - | App(s,[m;f]) when is_summation s -> - if memq (feed f) !coords then - propagate_sum m (var_index(feed f)) (f@<[feed f]) t - else( - print_endline("Out of coordinates with "^ str t); - Iter.empty) - | _ -> Iter.empty) - in - HT.add recurrence_table t r; - r - -and propagate_affine ?(coef1=Z.one) t ?(coef2=Z.one) s t_plus_s = - let env, saturate = make_polynomial_environment(R.elim_oper_args[t,2; s,2; t_plus_s,1]) in - let poly x = R.(if is_Z x then const_eq_poly(to_Z x) - else if memq x !coords then [[mul_var(var_index x)]]>< const_eq_poly Z.one - else of_term x) in - Iter.of_list(recurrences_of t @ recurrences_of s) - |> Iter.cons(definitional_poly_clause R.(of_term t_plus_s -- coef1*: poly t -- coef2*: poly s)) - |> saturate - |> filter_recurrences_of((==)t_plus_s) - -and propagate_times t s t_x_s = - let env, saturate = make_polynomial_environment(R.elim_oper_args[t,2; s,2; t_x_s,1]) in - let init_recurrences = Iter.of_list(recurrences_of t @ recurrences_of s) - |> saturate - |> filter_recurrences_of(fun x -> x==t or x==s) - in - init_recurrences - |> Iter.cons(definitional_poly_clause R.(of_term t_x_s -- (mul_indet(of_term t) >< of_term s))) - |> saturate - |> filter_recurrences_of((==)t_x_s) - -and propagate_sum set sum_var s sum = - let bad = ref[] in - (* let nice = ref true in *) - let sum_blocker = function - |`T t when t != s -> [] - (* |`V v when v=sum_var -> [1] *) - |`V v when v!=sum_var -> [] - |`O[v, R.[[A(V w)];[A I]]] when v=w -> (try fst([], (if v=sum_var then near_bijectivity_error else near_commutation_error v) set sum_var) - with Exit -> [1]) - | _ -> [1] - in - let env, saturate = make_polynomial_environment sum_blocker in - (* Note: Unfortunately post-saturation processing here reveals all the structural details of recurrence polynomials and so violates encapsulation. *) - let rec_of_sum_with_bad_terms = Iter.of_list(recurrences_of s) - |> saturate - (* Remove recurrences from which it was not possible to eliminate the blocking indeterminates. *) - (* |> filter_recurrences R.(fun p -> fold_coordinates true (fun pass v -> - pass & for_all(function - | _, m, One -> true - | _, m, Shift(s,f) -> 0 = m.(v)*sum_fobic(`Mul,v,f) + s.(v)*sum_fobic(`Shift,v,f) - | _ -> false - )p)) *) - |> Iter.map R.(fun c -> - (* Above filtering ⟹ get_exn OK *) - let p, lits = get_exn(view_poly_clause c) in - (* let p' = - (* Eliminate shifts w.r.t. summation variable. *) - let e = near_bijectivity_error set sum_var in - let r,q = substitute_division sum_var s p in - e q ++ r - (* Pull out shifts w.r.t. all remaining variables. Multipliers get pulled out implicitly. *) - |> flip fold_coordinates (fun p v -> p |> map_monomials(function - | c, m, Shift(z,t) as cmZt -> - let e = near_commutation_error v set sum_var in - (* Cut z into two at v. Important to get ∑ₙMK - MK∑ₙ = eᴹK + Meᴷ right. *) - let outZ, inZ = power0(), power0() in - blit z 0 outZ 0 v; - blit z v inZ v (!coordinate_count - v); - (* c m outZ Vᵃ inZ t ↦ ∑ᵢ₊ⱼ₌ₐ₋₁ c m outZ Vʲ e(Vⁱ inZ t) *) - cmZt :: concat(init z.(v) (fun j -> - substiply (c, m, Shift((v|->j) outZ, t)) (e [Z.one, power0(), Shift((v|->z.(v)-1-j) inZ, t)]))) - | other -> [other] - )) - (* Replace s by sum=∑s, and record excess terms to eliminate later. *) - |> map_monomials(fun(c,m,z) -> [c, m, match z with - | One -> todo "∑m over the set" - | Shift(z,s') when s'==s -> Shift(z,sum) - (* TODO Variables may not escape. Can we some times eliminate f? If so, this is incomplete. Now try to copy summation from the given term to f. *) - | Shift(z,f) when Term.subterm ~sub:(var_term sum_var) f -> - (match view sum with App(sum,[set;_]) -> - let new_var = HVar.fresh ~ty:(ty s) () in - Shift(z, app sum [set; fun_of_fvars [new_var] ((var new_var =: var_term sum_var) f)]) - | _ -> assert false) - (* | Diagonal(_,_,_,s') when s'==s -> nice:=false; z *) - | Shift(_,f) | Diagonal(_,_,_,f) -> bad:= add_nodup ~eq:(==) f !bad; z - (* | _ -> z]) *) - | _ -> assert false]) - in *) - make_clause (R.polyliteral p :: to_list lits) ~parents:[c] - Proof.(Step.inference ~rule:(Rule.mk "pull recurrence out of sum")) - ) - (* Force the iteration through to decide necessity of resaturation. *) - |> Iter.persistent in - if !bad=[] then rec_of_sum_with_bad_terms else( - let _,resaturate = make_polynomial_environment(R.elim_oper_args((sum,1)::map(fun f -> f,2)!bad)) in - Iter.of_list(flat_map recurrences_of !bad) - (* Iter.of_list(recurrences_of s) *) - |> Iter.append rec_of_sum_with_bad_terms - |> resaturate - ) - (* |> filter_recurrences R.(fun r -> - exists(function _,_,Shift(_,sm) when sm==sum ->true | _->false) r - & for_all(function _,_,Shift(_,t) when subterm ~sub:(var_term sum_var) t ->false | _->true) r) *) - -(* TODO With only exclusive upper bound now: ∑ᑉᵐ(N-1) = @ᵐ-@⁰ *) -and near_bijectivity_error set var = near_either_error var set var -(* TODO With only exclusive upper bound: ∑ᑉᵐM-M∑ᑉᵐ = -@ᵐ *) -and near_commutation_error v = near_either_error v - -and near_either_error = - let eq ((v,s),n) ((v',s'),n') = v=v' & s==s' & n=n' in - (* Note: this has hit assertion failure with lru cache. *) - with_cache_3 (replacing 32 ~eq) ~=R.(fun op_var set sum_var -> - (* TODO actually deduce end_points by superposition from op_var, set, sum_var *) - let end_points = - let set, base = match view set with - | AppBuiltin(B.Sum, [_;y;x]) when is_Z y -> - x, to_int y - | AppBuiltin(B.(Sum|Difference) as op, [_;x;y]) when is_Z y -> - x, to_int y * if op = B.Sum then 1 else -1 - | _ -> set, 0 - in - if base < -1 then todo"base<-1"; - if op_var = sum_var then [1,1,`Dup(var_index set); -1,1,`None] - else if op_var = var_index set then [-1,1+base,`Dup op_var] - else [] - in end_points|>todo"near errors") - (* map_monomials(fun(c,m,s) -> - assert(m.(sum_var)=0); (* those must be eliminated before these errors are meaningful. *) - match s with - | One -> _0 - | Shift(s,f) -> end_points |> flat_map(fun(sign, base, scale) -> - let c = Z.( * ) (Z.of_int sign) c in - match scale with - (* (±1,b,None) represents ±[sum_var:=b] *) - |`None -> [c, m, Shift((sum_var|=>0) s, (_z base =: var_term sum_var) f (*sum_var↦base*))] - (* (±1, b, Dup v) represents ±Vᵇ{sum_var↦v} where commuting Vᵇ duplicates it *) - |`Dup var -> - [c, m, if subterm ~sub:(var_term var) f - then Diagonal(sum_var, var, (var|+>base) ((sum_var|+>base) s), f) - else Shift((var |-> s.(sum_var)+base) ((sum_var|=>0) s), (var_term var =: var_term sum_var) f)] - | _ -> todo"") - | _ -> assert false)) *) - - -let step text parents lits = - make_clause ~parents lits (fun parent_proofs -> if parents=[] - then (if text="goal" then Proof.Step.goal' else Proof.Step.assert') ~file:"" ~name:text () - else Proof.Step.inference ~tags:[] ~rule:(Proof.Rule.mk text) parent_proofs) - - -let sum_equality_inference' clause = - fold_lits ~eligible:(C.Eligible.res clause) (C.lits clause) - |> Iter.find(fun(lit, place) -> - (* Top-level ∑ must exist. *) - if Literal.fold (fun ok t -> ok or match view t with App(s,_) -> is_summation s | _->ok) false lit - then match to_form lit with SLiteral.Neq(lhs,rhs) -> - let main_expr = app_builtin ~ty:int B.Difference [of_ty int; lhs; rhs] in - (* TODO better initialization *) - let open Term.Set in - let coord_set, sym_set = ref empty, ref empty in - let rec walk t = if not(is_Z t) & ty t == int then - if is_atom t then coord_set <:> add t - else match view t with - | AppBuiltin(B.(Sum|Difference|Product), [_;x;y]) -> walk x; walk y - | App(s, [m;f]) when is_summation s -> walk m; walk(f@<[feed f]) - | App(f,x) -> List.iter walk x; if List.for_all is_atom x then sym_set <:> add t - | _ -> () - in - walk main_expr; - (* R.coordinate_count := cardinal !coord_set; *) - get_clauses(module MainEnv) (fun c -> c|>register_if_clause_is_recurrence{ - coords = to_list !coord_set; - symbols = to_list !sym_set; - specialise = HV.create 4}); - coords := to_list !coord_set; - (* Add constant recurrences (form Vfₓ-fₓ=0) for all coordinates that atoms (form App(f,x)) lack. *) - to_iter !sym_set (fun s -> match view s with App(_,x) -> - to_iter(diff !coord_set (of_list x)) (fun v -> add_recurrence s R.( - let v_const = ([[shift(var_index v)]] -- const_op_poly Z.one) >< of_term s in - make_clause [R.polyliteral v_const] ~=Proof.(Step.inference [] ~rule:(Rule.mk "constantness")))) - |_-> assert false); - let r = recurrences_of main_expr in - print_endline("Refuting "^ str lit); - print_endline "Final recurrences:"; - List.iter (print_endline%str) r; - (* Some[step "" (r) []] *) - print_endline "————— summation_equality: Missing induction phase => terminated —————"; - exit 1 - |_->None - else None) - |> get_or ~default:[] - (* Setup to do when MakeSumSolver(...) is called. *);; (* MainEnv.add_unary_inf "test" test_hook; *)