Merge branch 'SMT-COMP:master' into master

Author: Heizmann

.gitignore

@@ -170,3 +170,4 @@ cython_debug/
 schema_doc.css
 schema_doc.min.js
 *.feather
+tmp/

README.md

@@ -1,4 +1,4 @@
-# smtcomp
+# SMT Competition
 
 [![Release](https://img.shields.io/github/v/release/smtcomp/smtcomp.github.io)](https://img.shields.io/github/v/release/smtcomp/smtcomp.github.io)
 [![Build status](https://img.shields.io/github/actions/workflow/status/smtcomp/smtcomp.github.io/main.yml?branch=main)](https://github.com/smtcomp/smtcomp.github.io/actions/workflows/main.yml?query=branch%3Amain)
@@ -38,7 +38,7 @@ make install
 
 ## For starting a new SMT-COMP year
 
-Edit the file `smtcomp/defs.py`, in particular `Config.current_year`, `Logic` for adding new logics and `tracks` for new divisions.
+Edit the file `smtcomp/defs.py`, in particular `Config.current_year`, `Logic` for adding new logics and `tracks` for new divisions. Reset `Config.NYSE_seed` to `None`, and set the date the New York Stock Exchange Index will be used in `Config.NYSE_date`.
 
 Download the new benchmarks from zenodo, unpack them, unpack the .tar.zst, you should get something like:
 
@@ -74,10 +74,9 @@ smtcomp create-benchmarks-list $DIR/zenodo ./data/
 
 The directory `./data/` is the one present in this repository.
 
-## Using the smtcomp tool for selecting the benchmarks
+## Using the `smtcomp` tool for selecting the benchmarks
 
-The list of benchmarks and the previous results are in json which are human
-readable, but slow to parse (1min). So locally the tool use the feather format. The
+The list of benchmarks and the previous results are in `json` which are human-readable, but slow to parse (1min). So locally the tool use the feather format. The
 feather files are generated with:
 
 ```
@@ -87,7 +86,7 @@ smtcomp create-cache ./data/
 Working with the feather files with [polars](https://docs.pola.rs/) is very fast,
 so no more intermediate files are needed.
 
-However statistics can be shown, for example for the selection of single track:
+However, statistics can be shown, for example for the selection of single track:
 
 ```
 smtcomp show-sq-selection-stats ./data/ 0
@@ -110,7 +109,7 @@ Which outputs:
 ...
 ```
 
-## Using the smtcomp tool for generating benchexec
+## Using the `smtcomp` tool for generating `benchexec` configuration
 
 #### Generate submissions [Optional]
 
@@ -129,37 +128,37 @@ smtcomp show ../tmp/submissions/YicesQS.json
 The solver downloaded using:
 
 ```
-smtcomp download-archive ../tmp/submissions/*.json ../tmp/benchexec/execution
+smtcomp download-archive submissions/*.json ../tmp/execution
 ```
 
 Trivial tests benchmarks generated with:
 
 ```
-smtcomp generate-benchmarks ../tmp/benchexec/includes/
+smtcomp generate-trivial-benchmarks ../tmp/execution/benchmarks
 ```
 
 The benchexec tasks generated using:
 
 ```
-smtcomp generate-benchexec ../tmp/submissions/*.json ../tmp/benchexec/includes/all.xml ../tmp/benchexec/execution
+smtcomp generate-benchexec submissions/*.json ../tmp/execution
 ```
 
 The benchexec execution environment generated using:
 
 ```
-smtcomp prepare-execution ../tmp/benchexec/execution
+smtcomp prepare-execution ../tmp/execution
 ```
 
 Benchexec started using:
 
 ```
-(cd ../tmp/benchexec/execution; benchexec ../includes/all.xml  --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1)
+(cd ../tmp/execution; PYTHONPATH=$(pwd) benchexec SOLVERNAME.xml --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1)
 ```
 
 Benchexec in verifier cloud started using:
 
 ```
-(cd ../tmp/benchexec/execution; PATH_TO_BENCHEXEC/contrib/vcloud-benchmark.py ../includes/all.xml  --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1 --vcloudMaster VCLOUD_MASTER --vcloudClientHeap 500)
+(cd ../tmp/execution; PYTHONPATH=$(pwd) PATH_TO_BENCHEXEC/contrib/vcloud-benchmark.py SOLVERNAME.xml --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1 --vcloudMaster VCLOUD_MASTER --vcloudClientHeap 500)
 ```
 
 ---

smtcomp/archive.py

@@ -38,6 +38,10 @@ def is_unpack_present(archive: defs.Archive, dst: Path) -> bool:
     return any(True for _ in d.iterdir())
 
 
+def command_path(command: defs.Command, archive: defs.Archive, dst: Path) -> Path:
+    return archive_unpack_dir(archive, dst).joinpath(command.binary)
+
+
 def find_command(command: defs.Command, archive: defs.Archive, dst: Path) -> Path:
     d = archive_unpack_dir(archive, dst)
     if not (d.exists()):
@@ -101,3 +105,17 @@ def unpack(archive: defs.Archive, dst: Path) -> None:
     if not (is_unpack_present(archive, dst)):
         print("[red]Empty archive", archive_file)
         exit(1)
+
+
+def download_unpack(s: defs.Submission, dst: Path) -> None:
+    """
+    Download and unpack
+    """
+    dst.mkdir(parents=True, exist_ok=True)
+    if s.archive:
+        download(s.archive, dst)
+        unpack(s.archive, dst)
+    for p in s.participations.root:
+        if p.archive:
+            download(p.archive, dst)
+            unpack(p.archive, dst)

smtcomp/benchexec.py

@@ -1,14 +1,40 @@
 from pathlib import Path
+import rich
 from os.path import relpath
 from typing import List, cast, Dict, Optional
 
 from yattag import Doc, indent
 
 from smtcomp import defs
-from smtcomp.archive import find_command
+from smtcomp.archive import find_command, archive_unpack_dir, command_path
 from pydantic import BaseModel
 
 import shlex
+from re import sub
+
+
+def get_suffix(track: defs.Track) -> str:
+    match track:
+        case defs.Track.Incremental:
+            return "_inc"
+        case defs.Track.ModelValidation:
+            return "_model"
+        case defs.Track.UnsatCore:
+            return "_unsatcore"
+        case defs.Track.SingleQuery:
+            return ""
+        case _:
+            raise ValueError("No Cloud or Parallel")
+
+
+def get_xml_name(s: defs.Submission, track: defs.Track) -> str:
+    suffix = get_suffix(track)
+    return sub(r"\W+", "", s.name.lower()) + suffix + ".xml"
+
+
+def tool_module_name(s: defs.Submission, incremental: bool) -> str:
+    suffix = "_inc" if incremental else ""
+    return sub(r"\W+", "", s.name.lower()) + suffix
 
 
 class CmdTask(BaseModel):
@@ -17,7 +43,66 @@ class CmdTask(BaseModel):
     includesfiles: List[str]
 
 
-def generate_xml(timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: List[CmdTask], file: Path) -> None:
+def generate_benchmark_yml(benchmark: Path, expected_result: Optional[bool], orig_file: Optional[Path]) -> None:
+    ymlfile = benchmark.with_suffix(".yml")
+    with ymlfile.open("w") as f:
+        f.write("format_version: '2.0'\n\n")
+
+        f.write(f"input_files: '{str(benchmark.name)}'\n\n")
+
+        if orig_file is not None:
+            f.write(f"# original_files: '{str(orig_file)}'\n\n")
+
+        expected_str = "true" if expected_result else "false"
+        f.write("properties:\n")
+        f.write(f"  - property_file: '../../properties/SMT.prp'\n")
+        if expected_result is not None:
+            f.write(f"    expected_verdict: {expected_str}\n")
+
+
+def generate_tool_module(s: defs.Submission, cachedir: Path, incremental: bool) -> None:
+    name = tool_module_name(s, incremental)
+    file = cachedir / "tools" / f"{name}.py"
+
+    with file.open("w") as f:
+        if incremental:
+            base_module = "incremental_tool"
+            base_class = "IncrementalSMTCompTool"
+        else:
+            base_module = "tool"
+            base_class = "SMTCompTool"
+        f.write(f"from tools.{base_module} import {base_class}\n\n")
+        f.write(f"class Tool({base_class}):  # type: ignore\n")
+
+        f.write(f"    NAME = '{s.name}'\n")
+        if s.command is not None:
+            assert s.archive is not None
+            if s.command.compa_starexec:
+                executable_path = find_command(s.command, s.archive, cachedir)
+                executable = str(relpath(executable_path, start=str(cachedir)))
+            else:
+                executable = str(command_path(s.command, s.archive, Path()))
+            f.write(f"    EXECUTABLE = '{executable}'\n")
+
+        required_paths = []
+
+        if s.archive is not None:
+            archive_path = relpath(archive_unpack_dir(s.archive, cachedir), start=str(cachedir))
+            required_paths.append(str(archive_path))
+        for p in s.participations.root:
+            if p.archive is not None:
+                archive_path = relpath(archive_unpack_dir(p.archive, cachedir), start=str(cachedir))
+                required_paths.append(str(archive_path))
+        if required_paths:
+            f.write(f"    REQUIRED_PATHS = {required_paths}\n")
+
+
+def generate_tool_modules(s: defs.Submission, cachedir: Path) -> None:
+    generate_tool_module(s, cachedir, True)
+    generate_tool_module(s, cachedir, False)
+
+
+def generate_xml(config: defs.Config, cmdtasks: List[CmdTask], file: Path, tool_module_name: str) -> None:
     doc, tag, text = Doc().tagtext()
 
     doc.asis('<?xml version="1.0"?>')
@@ -27,13 +112,18 @@ def generate_xml(timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: Lis
     )
     with tag(
         "benchmark",
-        tool=f"smtcomp.tool",
-        timelimit=f"{timelimit_s}s",
-        hardlimit=f"{timelimit_s+30}s",
-        memlimit=f"{memlimit_M} MB",
-        cpuCores=f"{cpuCores}",
-        displayname="SC",
+        tool=f"tools.{tool_module_name}",
+        timelimit=f"{config.timelimit_s}s",
+        hardlimit=f"{config.timelimit_s+30}s",
+        memlimit=f"{config.memlimit_M} MB",
+        cpuCores=f"{config.cpuCores}",
     ):
+        with tag("require", cpuModel="Intel Xeon E3-1230 v5 @ 3.40 GHz"):
+            text()
+
+        with tag("resultfiles"):
+            text("**/error.log")
+
         for cmdtask in cmdtasks:
             for includesfile in cmdtask.includesfiles:
                 with tag("rundefinition", name=f"{cmdtask.name},{includesfile}"):
@@ -42,71 +132,70 @@ def generate_xml(timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: Lis
                             text(option)
                     with tag("tasks", name="task"):
                         with tag("includesfile"):
-                            text(includesfile)
+                            text(f"benchmarks/{includesfile}")
+
+        with tag("propertyfile"):
+            text("benchmarks/properties/SMT.prp")
 
     file.write_text(indent(doc.getvalue()))
 
 
-def cmdtask_for_submission(s: defs.Submission, cachedir: Path) -> List[CmdTask]:
+def cmdtask_for_submission(s: defs.Submission, cachedir: Path, target_track: defs.Track) -> List[CmdTask]:
     res: List[CmdTask] = []
     i = -1
     for p in s.participations.root:
         command = cast(defs.Command, p.command if p.command else s.command)
         archive = cast(defs.Archive, p.archive if p.archive else s.archive)
         for track, divisions in p.get().items():
+            if track != target_track:
+                continue
+
             i = i + 1
-            match track:
-                case defs.Track.Incremental:
-                    suffix = "_inc"
-                    mode = "trace"
-                case defs.Track.ModelValidation:
-                    suffix = "_model"
-                    mode = "direct"
-                case defs.Track.UnsatCore:
-                    suffix = ""
-                    mode = "direct"
-                case defs.Track.ProofExhibition:
-                    suffix = ""
-                    mode = "direct"
-                case defs.Track.SingleQuery:
-                    suffix = ""
-                    mode = "direct"
-                case defs.Track.Cloud | defs.Track.Parallel:
-                    continue
+            suffix = get_suffix(track)
             tasks: list[str] = []
             for _, logics in divisions.items():
                 tasks.extend([str(logic) + suffix for logic in logics])
             if tasks:
-                executable_path = find_command(command, archive, cachedir)
-                executable = str(relpath(executable_path, start=str(cachedir)))
                 if command.compa_starexec:
                     assert command.arguments == []
+                    executable_path = find_command(command, archive, cachedir)
+                    executable = str(relpath(executable_path, start=str(cachedir)))
                     dirname = str(relpath(executable_path.parent, start=str(cachedir)))
 
-                    if mode == "direct":
-                        options = [
-                            "bash",
-                            "-c",
-                            f'FILE=$(realpath $1); (cd {shlex.quote(dirname)}; exec ./{shlex.quote(executable_path.name)} "$FILE")',
-                            "compa_starexec",
-                        ]
-                    else:
-                        assert mode == "trace"
-                        options = [
-                            "bash",
-                            "-c",
-                            f'ROOT=$(pwd); FILE=$(realpath $1); (cd {shlex.quote(dirname)}; exec $ROOT/smtlib2_trace_executor ./{shlex.quote(executable_path.name)} "$FILE")',
-                            "compa_starexec",
-                        ]
+                    options = [
+                        "bash",
+                        "-c",
+                        f'FILE=$(realpath $1); (cd {shlex.quote(dirname)}; exec ./{shlex.quote(executable_path.name)} "$FILE")',
+                        "compa_starexec",
+                    ]
                 else:
-                    if mode == "direct":
-                        options = [executable] + command.arguments
-                    else:
-                        options = ["./smtlib2_trace_executor", executable] + command.arguments
+                    executable = str(command_path(command, archive, Path()))
+                    options = [executable] + command.arguments
                 cmdtask = CmdTask(
                     name=f"{s.name},{i},{track}",
                     options=options,
                     includesfiles=tasks,
                 )
                 res.append(cmdtask)
     return res
+
+
+def generate(s: defs.Submission, cachedir: Path, config: defs.Config) -> None:
+    generate_tool_modules(s, cachedir)
+
+    for target_track in [
+        defs.Track.SingleQuery,
+        defs.Track.Incremental,
+        defs.Track.ModelValidation,
+        defs.Track.UnsatCore,
+    ]:
+        res = cmdtask_for_submission(s, cachedir, target_track)
+        if res:
+            basename = get_xml_name(s, target_track)
+            file = cachedir / basename
+            generate_xml(
+                config=config,
+                cmdtasks=res,
+                file=file,
+                tool_module_name=tool_module_name(s, target_track == defs.Track.Incremental),
+            )