2023-03-19 23:28:36 +01:00
|
|
|
function check_positivity(
|
|
|
|
elt,
|
|
|
|
unit;
|
|
|
|
upper_bound = Inf,
|
|
|
|
halfradius = 2,
|
|
|
|
optimizer,
|
|
|
|
)
|
2022-11-16 00:16:01 +01:00
|
|
|
@time sos_problem =
|
2023-03-19 23:28:36 +01:00
|
|
|
PropertyT.sos_problem_primal(elt, unit; upper_bound = upper_bound)
|
2022-11-16 00:16:01 +01:00
|
|
|
|
|
|
|
status, _ = PropertyT.solve(sos_problem, optimizer)
|
|
|
|
P = JuMP.value.(sos_problem[:P])
|
|
|
|
Q = real.(sqrt(P))
|
|
|
|
certified, λ_cert = PropertyT.certify_solution(
|
|
|
|
elt,
|
|
|
|
unit,
|
|
|
|
JuMP.objective_value(sos_problem),
|
2023-03-19 23:28:36 +01:00
|
|
|
Q;
|
|
|
|
halfradius = halfradius,
|
2022-11-16 00:16:01 +01:00
|
|
|
)
|
|
|
|
return status, certified, λ_cert
|
|
|
|
end
|
|
|
|
|
2023-03-19 23:28:36 +01:00
|
|
|
function check_positivity(
|
|
|
|
elt,
|
|
|
|
unit,
|
|
|
|
wd;
|
|
|
|
upper_bound = Inf,
|
|
|
|
halfradius = 2,
|
|
|
|
optimizer,
|
|
|
|
)
|
2022-11-16 00:16:01 +01:00
|
|
|
@assert aug(elt) == aug(unit) == 0
|
|
|
|
@time sos_problem, Ps =
|
2023-03-19 23:28:36 +01:00
|
|
|
PropertyT.sos_problem_primal(elt, unit, wd; upper_bound = upper_bound)
|
2022-11-16 00:16:01 +01:00
|
|
|
|
|
|
|
@time status, _ = PropertyT.solve(sos_problem, optimizer)
|
|
|
|
|
|
|
|
Q = let Ps = Ps
|
|
|
|
Qs = [real.(sqrt(JuMP.value.(P))) for P in Ps]
|
|
|
|
PropertyT.reconstruct(Qs, wd)
|
|
|
|
end
|
|
|
|
|
|
|
|
λ = JuMP.value(sos_problem[:λ])
|
|
|
|
|
2023-03-19 23:28:36 +01:00
|
|
|
certified, λ_cert =
|
|
|
|
PropertyT.certify_solution(elt, unit, λ, Q; halfradius = halfradius)
|
2022-11-16 00:16:01 +01:00
|
|
|
return status, certified, λ_cert
|
|
|
|
end
|