using ArgParse using Nemo using GroupRings using PropertyT import SCS.SCSSolver function E(i::Int, j::Int, M::Nemo.MatSpace) @assert i≠j m = one(M) m[i,j] = m[1,1] return m end function SL_generatingset(n::Int) indexing = [(i,j) for i in 1:n for j in 1:n if i≠j] G = Nemo.MatrixSpace(Nemo.ZZ, n,n) S = [E(i,j,G) for (i,j) in indexing]; S = vcat(S, [transpose(x) for x in S]); return unique(S) end function SLsize(n,p) result = 1 for k in 0:n-1 result *= p^n - p^k end return div(result, p-1) end function SL_generatingset(n::Int, p::Int) p == 0 && return SL_generatingset(n) (p > 1 && n > 0) || throw(ArgumentError("Both n and p should be positive integers!")) println("Size(SL($n,$p)) = $(SLsize(n,p))") F = Nemo.ResidueRing(Nemo.ZZ, p) G = Nemo.MatrixSpace(F, n,n) indexing = [(i,j) for i in 1:n for j in 1:n if i≠j] S = [E(i, j, G) for (i,j) in indexing] S = vcat(S, [transpose(x) for x in S]) return unique(S) end function cpuinfo_physicalcores() maxcore = -1 for line in eachline("/proc/cpuinfo") if startswith(line, "core id") maxcore = max(maxcore, parse(Int, split(line, ':')[2])) end end maxcore < 0 && error("failure to read core ids from /proc/cpuinfo") return maxcore + 1 end function parse_commandline() s = ArgParseSettings() @add_arg_table s begin "--tol" help = "set numerical tolerance for the SDP solver (default: 1e-5)" arg_type = Float64 default = 1e-5 "--iterations" help = "set maximal number of iterations for the SDP solver (default: 20000)" arg_type = Int default = 20000 "--upper-bound" help = "Set an upper bound for the spectral gap (default: Inf)" arg_type = Float64 default = Inf "--cpus" help = "Set number of cpus used by solver (default: auto)" arg_type = Int required = false "-N" help = "Consider matrices of size N (default: N=3)" arg_type = Int default = 3 "-p" help = "Matrices over filed of p-elements (default: p=0 => over ZZ)" arg_type = Int default = 0 "--radius" help = "Find the decomposition over B_r(e,S)" arg_type = Int default = 2 end return parse_args(s) end function main() parsed_args = parse_commandline() if parsed_args["cpus"] ≠ nothing if parsed_args["cpus"] > cpuinfo_physicalcores() warn("Number of specified cores exceeds the physical core cound. Performance will suffer.") end Blas.set_num_threads(parsed_args["cpus"]) end tol = parsed_args["tol"] iterations = parsed_args["iterations"] solver = SCSSolver(eps=tol, max_iters=iterations, linearsolver=SCS.Direct) N = parsed_args["N"] upper_bound = parsed_args["upper-bound"] p = parsed_args["p"] if p == 0 name = "SL$(N)Z" else name = "SL$(N)_$p" end radius = parsed_args["radius"] name = "$(name)_$(upper_bound)_r=$radius" logger = PropertyT.setup_logging(name) info(logger, "Group: $name") info(logger, "Iterations: $iterations") info(logger, "Precision: $tol") info(logger, "Upper bound: $upper_bound") S = SL_generatingset(N, p) S = unique([S; [inv(s) for s in S]]) Id = one(parent(S[1])) @time PropertyT.check_property_T(name, S, Id, solver, upper_bound, tol, radius) return 0 end main()