From ca93e43cec50e98066bb1fe136dd00dddb5958f3 Mon Sep 17 00:00:00 2001 From: SeddonShen <283481855@qq.com> Date: Tue, 18 Mar 2025 16:06:16 +0800 Subject: [PATCH] feat(sby_engine_aiger): add rIC3 support for BMC mode --- sbysrc/sby_engine_aiger.py | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index 07fc965..11e176f 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -48,9 +48,13 @@ def run(mode, task, engine_idx, engine): solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:]) elif solver_args[0] == "rIC3": - if mode != "prove": - task.error("The aiger solver 'rIC3' is only supported in prove mode.") - solver_cmd = " ".join([task.exe_paths["rIC3"], "--witness"] + solver_args[1:]) + if mode not in ["bmc", "prove"]: + task.error("The aiger solver 'rIC3' is only supported in bmc and prove mode.") + if mode == "prove": + solver_cmd = " ".join([task.exe_paths["rIC3"], "--witness"] + solver_args[1:]) + if mode == "bmc": + solver_cmd = " ".join([task.exe_paths["rIC3"], "--bmc-max-k {}".format(task.opt_depth - 1), "-e bmc", "-v 0", "--witness"] + solver_args[1:]) + status_2 = "PASS" # rIC3 outputs status 2 when BMC passes elif solver_args[0] == "aigbmc": if mode != "bmc":