Moving the post_mortem.py script out of contrib and into the cvc4 scripts directory.

diff --git a/contrib/post_mortem.py b/contrib/post_mortem.py
deleted file mode 100644 (file)
index ccba084..0000000
--- a/contrib/post_mortem.py
+++ /dev/null
@@ -1,251 +0,0 @@
-
-
-stat_name_delim = ","
-
-class Database:
-    def __init__(self):
-        self.rows = []
-        self.currentRow = dict()
-    def insert(self, name, val):
-        assert name not in self.currentRow
-        self.currentRow[name] = val
-    def commitRow(self):
-        self.rows.append(self.currentRow)
-        self.currentRow = dict()
-    def currentRowIsClear(self):
-        return len(self.currentRow) == 0
-    def writeDB(self, file, order):
-        assert self.currentRowIsClear()
-        first = True
-        for name in order:
-            if first:
-                first = False
-            else:
-                file.write(",")
-            file.write(name)
-
-        file.write("\n")
-        for row in self.rows:
-            first = True
-            for name in order:
-                if first:
-                    first = False
-                else:
-                    file.write(",")
-                if name in row:
-                    file.write(str(row[name]))
-                else:
-                    file.write(" ")
-            file.write("\n")
-
-def readDatabase(filename):
-    file = open(filename)
-    db = Database()
-    first = True
-    names = []
-    for line in file:
-        if first:
-            first = False
-            (_,hash,line) = line.partition("#")
-            assert hash == "#"
-            line = line.strip()
-            names = line.split(",")
-            for n in names:
-                assert n in registry
-        else:
-            vals = line.split(",")
-            for index in xrange(len(vals)):
-                addStat(db,names[index],vals[index])
-            db.commitRow()
-    file.close()
-    return db
-
-
-int_default = "-1"
-def str2int(x):
-    if x.strip() == "":
-        return int_default
-    else:
-        return int(x)
-
-str2str = lambda x: x
-
-str2strip2str = lambda x: x.strip()
-
-float_default = "-1.0"
-def str2float(x):
-    if x.strip() == "":
-        return float_default
-    else:
-        return float(x)
-
-def strpercent2float(x):
-    if x.strip() == "":
-        return float_default
-    else:
-        return float(x.strip('%'))
-
-registry = dict()
-registry["sat/unsat"] = lambda x: x.upper() == "SAT" and 1 or 0
-registry["filename"] = str2strip2str
-registry["sat::clauses_literals"] = str2int
-registry["sat::tot_literals"] = str2int
-registry["sat::starts"] = str2int
-registry["sat::rnd_decisions"] = str2int
-registry["sat::propagations"] = str2int
-registry["sat::max_literals"] = str2int
-registry["sat::learnts_literals"] = str2int
-registry["sat::decisions"] = str2int
-registry["sat::conflicts"] = str2int
-registry["theory::arith::AssertLowerConflicts"] = str2int
-registry["theory::arith::AssertUpperConflicts"] = str2int
-registry["theory::arith::UpdateConflicts"] = str2int
-registry["theory::arith::Average#ConstantInPivotRow"] = str2float
-registry["theory::arith::AveragePivotLength"] = str2float
-
-registry["theory::arith::Ejections"] = str2int
-registry["theory::arith::UnEjections"] = str2int
-
-registry["theory::arith::SlackVariables"] = str2int
-registry["theory::arith::UserVariables"] = str2int
-
-registry["theory::arith::pivots"] = str2int
-registry["theory::arith::updates"] = str2int
-registry["theory::aug_lemma"] = str2int
-registry["theory::conflicts"] = str2int
-registry["theory::explanation"] = str2int
-registry["theory::lemma"] = str2int
-registry["theory::propagate"] = str2int
-
-registry["cpu_percent"] = strpercent2float
-registry["exit_status"] = str2int
-registry["system_time"] = str2float
-registry["user_time"] = str2float
-registry["major_page_faults"] = str2float
-registry["minor_page_faults"] = str2int
-registry["average_unshared_memory"] = str2int
-registry["average_total_memory"] = str2int
-registry["maximum_resident_size"] = str2int
-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":
-        return True
-    elif up  == "SAT":
-        return True
-    else:
-        return False
-
-def addStat(db, name, result):
-    assert name in registry
-    interpreter = registry[name]
-
-    val = interpreter(result)
-    db.insert(name, val)
-
-def handleCoutFile(db, filename):
-    file = open(filename)
-    num_lines = 0
-    for line in file:
-        assert num_lines <= 2
-        num_lines += 1
-        if(isSatResult(line)):
-            continue
-        time_return = line.split()
-        # First word is 'empty' to distinguish the 'empty' output
-        addStat(db, "exit_status", time_return[1])
-        addStat(db, "system_time", time_return[2])
-        addStat(db, "user_time", time_return[3])
-        addStat(db, "cpu_percent", time_return[4])
-        addStat(db, "major_page_faults", time_return[5])
-        addStat(db, "minor_page_faults", time_return[6])
-        addStat(db, "average_unshared_memory", time_return[7])
-        addStat(db, "average_total_memory", time_return[8])
-        addStat(db, "maximum_resident_size", time_return[9])
-        addStat(db, "average_resident_size", time_return[10])
-    file.close()
-
-ignoreThese = ["Illegal instruction",
-               "Aborted",
-               "CVC4 interrupted by timeout.",
-               "CVC4 suffered a segfault.",
-               "ssh: Could not resolve hostname",
-               "Trace/breakpoint trap",
-               "Segmentation fault"]
-def ignoreFault(ln):
-    for ignore in ignoreThese:
-        if (ln.find(ignore) != -1):
-            return True
-    return False
-
-
-def handleLine(db, ln):
-    assert ln.strip() != ""
-    if isSatResult(ln):
-        addStat(db,"sat/unsat",ln)
-    elif (not ignoreFault(ln)):
-        (name,delim,result) = ln.partition(stat_name_delim)
-        assert delim != ""
-        addStat(db, name,result)
-
-def handleCerrFile(db, filename):
-    assert db.currentRowIsClear()
-    file = open(filename)
-    for line in file:
-        handleLine(db,line)
-    file.close()
-
-ignore_files = ["done", "done.err", "init", "init.err"]
-
-import os
-def handleDirectory(db, path):
-    files = os.listdir(path)
-    for name in files:
-        if name in ignore_files:
-            continue
-        if(not name.endswith(".err")):
-            errFile = name+".err"
-            handleCerrFile(db, path+'/'+errFile)
-            addStat(db, "id", name)
-            handleCoutFile(db, path+'/'+name)
-            db.commitRow()
-
-import sys
-
-dbfile = sys.argv[1]
-target = sys.argv[2]
-
-assert os.path.exists(dbfile)
-assert os.path.exists(target)
-
-db = readDatabase(dbfile)
-
-if os.path.isdir(target):
-    handleDirectory(db, target)
-else:
-    handleFile(db, target)
-    db.commitRow()
-
-db.writeDB(sys.stdout, regOrder)