Added post_mortem.py a statistics collector for user with the smt_curnch cluster. Also a spelling correction for the statistic theory::conflict.

2 files changed, 213 insertions, 1 deletions

diff --git a/contrib/post_mortem.py b/contrib/post_mortem.py
new file mode 100644
index 000000000..e0fe2b9d4
--- /dev/null
+++ b/contrib/post_mortem.py
@@ -0,0 +1,212 @@
+
+
+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):
+        assert self.currentRowIsClear()
+        file.write("#")
+        first = True
+        for name in registry:
+            if first:
+                first = False
+            else:
+                file.write(",")
+            file.write(name)
+
+        file.write("\n")
+        for row in self.rows:
+            first = True
+            for name in registry:
+                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::UpdateConflicts"] = 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 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()
+
+
+def handleLine(db, ln):
+    assert ln.strip() != ""
+    if isSatResult(ln):
+        addStat(db,"sat/unsat",ln)
+    else:
+        (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)
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index bf4d8d10c..c2511f4e6 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -335,7 +335,7 @@ private:
   public:
     IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanatation;
     Statistics():
-      d_statConflicts("theory::conlficts",0),
+      d_statConflicts("theory::conflicts",0),
       d_statPropagate("theory::propagate",0),
       d_statLemma("theory::lemma",0),
       d_statAugLemma("theory::aug_lemma", 0),