From: Tim King Date: Thu, 4 Nov 2010 16:30:25 +0000 (+0000) Subject: Moving the post_mortem.py script out of contrib and into the cvc4 scripts directory. X-Git-Tag: cvc5-1.0.0~8747 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d837718bfa4a2b8cb46add5f1c510b0d2a7785f5;p=cvc5.git 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 index ccba084a5..000000000 --- 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)