Add finalization script

- Add tool to convert CSV schedules to scripts
- Use Jinja2 templating system to do this
- Add Jinja2 as dependency to setup.py and shell.nix
- Mark old options to print full schedule as obsolete
- Fix small typo in optimization tool

contrib/scheduler_template

 #!/usr/bin/env bash
 
-exec=./veriT
+exec={{ executable }}
 problem="$1"
-#memory=60000000
 
 logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$problem")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
 
@@ -21,7 +20,15 @@ function finishwith {
 }
 
 case "$logic" in
-REPLACEME
+    {% for logic in logics %}
+    {{ logic }})
+        {% for time,strategy in schedules[logic] -%}
+        {%- if loop.last -%}
+            finishwith	{{ strategy }}
+        ;;
+        {% else %}trywith	{{ (time*1000)|int }}	{{ strategy }}
+        {% endif -%}
+    {%- endfor -%}{%- endfor %}
     *)
         finishwith
         ;;
@@ -29,14 +36,3 @@ esac
 
 # Configuration script structure adapted from CVC4's configuration for SMTCOMP 2015
 
-#function trywith {
-#    limit=$1; shift;
-#    output="$(ulimit -S -v $memory -t "$limit";$exec --disable-banner --disable-print-success "$@" $problem 2>&1)"
-#    result="$(grep -m 1 "unsat\|sat" <<< $result)"
-#    if [[ ${result} ]]
-#    then
-#        echo "$result"
-#        exit 0
-#    fi
-#}
-

schedgen/opt/schedule.py

@@ -15,11 +15,12 @@ def read_from_file(csvfile):
     for the timeout (floating point in seconds).
     """
     schedule = []
-    reader = csv.DictReader(csvfile, delimiter=";")
-    for row in reader:
-        time = float(row["time"].strip())
-        strategy = row["strategy"]
-        schedule.append((time, strategy))
+    with open(csvfile) as openfile:
+        reader = csv.DictReader(openfile, delimiter=";")
+        for row in reader:
+            time = float(row["time"].strip())
+            strategy = row["strategy"]
+            schedule.append((time, strategy))
     return schedule
 
 

schedgen/schedgen-finalize.py

+#!/usr/bin/env python3
+
+import argparse
+import jinja2
+
+from schedgen.opt.schedule import read_from_file
+from schedgen.opt.helper import message, file_or_dir_path, new_file_path, file_path
+
+args_parser = argparse.ArgumentParser(
+    description="Transforms a set of pre-schedules into a scheduling script."
+)
+
+args_parser.add_argument(
+    "-l",
+    "--logics",
+    dest="logics",
+    metavar="L",
+    nargs="*",
+    default=["UF"],
+    type=str,
+    help="A list of logics.  One for for each schedule.",
+)
+args_parser.add_argument(
+    "-s",
+    "--pre-schedules",
+    metavar="FILE",
+    dest="schedules",
+    help="The pre-schedulers as files.  As many as there are logics given",
+    nargs="*",
+    default=["schedule.csv"],
+    type=file_path,
+)
+args_parser.add_argument(
+    "--timeout",
+    metavar="TIMEOUT",
+    dest="timeout",
+    help="Total time available to the schedules.  Exposed to the template.",
+    default=None,
+    type=float,
+)
+args_parser.add_argument(
+    "--executable",
+    metavar="EXECUTABLE",
+    dest="executable",
+    help="Path of the executable of the solver.  Exposed to the template.",
+    default=None,
+    type=str,
+)
+args_parser.add_argument(
+    metavar="TEMPLATE",
+    dest="template",
+    help="Template for the schedule script.",
+    type=file_path,
+)
+args_parser.add_argument(
+    metavar="OUTPUT",
+    dest="output",
+    help="File name to write the generated file into.",
+    type=new_file_path,
+)
+
+
+if __name__ == "__main__":
+    args = args_parser.parse_args()
+    logics = args.logics
+    message(f"Logics: {logics}", logics)
+    pre_schedules = args.schedules
+    message(f"Pre-schedules: {pre_schedules}", logics)
+    message(f"Template: {args.template}", logics)
+
+    if len(logics) != len(pre_schedules):
+        message("Error: number of logics does not match number of schedules.", logics)
+        exit(1)
+
+    # schedules are a list of (time, strategy) tuples
+    schedules = [read_from_file(f) for f in pre_schedules]
+
+    dir = args.template.parent
+    env = jinja2.Environment(
+        loader=jinja2.FileSystemLoader(dir), autoescape=jinja2.select_autoescape(["html", "xml"])
+    )
+    template = env.get_template(args.template.name)
+
+    referencedSchedules = {}
+    for i in range(len(logics)):
+        referencedSchedules[logics[i]] = schedules[i]
+
+    rendered = template.render(
+        logics=logics,
+        schedules=referencedSchedules,
+        timeout=args.timeout,
+        executable=args.executable,
+    )
+    with open(args.output, "w") as outputFile:
+        outputFile.write(rendered)
+
+    message("All done.", logics)

schedgen/schedgen-optimize.py

@@ -74,13 +74,13 @@ args_parser.add_argument(
     "-f",
     "--full",
     dest="full",
-    help="Write full script instead of CSV file.",
+    help="Write full script instead of CSV file (obsolet).",
     action="store_true",
 )
 args_parser.add_argument(
     "-z",
     dest="seconds_out",
-    help="Write seconds not milliseconds.",
+    help="Write seconds not milliseconds (obsolet).",
     action="store_true",
 )
 args_parser.add_argument(
@@ -154,7 +154,7 @@ def writeScript(outFile, logics, schedule, seconds=False):
 
 def writeCSV(outFile, logics, schedule):
     message(f"Writing CSV schedule to {outFile}.", logics)
-    with open(outFile, "w") as af:,
+    with open(outFile, "w") as af:
         af.write("time;strategy\n")
         for i in range(len(schedule)):
             (t, e) = schedule[i]

setup.py

@@ -28,10 +28,10 @@ setup(
     author_email="hans-jorg.schurr@inria.fr",
     python_requires=">=3.6.0",
     url="https://gitlab.inria.fr/hschurr/verit-schedgen",
-    install_requires=["pandas", "pulp", "numpy"],
+    install_requires=["pandas", "pulp", "numpy", "jinja2"],
     include_package_data=True,
     packages=["schedgen"],
-    scripts=["schedgen/schedgen-optimize.py"],
+    scripts=["schedgen/schedgen-optimize.py", "schedgen/schedgen-finalize.py"],
     license="BSD 3-Clause License",
     classifiers=[
         # Trove classifiers

shell.nix

@@ -17,13 +17,14 @@ pkgs.stdenv.mkDerivation {
   hardeningDisable = [ "all" ];
   buildInputs = with pkgs; [
       python3
-      python38Packages.pandas
-      python38Packages.pulp
-      python38Packages.numpy
-      python38Packages.setuptools
-      python38Packages.black
-      python38Packages.bootstrapped-pip
-      python38Packages.virtualenv
+      python39Packages.pandas
+      python39Packages.jinja2
+      python39Packages.pulp
+      python39Packages.numpy
+      python39Packages.setuptools
+      python39Packages.black
+      python39Packages.bootstrapped-pip
+      python39Packages.virtualenv
       cbc
       parallel ];