forked from coq-tactician/coq-tactician-stdlib
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathTacticican-stats.py
61 lines (40 loc) · 1.54 KB
/
Tacticican-stats.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
import pandas as pd
bench_list = ["theories/Numbers/HexadecimalNat.bench",
"theories/Logic/Hurkens.bench", "theories/Reals/PartSum.bench"]
for i in range(len(bench_list)):
#print (bench_list[i])
f = open(bench_list[i])
lines = f.readlines()
successful_proof_num = 0
for line in lines:
line = str.split(line)
if len(line) > 2:
successful_proof_num += 1
f.close()
print (successful_proof_num)
import shutil
for root, dirs, files in os.walk('./'):
for file in files:
if file.endswith('.bench'):
shutil.move(root+ '/' +file, '/home/zhangliao/Desktop/Tactician_stats/length-3/'+file )
successful_proof_num = 0
for root, dirs, files in os.walk('./'):
for file in files:
if file.endswith('.bench'):
#print(file)
f = open(root + file)
lines = f.readlines()
for line in lines:
line = str.split(line)
if len(line) > 2:
successful_proof_num += 1
f.close()
print (successful_proof_num)
# shutil.move(root+ '/' +file, '/home/zhangliao/Desktop/Tactician_stats/legth-3/'+file)
import os
for root, dirs, files in os.walk('./'):
for file in files:
if file.endswith('.bench'):
correct_file = file[7:]
# print(root + 'length-3/' + correct_file)
print(correct_file)