diff --git a/SL.jl b/SL.jl index 4f2bc3a..e9f6cb5 100644 --- a/SL.jl +++ b/SL.jl @@ -1,72 +1,11 @@ using ArgParse -using Nemo -import SCS.SCSSolver -using PropertyT - - -############################################################################### -# -# Generating set -# -############################################################################### - -function E(i::Int, j::Int, M::MatSpace, val=one(M.base_ring)) - @assert i≠j - m = one(M) - m[i,j] = val - return m -end - -function SLsize(n,p) - result = BigInt(1) - for k in 0:n-1 - result *= p^n - p^k - end - return div(result, p-1) -end - -function SL_generatingset(n::Int, X::Bool=false) - indexing = [(i,j) for i in 1:n for j in 1:n if i≠j] - G = MatrixSpace(ZZ, n, n) - if X - S = [E(i,j,G,v) for (i,j) in indexing for v in [1, 100]] - else - S = [E(i,j,G,v) for (i,j) in indexing for v in [1]] - end - S = vcat(S, [inv(x) for x in S]) - return G, unique(S) -end - -function SL_generatingset(n::Int, p::Int, X::Bool=false) - p == 0 && return SL_generatingset(n, X) - (p > 1 && n > 1) || throw("Both n and p should be positive integers!") - info("Size(SL($n,$p)) = $(SLsize(n,p))") - F = ResidueRing(ZZ, p) - G = 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, [inv(x) for x in S]) - return G, unique(S) -end - ############################################################################### # # Parsing command line # ############################################################################### -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() settings = ArgParseSettings() @@ -99,53 +38,61 @@ function parse_commandline() help = "Radius of ball B_r(e,S) to find solution over" arg_type = Int default = 2 + "-X" + help = "Consider EL(N, ZZ⟨X⟩)" + action = :store_true + "--warmstart" + help = "Use warmstart.jl as the initial guess for SCS" + action = :store_true end return parse_args(settings) end -function main() +const PARSEDARGS = parse_commandline() - 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 +include("CPUselect.jl") - N = parsed_args["N"] - p = parsed_args["p"] +# set_parallel_mthread(PARSEDARGS, workers=true) - if p == 0 - dirname = "SL$(N)Z" - else - dirname = "SL$(N)_$p" - end +using SCS.SCSSolver +using Nemo +using PropertyT +using Groups -  radius = parsed_args["radius"] +include("SLNs.jl") + +function main(GROUP, parsed_args) + + radius = parsed_args["radius"] tol = parsed_args["tol"] iterations = parsed_args["iterations"] upper_bound = parsed_args["upper-bound"] + warm = parsed_args["warmstart"] - dirname = "$(dirname)_$(upper_bound)_r=$radius" + name, N = GROUP.groupname(parsed_args) + G, S = G, S = GROUP.generatingset(parsed_args) - logger = PropertyT.setup_logging(dirname) + name = "$(name)_r$radius" + isdir(name) || mkdir(name) - info(logger, "Group: $dirname") + logger = PropertyT.setup_logging(joinpath(name, "$(upper_bound)")) + + info(logger, "Group: $name") info(logger, "Iterations: $iterations") info(logger, "Precision: $tol") info(logger, "Upper bound: $upper_bound") - - G, S = SL_generatingset(N, p) + info(logger, "Threads: $(Threads.nthreads())") + info(logger, "Workers: $(workers())") info(logger, G) info(logger, "Symmetric generating set of size $(length(S))") + Id = one(G) - solver = SCSSolver(eps=tol, max_iters=iterations, linearsolver=SCS.Direct) + solver = SCSSolver(eps=tol, max_iters=iterations, linearsolver=SCS.Direct, alpha=1.9, acceleration_lookback=1) - @time PropertyT.check_property_T(dirname, S, Id, solver, upper_bound, tol, radius) + PropertyT.check_property_T(name, S, Id, solver, upper_bound, tol, radius) return 0 end -main() +main(SLNs, PARSEDARGS)