✨ Integrate LogicBlocks (#79)

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.

Co-authored-by: Sarah Schneider <sarah.schneider@jku.at>
Co-authored-by: burgholzer <burgholzer@me.com>

Author: 3 people

.github/workflows/codeql-analysis.yml

@@ -9,18 +9,58 @@ on:
     - cron: '15 21 * * 6'
 
 jobs:
-  analyze:
-    name:    Analyze
+  analyze-cpp:
+    name:    Analyze C++
     runs-on: ubuntu-latest
     permissions:
       actions:         read
       contents:        read
       security-events: write
 
-    strategy:
-      fail-fast: false
-      matrix:
-        language: [ 'cpp', 'python' ]
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      # Initializes the CodeQL tools for scanning.
+      - name: Initialize CodeQL
+        uses: github/codeql-action/init@v2
+        with:
+          languages: 'cpp'
+
+      - uses: actions/setup-python@v4
+        name: Install Python
+        with:
+          python-version: '3.10'
+
+      - name: Installing boost
+        run:  sudo apt-get install -y libboost-program-options-dev
+
+      - name: Install Z3
+        run:  python -m pip install z3-solver
+
+      - name: Configure CMake
+        run: |
+          export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$pythonLocation/lib/python3.10/site-packages/z3/lib 
+          export Z3_ROOT=$pythonLocation/lib/python3.10/site-packages/z3 
+          export Z3_DIR=$pythonLocation/lib/python3.10/site-packages/z3
+          cmake -S "${{github.workspace}}" -B "${{github.workspace}}/build" -DCMAKE_BUILD_TYPE=Release -DBUILD_QMAP_TESTS=ON -DBINDINGS=ON
+
+      - name: Build
+        run:  cmake --build "${{github.workspace}}/build" --parallel 4
+
+
+      - name: Perform CodeQL Analysis
+        uses: github/codeql-action/analyze@v2
+
+  analyze-python:
+    name:    Analyze Python
+    runs-on: ubuntu-latest
+    permissions:
+      actions:         read
+      contents:        read
+      security-events: write
 
     steps:
       - name: Checkout repository
@@ -32,9 +72,8 @@ jobs:
       - name: Initialize CodeQL
         uses: github/codeql-action/init@v2
         with:
-          languages: ${{ matrix.language }}
+          languages: 'python'
 
-      # Autobuild attempts to build any compiled languages  (C/C++, C#, or Java).
       - name: Autobuild
         uses: github/codeql-action/autobuild@v2
 

.gitmodules

@@ -3,3 +3,8 @@
 	url = https://github.com/cda-tum/qfr.git
 	branch = main
     shallow = true
+[submodule "extern/LogicBlocks"]
+	path = extern/LogicBlocks
+	url = https://github.com/IsFairy/LogicBlocks.git
+    branch = main
+    shallow = true

.lgtm.yml

@@ -10,11 +10,15 @@ extraction:
       packages:
         - python-pip
     after_prepare:
-      - export PATH=~/.local/bin:$PATH
+      - export PATH=~/.local/bin:~/.local/lib:$PATH
       - pip3 install cmake --user
+      - pip3 install z3-solver --user
       - cmake --version
+      - pip3 show z3-solver
     configure:
       command:
+        - export Z3_ROOT=~/.local/lib/python3.8/site-packages/z3
+        - export Z3_DIR=~/.local/lib/python3.8/site-packages/z3
         - cmake -S . -B build -DBUILD_QMAP_TESTS=ON -DBUILD_QFR_TESTS=ON -DBUILD_DD_PACKAGE_TESTS=ON -DBINDINGS=ON
     index:
       build_command:

CMakeLists.txt

@@ -35,26 +35,29 @@ if (NOT CMAKE_BUILD_TYPE AND NOT CMAKE_CONFIGURATION_TYPES)
 endif ()
 
 macro(check_submodule_present MODULENAME)
-	if(NOT EXISTS "${PROJECT_SOURCE_DIR}/extern/${MODULENAME}/CMakeLists.txt")
+	if (NOT EXISTS "${PROJECT_SOURCE_DIR}/extern/${MODULENAME}/CMakeLists.txt")
 		message(FATAL_ERROR "${MODULENAME} submodule not cloned properly. Please run `git submodule update --init --recursive` from the main project directory")
-	endif()
+	endif ()
 endmacro()
 
 check_submodule_present(qfr)
 
+check_submodule_present(LogicBlocks)
+
 # Add path for custom modules
-list (APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_SOURCE_DIR}/cmake")
+list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_SOURCE_DIR}/cmake")
 
 # search for Z3
 find_package(Z3)
-if(Z3_FOUND AND NOT TARGET z3::z3lib)
+if (Z3_FOUND AND NOT TARGET z3::z3lib)
 	message(STATUS "Found Z3 with version ${Z3_VERSION_STRING}")
 	add_library(z3::z3lib IMPORTED INTERFACE)
 	set_property(TARGET z3::z3lib PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${Z3_CXX_INCLUDE_DIRS})
 	set_property(TARGET z3::z3lib PROPERTY INTERFACE_LINK_LIBRARIES ${Z3_LIBRARIES})
-else()
+	add_definitions(-DZ3_FOUND)
+else ()
 	message(WARNING "Did not find Z3. Exact library and other depending target will not be available")
-endif()
+endif ()
 
 # add main library code
 add_subdirectory(src)
@@ -72,6 +75,6 @@ if (CMAKE_PROJECT_NAME STREQUAL PROJECT_NAME)
 endif ()
 
 # add Python binding code
-if(BINDINGS)
+if (BINDINGS)
 	add_subdirectory(mqt/qmap)
-endif()
+endif ()

MANIFEST.in

@@ -15,3 +15,5 @@ prune extern/qfr/extern/dd_package/extern
 prune extern/qfr/extern/zx/extern/googletest
 
 graft apps
+
+graft extern/LogicBlocks

cmake/FindZ3.cmake

@@ -3,9 +3,9 @@ INCLUDE(CheckCXXSourceRuns)
 
 # Function to check Z3's version
 function(check_z3_version z3_include z3_lib)
-	# The program that will be executed to print Z3's version.
-	file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
-	     "#include <assert.h>
+    # The program that will be executed to print Z3's version.
+    file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
+            "#include <assert.h>
         #include <z3.h>
         int main() {
           unsigned int major, minor, build, rev;
@@ -14,70 +14,70 @@ function(check_z3_version z3_include z3_lib)
           return 0;
        }")
 
-	# Get lib path
-	get_filename_component(z3_lib_path ${z3_lib} PATH)
+    # Get lib path
+    get_filename_component(z3_lib_path ${z3_lib} PATH)
 
-	try_run(
-			Z3_RETURNCODE
-			Z3_COMPILED
-			${CMAKE_BINARY_DIR}
-			${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
-			COMPILE_DEFINITIONS -I"${z3_include}"
-			LINK_LIBRARIES -L${z3_lib_path} -lz3
-			RUN_OUTPUT_VARIABLE SRC_OUTPUT
-	)
+    try_run(
+            Z3_RETURNCODE
+            Z3_COMPILED
+            ${CMAKE_BINARY_DIR}
+            ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
+            COMPILE_DEFINITIONS -I"${z3_include}"
+            LINK_LIBRARIES -L${z3_lib_path} -lz3
+            RUN_OUTPUT_VARIABLE SRC_OUTPUT
+    )
 
-	if(Z3_COMPILED)
-		string(REGEX REPLACE "([0-9]*\\.[0-9]*\\.[0-9]*)" "\\1"
-		       z3_version "${SRC_OUTPUT}")
-		set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE)
-	endif()
+    if (Z3_COMPILED)
+        string(REGEX REPLACE "([0-9]*\\.[0-9]*\\.[0-9]*)" "\\1"
+                z3_version "${SRC_OUTPUT}")
+        set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE)
+    endif ()
 endfunction(check_z3_version)
 
 # if Z3_ROOT is provided, check there first
 set(Z3_ROOT "" CACHE PATH "Root of Z3 distribution.")
 if (DEFINED ENV{Z3_ROOT})
-	set(Z3_ROOT $ENV{Z3_ROOT})
-	message("Z3_ROOT: ${Z3_ROOT}")
+    set(Z3_ROOT $ENV{Z3_ROOT})
+    message("Z3_ROOT: ${Z3_ROOT}")
 endif ()
 if (NOT ${Z3_ROOT} STREQUAL "")
-	find_path(Z3_CXX_INCLUDE_DIRS NAMES z3.h z3++.h
-	          NO_DEFAULT_PATH
-	          PATHS ${Z3_ROOT}/include
-	          PATH_SUFFIXES libz3 z3)
+    find_path(Z3_CXX_INCLUDE_DIRS NAMES z3.h z3++.h
+            NO_DEFAULT_PATH
+            PATHS ${Z3_ROOT}/include
+            PATH_SUFFIXES libz3 z3)
 
-	find_library(Z3_LIBRARIES NAMES z3 libz3
-	             NO_DEFAULT_PATH
-	             PATHS ${Z3_ROOT}
-	             PATH_SUFFIXES lib bin)
+    find_library(Z3_LIBRARIES NAMES z3 libz3
+            NO_DEFAULT_PATH
+            PATHS ${Z3_ROOT}
+            PATH_SUFFIXES lib bin)
 endif ()
 
 # see if a config file is available
 if (NOT Z3_CXX_INCLUDE_DIRS OR NOT Z3_LIBRARIES)
-	find_package(Z3 CONFIG)
-endif()
+    find_package(Z3 CONFIG)
+endif ()
 
 # try default paths as a last hope
 if (NOT Z3_FOUND)
-	find_path(Z3_CXX_INCLUDE_DIRS NAMES z3.h z3++.h
-	          PATH_SUFFIXES libz3 z3)
-	find_library(Z3_LIBRARIES NAMES z3 libz3
-	             PATH_SUFFIXES lib bin)
+    find_path(Z3_CXX_INCLUDE_DIRS NAMES z3.h z3++.h
+            PATH_SUFFIXES libz3 z3)
+    find_library(Z3_LIBRARIES NAMES z3 libz3
+            PATH_SUFFIXES lib bin)
 
-	unset(Z3_VERSION_STRING)
+    unset(Z3_VERSION_STRING)
 
-	# Try to check version by compiling a small program that prints Z3's version
-	if(Z3_CXX_INCLUDE_DIRS AND Z3_LIBRARIES)
-		check_z3_version(${Z3_CXX_INCLUDE_DIRS} ${Z3_LIBRARIES})
-	endif()
+    # Try to check version by compiling a small program that prints Z3's version
+    if (Z3_CXX_INCLUDE_DIRS AND Z3_LIBRARIES)
+        check_z3_version(${Z3_CXX_INCLUDE_DIRS} ${Z3_LIBRARIES})
+    endif ()
 
-	if(NOT Z3_VERSION_STRING)
-		set(Z3_VERSION_STRING "0.0.0")
-	endif()
+    if (NOT Z3_VERSION_STRING)
+        set(Z3_VERSION_STRING "0.0.0")
+    endif ()
 
-	include (FindPackageHandleStandardArgs)
-	find_package_handle_standard_args(Z3
-	                                  REQUIRED_VARS Z3_LIBRARIES Z3_CXX_INCLUDE_DIRS
-	                                  VERSION_VAR Z3_VERSION_STRING)
-	mark_as_advanced(Z3_CXX_INCLUDE_DIRS Z3_LIBRARIES)
-endif ()
+    include(FindPackageHandleStandardArgs)
+    find_package_handle_standard_args(Z3
+            REQUIRED_VARS Z3_LIBRARIES Z3_CXX_INCLUDE_DIRS
+            VERSION_VAR Z3_VERSION_STRING)
+    mark_as_advanced(Z3_CXX_INCLUDE_DIRS Z3_LIBRARIES)
+endif ()

extern/LogicBlocks

@@ -6,7 +6,6 @@
 #ifndef EXACT_MAPPER_hpp
 #define EXACT_MAPPER_hpp
 
-#include "Encodings.hpp"
 #include "Mapper.hpp"
 
 #include <algorithm>
@@ -16,10 +15,7 @@
 #include <functional>
 #include <set>
 #include <unordered_set>
-#include <z3++.h>
 
-using namespace z3;
-using matrix      = std::vector<expr_vector>;
 using Swaps       = std::vector<std::pair<unsigned short, unsigned short>>;
 using QubitChoice = std::set<unsigned short>;