Fix local model validation

and raise stack limit for dolmen

smtcomp/main.py

@@ -19,6 +19,7 @@
 import smtcomp.benchexec as benchexec
 import smtcomp.benchexec
 import smtcomp.defs as defs
+import smtcomp.model_validation
 import smtcomp.results
 import smtcomp.scoring
 import smtcomp.submission as submission
@@ -971,29 +972,35 @@ def check_model_locally(
  for resultdir in resultdirs:
  l2 = model_validation.check_results_locally(config, cachedir, resultdir, executor, progress)
  l.extend(filter_map(map_none3(model_validation.is_error), l2))
- keyfunc = lambda v: v[0].solver
+ if not l:
+ print("[green]All models validated[/green]")
+ return
+
+ def keyfunc(
+ v: tuple[smtcomp.results.RunId, smtcomp.results.Run, smtcomp.model_validation.ValidationError],
+ ) -> str:
+ return v[0].solver
+
  l.sort(key=keyfunc)
- d = itertools.groupby(l, key=keyfunc)
- t = Tree("Unvalidated models")
- for solver, rs in d:
+ t = Tree("[red]Unvalidated models[/red]")
+ for solver, rs in itertools.groupby(l, key=keyfunc):
  t2 = t.add(solver)
  for rid, r, result in rs:
  stderr = result.stderr.strip().replace("\n", ", ")
  basename = smtcomp.scramble_benchmarks.scramble_basename(r.scramble_id)
  t2.add(f"{basename}: {stderr}")
  print(t)
  if outdir is not None:
- for solver, models in d:
- dst = outdir / solver
+ for rid, r, result in l:
+ dst = outdir / rid.solver
  dst.mkdir(parents=True, exist_ok=True)
- for rid, r, result in models:
- filedir = benchmark_files_dir(cachedir, rid.track)
- basename = smtcomp.scramble_benchmarks.scramble_basename(r.scramble_id)
- basename_model = smtcomp.scramble_benchmarks.scramble_basename(r.scramble_id, suffix="rsmt2")
- smt2_file = filedir / str(r.logic) / basename
- (dst / basename).unlink(missing_ok=True)
- (dst / basename).symlink_to(smt2_file)
- (dst / basename_model).write_text(result.model)
+ filedir = benchmark_files_dir(cachedir, rid.track)
+ basename = smtcomp.scramble_benchmarks.scramble_basename(r.scramble_id)
+ basename_model = smtcomp.scramble_benchmarks.scramble_basename(r.scramble_id, suffix="rsmt2")
+ smt2_file = filedir / str(r.logic) / basename
+ (dst / basename).unlink(missing_ok=True)
+ (dst / basename).symlink_to(smt2_file.absolute())
+ (dst / basename_model).write_text(result.model)
 
 
 @app.command()

smtcomp/model_validation.py

@@ -1,7 +1,7 @@
 from dataclasses import dataclass
 from pathlib import Path
 import smtcomp.defs as defs
-import subprocess
+import subprocess, resource
 import smtcomp.results as results
 from smtcomp.benchexec import get_suffix
 import smtcomp.scramble_benchmarks
@@ -41,7 +41,7 @@ class ValidationOk:
 class ValidationError:
  status: defs.Status
  stderr: str
- model: str | None
+ model: str
 
 
 @dataclass
@@ -62,6 +62,12 @@ def is_error(x: Validation) -> ValidationError | None:
  return None
 
 
+def raise_stack_limit() -> None:
+ soft, hard = resource.getrlimit(resource.RLIMIT_STACK)
+ soft = min(40_000_000_000, hard)
+ resource.setrlimit(resource.RLIMIT_STACK, (soft, hard))
+
+
 def check_locally(config: defs.Config, smt2_file: Path, model: str) -> Validation:
  r = subprocess.run(
  [
@@ -75,6 +81,7 @@ def check_locally(config: defs.Config, smt2_file: Path, model: str) -> Validatio
  ],
  input=model.encode(),
  capture_output=True,
+ preexec_fn=raise_stack_limit,
  )
  match r.returncode:
  case 0: