Merge remote-tracking branch 'origin/develop'

pyk/src/pyk/ktool/kompile.py

@@ -20,6 +20,7 @@
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Mapping
+    from fractions import Fraction
     from typing import Any, Final, Literal
 
     from ..utils import BugReport
@@ -421,6 +422,8 @@ class LLVMKompile(Kompile):
     enable_llvm_debug: bool
     llvm_proof_hint_instrumentation: bool
     llvm_mutable_bytes: bool
+    iterated_threshold: Fraction | None
+    heuristic: str | None
 
     def __init__(
         self,
@@ -435,6 +438,8 @@ def __init__(
         enable_llvm_debug: bool = False,
         llvm_proof_hint_instrumentation: bool = False,
         llvm_mutable_bytes: bool = False,
+        iterated_threshold: Fraction | None = None,
+        heuristic: str | None = None,
     ):
         llvm_kompile_type = LLVMKompileType(llvm_kompile_type) if llvm_kompile_type is not None else None
         llvm_kompile_output = Path(llvm_kompile_output) if llvm_kompile_output is not None else None
@@ -455,6 +460,8 @@ def __init__(
         object.__setattr__(self, 'enable_llvm_debug', enable_llvm_debug)
         object.__setattr__(self, 'llvm_proof_hint_instrumentation', llvm_proof_hint_instrumentation)
         object.__setattr__(self, 'llvm_mutable_bytes', llvm_mutable_bytes)
+        object.__setattr__(self, 'iterated_threshold', iterated_threshold)
+        object.__setattr__(self, 'heuristic', heuristic)
 
     @property
     def backend(self) -> Literal[KompileBackend.LLVM]:
@@ -491,6 +498,12 @@ def args(self) -> list[str]:
         if self.llvm_mutable_bytes:
             args += ['--llvm-mutable-bytes']
 
+        if self.iterated_threshold:
+            args += ['--iterated-threshold', str(self.iterated_threshold)]
+
+        if self.heuristic:
+            args += ['--heuristic', self.heuristic]
+
         return args