2025 final execution

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
@@ -31,6 +30,12 @@ build: clean-build ## Build wheel file using poetry
 clean-build: ## clean build artifacts
 	@rm -rf dist
 
+.PHONY: clean-web-results
+clean-web-results: ## clean web results
+	@rm -rf web/content/results
+	@rm -rf web/public/results
+
+
 .PHONY: help
 help:
 	@grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-20s\033[0m %s\n", $$1, $$2}'
@@ -76,8 +81,23 @@ results-generation:
 	@poetry run smtcomp export-results-pages data Incremental
 	# @echo "🚀 Generating results to web/content/results for Cloud"
 	# @poetry run smtcomp export-results-pages data Cloud
-	# @echo "🚀 Generating results to web/content/results for Parallel"
-	# @poetry run smtcomp export-results-pages data Parallel
+	@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"

README.md

@@ -257,7 +257,7 @@ The step from Single Query can be followed with the model validation results whe
 Tasks for unsat core validation can be generated by:
 
 ```
-smtcomp generate-unsatcore-validation-files ../tmp/execution SCRAMBLER_EXECUTABLE UNSAT_CORE_RESULT_DIR/*/*
+smtcomp generate-unsatcore-validation-files ../tmp/execution SCRAMBLER_EXECUTABLE UNSAT_CORE_RESULT_DIR
 ```
 
 ---

data/2025/slides/future/prover.json

@@ -0,0 +1,30 @@
+{
+    "name": "bub4",
+    "authors": ["you"],
+    "logics": {
+        "sq": ["UF"],
+        "uc": "^QF_(LRA)?(UF)?$",
+        "mv": {
+            "theories": ["QF", "+-UF", "+-BV", "+-A"],
+            "except": ["QF_UFBVA"],
+            "logics": ["QF_LRA"]
+        }
+    },
+    "versions": [
+        {
+            "name": "10/05/24",
+            "url": "http://...",
+            "sha256": "123434ac",
+            "competing": true,
+            "cmd": {
+                "mv": ["bub4", "--model"]
+            }
+        },
+        {
+            "name": "fixed",
+            "url": "http://...",
+            "sha256": "123434ac",
+            "competing": false
+        }
+    ]
+}