Merge branch 'master' into yices2

.gitignore

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

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()):

smtcomp/benchexec.py

@@ -6,13 +6,37 @@
 from yattag import Doc, indent
 
 from smtcomp import defs
-from smtcomp.archive import find_command, archive_unpack_dir
+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):
     name: str
     options: List[str]
@@ -36,35 +60,28 @@ def generate_benchmark_yml(benchmark: Path, expected_result: Optional[bool], ori
             f.write(f"    expected_verdict: {expected_str}\n")
 
 
-def tool_module_name(s: defs.Submission, track: defs.Track) -> str:
-    return sub(r"\W+", "", s.name.lower()) + get_suffix(track)
-
-
-def generate_tool_module(s: defs.Submission, cachedir: Path, track: defs.Track) -> None:
-    name = tool_module_name(s, track)
+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:
-        match track:
-            case defs.Track.Incremental:
-                base_module = "incremental_tool"
-                base_class = "IncrementalSMTCompTool"
-            case defs.Track.SingleQuery:
-                base_module = "tool"
-                base_class = "SMTCompTool"
-            case _:
-                rich.print(
-                    f"[red]generate_tool_module command does not yet work for the competition track: {track}[/red]"
-                )
-                exit(1)
+        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
-            executable_path = find_command(s.command, s.archive, cachedir)
-            executable = str(relpath(executable_path, start=str(cachedir)))
+            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 = []
@@ -80,8 +97,13 @@ def generate_tool_module(s: defs.Submission, cachedir: Path, track: defs.Track)
             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(
-    timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: List[CmdTask], cachedir: Path, tool_module_name: str
+    timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: List[CmdTask], file: Path, tool_module_name: str
 ) -> None:
     doc, tag, text = Doc().tagtext()
 
@@ -117,20 +139,9 @@ def generate_xml(
         with tag("propertyfile"):
             text("benchmarks/properties/SMT.prp")
 
-    file = cachedir.joinpath(f"{tool_module_name}.xml")
     file.write_text(indent(doc.getvalue()))
 
 
-def get_suffix(track: defs.Track) -> str:
-    match track:
-        case defs.Track.Incremental:
-            return "_inc"
-        case defs.Track.ModelValidation:
-            return "_model"
-        case _:
-            return ""
-
-
 def cmdtask_for_submission(s: defs.Submission, cachedir: Path, target_track: defs.Track) -> List[CmdTask]:
     res: List[CmdTask] = []
     i = -1
@@ -147,10 +158,10 @@ def cmdtask_for_submission(s: defs.Submission, cachedir: Path, target_track: def
             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)))
 
                     options = [
@@ -160,6 +171,7 @@ def cmdtask_for_submission(s: defs.Submission, cachedir: Path, target_track: def
                         "compa_starexec",
                     ]
                 else:
+                    executable = str(command_path(command, archive, Path()))
                     options = [executable] + command.arguments
                 cmdtask = CmdTask(
                     name=f"{s.name},{i},{track}",

smtcomp/defs.py

@@ -1351,6 +1351,10 @@ class Config:
     cpuCores = 4
     min_used_benchmarks = 300
     ratio_of_used_benchmarks = 0.5
+    use_previous_results_for_status = True
+    """
+    Complete the status given in the benchmarks using previous results
+    """
     old_criteria = False
     """"Do we try to emulate <= 2023 criteria that does not really follow the rules"""
     invert_triviality = False

smtcomp/execution.py

@@ -6,13 +6,11 @@
 
 
 def trace_executor_url() -> str:
-    return (
-        "https://github.com/SMT-COMP/trace-executor/releases/download/smtcomp2022/SMT-COMP-2022-trace-executor.tar.gz"
-    )
+    return "https://github.com/SMT-COMP/trace-executor/releases/download/smtcomp2024-rc1/SMT-COMP-2024-trace-executor.tar.gz"
 
 
 def trace_executor_filename() -> str:
-    return "SMT-COMP-2022-trace-executor.tar.gz"
+    return "SMT-COMP-2024-trace-executor.tar.gz"
 
 
 def download_trace_executor(dst: Path) -> None:

smtcomp/main.py

@@ -157,22 +157,32 @@ def generate_benchexec(
 ) -> None:
     """
     Generate the benchexec file for the given submissions
+
+    (The cachedir directory need to contain unpacked archive only with compa_starexec command)
     """
+    (cachedir / "tools").mkdir(parents=True, exist_ok=True)
     for file in track(files):
         s = submission.read(str(file))
+        benchexec.generate_tool_modules(s, cachedir)
 
-        for target_track in [defs.Track.SingleQuery, defs.Track.Incremental]:
-            tool_module_name = benchexec.tool_module_name(s, target_track)
-            benchexec.generate_tool_module(s, cachedir, target_track)
+        for target_track in [
+            defs.Track.SingleQuery,
+            defs.Track.Incremental,
+            defs.Track.ModelValidation,
+            defs.Track.UnsatCore,
+        ]:
+            tool_module_name = benchexec.tool_module_name(s, target_track == defs.Track.Incremental)
 
             res = benchexec.cmdtask_for_submission(s, cachedir, target_track)
             if res:
+                basename = benchexec.get_xml_name(s, target_track)
+                file = cachedir / basename
                 benchexec.generate_xml(
                     timelimit_s=timelimit_s,
                     memlimit_M=memlimit_M,
                     cpuCores=cpuCores,
                     cmdtasks=res,
-                    cachedir=cachedir,
+                    file=file,
                     tool_module_name=tool_module_name,
                 )
 
@@ -372,6 +382,7 @@ def show_sq_selection_stats(
     min_use_benchmarks: int = defs.Config.min_used_benchmarks,
     ratio_of_used_benchmarks: float = defs.Config.ratio_of_used_benchmarks,
     invert_triviality: bool = False,
+    use_previous_results_for_status: bool = defs.Config.use_previous_results_for_status,
 ) -> None:
     """
     Show statistics on the benchmarks selected for single query track
@@ -385,6 +396,7 @@ def show_sq_selection_stats(
     config.ratio_of_used_benchmarks = ratio_of_used_benchmarks
     config.invert_triviality = invert_triviality
     config.old_criteria = old_criteria
+    config.use_previous_results_for_status = use_previous_results_for_status
     benchmarks_with_info = smtcomp.selection.helper_compute_sq(config)
     b3 = (
         benchmarks_with_info.group_by(["logic"])
@@ -394,6 +406,8 @@ def show_sq_selection_stats(
             old_never_ran=pl.col("file").filter(run=False, new=False).len(),
             new=pl.col("new").sum(),
             selected=pl.col("file").filter(selected=True).len(),
+            selected_sat=pl.col("file").filter(selected=True, status=int(defs.Status.Sat)).len(),
+            selected_unsat=pl.col("file").filter(selected=True, status=int(defs.Status.Unsat)).len(),
             selected_already_run=pl.col("file").filter(selected=True, run=True).len(),
         )
         .sort(by="logic")
@@ -407,6 +421,8 @@ def show_sq_selection_stats(
     table.add_column("never compet.", justify="right", style="magenta")
     table.add_column("new", justify="right", style="magenta1")
     table.add_column("selected", justify="right", style="green3")
+    table.add_column("selected sat", justify="right", style="green4")
+    table.add_column("selected unsat", justify="right", style="green4")
     table.add_column("selected already run", justify="right", style="green4")
 
     used_logics = defs.logic_used_for_track(defs.Track.SingleQuery)
@@ -424,6 +440,8 @@ def show_sq_selection_stats(
             str(d["old_never_ran"]),
             str(d["new"]),
             str(d["selected"]),
+            str(d["selected_sat"]),
+            str(d["selected_unsat"]),
             str(d["selected_already_run"]),
         )
 
@@ -435,6 +453,8 @@ def show_sq_selection_stats(
         str(b3["old_never_ran"].sum()),
         str(b3["new"].sum()),
         str(b3["selected"].sum()),
+        str(b3["selected_sat"].sum()),
+        str(b3["selected_unsat"].sum()),
         str(b3["selected_already_run"].sum()),
     )
 
@@ -587,13 +607,17 @@ def read_submission(file: Path) -> defs.Submission:
             for part in sub.complete_participations():
                 for track, divisions in part.tracks.items():
                     match track:
-                        case defs.Track.Incremental:
-                            statuses = [defs.Status.Sat, defs.Status.Unsat]
                         case defs.Track.ModelValidation:
                             statuses = [defs.Status.Sat]
                         case defs.Track.SingleQuery:
                             statuses = [defs.Status.Sat, defs.Status.Unsat]
-                        case defs.Track.UnsatCore | defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel:
+                        case (
+                            defs.Track.Incremental
+                            | defs.Track.UnsatCore
+                            | defs.Track.ProofExhibition
+                            | defs.Track.Cloud
+                            | defs.Track.Parallel
+                        ):
                             continue
                     for _, logics in divisions.items():
                         for logic in logics: