Skip to content

Commit

Permalink
Refactor code
Browse files Browse the repository at this point in the history
  • Loading branch information
@adyang1
adyang1 committed Oct 14, 2024
1 parent d55b0a5 commit 2c7c2fd
Show file tree
Hide file tree
Showing 2 changed files with 86 additions and 97 deletions.
6 changes: 4 additions & 2 deletions blueprint/src/python/polytope.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -165,8 +165,10 @@ def _to_str(row, is_equality):
c = row[i]
if c == 0:
continue
if len(f) != 0:
f += " + " if c > 0 else " - "
elif c > 0:
if len(f) != 0: f += " + "
else:
f += " - " if len(f) != 0 else "-"
if c == 1 or c == -1:
f += v
else:
Expand Down
177 changes: 82 additions & 95 deletions blueprint/src/python/zeta_large_values.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
import bound_beta as bbeta
import large_values as lv
from reference import Reference
from region import Region, Region_Type

###############################################################################

Expand Down Expand Up @@ -133,64 +134,53 @@ def beta_to_zlv(hypotheses):
# piecewise function defined on the whole domain. Only the first of
# these pieces if the bound, the other 3 pieces complete the domain with
# the trivial bound LVZ(s, t) \leq t
f = Piecewise(
[
Affine2(
[0, 0, 0],
Polytope(
[
[1, -1, 0], # \sigma <= 1
[-frac(1, 2), 1, 0], # \sigma > 1/2
[-tau_lower, 0, 1], # \tau >= max(2, 1/a1)
[tau_upper, 0, -1], # \tau <= min(some large number, 1/a0)
[-B, 1, -A], # \sigma >= A\tau + B
]
),
),
# Trivial bound elsewhere -----------------------------------------
Affine2(
[0, 0, 1],
Polytope(
[
[1, -1, 0], # \sigma <= 1
[-frac(1, 2), 1, 0], # \sigma > 1/2
[-tau_lower, 0, 1], # \tau >= max(2, 1/a1)
[tau_upper, 0, -1], # \tau <= min(some large number, 1/a0)
[B, -1, A], # \sigma <= A\tau + B
]
),
),
Affine2(
[0, 0, 1],
Polytope(
[
[1, -1, 0], # \sigma <= 1
[-frac(1, 2), 1, 0], # \sigma > 1/2
[tau_lower, 0, -1], # \tau <= max(2, 1/a1)
[-2, 0, 1], # \tau >= 2
]
),
),
Affine2(
[0, 0, 1],
Polytope(
[
[1, -1, 0], # \sigma <= 1
[-frac(1, 2), 1, 0], # \sigma > 1/2
[-tau_upper, 0, 1], # \tau >= min(some large number, 1/a0)
[
Constants.TAU_UPPER_LIMIT,
0,
-1,
], # \tau <= TAU_UPPER_LIMIT
]
),
),
]
polys = [
Polytope([
[0, 0, 0, -1], # \rho <= 0
[0, 0, 0, 1], # \rho >= 0
[1, -1, 0, 0], # \sigma <= 1
[-frac(1, 2), 1, 0, 0], # \sigma > 1/2
[-tau_lower, 0, 1, 0], # \tau >= max(2, 1/a1)
[tau_upper, 0, -1, 0], # \tau <= min(some large number, 1/a0)
[-B, 1, -A, 0], # \sigma >= A\tau + B
]),
# Trivial bound elsewhere -----------------------------------------
Polytope([
[0, 0, 1, -1], # \rho <= \tau
[0, 0, 0, 1], # \rho >= 0
[1, -1, 0, 0], # \sigma <= 1
[-frac(1, 2), 1, 0], # \sigma > 1/2
[-tau_lower, 0, 1, 0], # \tau >= max(2, 1/a1)
[tau_upper, 0, -1, 0], # \tau <= min(some large number, 1/a0)
[B, -1, A, 0], # \sigma <= A\tau + B
]),
Polytope([
[0, 0, 1, -1], # \rho <= \tau
[0, 0, 0, 1], # \rho >= 0
[1, -1, 0, 0], # \sigma <= 1
[-frac(1, 2), 1, 0, 0], # \sigma > 1/2
[tau_lower, 0, -1, 0], # \tau <= max(2, 1/a1)
[-2, 0, 1, 0], # \tau >= 2
]),
Polytope([
[0, 0, 1, -1], # \rho <= \tau
[0, 0, 0, 1], # \rho >= 0
[1, -1, 0, 0], # \sigma <= 1
[-frac(1, 2), 1, 0, 0], # \sigma > 1/2
[-tau_upper, 0, 1, 0], # \tau >= min(some large number, 1/a0)
[
Constants.TAU_UPPER_LIMIT,
0,
-1,
0
], # \tau <= TAU_UPPER_LIMIT
])
]
region = Region(
Region_Type.DISJOINT_UNION,
[Region.from_polytope(p) for p in polys]
)
f.simplify()

zlv_estimates.append(derived_bound_zeta_LV(f, f"Follows from {be.name}", {be}))
zlv_estimates.append(derived_bound_zeta_LV(region, f"Follows from {be.name}", {be}))

return zlv_estimates

Expand All @@ -205,44 +195,41 @@ def mu_to_zlv(hypotheses):
for mb in mu_bounds:
sigma0 = mb.data.sigma
mu0 = mb.data.mu
f = Piecewise(
[
Affine2(
[0, 0, 0],
Polytope(
[
[1, -1, 0], # \sigma <= 1
[-frac(1, 2), 1, 0], # \sigma > 1/2
[-2, 0, 1], # \tau >= 2
[
Constants.TAU_UPPER_LIMIT,
0,
-1,
], # \tau <= min(some large number, 1/a0)
[-sigma0, 1, -mu0], # \sigma >= sigma0 + \tau * mu0
]
),
),
# Trivial bound elsewhere -----------------------------------------
Affine2(
[0, 0, 1],
Polytope(
[
[1, -1, 0], # \sigma <= 1
[-frac(1, 2), 1, 0], # \sigma > 1/2
[-2, 0, 1], # \tau >= 2
[
Constants.TAU_UPPER_LIMIT,
0,
-1,
], # \tau <= min(some large number, 1/a0)
[sigma0, -1, mu0], # \sigma <= sigma0 + \tau * mu0
]
),
),
]
polys = [
Polytope([
[0, 0, 0, 1], # \rho >= 0
[0, 0, 0, -1], # \rho <= 0
[1, -1, 0, 0], # \sigma <= 1
[-frac(1, 2), 1, 0, 0], # \sigma > 1/2
[-2, 0, 1, 0], # \tau >= 2
[
Constants.TAU_UPPER_LIMIT,
0,
-1,
0
], # \tau <= min(some large number, 1/a0)
[-sigma0, 1, -mu0, 0], # \sigma >= sigma0 + \tau * mu0
]),
# Trivial bound elsewhere -----------------------------------------
Polytope([
[0, 0, 1, -1], # \rho <= \tau
[0, 0, 0, 1], # \rho >= 0
[1, -1, 0, 0], # \sigma <= 1
[-frac(1, 2), 1, 0, 0], # \sigma > 1/2
[-2, 0, 1, 0], # \tau >= 2
[
Constants.TAU_UPPER_LIMIT,
0,
-1,
0
], # \tau <= min(some large number, 1/a0)
[sigma0, -1, mu0, 0], # \sigma <= sigma0 + \tau * mu0
])
]
region = Region(
Region_Type.DISJOINT_UNION,
[Region.from_polytope(p) for p in polys]
)
f.simplify()
zlv_estimates.append(derived_bound_zeta_LV(f, f"Follows from {mb.name}", {mb}))
zlv_estimates.append(derived_bound_zeta_LV(region, f"Follows from {mb.name}", {mb}))

return zlv_estimates

0 comments on commit 2c7c2fd

Please sign in to comment.