Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

✨ Remove Logicblocks backend #347

Open
pehamTom opened this issue Jul 14, 2023 · 1 comment
Open

✨ Remove Logicblocks backend #347

pehamTom opened this issue Jul 14, 2023 · 1 comment
Assignees
Labels
enhancement Anything related to improvements of the existing library

Comments

@pehamTom
Copy link
Member

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 pehamTom added the enhancement Anything related to improvements of the existing library label Jul 14, 2023
@pehamTom pehamTom assigned pehamTom and unassigned burgholzer Jul 22, 2023
@burgholzer
Copy link
Member

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement Anything related to improvements of the existing library
Projects
None yet
Development

No branches or pull requests

2 participants