X-Git-Url: https://git.siccegge.de//index.cgi?p=master%2Fcool-versuchung.git;a=blobdiff_plain;f=cool.py;h=63e364d18e73506968f2bc8021afaa25ddc42f22;hp=0c90acf2725f707828e150c8902d1d1c4bec6808;hb=HEAD;hpb=ab6a62127469f9f14bc9bac27da1df189bc9b6f1 diff --git a/cool.py b/cool.py index 0c90acf..63e364d 100755 --- a/cool.py +++ b/cool.py @@ -13,18 +13,20 @@ import re import os import glob import argparse +import subprocess def natural_key(string_): return [int(s) if s.isdigit() else s for s in re.split(r'(\d+)', string_)] def parse_timedelta(strrep): minutes, seconds = strrep.split(":") - return seconds + 60 * minutes + return float(seconds) + 60 * float(minutes) class SolverExperiment(Experiment): inputs = { 'formulas' : TarArchive() } - outputs = { 'timing' : Directory() } + outputs = { 'output' : Directory('output'), + 'timing' : CSV_File('timing.csv') } def build_solver(self): @@ -35,17 +37,33 @@ class SolverExperiment(Experiment): pass + def execute_timed(self, formula, command, **kwargs): + with self.outputs.output as directory: + with open(os.path.join(directory, '%s_stdout' % formula), 'w') as stdoutfd: + with open(os.path.join(directory, '%s_stderr' % formula), 'w') as stderrfd: + p = subprocess.Popen(command, stdout=stdoutfd, stderr=stderrfd, **kwargs) + _pid, ret, ru = os.wait4(p.pid, 0) + p.wait() + + if ret != 0: + raise CommandFailed(command, ret) + + self.outputs.timing.append([formula, ru.ru_utime, ru.ru_maxrss]) + return ret + + def run(self): print("Building Solver ...") self.build_solver() - formulas = sorted(os.listdir(self.inputs.formulas.path), key=natural_key) - shell.track(self.outputs.timing.path) - for formula in formulas: - print("Running for %s ..." % formula) - try: - self.run_solver(os.path.join(self.inputs.formulas.path, formula)) - except CommandFailed: - break + with self.inputs.formulas as path: + formulas = sorted(os.listdir(path), key=natural_key) + + for formula in formulas: + print("Running for %s ..." % formula) + try: + self.run_solver(os.path.join(path, formula)) + except CommandFailed: + break @@ -67,8 +85,11 @@ class CoolExperiment(SolverExperiment): def run_solver(self, formula): with self.inputs.cool as path: - shell("timeout 1001 ./coalg.native sat KD --verbose < %s" % formula) - + executable = os.path.join(path, 'coalg.native') + self.execute_timed(os.path.basename(formula), + "timeout 1000 %s sat KD --verbose < %s" + % (executable, formula), + shell=True) class TreeTabExperiment(SolverExperiment): @@ -89,7 +110,11 @@ class TreeTabExperiment(SolverExperiment): def run_solver(self, formula): with self.inputs.treetab as path: - shell("timeout 1001 ./ctl tree --verbose < %s" % formula) + executable = os.path.join(path, 'ctl') + self.execute_timed(os.path.basename(formula), + "timeout 1001 %s tree --verbose < %s" + % (executable, formula), + shell=True) class GMULExperiment(SolverExperiment): @@ -110,16 +135,22 @@ class GMULExperiment(SolverExperiment): def run_solver(self, formula): with self.inputs.gmul as path: - shell("timeout 1001 ./ctl tr --verbose < %s" % formula) + executable = os.path.join(path, 'ctl') + self.execute_timed(os.path.basename(formula), + "timeout 1001 %s tr --verbose < %s" + % (executable, formula), + shell=True) class ComparisonExperiment(Experiment): outputs = { 'cool_data' : CSV_File('cool.csv'), 'treetab_data' : CSV_File('treetab.csv'), + 'gmul_data' : CSV_File('gmul.csv'), 'graphs' : Directory('graphs') } inputs = { 'cool' : CoolExperiment(), - 'treetab' : TreeTabExperiment() + 'treetab' : TreeTabExperiment(), + 'gmul' : GMULExperiment() } def folder_to_csv(self, folder, csv): @@ -135,6 +166,7 @@ class ComparisonExperiment(Experiment): command = command.split("<")[1].strip().strip('"') formula = os.path.basename(command) time = parse_timedelta(timeline.split(": ")[1].strip()) + time = time if time > 0 else 0.001 memory = memoryline.split(": ")[1].strip() csv.append([formula, time, memory]) csv.flush() @@ -143,6 +175,7 @@ class ComparisonExperiment(Experiment): def run(self): self.folder_to_csv(self.inputs.cool.timing.path, self.outputs.cool_data) self.folder_to_csv(self.inputs.treetab.timing.path, self.outputs.treetab_data) + self.folder_to_csv(self.inputs.gmul.timing.path, self.outputs.gmul_data) with self.outputs.graphs as path: # Time @@ -150,14 +183,19 @@ class ComparisonExperiment(Experiment): os.path.basename(self.inputs.treetab.metadata['formulas'])) plt.yscale('log') plt.ylabel('time / s') + plt.ylim(0.001, 10000) plt.xlabel('problem size') - plt.plot(range(1,21), + plt.plot([x[0].split('.')[1] for x in self.outputs.cool_data.value], [x[1] for x in self.outputs.cool_data.value], 'bo', label="cool") - plt.plot(range(1,21), + plt.plot([x[0].split('.')[1] for x in self.outputs.treetab_data.value], [x[1] for x in self.outputs.treetab_data.value], 'gv', label="TreeTab") - plt.legend() + plt.plot([x[0].split('.')[1] for x in self.outputs.gmul_data.value], + [x[1] for x in self.outputs.gmul_data.value], + 'r*', label="GMUL") + + plt.legend(loc=2) plt.savefig('time.svg', format='svg') plt.close() @@ -167,13 +205,17 @@ class ComparisonExperiment(Experiment): plt.yscale('log') plt.ylabel('memory / kB') plt.xlabel('problem size') - plt.plot(range(1,21), + plt.plot([x[0].split('.')[1] for x in self.outputs.cool_data.value], [x[2] for x in self.outputs.cool_data.value], 'bo', label="cool") - plt.plot(range(1,21), + plt.plot([x[0].split('.')[1] for x in self.outputs.treetab_data.value], [x[2] for x in self.outputs.treetab_data.value], 'gv', label="TreeTab") - plt.legend() + plt.plot([x[0].split('.')[1] for x in self.outputs.gmul_data.value], + [x[2] for x in self.outputs.gmul_data.value], + 'r*', label="GMUL") + + plt.legend(loc=2) plt.savefig('memory.svg', format='svg')