cool.py

   1 #!/usr/bin/env python3
   2
   3 from versuchung.experiment import Experiment
   4 from versuchung.archives import TarArchive, GitArchive
   5 from versuchung.files import Directory
   6 from versuchung.execute import shell, CommandFailed
   7
   8 import re
   9 import os
  10
  11 def natural_key(string_):
  12     return [int(s) if s.isdigit() else s for s in re.split(r'(\d+)', string_)]
  13
  14
  15 class SolverExperiment(Experiment):
  16     inputs = { 'formulas' : TarArchive() }
  17     outputs = { 'timing' : Directory() }
  18
  19
  20     def build_solver(self):
  21         pass
  22
  23
  24     def run_solver(self, formula):
  25         pass
  26
  27
  28     def run(self):
  29         print("Building Solver ...")
  30         self.build_solver()
  31         formulas = sorted(os.listdir(self.inputs.formulas.path), key=natural_key)
  32         shell.track(self.outputs.timing.path)
  33         for formula in formulas:
  34             print("Running for %s ..." % formula)
  35             try:
  36                 self.run_solver(os.path.join(self.inputs.formulas.path, formula))
  37             except CommandFailed:
  38                 break
  39
  40
  41
  42 class CoolExperiment(SolverExperiment):
  43     inputs = { 'cool' : GitArchive() }
  44     outputs = {}
  45
  46
  47     def __init__(self):
  48         CoolExperiment.inputs.update(SolverExperiment.inputs)
  49         CoolExperiment.outputs.update(SolverExperiment.outputs)
  50         super(CoolExperiment, self).__init__()
  51
  52
  53     def build_solver(self):
  54         with self.inputs.cool as path:
  55             shell("make")
  56
  57
  58     def run_solver(self, formula):
  59         with self.inputs.cool as path:
  60             shell("timeout 1001 ./coalg.native sat KD --verbose < %s" % formula)
  61
  62
  63
  64 class TreeTabExperiment(SolverExperiment):
  65     inputs = { 'treetab' : TarArchive('ctlProver_r1368.tar') }
  66     outputs = {}
  67
  68
  69     def __init__(self):
  70         TreeTabExperiment.inputs.update(SolverExperiment.inputs)
  71         TreeTabExperiment.outputs.update(SolverExperiment.outputs)
  72         super(TreeTabExperiment, self).__init__()
  73
  74
  75     def build_solver(self):
  76         with self.inputs.treetab as path:
  77             shell("make")
  78
  79
  80     def run_solver(self, formula):
  81         with self.inputs.treetab as path:
  82             shell("timeout 1001 ./ctl tree --verbose < %s" % formula)
  83
  84
  85 class GMULExperiment(SolverExperiment):
  86     inputs = { 'gmul' : TarArchive('ctlgraph.tar') }
  87     outputs = {}
  88
  89
  90     def __init__(self):
  91         GMULExperiment.inputs.update(SolverExperiment.inputs)
  92         GMULExperiment.outputs.update(SolverExperiment.outputs)
  93         super(GMULExperiment, self).__init__()
  94
  95
  96     def build_solver(self):
  97         with self.inputs.gmul as path:
  98             shell("make")
  99
 100
 101     def run_solver(self, formula):
 102         with self.inputs.gmul as path:
 103             shell("timeout 1001 ./ctl tr --verbose < %s" % formula)
 104
 105
 106 if __name__ == "__main__":
 107     import sys
 108     experiment = CoolExperiment()
 109     dirname = experiment(sys.argv)
 110
 111     print(dirname)