From: Jannis Harder <me@jix.one>
Date: Mon, 30 May 2022 12:37:20 +0000 (+0200)
Subject: Better checking of available solvers
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dc22d97362162c39bd826df2600f34c6b9ba7fbe;p=SymbiYosys.git

Better checking of available solvers

Check for required auxiliary tools and always regenerate the make rules
when the set of available tools changes.
---

diff --git a/tests/Makefile b/tests/Makefile
index eb941e2..6992f92 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -2,6 +2,23 @@ test:
 
 .PHONY: test clean refresh help
 
+TOOL_LIST := \
+	btorsim \
+	yices \
+	aigbmc \
+	avy \
+	bitwuzla \
+	boolector \
+	btormc \
+	cvc4 \
+	mathsat \
+	pono \
+	suprove \
+	yices-smt2 \
+	yices \
+	yosys-abc \
+	z3
+
 help:
 	@cat make/help.txt
 
@@ -15,5 +32,12 @@ make/rules/test/%.mk:
 	python3 make/test_rules.py $<
 
 ifneq (help,$(MAKECMDGOALS))
+
+FIND_TOOLS := $(shell \
+	TOOLS=$$(which $(TOOL_LIST) 2>/dev/null || true); \
+	echo $$TOOLS | cmp -s make/rules/found_tools || echo $$TOOLS > make/rules/found_tools \
+)
+
 include make/rules/collect.mk
+
 endif
diff --git a/tests/make/collect_tests.py b/tests/make/collect_tests.py
index cf782b9..7b0cda3 100644
--- a/tests/make/collect_tests.py
+++ b/tests/make/collect_tests.py
@@ -37,7 +37,7 @@ with out_file.open("w") as output:
         print(f"{out_file}: {checked_dir}", file=output)
 
     for test in tests:
-        print(f"make/rules/test/{test}.mk: {test}", file=output)
+        print(f"make/rules/test/{test}.mk: {test} make/rules/found_tools", file=output)
         for ext in [".sh", ".py"]:
             script_file = test.parent / (test.stem + ext)
             if script_file.exists():
diff --git a/tests/make/test_rules.py b/tests/make/test_rules.py
index 1ad49ba..149e524 100644
--- a/tests/make/test_rules.py
+++ b/tests/make/test_rules.py
@@ -26,6 +26,8 @@ def parse_engine(engine):
     return engine, default_solvers.get(engine)
 
 
+# When adding new tools, also update TOOL_LIST in Makefile to make sure we regenerate
+# the rules when the user installs or removes any of the tools
 REQUIRED_TOOLS = {
     ("smtbmc", "yices"): ["yices-smt2"],
     ("smtbmc", "z3"): ["z3"],
@@ -34,11 +36,12 @@ REQUIRED_TOOLS = {
     ("smtbmc", "boolector"): ["boolector"],
     ("smtbmc", "bitwuzla"): ["bitwuzla"],
     ("smtbmc", "abc"): ["yosys-abc"],
-    ("aiger", "suprove"): ["suprove"],
-    ("aiger", "avy"): ["avy"],
-    ("aiger", "aigbmc"): ["aigbmc"],
-    ("btor", "btormc"): ["btormc"],
-    ("btor", "pono"): ["pono"],
+    ("aiger", "suprove"): ["suprove", "yices"],
+    ("aiger", "avy"): ["avy", "yices"],
+    ("aiger", "aigbmc"): ["aigbmc", "yices"],
+    ("btor", "btormc"): ["btormc", "btorsim"],
+    ("btor", "pono"): ["pono", "btorsim"],
+    ("abc"): ["yices"],
 }
 
 rules_file = Path("make/rules/test") / sby_dir / (sby_file.name + ".mk")
@@ -63,7 +66,9 @@ with rules_file.open("w") as rules:
         for engine in info["engines"]:
             engine, solver = parse_engine(engine)
             engines.add(engine)
-            required_tools.update(REQUIRED_TOOLS.get((engine, solver), ()))
+            required_tools.update(
+                REQUIRED_TOOLS.get((engine, solver), REQUIRED_TOOLS.get(engine, ()))
+            )
             if solver:
                 solvers.add(solver)
                 engine_solvers.add((engine, solver))