Skip to content

Commit

Permalink
assert -> invariant
Browse files Browse the repository at this point in the history
  • Loading branch information
sumiya11 committed Jan 31, 2024
1 parent 3083376 commit 41b76fe
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 10 deletions.
12 changes: 6 additions & 6 deletions src/reconstruction/crt.jl
Original file line number Diff line number Diff line change
Expand Up @@ -310,19 +310,19 @@ function crt_vec_full!(
) where {T <: Integer}
# indices = [(j, i) for j in 1:length(table_zz) for i in 1:length(table_zz[j])]
# crt_vec_partial!(table_zz, modulo, tables_ff, moduli, indices)
@assert isbitstype(T)
@assert length(moduli) > 0
@invariant isbitstype(T)
@invariant length(moduli) > 0

n = length(moduli)
# Base case
if n == 1
table_ff = tables_ff[1]
Base.GMP.MPZ.set_ui!(modulo, UInt64(moduli[1]))
@inbounds for i in 1:length(table_zz)
@assert length(table_zz[i]) == length(table_ff[i])
@invariant length(table_zz[i]) == length(table_ff[i])
for j in 1:length(table_zz[i])
rem_ij = UInt64(table_ff[i][j])
@assert 0 <= rem_ij < moduli[1]
@invariant 0 <= rem_ij < moduli[1]
table_zz[i][j] = rem_ij
end
end
Expand All @@ -343,8 +343,8 @@ function crt_vec_full!(
@inbounds for i in 1:length(table_zz)
for j in 1:length(table_zz[i])
for t in 1:n
@assert length(table_zz[i]) == length(tables_ff[t][i])
@assert 0 <= tables_ff[t][i][j] < moduli[t]
@invariant length(table_zz[i]) == length(tables_ff[t][i])
@invariant 0 <= tables_ff[t][i][j] < moduli[t]
rems[t] = UInt64(tables_ff[t][i][j])
end

Expand Down
8 changes: 4 additions & 4 deletions src/reconstruction/ratrec.jl
Original file line number Diff line number Diff line change
Expand Up @@ -206,15 +206,15 @@ function ratrec_vec_full!(
)
# indices = [(j, i) for j in 1:length(table_zz) for i in 1:length(table_zz[j])]
# ratrec_vec_partial!(table_qq, table_zz, modulo, indices)
@assert length(table_qq) == length(table_zz)
@assert modulo > 1
@invariant length(table_qq) == length(table_zz)
@invariant modulo > 1

modulo_nemo = Nemo.ZZRingElem(modulo)
@inbounds for i in 1:length(table_zz)
@assert length(table_zz[i]) == length(table_qq[i])
@invariant length(table_zz[i]) == length(table_qq[i])
for j in 1:length(table_zz[i])
rem_nemo = Nemo.ZZRingElem(table_zz[i][j])
@assert 0 <= rem_nemo < modulo
@invariant 0 <= rem_nemo < modulo

success, (num, den) = ratrec_nemo(rem_nemo, modulo_nemo)
table_qq[i][j] = Base.unsafe_rational(num, den)
Expand Down

0 comments on commit 41b76fe

Please sign in to comment.