Add support for cosa2 BTOR solver

Signed-off-by: Claire Wolf <claire@symbioticeda.com>

diff --git a/sbysrc/sby.py b/sbysrc/sby.py
index 82f6eae238b38f40f478cf8a9aae6eeb1c235fd9..5c8c797ed26f6a89be3056150b2b34d49e5fb2a1 100644 (file)
--- a/sbysrc/sby.py
+++ b/sbysrc/sby.py
@@ -58,6 +58,8 @@ parser.add_argument("--aigbmc", metavar="<path_to_executable>",
 parser.add_argument("--avy", metavar="<path_to_executable>",
         action=DictAction, dest="exe_paths")
 parser.add_argument("--btormc", metavar="<path_to_executable>",
+        action=DictAction, dest="exe_paths")
+parser.add_argument("--cosa2", metavar="<path_to_executable>",
         action=DictAction, dest="exe_paths",
         help="configure which executable to use for the respective tool")
 parser.add_argument("--dumpcfg", action="store_true", dest="dump_cfg",

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index b62d5f7f5000716a48a91c13fb51e7fc48652dac..972e04786f6696b953f971f2986bb9c817757a79 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -90,15 +90,18 @@ class SbyTask:
         else:
             self.notify.append(next_task)
 
+    def log(self, line):
+        if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)):
+            if self.logfile is not None:
+                print(line, file=self.logfile)
+            self.job.log("{}: {}".format(self.info, line))
+
     def handle_output(self, line):
         if self.terminated or len(line) == 0:
             return
         if self.output_callback is not None:
             line = self.output_callback(line)
-        if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)):
-            if self.logfile is not None:
-                print(line, file=self.logfile)
-            self.job.log("{}: {}".format(self.info, line))
+        self.log(line)
 
     def handle_exit(self, retcode):
         if self.terminated:
@@ -222,6 +225,7 @@ class SbyJob:
             "aigbmc": "aigbmc",
             "avy": "avy",
             "btormc": "btormc",
+            "cosa2": "cosa2",
         }
 
         self.tasks_running = []

diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py
index 6dbec1bce936e19f6cf0006d4f503c508fe73cfe..caa999f434c5b6b7376a6222708d0746753087d8 100644 (file)
--- a/sbysrc/sby_engine_btor.py
+++ b/sbysrc/sby_engine_btor.py
@@ -35,6 +35,9 @@ def run(mode, job, engine_idx, engine):
             solver_cmd += " -kmin {}".format(job.opt_skip)
         solver_cmd += " ".join([""] + solver_args[1:])
 
+    elif solver_args[0] == "cosa2":
+        solver_cmd = job.exe_paths["cosa2"] + " -v 1 -e bmc -k {}".format(job.opt_depth - 1)
+
     else:
         job.error("Invalid solver command {}.".format(solver_args[0]))
 
@@ -111,10 +114,14 @@ def run(mode, job, engine_idx, engine):
 
     def output_callback(line):
         if mode == "cover":
-            match = re.search(r"calling BMC on ([0-9]+) properties", line)
-            if match:
-                common_state.expected_cex = int(match[1])
-                assert common_state.produced_cex == 0
+            if solver_args[0] == "btormc":
+                match = re.search(r"calling BMC on ([0-9]+) properties", line)
+                if match:
+                    common_state.expected_cex = int(match[1])
+                    assert common_state.produced_cex == 0
+
+            else:
+                job.error("engine_{}: BTOR solver '{}' is currently not supported in cover mode.".format(solver_args[0]))
 
         if (common_state.produced_cex < common_state.expected_cex) and line == "sat":
             assert common_state.wit_file == None
@@ -122,6 +129,8 @@ def run(mode, job, engine_idx, engine):
                 common_state.wit_file = open("{}/engine_{}/trace.wit".format(job.workdir, engine_idx), "w")
             else:
                 common_state.wit_file = open("{}/engine_{}/trace{}.wit".format(job.workdir, engine_idx, common_state.produced_cex), "w")
+            if solver_args[0] != "btormc":
+                task.log("Found satisfiability witness.")
 
         if common_state.wit_file:
             print(line, file=common_state.wit_file)
@@ -130,7 +139,7 @@ def run(mode, job, engine_idx, engine):
                     suffix = ""
                 else:
                     suffix = common_state.produced_cex
-                task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("btor"),
+                task2 = SbyTask(job, "engine_{}_{}".format(engine_idx, common_state.produced_cex), job.model("btor"),
                         "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor.info model/design_btor.btor engine_{idx}/trace{i}.wit".format(dir=job.workdir, idx=engine_idx, i=suffix),
                         logfile=open("{dir}/engine_{idx}/logfile2.txt".format(dir=job.workdir, idx=engine_idx), "w"))
                 task2.output_callback = output_callback2
@@ -144,28 +153,36 @@ def run(mode, job, engine_idx, engine):
                 if common_state.produced_cex == common_state.expected_cex:
                     common_state.solver_status = "sat"
 
-        if line.startswith("u"):
-            return "No CEX up to depth {}.".format(int(line[1:])-1)
-
-        if solver_args[0] == "btormc":
-            if "calling BMC on" in line:
-                return line
-            if "SATISFIABLE" in line:
-                return line
-            if "bad state properties at bound" in line:
-                return line
-            if "deleting model checker:" in line:
-                if common_state.solver_status is None:
-                    common_state.solver_status = "unsat"
-                return line
-
-        if not common_state.wit_file:
+        else:
+            if solver_args[0] == "btormc":
+                if "calling BMC on" in line:
+                    return line
+                if "SATISFIABLE" in line:
+                    return line
+                if "bad state properties at bound" in line:
+                    return line
+                if "deleting model checker:" in line:
+                    if common_state.solver_status is None:
+                        common_state.solver_status = "unsat"
+                    return line
+
+            elif solver_args[0] == "cosa2":
+                if line == "unknown":
+                    if common_state.solver_status is None:
+                        common_state.solver_status = "unsat"
+                    return "No CEX found."
+                if line not in ["b0"]:
+                    return line
+
             print(line, file=task.logfile)
 
         return None
 
     def exit_callback(retcode):
-        assert retcode == 0
+        if solver_args[0] == "cosa2":
+            assert retcode in [1, 2]
+        else:
+            assert retcode == 0
         if common_state.expected_cex != 0:
             assert common_state.solver_status is not None