1ad49ba92ec472031ea0a03c48466efd24072e18
6 from pathlib
import Path
9 sby_file
= Path(sys
.argv
[1])
10 sby_dir
= sby_file
.parent
13 taskinfo
= json
.loads(
14 subprocess
.check_output(
15 [sys
.executable
, os
.getenv("SBY_MAIN"), "--dumptaskinfo", sby_file
]
20 def parse_engine(engine
):
21 engine
, *args
= engine
22 default_solvers
= {"smtbmc": "yices"}
24 if not arg
.startswith("-"):
26 return engine
, default_solvers
.get(engine
)
30 ("smtbmc", "yices"): ["yices-smt2"],
31 ("smtbmc", "z3"): ["z3"],
32 ("smtbmc", "cvc4"): ["cvc4"],
33 ("smtbmc", "mathsat"): ["mathsat"],
34 ("smtbmc", "boolector"): ["boolector"],
35 ("smtbmc", "bitwuzla"): ["bitwuzla"],
36 ("smtbmc", "abc"): ["yosys-abc"],
37 ("aiger", "suprove"): ["suprove"],
38 ("aiger", "avy"): ["avy"],
39 ("aiger", "aigbmc"): ["aigbmc"],
40 ("btor", "btormc"): ["btormc"],
41 ("btor", "pono"): ["pono"],
44 rules_file
= Path("make/rules/test") / sby_dir
/ (sby_file
.name
+ ".mk")
45 rules_file
.parent
.mkdir(exist_ok
=True, parents
=True)
47 with rules_file
.open("w") as rules
:
48 name
= str(sby_dir
/ sby_file
.stem
)
50 for task
, info
in taskinfo
.items():
52 workdirname
= sby_file
.stem
55 workdirname
+= f
"_{task}"
59 engine_solvers
= set()
61 required_tools
= set()
63 for engine
in info
["engines"]:
64 engine
, solver
= parse_engine(engine
)
66 required_tools
.update(REQUIRED_TOOLS
.get((engine
, solver
), ()))
69 engine_solvers
.add((engine
, solver
))
71 print(f
".PHONY: {target}", file=rules
)
72 print(f
"{target}:", file=rules
)
74 shell_script
= sby_dir
/ f
"{sby_file.stem}.sh"
76 missing_tools
= sorted(
77 f
"`{tool}`" for tool
in required_tools
if shutil
.which(tool
) is None
82 f
"\t@echo; echo 'SKIPPING {target}: {', '.join(missing_tools)} not found'; echo",
86 elif shell_script
.exists():
88 f
"\tcd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}",
93 f
"\tcd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}",
97 print(f
".PHONY: clean-{target}", file=rules
)
98 print(f
"clean-{target}:", file=rules
)
99 print(f
"\trm -rf {target}", file=rules
)
105 test_groups
.append(f
"test_m_{mode}")
107 for engine
in sorted(engines
):
108 test_groups
.append(f
"test_e_{engine}")
109 test_groups
.append(f
"test_m_{mode}_e_{engine}")
111 for solver
in sorted(solvers
):
112 test_groups
.append(f
"test_s_{solver}")
113 test_groups
.append(f
"test_m_{mode}_s_{solver}")
115 for engine
, solver
in sorted(engine_solvers
):
116 test_groups
.append(f
"test_e_{engine}_s_{solver}")
117 test_groups
.append(f
"test_m_{mode}_e_{engine}_s_{solver}")
121 for part
in [*sby_dir
.parts
, ""]:
122 print(f
".PHONY: {prefix}clean {prefix}test", file=rules
)
123 print(f
"{prefix}clean: clean-{target}", file=rules
)
124 print(f
"{prefix}test: {target}", file=rules
)
126 for test_group
in test_groups
:
127 print(f
".PHONY: {prefix}{test_group}", file=rules
)
128 print(f
"{prefix}{test_group}: {target}", file=rules
)
131 tasks
= [task
for task
in taskinfo
.keys() if task
]
134 print(f
".PHONY: {name}", file=rules
)
135 print(f
"{name}:", *(f
"{name}_{task}" for task
in tasks
), file=rules
)