mqt-qmap icon indicating copy to clipboard operation
mqt-qmap copied to clipboard

✨ Remove Logicblocks backend

Open pehamTom opened this issue 1 year ago • 1 comments

What's the problem this feature will solve?

At the moment the Logicblocks library serves only as an abstraction layer to Z3 without adding much benefit. Since the Logicblocks library is probably not going to be maintained anymore, I propose removing it and replacing it with something else.

Describe the solution you'd like

An intermediate layer between SMT and SAT solvers is perfectly fine, however the most important features that such a layer should provide are:

  • easy export to Dimacs format
  • efficient representations (Logicblocks just stores an entire syntax tree)
  • active maintenance

With an export feature, we can still use Z3 but also other solvers as well without too much hassle.

pehamTom avatar Jul 14 '23 11:07 pehamTom

With the merge of #424, the situation has become quite a bit better here. I'd still like to remove the logicblocks completely and keep some of the useful wrappers at some point.

burgholzer avatar Feb 22 '24 10:02 burgholzer