From 222801e6877fa89e823b3c802b20ceef939829f6 Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Sun, 7 Dec 2025 14:19:23 +0800 Subject: [PATCH] Support rIC3 engine for btor --- docs/source/install.rst | 2 +- docs/source/reference.rst | 4 +++ sbysrc/sby_engine_btor.py | 57 ++++++++++++++++++++++++++++++++++++++- sbysrc/sby_mode_prove.py | 4 +++ 4 files changed, 65 insertions(+), 2 deletions(-) diff --git a/docs/source/install.rst b/docs/source/install.rst index ad2075b..1e21e4c 100644 --- a/docs/source/install.rst +++ b/docs/source/install.rst @@ -138,4 +138,4 @@ rIC3 ^^^^ https://github.com/gipsyh/rIC3/ -The minimum required version is 1.3.5 +The minimum required version of rIC3 is 1.5.2 diff --git a/docs/source/reference.rst b/docs/source/reference.rst index a50e31e..80b8f38 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -298,6 +298,8 @@ The following mode/engine/solver combinations are currently supported: | | ``abc sim3`` | | | | | | ``aiger aigbmc`` | +| | | +| | ``aiger rIC3`` | +-----------+--------------------------+ | ``prove`` | ``smtbmc [all solvers]`` | | | | @@ -308,6 +310,8 @@ The following mode/engine/solver combinations are currently supported: | | ``aiger rIC3`` | | | | | | ``aiger suprove`` | +| | | +| | ``btor rIC3`` | +-----------+--------------------------+ | ``cover`` | ``smtbmc [all solvers]`` | | | | diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index b938397..31cd6c9 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -36,6 +36,8 @@ def run(mode, task, engine_idx, engine): task.error("Unexpected BTOR engine options.") if solver_args[0] == "btormc": + if mode != "bmc": + task.error("The btormc solver is only supported in bmc mode.") solver_cmd = "" if random_seed: solver_cmd += f"BTORSEED={random_seed} " @@ -45,6 +47,8 @@ def run(mode, task, engine_idx, engine): solver_cmd += " ".join([""] + solver_args[1:]) elif solver_args[0] == "pono": + if mode != "bmc": + task.error("The pono solver is only supported in bmc mode.") if random_seed: task.error("Setting the random seed is not available for the pono solver.") if task.opt_skip is not None: @@ -52,6 +56,25 @@ def run(mode, task, engine_idx, engine): solver_cmd = task.exe_paths["pono"] + f" --witness -v 1 -e bmc -k {task.opt_depth - 1}" solver_cmd += " ".join([""] + solver_args[1:]) + elif solver_args[0] == "rIC3": + if random_seed: + task.error("Setting the random seed is not available for the rIC3 solver.") + if task.opt_skip is not None: + task.error("The btor engine supports the option skip only for the btormc solver.") + if mode == "prove": + solver_cmd = " ".join([task.exe_paths["rIC3"], "--witness"] + solver_args[1:]) + elif mode == "bmc": + solver_cmd = " ".join( + [ + task.exe_paths["rIC3"], + "-e bmc", + "--end {}".format(task.opt_depth - 1), + "--witness", + ] + + solver_args[1:] + ) + else: + task.error("The rIC3 solver is only supported in bmc and prove mode.") else: task.error(f"Invalid solver command {solver_args[0]}.") @@ -92,13 +115,26 @@ def run(mode, task, engine_idx, engine): else: task.error(f"engine_{engine_idx}: Engine terminated without status.") task.update_unknown_props(dict(source="btor", engine=f"engine_{engine_idx}")) - else: + elif mode == "bmc": if common_state.expected_cex == 0: proc_status = "pass" elif common_state.solver_status == "sat": proc_status = "FAIL" elif common_state.solver_status == "unsat": proc_status = "pass" + elif common_state.solver_status == "unknown": + proc_status = "pass" + else: + task.error(f"engine_{engine_idx}: Engine terminated without status.") + elif mode == "prove": + if common_state.expected_cex == 0: + proc_status = "pass" + elif common_state.solver_status == "sat": + proc_status = "FAIL" + elif common_state.solver_status == "unsat": + proc_status = "pass" + elif common_state.solver_status == "unknown": + proc_status = "UNKNOWN" else: task.error(f"engine_{engine_idx}: Engine terminated without status.") @@ -233,6 +269,23 @@ def run(mode, task, engine_idx, engine): if line not in ["b0"]: return line + elif solver_args[0] == "rIC3": + match = re.match(r".*bmc found counter-example in depth (\d+).*", line) + if match: + common_state.current_step = int(match[1]) + if line == "UNSAT": + if common_state.solver_status is None: + common_state.solver_status = "unsat" + return "No CEX found." + if line == "UNKNOWN": + if common_state.solver_status is None: + common_state.solver_status = "unknown" + if line == "SAT": + if common_state.solver_status is None: + common_state.solver_status = "sat" + return line + + print(line, file=proc.logfile) return None @@ -264,6 +317,8 @@ def run(mode, task, engine_idx, engine): proc.checkretcode = True if solver_args[0] == "pono": proc.retcodes = [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2 + if solver_args[0] == "rIC3": + proc.retcodes = [10, 20, 30] # FALSE = 10, TRUE = 20, ERROR = 30 proc.output_callback = output_callback proc.register_exit_callback(exit_callback) common_state.running_procs += 1 diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index c608c6b..ac0efdb 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -42,6 +42,10 @@ def run(task): import sby_engine_aiger sby_engine_aiger.run("prove", task, engine_idx, engine) + elif engine[0] == "btor": + import sby_engine_btor + sby_engine_btor.run("prove", task, engine_idx, engine) + elif engine[0] == "abc": import sby_engine_abc sby_engine_abc.run("prove", task, engine_idx, engine)