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):
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
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):
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):
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):
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()
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
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()
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')