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_)]
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()
with self.inputs.formulas as path:
formulas = sorted(os.listdir(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(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):