diff options
author | Tim King <taking@cs.nyu.edu> | 2010-07-08 01:24:34 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-07-08 01:24:34 +0000 |
commit | 586c8f2d51d790942fd82598a2bf532f2b5ebc9a (patch) | |
tree | 3b5dc8ba79509747a7f5909a39aa4284fce58819 /contrib | |
parent | 5b4b7727433f06c1788647b08e7da1ee1cc37bc9 (diff) |
Updates to the post_mortem.py script.
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/post_mortem.py | 28 |
1 files changed, 23 insertions, 5 deletions
diff --git a/contrib/post_mortem.py b/contrib/post_mortem.py index e0fe2b9d4..4a941f1c9 100644 --- a/contrib/post_mortem.py +++ b/contrib/post_mortem.py @@ -14,11 +14,10 @@ class Database: self.currentRow = dict() def currentRowIsClear(self): return len(self.currentRow) == 0 - def writeDB(self, file): + def writeDB(self, file, order): assert self.currentRowIsClear() - file.write("#") first = True - for name in registry: + for name in order: if first: first = False else: @@ -28,7 +27,7 @@ class Database: file.write("\n") for row in self.rows: first = True - for name in registry: + for name in order: if first: first = False else: @@ -123,6 +122,25 @@ registry["average_resident_size"] = str2int registry["id"] = str2int +def find(l, elem): + for i in xrange(len(l)): + if elem == l[i]: + return i + return -1 + +def pushToFront(l, elem): + l.remove(elem) + l.insert(0,elem) + +regOrder = list(registry.keys()) +regOrder.sort() +pushToFront(regOrder, "filename") +pushToFront(regOrder, "theory::propagate") +pushToFront(regOrder, "theory::conflicts") +pushToFront(regOrder, "sat::decisions") +pushToFront(regOrder, "system_time") +pushToFront(regOrder, "user_time") + def isSatResult(line): up = line.upper().strip() if up == "UNSAT": @@ -209,4 +227,4 @@ else: handleFile(db, target) db.commitRow() -db.writeDB(sys.stdout) +db.writeDB(sys.stdout, regOrder) |