From dc22d97362162c39bd826df2600f34c6b9ba7fbe Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 30 May 2022 14:37:20 +0200 Subject: [PATCH] Better checking of available solvers Check for required auxiliary tools and always regenerate the make rules when the set of available tools changes. --- tests/Makefile | 24 ++++++++++++++++++++++++ tests/make/collect_tests.py | 2 +- tests/make/test_rules.py | 17 +++++++++++------ 3 files changed, 36 insertions(+), 7 deletions(-) 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)) -- 2.30.2