✨ Integrate LogicBlocks

[IsFairy]

This PR adds the https://github.com/IsFairy/LogicBlocks submodule as a drop-in replacement for the existing Z3 code.
It effectively replaces all existing Z3 code with a corresponding wrapper that allows for higher levels of abstraction and (in the future) for employing different solvers in QMAP.

[codecov]

Codecov Report

Merging #79 (3a36023) into main (c1b13f9) will increase coverage by 0.2%.
The diff coverage is 98.7%.

@@           Coverage Diff           @@
##            main     #79     +/-   ##
=======================================
+ Coverage   90.8%   91.1%   +0.2%     
=======================================
  Files         22      20      -2     
  Lines       1877    1726    -151     
  Branches     444     411     -33     
=======================================
- Hits        1706    1573    -133     
+ Misses       171     153     -18     

Impacted Files	Coverage Δ
include/exact/ExactMapper.hpp	100.0% <ø> (ø)
include/utils.hpp	83.3% <ø> (ø)
src/utils.cpp	89.2% <ø> (+13.1%)	⬆️
src/exact/ExactMapper.cpp	97.7% <98.6%> (-0.3%)	⬇️
src/Architecture.cpp	95.1% <100.0%> (-0.6%)	⬇️

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

[burgholzer]

Thanks for this contribution!
I just quickly went through all the changes and have some questions/remarks/requests. You can find all of them below. Most of them should be an easy fix. Some might require small refactorings in the LogicBlocks library.
Let me know if I can help.

[burgholzer]

Just went through all the changes here and left my comments below with some things to be addressed before this can be merged.
I still believe we should get this PR in before #78.

One thing I could not annotate in the changed files: The LGTM C++ run is failing for the same reason the CodeQL run was failing: a more recent version of Z3 is needed to build the project and the standard ubuntu repo only provides 4.8.7.
Two comments on that end:

• for one, it should not be possible to reach that point of failure at all. The LogicBlocks submodule should specify a minimum required version of Z3 so that compilation is not even started when no suitable version is installed.
• the fix for the LGTM run is similar to your fix for the CodeQL run: z3 has to be installed from pip and the respective paths have to be set as environment variables in https://github.com/cda-tum/qmap/blob/main/.lgtm.yml

Last but not least, I was wondering whether the "fallback" when z3 is not available should also be tested. Is this sufficiently implemented in the LogicBlocks module?

[burgholzer]

this URL has to be changed once the LogicBlocks project has been moved to the cda-tum organisation.

[IsFairy]

Last but not least, I was wondering whether the "fallback" when z3 is not available should also be tested. Is this sufficiently implemented in the LogicBlocks module?

The replacement, or fallback for z3 is still in the works for now and not really tested, so for the moment z3 is still required when using the exact mapper. The planned fallback (SMTLibv2 Export) also wont produce a model, so its something that the exact mapper will need to handle anyway.

[burgholzer]

Last but not least, I was wondering whether the "fallback" when z3 is not available should also be tested. Is this sufficiently implemented in the LogicBlocks module?

The replacement, or fallback for z3 is still in the works for now and not really tested, so for the moment z3 is still required when using the exact mapper. The planned fallback (SMTLibv2 Export) also wont produce a model, so its something that the exact mapper will need to handle anyway.

I see, makes sense. From that point of view, Z3 will be required for the foreseeable future when using QMAP.
At least until we figure out how to bundle another SMT solver (that works under all operating systems) with the distributed package and automatically employ it instead of Z3.

[lgtm-com]

This pull request introduces 1 alert when merging 974ae4a into c1b13f9 - view on LGTM.com

new alerts:

• 1 for Accidental rethrow

[burgholzer]

Two very small requests (in the comments), otherwise this seems almost ready.

LGTM shows two alerts in the LogicBlocks submodule that should be very quick to fix (see https://lgtm.com/projects/g/cda-tum/qmap/snapshot/72b875f873c787a1b50dd6a177f689ac21022440/files/extern/LogicBlocks/?sort=name&dir=ASC&mode=heatmap).

The wheel builds fails because the Z3 library is not picked up. This is most likely due to you deleting the FindZ3.cmake file. This leads to the libraries not being found in https://github.com/IsFairy/qmap/blob/974ae4a867603163abd0e901088b981e5b30a6ba/CMakeLists.txt#L51
And, potentially, Z3_FOUND not being truthy in https://github.com/IsFairy/qmap/blob/LogicBlocks/mqt/qmap/CMakeLists.txt.
But this is just a guess. This guess is supported by the fact that Windows wheels (where Z3 is installed including CMake Config files) works just fine.

[burgholzer]

Overall all the present changes LGTM. I would love to see the coverage check turn green, which probably requires covering 1-2 more lines.
To that end, I was wondering whether the following lines can simply be removed as they do not seem to be used anymore:
https://github.com/IsFairy/qmap/blob/1bf45637a875228c7402a664e3b87fa6bed7eabf/src/utils.cpp#L116-L144

What I was also thinking about: does the https://github.com/IsFairy/qmap/blob/LogicBlocks/include/configuration/Encoding.hpp file and code related to it still fit into this project or should it also be moved to the LogicBlocks submodule?
The same goes for https://github.com/IsFairy/qmap/blob/LogicBlocks/include/configuration/CommanderGrouping.hpp
Most probably, this should be done in a separate PR since it also requires tuning the bindings code here.