From 4f37db5bde07bf979bfa9a835a022ecb7ec4a605 Mon Sep 17 00:00:00 2001
From: kalmar <kalmar@amu.edu.pl>
Date: Mon, 27 Mar 2017 22:43:58 +0200
Subject: [PATCH] update AutFN.jl to latest changes in PropertyT

---
 AutFN.jl | 99 +++++++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 77 insertions(+), 22 deletions(-)

diff --git a/AutFN.jl b/AutFN.jl
index cf98640..de1878e 100644
--- a/AutFN.jl
+++ b/AutFN.jl
@@ -1,5 +1,10 @@
+using ArgParse
+
 using Groups
-using ProgressMeter
+using GroupAlgebras
+using PropertyT
+
+import SCS.SCSSolver
 
 #=
 Note that the element
@@ -25,7 +30,7 @@ function generating_set_of_AutF(N::Int)
     S = vcat(ϱs,λs)
     S = vcat(S..., σs..., ɛs)
     S = vcat(S..., [inv(g) for g in S])
-    return Vector{AutWord}(unique(S))
+    return Vector{AutWord}(unique(S)), one(AutWord)
 end
 
 function generating_set_of_OutF(N::Int)
@@ -37,7 +42,8 @@ function generating_set_of_OutF(N::Int)
     S = ϱs
     push!(S, λs..., ɛs...)
     push!(S,[inv(g) for g in S]...)
-    return Vector{AutWord}(unique(S))
+
+    return Vector{AutWord}(unique(S)), one(AutWord)
 end
 
 function generating_set_of_Sym(N::Int)
@@ -45,7 +51,7 @@ function generating_set_of_Sym(N::Int)
 
     S = σs
     push!(S, [inv(s) for s in S]...)
-    return Vector{AutWord}(unique(S))
+    return Vector{AutWord}(unique(S)), one(AutWord)
 end
 
 
@@ -53,7 +59,6 @@ function products(S1::Vector{AutWord}, S2::Vector{AutWord})
     result = Vector{AutWord}()
     seen = Set{Vector{FGWord}}()
     n = length(S1)
-    p = Progress(n, 1, "Computing complete products...", 50)
     for (i,x) in enumerate(S1)
         for y in S2
             z::AutWord = x*y
@@ -63,7 +68,6 @@ function products(S1::Vector{AutWord}, S2::Vector{AutWord})
                 push!(result, z)
             end
         end
-        next!(p)
     end
     return result
 end
@@ -72,8 +76,6 @@ function products_images(S1::Vector{AutWord}, S2::Vector{AutWord})
     result = Vector{Vector{FGWord}}()
     seen = Set{Vector{FGWord}}()
     n = length(S1)
-
-    p = Progress(n, 1, "Computing images of elts in B₄...", 50)
     for (i,x) in enumerate(S1)
         z = x(domain)
         for y in S2
@@ -83,7 +85,6 @@ function products_images(S1::Vector{AutWord}, S2::Vector{AutWord})
                 push!(result, v)
             end
         end
-        next!(p)
     end
     return result
 end
@@ -108,11 +109,9 @@ function create_product_matrix(basis::Vector{AutWord}, images)
     @time images_dict = Dict{Vector{FGWord}, Int}(x => i
         for (i,x) in enumerate(images))
 
-    p = Progress(n, 1, "Computing product matrix in basis...", 50)
     for i in 1:n
         z = (inv(basis[i]))(domain)
         product_matrix[i,:] = hashed_product(z, basis, images_dict)
-        next!(p)
     end
     return product_matrix
 end
@@ -141,7 +140,7 @@ function ΔandSDPconstraints(identity::AutWord, S::Vector{AutWord})
     # @assert length(B₄_images) == 3425657
 
     println("Creating product matrix...")
-    @time pm = PropertyT.create_product_matrix(B₂, B₄_images)
+    @time pm = create_product_matrix(B₂, B₄_images)
     println("Creating sdp_constratints...")
     @time sdp_constraints = PropertyT.constraints_from_pm(pm)
 
@@ -151,16 +150,52 @@ function ΔandSDPconstraints(identity::AutWord, S::Vector{AutWord})
     return Δ, sdp_constraints
 end
 
-
-using GroupAlgebras
-using PropertyT
-
 const symbols =  [FGSymbol("x₁",1), FGSymbol("x₂",1), FGSymbol("x₃",1), FGSymbol("x₄",1), FGSymbol("x₅",1), FGSymbol("x₆",1)]
 
 const TOL=1e-8
 const N = 4
 const domain = Vector{FGWord}(symbols[1:N])
-const ID = one(AutWord)
+
+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 automorphisms of free group on N generators (default: N=3)"
+            arg_type = Int
+            default = 3
+    end
+
+    return parse_args(s)
+end
+
 
 # const name = "SYM$N"
 # const upper_bound=factorial(N)-TOL^(1/5)
@@ -169,9 +204,29 @@ const ID = one(AutWord)
 # name = "AutF$N"
 # S() = generating_set_of_AutF(N)
 
-name = "OutF$N"
-S() = generating_set_of_OutF(N)
-const upper_bound=0.05
+function main()
+    parsed_args = parse_commandline()
 
-BLAS.set_num_threads(4)
-@time check_property_T(name, ID, S; verbose=true, tol=TOL, upper_bound=upper_bound)
+    tol = parsed_args["tol"]
+    iterations = parsed_args["iterations"]
+
+    solver = SCSSolver(eps=tol, max_iters=iterations, verbose=true, linearsolver=SCS.Indirect)
+
+    N = parsed_args["N"]
+    upper_bound = parsed_args["upper-bound"]
+
+    name = "OutF$N"
+    name = name*"-$(string(upper_bound))"
+    S() = generating_set_of_OutF(N)
+
+    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
+    @time PropertyT.check_property_T(name, S, solver, upper_bound, tol)
+    return 0
+end
+
+main()