Merge pull request #4 from hansjoergschurr/devel/cmake

Add cmake and Github workflow

.github/workflows/main.yml

@@ -0,0 +1,43 @@
+name: CI
+
+on:
+  push:
+    branches: [ main, devel/cmake ]
+  pull_request:
+    branches: [ main ]
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        name: [ production ]
+
+    name: ${{ matrix.os }}:${{ matrix.name }}
+    # The type of runner that the job will run on
+    runs-on: ${{ matrix.os }}
+
+    steps:
+    - uses: actions/checkout@v2
+    - name: Install Packages
+      if: runner.os == 'Linux'
+      run: |
+        sudo apt-get update
+        sudo apt-get install -y \
+          libgmp-dev
+    - name: Install Packages (MacOS)
+      if: runner.os == 'macOS'
+      run: |
+        brew install \
+          gmp
+    - name: Setup Build Dir
+      run: mkdir build
+    - name: Configure
+      run: cmake ..
+      working-directory: build
+    - name: Build
+      run: make -j2
+      working-directory: build
+    - name: Test
+      run: ctest --output-on-failure
+      working-directory: build

.gitignore

@@ -0,0 +1 @@
+build

CMakeLists.txt

@@ -0,0 +1,40 @@
+cmake_minimum_required (VERSION 3.12)
+
+macro(add_cxx_flag flag)
+  message(STATUS "Configure with flag '${flag}'")
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}")
+endmacro()
+
+project (alethelf_checker)
+
+set (CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
+
+find_package(GMP REQUIRED)
+set(LIBRARIES ${LIBRARIES} ${GMP_LIBRARIES})
+include_directories(${GMP_INCLUDE_DIR})
+
+if(NOT CMAKE_BUILD_TYPE)
+  message(STATUS "Defaulting to release build.")
+  set(CMAKE_BUILD_TYPE Release CACHE STRING "" FORCE)
+endif()
+
+add_cxx_flag("-Wall")
+add_cxx_flag("-Wno-deprecated")
+add_cxx_flag("-std=gnu++17")
+
+if(CMAKE_BUILD_TYPE STREQUAL "Debug")
+  add_cxx_flag("-g")
+  message(STATUS "Configured debug build.")
+elseif(CMAKE_BUILD_TYPE STREQUAL "Release")
+  message(STATUS "Configured release build.")
+else()
+  message(FATAL_ERROR "Invalid build type '${CMAKE_BUILD_TYPE}'")
+endif()
+
+enable_testing()
+
+include_directories(src)
+add_subdirectory(src)
+add_subdirectory(tests)
+add_subdirectory(proofs)
+

cmake/FindGMP.cmake

@@ -0,0 +1,12 @@
+# Try to find the GMP librairies
+# GMP_FOUND - system has GMP lib
+# GMP_INCLUDE_DIR - the GMP include directory
+# GMP_LIBRARIES - Libraries needed to use GMP
+
+find_path(GMP_INCLUDE_DIR NAMES gmp.h)
+find_library(GMP_LIBRARIES NAMES gmp libgmp)
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES)
+
+mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES)

proofs/CMakeLists.txt

@@ -0,0 +1,20 @@
+set(atc_test_file_list
+  theories/ArithBridge.smt2
+  theories/BitVectors.smt2
+  theories/Core.smt2
+  theories/Ints.smt2
+  theories/Reals.smt2
+)
+
+macro(atc_test file)
+  add_test(
+    NAME ${file}
+    COMMAND $<TARGET_FILE:atc> ${CMAKE_CURRENT_LIST_DIR}/${file}
+    WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
+  )
+  set_tests_properties(${file} PROPERTIES TIMEOUT 40)
+endmacro()
+
+foreach(file ${atc_test_file_list})
+  atc_test(${file})
+endforeach()

src/CMakeLists.txt

@@ -0,0 +1,3 @@
+file(GLOB atc_SRC CONFIGURE_DEPENDS "*.h" "*.cpp")
+
+add_executable(atc ${atc_SRC})

tests/CMakeLists.txt

@@ -0,0 +1,27 @@
+set(atc_test_file_list
+    Bools.smt2
+    literals.smt2
+    simple-pf2.smt2
+    simple.smt2
+    bv-dep-type.smt2
+    quoted.smt2
+    simple-pf-implicit.smt2
+    requires.smt2
+    simple-pf.smt2
+    evaluate.smt2
+    simple-include.smt2
+    simple-program.smt2
+)
+
+macro(atc_test file)
+  add_test(
+    NAME ${file}
+    COMMAND $<TARGET_FILE:atc> ${CMAKE_CURRENT_LIST_DIR}/${file}
+    WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
+  )
+  set_tests_properties(${file} PROPERTIES TIMEOUT 40)
+endmacro()
+
+foreach(file ${atc_test_file_list})
+  atc_test(${file})
+endforeach()