btor2aiger: Use asserts and assumes from .ywb file

Author: KrystalDelusion

sbysrc/sby_core.py

@@ -1159,7 +1159,7 @@ def instance_hierarchy_error_callback(retcode):
                 self,
                 "btor_aig",
                 self.model(btor_model),
-                f"cd {self.workdir}/model; btor2aig_yw design_{btor_model}.btor"
+                f"cd {self.workdir}/model; btor2aig_yw design_{btor_model}.btor design_btor.ywb"
             )
             proc.checkretcode = True
 

tools/btor2aig_yw/btor2aig_yw.py

@@ -15,6 +15,11 @@ def arg_parser():
         type=Path
     )
 
+    parser.add_argument(
+        "ywb_file",
+        type=Path
+    )
+
     parser.add_argument(
         "-d", "--dest",
         dest="dest",
@@ -118,15 +123,10 @@ async def main() -> None:
         data = await proc.stdout.readline()
     aimf.close()
 
-    # find assertions by looking for 'bad' statements in the btor
-    with open(args.btor_file, mode='r') as f:
-        data = f.readline()
-        while data:
-            if "bad" in data:
-                m = re.match(r"^\d+ bad \d+ (\S+)", data)
-                path = fix_path(m.group(1))
-                ywa['asserts'].append(path)
-            data = f.readline()
+    with open(args.ywb_file, mode='r') as f:
+        data = json.load(f)
+        ywa['asserts'].extend(data['asserts'])
+        ywa['assumes'].extend(data['assumes'])
 
 
     with open(work_dir / "design_aiger.ywa", mode="w") as f: