Skip to content

Commit

Permalink
btor2aiger: Use asserts and assumes from .ywb file
Browse files Browse the repository at this point in the history
  • Loading branch information
KrystalDelusion committed Apr 6, 2024
1 parent 49750a9 commit 28ee667
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 10 deletions.
2 changes: 1 addition & 1 deletion sbysrc/sby_core.py
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
18 changes: 9 additions & 9 deletions tools/btor2aig_yw/btor2aig_yw.py
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,11 @@ def arg_parser():
type=Path
)

parser.add_argument(
"ywb_file",
type=Path
)

parser.add_argument(
"-d", "--dest",
dest="dest",
Expand Down Expand Up @@ -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:
Expand Down

0 comments on commit 28ee667

Please sign in to comment.