#!/usr/bin/env python3 """ This script will produce the final value of a variable named 'objective' and its area for every file ending in '.sol' in the directory provided. The files are expected to be fzn-gecode output piped through solns2out with the '--output-time' flag. Furthermore the file is expected to contain the initial area which can be found by adding 'constraint trace("% init_area = \(ub(objective));\n", true);' to the model in question. """ import csv import os import re import sys def compute_area(file): area = -1 objectives = [] times = [0] timeout = -1 objectives.append(0) for line in contents: # match = re.match(r'%\sinit_area\s=\s(\d+)', line) # if match: # objectives.append(int(match[1])) # continue match = re.match(r"objective\s=\s(\d+)", line) if match: objectives.append(int(match[1])) continue match = re.match(r"%\stime elapsed:\s(\d+)\sms", line) if match: times.append(int(match[1])) continue match = re.search(r"solvetime:.*\((\d+).(\d+)\s+ms\)", line) if match: times.append(int(match.group(1))) continue assert len(objectives) > 0 assert len(objectives) + 1 == len(times) area = 0 for i in range(len(objectives)): area += ((times[i + 1] - times[i]) / 1000) * objectives[i] return int(area) foler = sys.argv[1] statistics = {} for root, dirs, files in os.walk(folder): for name in files: if name.endswith(".sol"): seed = 1 match = re.search(r"\.(\d+)\.sol", name) if match: seed = int(match.group(1)) with open(os.path.join(root, name)) as f: contents = f.readlines() # Area area = compute_area(contents) objective = "UNSAT" for line in contents[::-1]: # Best objective match = re.match(r"objective\s=\s(\d+)", line) if match: objective = int(match[1]) break nodes = -1 solvetime = -1 restarts = -1 for line in contents: # Evaluation time match = re.search(r"copies:\s+(\d+)", line) if match: nodes = int(match.group(1)) continue # Solve time match = re.search(r"solvetime:.*\((\d+).(\d+)\s+ms\)", line) if match: solvetime = int(match.group(1)) continue # Restarts match = re.search(r"restarts:\s+(\d+)", line) if match: restarts = int(match.group(1)) continue statistics[name[:-(4)].replace(".", ",")] = ( area, objective, solvetime, restarts, nodes, ) sorted_stats = sorted(statistics.items()) a = sorted_stats[0][0][: sorted_stats[0][0].find(",")] for key, val in sorted_stats: if key[: key.find(",")] != a: print("\n\n") a = key[: key.find(",")] print("%s,%s" % (key, ",".join([v.__str__() for v in val]))) exit(1)