diff --git a/Orb_AutFN.jl b/Orb_AutFN.jl index 2546f31..0120ba8 100644 --- a/Orb_AutFN.jl +++ b/Orb_AutFN.jl @@ -130,13 +130,6 @@ function addconstraints!(m::JuMP.Model, data::OrbitData, l::Int=length(data.lapl end end -function reconstructP(m::JuMP.Model, data::OrbitData) - computedPs = [getvalue(P) for P in data.Ps] - return sum( - data.dims[π]*transform(data.Us[π]',computedPs[π], sparse=false) - for π in 1:endof(data.Ps)) -end - function create_SDP_problem(name::String; upper_bound=Inf) info(PropertyT.logger, "Loading data....") t = @timed SDP_problem, orb_data = init_OrbitData(name); @@ -158,11 +151,43 @@ function λandP(m::JuMP.Model, data::OrbitData) info(PropertyT.logger, "Solving SDP problem...") varλ = m[:λ] varP = data.Ps - λ, P = PropertyT.λandP(data.name, m, varλ, varP) + λ, Ps = PropertyT.λandP(data.name, m, varλ, varP) + return λ, Ps +end + +function matrix_reps{T<:GroupElem}(G::Group, S::Vector{T}, AutS::Group, radius::Int) + Id = (isa(G, Nemo.Ring) ? one(G) : G()) + E2, _ = Groups.generate_balls(S, Id, radius=radius) + Edict = GroupRings.reverse_dict(E2) + + mreps = Dict(g => matrix_repr(g, E2, Edict) for g in elements(AutS)) + return mreps +end + +function reconstruct(mreps::Dict, Us::Vector, Ps::Vector, dims::Vector) + recP = zeros(size(Us[1],1), size(Us[1],1)) + + for g in keys(mreps) + for π in 1:endof(Us) + recP .+= dims[π] .* mreps[g]*transform(Us[π]', Ps[π])*mreps[inv(g)] + end + end + recP .*= 1/length(collect(keys(mreps))) + + return recP +end + +function λandP(m::JuMP.Model, data::OrbitData, sett::Settings) + info(PropertyT.logger, "Solving SDP problem...") + λ, Ps = λandP(m, data) + + info(PropertyT.logger, "Reconstructing P...") + mreps = matrix_reps(sett.G, sett.S, sett.AutS, sett.radius) + + recP = reconstruct(mreps, data.Us, Ps, data.dims) - recP = reconstructP(m, data) fname = PropertyT.λSDPfilenames(data.name)[2] - save(fname, "origP", P, "P", recP) + save(fname, "origP", Ps, "P", recP) return λ, recP end @@ -193,7 +218,8 @@ function orbit_check_propertyT(logger, sett::Settings) info(logger, "Creating SDP problem...") SDP_problem, orb_data = create_SDP_problem(sett.name, upper_bound=sett.upper_bound) JuMP.setsolver(SDP_problem, sett.solver) - λ, P = λandP(SDP_problem, orb_data) + + λ, P = λandP(SDP_problem, orb_data, sett) end info(logger, "λ = $λ")