-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathclingo.py
108 lines (96 loc) · 5.78 KB
/
clingo.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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
'''
Created on Jan 17, 2010
@author: Roland Kaminski
modified by: Javier
'''
import os
import re
import sys
import codecs
clingo_re = {
"models" : ("float", re.compile(r"^(c )?Models[ ]*:[ ]*(?P<val>[0-9]+)\+?[ ]*$")),
"optimal" : ("float", re.compile(r"^(c )?[ ]*Optimal[ ]*:[ ]*(?P<val>[0-9]+)\+?[ ]*$")),
"choices" : ("float", re.compile(r"^(c )?Choices[ ]*:[ ]*(?P<val>[0-9]+)\+?[ ]*")),
"time" : ("float", re.compile(r"^Real time \(s\): (?P<val>[0-9]+(\.[0-9]+)?)$")),
"conflicts" : ("float", re.compile(r"^(c )?Conflicts[ ]*:[ ]*(?P<val>[0-9]+)\+?[ ]*")),
"ctime" : ("float", re.compile(r"^(c )?Time[ ]*:[ ]*(?P<val>[0-9]+(\.[0-9]+)?)")),
"csolve" : ("float", re.compile(r"^(c )?Time[ ]*:[ ]*[0-9]+(\.[0-9]+)?s[ ]*\(Solving:[ ]*(?P<val>[0-9]+(\.[0-9]+)?)")),
"domain" : ("float", re.compile(r"^(c )?Choices[ ]*:[ ]*[0-9]+[ ]*\(Domain:[ ]*(?P<val>[0-9]+)")),
"rules" : ("float", re.compile(r"^(c )?Rules[ ]*:[ ]*(?P<val>[0-9]+)")),
"roriginal" : ("float", re.compile(r"^(c )?Rules[ ]*:[ ]*[0-9]+(\.[0-9]+)?[ ]*\(Original:[ ]*(?P<val>[0-9]+(\.[0-9]+)?)")),
"rchoices" : ("float", re.compile(r"^(c )? Choice [ ]*:[ ]*(?P<val>[0-9]+)")),
"atoms" : ("float", re.compile(r"^(c )?Atoms[ ]*:[ ]*(?P<val>[0-9]+)")),
"bodies" : ("float", re.compile(r"^(c )?Bodies[ ]*:[ ]*(?P<val>[0-9]+)")),
"equiv" : ("float", re.compile(r"^(c )?Equivalences[ ]*:[ ]*(?P<val>[0-9]+)")),
"vars" : ("float", re.compile(r"^(c )?Variables[ ]*:[ ]*(?P<val>[0-9]+)")),
"cons" : ("float", re.compile(r"^(c )?Constraints[ ]*:[ ]*(?P<val>[0-9]+)")),
"restarts" : ("float", re.compile(r"^(c )?Restarts[ ]*:[ ]*(?P<val>[0-9]+)\+?[ ]*")),
"optimum" : ("string", re.compile(r"^(c )?Optimization[ ]*:[ ]*(?P<val>(-?[0-9]+)( -?[0-9]+)*)[ ]*$")),
"status" : ("string", re.compile(r"^(s )?(?P<val>SATISFIABLE|UNSATISFIABLE|UNKNOWN|OPTIMUM FOUND)[ ]*$")),
"interrupted" : ("string", re.compile(r"(c )?(?P<val>INTERRUPTED)")),
"error" : ("string", re.compile(r"^\*\*\* ERROR: (?P<val>.*)$")),
"memerror" : ("string", re.compile(r"^Maximum VSize (?P<val>exceeded): sending SIGTERM then SIGKILL")),
"memerror2" : ("string", re.compile(r"^\*\*\* ERROR: \((?P<val>.*)\): std::bad_alloc")),
"mem" : ("float", re.compile(r"^Max\. virtual memory \(cumulated for all children\) \(KiB\): (?P<val>[0-9]+)")),
"ground0" : ("float", re.compile(r"^(c )?First Ground[ ]*:[ ]*(?P<val>[0-9]+(\.[0-9]+)?)")),
"groundN" : ("float", re.compile(r"^(c )?Next Ground[ ]*:[ ]*(?P<val>[0-9]+(\.[0-9]+)?)")),
"max_length" : ("float", re.compile(r"^(c )?Max\. Length[ ]*:[ ]*(?P<val>[0-9]+)\+?[ ]*")),
"sol_length" : ("float", re.compile(r"^(c )?Sol\. Length[ ]*:[ ]*(?P<val>[0-9]+)\+?[ ]*")),
"calls" : ("float", re.compile(r"^(c )?Calls[ ]*:[ ]*(?P<val>[0-9]+)\+?[ ]*$")),
"ngadded" : ("float", re.compile(r"total nogoods added:[ ]*(?P<val>[0-9]+)\+?[ ]*$")),
}
status_mapping = {"SATISFIABLE": 1, "UNSATISFIABLE": 0, "UNKNOWN": 2, "OPTIMUM FOUND": 3}
def clingo(root, runspec, instance):
"""
Extracts some clingo statistics.
"""
timeout = runspec.project.job.timeout
res = { "time": ("float", timeout) }
for f in ["runsolver.solver", "runsolver.watcher", "benchmark.txt"]:
if f == "benchmark.txt":
if "choices" in res or not os.path.isfile(os.path.join(root, f)):
break
res["status"] = ("string", "UNKNOWN")
for line in codecs.open(os.path.join(root, f), errors='ignore', encoding='utf-8'):
for val, reg in clingo_re.items():
m = reg[1].search(line)
if m:
res[val] = (reg[0], float(m.group("val")) if reg[0] == "float" else m.group("val"))
if "memerror" in res or "memerror2" in res:
res["error"] = ("string", "std::bad_alloc")
res["status"] = ("string", "UNKNOWN")
res.pop("memerror", None)
res.pop("memerror2", None)
if "status" in res and res["status"][1] == "OPTIMUM FOUND" and not "optimal" in res:
res["optimal"] = ("float", float("1"))
result = []
error = (not "status" in res and not "interrupted" in res) or ("error" in res and res["error"][1] != "std::bad_alloc")
memout = "error" in res and res["error"][1] == "std::bad_alloc"
status = res["status"][1] if "status" in res else None
if "models" in res and not "optimal" in res:
res["optimal"] = ("float", float("0"))
timedout = memout or error or status == "UNKNOWN" or (status == "SATISFIABLE" and "optimum" in res) or res["time"][1] >= timeout or "interrupted" in res;
if timedout: res["time"] = ("float", timeout)
if memout:
sys.stderr.write("*** MEMOUT: Run {0} did a memout!\n".format(root))
elif error:
sys.stderr.write("*** ERROR: Run {0} failed with unrecognized status or error!\n".format(root))
result.append(("error", "float", int(error)))
result.append(("timeout", "float", int(timedout)))
result.append(("memout", "float", int(memout)))
if "optimum" in res and not " " in res["optimum"][1]:
result.append(("optimum", "float", float(res["optimum"][1])))
del res["optimum"]
if "interrupted" in res: del res["interrupted"]
if "error" in res: del res["error"]
if "status" in res:
status_val = res["status"][1]
res["status"] = ("float", status_mapping[status_val])
else:
res["status"] = ("float", status_mapping["UNKNOWN"])
if "ngadded" not in res:
res["ngadded"] = ("float", 0.0)
for key, val in res.items(): result.append((key, val[0], val[1]))
if "ctime" in res:
result.append(("ptime","float",res["time"][1]-res["ctime"][1]))
return result