Use own, more advanced timing

diff --git a/cool.py b/cool.py
index d8dd0930fe292ed975b163596996664f093f737b..e64929f26516487cac348146884cd52e1c73835b 100755 (executable)
--- a/cool.py
+++ b/cool.py
@@ -13,6 +13,7 @@ import re
 import os
 import glob
 import argparse
 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 natural_key(string_):
     return [int(s) if s.isdigit() else s for s in re.split(r'(\d+)', string_)]


@@ -24,7 +25,8 @@ def parse_timedelta(strrep):
 
 class SolverExperiment(Experiment):
     inputs = { 'formulas' : TarArchive() }
 
 class SolverExperiment(Experiment):
     inputs = { 'formulas' : TarArchive() }

-    outputs = { 'timing' : Directory() }
+    outputs = { 'output' : Directory('output'),
+                'timing' : CSV_File('timing.csv') }

 
 
     def build_solver(self):
 
 
     def build_solver(self):


@@ -35,17 +37,30 @@ class SolverExperiment(Experiment):
         pass
 
 
         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)
     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:
 
             for formula in formulas:
                 print("Running for %s ..." % formula)
                 try:

-

                     self.run_solver(os.path.join(path, formula))
                 except CommandFailed:
                     break
                     self.run_solver(os.path.join(path, formula))
                 except CommandFailed:
                     break


@@ -70,8 +85,11 @@ class CoolExperiment(SolverExperiment):
 
     def run_solver(self, formula):
         with self.inputs.cool as path:
 
     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):
 
 
 class TreeTabExperiment(SolverExperiment):


@@ -92,7 +110,11 @@ class TreeTabExperiment(SolverExperiment):
 
     def run_solver(self, formula):
         with self.inputs.treetab as path:
 
     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):
 
 
 class GMULExperiment(SolverExperiment):


@@ -113,7 +135,11 @@ class GMULExperiment(SolverExperiment):
 
     def run_solver(self, formula):
         with self.inputs.gmul as path:
 
     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):
 
 
 class ComparisonExperiment(Experiment):