Skip to content

Commit 8906dce

Browse files
alberto-paparellaalberto-paparella
authored
Merge pull request #13 from aclai-lab/experiments
Experiments
2 parents c568498 + 2fdf702 commit 8906dce

10 files changed

Lines changed: 81 additions & 81 deletions

File tree

‎.gitignore‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,5 @@ Manifest.toml
77
docs/build/
88
.vscode
99
experiments/*/formulas/*/
10-
experiments/*/results/*
1110
results/
1211
test/alphaval/mvhs-tableau/enriched_valid*

‎experiments/.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
results/
2+
*.toml

‎experiments/alphasat/mvcl-tableau.jl‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,12 @@ using SoleLogics
33
using SoleLogics.ManyValuedLogics
44
using SoleReasoners
55
using StatsBase
6-
import SoleBase: initrng
76
import SoleLogics: sample
87

98
myalphabet = Atom.(["p", "q", "r"])
109

1110
min_height = 1
12-
max_height = 7
11+
max_height = 6
1312
max_it = 99999
1413
max_avg = 200
1514
max_timeout = 60 # seconds
@@ -35,7 +34,7 @@ append!(
3534
mvclopweights = [8, 8, 8, 3, 3, 3, 3, 3, 3, 3, 3]
3635

3736
using SoleLogics.ManyValuedLogics: booleanalgebra, G3, Ł3, G4, Ł4, H4
38-
using SoleLogics.ManyValuedLogics: G5, G6, H6_1, H6_2, H6_3, H6
37+
using SoleLogics.ManyValuedLogics: G6, H6_1, H6_2, H6_3, H6, H9
3938

4039
algebras = [
4140
("BA", booleanalgebra),
@@ -44,12 +43,12 @@ algebras = [
4443
("G4", G4 ),
4544
("Ł4", Ł4 ),
4645
("H4", H4 ),
47-
# ("G5", G5 ),
48-
# ("G6", G6 ),
49-
# ("H6_1", H6_1 ),
50-
# ("H6_2", H6_2 ),
51-
# ("H6_3", H6_3 ),
52-
# ("H6", H6 )
46+
("G6", G6 ),
47+
("H6_1", H6_1 ),
48+
("H6_2", H6_2 ),
49+
("H6_3", H6_3 ),
50+
("H6", H6 ),
51+
("H9", H9 )
5352
]
5453

5554
# Latex
@@ -66,7 +65,7 @@ for a in algebras
6665
unsats = zeros(Int64, max_height-min_height+1) # unsat for each height
6766
times = zeros(Float16, max_height-min_height+1) # times for each height
6867

69-
rng = initrng(Random.GLOBAL_RNG)
68+
rng = Random.GLOBAL_RNG
7069
aot = vcat(myalphabet,getdomain(a[2])) # atoms or truths
7170
aotweights = StatsBase.uweights(length(myalphabet)+length(getdomain(a[2])))
7271
aotpicker = (rng)->StatsBase.sample(rng, aot, aotweights)
@@ -165,6 +164,7 @@ for a in algebras
165164
print("($(i+min_height-1),$(times[i]))")
166165
end
167166
println("\n\n")
167+
flush(stdout)
168168
end
169169

170170
# Latex

‎experiments/alphasat/mvhs-tableau.jl‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,12 @@ using SoleLogics
33
using SoleLogics.ManyValuedLogics
44
using SoleReasoners
55
using StatsBase
6-
import SoleBase: initrng
76
import SoleLogics: sample
87

98
myalphabet = Atom.(["p", "q", "r"])
109

1110
min_height = 1
12-
max_height = 7
11+
max_height = 6
1312
max_it = 99999
1413
max_avg = 200
1514
max_timeout = 60 # seconds
@@ -52,7 +51,7 @@ append!(
5251
mvhsopweights = [8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
5352

5453
using SoleLogics.ManyValuedLogics: booleanalgebra, G3, Ł3, G4, Ł4, H4
55-
using SoleLogics.ManyValuedLogics: G5, G6, H6_1, H6_2, H6_3, H6
54+
using SoleLogics.ManyValuedLogics: G6, H6_1, H6_2, H6_3, H6, H9
5655

5756
algebras = [
5857
("BA", booleanalgebra),
@@ -61,12 +60,12 @@ algebras = [
6160
("G4", G4 ),
6261
("Ł4", Ł4 ),
6362
("H4", H4 ),
64-
# ("G5", G5 ),
65-
# ("G6", G6 ),
66-
# ("H6_1", H6_1 ),
67-
# ("H6_2", H6_2 ),
68-
# ("H6_3", H6_3 ),
69-
# ("H6", H6 )
63+
("G6", G6 ),
64+
("H6_1", H6_1 ),
65+
("H6_2", H6_2 ),
66+
("H6_3", H6_3 ),
67+
("H6", H6 ),
68+
("H9", H9 )
7069
]
7170

7271
# Latex
@@ -83,7 +82,7 @@ for a in algebras
8382
unsats = zeros(Int64, max_height-min_height+1) # unsat for each height
8483
times = zeros(Float16, max_height-min_height+1) # times for each height
8584

86-
rng = initrng(Random.GLOBAL_RNG)
85+
rng = Random.GLOBAL_RNG
8786
aot = vcat(myalphabet,getdomain(a[2])) # atoms or truths
8887
aotweights = StatsBase.uweights(length(myalphabet)+length(getdomain(a[2])))
8988
aotpicker = (rng)->StatsBase.sample(rng, aot, aotweights)
@@ -182,6 +181,7 @@ for a in algebras
182181
print("($(i+min_height-1),$(times[i]))")
183182
end
184183
println("\n\n")
184+
flush(stdout)
185185
end
186186

187187
# Latex

‎experiments/alphasat/mvlrcc8-tableau.jl‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,12 @@ using SoleLogics
33
using SoleLogics.ManyValuedLogics
44
using SoleReasoners
55
using StatsBase
6-
import SoleBase: initrng
76
import SoleLogics: sample
87

98
myalphabet = Atom.(["p", "q", "r"])
109

1110
min_height = 1
12-
max_height = 7
11+
max_height = 6
1312
max_it = 99999
1413
max_avg = 200
1514
max_timeout = 60 # seconds
@@ -42,7 +41,7 @@ append!(
4241
mvlrcc8opweights = [14, 14, 14, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3]
4342

4443
using SoleLogics.ManyValuedLogics: booleanalgebra, G3, Ł3, G4, Ł4, H4
45-
using SoleLogics.ManyValuedLogics: G5, G6, H6_1, H6_2, H6_3, H6
44+
using SoleLogics.ManyValuedLogics: G5, G6, H6_1, H6_2, H6_3, H6, H9
4645

4746
algebras = [
4847
("BA", booleanalgebra),
@@ -51,12 +50,12 @@ algebras = [
5150
("G4", G4 ),
5251
("Ł4", Ł4 ),
5352
("H4", H4 ),
54-
# ("G5", G5 ),
55-
# ("G6", G6 ),
56-
# ("H6_1", H6_1 ),
57-
# ("H6_2", H6_2 ),
58-
# ("H6_3", H6_3 ),
59-
# ("H6", H6 )
53+
("G6", G6 ),
54+
("H6_1", H6_1 ),
55+
("H6_2", H6_2 ),
56+
("H6_3", H6_3 ),
57+
("H6", H6 ),
58+
("H9", H9 )
6059
]
6160

6261
# Latex
@@ -73,7 +72,7 @@ for a in algebras
7372
unsats = zeros(Int64, max_height-min_height+1) # unsat for each height
7473
times = zeros(Float16, max_height-min_height+1) # times for each height
7574

76-
rng = initrng(Random.GLOBAL_RNG)
75+
rng = Random.GLOBAL_RNG
7776
aot = vcat(myalphabet,getdomain(a[2])) # atoms or truths
7877
aotweights = StatsBase.uweights(length(myalphabet)+length(getdomain(a[2])))
7978
aotpicker = (rng)->StatsBase.sample(rng, aot, aotweights)
@@ -172,6 +171,7 @@ for a in algebras
172171
print("($(i+min_height-1),$(times[i]))")
173172
end
174173
println("\n\n")
174+
flush(stdout)
175175
end
176176

177177
# Latex

‎experiments/alphasat/mvltlfp-tableau.jl‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,12 @@ using SoleLogics
33
using SoleLogics.ManyValuedLogics
44
using SoleReasoners
55
using StatsBase
6-
import SoleBase: initrng
76
import SoleLogics: sample
87

98
myalphabet = Atom.(["p", "q", "r"])
109

1110
min_height = 1
12-
max_height = 7
11+
max_height = 6
1312
max_it = 99999
1413
max_avg = 200
1514
max_timeout = 60 # seconds
@@ -31,7 +30,7 @@ append!(
3130
mvltlfpopweights = [4, 4, 4, 3, 3, 3, 3]
3231

3332
using SoleLogics.ManyValuedLogics: booleanalgebra, G3, Ł3, G4, Ł4, H4
34-
using SoleLogics.ManyValuedLogics: G5, G6, H6_1, H6_2, H6_3, H6
33+
using SoleLogics.ManyValuedLogics: G6, H6_1, H6_2, H6_3, H6, H9
3534

3635
algebras = [
3736
("BA", booleanalgebra),
@@ -40,12 +39,12 @@ algebras = [
4039
("G4", G4 ),
4140
("Ł4", Ł4 ),
4241
("H4", H4 ),
43-
# ("G5", G5 ),
44-
# ("G6", G6 ),
45-
# ("H6_1", H6_1 ),
46-
# ("H6_2", H6_2 ),
47-
# ("H6_3", H6_3 ),
48-
# ("H6", H6 )
42+
("G6", G6 ),
43+
("H6_1", H6_1 ),
44+
("H6_2", H6_2 ),
45+
("H6_3", H6_3 ),
46+
("H6", H6 ),
47+
("H9", H9 )
4948
]
5049

5150
# Latex
@@ -62,7 +61,7 @@ for a in algebras
6261
unsats = zeros(Int64, max_height-min_height+1) # unsat for each height
6362
times = zeros(Float16, max_height-min_height+1) # times for each height
6463

65-
rng = initrng(Random.GLOBAL_RNG)
64+
rng = Random.GLOBAL_RNG
6665
aot = vcat(myalphabet,getdomain(a[2])) # atoms or truths
6766
aotweights = StatsBase.uweights(length(myalphabet)+length(getdomain(a[2])))
6867
aotpicker = (rng)->StatsBase.sample(rng, aot, aotweights)
@@ -161,6 +160,7 @@ for a in algebras
161160
print("($(i+min_height-1),$(times[i]))")
162161
end
163162
println("\n\n")
163+
flush(stdout)
164164
end
165165

166166
# Latex

‎experiments/alphaval/mvcl-tableau.jl‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,12 @@ using SoleLogics
33
using SoleLogics.ManyValuedLogics
44
using SoleReasoners
55
using StatsBase
6-
import SoleBase: initrng
76
import SoleLogics: sample
87

98
myalphabet = Atom.(["p", "q", "r"])
109

1110
min_height = 1
12-
max_height = 7
11+
max_height = 6
1312
max_it = 99999
1413
max_avg = 200
1514
max_timeout = 60 # seconds
@@ -35,7 +34,7 @@ append!(
3534
mvclopweights = [8, 8, 8, 3, 3, 3, 3, 3, 3, 3, 3]
3635

3736
using SoleLogics.ManyValuedLogics: booleanalgebra, G3, Ł3, G4, Ł4, H4
38-
using SoleLogics.ManyValuedLogics: G5, G6, H6_1, H6_2, H6_3, H6
37+
using SoleLogics.ManyValuedLogics: G6, H6_1, H6_2, H6_3, H6, H9
3938

4039
algebras = [
4140
("BA", booleanalgebra),
@@ -44,12 +43,12 @@ algebras = [
4443
("G4", G4 ),
4544
("Ł4", Ł4 ),
4645
("H4", H4 ),
47-
# ("G5", G5 ),
48-
# ("G6", G6 ),
49-
# ("H6_1", H6_1 ),
50-
# ("H6_2", H6_2 ),
51-
# ("H6_3", H6_3 ),
52-
# ("H6", H6 )
46+
("G6", G6 ),
47+
("H6_1", H6_1 ),
48+
("H6_2", H6_2 ),
49+
("H6_3", H6_3 ),
50+
("H6", H6 ),
51+
("H9", H9 )
5352
]
5453

5554
# Latex
@@ -66,7 +65,7 @@ for a in algebras
6665
unvals = zeros(Int64, max_height-min_height+1) # unval for each height
6766
times = zeros(Float16, max_height-min_height+1) # times for each height
6867

69-
rng = initrng(Random.GLOBAL_RNG)
68+
rng = Random.GLOBAL_RNG
7069
aot = vcat(myalphabet,getdomain(a[2])) # atoms or truths
7170
aotweights = StatsBase.uweights(length(myalphabet)+length(getdomain(a[2])))
7271
aotpicker = (rng)->StatsBase.sample(rng, aot, aotweights)
@@ -165,6 +164,7 @@ for a in algebras
165164
print("($(i+min_height-1),$(times[i]))")
166165
end
167166
println("\n\n")
167+
flush(stdout)
168168
end
169169

170170
# Latex

‎experiments/alphaval/mvhs-tableau.jl‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,12 @@ using SoleLogics
33
using SoleLogics.ManyValuedLogics
44
using SoleReasoners
55
using StatsBase
6-
import SoleBase: initrng
76
import SoleLogics: sample
87

98
myalphabet = Atom.(["p", "q", "r"])
109

1110
min_height = 1
12-
max_height = 7
11+
max_height = 6
1312
max_it = 99999
1413
max_avg = 200
1514
max_timeout = 60 # seconds
@@ -52,7 +51,7 @@ append!(
5251
mvhsopweights = [8, 8, 8, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
5352

5453
using SoleLogics.ManyValuedLogics: booleanalgebra, G3, Ł3, G4, Ł4, H4
55-
using SoleLogics.ManyValuedLogics: G5, G6, H6_1, H6_2, H6_3, H6
54+
using SoleLogics.ManyValuedLogics: G6, H6_1, H6_2, H6_3, H6, H9
5655

5756
algebras = [
5857
("BA", booleanalgebra),
@@ -61,12 +60,12 @@ algebras = [
6160
("G4", G4 ),
6261
("Ł4", Ł4 ),
6362
("H4", H4 ),
64-
# ("G5", G5 ),
65-
# ("G6", G6 ),
66-
# ("H6_1", H6_1 ),
67-
# ("H6_2", H6_2 ),
68-
# ("H6_3", H6_3 ),
69-
# ("H6", H6 )
63+
("G6", G6 ),
64+
("H6_1", H6_1 ),
65+
("H6_2", H6_2 ),
66+
("H6_3", H6_3 ),
67+
("H6", H6 ),
68+
("H9", H9 )
7069
]
7170

7271
# Latex
@@ -83,7 +82,7 @@ for a in algebras
8382
unvals = zeros(Int64, max_height-min_height+1) # unval for each height
8483
times = zeros(Float16, max_height-min_height+1) # times for each height
8584

86-
rng = initrng(Random.GLOBAL_RNG)
85+
rng = Random.GLOBAL_RNG
8786
aot = vcat(myalphabet,getdomain(a[2])) # atoms or truths
8887
aotweights = StatsBase.uweights(length(myalphabet)+length(getdomain(a[2])))
8988
aotpicker = (rng)->StatsBase.sample(rng, aot, aotweights)
@@ -182,6 +181,7 @@ for a in algebras
182181
print("($(i+min_height-1),$(times[i]))")
183182
end
184183
println("\n\n")
184+
flush(stdout)
185185
end
186186

187187
# Latex

0 commit comments

Comments
 (0)