circt icon indicating copy to clipboard operation
circt copied to clipboard

Published 20 hours ago • verified publisher icon llvm

[SMT] Added support for :pattern attribute

Open luisacicolini opened this issue 1 year ago • 5 comments

This PR addressess issue #6913 to enable the support of attributes in the SMTLIB export pass.

luisacicolini avatar May 01 '24 12:05 luisacicolini

Sorry @luisacicolini, looks like rebasing with the correct LLVM commit made GitHub think I was the author of the commits on the branch!

TaoBi22 avatar May 05 '24 20:05 TaoBi22

No worries @TaoBi22 and thanks a lot for your help! Sorry for the delay in working on your commits @maerhart, had some issues with llvm and struggled a bit, luckily @TaoBi22 came to rescue. Getting everything done asap :)

luisacicolini avatar May 05 '24 20:05 luisacicolini

No worries, there's no need to stress. If you need help with something, let me know :)

maerhart avatar May 06 '24 07:05 maerhart

@maerhart all fixed now, this currently only supports single patterns, will open a new PR for the multi pattern :) [EDIT: it actually required fewer changes than I thought, so everything is here now]

luisacicolini avatar May 14 '24 11:05 luisacicolini

Adding multi patterns turned out to require just a few changes compared to this version, so now everything is pushed here :)

luisacicolini avatar May 15 '24 14:05 luisacicolini