Generate graphics

Makefile

@@ -1,8 +1,7 @@
 .PHONY: install
-install: ## Install the poetry environment and install the pre-commit hooks
+install: ## Install the poetry environment
 	@echo "🚀 Creating virtual environment using pyenv and poetry"
 	@poetry install
-	@poetry shell
 
 .PHONY: check
 check: ## Run code quality tools.
@@ -20,7 +19,7 @@ test: generation ## Test the code with pytest
 	@echo "🚀 Testing code: Running pytest"
 	@poetry run pytest
 
-generation: submission-generation participant-data track-data division-track-data results-generation ## Files generation for the website
+generation: submission-generation participant-data track-data division-track-data results-generation charts-generation ## Files generation for the website
 
 .PHONY: build
 build: clean-build ## Build wheel file using poetry
@@ -85,6 +84,21 @@ results-generation:
 	@echo "🚀 Generating results to web/content/results for Parallel"
 	@poetry run smtcomp export-results-pages data Parallel
 
+charts-generation:
+	@echo "🚀 Generating results to web/content/results for SingleQuery"
+	@poetry run smtcomp generate-website-graphics data SingleQuery
+	@echo "🚀 Generating results to web/content/results for ModelValidation"
+	@poetry run smtcomp generate-website-graphics data ModelValidation
+	@echo "🚀 Generating results to web/content/results for UnsatCore"
+	@poetry run smtcomp generate-website-graphics data UnsatCore
+	@echo "🚀 Generating results to web/content/results for Incremental"
+	@poetry run smtcomp generate-website-graphics data Incremental
+	# @echo "🚀 Generating results to web/content/results for Cloud"
+	# @poetry run smtcomp generate-website-graphics data Cloud
+	@echo "🚀 Generating results to web/content/results for Parallel"
+	@poetry run smtcomp generate-website-graphics data Parallel
+
+
 cache:
 	@echo "🚀 Generating cache"
 	@poetry run smtcomp create-cache data

pyproject.toml

@@ -19,7 +19,9 @@ dependencies = [
 "wget",
 "benchexec",
 "polars",
-"PyGithub"
+"PyGithub",
+"altair",
+"python-frontmatter",
 ]
 #pystemd is not set as dependency because it is not in the CI
 
@@ -69,11 +71,10 @@ module = [
     "benchexec","benchexec.util",
     "benchexec.result","benchexec.tools.template",
     "benchexec.runexecutor",
-    "bs4","wget"
+    "bs4","wget","frontmatter"
 ]
 ignore_missing_imports = true
 
-
 [tool.ruff]
 target-version = "py37"
 line-length = 120

smtcomp/generate_graphics.py

@@ -0,0 +1,229 @@
+import math
+import functools, itertools
+from collections import defaultdict
+from typing import Set, Dict, Optional, cast, List, DefaultDict, Tuple
+from pathlib import Path, PurePath
+from smtcomp import defs
+from rich.progress import track as rich_track
+
+import polars as pl
+import altair as alt
+import altair.utils.html
+import altair.vegalite.display
+from smtcomp.utils import *
+import smtcomp.generate_website_page
+import frontmatter
+
+c_file = pl.col("file")
+c_logic = pl.col("logic")
+c_division = pl.col("division")
+c_solver = pl.col("solver")
+c_solver2 = pl.col("solver2")
+c_answer = pl.col("answer")
+c_answer2 = pl.col("answer2")
+c_cputime_s = pl.col("cputime_s")
+c_cputime_s2 = pl.col("cputime_s2")
+c_run = pl.col("run")
+c_bucket = pl.col("bucket")
+c_bucket2 = pl.col("bucket2")
+
+
+def create_output(
+    config: defs.Config,
+    results: pl.LazyFrame,
+    logics: list[defs.Logic] = [],
+    divisions: list[defs.Division] = [],
+) -> alt.api.ChartType:
+
+    # We are computing the buckets offline because we have too much data
+    results = results.filter(
+        c_run == True, c_logic.is_in(set(map(int, logics))) | c_division.is_in(set(map(int, divisions)))
+    ).select(
+        c_file,
+        c_logic,
+        c_division,
+        c_solver,
+        c_answer,
+        c_cputime_s,
+        bucket=pl.lit(10.0).pow(c_cputime_s.log(10).floor()),
+        # bucket=c_cputime_s.log(10).floor(),
+    )
+
+    results_with = results.select(c_file, solver2=c_solver, bucket2=c_bucket, cputime_s2=c_cputime_s, answer2=c_answer)
+    results = results.join(results_with, on=c_file, how="left")
+
+    corr = (
+        results.group_by(c_solver, c_solver2)
+        .agg(corr=pl.corr(c_cputime_s, c_cputime_s2, method="pearson"))
+        .sort(c_solver, c_solver2)
+    )
+
+    results = (
+        results.group_by(c_solver, c_solver2, c_answer, c_answer2, c_bucket, c_bucket2, c_logic, c_division)
+        .len()
+        .sort(c_solver, c_solver2)
+    )
+
+    # Replace integer by names
+    # It should be possible to do it later in altair; the html file would be smaller
+    if True:
+        for lookup, replaced in [
+            (defs.Answer, "answer"),
+            (defs.Answer, "answer2"),
+            (defs.Logic, "logic"),
+            (defs.Division, "division"),
+        ]:
+            lf_lookup = pl.DataFrame(
+                data=((int(n), str(n)) for n in lookup), schema=[(replaced, pl.Int8), ("pretty", pl.String)]
+            ).lazy()
+            results = results.join(lf_lookup, how="left", on=replaced).drop(replaced).rename({"pretty": replaced})
+
+    buckets = results.select(c_bucket.unique())
+
+    df_corr, df_results, df_buckets = pl.collect_all([corr, results, buckets])
+
+    bucket_domain: list[float] = list(df_buckets["bucket"])
+
+    row1 = df_corr.row(min(1, len(df_corr) - 1), named=True)
+
+    # Create heatmap with selection
+    select_x = alt.selection_point(fields=["solver"], name="solver1", value=row1["solver"], toggle=False)
+    select_y = alt.selection_point(fields=["solver2"], name="solver2", value=row1["solver2"], toggle=False)
+    answer_x = alt.selection_point(fields=["answer"], name="answer1")
+    answer_y = alt.selection_point(fields=["answer2"], name="answer2")
+    logic = alt.selection_point(fields=["logic"], name="logic")
+    division = alt.selection_point(fields=["division"], name="division")
+    g_select_provers = (
+        alt.Chart(df_corr, title="Click a tile to compare solvers", height=250, width=250)
+        .mark_rect()
+        .encode(
+            alt.X("solver", title=None),
+            alt.Y("solver2", title=None),
+            alt.Color("corr", scale=alt.Scale(domain=[-1, 1], scheme="blueorange")),
+            opacity=alt.when(select_x, select_y).then(alt.value(1)).otherwise(alt.value(0.4)),
+        )
+        .add_params(select_x, select_y)
+    )
+
+    title = alt.Title(alt.expr(f'{select_x.name}.solver + " vs " + {select_y.name}.solver2'))
+    g_results = (
+        alt.Chart(df_results, title=title, height=250, width=250)
+        .transform_filter(select_x, select_y, answer_x, answer_y)
+        .transform_aggregate(benchs="sum(len)", groupby=["bucket", "bucket2"])
+        .add_params(select_x, select_y, answer_x, answer_y)
+        .encode(
+            alt.X("bucket:O").axis(title="solver1", bandPosition=0.5)
+            # align should move the center of the cell, it does not
+            .scale(type="band", align=0, domain=bucket_domain),
+            alt.Y("bucket2:O")
+            .axis(title="solver2", bandPosition=0.5)
+            .scale(type="band", align=0, domain=list(reversed(bucket_domain))),
+            text="benchs:Q",
+        )
+    )
+
+    g_results_rect = g_results.mark_rect().encode(alt.Color("benchs:Q", scale=alt.Scale(scheme="yellowgreenblue")))
+
+    g_results_text = g_results.mark_text(baseline="middle")
+
+    # g_answers = (
+    #     alt.Chart(df_results, title="Answers")
+    #     .transform_filter(select_x, select_y, answer_x, answer_y)
+    #     .transform_aggregate(benchs="sum(len)", groupby=["answer_x", "bucket2"])
+    #     .add_params(select_x, select_y, answer_x, answer_y)
+    #     .encode(
+    #         alt.X("bucket:O").axis(title="solver1", bandPosition=0.5)
+    #         # align should move the center of the cell, it does not
+    #         .scale(type="band", align=0),
+    #         alt.Y("bucket2:O").axis(title="solver2", bandPosition=0.5).scale(type="band", align=0).sort("descending"),
+    #         text="benchs:Q",
+    #     )
+    #     .mark_bar()
+    # )
+    opacity = (
+        alt.when(select_x, select_y, answer_x, answer_y, logic, division).then(alt.value(1)).otherwise(alt.value(0.0))
+    )
+
+    legend_answer_x = (
+        alt.Chart(df_results, title=alt.Title(alt.expr(f'"solver1:" + {select_x.name}.solver')))
+        .mark_point()
+        .encode(alt.Y("answer:N").axis(title="", orient="right"), opacity=opacity)
+        .add_params(answer_x)
+    )
+
+    legend_answer_y = (
+        alt.Chart(df_results, title=alt.Title(alt.expr(f'"solver2:" + {select_y.name}.solver2')))
+        .mark_point()
+        .encode(alt.Y("answer2:N").axis(title="", orient="right"), opacity=opacity)
+        .add_params(answer_y)
+    )
+
+    legend_logic = (
+        alt.Chart(df_results, title="Logic")
+        .mark_point()
+        .encode(alt.Y("logic:N").axis(title="", orient="right"), opacity=opacity)
+        .add_params(logic)
+    )
+
+    legend_division = (
+        alt.Chart(df_results, title="Division")
+        .mark_point()
+        .encode(alt.Y("division:N").axis(title="", orient="right"), opacity=opacity)
+        .add_params(division)
+    )
+
+    graph: alt.api.ChartType = (g_select_provers | g_results_rect + g_results_text).resolve_scale(color="independent")
+
+    graph = alt.vconcat(graph, legend_answer_x | legend_answer_y | legend_logic | legend_division)
+
+    graph = graph.resolve_scale(color="independent")
+
+    return graph
+
+
+def save_output(
+    config: defs.Config,
+    results: pl.LazyFrame,
+    output: Path,
+    logics: list[defs.Logic] = [],
+    divisions: list[defs.Division] = [],
+) -> None:
+
+    create_output(config, results, logics, divisions).save(output)
+
+
+def save_hugo_output(chart: alt.api.ChartType, output: Path, title: str) -> None:
+
+    with alt.data_transformers.disable_max_rows():
+        content = chart.to_html(
+            fullhtml=False,
+        )
+    post = frontmatter.Post(content=content, title=title, layout="chart")
+    output.write_text(frontmatter.dumps(post))
+
+
+def generate_pages(config: defs.Config, results: pl.LazyFrame, track: defs.Track) -> None:
+    page_suffix = smtcomp.generate_website_page.page_track_suffix(track)
+    dst = config.web_results
+    dst.mkdir(parents=True, exist_ok=True)
+
+    df_results = results.filter(c_run == True).collect()
+    results = df_results.lazy()
+
+    divisions = list(df_results["division"].unique())
+    for div in rich_track(list(map(defs.Division.of_int, divisions)), description="Generating chart for divisions"):
+        chart = create_output(config, results, divisions=[div])
+        save_hugo_output(
+            chart,
+            output=dst / f"{div.name.lower()}-{page_suffix}-chart.html",
+            title=f"Chart for division {div.name}",
+        )
+
+    logics = list(df_results["logic"].unique())
+    for logic in rich_track(list(map(defs.Logic.of_int, logics)), description="Generating chart for logics"):
+        chart = create_output(config, results, logics=[logic])
+        save_hugo_output(
+            chart,
+            output=dst / f"{logic.name.lower()}-{page_suffix}-chart.html",
+            title=f"Chart for logic {logic.name}",
+        )

smtcomp/main.py

@@ -31,6 +31,7 @@
 import smtcomp.list_benchmarks
 import smtcomp.selection
 import smtcomp.generate_website_page
+import smtcomp.generate_graphics as smtcomp_generate_graphics
 from smtcomp.unpack import write_cin, read_cin
 import smtcomp.scramble_benchmarks
 from rich.console import Console
@@ -1125,3 +1126,48 @@ def generate_certificates(
     smtcomp.certificates.generate_certificates(
         website_results, input_for_certificates, submission_dir, experimental_division
     )
+
+
+@app.command()
+def generate_graphics(
+    data: Path,
+    output: Path,
+    logic: list[defs.Logic] = [],
+    division: list[defs.Division] = [],
+    track: defs.Track = defs.Track.SingleQuery,
+    src: List[Path] = typer.Argument(None),
+) -> None:
+    """
+    Generate graphics in html format
+
+    If src is empty use results in data
+    """
+    config = defs.Config(data)
+    results = smtcomp.results.helper_get_results(config, src, track)
+
+    smtcomp.scoring.sanity_check(config, results)
+
+    results = smtcomp.scoring.add_disagreements_info(results, track).filter(disagreements=False).drop("disagreements")
+
+    smtcomp_generate_graphics.save_output(config, results, output, logic, division)
+
+
+@app.command()
+def generate_website_graphics(
+    data: Path,
+    track: defs.Track,
+    src: List[Path] = typer.Argument(None),
+) -> None:
+    """
+    Generate graphics for hugo website
+
+    If src is empty use results in data
+    """
+    config = defs.Config(data)
+    results = smtcomp.results.helper_get_results(config, src, track)
+
+    smtcomp.scoring.sanity_check(config, results)
+
+    results = smtcomp.scoring.add_disagreements_info(results, track).filter(disagreements=False).drop("disagreements")
+
+    smtcomp_generate_graphics.generate_pages(config, results, track)

smtcomp/results.py

@@ -525,4 +525,7 @@ def helper_get_results(config: defs.Config, results: List[Path], track: defs.Tra
         defaults=defaults,
     )
 
+    if track == defs.Track.Parallel:
+        selected = selected.with_columns(run=True)
+
     return selected

web/themes/smtcomp/layouts/_default/result.html

@@ -15,9 +15,8 @@ <h1>{{ .Params.division }} ({{ $prettyTrack }})</h1>
   <p>
     Competition results for the {{ .Params.division }}
     {{ if $trueDivision }} division {{ else }} logic {{ end }}
-    in the {{ $prettyTrack }}.
+    in the {{ $prettyTrack }}. <a href="{{math.Add (path.Dir .RelPermalink) "-chart"}}"><b>Chart</b></a> </p>
   <p>Results were generated on {{ .Params.resultdate }}</p>
-  </p>
   <p>
     <b>Benchmarks</b>: {{ .Params.n_benchmarks }}<br/>
     <b>Time Limit:</b> {{ .Params.time_limit }} seconds<br/>