forked from arminbiere/kissat
-
Notifications
You must be signed in to change notification settings - Fork 1
/
process.py
executable file
·55 lines (44 loc) · 1.61 KB
/
process.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
#!/usr/bin/python3
import sys
import re
message = sys.stdin.read()
def normalize(str_):
return re.sub('\s+', ' ', str_).strip()
def handleOne(message):
result = []
lines = message.splitlines()
number_lines = len(lines)
if len([line for line in lines if line.startswith('c ---- [ result ]')]) > 0:
for i in range(number_lines):
if lines[i].startswith('c opened and reading DIMACS file:'):
result.append(normalize(lines[i + 2]))
if lines[i].startswith('c ---- [ result ]'):
result_text = normalize(lines[i + 2])
result.append(result_text)
# for j in range (i + 3, number_lines):
# if lines[j].startswith('v'):
# result.append(lines[j])
if lines[i].startswith('c process-time'):
result.append(normalize(lines[i]))
return result
else:
for i in range(number_lines):
if lines[i].startswith('c opened and reading DIMACS file:'):
result.append(normalize(lines[i + 2]))
if lines[i].startswith('c process-time'):
result.append(normalize(lines[i]))
result.append('UNKNOWN')
return result
def handleMany(message_inp):
lst_message = re.split('c exit 10\n|c exit 0\n', message_inp)
result = []
for message in lst_message:
result.append(handleOne(message))
return result
def serialize(data):
result = ''
for item in data:
result += '\n'.join(item)
result += '\n-----\n'
return result
print(serialize(handleMany(message)))