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 eb941e2338c8950cd876a406ff1540dc15232777..6992f921c34916ea0bf7c8f7fbffe697cc9771b8 100644 (file)
--- 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 cf782b99e289e8b240234dd243d7806bf378b02d..7b0cda3759d8e30030526721bdc8c7ffcde8c619 100644 (file)
--- 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 1ad49ba92ec472031ea0a03c48466efd24072e18..149e524f2352caea26b343573897cf1691d6a96d 100644 (file)
--- 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))