Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

First try at factoring saturation polynomials #240

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions benchmarking/IdentifiableFunctions/experiments.jl
Original file line number Diff line number Diff line change
Expand Up @@ -988,14 +988,15 @@ begin
)

using Nemo, Logging
using JuliaInterpreter
Groebner = StructuralIdentifiability.Groebner
# ParamPunPam = StructuralIdentifiability.ParamPunPam
Base.global_logger(ConsoleLogger(Logging.Info))
end

dennums, ring =
StructuralIdentifiability.initial_identifiable_functions(Pivastatin, p = 0.99);
res = StructuralIdentifiability.find_identifiable_functions(CGV1990);

res = StructuralIdentifiability.assess_identifiability(CGV1990);

fracs = StructuralIdentifiability.dennums_to_fractions(dennums);

rff = StructuralIdentifiability.RationalFunctionField(dennums);
Expand Down
98 changes: 72 additions & 26 deletions src/RationalFunctionFields/IdealMQS.jl
Original file line number Diff line number Diff line change
Expand Up @@ -25,14 +25,16 @@ mutable struct IdealMQS{T} <: AbstractBlackboxIdeal
# NB: this lists may have different length
nums_qq::Vector{T}
dens_qq::Vector{T}
sat_qq::T
sat_qq::Vector{T}
# dens_indices[i] is a pair of form (from, to).
# Denominator as index i corresponds to numerators at indices [from..to]
dens_indices::Vector{Tuple{Int, Int}}
# Indices of pivot elements for each component of funcs_den_nums
pivots_indices::Vector{Int}
den_lcm::T
# Saturation
sat_var_index::Int
sat_var_count::Int
# Numerators and denominators over GF.
# We cache them and maintain a map:
# a finite field --> an image over this finite field
Expand All @@ -46,16 +48,26 @@ mutable struct IdealMQS{T} <: AbstractBlackboxIdeal
"""
IdealMQS(funcs_den_nums::Vector{Vector})

Given an array of polynomials, that is generators of form
Given an array of polynomials, that is generators of the form

[[f1, f2, f3, ...], [g1, g2, g3, ...], ...]

constructs an MQS ideal.
constructs the corresponding MQS ideal.

## Options

This constructor takes the following optional arguments:
- `sat_varname`: a string, name of the saturation variable.
- `sat_var_position`: a symbol, position of the saturation variable in the
monomial ordering. Possible options are `:first` and `:last`.
- `ordering`: a symbol, monomial ordering.
- `sat_factorize`: a bool, if the saturating `Q(y)` should be factored.
"""
function IdealMQS(
funcs_den_nums::Vector{Vector{PolyQQ}};
sat_varname = "t",
sat_var_position = :first,
sat_factorize = true,
ordering = :degrevlex,
) where {PolyQQ}
# We are given polynomials of form
Expand Down Expand Up @@ -102,7 +114,6 @@ mutable struct IdealMQS{T} <: AbstractBlackboxIdeal
@debug "Saturating variable is $sat_varname, index is $sat_var_index"
flush(stdout)
R_sat, v_sat = Nemo.PolynomialRing(K, varnames, ordering = ordering)
# Saturation
t_sat = v_sat[sat_var_index]
den_lcm_orig = den_lcm
den_lcm = parent_ring_change(
Expand All @@ -111,8 +122,32 @@ mutable struct IdealMQS{T} <: AbstractBlackboxIdeal
matching = :byindex,
shift = Int(sat_var_index == 1),
)
# Construct the saturating polynomial Q(x) * t - 1.
# If `sat_factorize` is true, then factorize Q(x).
den_lcm_sat = parent_ring_change(den_lcm, R_sat)
sat_qq = den_lcm_sat * t_sat - 1
den_lcm_sat = divexact(den_lcm_sat, leading_coefficient(den_lcm_sat))
@assert isone(leading_coefficient(den_lcm_sat))
sat_qq = Vector{PolyQQ}()
# TODO: in addition to these cases, also do not factor the saturation
# polynomial when the ideal contains a single polynomial plus saturaton
# (this case is the most frequent one)
if !sat_factorize || isone(den_lcm_sat)
push!(sat_qq, den_lcm_sat * t_sat - 1)
else
fact_qq = Nemo.factor(den_lcm_sat)
# Potentially extend the ring with more variables for saturation
sat_varnames = map(i -> "$sat_varname$i", 1:length(fact_qq))
varnames = append_at_index(ystrs, sat_var_index, sat_varnames)
@debug "Saturating variables are $sat_varnames, index is $sat_var_index"
R_sat, v_sat = Nemo.PolynomialRing(K, varnames, ordering = ordering)
t_sat_many = v_sat[sat_var_index:(sat_var_index + length(sat_varnames) - 1)]
for ((sat_qq_factor, deg), sat_var_i) in zip(fact_qq, t_sat_many)
sat_qq_factor = parent_ring_change(sat_qq_factor, R_sat)
push!(sat_qq, sat_qq_factor^deg * sat_var_i - 1)
end
end
sat_var_count = length(sat_qq)
@info "Degrees of saturating polynomials are $(map(total_degree, sat_qq))"
# We construct the array of numerators nums_qq and the array of
# denominators dens_qq. Since there are usually more unique numerators
# than denominators, we condense the array dens_qq and produce an
Expand All @@ -129,7 +164,7 @@ mutable struct IdealMQS{T} <: AbstractBlackboxIdeal
den,
R_sat,
matching = :byindex,
shift = Int(sat_var_index == 1),
shift = sat_var_count * (sat_var_index == 1),
)
push!(dens_qq, den)
push!(dens_indices, (length(nums_qq) + 1, length(nums_qq) + length(plist) - 1))
Expand All @@ -140,16 +175,17 @@ mutable struct IdealMQS{T} <: AbstractBlackboxIdeal
num,
R_sat,
matching = :byindex,
shift = Int(sat_var_index == 1),
shift = sat_var_count * (sat_var_index == 1),
)
push!(nums_qq, num)
end
end
parent_ring_param, _ = PolynomialRing(ring, varnames, ordering = ordering)
@debug "Constructed MQS ideal in $R_sat with $(length(nums_qq) + 1) elements"
@debug "Constructed MQS ideal in $R_sat with $(length(nums_qq)) + $(length(sat_qq)) elements"
flush(stdout)
@assert length(pivots_indices) == length(dens_indices) == length(dens_qq)
@assert length(pivots_indices) == length(funcs_den_nums)
@assert length(sat_qq) == sat_var_count && length(sat_qq) > 0

new{elem_type(R_sat)}(
funcs_den_nums,
Expand All @@ -162,6 +198,7 @@ mutable struct IdealMQS{T} <: AbstractBlackboxIdeal
pivots_indices,
den_lcm,
sat_var_index,
sat_var_count,
Dict(),
Dict(),
Dict(),
Expand All @@ -170,7 +207,7 @@ mutable struct IdealMQS{T} <: AbstractBlackboxIdeal
end
end

Base.length(ideal::IdealMQS) = length(ideal.nums_qq) + 1
Base.length(ideal::IdealMQS) = length(ideal.nums_qq) + length(ideal.sat_qq)
AbstractAlgebra.base_ring(ideal::IdealMQS) = base_ring(ideal.nums_qq[1])
AbstractAlgebra.parent(ideal::IdealMQS) = ideal.parent_ring_param
ParamPunPam.parent_params(ideal::IdealMQS) = base_ring(ideal.parent_ring_param)
Expand All @@ -191,7 +228,8 @@ end
end

function fractionfree_generators_raw(mqs::IdealMQS)
# TODO: this assumes mqs.sat_var_index is last, and thus is broken
# TODO: this assumes mqs.sat_var_index is last, and thus is broken.
# TODO: well, now this is totally broken.
ring_params = ParamPunPam.parent_params(mqs)
K = base_ring(ring_params)
varnames = map(string, Nemo.symbols(ring_params))
Expand Down Expand Up @@ -239,8 +277,8 @@ function ParamPunPam.reduce_mod_p!(
return nothing
end
nums_qq, dens_qq, sat_qq = mqs.nums_qq, mqs.dens_qq, mqs.sat_qq
sat_gf = map_coefficients(c -> ff(c), sat_qq)
ring_ff = parent(sat_gf)
sat_gf = map(poly -> map_coefficients(c -> ff(c), poly), sat_qq)
ring_ff = parent(first(sat_gf))
nums_gf = map(poly -> map_coefficients(c -> ff(c), poly, parent = ring_ff), nums_qq)
dens_gf = map(poly -> map_coefficients(c -> ff(c), poly, parent = ring_ff), dens_qq)
mqs.cached_nums_gf[ff] = nums_gf
Expand All @@ -263,12 +301,13 @@ function ParamPunPam.specialize_mod_p(
K_2 = base_ring(nums_gf[1])
@assert K_1 == K_2
@assert length(point) == nvars(ParamPunPam.parent_params(mqs))
# +1 actual variable because of the saturation!
@assert length(point) + 1 == nvars(parent(nums_gf[1]))
point_sat = append_at_index(point, mqs.sat_var_index, one(K_1))
# +k actual variables because of the saturation!
@assert length(point) + mqs.sat_var_count == nvars(parent(nums_gf[1]))
point_sat =
append_at_index(point, mqs.sat_var_index, map(_ -> one(K_1), 1:(mqs.sat_var_count)))
nums_gf_spec = map(num -> evaluate(num, point_sat), nums_gf)
dens_gf_spec = map(den -> evaluate(den, point_sat), dens_gf)
polys = Vector{typeof(sat_gf)}(undef, length(nums_gf_spec) + 1)
polys = Vector{eltype(sat_gf)}(undef, length(nums_gf_spec) + length(sat_gf))
@inbounds for i in 1:length(dens_gf_spec)
den, den_spec = dens_gf[i], dens_gf_spec[i]
iszero(den_spec) && __throw_unlucky_evaluation("Point: $point")
Expand All @@ -278,9 +317,12 @@ function ParamPunPam.specialize_mod_p(
polys[j] = num * den_spec - den * num_spec
end
end
polys[end] = sat_gf
if !saturated
resize!(polys, length(polys) - 1)
if saturated
for i in 1:length(sat_gf)
polys[length(nums_gf_spec) + i] = sat_gf[i]
end
else
resize!(polys, length(nums_gf_spec))
end
return polys
end
Expand All @@ -291,12 +333,13 @@ function specialize(mqs::IdealMQS, point::Vector{Nemo.fmpq}; saturated = true)
dens_indices = mqs.dens_indices
K = base_ring(mqs)
@assert length(point) == nvars(ParamPunPam.parent_params(mqs))
# +1 actual variable because of the saturation!
@assert length(point) + 1 == nvars(parent(nums_qq[1]))
point_sat = append_at_index(point, mqs.sat_var_index, one(K))
# +k actual variables because of the saturation!
@assert length(point) + mqs.sat_var_count == nvars(parent(nums_qq[1]))
point_sat =
append_at_index(point, mqs.sat_var_index, map(_ -> one(K), 1:(mqs.sat_var_count)))
nums_qq_spec = map(num -> evaluate(num, point_sat), nums_qq)
dens_qq_spec = map(den -> evaluate(den, point_sat), dens_qq)
polys = Vector{typeof(sat_qq)}(undef, length(nums_qq_spec) + 1)
polys = Vector{eltype(sat_qq)}(undef, length(nums_qq_spec) + length(sat_qq))
@inbounds for i in 1:length(dens_qq_spec)
den, den_spec = dens_qq[i], dens_qq_spec[i]
iszero(den_spec) && __throw_unlucky_evaluation("Point: $point")
Expand All @@ -306,9 +349,12 @@ function specialize(mqs::IdealMQS, point::Vector{Nemo.fmpq}; saturated = true)
polys[j] = num * den_spec - den * num_spec
end
end
polys[end] = sat_qq
if !saturated
resize!(polys, length(polys) - 1)
if saturated
for i in 1:length(sat_qq)
polys[length(nums_qq_spec) + i] = sat_qq[i]
end
else
resize!(polys, length(nums_qq_spec))
end
return polys
end
22 changes: 18 additions & 4 deletions src/RationalFunctionFields/normalforms.jl
Original file line number Diff line number Diff line change
Expand Up @@ -54,14 +54,20 @@ function local_normal_forms(
)
@assert !isempty(point)
@assert parent(first(point)) == finite_field
point_ff_ext = append_at_index(point, mqs.sat_var_index, one(finite_field))
# TODO: it is possible that the saturation details should be hidden in the
# MQS ideal and not visible to the outside code
point_ff_ext = append_at_index(
point,
mqs.sat_var_index,
map(_ -> one(finite_field), 1:(mqs.sat_var_count)),
)
gens_ff_spec = specialize_mod_p(mqs, point)
gb_ff_spec = Groebner.groebner(gens_ff_spec)
ring_ff = parent(gb_ff_spec[1])
xs_ff = gens(ring_ff)
normal_forms_ff = Vector{elem_type(ring_ff)}(undef, 0)
monoms_ff = Vector{elem_type(ring_ff)}(undef, 0)
xs_ff = cut_at_index(xs_ff, mqs.sat_var_index)
xs_ff = cut_at_index(xs_ff, mqs.sat_var_index, mqs.sat_var_count)
pivot_vectors = map(f -> exponent_vector(f, 1), xs_ff)
@debug """
variables in the finite field: $(xs_ff)
Expand Down Expand Up @@ -356,7 +362,11 @@ function linear_relations_between_normal_forms(
n_relations_ff = length(complete_intersection_relations_ff)
# Filter out some relations from the complete intersection
zeroed_relations_inds = Vector{Int}()
point_ext = append_at_index(point, mqs.sat_var_index, one(finite_field))
point_ext = append_at_index(
point,
mqs.sat_var_index,
map(_ -> one(finite_field), 1:(mqs.sat_var_count)),
)
for i in 1:length(complete_intersection_relations_ff)
relation = complete_intersection_relations_ff[i]
relation_mqs = relation - evaluate(relation, point_ext)
Expand Down Expand Up @@ -408,7 +418,11 @@ function linear_relations_between_normal_forms(
end
relation_qq_param = evaluate(
relation_qq,
append_at_index(xs_param, mqs.sat_var_index, one(ring_param)),
append_at_index(
xs_param,
mqs.sat_var_index,
map(_ -> one(ring_param), 1:(mqs.sat_var_count)),
),
)
relations_qq[i] = relation_qq_param // one(relation_qq_param)
end
Expand Down
8 changes: 4 additions & 4 deletions src/util.jl
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ end

# ------------------------------------------------------------------------------

function append_at_index(vec::Vector{T}, idx::Integer, val::T) where {T}
function append_at_index(vec::Vector{T}, idx::Integer, val) where {T}
# NOTE: could also just use insert!
@assert (idx == 1) || (idx == length(vec) + 1)
if idx == 1
Expand All @@ -20,12 +20,12 @@ function append_at_index(vec::Vector{T}, idx::Integer, val::T) where {T}
end
end

function cut_at_index(vec::Vector{T}, idx::Integer) where {T}
function cut_at_index(vec::Vector{T}, idx::Integer, count::Integer) where {T}
@assert (idx == 1) || (idx == length(vec))
if idx == 1
vec[2:end]
vec[(count + 1):end]
else
vec[1:(end - 1)]
vec[1:(end - count)]
end
end

Expand Down
2 changes: 1 addition & 1 deletion test/identifiable_functions.jl
Original file line number Diff line number Diff line change
Expand Up @@ -935,7 +935,7 @@ ode = StructuralIdentifiability.@ODEmodel(
ident_funcs = [k3, k1 // k7, k5 // k2, k6 // k2, k7 * EpoR_A]
push!(test_cases, (ode = ode, ident_funcs = ident_funcs))

ode = @ODEmodel(x1'(t) = x1, x2'(t) = x2, y(t) = x1 + x2(t))
ode = StructuralIdentifiability.@ODEmodel(x1'(t) = x1, x2'(t) = x2, y(t) = x1 + x2(t))
ident_funcs = [x1 + x2]
push!(test_cases, (ode = ode, ident_funcs = ident_funcs, with_states = true))

Expand Down
Loading