diff --git a/.github/workflows/Dockerfile.archlinux b/.github/workflows/Dockerfile.archlinux index 9e6312e2f4..61b6e901e7 100644 --- a/.github/workflows/Dockerfile.archlinux +++ b/.github/workflows/Dockerfile.archlinux @@ -15,9 +15,10 @@ ARG build_type=Release ARG no_threads=1 # Specify Storm configuration (ON/OFF) -ARG gurobi_support="ON" -ARG soplex_support="ON" -ARG spot_support="ON" +ARG disable_gurobi="OFF" +ARG disable_spot="OFF" +ARG disable_mathsat="OFF" +ARG disable_soplex="OFF" ARG developer="OFF" ARG cln_exact="OFF" ARG cln_ratfunc="ON" @@ -48,15 +49,16 @@ RUN mkdir -p /opt/storm/build WORKDIR /opt/storm/build # Configure Storm -RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type \ +RUN cmake -DCMAKE_BUILD_TYPE=$build_type \ -DSTORM_PORTABLE=ON \ - -DSTORM_USE_GUROBI=$gurobi_support \ - -DSTORM_USE_SOPLEX=$soplex_support \ - -DSTORM_USE_SPOT_SYSTEM=$spot_support \ + -DSTORM_DISABLE_GUROBI=$disable_gurobi \ + -DSTORM_DISABLE_MATHSAT=$disable_mathsat \ + -DSTORM_DISABLE_SOPLEX=$disable_gurobi \ + -DSTORM_DISABLE_SPOT=$disable_spot \ -DSTORM_DEVELOPER=$developer \ -DSTORM_USE_CLN_EA=$cln_exact \ -DSTORM_USE_CLN_RF=$cln_ratfunc \ - $cmake_args + $cmake_args .. # Build external dependencies of Storm RUN make resources -j $no_threads @@ -68,5 +70,4 @@ RUN make storm -j $no_threads # (This can be skipped or adapted depending on custom needs) RUN make binaries -j $no_threads -# Set path -ENV PATH="/opt/storm/build/bin:$PATH" +WORKDIR /opt/storm diff --git a/.github/workflows/Dockerfile.doxygen b/.github/workflows/Dockerfile.doxygen index 749bce87a2..a358bc1acf 100644 --- a/.github/workflows/Dockerfile.doxygen +++ b/.github/workflows/Dockerfile.doxygen @@ -36,6 +36,7 @@ WORKDIR /opt/storm/build RUN cmake .. -DCMAKE_BUILD_TYPE=Release \ -DSTORM_PORTABLE=ON \ -DSTORM_USE_GUROBI=ON \ + -DSTORM_USE_MATHSAT=ON \ -DSTORM_USE_SOPLEX=ON \ -DSTORM_USE_SPOT_SYSTEM=ON diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index a979cb16ac..ebf384c790 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -4,8 +4,8 @@ name: Build Test on: schedule: - # run daily - - cron: '0 6 * * *' + # run daily + - cron: '0 6 * * *' # needed to trigger the workflow manually workflow_dispatch: pull_request: @@ -25,63 +25,68 @@ jobs: - {name: "GMP exact; GMP rational functions; All dependencies", baseImg: "storm-dependencies:latest-debug", buildType: "Debug", - Gurobi: "ON", - Soplex: "ON", - Spot: "ON", + disable_gurobi: "OFF", + disable_mathsat: "OFF", + disable_soplex: "OFF", + disable_spot: "OFF", Developer: "ON", ClnExact: "OFF", ClnRatfunc: "OFF", AllSanitizers: "ON", - cmakeArgs: "-DMSAT_ROOT=/opt/mathsat5" - } + cmakeArgs: "" + } - {name: "CLN exact; GMP rational functions; All dependencies", baseImg: "storm-dependencies:latest-debug", buildType: "Debug", - Gurobi: "ON", - Soplex: "ON", - Spot: "ON", + disable_gurobi: "OFF", + disable_mathsat: "OFF", + disable_soplex: "OFF", + disable_spot: "OFF", Developer: "ON", ClnExact: "ON", ClnRatfunc: "OFF", AllSanitizers: "ON", - cmakeArgs: "-DMSAT_ROOT=/opt/mathsat5" - } + cmakeArgs: "" + } - {name: "CLN exact; CLN rational functions; All dependencies", baseImg: "storm-dependencies:latest-debug", buildType: "Debug", - Gurobi: "ON", - Soplex: "ON", - Spot: "ON", + disable_gurobi: "OFF", + disable_mathsat: "OFF", + disable_soplex: "OFF", + disable_spot: "OFF", Developer: "ON", ClnExact: "ON", ClnRatfunc: "ON", AllSanitizers: "ON", - cmakeArgs: "-DMSAT_ROOT=/opt/mathsat5" - } + cmakeArgs: "" + } - {name: "GMP exact; CLN rational functions; No dependencies", baseImg: "storm-dependencies:latest-debug", buildType: "Debug", - Gurobi: "OFF", - Soplex: "OFF", - Spot: "OFF", + disable_gurobi: "ON", + disable_mathsat: "ON", + disable_soplex: "ON", + disable_spot: "ON", Developer: "ON", ClnExact: "OFF", ClnRatfunc: "ON", AllSanitizers: "ON", - cmakeArgs: "-DMSAT_ROOT=" - } - - {name: "Minimal dependencies", - baseImg: "storm-basesystem:minimal_dependencies", - buildType: "Debug", - Gurobi: "OFF", - Soplex: "OFF", - Spot: "OFF", + cmakeArgs: "" + } + - {name: "Minimal dependencies (without CLN!)", + baseImg: "storm-basesystem:minimal_dependencies", + buildType: "Debug", + disable_gurobi: "ON", + disable_mathsat: "ON", + disable_soplex: "ON", + disable_spot: "ON", Developer: "ON", ClnExact: "OFF", - ClnRatfunc: "ON", + ClnRatfunc: "OFF", AllSanitizers: "ON", - cmakeArgs: "-DMSAT_ROOT=" - } + cmakeArgs: "" + } steps: - name: Git clone uses: actions/checkout@v4 @@ -90,9 +95,10 @@ jobs: docker build -t movesrwth/storm:ci . \ --build-arg BASE_IMG=movesrwth/${{ matrix.config.baseImg }} \ --build-arg build_type="${{ matrix.config.buildType }}" \ - --build-arg gurobi_support="${{ matrix.config.Gurobi }}" \ - --build-arg soplex_support="${{ matrix.config.Soplex }}" \ - --build-arg spot_support="${{ matrix.config.Spot }}" \ + --build-arg disable_gurobi="${{ matrix.config.disable_gurobi }}" \ + --build-arg disable_mathsat="${{ matrix.config.disable_mathsat }}" \ + --build-arg disable_soplex="${{ matrix.config.disable_soplex }}" \ + --build-arg disable_spot="${{ matrix.config.disable_spot }}" \ --build-arg developer="${{ matrix.config.Developer }}" \ --build-arg cln_exact="${{ matrix.config.ClnExact }}" \ --build-arg cln_ratfunc="${{ matrix.config.ClnRatfunc }}" \ @@ -106,18 +112,43 @@ jobs: - name: Check release makeflags if: matrix.config.buildType == 'Release' run: | - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -O3' || (echo \"Error: Missing flag \'-O3\' for release build.\" && false)" - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -DNDEBUG' || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false)" + docker exec ci bash -c " grep -e \"-g\" /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; test $? -eq 1 || (echo \"Error: Unexpected flag \'-g\' for release build.\" && false)" + docker exec ci bash -c " grep -e \"-O3\" /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make || (echo \"Error: Missing flag \'-O3\' for release build.\" && false)" + docker exec ci bash -c " grep -e \"-DNDEBUG\" /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false)" - name: Check debug makeflags if: matrix.config.buildType == 'Debug' run: | - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -g' || (echo \"Error: Missing flag \'-g\' for debug build.\" && false)" + docker exec ci bash -c "if ! grep -q -e '-g' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-g' for debug build.\"; exit 1; fi" + docker exec ci bash -c "if grep -q -e '-O3' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-O3' for debug build.\"; exit 1; fi" + docker exec ci bash -c "if grep -q -e '-DNDEBUG' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-DNDEBUG' for debug build.\"; exit 1; fi" - name: Build tests run: docker exec ci bash -c "cd /opt/storm/build; make -j ${NR_JOBS}" - name: Run tests run: docker exec ci bash -c "cd /opt/storm/build; ASAN_OPTIONS=detect_leaks=0,detect_odr_violation=0 ctest test --output-on-failure" - + - name: Checkout starter-project + run: | + docker exec ci bash -c "git clone https://github.com/sjunges/storm-project-starter-cpp /opt/storm-starter" + docker exec ci bash -c "cd /opt/storm-starter; git checkout cmakeupdates" + - name: Configure and make starter project on intree storm. + run: | + docker exec ci bash -c "cd /opt/storm-starter; mkdir build-intree; cd build-intree; cmake -DNEVER_FETCH_STORM=TRUE -DSTORM_ROOT='/opt/storm/build' .." + docker exec ci bash -c "cd /opt/storm-starter/build-intree; make -j ${NR_JOBS}" + docker exec ci bash -c "/opt/storm-starter/build-intree/bin/starter-project --help" ## TODO using --help as running the starter-project requires Z3. + - name: Install storm + run: docker exec ci bash -c "cd /opt/storm/build; make install" + - name: Run installed storm + run: | + docker exec ci bash -c "mv /opt/storm/build /opt/storm/build-backup" + docker exec ci bash -c "/usr/local/bin/storm --version" + docker exec ci bash -c "mv /opt/storm/build-backup /opt/storm/build" + - name: Configure and make starter project on installed storm. + run: | + docker exec ci bash -c "mv /opt/storm/build /opt/storm/build-backup" + docker exec ci bash -c "cd /opt/storm-starter; mkdir build-installed; cd build-installed; cmake -DNEVER_FETCH_STORM=TRUE .." + docker exec ci bash -c "cd /opt/storm-starter/build-installed; make -j ${NR_JOBS}" + docker exec ci bash -c "/opt/storm-starter/build-installed/bin/starter-project --help" ## TODO using --help as running the starter-project requires Z3. + docker exec ci bash -c "mv /opt/storm/build-backup /opt/storm/build" compilerTests: # Build and run with different compilers (GCC, Clang) # Run on latest Archlinux version to get most recent compiler versions @@ -128,22 +159,24 @@ jobs: config: - {name: "GCC", buildType: "Debug", - Gurobi: "OFF", - Soplex: "OFF", - Spot: "OFF", + disable_gurobi: "ON", + disable_mathsat: "ON", + disable_soplex: "ON", + disable_spot: "ON", Developer: "ON", cmakeArgs: "-DCMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ -DSTORM_USE_SPOT_SHIPPED=ON", packages: "" - } + } - {name: "Clang", buildType: "Debug", - Gurobi: "OFF", - Soplex: "OFF", - Spot: "OFF", + disable_gurobi: "ON", + disable_mathsat: "ON", + disable_soplex: "ON", + disable_spot: "ON", Developer: "ON", cmakeArgs: "-DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DSTORM_USE_SPOT_SHIPPED=ON", packages: "clang" - } + } steps: - name: Git clone uses: actions/checkout@v4 @@ -153,9 +186,10 @@ jobs: run: | docker build -t movesrwth/storm:ci . \ --build-arg build_type="${{ matrix.config.buildType }}" \ - --build-arg gurobi_support="${{ matrix.config.Gurobi }}" \ - --build-arg soplex_support="${{ matrix.config.Soplex }}" \ - --build-arg spot_support="${{ matrix.config.Spot }}" \ + --build-arg disable_gurobi="${{ matrix.config.disable_gurobi }}" \ + --build-arg disable_mathsat="${{ matrix.config.disable_mathsat }}" \ + --build-arg disable_soplex="${{ matrix.config.disable_soplex }}" \ + --build-arg disable_spot="${{ matrix.config.disable_spot }}" \ --build-arg developer="${{ matrix.config.Developer }}" \ --build-arg cmake_args="${{ matrix.config.cmakeArgs }}" \ --build-arg packages="${{ matrix.config.packages }}" \ @@ -168,24 +202,50 @@ jobs: - name: Check release makeflags if: matrix.config.buildType == 'Release' run: | - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -O3' || (echo \"Error: Missing flag \'-O3\' for release build.\" && false)" - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -DNDEBUG' || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false)" + docker exec ci bash -c "if grep -q -e '-g' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-g' for release build.\"; exit 1; fi" + docker exec ci bash -c "if ! grep -q -e '-O3' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-O3' for release build.\"; exit 1; fi" + docker exec ci bash -c "if ! grep -q -e '-DNDEBUG' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-DNDEBUG' for release build.\"; exit 1; fi" - name: Check debug makeflags if: matrix.config.buildType == 'Debug' run: | - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -g' || (echo \"Error: Missing flag \'-g\' for debug build.\" && false)" + docker exec ci bash -c "if ! grep -q -e '-g' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-g' for debug build.\"; exit 1; fi" + docker exec ci bash -c "if grep -q -e '-O3' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-O3' for debug build.\"; exit 1; fi" + docker exec ci bash -c "if grep -q -e '-DNDEBUG' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-DNDEBUG' for debug build.\"; exit 1; fi" - name: Build tests run: docker exec ci bash -c "cd /opt/storm/build; make -j ${NR_JOBS}" - name: Run tests run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" + - name: Checkout starter-project + run: | + docker exec ci bash -c "git clone https://github.com/sjunges/storm-project-starter-cpp /opt/storm-starter" + docker exec ci bash -c "cd /opt/storm-starter; git checkout cmakeupdates" + - name: Configure and make starter project on intree storm. + run: | + docker exec ci bash -c "cd /opt/storm-starter; mkdir build-intree; cd build-intree; cmake -DNEVER_FETCH_STORM=TRUE -DSTORM_ROOT='/opt/storm/build' .." + docker exec ci bash -c "cd /opt/storm-starter/build-intree; make -j ${NR_JOBS}" + docker exec ci bash -c "/opt/storm-starter/build-intree/bin/starter-project /opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + - name: Install storm + run: docker exec ci bash -c "cd /opt/storm/build; make install" + - name: Run installed storm + run: | + docker exec ci bash -c "mv /opt/storm/build /opt/storm/build-backup" + docker exec ci bash -c "/usr/local/bin/storm --version" + docker exec ci bash -c "mv /opt/storm/build-backup /opt/storm/build" + - name: Configure and make starter project on installed storm. + run: | + docker exec ci bash -c "mv /opt/storm/build /opt/storm/build-backup" + docker exec ci bash -c "cd /opt/storm-starter; mkdir build-installed; cd build-installed; cmake -DNEVER_FETCH_STORM=TRUE .." + docker exec ci bash -c "cd /opt/storm-starter/build-installed; make -j ${NR_JOBS}" + docker exec ci bash -c "/opt/storm-starter/build-installed/bin/starter-project /opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + docker exec ci bash -c "mv /opt/storm/build-backup /opt/storm/build" linuxTests: name: Linux Tests (${{ matrix.distro }}, ${{ matrix.buildType }}) runs-on: ubuntu-latest strategy: matrix: - distro: ["debian-12", "ubuntu-22.04", "ubuntu-24.04"] + distro: ["debian-12", "ubuntu-24.04"] buildType: ["Release"] steps: - name: Git clone @@ -195,9 +255,10 @@ jobs: docker build -t movesrwth/storm:ci . \ --build-arg BASE_IMG=movesrwth/storm-basesystem:${{ matrix.distro }} \ --build-arg build_type="${{ matrix.buildType }}" \ - --build-arg gurobi_support="OFF" \ - --build-arg soplex_support="OFF" \ - --build-arg spot_support="OFF" \ + --build-arg disable_gurobi="ON" \ + --build-arg disable_mathsat="ON" \ + --build-arg disable_spot="ON" \ + --build-arg disable_soplex="ON" \ --build-arg no_threads=${NR_JOBS} # Omitting arguments developer, cln_exact, cln_ratfunc, all_sanitizers, cmake_args - name: Run Docker @@ -207,18 +268,43 @@ jobs: - name: Check release makeflags if: matrix.buildType == 'Release' run: | - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -O3' || (echo \"Error: Missing flag \'-O3\' for release build.\" && false)" - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -DNDEBUG' || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false)" + docker exec ci bash -c "if grep -q -e '-g' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-g' for release build.\"; exit 1; fi" + docker exec ci bash -c "if ! grep -q -e '-O3' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-O3' for release build.\"; exit 1; fi" + docker exec ci bash -c "if ! grep -q -e '-DNDEBUG' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-DNDEBUG' for release build.\"; exit 1; fi" - name: Check debug makeflags if: matrix.buildType == 'Debug' run: | - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -g' || (echo \"Error: Missing flag \'-g\' for debug build.\" && false)" + docker exec ci bash -c "if ! grep -q -e '-g' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-g' for debug build.\"; exit 1; fi" + docker exec ci bash -c "if grep -q -e '-O3' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-O3' for debug build.\"; exit 1; fi" + docker exec ci bash -c "if grep -q -e '-DNDEBUG' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-DNDEBUG' for debug build.\"; exit 1; fi" - name: Build tests run: docker exec ci bash -c "cd /opt/storm/build; make -j ${NR_JOBS}" - name: Run tests run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" - + - name: Checkout starter-project + run: | + docker exec ci bash -c "git clone https://github.com/sjunges/storm-project-starter-cpp /opt/storm-starter" + docker exec ci bash -c "cd /opt/storm-starter; git checkout cmakeupdates" + - name: Configure and make starter project on build-tree storm. + run: | + docker exec ci bash -c "cd /opt/storm-starter; mkdir build-intree; cd build-intree; cmake -DNEVER_FETCH_STORM=TRUE -DSTORM_ROOT='/opt/storm/build' .." + docker exec ci bash -c "cd /opt/storm-starter/build-intree; make -j ${NR_JOBS}" + docker exec ci bash -c "/opt/storm-starter/build-intree/bin/starter-project /opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + - name: Install storm + run: docker exec ci bash -c "cd /opt/storm/build; make install" + - name: Run installed storm + run: | + docker exec ci bash -c "mv /opt/storm/build /opt/storm/build-backup" + docker exec ci bash -c "/usr/local/bin/storm --version" + docker exec ci bash -c "mv /opt/storm/build-backup /opt/storm/build" + - name: Configure and make starter project on installed storm. + run: | + docker exec ci bash -c "mv /opt/storm/build /opt/storm/build-backup" + docker exec ci bash -c "cd /opt/storm-starter; mkdir build-installed; cd build-installed; cmake -DNEVER_FETCH_STORM=TRUE .." + docker exec ci bash -c "cd /opt/storm-starter/build-installed; make -j ${NR_JOBS}" + docker exec ci bash -c "/opt/storm-starter/build-installed/bin/starter-project /opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + docker exec ci bash -c "mv /opt/storm/build-backup /opt/storm/build" macTests: name: macOS Tests (${{ matrix.config.name }}) strategy: @@ -239,7 +325,11 @@ jobs: xcode: "16.2", buildType: "Release" } - buildType: ["Release"] + - { name: "XCode 16.2, ARM, Debug", + distro: "macos-15", + xcode: "16.2", + buildType: "Debug" + } runs-on: ${{ matrix.config.distro }} steps: - uses: maxim-lobanov/setup-xcode@v1 @@ -266,21 +356,50 @@ jobs: working-directory: ./build if: matrix.config.buildType == 'Release' run: | - ./bin/storm --version | grep 'with flags .* -O3' || (echo \"Error: Missing flag \'-O3\' for release build.\" && false) - ./bin/storm --version | grep 'with flags .* -DNDEBUG' || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false) + if grep -q -e '-g' src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-g' for release build.\"; exit 1; fi + if ! grep -q -e '-O3' src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-O3' for release build.\"; exit 1; fi + if ! grep -q -e '-DNDEBUG' src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-DNDEBUG' for release build.\"; exit 1; fi - name: Check debug makeflags working-directory: ./build if: matrix.config.buildType == 'Debug' run: | - ./bin/storm --version | grep 'with flags .* -g' || (echo \"Error: Missing flag \'-g\' for debug build.\" && false) - + if ! grep -q -e '-g' src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-g' for debug build.\"; exit 1; fi + if grep -q -e '-O3' src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-O3' for debug build.\"; exit 1; fi + if grep -q -e '-DNDEBUG' src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-DNDEBUG' for debug build.\"; exit 1; fi - name: Build tests working-directory: ./build run: make -j ${NR_JOBS} - name: Run tests working-directory: ./build run: ctest test--output-on-failure - + - name: Checkout starter-project + working-directory: . + run: | + cd ..; git clone https://github.com/sjunges/storm-project-starter-cpp storm-starter + cd storm-starter; git checkout cmakeupdates + - name: Configure and make starter project on intree storm. + working-directory: . + run: | + cd ../storm-starter; mkdir build-intree; cd build-intree; cmake -DNEVER_FETCH_STORM=TRUE -DSTORM_ROOT="${GITHUB_WORKSPACE}/build" .. + make -j ${NR_JOBS} + ./bin/starter-project ${GITHUB_WORKSPACE}/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]' + - name: Install storm + working-directory: ./build + run: sudo make install + - name: Run installed storm + working-directory: . + run: | + mv ${GITHUB_WORKSPACE}/build ${GITHUB_WORKSPACE}/build-backup + /usr/local/bin/storm --version + mv ${GITHUB_WORKSPACE}/build-backup ${GITHUB_WORKSPACE}/build + - name: Configure and make starter project on installed storm. + working-directory: . + run: | + mv ${GITHUB_WORKSPACE}/build ${GITHUB_WORKSPACE}/build-backup + cd ../storm-starter; mkdir build-installed; cd build-installed; cmake -DNEVER_FETCH_STORM=TRUE .. + make -j ${NR_JOBS} + ./bin/starter-project ${GITHUB_WORKSPACE}/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]' + mv ${GITHUB_WORKSPACE}/build-backup ${GITHUB_WORKSPACE}/build deploy: name: Test and Deploy (${{ matrix.buildType.name }}) runs-on: ubuntu-latest @@ -291,12 +410,12 @@ jobs: dockerTag: "ci-debug", baseImg: "storm-dependencies:latest-debug", Developer: "ON" - } + } - {name: "Release", dockerTag: "ci", baseImg: "storm-dependencies:latest", Developer: "OFF" - } + } steps: - name: Git clone uses: actions/checkout@v4 @@ -313,7 +432,7 @@ jobs: --build-arg developer="${{ matrix.buildType.Developer }}" \ --build-arg cmake_args="${{ matrix.buildType.cmakeArgs }}" \ --build-arg no_threads=${NR_JOBS} - # Omitting arguments gurobi_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers + # Omitting arguments gurobi_support, mathsat_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers - name: Run Docker run: docker run -d -it --name ci movesrwth/storm:${{ matrix.buildType.dockerTag }} @@ -321,18 +440,43 @@ jobs: - name: Check release makeflags if: matrix.buildType.name == 'Release' run: | - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -O3' || (echo \"Error: Missing flag \'-O3\' for release build.\" && false)" - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -DNDEBUG' || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false)" + docker exec ci bash -c "if grep -q -e '-g' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-g' for release build.\"; exit 1; fi" + docker exec ci bash -c "if ! grep -q -e '-O3' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-O3' for release build.\"; exit 1; fi" + docker exec ci bash -c "if ! grep -q -e '-DNDEBUG' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-DNDEBUG' for release build.\"; exit 1; fi" - name: Check debug makeflags if: matrix.buildType.name == 'Debug' run: | - docker exec ci bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -g' || (echo \"Error: Missing flag \'-g\' for debug build.\" && false)" + docker exec ci bash -c "if ! grep -q -e '-g' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Missing flag '-g' for debug build.\"; exit 1; fi" + docker exec ci bash -c "if grep -q -e '-O3' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-O3' for debug build.\"; exit 1; fi" + docker exec ci bash -c "if grep -q -e '-DNDEBUG' /opt/storm/build/src/storm/CMakeFiles/storm.dir/flags.make; then echo \"Error: Unexpected flag '-DNDEBUG' for debug build.\"; exit 1; fi" - name: Build tests run: docker exec ci bash -c "cd /opt/storm/build; make -j ${NR_JOBS}" - name: Run tests run: docker exec ci bash -c "cd /opt/storm/build; ctest test --output-on-failure" - + - name: Checkout starter-project + run: | + docker exec ci bash -c "git clone https://github.com/sjunges/storm-project-starter-cpp /opt/storm-starter" + docker exec ci bash -c "cd /opt/storm-starter; git checkout cmakeupdates" + - name: Configure and make starter project on intree storm. + run: | + docker exec ci bash -c "cd /opt/storm-starter; mkdir build-intree; cd build-intree; cmake -DNEVER_FETCH_STORM=TRUE -DSTORM_ROOT='/opt/storm/build' .." + docker exec ci bash -c "cd /opt/storm-starter/build-intree; make -j ${NR_JOBS}" + docker exec ci bash -c "/opt/storm-starter/build-intree/bin/starter-project /opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + - name: Install storm + run: docker exec ci bash -c "cd /opt/storm/build; make install" + - name: Run installed storm + run: | + docker exec ci bash -c "mv /opt/storm/build /opt/storm/build-backup" + docker exec ci bash -c "/usr/local/bin/storm --version" + docker exec ci bash -c "mv /opt/storm/build-backup /opt/storm/build" + - name: Configure and make starter project on installed storm. + run: | + docker exec ci bash -c "mv /opt/storm/build /opt/storm/build-backup" + docker exec ci bash -c "cd /opt/storm-starter; mkdir build-installed; cd build-installed; cmake -DNEVER_FETCH_STORM=TRUE .." + docker exec ci bash -c "cd /opt/storm-starter/build-installed; make -j ${NR_JOBS}" + docker exec ci bash -c "/opt/storm-starter/build-installed/bin/starter-project /opt/storm/resources/examples/testfiles/dtmc/brp-16-2.pm 'P=? [F s=5]'" + docker exec ci bash -c "mv /opt/storm/build-backup /opt/storm/build" - name: Login into docker # Only login if using master on original repo (and not for pull requests or forks) if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master' @@ -365,4 +509,4 @@ jobs: For more information, see https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}" to: ${{ secrets.STORM_CI_MAIL_RECIPIENTS }} from: Github Actions - if: env.WORKFLOW_CONCLUSION != 'success' # notify only if failure + if: env.WORKFLOW_CONCLUSION != 'success' # notify only if failure \ No newline at end of file diff --git a/.github/workflows/release_docker.yml b/.github/workflows/release_docker.yml index 18f1178f09..3fb29f3272 100644 --- a/.github/workflows/release_docker.yml +++ b/.github/workflows/release_docker.yml @@ -39,7 +39,7 @@ jobs: --build-arg developer="${{ matrix.buildType.Developer }}" \ --build-arg cmake_args="${{ matrix.buildType.cmakeArgs }}" \ --build-arg no_threads=${NR_JOBS} - # Omitting arguments gurobi_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers + # Omitting arguments gurobi_support, soplex_support, mathsat_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers - name: Login to Docker Hub # Only login if using original repo if: github.repository_owner == 'moves-rwth' diff --git a/CMakeLists.txt b/CMakeLists.txt index 06d4c92780..8a0c0a65a8 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,31 +1,34 @@ -cmake_minimum_required (VERSION 3.22) - -set(CMAKE_CXX_STANDARD 20) +cmake_minimum_required (VERSION 3.23) +if (NOT ${CMAKE_VERSION} VERSION_LESS 3.24) + cmake_policy(VERSION 3.24) +endif() # Set project name project (storm CXX C) -# Add base folder for better inclusion paths -# include_directories("${PROJECT_SOURCE_DIR}/src") - -# Add the resources/cmake folder to Module Search Path for FindTBB.cmake -set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/resources/cmake/find_modules" "${PROJECT_SOURCE_DIR}/resources/cmake/macros") +# Add the resources/cmake folder to Module Search Path +set(STORM_CMAKE_FIND_MODULES "${PROJECT_SOURCE_DIR}/resources/cmake/find_modules") +set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${STORM_CMAKE_FIND_MODULES}" "${PROJECT_SOURCE_DIR}/resources/cmake/macros") +add_custom_target(storm_resources) include(ExternalProject) -include(RegisterSourceGroup) include(imported) include(CheckCXXSourceCompiles) include(CheckCSourceCompiles) include(ProcessorCount) +set(CMAKE_CXX_STANDARD 20) + ############################################################# ## ## CMake options of Storm ## ############################################################# +## Compilation options. option(STORM_DEVELOPER "Sets whether the development mode is used." OFF) option(STORM_ALLWARNINGS "Compile with even more warnings" OFF) -option(STORM_USE_LTO "Sets whether link-time optimizations are enabled." ON) +# TODO revert to standard on +option(STORM_USE_LTO "Sets whether link-time optimizations are enabled." OFF) MARK_AS_ADVANCED(STORM_USE_LTO) option(STORM_USE_THIN_LTO "Sets whether thin link-time optimizations are enabled (faster compile times than normal LTO)." OFF) MARK_AS_ADVANCED(STORM_USE_THIN_LTO) @@ -34,53 +37,49 @@ MARK_AS_ADVANCED(STORM_PORTABLE) # Force POPCNT is helpful for portable code targetting platforms with SSE4.2 operation support. option(STORM_FORCE_POPCNT "Sets whether the popcnt instruction is forced to be used (advanced)." OFF) MARK_AS_ADVANCED(STORM_FORCE_POPCNT) -option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." OFF) -option(STORM_USE_INTELTBB "Sets whether the Intel TBB libraries should be used." OFF) -option(STORM_USE_GUROBI "Sets whether Gurobi should be used." OFF) -option(STORM_USE_SOPLEX "Sets whether Soplex should be used." OFF) -set(STORM_CARL_DIR_HINT "" CACHE STRING "A hint where the preferred CArL version can be found. If CArL cannot be found there, it is searched in the OS's default paths.") -option(STORM_FORCE_SHIPPED_CARL "Sets whether the shipped version of carl is to be used no matter whether carl is found or not." OFF) -MARK_AS_ADVANCED(STORM_FORCE_SHIPPED_CARL) -option(USE_SMTRAT "Sets whether SMT-RAT should be included." OFF) -mark_as_advanced(USE_SMTRAT) -option(STORM_USE_SPOT_SYSTEM "Sets whether the system version of Spot should be included (if found)." ON) -option(STORM_USE_SPOT_SHIPPED "Sets whether Spot should be downloaded and installed (if system version is not available or not used)." OFF) -option(XML_SUPPORT "Sets whether xml based format parsing should be included." ON) -option(FORCE_COLOR "Force color output" OFF) -mark_as_advanced(FORCE_COLOR) option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON) mark_as_advanced(STORM_COMPILE_WITH_CCACHE) option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF) +option(STORM_COMPILE_WITH_ADDRESS_SANITIZER "Sets whether to compile with AddressSanitizer enabled" OFF) +option(STORM_COMPILE_WITH_ALL_SANITIZERS "Sets whether to compile with all sanitizers enabled" OFF) +option(STORM_COMPILE_WITH_COMPILATION_PROFILING "Compile with output to profile compilation process" OFF) +MARK_AS_ADVANCED(STORM_COMPILE_WITH_COMPILATION_PROFILING) option(STORM_USE_CLN_EA "Sets whether CLN instead of GMP numbers should be used for exact arithmetic." OFF) export_option(STORM_USE_CLN_EA) option(STORM_USE_CLN_RF "Sets whether CLN instead of GMP numbers should be used for rational functions." ON) export_option(STORM_USE_CLN_RF) -option(BUILD_SHARED_LIBS "Build the Storm library dynamically" OFF) -option(STORM_DEBUG_CUDD "Build CUDD in debug mode." OFF) -MARK_AS_ADVANCED(STORM_DEBUG_CUDD) -option(STORM_DEBUG_SYLVAN "Build Sylvan in debug mode." OFF) -MARK_AS_ADVANCED(STORM_DEBUG_SYLVAN) + +## Configuration setup. option(STORM_EXCLUDE_TESTS_FROM_ALL "If set, tests will not be compiled by default" OFF ) export_option(STORM_EXCLUDE_TESTS_FROM_ALL) MARK_AS_ADVANCED(STORM_EXCLUDE_TESTS_FROM_ALL) -set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).") -set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") -set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") -set(MSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (optional).") -set(SPOT_ROOT "" CACHE STRING "The hint to the root directory of Spot (optional).") -MARK_AS_ADVANCED(SPOT_ROOT) option(STORM_LOAD_QVBS "Sets whether the Quantitative Verification Benchmark Set (QVBS) should be downloaded." OFF) set(STORM_QVBS_ROOT "" CACHE STRING "The root directory of the Quantitative Verification Benchmark Set (QVBS) in case it should not be downloaded (optional).") MARK_AS_ADVANCED(STORM_QVBS_ROOT) -set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") -set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.") -set(USE_XERCESC ${XML_SUPPORT}) -mark_as_advanced(USE_XERCESC) -option(STORM_COMPILE_WITH_ADDRESS_SANITIZER "Sets whether to compile with AddressSanitizer enabled" OFF) -option(STORM_COMPILE_WITH_ALL_SANITIZERS "Sets whether to compile with all sanitizers enabled" OFF) -option(STORM_COMPILE_WITH_COMPILATION_PROFILING "Compile with output to profile compilation process" OFF) -MARK_AS_ADVANCED(STORM_COMPILE_WITH_COMPILATION_PROFILING) +## Configuring dependencies +set(STORM_CARL_GIT_REPO "https://github.com/sjunges/carl-storm.git" CACHE STRING "For fetching carl: which git repo to use") +set(STORM_CARL_GIT_TAG "e16e865a934853459d68d30e13e494b74db1fc0b" CACHE STRING "For fetching carl: which git tag to use") +option(STORM_DISABLE_GUROBI "Sets whether linking with Gurobi should be disabled." OFF) +set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi.") +option(STORM_DISABLE_MATHSAT "Sets whether linking with MathSat should be disabled." OFF) +set(MATHSAT_ROOT "" CACHE STRING "A hint to the root directory of MathSAT.") +option(STORM_DISABLE_SPOT "Sets whether linking with Spot should be disabled." OFF) +option(STORM_USE_SPOT_SHIPPED "Sets whether Spot should be downloaded and installed (if system version is not available)." OFF) +set(SPOT_ROOT "" CACHE STRING "A hint to the root directory of Spot.") +MARK_AS_ADVANCED(SPOT_ROOT) +option(STORM_DISABLE_SOPLEX "Sets whether linking with Soplex should be disabled." OFF) +option(STORM_DISABLE_XERCES "Sets whether linking with Xerces should be disabled." OFF) +set(XERCESC_ROOT "" CACHE STRING "A hint to the root directory of Xerces (optional).") +mark_as_advanced(XERCESC_ROOT) +option(STORM_DISABLE_Z3 "Sets whether linking with Spot should be disabled." Z3) +set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3.") +mark_as_advanced(Z3_ROOT) + +option(STORM_DEBUG_CUDD "Build CUDD in debug mode." OFF) +MARK_AS_ADVANCED(STORM_DEBUG_CUDD) +option(STORM_DEBUG_SYLVAN "Build Sylvan in debug mode." OFF) +MARK_AS_ADVANCED(STORM_DEBUG_SYLVAN) if (STORM_COMPILE_WITH_ALL_SANITIZERS) set(STORM_COMPILE_WITH_ADDRESS_SANITIZER ON) @@ -103,31 +102,22 @@ mark_as_advanced(CMAKE_OSX_SYSROOT) mark_as_advanced(CMAKE_OSX_DEPLOYMENT_TARGET) # Offer the user the choice of overriding the installation directories -set(INCLUDE_INSTALL_DIR include/ CACHE PATH "Installation directory for header files" ) -set(LIB_INSTALL_DIR lib/ CACHE PATH "Installation directory for libraries") -#set(SYSCONFIG_INSTALL_DIR etc/carl/ CACHE PATH "Installation for system configuration files) -set(BIN_INSTALL_DIR lib/ CACHE PATH "Installation directory for executables") - - -# Install dir for cmake files (info for other libraries that include Storm) -set(DEF_INSTALL_CMAKE_DIR "lib/CMake/storm") -set(CMAKE_INSTALL_DIR ${DEF_INSTALL_CMAKE_DIR} CACHE PATH "Installation directory for CMake files") - -# Add CMake install prefix -foreach(p LIB BIN INCLUDE CMAKE) - set(var ${p}_INSTALL_DIR) - if(NOT IS_ABSOLUTE "${${var}}") - set(${var} "${CMAKE_INSTALL_PREFIX}/${${var}}") - endif() -endforeach() - -message(STATUS "Storm - CMake install dir: ${CMAKE_INSTALL_DIR}") +set(STORM_INCLUDE_INSTALL_DIR include/storm CACHE PATH "Installation directory for header files" ) +set(STORM_LIB_INSTALL_DIR lib/storm CACHE PATH "Installation directory for libraries") +set(STORM_BIN_INSTALL_DIR bin/storm CACHE PATH "Installation directory for executables") +set(STORM_CMAKE_INSTALL_DIR lib/cmake/storm CACHE PATH "Installation directory for CMake files") +set(STORM_RESOURCE_INCLUDE_INSTALL_DIR include/storm/resources/ CACHE PATH "Installation directory for dependency header files") +set(STORM_RESOURCE_LIBRARY_INSTALL_DIR lib/storm/resources/ CACHE PATH "Installation directory for depency library files") +set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) +set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) +set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) # If the STORM_DEVELOPER option was turned on, by default we target a debug version, otherwise a release version. if (STORM_DEVELOPER) if (NOT CMAKE_BUILD_TYPE) set(CMAKE_BUILD_TYPE "DEBUG") - endif() + endif() + # TODO Do this more targeted add_definitions(-DSTORM_DEV) set(STORM_DEBUG_CUDD ON) set(STORM_DEBUG_SYLVAN ON) @@ -182,43 +172,15 @@ else() ENDIF() message(STATUS "Storm - Detected operating system ${OPERATING_SYSTEM}.") -# Set compile flags for dependencies -if(STORM_USE_CLN_EA OR STORM_USE_CLN_RF) - set(SHIPPED_CARL_USE_CLN_NUMBERS ON) - set(SHIPPED_CARL_USE_GINAC ON) -else() - set(SHIPPED_CARL_USE_CLN_NUMBERS OFF) - set(SHIPPED_CARL_USE_GINAC OFF) -endif() - -# Warning for Apple Silicon -if(APPLE_SILICON) - message(WARNING "Compiling natively on Apple Silicon is experimental. Please report any issues to support@stormchecker.org.") -endif() - - -set(DYNAMIC_EXT ".so") set(STATIC_EXT ".a") set(LIB_PREFIX "lib") if(MACOSX) set(DYNAMIC_EXT ".dylib") - set(STATIC_EXT ".a") - set(LIB_PREFIX "lib") -elseif (WIN32) - set(DYNAMIC_EXT ".dll") - set(STATIC_EXT ".lib") - set(LIB_PREFIX "") -endif() -message(STATUS "Storm - Assuming extension for shared libraries: ${DYNAMIC_EXT}") -message(STATUS "Storm - Assuming extension for static libraries: ${STATIC_EXT}") - -if(BUILD_SHARED_LIBS) - set(LIB_EXT ${DYNAMIC_EXT}) - message(STATUS "Storm - Build dynamic libraries.") else() - set(LIB_EXT ${STATIC_EXT}) - message(STATUS "Storm - Build static libraries.") + set(DYNAMIC_EXT ".so") endif() +message(VERBOSE "Storm - Assuming extension for shared libraries: ${DYNAMIC_EXT}") +message(VERBOSE "Storm - Assuming extension for static libraries: ${STATIC_EXT}") ############################################################# ## @@ -287,10 +249,6 @@ endif() ## ############################################################# if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG) - if(FORCE_COLOR) - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics") - endif() - if (LINUX) set(CLANG_STDLIB libstdc++) else() @@ -298,7 +256,6 @@ if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG) endif() set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -stdlib=${CLANG_STDLIB} -ftemplate-depth=1024") - set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE}") if(LINUX) set (CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -rdynamic") @@ -308,12 +265,12 @@ if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG) set (CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-export_dynamic") endif() elseif (STORM_COMPILER_GCC) - if(FORCE_COLOR) - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color=always") - endif() set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fprefetch-loop-arrays") set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -rdynamic") set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -rdynamic") + + # Do not warn about problems internally to GCC 12 + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-stringop-overflow") endif () if (STORM_USE_THIN_LTO) @@ -359,6 +316,8 @@ endif() if (STORM_DEVELOPER) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -pedantic") if (STORM_ALLWARNINGS) + # With gcc, we already set (almost) all warnings. + # With Clang, we can even go further using Weverything, which is not always helpful, which is why these options are guarded by STORM_ALL_WARNINGS if (CLANG) # Enable strictly every warning and then disable selected ones. set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Weverything") @@ -418,9 +377,6 @@ if (STORM_DEVELOPER) set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-documentation-unknown-command") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-missing-noreturn") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-missing-prototypes") - - - endif () else () set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wextra") @@ -487,7 +443,8 @@ SET(CMAKE_SKIP_BUILD_RPATH FALSE) SET(CMAKE_BUILD_WITH_INSTALL_RPATH FALSE) # the RPATH to be used when installing -SET(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/lib") +# TODO move these to the right targets rather than setting them globally. +SET(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/lib;${CMAKE_INSTALL_PREFIX}/lib/storm;${CMAKE_INSTALL_PREFIX}/lib/storm/resources") # don't add the automatically determined parts of the RPATH # which point to directories outside the build tree to the install RPATH @@ -498,20 +455,9 @@ SET(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE) ## Generator specific settings ## ############################################################# -if ("${CMAKE_GENERATOR}" STREQUAL "Xcode") - message(WARNING "Using the XCode Project Generator has previously yielded problems. See https://github.com/moves-rwth/storm/issues/65. We recommend using the command line or an IDE with native CMAKE support, such as CLION.") - set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LANGUAGE_STANDARD "c++17") - set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LIBRARY "libc++") -endif() - # Display information about build configuration. message(STATUS "Storm - Using compiler configuration ${STORM_COMPILER_ID} ${STORM_COMPILER_VERSION}.") -if (STORM_DEVELOPER) - message(STATUS "Storm - CXX Flags: ${CMAKE_CXX_FLAGS}") - message(STATUS "Storm - CXX Debug Flags: ${CMAKE_CXX_FLAGS_DEBUG}") - message(STATUS "Storm - CXX Release Flags: ${CMAKE_CXX_FLAGS_RELEASE}") - message(STATUS "Storm - Build type: ${CMAKE_BUILD_TYPE}") -endif() +message(STATUS "Storm - Build type: ${CMAKE_BUILD_TYPE}") ############################################################# ############################################################# @@ -531,47 +477,63 @@ endif() # in the the system does not have a library include(resources/3rdparty/CMakeLists.txt) -# Include Doxygen -include(resources/doxygen/CMakeLists.txt) +if(STORM_HAVE_GLPK OR STORM_HAVE_GUROBI OR STORM_HAVE_SOPLEX OR STORM_HAVE_Z3_OPTIMIZE) + set(STORM_HAVE_LP_SOLVER ON) + message(STATUS "Storm -- compiled with an LP solver!") +else() + set(STORM_HAVE_LP_SOLVER OFF) + message(WARNING "Storm -- compiled without LP solver! This may yield errors at run time.") +endif() +if(PROJECT_IS_TOP_LEVEL) + # Include Doxygen + include(resources/doxygen/CMakeLists.txt) +endif() ############################################################# ## ## CMake-generated Config File for Storm ## ############################################################# -# try to obtain the current version from git. -include(GetGitRevisionDescription) -get_git_head_revision(STORM_VERSION_REFSPEC STORM_VERSION_GIT_HASH) -git_describe(STORM_GIT_VERSION_STRING) - -# parse the git tag into variables -# start with major.minor.patch -string(REGEX MATCH "^([0-9]+)\\.([0-9]+)\\.([0-9]+)(.*)$" STORM_VERSION_MATCH "${STORM_GIT_VERSION_STRING}") -set(STORM_VERSION_MAJOR "${CMAKE_MATCH_1}") -set(STORM_VERSION_MINOR "${CMAKE_MATCH_2}") -set(STORM_VERSION_PATCH "${CMAKE_MATCH_3}") -set(STORM_GIT_VERSION_REST "${CMAKE_MATCH_4}") -# parse rest of the form (-label)-commitsahead-hash(-appendix) -string(REGEX MATCH "^(\\-([a-z][a-z0-9\\.]+))?\\-([0-9]+)\\-([a-z0-9]+)(\\-.*)?$" STORM_VERSION_REST_MATCH "${STORM_GIT_VERSION_REST}") -set(STORM_VERSION_LABEL "${CMAKE_MATCH_2}") # might be empty -set(STORM_VERSION_COMMITS_AHEAD "${CMAKE_MATCH_3}") -set(STORM_VERSION_TAG_HASH "${CMAKE_MATCH_4}") # is not used -set(STORM_VERSION_APPENDIX "${CMAKE_MATCH_5}") # might be empty +if (PROJECT_IS_TOP_LEVEL) + # try to obtain the current version from git. + include(GetGitRevisionDescription) + get_git_head_revision(STORM_VERSION_REFSPEC STORM_VERSION_GIT_HASH) + git_describe(STORM_GIT_VERSION_STRING) + + # parse the git tag into variables + # start with major.minor.patch + string(REGEX MATCH "^([0-9]+)\\.([0-9]+)\\.([0-9]+)(.*)$" STORM_VERSION_MATCH "${STORM_GIT_VERSION_STRING}") + set(STORM_VERSION_MAJOR "${CMAKE_MATCH_1}") + set(STORM_VERSION_MINOR "${CMAKE_MATCH_2}") + set(STORM_VERSION_PATCH "${CMAKE_MATCH_3}") + set(STORM_GIT_VERSION_REST "${CMAKE_MATCH_4}") + # parse rest of the form (-label)-commitsahead-hash(-appendix) + string(REGEX MATCH "^(\\-([a-z][a-z0-9\\.]+))?\\-([0-9]+)\\-([a-z0-9]+)(\\-.*)?$" STORM_VERSION_REST_MATCH "${STORM_GIT_VERSION_REST}") + set(STORM_VERSION_LABEL "${CMAKE_MATCH_2}") # might be empty + set(STORM_VERSION_COMMITS_AHEAD "${CMAKE_MATCH_3}") + set(STORM_VERSION_TAG_HASH "${CMAKE_MATCH_4}") # is not used + set(STORM_VERSION_APPENDIX "${CMAKE_MATCH_5}") # might be empty +else() + set(STORM_GIT_VERSION_STRING "NOTFOUND") +endif() # check whether the git version lookup failed if (STORM_GIT_VERSION_STRING MATCHES "NOTFOUND") set(STORM_VERSION_SOURCE "VersionSource::Static") set(STORM_VERSION_COMMITS_AHEAD 0) set(STORM_VERSION_DIRTY DirtyState::Unknown) + set(STORM_VERSION_TWEAK 0) include(version.cmake) message(WARNING "Storm - Git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.") else() set(STORM_VERSION_SOURCE "VersionSource::Git") if ("${STORM_VERSION_APPENDIX}" MATCHES "^.*dirty.*$") set(STORM_VERSION_DIRTY "DirtyState::Dirty") + set(STORM_VERSION_TWEAK 1) else() set(STORM_VERSION_DIRTY "DirtyState::Clean") + set(STORM_VERSION_TWEAK 0) endif() endif() @@ -612,20 +574,22 @@ configure_file ( "${PROJECT_BINARY_DIR}/include/storm-config.h" ) -# Add the binary dir include directory for storm-config.h -include_directories("${PROJECT_BINARY_DIR}/include") - -include(CTest) -# Compiles all tests -add_custom_target(tests) -# Compiles and runs all tests -add_custom_target(check COMMAND ${CMAKE_CTEST_COMMAND} --output-on-failure) -set(CMAKE_CTEST_COMMAND_VERBOSE ${CMAKE_CTEST_COMMAND} -V) -add_custom_target(check-verbose COMMAND ${CMAKE_CTEST_COMMAND_VERBOSE}) -add_dependencies(check tests) -add_dependencies(check-verbose tests) -# Apply code formatting -add_custom_target(format COMMAND ${PROJECT_SOURCE_DIR}/resources/scripts/auto-format.sh) +if(PROJECT_IS_TOP_LEVEL) + include(CTest) + # Compiles all tests + add_custom_target(tests) + # Compiles and runs all tests + add_custom_target(check COMMAND ${CMAKE_CTEST_COMMAND} --output-on-failure) + set(CMAKE_CTEST_COMMAND_VERBOSE ${CMAKE_CTEST_COMMAND} -V) + add_custom_target(check-verbose COMMAND ${CMAKE_CTEST_COMMAND_VERBOSE}) + add_dependencies(check tests) + add_dependencies(check-verbose tests) +endif() + +if(PROJECT_IS_TOP_LEVEL) + # Apply code formatting + add_custom_target(format COMMAND ${PROJECT_SOURCE_DIR}/resources/scripts/auto-format.sh) +endif() set(STORM_TARGETS "") add_subdirectory(src) @@ -633,11 +597,14 @@ add_subdirectory(src) export_option(STORM_HAVE_XERCES) export_option(STORM_HAVE_SPOT) export_option(STORM_HAVE_GUROBI) +export_option(STORM_HAVE_SOPLEX) +export_option(STORM_HAVE_Z3) include(export) -install(FILES ${CMAKE_BINARY_DIR}/stormConfig.install.cmake DESTINATION ${CMAKE_INSTALL_DIR} RENAME stormConfig.cmake) -install(FILES ${CMAKE_BINARY_DIR}/stormConfigVersion.cmake DESTINATION ${CMAKE_INSTALL_DIR}) -install(EXPORT storm_Targets FILE stormTargets.cmake DESTINATION ${CMAKE_INSTALL_DIR}) +install(DIRECTORY ${STORM_CMAKE_FIND_MODULES} DESTINATION ${STORM_CMAKE_INSTALL_DIR}) +install(FILES ${PROJECT_BINARY_DIR}/stormConfig.cmake.install DESTINATION ${STORM_CMAKE_INSTALL_DIR} RENAME stormConfig.cmake) +install(FILES ${PROJECT_BINARY_DIR}/stormConfigVersion.cmake DESTINATION ${STORM_CMAKE_INSTALL_DIR}) +install(EXPORT storm_Targets FILE stormTargets.cmake DESTINATION ${STORM_CMAKE_INSTALL_DIR}) include(StormCPackConfig.cmake) diff --git a/Dockerfile b/Dockerfile index b08afb16c3..5a968ae5ad 100644 --- a/Dockerfile +++ b/Dockerfile @@ -20,9 +20,10 @@ ARG build_type=Release ARG no_threads=1 # Specify Storm configuration (ON/OFF) -ARG gurobi_support="ON" -ARG soplex_support="ON" -ARG spot_support="ON" +ARG disable_gurobi="OFF" +ARG disable_soplex="OFF" +ARG disable_spot="OFF" +ARG disable_mathsat="OFF" ARG developer="OFF" ARG cln_exact="OFF" ARG cln_ratfunc="ON" @@ -47,9 +48,10 @@ WORKDIR /opt/storm/build # Configure Storm RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type \ -DSTORM_PORTABLE=ON \ - -DSTORM_USE_GUROBI=$gurobi_support \ - -DSTORM_USE_SOPLEX=$soplex_support \ - -DSTORM_USE_SPOT_SYSTEM=$spot_support \ + -DSTORM_DISABLE_GUROBI=$disable_gurobi \ + -DSTORM_DISABLE_MATHSAT=$disable_mathsat \ + -DSTORM_DISABLE_SOPLEX=$disable_spot \ + -DSTORM_DISABLE_SPOT=$disable_spot \ -DSTORM_DEVELOPER=$developer \ -DSTORM_USE_CLN_EA=$cln_exact \ -DSTORM_USE_CLN_RF=$cln_ratfunc \ @@ -65,5 +67,4 @@ RUN make storm -j $no_threads # (This can be skipped or adapted depending on custom needs) RUN make binaries -j $no_threads -# Set path -ENV PATH="/opt/storm/build/bin:$PATH" +WORKDIR /opt/storm diff --git a/StormCPackConfig.cmake b/StormCPackConfig.cmake index ddd227bd21..9612e9750d 100644 --- a/StormCPackConfig.cmake +++ b/StormCPackConfig.cmake @@ -5,7 +5,7 @@ include(InstallRequiredSystemLibraries) ### general settings set(CPACK_PACKAGE_NAME "Storm") -set(CPACK_PACKAGE_VENDOR "RWTH Aachen University") +set(CPACK_PACKAGE_VENDOR "Storm Developers") set(CPACK_PACKAGE_DESCRIPTION_SUMMARY "Storm - A probabilistic model checker written in C++.") set(CPACK_PACKAGE_CONTACT "support@stormchecker.org") diff --git a/doc/update_resources.md b/doc/update_resources.md index 1e1abadf9c..116ce365ed 100644 --- a/doc/update_resources.md +++ b/doc/update_resources.md @@ -17,6 +17,7 @@ In case a new patch needs to be created follow these steps: 6. Resolve issues, make changes, and commit them 7. Create a new patch file via `git format-patch --stdout > eigen.patch`, where `` is the tag, branch or commit from step 5 8. add the patch to resources/patches/ and change the resources/3rdparty/CmakeLists.txt file accordingly. + ## GLPK To update GLPK, download the new sources from [here](https://ftp.gnu.org/gnu/glpk/) and put them into `$STORM_DIR/resources/3rdparty/glpk-5.0`. diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index fade2ede96..83b70785da 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -1,4 +1,8 @@ -add_custom_target(resources) + +if(PROJECT_TOP_LEVEL) + add_custom_target(resources) + add_dependencies(resources storm_resources) +endif() add_custom_target(test-resources) set(STORM_3RDPARTY_SOURCE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty) @@ -14,22 +18,28 @@ message(STATUS "Storm - Building external resources with ${STORM_RESOURCES_BUILD ############################################################# # Do not take a branch, needs internet connection. +message (STATUS "Storm - Including l3pp logging.") ExternalProject_Add( l3pp_ext GIT_REPOSITORY https://github.com/hbruintjes/l3pp.git GIT_TAG e4f8d7fe6c328849aff34d2dfd6fd592c14070d5 - SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/l3pp + SOURCE_DIR ${STORM_3RDPARTY_BINARY_DIR}/l3pp UPDATE_COMMAND "" CONFIGURE_COMMAND "" BUILD_COMMAND "" INSTALL_COMMAND "" LOG_INSTALL ON + LOG_DOWNLOAD ON ) -ExternalProject_Get_Property(l3pp_ext source_dir) -set(l3pp_INCLUDE "${source_dir}/") -add_imported_library_interface(l3pp "${l3pp_INCLUDE}") -list(APPEND STORM_DEP_TARGETS l3pp) +add_library(l3pp INTERFACE) # Not imported, we are in control of the sources. add_dependencies(l3pp l3pp_ext) +target_include_directories(l3pp INTERFACE + $ + $ +) +install(TARGETS l3pp EXPORT storm_Targets) +install(DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/l3pp/ DESTINATION ${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/l3pp FILES_MATCHING PATTERN "*.h" PATTERN ".git" EXCLUDE) +list(APPEND STORM_DEP_TARGETS l3pp) ############################################################# ## @@ -37,7 +47,16 @@ add_dependencies(l3pp l3pp_ext) ## ############################################################# -add_imported_library_interface(gmm "${STORM_3RDPARTY_SOURCE_DIR}/gmm-5.2/include") +message (STATUS "Storm - Including gmm 5.2.") +add_library(gmm INTERFACE) # Not imported, we are in control of the sources. +target_include_directories(gmm INTERFACE + $ + $ +) +install(TARGETS gmm EXPORT storm_Targets) +install(DIRECTORY ${STORM_3RDPARTY_SOURCE_DIR}/gmm-5.2/include/ + DESTINATION ${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/gmm + FILES_MATCHING PATTERN "*.h" PATTERN ".git" EXCLUDE) list(APPEND STORM_DEP_TARGETS gmm) ############################################################# @@ -46,7 +65,7 @@ list(APPEND STORM_DEP_TARGETS gmm) ## ############################################################# -# Checkout Eigen +# Checkout Eigen # We're checking out Eigen using the (currently not officially released) version 3.4.1 # See here https://gitlab.com/libeigen/eigen/-/commit/bae907b8f6078b1df290729eef946360315bd312 # The current official release is 3.4.0 which results in issues, see https://github.com/moves-rwth/storm/issues/162 @@ -55,21 +74,28 @@ ExternalProject_Add( eigen_src GIT_REPOSITORY https://gitlab.com/libeigen/eigen.git GIT_TAG bae907b8f6078b1df290729eef946360315bd312 - SOURCE_DIR ${STORM_3RDPARTY_INCLUDE_DIR}/StormEigen - PREFIX ${STORM_3RDPARTY_BINARY_DIR}/StormEigen-3.4.1alpha + SOURCE_DIR ${STORM_3RDPARTY_BINARY_DIR}/StormEigen # First check whether patch was already applied (--reverse --check), otherwise apply patch PATCH_COMMAND git apply ${STORM_3RDPARTY_SOURCE_DIR}/patches/eigen341alpha.patch --reverse --check || git apply ${STORM_3RDPARTY_SOURCE_DIR}/patches/eigen341alpha.patch UPDATE_COMMAND "" CONFIGURE_COMMAND "" BUILD_COMMAND "" INSTALL_COMMAND "" + LOG_DOWNLOAD ON LOG_INSTALL ON ) -add_imported_library_interface(StormEigen "${STORM_3RDPARTY_INCLUDE_DIR}") -list(APPEND STORM_DEP_TARGETS StormEigen) -add_dependencies(StormEigen eigen_src) - - +add_library(eigen3storm INTERFACE) # Not imported, we are in control of the sources. +add_dependencies(eigen3storm eigen_src) +# note that we include without StormEigen +target_include_directories(eigen3storm INTERFACE + $ + $ +) +install(TARGETS eigen3storm EXPORT storm_Targets) +install(DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/StormEigen/ + DESTINATION ${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/StormEigen + PATTERN ".git" EXCLUDE) +list(APPEND STORM_DEP_TARGETS eigen3storm) ############################################################# ## @@ -78,37 +104,16 @@ add_dependencies(StormEigen eigen_src) ############################################################# # Boost Option variables -set(Boost_USE_STATIC_LIBS ${USE_BOOST_STATIC_LIBRARIES}) -set(Boost_USE_MULTITHREADED ON) -set(Boost_USE_STATIC_RUNTIME OFF) -set(Boost_NO_BOOST_CMAKE ON) - -find_package(Boost 1.65.1 QUIET REQUIRED COMPONENTS filesystem system) -if (NOT Boost_FOUND) - if (Boost_VERSION) - message(FATAL_ERROR "The required Boost version is 1.65.1 or newer, however, only ${Boost_VERSION} was found.") - else () - message(FATAL_ERROR "Boost was not found.") - endif () -endif () -if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL "")) - set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib") -endif () - +set(Boost_NO_WARN_NEW_VERSIONS ON) +find_package(Boost 1.70.0 QUIET REQUIRED NO_MODULE) if (${Boost_VERSION} VERSION_GREATER_EQUAL "1.81.0") message(STATUS "Storm - Using workaround for Boost >= 1.81") - set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DBOOST_PHOENIX_STL_TUPLE_H_") + add_compile_options(-DBOOST_PHOENIX_STL_TUPLE_H_) # or add compile_definitions? + # TODO Only do this for a specific target? endif() -set(CNTVAR 1) -foreach(BOOSTLIB ${Boost_LIBRARIES}) - add_imported_library(target-boost-${CNTVAR} SHARED ${BOOSTLIB} ${Boost_INCLUDE_DIRS}) - list(APPEND STORM_DEP_TARGETS target-boost-${CNTVAR}_SHARED) - MATH(EXPR CNTVAR "${CNTVAR}+1") -endforeach() message(STATUS "Storm - Using boost ${Boost_VERSION} (library version ${Boost_LIB_VERSION}).") -# set the information for the config header -set(STORM_BOOST_INCLUDE_DIR "${Boost_INCLUDE_DIRS}") +list(APPEND STORM_DEP_IMP_TARGETS Boost::boost) ############################################################# ## @@ -118,10 +123,18 @@ set(STORM_BOOST_INCLUDE_DIR "${Boost_INCLUDE_DIRS}") # Use the shipped version of ExprTK message (STATUS "Storm - Including ExprTk.") -add_imported_library_interface(ExprTk "${STORM_3RDPARTY_SOURCE_DIR}/exprtk") -list(APPEND STORM_DEP_TARGETS ExprTk) - - +set(exprTk_SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/exprtk) +set(exprTk_INSTALL_DIR ${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/exprtk) +add_library(exprTk INTERFACE) # Not imported, we are in control of the sources. +target_include_directories(exprTk INTERFACE + $ + $ +) +install(TARGETS exprTk EXPORT storm_Targets) +install(DIRECTORY ${exprTk_SOURCE_DIR} + DESTINATION ${exprTk_INSTALL_DIR} + FILES_MATCHING PATTERN "*.hpp" PATTERN ".git" EXCLUDE) +list(APPEND STORM_DEP_TARGETS exprTk) ############################################################# ## @@ -131,24 +144,17 @@ list(APPEND STORM_DEP_TARGETS ExprTk) # Use the shipped version of Parallel Hashmap message (STATUS "Storm - Including Parallel Hashmap.") -set(PHMAP_INCLUDE_DIR "${STORM_3RDPARTY_SOURCE_DIR}/parallel_hashmap/parallel_hashmap") -file(GLOB PHMAP_HEADERS "${PHMAP_INCLUDE_DIR}/*.h") - -# Add the parallel_hashmap headers to the headers that are copied to the include directory in the build directory. -set(PHMAP_BINDIR_DIR ${STORM_3RDPARTY_INCLUDE_DIR}/parallel_hashmap) -include_directories("${PHMAP_BINDIR_DIR}") -foreach(HEADER ${PHMAP_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${PHMAP_BINDIR_DIR}/parallel_hashmap/${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${PHMAP_BINDIR_DIR}/parallel_hashmap - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${PHMAP_BINDIR_DIR}/parallel_hashmap/${HEADER_FILENAME} - DEPENDS ${PHMAP_INCLUDE_DIR}/${HEADER_FILENAME} - ) - list(APPEND PHMAP_BINDIR_HEADERS ${PHMAP_BINDIR_DIR}/parallel_hashmap/${HEADER_FILENAME}) -endforeach() +set(phmap_SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/parallel_hashmap) +set(phmap_INSTALL_DIR ${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/parallel_hashmap) +add_library(phmap INTERFACE) # Not imported, we are in control of the sources. +target_include_directories(phmap INTERFACE + $ + $) +install(TARGETS phmap EXPORT storm_Targets) +install(DIRECTORY ${phmap_SOURCE_DIR} + DESTINATION ${phmap_INSTALL_DIR} + FILES_MATCHING PATTERN "*.h" PATTERN ".git" EXCLUDE) +list(APPEND STORM_DEP_TARGETS phmap) ############################################################# ## @@ -158,7 +164,17 @@ endforeach() # Use the shipped version of cpphoafparser message (STATUS "Storm - Including cpphoafparser 0.99.2") -include_directories("${STORM_3RDPARTY_SOURCE_DIR}/cpphoafparser-0.99.2/include") +set(cppHOAparser_SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/cpphoafparser-0.99.2/include) +set(cppHOAparser_INSTALL_DIR ${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/cpphoafparser-0.99.2/) +add_library(cppHOAparser INTERFACE) # Not imported, we are in control of the sources. +target_include_directories(cppHOAparser INTERFACE + $ + $) +install(TARGETS cppHOAparser EXPORT storm_Targets) +install(DIRECTORY ${cppHOAparser_SOURCE_DIR} + DESTINATION ${cppHOAparser_INSTALL_DIR} + FILES_MATCHING PATTERN "*.h" PATTERN ".git" EXCLUDE) +list(APPEND STORM_DEP_TARGETS cppHOAparser) ############################################################# ## @@ -168,7 +184,16 @@ include_directories("${STORM_3RDPARTY_SOURCE_DIR}/cpphoafparser-0.99.2/include") #use the shipped version of modernjson message (STATUS "Storm - Including ModernJSON.") -add_imported_library_interface(ModernJSON "${STORM_3RDPARTY_SOURCE_DIR}/modernjson/include/") +set(ModernJSON_SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/modernjson/include/) +set(ModernJSON_INSTALL_DIR ${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/modernjson/) +add_library(ModernJSON INTERFACE) # Not imported, we are in control of the sources. +target_include_directories(ModernJSON INTERFACE + $ + $) +install(TARGETS ModernJSON EXPORT storm_Targets) +install(DIRECTORY ${ModernJSON_SOURCE_DIR} + DESTINATION ${ModernJSON_INSTALL_DIR} + FILES_MATCHING PATTERN "*.hpp" PATTERN ".git" EXCLUDE) list(APPEND STORM_DEP_TARGETS ModernJSON) ############################################################# @@ -177,31 +202,14 @@ list(APPEND STORM_DEP_TARGETS ModernJSON) ## ############################################################# -find_package(Z3 QUIET) +if(NOT STORM_DISABLE_Z3) + find_package(Z3 QUIET 4.8.7 NO_MODULE) + # Notice that such old z3 versions do not provide config files, so we could bump this version ahead. + if(TARGET z3::libz3) + set(STORM_HAVE_Z3 ON) + set(STORM_Z3_CONFIG ON) # For the config file, did we include z3 via a config (yes) -# Z3 Defines -set(STORM_HAVE_Z3 ${Z3_FOUND}) - -if(Z3_FOUND) - if(NOT EXISTS "${Z3_INCLUDE_DIR}/z3_version.h") - message(FATAL_ERROR "No file z3_version.h found in ${Z3_INCLUDE_DIR}.") - endif() - - # Parse z3 version from version file - file(STRINGS ${Z3_INCLUDE_DIR}/z3_version.h Z3_VERSION_MAJOR REGEX "^#define[\t ]+Z3_MAJOR_VERSION .*") - file(STRINGS ${Z3_INCLUDE_DIR}/z3_version.h Z3_VERSION_MINOR REGEX "^#define[\t ]+Z3_MINOR_VERSION .*") - file(STRINGS ${Z3_INCLUDE_DIR}/z3_version.h Z3_VERSION_PATCH REGEX "^#define[\t ]+Z3_BUILD_NUMBER .*") - string(REGEX MATCH "[0-9]+$" Z3_VERSION_MAJOR "${Z3_VERSION_MAJOR}") - string(REGEX MATCH "[0-9]+$" Z3_VERSION_MINOR "${Z3_VERSION_MINOR}") - string(REGEX MATCH "[0-9]+$" Z3_VERSION_PATCH "${Z3_VERSION_PATCH}") - set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}") - - if(Z3_VERSION) - # Split Z3 version into its components - string(REPLACE "." ";" Z3_VERSION_LIST ${Z3_VERSION}) - list(GET Z3_VERSION_LIST 0 STORM_Z3_VERSION_MAJOR) - list(GET Z3_VERSION_LIST 1 STORM_Z3_VERSION_MINOR) - list(GET Z3_VERSION_LIST 2 STORM_Z3_VERSION_PATCH) + set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}") if ("${Z3_VERSION}" VERSION_EQUAL "4.10.1") message (WARNING "Storm cannot be linked against Z3 version 4.10.1, see issue 252.") @@ -209,28 +217,50 @@ if(Z3_FOUND) set(Z3_FOUND FALSE) else() # Check whether the version of z3 supports optimization - if(NOT "${Z3_VERSION}" VERSION_LESS "4.5.0") - set(STORM_HAVE_Z3_OPTIMIZE ON) - message (STATUS "Storm - Linking with Z3 (version ${Z3_VERSION}). (Z3 version supports optimization)") + message (STATUS "Storm - Linking with Z3 (version ${Z3_VERSION}). (Z3 version supports optimization)") + list(APPEND STORM_DEP_IMP_TARGETS z3::libz3) + endif() + else() + # Debian and Ubuntu packages are as of Debian 14 and Ubuntu 24.04 very old, + # such that no Cmake config files are provided. For the time being, we use a FindZ3.cmake script. + find_package(Z3 QUIET 4.8.7) + + if (Z3_FOUND) + + set(STORM_HAVE_Z3 ON) + set(STORM_Z3_CONFIG OFF) # For the config file, did we include z3 via a config (no) + + if ("${Z3_VERSION}" VERSION_EQUAL "4.10.1") + message (WARNING "Storm cannot be linked against Z3 version 4.10.1, see issue 252.") + message(WARNING "Storm - Could not link with z3. Building of Prism/JANI models will not be supported.") + set(Z3_FOUND FALSE) else() - message (STATUS "Storm - Linking with Z3 (version ${Z3_VERSION}). (Z3 version does not support optimization)") - endif() - if (NOT "${Z3_VERSION}" VERSION_LESS "4.7.1") - set(STORM_Z3_API_USES_STANDARD_INTEGERS ON) - endif() + # Check whether the version of z3 supports optimization + message (STATUS "Storm - Linking with Z3 (version ${Z3_VERSION}). (Z3 version supports optimization)") - add_imported_library(Z3 SHARED ${Z3_LIBRARIES} ${Z3_INCLUDE_DIRS}) - list(APPEND STORM_DEP_TARGETS Z3_SHARED) + add_library(z3 SHARED IMPORTED) + set_target_properties( + z3 + PROPERTIES + IMPORTED_LOCATION ${Z3_LIBRARIES} + INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR} + ) + list(APPEND STORM_DEP_IMP_TARGETS z3) + endif() + else() + message (WARNING "Storm - Z3 not found. Building of Prism/JANI models will not be supported.") endif() - else() - message(WARNING "Storm - Could not obtain Z3 version. Building of Prism/JANI models will not be supported.") - set(Z3_FOUND FALSE) endif() - else() - message (WARNING "Storm - Z3 not found. Building of Prism/JANI models will not be supported.") -endif(Z3_FOUND) + message (WARNING "Storm - Z3 not linked. Building of Prism/JANI models will not be supported.") +endif() +if (Z3_FOUND) + # TODO We may remove STORM_HAVE_Z3_OPTIMIZE checks + # TODO We may remove STORM_Z3_API_USES_STANDARD_INTEGERS checks + set(STORM_Z3_API_USES_STANDARD_INTEGERS ON) + set(STORM_HAVE_Z3_OPTIMIZE ON) +endif() ############################################################# ## @@ -246,23 +276,30 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_glpk.cmake) ## ############################################################# -if (STORM_USE_GUROBI) - find_package(GUROBI QUIET REQUIRED) - set(STORM_HAVE_GUROBI ${GUROBI_FOUND}) - if (GUROBI_FOUND) - if (EXISTS ${GUROBI_LIBRARY}) +if(NOT STORM_DISABLE_GUROBI) + find_package(GUROBI QUIET) + if(GUROBI_FOUND) + set(STORM_HAVE_GUROBI ${GUROBI_FOUND}) + if (EXISTS ${GUROBI_LIBRARY}) message (STATUS "Storm - Linking with Gurobi (${GUROBI_CXX_LIBRARY}).") - add_imported_library(GUROBI SHARED ${GUROBI_LIBRARY} ${GUROBI_INCLUDE_DIRS}) - list(APPEND STORM_DEP_TARGETS GUROBI_SHARED) + add_library(GUROBI UNKNOWN IMPORTED) + set_target_properties( + GUROBI + PROPERTIES + IMPORTED_LOCATION ${GUROBI_LIBRARY} + INTERFACE_INCLUDE_DIRECTORIES ${GUROBI_INCLUDE_DIRS} + ) + list(APPEND STORM_DEP_IMP_TARGETS GUROBI) else() # The FindGurobi.cmake script needs to be updated every now and then as the library file contains the version number... - message(FATAL_ERROR "Gurobi Library ${GUROBI_LIBRARY} not found. If your Gurobi Version is higher then 9.0.0, please contact the Storm developers.") + message(FATAL_ERROR "Gurobi Library ${GUROBI_LIBRARY} not found. If your Gurobi Version is higher then 11.0.0, please contact the Storm developers.") endif() else() - # The FindGurobi.cmake script needs to be updated every now and then as the library file contains the version number ... - message(FATAL_ERROR "Gurobi Library requested but was not found. Make sure that GUROBI_ROOT points to the correct directory (containing include/ and lib/ subdirectories). If your Gurobi Version is higher then 9.0.0, please contact the Storm developers.") + message (STATUS "Storm - Not linking with Gurobi. ") + set(STORM_HAVE_GUROBI OFF) endif() else() + message (STATUS "Storm - Not linking with Gurobi. ") set(STORM_HAVE_GUROBI OFF) endif() @@ -276,223 +313,97 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake) ############################################################# ## -## carl +## carl (including cln and ginac) ## ############################################################# - -set(STORM_HAVE_CARL OFF) -set(CARL_MINVERSION "14.26") -set(CARL_C14VERSION "14") -if (NOT STORM_FORCE_SHIPPED_CARL) - if (NOT "${STORM_CARL_DIR_HINT}" STREQUAL "") - find_package(carl QUIET PATHS ${STORM_CARL_DIR_HINT} NO_DEFAULT_PATH) - endif() - if (NOT carl_FOUND) - find_package(carl QUIET) - endif() -endif() - -set(STORM_SHIPPED_CARL OFF) -if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL) - get_target_property(carlLOCATION lib_carl LOCATION) - if("${carlLOCATION}" STREQUAL "carlLOCATION-NOTFOUND") - if(EXISTS ${STORM_3RDPARTY_BINARY_DIR}/carl) - message(WARNING "Storm - Library for carl location is not found but the directory ${STORM_3RDPARTY_BINARY_DIR}/carl exists. Will (re-)try to build a shipped version of carl.") - set(STORM_SHIPPED_CARL ON) - else() - message(FATAL_ERROR "Library location for carl is not found, did you build carl?") - endif() - elseif(EXISTS ${carlLOCATION}) - #empty on purpose - else() - if(EXISTS ${STORM_3RDPARTY_BINARY_DIR}/carl) - message(WARNING "Storm - File ${carlLOCATION} does not exist but the directory ${STORM_3RDPARTY_BINARY_DIR}/carl exists. Will (re-)try to build a shipped version of carl.") - set(STORM_SHIPPED_CARL ON) - else() - message(FATAL_ERROR "File ${carlLOCATION} does not exist, did you build carl?") - endif() - endif() - if("${carl_VERSION_MAJOR}" STREQUAL "${CARL_C14VERSION}") - message(STATUS "Storm - Found carl-storm version") - # empty on purpose. Maybe put a warning here? - if("${carl_VERSION_MAJOR}.${carl_VERSION_MINOR}" VERSION_LESS "${CARL_MINVERSION}") - message(FATAL_ERROR "Carl version outdated. We require ${CARL_MINVERSION}. Found ${carl_VERSION_MAJOR}.${carl_VERSION_MINOR} at ${carlLOCATION}") - endif() - else() - message(FATAL_ERROR "We only support a diverged version of carl, indicated by Carl version 14.x. These versions can be found at https://github.com/moves-rwth/carl-storm. - On this system, we found ${carl_VERSION_MAJOR}.${carl_VERSION_MINOR} at ${carlLOCATION}") - endif() - - set(STORM_HAVE_CARL ON) - message(STATUS "Storm - Use system version of carl.") - message(STATUS "Storm - Linking with preinstalled carl ${carl_VERSION} (include: ${carl_INCLUDE_DIR}, library ${carl_LIBRARIES}, CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}).") - set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS}) - set(STORM_HAVE_GINAC ${CARL_USE_GINAC}) +# Set compile flags for dependencies +if(STORM_USE_CLN_EA OR STORM_USE_CLN_RF) + set(SHIPPED_CARL_USE_CLN_NUMBERS ON) + set(SHIPPED_CARL_USE_GINAC ON) else() - set(STORM_SHIPPED_CARL ON) -endif() - -if (STORM_SHIPPED_CARL) - # The first external project will be built at *configure stage* - message(STATUS "Carl - Start of config process") - file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) - execute_process( - COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" "-DUse_CLN_NUMBERS=${SHIPPED_CARL_USE_CLN_NUMBERS}" "-DUse_GINAC=${SHIPPED_CARL_USE_GINAC}" - WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download - OUTPUT_VARIABLE carlconfig_out - RESULT_VARIABLE carlconfig_result) - - if(NOT carlconfig_result) - message(STATUS "${carlconfig_out}") - endif() - execute_process( - COMMAND ${CMAKE_COMMAND} --build . --target carl-config - WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download - OUTPUT_VARIABLE carlconfig_out - RESULT_VARIABLE carlconfig_result - ) - if(NOT carlconfig_result) - message(STATUS "${carlconfig_out}") - endif() - message(STATUS "Carl - End of config process") - - message(STATUS "Storm - Using shipped version of carl.") - ExternalProject_Add( - carl - SOURCE_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl - CONFIGURE_COMMAND "" - BUILD_IN_SOURCE 1 - BUILD_COMMAND make lib_carl -j${STORM_RESOURCES_BUILD_JOBCOUNT} - INSTALL_COMMAND make install -j${STORM_RESOURCES_BUILD_JOBCOUNT} - LOG_BUILD ON - LOG_INSTALL ON - BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT} - ) - include(${STORM_3RDPARTY_BINARY_DIR}/carl/carlConfig.cmake) - - set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS}) - set(STORM_HAVE_GINAC ${CARL_USE_GINAC}) - - add_dependencies(resources carl) - set(carl_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/carl/include/") - set(carl_DIR "${STORM_3RDPARTY_BINARY_DIR}/carl/") - set(carl_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}) - set(STORM_HAVE_CARL ON) - - message(STATUS "Storm - Linking with shipped carl ${carl_VERSION} (include: ${carl_INCLUDE_DIR}, library ${carl_LIBRARIES}, CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}).") - - # install the carl dynamic library if we built it - if(MACOSX) - install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl.${carl_VERSION}${DYNAMIC_EXT} DESTINATION lib) - else() - install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}.${carl_VERSION} DESTINATION lib) - endif() + set(SHIPPED_CARL_USE_CLN_NUMBERS OFF) + set(SHIPPED_CARL_USE_GINAC OFF) endif() -if("${carl_VERSION_MAJOR}.${carl_VERSION_MINOR}" VERSION_EQUAL "14.22") - # This version is too old for forward declarations and updating requires moving the git, - # so we warn users but start warning them now. - set(STORM_CARL_SUPPORTS_FWD_DECL OFF) - message(WARNING "Uses an outdated repo for Carl. Carl is now hosted at https://github.com/moves-rwth/carl-storm") -elseif("${carl_VERSION_MAJOR}.${carl_VERSION_MINOR}" VERSION_EQUAL "14.23") - # This version is too old for forward declarations, but we keep supporting it for the moment. - set(STORM_CARL_SUPPORTS_FWD_DECL OFF) -else() - set(STORM_CARL_SUPPORTS_FWD_DECL ON) -endif() +set(STORM_HAVE_CARL OFF) +set(CARL_MINVERSION "14.28") +set(CARL_C14VERSION "14") +include(FetchContent) +FETCHCONTENT_DECLARE( + carl + GIT_REPOSITORY ${STORM_CARL_GIT_REPO} + GIT_TAG ${STORM_CARL_GIT_TAG} +) +SET(EXCLUDE_TESTS_FROM_ALL ON) #carl without tests +SET(THREAD_SAFE ON) #carl thread safe code +SET(USE_CLN_NUMBERS ${SHIPPED_CARL_USE_CLN_NUMBERS}) +SET(USE_GINAC ${SHIPPED_CARL_USE_CLN_NUMBERS}) +SET(CARL_LIB_INSTALL_DIR "lib/storm") +SET(CARL_INCLUDE_INSTALL_DIR "include/storm") # maybe use resources folder /carl instead for consistency? +SET(CARL_EXPORT_TO_CMAKE OFF) +SET(CARL_CMAKE_INSTALL_DIR "lib/cmake/storm") +FETCHCONTENT_MAKEAVAILABLE(carl) +include(${carl_BINARY_DIR}/carlConfig.cmake) +# Read variables from this config. +set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS}) +set(STORM_HAVE_GINAC ${CARL_USE_GINAC}) +message(STATUS "storm -- using carl version ${carl_VERSION} (cln: ${STORM_HAVE_CLN}, ginac: ${STORM_HAVE_GINAC})") +# +add_dependencies(storm_resources lib_carl) +# TODO this old flag is no longer really relevant as CARL must always be present. +set(STORM_HAVE_CARL ON) +# This flag is currently required to pick the right carl adapter. +# TODO It can be removed as the old versions that did not support forward declarations are no longer supported either way. +set(STORM_CARL_SUPPORTS_FWD_DECL ON) +list(APPEND STORM_FETCHED_TARGETS lib_carl) + +# Some checks to see whether we correctly configured carl. if(STORM_USE_CLN_RF AND NOT STORM_HAVE_CLN) - message(FATAL_ERROR "Cannot use CLN numbers if carl is build without.") + message(FATAL_ERROR "Cannot use CLN numbers if carl is build without.") endif() if(STORM_USE_CLN_RF AND NOT STORM_HAVE_GINAC) message(FATAL_ERROR "Cannot use CLN numbers if carl is build without ginac.") endif() -# The library that needs symbols must be first, then the library that resolves the symbol. -list(APPEND STORM_DEP_IMP_TARGETS lib_carl) -if(STORM_USE_CLN_EA OR STORM_USE_CLN_RF) - list(APPEND STORM_DEP_IMP_TARGETS GINAC_SHARED CLN_SHARED) -endif() -list(APPEND STORM_DEP_IMP_TARGETS GMPXX_SHARED GMP_SHARED) - - -############################################################# -## -## SMT-RAT -## -############################################################# - -set(STORM_HAVE_SMTRAT OFF) -if(USE_SMTRAT) - find_package(smtrat QUIET REQUIRED) - if(smtrat_FOUND) - set(STORM_HAVE_SMTRAT ON) - message(STATUS "Storm - Linking with smtrat.") - include_directories("${smtrat_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES ${smtrat_LIBRARIES}) - else() - message(FATAL_ERROR "Storm - SMT-RAT was requested but not found") - endif() -endif() - - -############################################################# -## -## gmp -## -############################################################# - -get_target_property(GMPXX_LIB GMPXX_SHARED IMPORTED_LIB_LOCATION) -get_target_property(GMP_LIB GMP_SHARED IMPORTED_LIB_LOCATION) -get_target_property(GMPXX_INCLUDE_DIR GMPXX_SHARED INTERFACE_INCLUDE_DIRECTORIES) -get_target_property(GMP_INCLUDE_DIR GMP_SHARED INTERFACE_INCLUDE_DIRECTORIES) -get_filename_component(GMP_LIB_LOCATION ${GMP_LIB} DIRECTORY) -get_filename_component(GMPXX_LIB_LOCATION ${GMPXX_LIB} DIRECTORY) - - -############################################################# -## -## cln -## -############################################################# - -if(STORM_HAVE_CLN) - get_target_property(CLN_INCLUDE_DIR CLN_SHARED INTERFACE_INCLUDE_DIRECTORIES) -endif() - ############################################################# ## ## MathSAT (optional) ## ############################################################# - -if ("${MSAT_ROOT}" STREQUAL "") - set(ENABLE_MSAT OFF) +if(NOT STORM_DISABLE_MATHSAT) + find_package(MATHSAT QUIET) + if(MATHSAT_FOUND) + set(STORM_HAVE_MATHSAT ON) + add_library(mathsat SHARED IMPORTED) + set_target_properties( + mathsat + PROPERTIES + IMPORTED_LOCATION ${MATHSAT_LIBRARIES} + INTERFACE_INCLUDE_DIRECTORIES ${MATHSAT_INCLUDE_DIRS} + ) + list(APPEND STORM_DEP_IMP_TARGETS mathsat) + message(STATUS "Storm - Linking with MathSAT: (library: ${mathsat_}; include: ${MATHSAT_INCLUDE_DIRS})") + else() + set(STORM_HAVE_MATHSAT OFF) + if(MATHSAT_ROOT STREQUAL "") + message(STATUS "Storm - MathSAT not found.") + else() + message(WARNING "Storm - MathSAT not found, even though MATHSAT_ROOT is set.") + endif() + endif() else() - set(ENABLE_MSAT ON) + set(STORM_HAVE_MATHSAT OFF) + message(STATUS "Storm - Not linking with MathSat.") endif() -# MathSAT Defines -set(STORM_HAVE_MSAT ${ENABLE_MSAT}) -if (ENABLE_MSAT) - message (STATUS "Storm - Linking with MathSAT.") - if(${OPERATING_SYSTEM} MATCHES "Linux") - find_library(MSAT_LIB mathsat PATHS "${MSAT_ROOT}/lib") - add_imported_library(msat SHARED ${MSAT_LIB} "${MSAT_ROOT}/include") - list(APPEND STORM_DEP_TARGETS msat_SHARED) - else() - # on macOS, the .dylib file has some hard coded path (Version 5.5.4). - # we thus link statically - find_library(MSAT_LIB NAMES libmathsat${STATIC_EXT} mathsat PATHS "${MSAT_ROOT}/lib") - add_imported_library(msat STATIC ${MSAT_LIB} "${MSAT_ROOT}/include") - list(APPEND STORM_DEP_TARGETS msat_STATIC) - endif() -endif(ENABLE_MSAT) + ############################################################# ## ## QVBS (Quantitative verification benchmark set) ## +## TODO: Consider installing these files as well? ############################################################# set(STORM_HAVE_QVBS OFF) @@ -508,7 +419,7 @@ if (STORM_LOAD_QVBS) INSTALL_COMMAND "" LOG_INSTALL ON ) - add_dependencies(resources download_qvbs) + add_dependencies(storm_resources download_qvbs) set(STORM_HAVE_QVBS ON) ExternalProject_Get_Property(download_qvbs source_dir) set(STORM_QVBS_ROOT "${source_dir}/benchmarks") @@ -554,59 +465,33 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_spot.cmake) ## ############################################################# -if(STORM_SHIPPED_CARL) - set(sylvan_dep carl) -else() - set(sylvan_dep lib_carl) -endif() - -if (STORM_DEBUG_SYLVAN) - set(SYLVAN_BUILD_TYPE "Debug") - message(WARNING "Storm - Building Sylvan in DEBUG mode.") -else() - set(SYLVAN_BUILD_TYPE "Release") -endif() - -ExternalProject_Add( - sylvan - DOWNLOAD_COMMAND "" - PREFIX "sylvan" +FETCHCONTENT_DECLARE( + sylvanfetch SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan - CMAKE_ARGS -DPROJECT_NAME=storm -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DSYLVAN_BUILD_TESTS=OFF -DCMAKE_BUILD_TYPE=${SYLVAN_BUILD_TYPE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DSYLVAN_GMP=ON -DUSE_CARL=ON -Dcarl_DIR=${carl_DIR} -DBUILD_SHARED_LIBS=OFF - BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan - BUILD_IN_SOURCE 0 - INSTALL_COMMAND "" - INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan - LOG_CONFIGURE ON - LOG_BUILD ON - DEPENDS ${sylvan_dep} - BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT} - BUILD_ALWAYS 1 ) -# BUILD ALWAYS ON due to: https://stackoverflow.com/questions/46708124/cmake-doesnt-rebuild-externalproject-on-changes +SET(SYLVAN_GMP ON) +SET(USE_CARL ON) +SET(SYLVAN_INSTALL_BINDIR ${STORM_RESOURCE_BIN_INSTALL_DIR}/sylvan) +SET(SYLVAN_INSTALL_LIBDIR ${STORM_RESOURCE_LIBRARY_INSTALL_DIR}/sylvan) +SET(SYLVAN_INSTALL_INCLUDEDIR ${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/sylvan) +SET(CMAKE_POSITION_INDEPENDENT_CODE ON) # Likely only necessary on linux +SET(STORM_SOURCE_DIR "${PROJECT_SOURCE_DIR}/src/") # TODO this is ugly. +SET(STORM_BINARY_INCLUDE_DIR "${PROJECT_BINARY_DIR}/include/") #TODO this is ugly. +FETCHCONTENT_MAKEAVAILABLE(sylvanfetch) -ExternalProject_Get_Property(sylvan source_dir) -ExternalProject_Get_Property(sylvan binary_dir) -set(sylvan_INCLUDE_DIR "${source_dir}/src") -set(sylvan_LIBRARY "${binary_dir}/src/libsylvan${STATIC_EXT}") -message(STATUS "Storm - Using shipped version of sylvan.") -message(STATUS "Storm - Linking with sylvan.") -add_imported_library(sylvan STATIC ${sylvan_LIBRARY} ${sylvan_INCLUDE_DIR}) -add_dependencies(sylvan_STATIC sylvan) +# TODO We previously had -DSYLVAN_GMP=ON. Why? -list(APPEND STORM_DEP_TARGETS sylvan_STATIC) +list(APPEND STORM_FETCHED_TARGETS sylvan) ############################################################# ## ## Google Test gtest ## ############################################################# +## This is still old cmake, but as it is not installed, it is not as relevant. set(GOOGLETEST_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/googletest) ExternalProject_Add( googletest - #For downloads (may be useful later!) - #SVN_REPOSITORY http://googletest.googlecode.com/svn/trunk/ - #TIMEOUT 10 DOWNLOAD_COMMAND "" SOURCE_DIR "${STORM_3RDPARTY_SOURCE_DIR}/googletest" # Force the same output paths for debug and release builds so that @@ -633,69 +518,14 @@ set(GTEST_LIBRARIES ${binary_dir}/lib/libgtest${STATIC_EXT} ${binary_dir}/lib/li add_dependencies(test-resources googletest) list(APPEND STORM_TEST_LINK_LIBRARIES ${GTEST_LIBRARIES}) -############################################################# -## -## Intel Threading Building Blocks (optional) -## -############################################################# - -set(STORM_HAVE_INTELTBB OFF) -if (STORM_USE_INTELTBB) - find_package(TBB QUIET REQUIRED) - - if (TBB_FOUND) - message(STATUS "Storm - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.") - message(STATUS "Storm - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.") - set(STORM_HAVE_INTELTBB ON) - # Under Linux libtbb.so contains a linker script to libtbb.so.2 instead of a symlink. - # This breaks CMake. - # As a workaround we manually try to add the necessary suffix ".2" to the so file and hope for the best. - if (LINUX) - # Check if the library is a linker script which only links to the correct library - # Read first bytes of file - file(READ "${TBB_LIBRARY}" TMPTXT LIMIT 128) - # Check if file starts with "INPUT (libtbb.so.2)" - if("${TMPTXT}" MATCHES "INPUT \\(libtbb\\.so\\.(.*)\\)") - # Manually set library by adding the suffix from the linker script. - # CMAKE_MATCH_1 contains the parsed suffix. - set(TBB_LIB_LINUX "${TBB_LIBRARY}.${CMAKE_MATCH_1}") - set(TBB_MALLOC_LIB_LINUX "${TBB_MALLOC_LIBRARY}.${CMAKE_MATCH_1}") - if (EXISTS "${TBB_LIB_LINUX}") - set(TBB_LIBRARY ${TBB_LIB_LINUX}) - message(STATUS "Storm - Using Intel TBB library in manually set path ${TBB_LIBRARY}.") - endif() - if (EXISTS "${TBB_MALLOC_LIB_LINUX}") - set(TBB_MALLOC_LIBRARY ${TBB_MALLOC_LIB_LINUX}) - message(STATUS "Storm - Using Intel TBB malloc library in manually set path ${TBB_MALLOC_LIBRARY}.") - endif() - endif() - endif() - - add_imported_library(tbb SHARED ${TBB_LIBRARY} ${TBB_INCLUDE_DIRS}) - list(APPEND STORM_DEP_TARGETS tbb_SHARED) - add_imported_library(tbb_malloc SHARED ${TBB_MALLOC_LIBRARY} ${TBB_INCLUDE_DIRS}) - list(APPEND STORM_DEP_TARGETS tbb_malloc_SHARED) - - else(TBB_FOUND) - message(FATAL_ERROR "Storm - TBB was requested, but not found.") - endif(TBB_FOUND) -endif(STORM_USE_INTELTBB) - ############################################################# ## ## Threads ## ############################################################# -find_package(Threads QUIET REQUIRED) -if (NOT Threads_FOUND) - message(FATAL_ERROR "Storm - Threads was requested, but not found.") -endif() -include_directories(${THREADS_INCLUDE_DIRS}) -list(APPEND STORM_LINK_LIBRARIES ${CMAKE_THREAD_LIBS_INIT}) -if (STORM_USE_COTIRE) - target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT}) -endif(STORM_USE_COTIRE) - +set(CMAKE_THREAD_PREFER_PTHREAD TRUE) +set(THREADS_PREFER_PTHREAD_FLAG TRUE) +find_package(Threads REQUIRED) +list(APPEND STORM_DEP_IMP_TARGETS Threads::Threads) -add_custom_target(copy_resources_headers DEPENDS ${PHMAP_BINDIR_HEADERS}) diff --git a/resources/3rdparty/carl/CMakeLists.txt b/resources/3rdparty/carl/CMakeLists.txt deleted file mode 100644 index 398a31ed23..0000000000 --- a/resources/3rdparty/carl/CMakeLists.txt +++ /dev/null @@ -1,25 +0,0 @@ -project(carlext) -cmake_minimum_required(VERSION 3.3) -include(ExternalProject) - -option(STORM_3RDPARTY_BINARY_DIR "3rd party bin dir") - -message(STATUS "Carl-Storm - Storm 3rdparty binary dir: ${STORM_3RDPARTY_BINARY_DIR}") - -ExternalProject_Add(carl-config - GIT_REPOSITORY https://github.com/moves-rwth/carl-storm - GIT_TAG master - PREFIX here - SOURCE_DIR source_dir - BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl - CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DBOOST_INCLUDEDIR=${Boost_INCLUDE_DIRS} -DBOOST_LIBRARYDIR=${Boost_LIBRARY_DIRS} -DBoost_NO_SYSTEM_PATHS=ON -DEXPORT_TO_CMAKE=ON -DTHREAD_SAFE=ON -DUSE_CLN_NUMBERS=${Use_CLN_NUMBERS} -DUSE_GINAC=${Use_GINAC} -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=ON -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl - BUILD_IN_SOURCE 0 - LOG_UPDATE OFF - LOG_CONFIGURE OFF - BUILD_COMMAND "" # Disable build step. - INSTALL_COMMAND "" # Disable install step too. -) -add_custom_target(build-carl) -add_dependencies(build-carl carl-config) - -message(STATUS "Carl-Storm - Finished configuration.") diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake index 10b6a18a30..d9c21c1b66 100644 --- a/resources/3rdparty/include_cudd.cmake +++ b/resources/3rdparty/include_cudd.cmake @@ -43,14 +43,14 @@ if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang") endif() endif() - +# to also create shared library, do --enable-shared ExternalProject_Add( - cudd3 + cudd3_src DOWNLOAD_COMMAND "" SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0 PREFIX ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 PATCH_COMMAND ${CMAKE_COMMAND} -E env ${CUDD_AUTOTOOLS_LOCATIONS} ${AUTORECONF} - CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --with-pic=yes --prefix=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 --libdir=${CUDD_LIB_DIR} CC=${CMAKE_C_COMPILER} CXX=${CUDD_CXX_COMPILER} ${CUDD_INCLUDE_FLAGS} + CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0/configure --enable-obj --with-pic=yes --prefix=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 --libdir=${CUDD_LIB_DIR} CC=${CMAKE_C_COMPILER} CXX=${CUDD_CXX_COMPILER} ${CUDD_INCLUDE_FLAGS} # Multi-threaded compilation could lead to compile issues BUILD_COMMAND make -j1 ${STORM_CUDD_FLAGS} ${CUDD_AUTOTOOLS_LOCATIONS} INSTALL_COMMAND make install -j1 ${CUDD_AUTOTOOLS_LOCATIONS} @@ -58,24 +58,31 @@ ExternalProject_Add( LOG_CONFIGURE ON LOG_BUILD ON LOG_INSTALL ON - BUILD_BYPRODUCTS ${CUDD_LIB_DIR}/libcudd${DYNAMIC_EXT} ${CUDD_LIB_DIR}/libcudd${STATIC_EXT} + BUILD_BYPRODUCTS ${CUDD_LIB_DIR}/libcudd${STATIC_EXT} + LOG_OUTPUT_ON_FAILURE ON ) # Do not use system CUDD, StoRM has a modified version set(CUDD_INCLUDE_DIR ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/include) -set(CUDD_SHARED_LIBRARY ${CUDD_LIB_DIR}/libcudd${DYNAMIC_EXT}) set(CUDD_STATIC_LIBRARY ${CUDD_LIB_DIR}/libcudd${STATIC_EXT}) set(CUDD_VERSION_STRING 3.0.0) +set(CUDD_INSTALL_DIR ${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/cudd/) -add_imported_library(cudd SHARED ${CUDD_SHARED_LIBRARY} ${CUDD_INCLUDE_DIR}) -add_imported_library(cudd STATIC ${CUDD_STATIC_LIBRARY} ${CUDD_INCLUDE_DIR}) -add_dependencies(resources cudd3) +file(MAKE_DIRECTORY ${CUDD_INCLUDE_DIR}) # Workaround https://gitlab.kitware.com/cmake/cmake/-/issues/15052 +add_library(cudd3 STATIC IMPORTED) +set_target_properties( + cudd3 + PROPERTIES + IMPORTED_LOCATION ${CUDD_STATIC_LIBRARY} + INTERFACE_INCLUDE_DIRECTORIES ${CUDD_INCLUDE_DIR} +) +install(FILES ${CUDD_STATIC_LIBRARY} DESTINATION ${STORM_RESOURCE_LIBRARY_INSTALL_DIR}) +install(DIRECTORY ${CUDD_INCLUDE_DIR}/ DESTINATION ${CUDD_INSTALL_DIR} + FILES_MATCHING PATTERN "*.h" PATTERN "*.hh" PATTERN ".git" EXCLUDE) -if(BUILD_SHARED_LIBS) - list(APPEND STORM_DEP_TARGETS cudd_SHARED) -else() - list(APPEND STORM_DEP_TARGETS cudd_STATIC) -endif() +add_dependencies(storm_resources cudd3) +add_dependencies(cudd3 cudd3_src) +list(APPEND STORM_DEP_IMP_TARGETS cudd3) message(STATUS "Storm - Linking with CUDD ${CUDD_VERSION_STRING}.") diff --git a/resources/3rdparty/include_glpk.cmake b/resources/3rdparty/include_glpk.cmake index f869c31fa3..01e51ee491 100644 --- a/resources/3rdparty/include_glpk.cmake +++ b/resources/3rdparty/include_glpk.cmake @@ -1,38 +1,22 @@ +set(STORM_HAVE_GLPK OFF) find_package(GLPK QUIET) + if(GLPK_FOUND) + set(STORM_HAVE_GLPK ON) message (STATUS "Storm - Using system version of glpk.") -else() - message (STATUS "Storm - Using shipped version of glpk.") - set(GLPK_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/glpk-5.0/lib) - - # Set sysroot to circumvent problems in macOS "Mojave" (or higher) where the header files are no longer in /usr/include - set(GLPK_INCLUDE_FLAGS "") - if (CMAKE_OSX_SYSROOT) - set(GLPK_INCLUDE_FLAGS "CPPFLAGS=--sysroot=${CMAKE_OSX_SYSROOT}") - endif() - - ExternalProject_Add(glpk_ext - DOWNLOAD_COMMAND "" - PREFIX ${STORM_3RDPARTY_BINARY_DIR}/glpk-5.0 - SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/glpk-5.0 - CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/glpk-5.0/configure --prefix=${STORM_3RDPARTY_BINARY_DIR}/glpk-5.0 --libdir=${GLPK_LIB_DIR} CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} ${GLPK_INCLUDE_FLAGS} - BUILD_COMMAND make "CFLAGS=-O3 -w" -j${STORM_RESOURCES_BUILD_JOBCOUNT} - INSTALL_COMMAND make install -j${STORM_RESOURCES_BUILD_JOBCOUNT} - BUILD_IN_SOURCE 0 - LOG_CONFIGURE ON - LOG_BUILD ON - LOG_INSTALL ON - BUILD_BYPRODUCTS ${GLPK_LIB_DIR}/libglpk${DYNAMIC_EXT} ${GLPK_LIB_DIR}/libglpk${STATIC_EXT} + message (STATUS "Storm - Linking with glpk ${GLPK_VERSION_STRING}") + + add_library(glpk SHARED IMPORTED) + set_target_properties( + glpk + PROPERTIES + IMPORTED_LOCATION ${GLPK_LIBRARIES} + INTERFACE_INCLUDE_DIRECTORIES ${GLPK_INCLUDE_DIR} ) - set(GLPK_LIBRARIES ${GLPK_LIB_DIR}/libglpk${DYNAMIC_EXT}) - set(GLPK_INCLUDE_DIR ${STORM_3RDPARTY_BINARY_DIR}/glpk-5.0/include) - set(GLPK_VERSION_STRING 5.0) - add_dependencies(resources glpk_ext) + list(APPEND STORM_DEP_IMP_TARGETS glpk) + +else() + message (WARNING "Storm - Not using GLPK.") endif() -# Since there is a shipped version, always use GLPK -set(STORM_HAVE_GLPK ON) -message (STATUS "Storm - Linking with glpk ${GLPK_VERSION_STRING}") -add_imported_library(glpk SHARED ${GLPK_LIBRARIES} ${GLPK_INCLUDE_DIR}) -list(APPEND STORM_DEP_TARGETS glpk_SHARED) diff --git a/resources/3rdparty/include_soplex.cmake b/resources/3rdparty/include_soplex.cmake index 7c03e88bbe..2e32ca2638 100644 --- a/resources/3rdparty/include_soplex.cmake +++ b/resources/3rdparty/include_soplex.cmake @@ -1,14 +1,20 @@ -if (STORM_USE_SOPLEX) +if(NOT STORM_DISABLE_SPOT) find_package(soplex) - IF(SOPLEX_FOUND) + IF(TARGET libsoplex-pic) + set(STORM_HAVE_SOPLEX ON) get_target_property(soplexLOC libsoplex-pic LOCATION) get_target_property(soplexINCLUDE libsoplex-pic INTERFACE_INCLUDE_DIRECTORIES) MESSAGE(STATUS "Storm - Linking with SoPlex version ${soplex_VERSION}: (libary: ${soplexLOC}; include: ${soplexINCLUDE})") list(APPEND STORM_DEP_TARGETS libsoplex-pic) - ELSE(SOPLEX_FOUND) - MESSAGE(WARNING "Storm not linking with SoPlex!") - ENDIF(SOPLEX_FOUND) - set(STORM_HAVE_SOPLEX ${SOPLEX_FOUND}) -ENDIF(STORM_USE_SOPLEX) + ELSE() + set(STORM_HAVE_SOPLEX OFF) + MESSAGE(STATUS "Storm not linking with SoPlex!") + ENDIF() +else() + set(STORM_HAVE_SOPLEX OFF) + MESSAGE(STATUS "Storm not linking with SoPlex!") +endif() + + diff --git a/resources/3rdparty/include_spot.cmake b/resources/3rdparty/include_spot.cmake index 8076598f1e..498d4d255f 100644 --- a/resources/3rdparty/include_spot.cmake +++ b/resources/3rdparty/include_spot.cmake @@ -1,61 +1,108 @@ set(STORM_HAVE_SPOT OFF) +set(STORM_SHIPPED_SPOT OFF) -if(STORM_USE_SPOT_SYSTEM) +if(NOT STORM_DISABLE_SPOT) # try to find Spot on the system if (NOT "${SPOT_ROOT}" STREQUAL "") message(STATUS "Storm - searching for Spot in ${SPOT_ROOT}") - find_package(SPOT QUIET PATHS ${SPOT_ROOT} NO_DEFAULT_PATH) + find_package(Spot QUIET PATHS ${SPOT_ROOT} NO_DEFAULT_PATH) endif() - if (NOT SPOT_FOUND) - find_package(SPOT QUIET) + if (NOT Spot_FOUND) + find_package(Spot QUIET) endif() - if (SPOT_FOUND) - get_filename_component(SPOT_LIB_DIR ${SPOT_LIBRARIES} DIRECTORY) - find_library(BUDDY_LIBRARY NAMES libbddx bddx PATHS ${SPOT_LIB_DIR} NO_DEFAULT_PATH) + if (Spot_FOUND) + get_filename_component(Spot_LIB_DIR ${Spot_LIBRARIES} DIRECTORY) + find_library(BUDDY_LIBRARY NAMES libbddx bddx PATHS ${Spot_LIB_DIR} NO_DEFAULT_PATH) if(NOT BUDDY_LIBRARY) - message(FATAL_ERROR "Storm - Did not find BUDDY library that should ship with spot. To work around this, you may disable the system version Spot with '-DSTORM_USE_SPOT_SYSTEM=OFF'.") + message(FATAL_ERROR "Storm - Did not find BUDDY library that should ship with Spot. To work around this, you may disable the system version Spot with '-DSTORM_USE_Spot_SYSTEM=OFF'.") endif() - set(SPOT_LIBRARIES "${SPOT_LIBRARIES};${BUDDY_LIBRARY}") - message(STATUS "Storm - Using system version of Spot ${SPOT_VERSION} (include: ${SPOT_INCLUDE_DIR}, library: ${SPOT_LIBRARIES}).") + + add_library(Storm::Spot-bddx UNKNOWN IMPORTED) + set_target_properties(Storm::Spot-bddx PROPERTIES + IMPORTED_LOCATION ${BUDDY_LIBRARY}) + + add_library(Storm::Spot UNKNOWN IMPORTED) + set_target_properties(Storm::Spot PROPERTIES + INTERFACE_INCLUDE_DIRECTORIES "${Spot_INCLUDE_DIR}" + IMPORTED_LOCATION "${Spot_LIBRARIES}" + INTERFACE_LINK_LIBRARIES Storm::Spot-bddx + ) + + message(STATUS "Storm - Using system version of Spot ${Spot_VERSION} (include: ${Spot_INCLUDE_DIR}, library: ${Spot_LIBRARIES}).") + list(APPEND STORM_DEP_IMP_TARGETS Storm::Spot) + set(STORM_HAVE_SPOT ON) - elseif(NOT STORM_USE_SPOT_SHIPPED) - message (WARNING "Storm - Could not find Spot. Model checking of LTL formulas (beyond PCTL) will not be supported. You may want to set cmake option STORM_USE_SPOT_SHIPPED to install Spot automatically. If you already installed Spot, consider setting cmake option SPOT_ROOT. Unset STORM_USE_SPOT_SYSTEM to silence this warning.") endif() -elseif() -endif() -set(STORM_SHIPPED_SPOT OFF) -if(STORM_USE_SPOT_SHIPPED AND NOT STORM_HAVE_SPOT) - - # download and install shipped Spot - ExternalProject_Add(spot - URL https://www.lrde.epita.fr/dload/spot/spot-2.13.tar.gz # When updating, also change version output below - DOWNLOAD_NO_PROGRESS TRUE - DOWNLOAD_DIR ${STORM_3RDPARTY_BINARY_DIR}/spot_src - SOURCE_DIR ${STORM_3RDPARTY_BINARY_DIR}/spot_src - PREFIX ${STORM_3RDPARTY_BINARY_DIR}/spot - CONFIGURE_COMMAND ${STORM_3RDPARTY_BINARY_DIR}/spot_src/configure --prefix=${STORM_3RDPARTY_BINARY_DIR}/spot --disable-python - BUILD_COMMAND make -j${STORM_RESOURCES_BUILD_JOBCOUNT} - INSTALL_COMMAND make install -j${STORM_RESOURCES_BUILD_JOBCOUNT} - LOG_CONFIGURE ON - LOG_BUILD ON - LOG_INSTALL ON - BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot${DYNAMIC_EXT} - ) - add_dependencies(resources spot) - set(SPOT_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/spot/include/") - set(SPOT_DIR "${STORM_3RDPARTY_BINARY_DIR}/spot/") - set(SPOT_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot${DYNAMIC_EXT}) - set(SPOT_LIBRARIES "${SPOT_LIBRARIES};${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libbddx${DYNAMIC_EXT}") - set(STORM_HAVE_SPOT ON) - set(STORM_SHIPPED_SPOT ON) - - message(STATUS "Storm - Using shipped version of Spot 2.13 (include: ${SPOT_INCLUDE_DIR}, library ${SPOT_LIBRARIES}).") -endif() + if(NOT Spot_FOUND AND STORM_USE_SPOT_SHIPPED) + # Spot does not set library IDs with an rpath but with an absolute path. + if (APPLE) + set(Spot_RPATH_FIX_COMMAND "install_name_tool;-id;@rpath/libspot.dylib;${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot${DYNAMIC_EXT}") + set(BDDX_RPATH_FIX_COMMAND1 "install_name_tool;-change;${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libbddx.0.dylib;@rpath/libbddx.dylib;${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot${DYNAMIC_EXT}") + set(BDDX_RPATH_FIX_COMMAND2 "install_name_tool;-id;@rpath/libbddx.dylib;${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libbddx${DYNAMIC_EXT}") + else() + set(Spot_RPATH_FIX_COMMAND "true") #no op + set(BDDX_RPATH_FIX_COMMAND1 "true") #no op + set(BDDX_RPATH_FIX_COMMAND2 "true") #no op + endif() + + # download and install shipped Spot as shared libraries. + # Note that configuring static libraries requires various dependencies which was rather cumbersome. + # As of '25/3, SJ did not get this to work. + ExternalProject_Add(Spot -if (STORM_HAVE_SPOT) - include_directories("${SPOT_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES ${SPOT_LIBRARIES}) + URL https://www.lrde.epita.fr/dload/spot/spot-2.13.tar.gz # When updating, also change version output below + DOWNLOAD_NO_PROGRESS TRUE + DOWNLOAD_DIR ${STORM_3RDPARTY_BINARY_DIR}/spot_src + SOURCE_DIR ${STORM_3RDPARTY_BINARY_DIR}/spot_src + PREFIX ${STORM_3RDPARTY_BINARY_DIR}/spot + CONFIGURE_COMMAND ${STORM_3RDPARTY_BINARY_DIR}/spot_src/configure --prefix=${STORM_3RDPARTY_BINARY_DIR}/spot --disable-python #--enable-static --disable-shared + BUILD_COMMAND make -j${STORM_RESOURCES_BUILD_JOBCOUNT} + INSTALL_COMMAND make install -j${STORM_RESOURCES_BUILD_JOBCOUNT} + COMMAND ${Spot_RPATH_FIX_COMMAND} + COMMAND ${BDDX_RPATH_FIX_COMMAND1} + COMMAND ${BDDX_RPATH_FIX_COMMAND2} + LOG_DOWNLOAD ON + LOG_CONFIGURE ON + LOG_BUILD ON + LOG_INSTALL OFF # TODO For debugging + LOG_OUTPUT_ON_FAILURE ON + BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot.0${DYNAMIC_EXT};${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libbddx.0${DYNAMIC_EXT} + ) + add_dependencies(storm_resources Spot) + + set(Spot_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/spot/include/") + set(Spot_LIBRARIES "${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot.0${DYNAMIC_EXT};${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libbddx.0${DYNAMIC_EXT}") + set(Spot_INSTALL_DIR ${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/spot/) + set(STORM_HAVE_SPOT ON) + set(STORM_SHIPPED_SPOT ON) + + file(MAKE_DIRECTORY ${Spot_INCLUDE_DIR}) # Workaround https://gitlab.kitware.com/cmake/cmake/-/issues/15052 + add_library(Storm::Spot-bddx SHARED IMPORTED) + set_target_properties(Storm::Spot-bddx PROPERTIES + INTERFACE_INCLUDE_DIRECTORIES "${STORM_3RDPARTY_BINARY_DIR}/spot/include/" + IMPORTED_LOCATION ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libbddx.0${DYNAMIC_EXT}) + + add_library(Storm::Spot SHARED IMPORTED) + set_target_properties(Storm::Spot PROPERTIES + INTERFACE_INCLUDE_DIRECTORIES "${STORM_3RDPARTY_BINARY_DIR}/spot/include/" + IMPORTED_LOCATION ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot.0${DYNAMIC_EXT} + INTERFACE_LINK_LIBRARIES Storm::Spot-bddx + ) + + install(FILES ${Spot_LIBRARIES} DESTINATION ${STORM_RESOURCE_LIBRARY_INSTALL_DIR}) + install(DIRECTORY ${Spot_INCLUDE_DIR}/ DESTINATION ${Spot_INSTALL_DIR} + FILES_MATCHING PATTERN "*.h" PATTERN "*.hh" PATTERN ".git" EXCLUDE) + + list(APPEND STORM_DEP_IMP_TARGETS Storm::Spot) + add_dependencies(storm_resources Storm::Spot ) + + message(STATUS "Storm - Using shipped version of Spot 2.13 (include: ${Spot_INCLUDE_DIR}, library ${Spot_LIBRARIES}).") + + endif() endif() +if(NOT STORM_HAVE_SPOT) + message("Storm - Not using Spot.") +endif() \ No newline at end of file diff --git a/resources/3rdparty/include_xerces.cmake b/resources/3rdparty/include_xerces.cmake index f318251f9a..32a88a53ac 100644 --- a/resources/3rdparty/include_xerces.cmake +++ b/resources/3rdparty/include_xerces.cmake @@ -1,24 +1,9 @@ -if(USE_XERCESC) - find_package(XercesC QUIET) - if(XercesC_FOUND) - message(STATUS "Storm - Use system version of xerces.") +if(NOT STORM_DISABLE_XERCES) + find_package(XercesC QUIET) + if(TARGET XercesC::XercesC) set(STORM_HAVE_XERCES ON) - include_directories(${XercesC_INCLUDE_DIRS}) - if(APPLE) - FIND_LIBRARY(COREFOUNDATION_LIBRARY CoreFoundation ) - FIND_LIBRARY(CORESERVICES_LIBRARY CoreServices ) - mark_as_advanced(COREFOUNDATION_LIBRARY) - mark_as_advanced(CORESERVICES_LIBRARY) - if(${XercesC_VERSION} VERSION_LESS 3.2.2) - string(REPLACE ".dylib" ".so" XercesC_LIBRARIES ${XercesC_LIBRARIES}) - endif() - endif() - - - # find_package(CURL) - message (STATUS "Storm (GSPN) - Linking with Xerces-c ${XercesC_VERSION}: ${XercesC_LIBRARIES}") - - list(APPEND STORM_GSPN_LINK_LIBRARIES ${XercesC_LIBRARIES} ${COREFOUNDATION_LIBRARY} ${CORESERVICES_LIBRARY} ${CURL_LIBRARIES}) + message (STATUS "Storm (GSPN) - Linking with Xerces-c ${XercesC_VERSION}") + list(APPEND STORM_GSPN_LINK_LIBRARIES XercesC::XercesC) else() set(STORM_HAVE_XERCES OFF) message (STATUS "Storm - Could not find Xerces, will disable parsing XML formats (for GSPNs)") @@ -26,5 +11,5 @@ if(USE_XERCESC) else() set(STORM_HAVE_XERCES OFF) message (STATUS "Storm - Building without Xerces disables parsing XML formats (for GSPNs)") -endif(USE_XERCESC) +endif() diff --git a/resources/3rdparty/nix-scripts/README b/resources/3rdparty/nix-scripts/README deleted file mode 100644 index c4211378e1..0000000000 --- a/resources/3rdparty/nix-scripts/README +++ /dev/null @@ -1,20 +0,0 @@ -This directory contains a nixpkgs overlay that defines the necessary build -scripts to build storm and its dependencies. - -To use it, do one of the following: - 1. Link ./default.nix to ~/.config/nixpkgs/overlays/ - 2. Add its full path to the environment variable NIX_PATH, i.e.: - NIX_PATH=${NIX_PATH}:nixpkgs-overlays=$PWD/default.nix - -See also https://nixos.org/nixpkgs/manual/#chap-overlays for further -information. - -To build storm from the current branch call: - nix-build '' -A stormChecker - -The attribute stormChecker builds storm with minimal options, stormCheckerFull -activates all bells and whistles. See ./default.nix to change build options like -LTO support, Z3 and others. - -See ./storm/default.nix on how to specify a specific Git commit to build storm -from. diff --git a/resources/3rdparty/nix-scripts/carl/default.nix b/resources/3rdparty/nix-scripts/carl/default.nix deleted file mode 100644 index 838a95df76..0000000000 --- a/resources/3rdparty/nix-scripts/carl/default.nix +++ /dev/null @@ -1,52 +0,0 @@ -{ stdenv, fetchFromGitHub, autoconf, pkgconfig, cmake -, cln, ginac, gmp, boost, eigen3_3, python3, googletest }: - -let - gtest-cmake = ./gtest.cmake; - -in stdenv.mkDerivation rec { - name = "carl-${version}"; - version = "18.06"; - - buildInputs = [ cln ginac gmp boost python3 googletest ]; - - nativeBuildInputs = [ autoconf pkgconfig cmake ]; - - propagatedBuildInputs = [ eigen3_3 ]; - - src = fetchFromGitHub { - owner = "smtrat"; - repo = "carl"; - rev = version; - sha256 = "0lb4pbs3bwpi4z4bnh5113s9c4fzq7c8iwa0952j2jrhxf4kcb8q"; - }; - - enableParallelBuilding = true; - - cmakeFlags = [ - "-DEXPORT_TO_CMAKE=off" - "-DUSE_CLN_NUMBERS=on" - "-DTHREAD_SAFE=on" - "-DUSE_GINAC=on" - "-DGINAC_FOUND=on" - "-DGINAC_INCLUDE_DIR=${ginac}/include/ginac" - "-DGINAC_LIBRARY=${ginac}/lib/libginac.so" - "-DGTEST_FOUND=on" - "-DGTEST_VERSION=${googletest.version}" - "-DGTEST_MAIN_LIBRARY=${googletest}/lib/libgtest_main.a" - "-DGTEST_LIBRARY=${googletest}/lib/libgtest.a" - ]; - - postPatch = '' - cp ${gtest-cmake} resources/gtest.cmake - substituteInPlace resources/gtest.cmake --subst-var-by googletest ${googletest} - sed -e '/print_resource_info("GTest"/i include(resources/gtest.cmake)' -i resources/resources.cmake - ''; - - meta = with stdenv.lib; { - description = "Computer ARithmetic and Logic library"; - homepage = http://smtrat.github.io/carl; - mainainers = [ maintainers.spacefrogg ]; - platforms = platforms.all; - }; -} diff --git a/resources/3rdparty/nix-scripts/carl/gtest.cmake b/resources/3rdparty/nix-scripts/carl/gtest.cmake deleted file mode 100644 index 4f098157f9..0000000000 --- a/resources/3rdparty/nix-scripts/carl/gtest.cmake +++ /dev/null @@ -1,3 +0,0 @@ -add_imported_library(GTESTCORE STATIC "@googletest@/lib/${CMAKE_FIND_LIBRARY_PREFIXES}gtest${STATIC_EXT}" "@googletest@/include") -add_imported_library(GTESTMAIN STATIC "@googletest@/lib/${CMAKE_FIND_LIBRARY_PREFIXES}gtest_main${STATIC_EXT}" "@googletest@/include") -set(GTEST_LIBRARIES GTESTCORE_STATIC GTESTMAIN_STATIC pthread dl) \ No newline at end of file diff --git a/resources/3rdparty/nix-scripts/default.nix b/resources/3rdparty/nix-scripts/default.nix deleted file mode 100644 index 2067b839a8..0000000000 --- a/resources/3rdparty/nix-scripts/default.nix +++ /dev/null @@ -1,25 +0,0 @@ -# This file defines a nixpkgs overlay. To use it, do one of the following: -# 1. Link this file to ~/.config/nixpkgs/overlays/ -# 2. Add the full path to the environment variable NIX_PATH, i.e.: -# NIX_PATH=${NIX_PATH}:nixpkgs-overlays=$PWD/default.nix -# See also https://nixos.org/nixpkgs/manual/#chap-overlays -# -# To build storm from the current branch call either of: -# nix-build '' -A stormChecker -# nix-build '' -A stormCheckerFull - -self: super: -with self; -with self.lib; -let - callPackage = super.lib.callPackageWith self; - _self = { - z3 = callPackage ./z3 { }; - stormChecker = callPackage ./storm-checker { ltoSupport = false; tbbSupport = false; mathsatSupport = false; z3Support = false; }; - stormCheckerFull = callPackage ./storm-checker { ltoSupport = true; tbbSupport = true; mathsatSupport = true; z3Support = true; }; - carl = callPackage ./carl { }; - googletest = callPackage ./googletest { }; - l3pp = callPackage ./l3pp { }; - mathsat = callPackage ./mathsat { }; - }; -in _self diff --git a/resources/3rdparty/nix-scripts/googletest/default.nix b/resources/3rdparty/nix-scripts/googletest/default.nix deleted file mode 100644 index b46d51765b..0000000000 --- a/resources/3rdparty/nix-scripts/googletest/default.nix +++ /dev/null @@ -1,22 +0,0 @@ -{ stdenv, fetchFromGitHub, cmake }: - -stdenv.mkDerivation rec { - name = "googletest-${version}"; - version = "1.8.0"; - - buildInputs = [ cmake ]; - - src = fetchFromGitHub { - owner = "google"; - repo = "googletest"; - rev = "release-${version}"; - sha256 = "0bjlljmbf8glnd9qjabx73w6pd7ibv43yiyngqvmvgxsabzr8399"; - }; - - meta = with stdenv.lib; { - description = "Google's C++ test framework"; - homepage = "https://github.com/google/googletest"; - maintainers = [ maintainers.spacefrogg ]; - platforms = platforms.all; - }; -} diff --git a/resources/3rdparty/nix-scripts/l3pp/default.nix b/resources/3rdparty/nix-scripts/l3pp/default.nix deleted file mode 100644 index ac21c5f05e..0000000000 --- a/resources/3rdparty/nix-scripts/l3pp/default.nix +++ /dev/null @@ -1,26 +0,0 @@ -{ stdenv, fetchFromGitHub }: -stdenv.mkDerivation rec { - name = "l3pp-${version}"; - version = "git"; - - src = fetchFromGitHub { - owner = "hbruintjes"; - repo = "l3pp"; - rev = "e4f8d7fe6c328849aff34d2dfd6fd592c14070d5"; - sha256 = "0bd0m4hj7iy5y9546sr7d156hmq6q7d5jys495jd26ngvibkv9hp"; - }; - phases = "unpackPhase installPhase fixupPhase"; - - installPhase = '' - mkdir -p $out/include $out/share/doc/l3pp - cp LICENSE Readme.md $out/share/doc/l3pp - cp -r *.h impl $out/include - ''; - - meta = with stdenv.lib; { - description = "Lightweight Logging Library for C++"; - homepage = https://github.com/hbruintjes/l3pp; - maintainers = [ maintainers.spacefrogg ]; - platforms = platforms.all; - }; -} diff --git a/resources/3rdparty/nix-scripts/mathsat/default.nix b/resources/3rdparty/nix-scripts/mathsat/default.nix deleted file mode 100644 index 180e50a212..0000000000 --- a/resources/3rdparty/nix-scripts/mathsat/default.nix +++ /dev/null @@ -1,46 +0,0 @@ -{ stdenv, fetchurl, file -, gmp -, reentrantBuild ? true -}: - -let - version = "5.5.1"; - name = "mathsat-${version}"; - genUrl = reentrant: "http://mathsat.fbk.eu/download.php?file=${name}-linux-x86_64${reentrant}.tar.gz"; - srcAttrs = if reentrantBuild then { - url = genUrl "-reentrant"; - sha256 = "10ng53nvxyyvml3gbzl87vj3c75fgb14zdlakwasz7zczn7hm978"; - } else { - url = genUrl ""; - sha256 = "0jnbiaq27hzdzavkr3sdh2ym0bc3ykamacj8k08pvyf7vil2hkdz"; - }; - -in stdenv.mkDerivation rec { - inherit name version; - - src = fetchurl srcAttrs; - - nativeBuildInputs = [ gmp ]; - - libPath = stdenv.lib.makeLibraryPath [ stdenv.cc.cc stdenv.cc.libc stdenv.glibc gmp ]; - phases = "unpackPhase installPhase fixupPhase"; - - installPhase = '' - mkdir -p $out/{bin,lib,include} - patchelf --set-rpath "$libPath" lib/libmathsat.so - cp bin/* $out/bin - cp lib/* $out/lib - cp -r include/* $out/include - ''; - - meta = with stdenv.lib; { - description = "Satisfiability modulo theories (SMT) solver"; - homepage = http://mathsat.fbk.eu; - license = { - fullName = "Unfree, redistributable for non-commercial applications"; - free = false; - }; - maintainer = [ maintainers.spacefrogg ]; - platforms = platforms.linux; - }; -} diff --git a/resources/3rdparty/nix-scripts/storm-checker/default.nix b/resources/3rdparty/nix-scripts/storm-checker/default.nix deleted file mode 100644 index a83f53cde5..0000000000 --- a/resources/3rdparty/nix-scripts/storm-checker/default.nix +++ /dev/null @@ -1,53 +0,0 @@ -{ stdenv, fetchFromGitHub, writeText, autoconf, automake, cmake -, boost, carl, cln, doxygen, gmp, ginac, glpk, hwloc, l3pp, xercesc -, ltoSupport ? true -, mathsatSupport ? false, mathsat -, tbbSupport ? false, tbb -, z3Support ? true, z3 -}: - -let - l3ppCmakeSed = writeText "l3pp-sed" '' -8,27d -28i\ -set(l3pp_INCLUDE "${l3pp}/include/") -30d - ''; - inherit (stdenv.lib) optional singleton; - genCmakeOption = bool: name: - singleton "-D${name}=${if bool then "on" else "off"}"; - -in stdenv.mkDerivation { - name = "storm-git"; - - src = ../../../../.; - # Exchange with expression below to build a specific github revision: - # src = fetchFromGitHub { - # owner = "moves-rwth"; - # repo = "storm"; - # rev = "8332abab58f0c672561f5bbebd585a159852d8cc"; - # sha256 = "02ixywhfkxr8xlcizqbysb1yinsjzl6rc0cjlsg8dz8w2r3m6qix"; - # }; - - buildInputs = [ boost carl cln doxygen gmp ginac glpk hwloc l3pp xercesc ] - ++ optional tbbSupport tbb - ++ optional z3Support z3; - - nativeBuildInputs = [ autoconf automake cmake ]; - - cmakeFlags = genCmakeOption tbbSupport "STORM_USE_INTELTBB" - ++ genCmakeOption ltoSupport "STORM_USE_LTO" - ++ optional mathsatSupport "-DMSAT_ROOT=${mathsat}" ; - - postPatch = '' - sed -f ${l3ppCmakeSed} -i resources/3rdparty/CMakeLists.txt - ''; - - meta = with stdenv.lib; { - description = "Probabilistic Model Checker"; - homepage = http://www.stormchecker.org; - license = licenses.gpl3; - maintainer = [ maintainers.spacefrogg ]; - platforms = platforms.all; - }; -} diff --git a/resources/3rdparty/nix-scripts/z3/default.nix b/resources/3rdparty/nix-scripts/z3/default.nix deleted file mode 100644 index 3bb9d1aecb..0000000000 --- a/resources/3rdparty/nix-scripts/z3/default.nix +++ /dev/null @@ -1,20 +0,0 @@ -{ stdenv, fetchFromGitHub, python3 }: - -stdenv.mkDerivation rec { - name = "z3-${version}"; - version = "4.6.0"; - - src = fetchFromGitHub { - owner = "Z3Prover"; - repo = "z3"; - rev = "z3-${version}"; - sha256 = "1cgwlmjdbf4rsv2rriqi2sdpz9qxihxrcpm6a4s37ijy437xg78l"; - }; - - buildInputs = [ python3 ]; - phases = "unpackPhase buildPhase installPhase fixupPhase"; - preBuild = '' - python3 scripts/mk_make.py --prefix=$out - cd build - ''; -} diff --git a/resources/3rdparty/sylvan/cmake/sylvan-config.cmake.in b/resources/3rdparty/sylvan/cmake/sylvan-config.cmake.in new file mode 100644 index 0000000000..9ec09ab913 --- /dev/null +++ b/resources/3rdparty/sylvan/cmake/sylvan-config.cmake.in @@ -0,0 +1,5 @@ +@PACKAGE_INIT@ + +if(NOT TARGET sylvan::sylvan) + include(${CMAKE_CURRENT_LIST_DIR}/sylvan-targets.cmake) +endif() diff --git a/resources/3rdparty/sylvan/src/CMakeLists.txt b/resources/3rdparty/sylvan/src/CMakeLists.txt index 677bc3a5a5..fe4b6e0de5 100644 --- a/resources/3rdparty/sylvan/src/CMakeLists.txt +++ b/resources/3rdparty/sylvan/src/CMakeLists.txt @@ -1,110 +1,210 @@ add_library(sylvan STATIC) add_library(sylvan::sylvan ALIAS sylvan) +set(SYLVAN_HDRS + sylvan.h + sylvan_bdd.h + sylvan_cache.h + sylvan_config.h + sylvan_common.h + sylvan_hash.h + sylvan_int.h + sylvan_ldd.h + sylvan_ldd_int.h + sylvan_mt.h + sylvan_mtbdd.h + sylvan_mtbdd_int.h + sylvan_obj.hpp + sylvan_stats.h + sylvan_table.h + sylvan_tls.h + sylvan_zdd.h + sylvan_zdd_int.h +) + target_sources(sylvan - PRIVATE - sha2.c - sylvan_bdd.c - sylvan_cache.c - sylvan_common.c - sylvan_hash.c - sylvan_ldd.c - sylvan_mt.c - sylvan_mtbdd.c - sylvan_obj.cpp - sylvan_refs.c - sylvan_sl.c - sylvan_stats.c - sylvan_table.c - sylvan_zdd.c -# Added by Storm - lace.c - storm_wrapper.cpp - sylvan_bdd_storm.c - sylvan_mtbdd_storm.c - sylvan_obj_storm.cpp - sylvan_storm_rational_function.c - sylvan_storm_rational_number.c - PUBLIC - PUBLIC - sylvan.h - sylvan_bdd.h - sylvan_cache.h - sylvan_config.h - sylvan_common.h - sylvan_hash.h - sylvan_int.h - sylvan_ldd.h - sylvan_ldd_int.h - sylvan_mt.h - sylvan_mtbdd.h - sylvan_mtbdd_int.h - sylvan_obj.hpp - sylvan_stats.h - sylvan_table.h - sylvan_tls.h - sylvan_zdd.h - sylvan_zdd_int.h -# Added by Storm - lace.h - lace_config.h - storm_wrapper.h - sylvan_bdd_storm.h - sylvan_mtbdd_storm.h - sylvan_storm_rational_function.h - sylvan_storm_rational_number.h -) - -### STORM MODIFICATIONS FOR CARL -# C++11 -> C++14 -# C++14 is needed for CARL -set_target_properties(sylvan PROPERTIES VERSION ${sylvan_VERSION} SOVERSION ${sylvan_VERSION_MAJOR}) -target_compile_features(sylvan PUBLIC c_std_11 cxx_std_14) -target_compile_options(sylvan PRIVATE -Wall -Wextra -fno-strict-aliasing -Wno-deprecated) -target_include_directories(sylvan PUBLIC ${CMAKE_CURRENT_LIST_DIR}) -target_link_libraries(sylvan PUBLIC m pthread) + PRIVATE + sha2.c + sylvan_bdd.c + sylvan_cache.c + sylvan_common.c + sylvan_hash.c + sylvan_ldd.c + sylvan_mt.c + sylvan_mtbdd.c + sylvan_obj.cpp + sylvan_refs.c + sylvan_sl.c + sylvan_stats.c + sylvan_table.c + sylvan_zdd.c + ${SYLVAN_HDRS} +) -### MODIFICATIONS NEEDED FOR STORM -target_include_directories(sylvan PUBLIC ${PROJECT_SOURCE_DIR}/../../../src) -target_include_directories(sylvan PUBLIC ${PROJECT_BINARY_DIR}/../../../include) +## STORMCHANGED BEGIN +set(SYLVAN_STORM_HEADERS + lace.h + lace_config.h + storm_wrapper.h + sylvan_bdd_storm.h + sylvan_mtbdd_storm.h + sylvan_storm_rational_function.h + sylvan_storm_rational_number.h +) +set(SYLVAN_STORM_SOURCES + lace.c # TODO this should no longer be necessary. + storm_wrapper.cpp + sylvan_bdd_storm.c + sylvan_mtbdd_storm.c + sylvan_obj_storm.cpp + sylvan_storm_rational_function.c + sylvan_storm_rational_number.c +) +target_sources(sylvan PRIVATE +${SYLVAN_SYLVAN_STORM_HEADERS} ${SYLVAN_STORM_SOURCES}) +## STORMCHANGED why are the headers additionally added as private sources here? +## -- to comply with twhat is done with sthe SYLVAN_HDRS above. +## END STORMCHANGED option(SYLVAN_GMP "Include custom MTBDD type GMP") if(SYLVAN_GMP) # We only want to include the custom MTBDD type GMP if we actually have the GMP library find_package(GMP REQUIRED) - target_sources(sylvan PRIVATE sylvan_gmp.c PUBLIC sylvan_gmp.h) + set(SYLVAN_HDRS ${SYLVAN_HDRS} sylvan_gmp.h) + target_sources(sylvan PRIVATE sylvan_gmp.c sylvan_gmp.h) target_include_directories(sylvan PRIVATE ${GMP_INCLUDE_DIR}) target_link_libraries(sylvan PUBLIC ${GMP_LIBRARIES}) + set(PKGC_LINK_GMP -lgmp) +else() + set(PKGC_LINK_GMP "") endif() -### STORM MODIFICATIONS FOR CARL +set_target_properties(sylvan PROPERTIES VERSION ${sylvan_VERSION} SOVERSION ${sylvan_VERSION_MAJOR}) +## Stormchanged line below added SYLVAN_STORM_HEADERS +set_target_properties(sylvan PROPERTIES PUBLIC_HEADER "${SYLVAN_HDRS};${SYLVAN_STORM_HEADERS}") + +# STORMCHANGED This is changed by storm as carl requires c++14 +target_compile_features(sylvan PUBLIC c_std_11 cxx_std_14) + +# STORMCHANGED Removed the extra warnings from the debug build, temporarily. +target_compile_options(sylvan PRIVATE + $<$,$>: + -pipe -march=native + #$<$:-O0 -Wall -Wextra>> + $<$:-O0>> + $<$: + $<$:/Od /Wall /Zi>> +) + +target_include_directories(sylvan PUBLIC + $ + $ +) + +# STORMCHANGED lace::lace removed. +target_link_libraries(sylvan PUBLIC m pthread) + +option(SYLVAN_USE_MMAP "Let Sylvan use mmap to allocate (virtual) memory" ON) +if(SYLVAN_USE_MMAP) + include(CheckSymbolExists) + check_symbol_exists(mmap "sys/mman.h" HAVE_MMAP) + if(NOT HAVE_MMAP) + message(WARNING " mmap not found: disabling mmap support") + set(SYLVAN_USE_MMAP OFF) + else() + set_target_properties(sylvan PROPERTIES COMPILE_DEFINITIONS "SYLVAN_USE_MMAP") + endif() +endif() + +# Do we want to collect BDD statistics? +option(SYLVAN_STATS "Let Sylvan collect statistics at runtime" OFF) +if(SYLVAN_STATS) + set_target_properties(sylvan PROPERTIES COMPILE_DEFINITIONS "SYLVAN_STATS") +endif() + +set_target_properties(sylvan PROPERTIES + ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/lib + LIBRARY_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/lib + RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/bin +) + + +## STORMCHANGED BEGIN + +# TODO this is really ugly. +target_include_directories(sylvan PUBLIC + $ + $ +) +target_include_directories(sylvan PUBLIC + $ + $ +) option(USE_CARL "Sets whether carl should be included." ON) if(USE_CARL) target_compile_definitions(sylvan PRIVATE SYLVAN_HAVE_CARL) message(STATUS "Sylvan - Using CArL.") - find_package(carl REQUIRED PATHS ${carl_DIR} NO_DEFAULT_PATH) + # find_package(carl REQUIRED PATHS ${carl_DIR} NO_DEFAULT_PATH) + target_link_libraries(sylvan PUBLIC lib_carl) else() message(STATUS "Sylvan - Not using CArL.") endif() -### +## STORMCHANGED END +## STORMCHANGED START +# TODO changed to sylvan_prefixed variables. Probably worth PR'ing Sylvan such that this is no longer necessary to change. +install(TARGETS sylvan + EXPORT sylvan-targets + ARCHIVE DESTINATION ${SYLVAN_INSTALL_LIBDIR} + LIBRARY DESTINATION ${SYLVAN_INSTALL_LIBDIR} + RUNTIME DESTINATION ${SYLVAN_INSTALL_BINDIR} + INCLUDES DESTINATION ${SYLVAN_INSTALL_INCLUDEDIR} + PUBLIC_HEADER DESTINATION ${SYLVAN_INSTALL_INCLUDEDIR} +) -# Do we want to collect BDD statistics? -option(SYLVAN_STATS "Let Sylvan collect statistics at runtime" OFF) -if(SYLVAN_STATS) - set_target_properties(sylvan PROPERTIES COMPILE_DEFINITIONS "SYLVAN_STATS") -endif() +install(EXPORT sylvan-targets + FILE sylvan-targets.cmake + NAMESPACE sylvan:: + DESTINATION ${SYLVAN_INSTALL_LIBDIR}/cmake/sylvan +) -# MODIFICATIONS NEEDED FOR STORM +include(CMakePackageConfigHelpers) -set_target_properties(sylvan PROPERTIES - ARCHIVE_OUTPUT_DIRECTORY_DEBUG ${CMAKE_CURRENT_BINARY_DIR} - ARCHIVE_OUTPUT_DIRECTORY_RELEASE ${CMAKE_CURRENT_BINARY_DIR}) +configure_package_config_file( + ${PROJECT_SOURCE_DIR}/cmake/sylvan-config.cmake.in + ${CMAKE_CURRENT_BINARY_DIR}/cmake/sylvan-config.cmake + INSTALL_DESTINATION ${SYLVAN_INSTALL_LIBDIR}/cmake/sylvan +) -if(USE_CARL) - message(STATUS "Sylvan - linking CArL.") - target_link_libraries(sylvan PUBLIC ${carl_LIBRARIES}) -endif(USE_CARL) +write_basic_package_version_file( + ${CMAKE_CURRENT_BINARY_DIR}/cmake/sylvan-config-version.cmake + VERSION ${SYLVAN_VERSION} + COMPATIBILITY SameMinorVersion +) + + +#Remark: this file has not been updated, so I guess we could disable this. +configure_file("${CMAKE_CURRENT_SOURCE_DIR}/sylvan.pc.in" "${CMAKE_CURRENT_BINARY_DIR}/sylvan.pc" @ONLY) + +install( + FILES + ${CMAKE_CURRENT_BINARY_DIR}/cmake/sylvan-config.cmake + ${CMAKE_CURRENT_BINARY_DIR}/cmake/sylvan-config-version.cmake + DESTINATION ${SYLVAN_INSTALL_LIBDIR}/cmake/sylvan +) + +#Remark: this file has not been updated, so I guess we could disable this. +install( + FILES + ${CMAKE_CURRENT_BINARY_DIR}/sylvan.pc + DESTINATION ${SYLVAN_INSTALL_LIBDIR}/pkgconfig +) + +export(EXPORT sylvan-targets + FILE ${CMAKE_CURRENT_BINARY_DIR}/cmake/sylvan-targets.cmake + NAMESPACE sylvan:: +) +## STORMCHANGED END \ No newline at end of file diff --git a/resources/3rdparty/sylvan/src/sylvan.pc.in b/resources/3rdparty/sylvan/src/sylvan.pc.in new file mode 100644 index 0000000000..2d06e52e0e --- /dev/null +++ b/resources/3rdparty/sylvan/src/sylvan.pc.in @@ -0,0 +1,10 @@ +libdir=@CMAKE_INSTALL_FULL_LIBDIR@ +includedir=@CMAKE_INSTALL_FULL_INCLUDEDIR@ + +Name: @PROJECT_NAME@ +Description: @PROJECT_DESCRIPTION@ +URL: @PROJECT_HOMEPAGE_URL@ +Version: @PROJECT_VERSION@ +Cflags: -I${includedir} +Libs: -L${libdir} -lsylvan @PKGC_LINK_GMP@ +Requires: lace >= 1.4.2 diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index 67434f395b..afadbd8d79 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -265,7 +265,8 @@ VOID_TASK_0(mtbdd_refs_mark) void mtbdd_refs_init_key(void) { - assert(lace_is_worker()); // only use inside Lace workers + // THIS was commented out as it fails in storm test cases. + // assert(lace_is_worker()); // only use inside Lace workers mtbdd_refs_internal_t s = (mtbdd_refs_internal_t)malloc(sizeof(struct mtbdd_refs_internal)); s->pcur = s->pbegin = (const MTBDD**)malloc(sizeof(MTBDD*) * 1024); s->pend = s->pbegin + 1024; diff --git a/resources/3rdparty/z3/output_version.cpp b/resources/3rdparty/z3/output_version.cpp deleted file mode 100644 index 3f631199e2..0000000000 --- a/resources/3rdparty/z3/output_version.cpp +++ /dev/null @@ -1,9 +0,0 @@ -#include -#include - -int main() { - unsigned major, minor, build_number, revision_number; - Z3_get_version(&major, &minor, &build_number, &revision_number); - std::cout << major << "." << minor << "." << build_number << std::endl; - return 0; -} diff --git a/resources/cmake/find_modules/FindCUDD.cmake b/resources/cmake/find_modules/FindCUDD.cmake deleted file mode 100644 index 8cf09b3e22..0000000000 --- a/resources/cmake/find_modules/FindCUDD.cmake +++ /dev/null @@ -1,43 +0,0 @@ -# - Try to find libglpk -# Once done this will define -# CUDD_FOUND - System has cudd -# CUDD_INCLUDE_DIR - The cudd include directory -# CUDD_LIBRARIES - The libraries needed to use cudd -# CUDD_VERSION_STRING - The version of cudd ("major.minor.release") - -# use pkg-config to get the directories and then use these values -# in the find_path() and find_library() calls -find_package(PkgConfig QUIET) -PKG_CHECK_MODULES(PC_CUDD QUIET cudd) - -find_path(CUDD_INCLUDE_DIR NAMES cudd.h - HINTS - ${PC_CUDD_INCLUDEDIR} - ${PC_CUDD_INCLUDE_DIRS} - PATH_SUFFIXES cudd - ) - -find_library(CUDD_LIBRARIES NAMES cudd - HINTS - ${PC_CUDD_LIBDIR} - ${PC_CUDD_LIBRARY_DIRS} - ) - -if(PC_CUDD_VERSION) - set(CUDD_VERSION_STRING ${PC_CUDD_VERSION}) -elseif(CUDD_INCLUDE_DIR AND EXISTS "${CUDD_INCLUDE_DIR}/cudd.h") - file(STRINGS "${CUDD_INCLUDE_DIR}/cudd.h" cudd_version - REGEX "^#define[\t ]+CUDD_VERSION[\t ]+\".+\"") - string(REGEX REPLACE "^#define[\t ]+CUDD_VERSION[\t ]+\"(.+)\"" "\\1" - CUDD_VERSION_STRING "${cudd_version}") - unset(cudd_version) -endif() - -# handle the QUIETLY and REQUIRED arguments and set LIBXML2_FOUND to TRUE if -# all listed variables are TRUE -include(FindPackageHandleStandardArgs) -FIND_PACKAGE_HANDLE_STANDARD_ARGS(CUDD - REQUIRED_VARS CUDD_LIBRARIES CUDD_INCLUDE_DIR - VERSION_VAR CUDD_VERSION_STRING) - -mark_as_advanced(CUDD_INCLUDE_DIR CUDD_LIBRARIES) diff --git a/resources/cmake/find_modules/FindCusp.cmake b/resources/cmake/find_modules/FindCusp.cmake deleted file mode 100644 index bda1009115..0000000000 --- a/resources/cmake/find_modules/FindCusp.cmake +++ /dev/null @@ -1,56 +0,0 @@ -# -# FindCusp -# -# This module finds the CUSP header files and extracts their version. It -# sets the following variables. -# -# CUSP_INCLUDE_DIR - Include directory for cusp header files. (All header -# files will actually be in the cusp subdirectory.) -# CUSP_VERSION - Version of cusp in the form "major.minor.patch". -# -# CUSP_FOUND - Indicates whether Cusp has been found -# - -find_path(CUSP_INCLUDE_DIR - HINTS - /usr/include/cusp - /usr/local/include - /usr/local/cusp/include - ${CUSP_INCLUDE_DIRS} - ${CUSP_HINT} - NAMES cusp/version.h - DOC "Cusp headers" -) -if(CUSP_INCLUDE_DIR) - list(REMOVE_DUPLICATES CUSP_INCLUDE_DIR) - - # Find cusp version - file(STRINGS ${CUSP_INCLUDE_DIR}/cusp/version.h - version - REGEX "#define CUSP_VERSION[ \t]+([0-9x]+)" - ) - string(REGEX REPLACE - "#define CUSP_VERSION[ \t]+" - "" - version - "${version}" - ) - - #define CUSP_MAJOR_VERSION (CUSP_VERSION / 100000) - #define CUSP_MINOR_VERSION (CUSP_VERSION / 100 % 1000) - #define CUSP_SUBMINOR_VERSION (CUSP_VERSION % 100) - - math(EXPR CUSP_MAJOR_VERSION "${version} / 100000") - math(EXPR CUSP_MINOR_VERSION "${version} / 100 % 1000") - math(EXPR CUSP_PATCH_VERSION "${version} % 100") - - set(CUSP_VERSION "${CUSP_MAJOR_VERSION}.${CUSP_MINOR_VERSION}.${CUSP_PATCH_VERSION}") - - # Check for required components - include(FindPackageHandleStandardArgs) - find_package_handle_standard_args(Cusp REQUIRED_VARS CUSP_INCLUDE_DIR VERSION_VAR CUSP_VERSION) - - set(CUSP_INCLUDE_DIRS ${CUSP_INCLUDE_DIR}) - mark_as_advanced(CUSP_INCLUDE_DIR) - -endif(CUSP_INCLUDE_DIR) \ No newline at end of file diff --git a/resources/cmake/find_modules/FindGMP.cmake b/resources/cmake/find_modules/FindGMP.cmake deleted file mode 100644 index 7f3bc1bfab..0000000000 --- a/resources/cmake/find_modules/FindGMP.cmake +++ /dev/null @@ -1,56 +0,0 @@ -# FindGMP.cmake can be found at https://code.google.com/p/origin/source/browse/trunk/cmake/FindGMP.cmake -# Copyright (c) 2008-2010 Kent State University -# Copyright (c) 2011-2012 Texas A&M University -# -# This file is distributed under the MIT License. See the accompanying file -# LICENSE.txt or http://www.opensource.org/licenses/mit-license.php for terms -# and conditions. -# Modified by David Korzeniewski to also find MPIR as an alternative. - -# FIXME: How do I find the version of GMP that I want to use? -# What versions are available? - -# NOTE: GMP prefix is understood to be the path to the root of the GMP -# installation library. -set(GMP_PREFIX "" CACHE PATH "The path to the prefix of a GMP installation") - - -find_path(GMP_INCLUDE_DIR gmp.h - PATHS ${GMP_PREFIX}/include /usr/include /usr/local/include) - -find_library(GMP_LIBRARY NAMES gmp - PATHS ${GMP_PREFIX}/lib /usr/lib /usr/local/lib) - -find_library(GMP_MPIR_LIBRARY NAMES mpir - PATHS ${GMP_PREFIX}/lib /usr/lib /usr/local/lib) - -find_library(GMP_MPIRXX_LIBRARY NAMES mpirxx - PATHS ${GMP_PREFIX}/lib /usr/lib /usr/local/lib) - - -if(GMP_INCLUDE_DIR AND GMP_LIBRARY) - get_filename_component(GMP_LIBRARY_DIR ${GMP_LIBRARY} PATH) - set(GMP_FOUND TRUE) -endif() - -if(GMP_INCLUDE_DIR AND GMP_MPIR_LIBRARY AND GMP_MPIRXX_LIBRARY) - get_filename_component(GMP_MPIR_LIBRARY_DIR ${GMP_MPIR_LIBRARY} PATH) - get_filename_component(GMP_MPIRXX_LIBRARY_DIR ${GMP_MPIRXX_LIBRARY} PATH) - set(MPIR_FOUND TRUE) -endif() - -if(GMP_FOUND) - if(NOT GMP_FIND_QUIETLY) - MESSAGE(STATUS "Found GMP: ${GMP_LIBRARY}") - endif() -elseif(MPIR_FOUND) - if(NOT GMP_FIND_QUIETLY) - MESSAGE(STATUS "Found GMP alternative MPIR: ${GMP_MPIR_LIBRARY} and ${GMP_MPIRXX_LIBRARY}") - endif() -elseif(GMP_FOUND) - if(GMP_FIND_REQUIRED) - message(FATAL_ERROR "Could not find GMP") - endif() -endif() - -MARK_AS_ADVANCED(GMP_MPIRXX_LIBRARY GMP_MPIR_LIBRARY GMP_INCLUDE_DIR GMP_LIBRARY) \ No newline at end of file diff --git a/resources/cmake/find_modules/FindHWLOC.cmake b/resources/cmake/find_modules/FindHWLOC.cmake deleted file mode 100644 index b0027dd899..0000000000 --- a/resources/cmake/find_modules/FindHWLOC.cmake +++ /dev/null @@ -1,52 +0,0 @@ -# Try to find hwloc libraries and headers. -# -# Usage of this module: -# -# find_package(hwloc) -# -# Variables defined by this module: -# -# HWLOC_FOUND System has hwloc libraries and headers -# HWLOC_LIBRARIES The hwloc library -# HWLOC_INCLUDE_DIRS The location of HWLOC headers - -find_path( - HWLOC_PREFIX - NAMES include/hwloc.h -) - -if (NOT HWLOC_PREFIX AND NOT $ENV{HWLOC_BASE} STREQUAL "") - set(HWLOC_PREFIX $ENV{HWLOC_BASE}) -endif() - - -find_library( - HWLOC_LIBRARIES - NAMES hwloc - HINTS ${HWLOC_PREFIX}/lib -) - -find_path( - HWLOC_INCLUDE_DIRS - NAMES hwloc.h - HINTS ${HWLOC_PREFIX}/include -) - -include(FindPackageHandleStandardArgs) - -find_package_handle_standard_args( - HWLOC DEFAULT_MSG - HWLOC_LIBRARIES - HWLOC_INCLUDE_DIRS -) - -mark_as_advanced( - HWLOC_LIBRARIES - HWLOC_INCLUDE_DIRS -) - -if (HWLOC_FOUND) - if (NOT $ENV{HWLOC_LIB} STREQUAL "") -# set(HWLOC_LIBRARIES "$ENV{HWLOC_LIB}") - endif() -endif() \ No newline at end of file diff --git a/resources/cmake/find_modules/FindMATHSAT.cmake b/resources/cmake/find_modules/FindMATHSAT.cmake new file mode 100644 index 0000000000..bb30d8db5f --- /dev/null +++ b/resources/cmake/find_modules/FindMATHSAT.cmake @@ -0,0 +1,19 @@ +# Try to find libmathsat +# Once done this will define +# MATHSAT_FOUND - System has mathsat +# MATHSAT_INCLUDE_DIRS - The mathsat include directory +# MATHSAT_LIBRARIES - The libraries needed to use mathsat +find_path(MATHSAT_INCLUDE_DIRS NAMES mathsat.h + PATHS ENV PATH INCLUDE "${MATHSAT_ROOT}/include" "/usr/include/mathsat" "/usr/local/include/mathsat/" "/opt/mathsat/include" +) +find_library(MATHSAT_LIBRARIES mathsat + PATHS ENV PATH INCLUDE "${MATHSAT_ROOT}/lib" "/usr/include/mathsat" "/usr/local/include/mathsat/" "/opt/mathsat/lib" +) + +# handle the QUIETLY and REQUIRED arguments and set MATHSAT_FOUND to TRUE if +# all listed variables are TRUE +include(FindPackageHandleStandardArgs) +FIND_PACKAGE_HANDLE_STANDARD_ARGS(MATHSAT +REQUIRED_VARS MATHSAT_LIBRARIES MATHSAT_INCLUDE_DIRS +) +mark_as_advanced(MATHSAT_INCLUDE_DIR MATHSAT_LIBRARIES) \ No newline at end of file diff --git a/resources/cmake/find_modules/FindSPOT.cmake b/resources/cmake/find_modules/FindSPOT.cmake deleted file mode 100644 index f0ba329176..0000000000 --- a/resources/cmake/find_modules/FindSPOT.cmake +++ /dev/null @@ -1,41 +0,0 @@ -# - Try to find libspot -# Once done this will define -# SPOT_FOUND - System has glpk -# SPOT_INCLUDE_DIR - The glpk include directory -# SPOT_LIBRARIES - The libraries needed to use glpk -# SPOT_VERSION - The version of spot - -# use pkg-config to get the directories and then use these values - -# in the find_path() and find_library() calls -find_package(PkgConfig QUIET) -PKG_CHECK_MODULES(PC_SPOT QUIET spot) - -find_path(SPOT_INCLUDE_DIR NAMES spot/misc/_config.h - HINTS - ${PC_SPOT_INCLUDEDIR} - ${PC_SPOT_INCLUDE_DIRS} - ) - -find_library(SPOT_LIBRARIES NAMES spot - HINTS - ${PC_SPOT_LIBDIR} - ${PC_SPOT_LIBRARY_DIRS} - ) - -if(PC_SPOT_VERSION) - set(SPOT_VERSION ${PC_SPOT_VERSION}) -elseif(SPOT_INCLUDE_DIR AND EXISTS "${SPOT_INCLUDE_DIR}/spot/misc/_config.h") - file(STRINGS "${SPOT_INCLUDE_DIR}/spot/misc/_config.h" SPOT_VERSION - REGEX "^#define[\t ]+SPOT_VERSION[\t ]+\".+\"") - string(REGEX REPLACE "^#define[\t ]+SPOT_VERSION[\t ]+\"(.+)\"" "\\1" SPOT_VERSION "${SPOT_VERSION}") -endif() - -# handle the QUIETLY and REQUIRED arguments and set SPOT_FOUND to TRUE if -# all listed variables are TRUE -include(FindPackageHandleStandardArgs) -FIND_PACKAGE_HANDLE_STANDARD_ARGS(SPOT - REQUIRED_VARS SPOT_LIBRARIES SPOT_INCLUDE_DIR - VERSION_VAR SPOT_VERSION) - -mark_as_advanced(SPOT_INCLUDE_DIR SPOT_LIBRARIES) diff --git a/resources/cmake/find_modules/FindSpot.cmake b/resources/cmake/find_modules/FindSpot.cmake new file mode 100644 index 0000000000..eb53c3e63b --- /dev/null +++ b/resources/cmake/find_modules/FindSpot.cmake @@ -0,0 +1,41 @@ +# - Try to find libSpot +# Once done this will define +# Spot_FOUND - System has glpk +# Spot_INCLUDE_DIR - The glpk include directory +# Spot_LIBRARIES - The libraries needed to use glpk +# Spot_VERSION - The version of Spot + +# use pkg-config to get the directories and then use these values + +# in the find_path() and find_library() calls +find_package(PkgConfig QUIET) +PKG_CHECK_MODULES(PC_Spot QUIET Spot) + +find_path(Spot_INCLUDE_DIR NAMES Spot/misc/_config.h + HINTS + ${PC_Spot_INCLUDEDIR} + ${PC_Spot_INCLUDE_DIRS} + ) + +find_library(Spot_LIBRARIES NAMES Spot + HINTS + ${PC_Spot_LIBDIR} + ${PC_Spot_LIBRARY_DIRS} + ) + +if(PC_Spot_VERSION) + set(Spot_VERSION ${PC_Spot_VERSION}) +elseif(Spot_INCLUDE_DIR AND EXISTS "${Spot_INCLUDE_DIR}/Spot/misc/_config.h") + file(STRINGS "${Spot_INCLUDE_DIR}/Spot/misc/_config.h" Spot_VERSION + REGEX "^#define[\t ]+Spot_VERSION[\t ]+\".+\"") + string(REGEX REPLACE "^#define[\t ]+Spot_VERSION[\t ]+\"(.+)\"" "\\1" Spot_VERSION "${Spot_VERSION}") +endif() + +# handle the QUIETLY and REQUIRED arguments and set Spot_FOUND to TRUE if +# all listed variables are TRUE +include(FindPackageHandleStandardArgs) +FIND_PACKAGE_HANDLE_STANDARD_ARGS(Spot + REQUIRED_VARS Spot_LIBRARIES Spot_INCLUDE_DIR + VERSION_VAR Spot_VERSION) + +mark_as_advanced(Spot_INCLUDE_DIR Spot_LIBRARIES) diff --git a/resources/cmake/find_modules/FindTBB.cmake b/resources/cmake/find_modules/FindTBB.cmake deleted file mode 100644 index 8a2ae28fc8..0000000000 --- a/resources/cmake/find_modules/FindTBB.cmake +++ /dev/null @@ -1,310 +0,0 @@ -# FindTBB.cmake can be found at https://code.google.com/p/findtbb/ -# Written by Hannes Hofmann <hannes.hofmann _at_ informatik.uni-erlangen.de> -# Improvements by Gino van den Bergen <gino _at_ dtecta.com>, -# Florian Uhlig <F.Uhlig _at_ gsi.de>, -# Jiri Marsik <jiri.marsik89 _at_ gmail.com> - -# The MIT License -# -# Copyright (c) 2011 Hannes Hofmann -# -# Permission is hereby granted, free of charge, to any person obtaining a copy -# of this software and associated documentation files (the "Software"), to deal -# in the Software without restriction, including without limitation the rights -# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell -# copies of the Software, and to permit persons to whom the Software is -# furnished to do so, subject to the following conditions: -# -# The above copyright notice and this permission notice shall be included in -# all copies or substantial portions of the Software. -# -# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN -# THE SOFTWARE. - -# GvdB: This module uses the environment variable TBB_ARCH_PLATFORM which defines architecture and compiler. -# e.g. "ia32/vc8" or "em64t/cc4.1.0_libc2.4_kernel2.6.16.21" -# TBB_ARCH_PLATFORM is set by the build script tbbvars[.bat|.sh|.csh], which can be found -# in the TBB installation directory (TBB_INSTALL_DIR). -# -# GvdB: Mac OS X distribution places libraries directly in lib directory. -# -# For backwards compatibility, you may explicitely set the CMake variables TBB_ARCHITECTURE and TBB_COMPILER. -# TBB_ARCHITECTURE [ ia32 | em64t | itanium ] -# which architecture to use -# TBB_COMPILER e.g. vc9 or cc3.2.3_libc2.3.2_kernel2.4.21 or cc4.0.1_os10.4.9 -# which compiler to use (detected automatically on Windows) - -# This module respects -# TBB_INSTALL_DIR or $ENV{TBB21_INSTALL_DIR} or $ENV{TBB_INSTALL_DIR} - -# This module defines -# TBB_INCLUDE_DIRS, where to find task_scheduler_init.h, etc. -# TBB_LIBRARY_DIRS, where to find libtbb, libtbbmalloc -# TBB_DEBUG_LIBRARY_DIRS, where to find libtbb_debug, libtbbmalloc_debug -# TBB_INSTALL_DIR, the base TBB install directory -# TBB_LIBRARIES, the libraries to link against to use TBB. -# TBB_DEBUG_LIBRARIES, the libraries to link against to use TBB with debug symbols. -# TBB_FOUND, If false, don't try to use TBB. -# TBB_INTERFACE_VERSION, as defined in tbb/tbb_stddef.h - - -if (WIN32) - # has em64t/vc8 em64t/vc9 - # has ia32/vc7.1 ia32/vc8 ia32/vc9 - set(_TBB_DEFAULT_INSTALL_DIR "C:/Program Files/Intel/TBB" "C:/Program Files (x86)/Intel/TBB" "C:/Program Files (x86)/Intel/Composer XE 2013/tbb") - set(_TBB_LIB_NAME "tbb") - set(_TBB_LIB_MALLOC_NAME "${_TBB_LIB_NAME}malloc") - set(_TBB_LIB_DEBUG_NAME "${_TBB_LIB_NAME}_debug") - set(_TBB_LIB_MALLOC_DEBUG_NAME "${_TBB_LIB_MALLOC_NAME}_debug") - if (MSVC71) - set (_TBB_COMPILER "vc7.1") - endif(MSVC71) - if (MSVC80) - set(_TBB_COMPILER "vc8") - endif(MSVC80) - if (MSVC90) - set(_TBB_COMPILER "vc9") - endif(MSVC90) - if(MSVC10) - set(_TBB_COMPILER "vc10") - endif(MSVC10) - if(MSVC11) - set(_TBB_COMPILER "vc11") - endif(MSVC11) - if(MSVC12) - set(_TBB_COMPILER "vc12") - endif(MSVC12) - # Todo: add other Windows compilers such as ICL. - set(_TBB_ARCHITECTURE ${TBB_ARCHITECTURE}) -endif (WIN32) - -if (UNIX) - if (APPLE) - # MAC - set(_TBB_DEFAULT_INSTALL_DIR "/Library/Frameworks/Intel_TBB.framework/Versions") - # libs: libtbb.dylib, libtbbmalloc.dylib, *_debug - set(_TBB_LIB_NAME "tbb") - set(_TBB_LIB_MALLOC_NAME "${_TBB_LIB_NAME}malloc") - set(_TBB_LIB_DEBUG_NAME "${_TBB_LIB_NAME}_debug") - set(_TBB_LIB_MALLOC_DEBUG_NAME "${_TBB_LIB_MALLOC_NAME}_debug") - # default flavor on apple: ia32/cc4.0.1_os10.4.9 - # Jiri: There is no reason to presume there is only one flavor and - # that user's setting of variables should be ignored. - if(NOT TBB_COMPILER) - set(_TBB_COMPILER "cc4.0.1_os10.4.9") - elseif (NOT TBB_COMPILER) - set(_TBB_COMPILER ${TBB_COMPILER}) - endif(NOT TBB_COMPILER) - if(NOT TBB_ARCHITECTURE) - set(_TBB_ARCHITECTURE "ia32") - elseif(NOT TBB_ARCHITECTURE) - set(_TBB_ARCHITECTURE ${TBB_ARCHITECTURE}) - endif(NOT TBB_ARCHITECTURE) - else (APPLE) - # LINUX - set(_TBB_DEFAULT_INSTALL_DIR "/opt/intel/tbb" "/usr/local/include" "/usr/include") - set(_TBB_LIB_NAME "tbb") - set(_TBB_LIB_MALLOC_NAME "${_TBB_LIB_NAME}malloc") - set(_TBB_LIB_DEBUG_NAME "${_TBB_LIB_NAME}_debug") - set(_TBB_LIB_MALLOC_DEBUG_NAME "${_TBB_LIB_MALLOC_NAME}_debug") - # has em64t/cc3.2.3_libc2.3.2_kernel2.4.21 em64t/cc3.3.3_libc2.3.3_kernel2.6.5 em64t/cc3.4.3_libc2.3.4_kernel2.6.9 em64t/cc4.1.0_libc2.4_kernel2.6.16.21 - # has ia32/* - # has itanium/* - set(_TBB_COMPILER ${TBB_COMPILER}) - set(_TBB_ARCHITECTURE ${TBB_ARCHITECTURE}) - endif (APPLE) -endif (UNIX) - -if (CMAKE_SYSTEM MATCHES "SunOS.*") -# SUN -# not yet supported -# has em64t/cc3.4.3_kernel5.10 -# has ia32/* -endif (CMAKE_SYSTEM MATCHES "SunOS.*") - - -#-- Clear the public variables -set (TBB_FOUND "NO") - - -#-- Find TBB install dir and set ${_TBB_INSTALL_DIR} and cached ${TBB_INSTALL_DIR} -# first: use CMake variable TBB_INSTALL_DIR -if (TBB_INSTALL_DIR) - set (_TBB_INSTALL_DIR ${TBB_INSTALL_DIR}) -endif (TBB_INSTALL_DIR) -# second: use environment variable -if (NOT _TBB_INSTALL_DIR) - if (NOT "$ENV{TBB_INSTALL_DIR}" STREQUAL "") - set (_TBB_INSTALL_DIR $ENV{TBB_INSTALL_DIR}) - endif (NOT "$ENV{TBB_INSTALL_DIR}" STREQUAL "") - # Intel recommends setting TBB21_INSTALL_DIR - if (NOT "$ENV{TBB21_INSTALL_DIR}" STREQUAL "") - set (_TBB_INSTALL_DIR $ENV{TBB21_INSTALL_DIR}) - endif (NOT "$ENV{TBB21_INSTALL_DIR}" STREQUAL "") - if (NOT "$ENV{TBB22_INSTALL_DIR}" STREQUAL "") - set (_TBB_INSTALL_DIR $ENV{TBB22_INSTALL_DIR}) - endif (NOT "$ENV{TBB22_INSTALL_DIR}" STREQUAL "") - if (NOT "$ENV{TBB30_INSTALL_DIR}" STREQUAL "") - set (_TBB_INSTALL_DIR $ENV{TBB30_INSTALL_DIR}) - endif (NOT "$ENV{TBB30_INSTALL_DIR}" STREQUAL "") -endif (NOT _TBB_INSTALL_DIR) -# third: try to find path automatically -if (NOT _TBB_INSTALL_DIR) - if (_TBB_DEFAULT_INSTALL_DIR) - set (_TBB_INSTALL_DIR ${_TBB_DEFAULT_INSTALL_DIR}) - endif (_TBB_DEFAULT_INSTALL_DIR) -endif (NOT _TBB_INSTALL_DIR) -# sanity check -if (NOT _TBB_INSTALL_DIR) - message ("ERROR: Unable to find Intel TBB install directory. ${_TBB_INSTALL_DIR}") -else (NOT _TBB_INSTALL_DIR) -# finally: set the cached CMake variable TBB_INSTALL_DIR -if (NOT TBB_INSTALL_DIR) - mark_as_advanced(TBB_INSTALL_DIR) -endif (NOT TBB_INSTALL_DIR) - - -#-- A macro to rewrite the paths of the library. This is necessary, because -# find_library() always found the em64t/vc9 version of the TBB libs -macro(TBB_CORRECT_LIB_DIR var_name) -# if (NOT "${_TBB_ARCHITECTURE}" STREQUAL "em64t") - string(REPLACE em64t "${_TBB_ARCHITECTURE}" ${var_name} ${${var_name}}) -# endif (NOT "${_TBB_ARCHITECTURE}" STREQUAL "em64t") - string(REPLACE ia32 "${_TBB_ARCHITECTURE}" ${var_name} ${${var_name}}) - string(REPLACE vc7.1 "${_TBB_COMPILER}" ${var_name} ${${var_name}}) - string(REPLACE vc8 "${_TBB_COMPILER}" ${var_name} ${${var_name}}) - string(REPLACE vc9 "${_TBB_COMPILER}" ${var_name} ${${var_name}}) - string(REPLACE vc10 "${_TBB_COMPILER}" ${var_name} ${${var_name}}) - string(REPLACE vc11 "${_TBB_COMPILER}" ${var_name} ${${var_name}}) - string(REPLACE vc12 "${_TBB_COMPILER}" ${var_name} ${${var_name}}) -endmacro(TBB_CORRECT_LIB_DIR var_content) - - -#-- Look for include directory and set ${TBB_INCLUDE_DIR} -set (TBB_INC_SEARCH_DIR ${_TBB_INSTALL_DIR}/include) -# Jiri: tbbvars now sets the CPATH environment variable to the directory -# containing the headers. -find_path(TBB_INCLUDE_DIR tbb/tbb_stddef.h PATHS "${TBB_INC_SEARCH_DIR}" ENV CPATH) -mark_as_advanced(TBB_INCLUDE_DIR) - -#-- Look for libraries -include(CheckSymbolExists) - -# Check if we are on Windows -CHECK_SYMBOL_EXISTS("_WIN32" "" FINDTBB_HAVE_WIN32) -CHECK_SYMBOL_EXISTS("_WIN64" "" FINDTBB_HAVE_WIN64) -if(FINDTBB_HAVE_WIN64) - # this is a build on 64bit Windows - set(_TBB_ARCHITECTURE "intel64") - set (_TBB_LIBRARY_DIR "${_TBB_INSTALL_DIR}/lib/${_TBB_ARCHITECTURE}/${_TBB_COMPILER}" ${_TBB_LIBRARY_DIR}) -elseif(FINDTBB_HAVE_WIN32) - # this is a build on 32bit Windows - set(_TBB_ARCHITECTURE "ia32") - set (_TBB_LIBRARY_DIR "${_TBB_INSTALL_DIR}/lib/${_TBB_ARCHITECTURE}/${_TBB_COMPILER}" ${_TBB_LIBRARY_DIR}) -endif() - -# GvdB: $ENV{TBB_ARCH_PLATFORM} is set by the build script tbbvars[.bat|.sh|.csh] -if (NOT $ENV{TBB_ARCH_PLATFORM} STREQUAL "") - set (_TBB_LIBRARY_DIR - ${_TBB_INSTALL_DIR}/lib/$ENV{TBB_ARCH_PLATFORM} - ${_TBB_INSTALL_DIR}/$ENV{TBB_ARCH_PLATFORM}/lib - ) -endif (NOT $ENV{TBB_ARCH_PLATFORM} STREQUAL "") -# Jiri: This block isn't mutually exclusive with the previous one -# (hence no else), instead I test if the user really specified -# the variables in question. -if ((NOT ${TBB_ARCHITECTURE} STREQUAL "") AND (NOT ${TBB_COMPILER} STREQUAL "")) - # HH: deprecated - message(STATUS "[Warning] FindTBB.cmake: The use of TBB_ARCHITECTURE and TBB_COMPILER is deprecated and may not be supported in future versions. Please set \$ENV{TBB_ARCH_PLATFORM} (using tbbvars.[bat|csh|sh]).") - # Jiri: It doesn't hurt to look in more places, so I store the hints from - # ENV{TBB_ARCH_PLATFORM} and the TBB_ARCHITECTURE and TBB_COMPILER - # variables and search them both. - set (_TBB_LIBRARY_DIR "${_TBB_INSTALL_DIR}/${_TBB_ARCHITECTURE}/${_TBB_COMPILER}/lib" ${_TBB_LIBRARY_DIR}) -endif ((NOT ${TBB_ARCHITECTURE} STREQUAL "") AND (NOT ${TBB_COMPILER} STREQUAL "")) - -# GvdB: Mac OS X distribution places libraries directly in lib directory. -if (USE_LIBCXX OR LINK_LIBCXXABI) - message(STATUS "FindTBB - Detected libc++ usage, linking to TBB with libc++!") - list(APPEND _TBB_LIBRARY_DIR "${_TBB_INSTALL_DIR}/lib/libc++") -else() - list(APPEND _TBB_LIBRARY_DIR "${_TBB_INSTALL_DIR}/lib") -endif() - -message(STATUS "Searching for TBB: TBB_LIBRARY ${_TBB_LIB_NAME} HINTS ${_TBB_LIBRARY_DIR}, _TBB_COMPILER = ${_TBB_COMPILER} and _TBB_ARCHITECTURE = ${_TBB_ARCHITECTURE}") - -# Jiri: No reason not to check the default paths. From recent versions, -# tbbvars has started exporting the LIBRARY_PATH and LD_LIBRARY_PATH -# variables, which now point to the directories of the lib files. -# It all makes more sense to use the ${_TBB_LIBRARY_DIR} as a HINTS -# argument instead of the implicit PATHS as it isn't hard-coded -# but computed by system introspection. Searching the LIBRARY_PATH -# and LD_LIBRARY_PATH environment variables is now even more important -# that tbbvars doesn't export TBB_ARCH_PLATFORM and it facilitates -# the use of TBB built from sources. -find_library(TBB_LIBRARY ${_TBB_LIB_NAME} HINTS ${_TBB_LIBRARY_DIR} - PATHS ENV LIBRARY_PATH ENV LD_LIBRARY_PATH) -find_library(TBB_MALLOC_LIBRARY ${_TBB_LIB_MALLOC_NAME} HINTS ${_TBB_LIBRARY_DIR} - PATHS ENV LIBRARY_PATH ENV LD_LIBRARY_PATH) - -#Extract path from TBB_LIBRARY name -get_filename_component(TBB_LIBRARY_DIR ${TBB_LIBRARY} PATH) - -#TBB_CORRECT_LIB_DIR(TBB_LIBRARY) -#TBB_CORRECT_LIB_DIR(TBB_MALLOC_LIBRARY) -mark_as_advanced(TBB_LIBRARY TBB_MALLOC_LIBRARY) - -#-- Look for debug libraries -# Jiri: Changed the same way as for the release libraries. -find_library(TBB_LIBRARY_DEBUG ${_TBB_LIB_DEBUG_NAME} HINTS ${_TBB_LIBRARY_DIR} - PATHS ENV LIBRARY_PATH ENV LD_LIBRARY_PATH) -find_library(TBB_MALLOC_LIBRARY_DEBUG ${_TBB_LIB_MALLOC_DEBUG_NAME} HINTS ${_TBB_LIBRARY_DIR} - PATHS ENV LIBRARY_PATH ENV LD_LIBRARY_PATH) - -# Jiri: Self-built TBB stores the debug libraries in a separate directory. -# Extract path from TBB_LIBRARY_DEBUG name -get_filename_component(TBB_LIBRARY_DEBUG_DIR ${TBB_LIBRARY_DEBUG} PATH) - -#TBB_CORRECT_LIB_DIR(TBB_LIBRARY_DEBUG) -#TBB_CORRECT_LIB_DIR(TBB_MALLOC_LIBRARY_DEBUG) -mark_as_advanced(TBB_LIBRARY_DEBUG TBB_MALLOC_LIBRARY_DEBUG) - -if (TBB_INCLUDE_DIR) - if (TBB_LIBRARY) - set (TBB_FOUND ON) - set (TBB_LIBRARIES ${TBB_LIBRARY} ${TBB_MALLOC_LIBRARY} ${TBB_LIBRARIES}) - set (TBB_DEBUG_LIBRARIES ${TBB_LIBRARY_DEBUG} ${TBB_MALLOC_LIBRARY_DEBUG} ${TBB_DEBUG_LIBRARIES}) - set (TBB_INCLUDE_DIRS ${TBB_INCLUDE_DIR} CACHE PATH "TBB include directory" FORCE) - set (TBB_LIBRARY_DIRS ${TBB_LIBRARY_DIR} CACHE PATH "TBB library directory" FORCE) - # Jiri: Self-built TBB stores the debug libraries in a separate directory. - set (TBB_DEBUG_LIBRARY_DIRS ${TBB_LIBRARY_DEBUG_DIR} CACHE PATH "TBB debug library directory" FORCE) - mark_as_advanced(TBB_INCLUDE_DIRS TBB_LIBRARY_DIRS TBB_DEBUG_LIBRARY_DIRS TBB_LIBRARIES TBB_DEBUG_LIBRARIES) - message(STATUS "Found Intel TBB") - endif (TBB_LIBRARY) -endif (TBB_INCLUDE_DIR) - -if (NOT TBB_FOUND) - message("ERROR: Intel TBB NOT found!") - message(STATUS "Looked for Threading Building Blocks in ${_TBB_INSTALL_DIR}") - # do only throw fatal, if this pkg is REQUIRED - if (TBB_FIND_REQUIRED) - message(FATAL_ERROR "Could NOT find TBB library.") - endif (TBB_FIND_REQUIRED) -endif (NOT TBB_FOUND) - -endif (NOT _TBB_INSTALL_DIR) - -if (TBB_FOUND) - set(TBB_INTERFACE_VERSION 0) - FILE(READ "${TBB_INCLUDE_DIRS}/tbb/tbb_stddef.h" _TBB_VERSION_CONTENTS) - STRING(REGEX REPLACE ".*#define TBB_INTERFACE_VERSION ([0-9]+).*" "\\1" TBB_INTERFACE_VERSION "${_TBB_VERSION_CONTENTS}") - STRING(REGEX REPLACE ".*#define TBB_VERSION_MAJOR ([0-9]+).*" "\\1" TBB_VERSION_MAJOR "${_TBB_VERSION_CONTENTS}") - STRING(REGEX REPLACE ".*#define TBB_VERSION_MINOR ([0-9]+).*" "\\1" TBB_VERSION_MINOR "${_TBB_VERSION_CONTENTS}") - set(TBB_INTERFACE_VERSION "${TBB_INTERFACE_VERSION}") - set(TBB_VERSION_MAJOR "${TBB_VERSION_MAJOR}") - set(TBB_VERSION_MINOR "${TBB_VERSION_MINOR}") -endif (TBB_FOUND) \ No newline at end of file diff --git a/resources/cmake/find_modules/FindThrust.cmake b/resources/cmake/find_modules/FindThrust.cmake deleted file mode 100644 index 8f811bda36..0000000000 --- a/resources/cmake/find_modules/FindThrust.cmake +++ /dev/null @@ -1,52 +0,0 @@ -# -# FindThrust -# -# This module finds the Thrust header files and extracts their version. It -# sets the following variables. -# -# THRUST_INCLUDE_DIR - Include directory for thrust header files. (All header -# files will actually be in the thrust subdirectory.) -# THRUST_VERSION - Version of thrust in the form "major.minor.patch". -# -# Thrust_FOUND - Indicates whether Thrust has been found -# - -find_path(THRUST_INCLUDE_DIR - HINTS - /usr/include/cuda - /usr/local/include - /usr/local/cuda/include - ${CUDA_INCLUDE_DIRS} - NAMES thrust/version.h - DOC "Thrust headers" -) -if(THRUST_INCLUDE_DIR) - list(REMOVE_DUPLICATES THRUST_INCLUDE_DIR) -endif(THRUST_INCLUDE_DIR) - -# Find thrust version -file(STRINGS ${THRUST_INCLUDE_DIR}/thrust/version.h - version - REGEX "#define THRUST_VERSION[ \t]+([0-9x]+)" -) -string(REGEX REPLACE - "#define THRUST_VERSION[ \t]+" - "" - version - "${version}" -) - -string(REGEX MATCH "^[0-9]" major ${version}) -string(REGEX REPLACE "^${major}00" "" version "${version}") -string(REGEX MATCH "^[0-9]" minor ${version}) -string(REGEX REPLACE "^${minor}0" "" version "${version}") -set(THRUST_VERSION "${major}.${minor}.${version}") -set(THRUST_MAJOR_VERSION "${major}") -set(THRUST_MINOR_VERSION "${minor}") - -# Check for required components -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(Thrust REQUIRED_VARS THRUST_INCLUDE_DIR VERSION_VAR THRUST_VERSION) - -set(THRUST_INCLUDE_DIRS ${THRUST_INCLUDE_DIR}) -mark_as_advanced(THRUST_INCLUDE_DIR) \ No newline at end of file diff --git a/resources/cmake/find_modules/FindZ3.cmake b/resources/cmake/find_modules/FindZ3.cmake index 6c6a7beb14..79bc533ff0 100644 --- a/resources/cmake/find_modules/FindZ3.cmake +++ b/resources/cmake/find_modules/FindZ3.cmake @@ -1,47 +1,81 @@ -# - Try to find libz3 +# From https://github.com/SRI-CSL/sally/blob/master/cmake/FindZ3.cmake +# - Try to find Z3 # Once done this will define -# LIBZ3_FOUND - System has libz3 -# LIBZ3_INCLUDE_DIRS - The libz3 include directories -# LIBZ3_LIBRARIES - The libraries needed to use libz3 - -# dependencies -# -- TODO -- needed? - -# find include dir by searching for a concrete file, which definitely must be in it -find_path(Z3_INCLUDE_DIR - NAMES z3++.h - PATHS ENV PATH INCLUDE "${Z3_ROOT}/include" "/usr/include/z3" "/usr/local/include/z3/" - ) - -# find library -find_library(Z3_LIBRARY - NAMES z3 - PATHS ENV PATH INCLUDE "${Z3_ROOT}/lib" - ) - -find_program(Z3_EXEC - NAMES z3 - PATHS ENV PATH INCLUDE "${Z3_ROOT}/bin" -) - -# set up the final variables +# Z3_FOUND - System has Z3 +# Z3_INCLUDE_DIRS - The Z3 include directories +# Z3_LIBRARIES - The libraries needed to use Z3 + +if (Z3_ROOT) + find_path(Z3_INCLUDE_DIR z3.h PATHS "${Z3_ROOT}/include" NO_DEFAULT_PATH) +else() + find_path(Z3_INCLUDE_DIR z3.h) +endif() + +if (Z3_ROOT) + find_library(Z3_LIBRARY z3 PATHS "${Z3_ROOT}/lib" NO_DEFAULT_PATH) +else() + find_library(Z3_LIBRARY z3) +endif() + +# If library found, check the version +if (Z3_INCLUDE_DIR AND Z3_LIBRARY AND Z3_FIND_VERSION) + + # Check version from char *msat_get_version(void) + file(WRITE "${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/z3.cpp" " + #include + #include \"z3.h\" + + int main() { + unsigned major, minor, build_number, revision_number; + Z3_get_version(&major, &minor, &build_number, &revision_number); + printf(\"%u.%u.%u.%u\\n\", major, minor, build_number, revision_number); + return 0; + } + ") + + # Run the test program + try_run( + VERSION_TEST_EXITCODE + VERSION_TEST_COMPILED + ${CMAKE_BINARY_DIR} + ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/z3.cpp + COMPILE_DEFINITIONS + -I"${Z3_INCLUDE_DIR}" + LINK_LIBRARIES ${Z3_LIBRARY} ${GMP_LIBRARY} + CMAKE_FLAGS + -DCMAKE_SKIP_RPATH:BOOL=${CMAKE_SKIP_RPATH} + RUN_OUTPUT_VARIABLE + VERSION_TEST_RUN_OUTPUT + ) + + if (NOT VERSION_TEST_COMPILED) + unset(Z3_INCLUDE_DIR CACHE) + unset(Z3_LIBRARY CACHE) + elseif (NOT ("${VERSION_TEST_EXITCODE}" EQUAL 0)) + unset(Z3_INCLUDE_DIR CACHE) + unset(Z3_LIBRARY CACHE) + else() + # Output is of the form: major.minor.build_number.revision + if("${VERSION_TEST_RUN_OUTPUT}" MATCHES "([0-9]*\\.[0-9]*\\.[0-9]*\\.[0-9]*)") + set(Z3_VERSION "${CMAKE_MATCH_1}") + if ("${Z3_VERSION}" VERSION_LESS "${Z3_FIND_VERSION}") + unset(Z3_INCLUDE_DIR CACHE) + unset(Z3_LIBRARY CACHE) + elseif (Z3_FIND_VERSION_EXACT AND NOT "${Z3_VERSION}" VERSION_EQUAL "${Z3_FIND_VERSION}") + unset(Z3_INCLUDE_DIR CACHE) + unset(Z3_LIBRARY CACHE) + endif() + else() + unset(Z3_INCLUDE_DIR CACHE) + unset(Z3_LIBRARY CACHE) + endif() + endif() +endif() + set(Z3_LIBRARIES ${Z3_LIBRARY}) set(Z3_INCLUDE_DIRS ${Z3_INCLUDE_DIR}) -set(Z3_SOLVER ${Z3_EXEC}) -# set the LIBZ3_FOUND variable by utilizing the following macro -# (which also handles the REQUIRED and QUIET arguments) include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(Z3 DEFAULT_MSG - Z3_LIBRARY Z3_INCLUDE_DIR) - -IF (NOT Z3_FIND_QUIETLY) - MESSAGE(STATUS "Found Z3: ${Z3_LIBRARY}") -ENDIF (NOT Z3_FIND_QUIETLY) - -# debug output to see if everything went well -#message(${Z3_INCLUDE_DIR}) -#message(${Z3_LIBRARY}) +find_package_handle_standard_args(Z3 DEFAULT_MSG Z3_LIBRARY Z3_INCLUDE_DIR) -# make the set variables only visible in advanced mode -mark_as_advanced(Z3_LIBRARY Z3_INCLUDE_DIR Z3_SOLVER, Z3_EXEC) +mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARY) \ No newline at end of file diff --git a/resources/cmake/macros/RegisterSourceGroup.cmake b/resources/cmake/macros/RegisterSourceGroup.cmake deleted file mode 100644 index c36a9a3eb2..0000000000 --- a/resources/cmake/macros/RegisterSourceGroup.cmake +++ /dev/null @@ -1,22 +0,0 @@ -macro(register_source_groups_from_filestructure list_of_files remove_prefix) - foreach(FILE ${list_of_files}) - get_filename_component(PARENT_DIR "${FILE}" PATH) - - # skip src or include and changes /'s to \\'s - string(REPLACE ${PROJECT_SOURCE_DIR} "" PARENT_DIR "${PARENT_DIR}") - string(REGEX REPLACE "(\\./)?(src|include)/?" "" GROUP "${PARENT_DIR}") - string(REGEX REPLACE "${remove_prefix}/?" "" GROUP "${GROUP}") - #string(REGEX REPLACE "/storm?/" "" GROUP ${GROUP}) - #STRING(SUBSTRING "${GROUP}" 1 -1 GROUP) - string(REPLACE "/" "\\" GROUP "${GROUP}") - - # group into "Source Files" and "Header Files" - # if ("${FILE}" MATCHES ".*\\.cpp") - # set(GROUP "Source Files\\${GROUP}") - # elseif("${FILE}" MATCHES ".*\\.h") - # set(GROUP "Header Files\\${GROUP}") - # endif() - - source_group("${GROUP}" FILES "${FILE}") - endforeach() -endmacro() \ No newline at end of file diff --git a/resources/cmake/macros/export.cmake b/resources/cmake/macros/export.cmake index ab919d7502..d8711798f1 100644 --- a/resources/cmake/macros/export.cmake +++ b/resources/cmake/macros/export.cmake @@ -1,15 +1,5 @@ -option(EXPORT_TO_CMAKE "Export the project to CMake for easy inclusion" ON) - # Add all targets to the build-tree export set -export(TARGETS ${STORM_TARGETS} FILE "${PROJECT_BINARY_DIR}/stormTargets.cmake") - -# Export the package for use from the build-tree -# (this registers the build-tree with a global CMake-registry) -if(EXPORT_TO_CMAKE) - message(STATUS "Registered with cmake") - set(CMAKE_EXPORT_PACKAGE_REGISTRY ON) - export(PACKAGE storm) -endif() +export(EXPORT storm_Targets FILE "${PROJECT_BINARY_DIR}/stormTargets.cmake") set(DEP_TARGETS "") foreach(dt ${STORM_DEP_TARGETS}) @@ -24,25 +14,20 @@ endforeach() include(CMakePackageConfigHelpers) write_basic_package_version_file(${CMAKE_CURRENT_BINARY_DIR}/stormConfigVersion.cmake - VERSION 0.1.0 - COMPATIBILITY SameMajorVersion ) + VERSION ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.${STORM_VERSION_TWEAK} + COMPATIBILITY SameMinorVersion ) + -# For the build tree -set(CONF_INCLUDE_DIRS "${CMAKE_BINARY_DIR}/include/") configure_package_config_file( resources/cmake/stormConfig.cmake.in ${PROJECT_BINARY_DIR}/stormConfig.cmake - INSTALL_DESTINATION ${CMAKE_INSTALL_DIR} - PATH_VARS INCLUDE_INSTALL_DIR + INSTALL_DESTINATION ${PROJECT_BINARY_DIR} + PATH_VARS PROJECT_BINARY_DIR ) - # For the install tree -file(RELATIVE_PATH REL_INCLUDE_DIR "${CMAKE_INSTALL_DIR}" "${INCLUDE_INSTALL_DIR}") -set(CONF_INCLUDE_DIRS "\${storm_CMAKE_DIR}/${REL_INCLUDE_DIR}/storm") - configure_package_config_file( - resources/cmake/stormConfig.cmake.in - ${PROJECT_BINARY_DIR}/stormConfig.install.cmake - INSTALL_DESTINATION ${CMAKE_INSTALL_DIR} - PATH_VARS INCLUDE_INSTALL_DIR + resources/cmake/stormConfig.cmake.install.in + ${PROJECT_BINARY_DIR}/stormConfig.cmake.install + INSTALL_DESTINATION ${STORM_CMAKE_INSTALL_DIR} + PATH_VARS STORM_INCLUDE_INSTALL_DIR ) diff --git a/resources/cmake/macros/imported.cmake b/resources/cmake/macros/imported.cmake index fb847eff60..30247cd58c 100644 --- a/resources/cmake/macros/imported.cmake +++ b/resources/cmake/macros/imported.cmake @@ -1,13 +1,20 @@ # copied from CARL -macro(add_imported_library_interface name include) +macro(storm_add_imported_library_interface name include install_include) add_library(${name} INTERFACE IMPORTED) - set_target_properties(${name} PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${include}") -endmacro(add_imported_library_interface) + if("${install_include}" STREQUAL "") + target_include_directories(${name} INTERFACE ${include}) + else() + target_include_directories(${name} INTERFACE + $ + $ + ) + endif() +endmacro(storm_add_imported_library_interface) macro(add_imported_library name type lib include) -# Workaround from https://cmake.org/Bug/view.php?id=15052 +# Workaround from https://gitlab.kitware.com/cmake/cmake/-/issues/15052 file(MAKE_DIRECTORY "${include}") if("${lib}" STREQUAL "") if("${type}" STREQUAL "SHARED") diff --git a/resources/cmake/stormConfig.cmake.in b/resources/cmake/stormConfig.cmake.in index e0d95e70ae..d2ddc2528e 100644 --- a/resources/cmake/stormConfig.cmake.in +++ b/resources/cmake/stormConfig.cmake.in @@ -1,21 +1,129 @@ -set(storm_VERSION @STORM_VERSION@) +include(CMakeFindDependencyMacro) -get_filename_component(storm_CMAKE_DIR "${CMAKE_CURRENT_LIST_FILE}" PATH) -include("@carl_CMAKE_DIR@/carlConfig.cmake") +@PACKAGE_INIT@ +@EXP_OPTIONS@ -@DEP_TARGETS@ -@EXP_OPTIONS@ +# Compute the installation prefix relative to this file. +get_filename_component(_IMPORT_PREFIX "${CMAKE_CURRENT_LIST_FILE}" PATH) +get_filename_component(_IMPORT_PREFIX "${_IMPORT_PREFIX}" PATH) +get_filename_component(_IMPORT_PREFIX "${_IMPORT_PREFIX}" PATH) +get_filename_component(_IMPORT_PREFIX "${_IMPORT_PREFIX}" PATH) +if(_IMPORT_PREFIX STREQUAL "/") + set(_IMPORT_PREFIX "") +endif() -# Our library dependencies (contains definitions for IMPORTED targets) -if(NOT TARGET storm) - include("${storm_CMAKE_DIR}/stormTargets.cmake") +include("${CMAKE_CURRENT_LIST_DIR}/_deps/carl-build/carlConfig.cmake") +if(NOT TARGET lib_carl) + message(FATAL_ERROR "Including _deps/carl-build/carlConfig.cmake did not define target lib_carl.") +endif() +set(storm_carl_DIR "_deps/carl-build") +include("${CMAKE_CURRENT_LIST_DIR}/_deps/sylvanfetch-build/src/cmake/sylvan-config.cmake") + +set(CMAKE_MODULE_PATH_save "${CMAKE_MODULE_PATH}") +# Note that this currently assumes that the sources are not moved away from the build tree. +list(INSERT CMAKE_MODULE_PATH 0 "@PROJECT_SOURCE_DIR@/resources/cmake/find_modules/") + +find_dependency(Boost QUIET NO_MODULE) +if(@STORM_HAVE_Z3@) + if(@STORM_Z3_CONFIG@) + find_dependency(Z3 4.8.7 NO_MODULE) + else() + find_dependency(Z3) + add_library(z3 SHARED IMPORTED) + set_target_properties( + z3 + PROPERTIES + IMPORTED_LOCATION ${Z3_LIBRARIES} + INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR} + ) + endif() +endif() +find_dependency(Threads) +if(@STORM_HAVE_GLPK@) + find_dependency(GLPK) + + add_library(glpk SHARED IMPORTED) + set_target_properties( + glpk + PROPERTIES + IMPORTED_LOCATION ${GLPK_LIBRARIES} + INTERFACE_INCLUDE_DIRECTORIES ${GLPK_INCLUDE_DIR} + ) +endif() + +if(@STORM_HAVE_XERCES@) # STORM_HAVE_XERCES + find_dependency(XercesC) +endif() +if(@STORM_HAVE_SOPLEX@) # STORM_HAVE_SOPLEX + find_dependency(soplex) +endif() +if(@STORM_HAVE_GUROBI@) # STORM_HAVE_GUROBI + find_dependency(GUROBI) + add_library(GUROBI UNKNOWN IMPORTED) + set_target_properties( + GUROBI + PROPERTIES + IMPORTED_LOCATION ${GUROBI_LIBRARY} + INTERFACE_INCLUDE_DIRECTORIES ${GUROBI_INCLUDE_DIRS} + ) +endif() + +add_library(cudd3 STATIC IMPORTED) +set_target_properties( + cudd3 + PROPERTIES + IMPORTED_LOCATION ${CMAKE_CURRENT_LIST_DIR}/resources/3rdparty/cudd-3.0.0/lib/libcudd@STATIC_EXT@ + INTERFACE_INCLUDE_DIRECTORIES ${CMAKE_CURRENT_LIST_DIR}/resources/3rdparty/cudd-3.0.0/include/ +) + +if(@STORM_HAVE_SPOT@) # STORM_HAVE_SPOT? + if(@STORM_SHIPPED_SPOT@) + add_library(Storm::Spot-bddx STATIC IMPORTED) + set_target_properties(Storm::Spot-bddx PROPERTIES + INTERFACE_INCLUDE_DIRECTORIES "${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/spot/" + IMPORTED_LOCATION ${STORM_RESOURCE_LIBRARY_INSTALL_DIR}/libbddx.0@DYNAMIC_EXT@ + ) + + add_library(Storm::Spot STATIC IMPORTED) + set_target_properties(Storm::Spot PROPERTIES + INTERFACE_INCLUDE_DIRECTORIES "${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/spot/" + IMPORTED_LOCATION ${STORM_RESOURCE_LIBRARY_INSTALL_DIR}/libspot.0@DYNAMIC_EXT@ + INTERFACE_LINK_LIBRARIES Storm::Spot-bddx + ) + else() + find_dependency(Spot) + add_library(Storm::Spot UNKNOWN IMPORTED) + set_target_properties( + Storm::Spot + PROPERTIES + IMPORTED_LOCATION ${Spot_LIBRARIES} + INTERFACE_INCLUDE_DIRECTORIES ${Spot_INCLUDE_DIR} + ) + + endif() endif() -@PACKAGE_INIT@ -set(storm_INCLUDE_DIR "@CONF_INCLUDE_DIRS@") +if(@STORM_HAVE_MATHSAT@) + set(MATHSAT_ROOT "@MATHSAT_ROOT@") + find_dependency(MATHSAT QUIET) + add_library(mathsat UNKNOWN IMPORTED) + set_target_properties( + mathsat + PROPERTIES + IMPORTED_LOCATION ${MATHSAT_LIBRARIES} + INTERFACE_INCLUDE_DIRECTORIES ${MATHSAT_INCLUDE_DIRS} + ) +endif() + + +set(CMAKE_MODULE_PATH "${CMAKE_MODULE_PATH_save}") +unset(CMAKE_MODULE_PATH_save) + +# Our library dependencies (contains definitions for IMPORTED targets) +if(NOT TARGET storm) + include("${CMAKE_CURRENT_LIST_DIR}/stormTargets.cmake") +endif() -set(storm_LIBRARIES storm) -check_required_components(storm) diff --git a/resources/cmake/stormConfig.cmake.install.in b/resources/cmake/stormConfig.cmake.install.in new file mode 100644 index 0000000000..64b249620c --- /dev/null +++ b/resources/cmake/stormConfig.cmake.install.in @@ -0,0 +1,131 @@ +include(CMakeFindDependencyMacro) + + +@PACKAGE_INIT@ +@EXP_OPTIONS@ + + +# Compute the installation prefix relative to this file. +get_filename_component(_IMPORT_PREFIX "${CMAKE_CURRENT_LIST_FILE}" PATH) +get_filename_component(_IMPORT_PREFIX "${_IMPORT_PREFIX}" PATH) +get_filename_component(_IMPORT_PREFIX "${_IMPORT_PREFIX}" PATH) +get_filename_component(_IMPORT_PREFIX "${_IMPORT_PREFIX}" PATH) +if(_IMPORT_PREFIX STREQUAL "/") + set(_IMPORT_PREFIX "") +endif() + +set(STORM_RESOURCE_INCLUDE_INSTALL_DIR "${_IMPORT_PREFIX}/@STORM_RESOURCE_INCLUDE_INSTALL_DIR@") +set(STORM_RESOURCE_LIBRARY_INSTALL_DIR "${_IMPORT_PREFIX}/@STORM_RESOURCE_LIBRARY_INSTALL_DIR@") + +include("${CMAKE_CURRENT_LIST_DIR}/carlConfig.cmake") +if(NOT TARGET lib_carl) + message(FATAL_ERROR "Including ${CMAKE_CURRENT_LIST_DIR}/carlConfig.cmake did not define target lib_carl.") +endif() +set(storm_carl_DIR "${CMAKE_CURRENT_LIST_DIR}") +include("${STORM_RESOURCE_LIBRARY_INSTALL_DIR}/sylvan/cmake/sylvan/sylvan-config.cmake") + +set(CMAKE_MODULE_PATH_save "${CMAKE_MODULE_PATH}") +list(INSERT CMAKE_MODULE_PATH 0 "${CMAKE_CURRENT_LIST_DIR}/find_modules/") + +find_dependency(Boost QUIET NO_MODULE) +if(@STORM_HAVE_Z3@) + if(@STORM_Z3_CONFIG@) + find_dependency(Z3 4.8.7 NO_MODULE) + else() + find_dependency(Z3) + add_library(z3 SHARED IMPORTED) + set_target_properties( + z3 + PROPERTIES + IMPORTED_LOCATION ${Z3_LIBRARIES} + INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR} + ) + endif() +endif() +find_dependency(Threads) +if(@STORM_HAVE_GLPK@) + find_dependency(GLPK) + + add_library(glpk SHARED IMPORTED) + set_target_properties( + glpk + PROPERTIES + IMPORTED_LOCATION ${GLPK_LIBRARIES} + INTERFACE_INCLUDE_DIRECTORIES ${GLPK_INCLUDE_DIR} + ) +endif() + +if(@STORM_HAVE_XERCES@) # STORM_HAVE_XERCES + find_dependency(XercesC) +endif() +if(@STORM_HAVE_SOPLEX@) # STORM_HAVE_SOPLEX + find_dependency(soplex) +endif() +if(@STORM_HAVE_GUROBI@) # STORM_HAVE_GUROBI + find_dependency(GUROBI) + add_library(GUROBI UNKNOWN IMPORTED) + set_target_properties( + GUROBI + PROPERTIES + IMPORTED_LOCATION ${GUROBI_LIBRARY} + INTERFACE_INCLUDE_DIRECTORIES ${GUROBI_INCLUDE_DIRS} + ) +endif() + +add_library(cudd3 STATIC IMPORTED) +set_target_properties( + cudd3 + PROPERTIES + IMPORTED_LOCATION ${STORM_RESOURCE_LIBRARY_INSTALL_DIR}/libcudd@STATIC_EXT@ + INTERFACE_INCLUDE_DIRECTORIES ${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/cudd/ +) + +if(@STORM_HAVE_SPOT@) # STORM_HAVE_SPOT? + if(@STORM_SHIPPED_SPOT@) + add_library(Storm::Spot-bddx STATIC IMPORTED) + set_target_properties(Storm::Spot-bddx PROPERTIES + INTERFACE_INCLUDE_DIRECTORIES "${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/spot/" + IMPORTED_LOCATION ${STORM_RESOURCE_LIBRARY_INSTALL_DIR}/libbddx.0@DYNAMIC_EXT@ + ) + + add_library(Storm::Spot STATIC IMPORTED) + set_target_properties(Storm::Spot PROPERTIES + INTERFACE_INCLUDE_DIRECTORIES "${STORM_RESOURCE_INCLUDE_INSTALL_DIR}/spot/" + IMPORTED_LOCATION ${STORM_RESOURCE_LIBRARY_INSTALL_DIR}/libspot.0@DYNAMIC_EXT@ + INTERFACE_LINK_LIBRARIES Storm::Spot-bddx + ) + else() + find_dependency(Spot) + add_library(Storm::Spot UNKNOWN IMPORTED) + set_target_properties( + Storm::Spot + PROPERTIES + IMPORTED_LOCATION ${Spot_LIBRARIES} + INTERFACE_INCLUDE_DIRECTORIES ${Spot_INCLUDE_DIR} + ) + + endif() +endif() + + +if(@STORM_HAVE_MATHSAT@) + set(MATHSAT_ROOT "@MATHSAT_ROOT@") + find_dependency(MATHSAT QUIET) + add_library(mathsat UNKNOWN IMPORTED) + set_target_properties( + mathsat + PROPERTIES + IMPORTED_LOCATION ${MATHSAT_LIBRARIES} + INTERFACE_INCLUDE_DIRECTORIES ${MATHSAT_INCLUDE_DIRS} + ) +endif() + + +set(CMAKE_MODULE_PATH "${CMAKE_MODULE_PATH_save}") +unset(CMAKE_MODULE_PATH_save) + +# Our library dependencies (contains definitions for IMPORTED targets) +if(NOT TARGET storm) + include("${CMAKE_CURRENT_LIST_DIR}/stormTargets.cmake") +endif() + diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 32ce46c25c..9bfcf2f4ac 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,7 +1,3 @@ -set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) -set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) -set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) - add_custom_target(binaries) add_subdirectory(storm) @@ -12,7 +8,6 @@ add_subdirectory(storm-parsers) add_subdirectory(storm-version-info) add_subdirectory(storm-cli-utilities) add_subdirectory(storm-cli) -# Additional libraries add_subdirectory(storm-conv) add_subdirectory(storm-conv-cli) add_subdirectory(storm-dft) diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt index 6f43e020a5..eba3308270 100644 --- a/src/storm-cli-utilities/CMakeLists.txt +++ b/src/storm-cli-utilities/CMakeLists.txt @@ -1,38 +1,25 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.h ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm-cli-utilities) - file(GLOB_RECURSE STORM_CLI_UTIL_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.cpp) -file(GLOB_RECURSE STORM_CLI_UTIL_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.h) +file(GLOB_RECURSE STORM_CLI_UTIL_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-cli-utilities" ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.h) # Create storm-cli-utilities. -add_library(storm-cli-utilities SHARED ${STORM_CLI_UTIL_SOURCES} ${STORM_CLI_UTIL_HEADERS}) +add_library(storm-cli-utilities SHARED) +target_sources(storm-cli-utilities + PRIVATE + ${STORM_CLI_UTIL_SOURCES} + PUBLIC + FILE_SET fs_storm_cli_utilities_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_CLI_UTIL_HEADERS}) target_precompile_headers(storm-cli-utilities REUSE_FROM storm) - -# Remove define symbol for shared libstorm. -set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "") +set_target_properties(storm-cli-utilities PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) +target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples storm-gamebased-ar storm-parsers storm-version-info) +set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. list(APPEND STORM_TARGETS storm-cli-utilities) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples storm-gamebased-ar storm-parsers storm-version-info) - -# Install storm headers to include directory. -foreach(HEADER ${STORM_CLI_UTIL_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_CLI_UTIL_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_cli_util_headers DEPENDS ${STORM_CLI_UTIL_OUTPUT_HEADERS} ${STORM_CLI_UTIL_HEADERS}) -add_dependencies(storm-cli-utilities copy_storm_cli_util_headers) - # installation -install(TARGETS storm-cli-utilities EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-cli-utilities EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_cli_utilities_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index 56f15af203..99ca18ffab 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -28,19 +28,22 @@ bool parseOptions(const int argc, const char* argv[]) { } storm::settings::modules::GeneralSettings const& general = storm::settings::getModule(); - - bool result = true; + bool terminate = false; if (general.isHelpSet()) { - storm::settings::manager().printHelp(storm::settings::getModule().getHelpFilterExpression()); - result = false; + storm::settings::manager().printHelp(general.getHelpFilterExpression()); + terminate = true; } if (general.isVersionSet()) { - printVersion(); - result = false; + storm::cli::printVersion(); + terminate = true; + } + if (terminate) { + exit(0); // Terminate after help and version output with success. + // TODO: Issue 674 discusses that this may not be ideal. } - return result; + return true; } void setResourceLimits() { diff --git a/src/storm-cli-utilities/print.cpp b/src/storm-cli-utilities/print.cpp index d802caed22..8558c7dd4c 100644 --- a/src/storm-cli-utilities/print.cpp +++ b/src/storm-cli-utilities/print.cpp @@ -1,4 +1,4 @@ -#include "print.h" +#include "storm-cli-utilities/print.h" #include "storm-version-info/storm-version.h" #include "storm/utility/cli.h" @@ -16,7 +16,7 @@ #ifdef STORM_HAVE_GUROBI #include "gurobi_c.h" #endif -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT #include "mathsat.h" #endif #ifdef STORM_HAVE_SOPLEX @@ -98,35 +98,38 @@ void printVersion() { #endif // Print linked dependencies -#ifdef STORM_HAVE_CARL STORM_PRINT("Linked with CArL v" << STORM_CARL_VERSION << ".\n"); -#endif #ifdef STORM_HAVE_GLPK STORM_PRINT("Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << ".\n"); +#else + STORM_PRINT("Not linked with GLPK.\n"); #endif #ifdef STORM_HAVE_GUROBI STORM_PRINT("Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << ".\n"); +#else + STORM_PRINT("Not linked with Gurobi.\n"); #endif -#ifdef STORM_HAVE_INTELTBB - STORM_PRINT("Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " - << TBB_INTERFACE_VERSION << ").\n"); -#endif -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT char* msatVersion = msat_get_version(); STORM_PRINT("Linked with " << msatVersion << ".\n"); msat_free(msatVersion); +#else + STORM_PRINT("Not linked with MathSat.\n"); #endif #ifdef STORM_HAVE_SOPLEX STORM_PRINT("Linked with Soplex v" << SOPLEX_VERSION << ".\n"); -#endif -#ifdef STORM_HAVE_SMTRAT - STORM_PRINT("Linked with SMT-RAT v" << SMTRAT_VERSION << ".\n"); +#else + STORM_PRINT("Not linked with Soplex.\n"); #endif #ifdef STORM_HAVE_SPOT STORM_PRINT("Linked with Spot v" << spot::version() << ".\n"); +#else + STORM_PRINT("Not linked with Spot.\n"); #endif #ifdef STORM_HAVE_XERCES STORM_PRINT("Linked with Xerces-C v" << gXercesMajVersion << "." << gXercesMinVersion << "." << gXercesRevision << ".\n"); +#else + STORM_PRINT("Not linked with Xerces-C.\n"); #endif #ifdef STORM_HAVE_Z3 unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; @@ -137,7 +140,10 @@ void printVersion() { #else STORM_PRINT("Linked with Z3 Theorem Prover v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << ".\n"); #endif +#else + STORM_PRINT("Not linked with Z3 Theorem Prover\n"); #endif + STORM_PRINT("[...]\n"); } void printTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) { diff --git a/src/storm-cli/CMakeLists.txt b/src/storm-cli/CMakeLists.txt index 54e870fef0..21a828f383 100644 --- a/src/storm-cli/CMakeLists.txt +++ b/src/storm-cli/CMakeLists.txt @@ -2,9 +2,11 @@ add_executable(storm-cli ${PROJECT_SOURCE_DIR}/src/storm-cli/storm-cli.cpp) target_link_libraries(storm-cli storm storm-cli-utilities) set_target_properties(storm-cli PROPERTIES OUTPUT_NAME "storm") +set_target_properties(storm-cli PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) target_precompile_headers(storm-cli PRIVATE ${STORM_PRECOMPILED_HEADERS}) add_dependencies(binaries storm-cli) # installation -install(TARGETS storm-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-cli EXPORT storm_Targets + RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-config.h.in b/src/storm-config.h.in index 5245fd709d..7d6299cc5b 100644 --- a/src/storm-config.h.in +++ b/src/storm-config.h.in @@ -1,107 +1,91 @@ /* - * StoRM - Build-in Options + * Storm - Build Options * - * This file is parsed by CMake during makefile generation - * It contains information such as the base path to the test/example data + * This file is parsed by CMake during Makefile generation + * It contains build and configuration information */ -#ifndef STORM_GENERATED_STORMCONFIG_H_ -#define STORM_GENERATED_STORMCONFIG_H_ +#pragma once + +// Directories +// ########### // The directory of the sources from which Storm was built. #define STORM_SOURCE_DIR "@PROJECT_SOURCE_DIR@" - +// The directory in which Storm was built. +#define STORM_BUILD_DIR "@PROJECT_BINARY_DIR@" // The directory of the test resources used in the tests (model files, ...). #define STORM_TEST_RESOURCES_DIR "@STORM_TEST_RESOURCES_DIR@" - -// The directory in which Storm was built. -#define STORM_BUILD_DIR "@CMAKE_BINARY_DIR@" - -// Boost include directory used during compilation. -#define STORM_BOOST_INCLUDE_DIR "@STORM_BOOST_INCLUDE_DIR@" - // Carl include directory used during compilation. #define STORM_CARL_INCLUDE_DIR "@carl_INCLUDE_DIR@" -// Whether Gurobi is available and to be used (define/undef) -#cmakedefine STORM_HAVE_GUROBI - -// Whether GLPK is available and to be used (define/undef) -#cmakedefine STORM_HAVE_GLPK - -// Whether Z3 is available and to be used (define/undef) -#cmakedefine STORM_HAVE_Z3 - -// Whether the optimization feature of Z3 is available and to be used (define/undef) -#cmakedefine STORM_HAVE_Z3_OPTIMIZE - -// Version of Z3 used by Storm. -#define STORM_Z3_VERSION_MAJOR @STORM_Z3_VERSION_MAJOR@ -#define STORM_Z3_VERSION_MINOR @STORM_Z3_VERSION_MINOR@ -#define STORM_Z3_VERSION_PATCH @STORM_Z3_VERSION_PATCH@ -#define STORM_Z3_VERSION @Z3_VERSION@ -#cmakedefine STORM_Z3_API_USES_STANDARD_INTEGERS - -// Whether MathSAT is available and to be used (define/undef) -#cmakedefine STORM_HAVE_MSAT - -// Whether SoPlex is available and to be used -#cmakedefine STORM_HAVE_SOPLEX +// Storm configuration options +// ########################### // Whether benchmarks from QVBS can be used as input #cmakedefine STORM_HAVE_QVBS - // The root directory of QVBS #cmakedefine STORM_QVBS_ROOT "@STORM_QVBS_ROOT@" +// Logging configuration +#cmakedefine STORM_LOGGING_FRAMEWORK +#cmakedefine STORM_LOG_DISABLE_DEBUG -// Whether Intel Threading Building Blocks are available and to be used (define/undef) -#cmakedefine STORM_HAVE_INTELTBB - -// Whether support for parametric systems should be enabled -#cmakedefine PARAMETRIC_SYSTEMS -// Whether CLN is available and to be used (define/undef) -#cmakedefine STORM_HAVE_CLN +// Carl configuration +// ################### +// Whether carl is available and to be used +#cmakedefine STORM_HAVE_CARL +// Whether carl has headers for forward declarations +#cmakedefine STORM_CARL_SUPPORTS_FWD_DECL +// Version of CARL used by Storm. +#define STORM_CARL_VERSION_MAJOR @carl_VERSION_MAJOR@ +#define STORM_CARL_VERSION_MINOR @carl_VERSION_MINOR@ +#define STORM_CARL_VERSION @carl_VERSION@ -// Include directory for CLN headers -#cmakedefine CLN_INCLUDE_DIR "@CLN_INCLUDE_DIR@" +// GMP +// ### // Whether GMP is available (it is always available nowadays) #define STORM_HAVE_GMP - // Include directory for GMP headers #cmakedefine GMP_INCLUDE_DIR "@GMP_INCLUDE_DIR@" #cmakedefine GMPXX_INCLUDE_DIR "@GMPXX_INCLUDE_DIR@" -// Whether carl is available and to be used. -#cmakedefine STORM_HAVE_CARL -// Whether carl has headers for forward declarations -#cmakedefine STORM_CARL_SUPPORTS_FWD_DECL -// Version of CARL used by Storm. -#define STORM_CARL_VERSION_MAJOR @carl_VERSION_MAJOR@ -#define STORM_CARL_VERSION_MINOR @carl_VERSION_MINOR@ -#define STORM_CARL_VERSION @carl_VERSION@ -#cmakedefine STORM_Z3_API_USES_STANDARD_INTEGERS +// CLN +// ### +// Whether CLN is available and to be used +#cmakedefine STORM_HAVE_CLN +// Whether Storm uses CLN for rationals and rational functions #cmakedefine STORM_USE_CLN_EA - #cmakedefine STORM_USE_CLN_RF -#cmakedefine STORM_HAVE_XERCES -// Whether Spot is available and to be used -#cmakedefine STORM_HAVE_SPOT +// Z3 configuration +// ################ +// Whether Z3 is available and to be used +#cmakedefine STORM_HAVE_Z3 +// Whether the optimization feature of Z3 is available and to be used +#cmakedefine STORM_HAVE_Z3_OPTIMIZE +// Whether Z3 uses standard integers +#cmakedefine STORM_Z3_API_USES_STANDARD_INTEGERS +// Version of Z3 used by Storm. +#define STORM_Z3_VERSION @Z3_VERSION@ + +// Dependencies +// ############ +// Whether the libraries are available and to be used +#cmakedefine STORM_HAVE_GLPK +#cmakedefine STORM_HAVE_GUROBI +#cmakedefine STORM_HAVE_MATHSAT +#cmakedefine STORM_HAVE_SOPLEX +#cmakedefine STORM_HAVE_SPOT +#cmakedefine STORM_HAVE_XERCES +#cmakedefine STORM_HAVE_LP_SOLVER +// Whether Intel Threading Building Blocks are available and to be used +#cmakedefine STORM_HAVE_INTELTBB // Whether LTL model checking shall be enabled #ifdef STORM_HAVE_SPOT - #define STORM_HAVE_LTL_MODELCHECKING_SUPPORT -#endif // STORM_HAVE_SPOT - -// Whether smtrat is available and to be used. -#cmakedefine STORM_HAVE_SMTRAT - -#cmakedefine STORM_LOGGING_FRAMEWORK - -#cmakedefine STORM_LOG_DISABLE_DEBUG - -#endif // STORM_GENERATED_STORMCONFIG_H_ + #define STORM_HAVE_LTL_MODELCHECKING_SUPPORT +#endif // STORM_HAVE_SPOT \ No newline at end of file diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp index 62955867f1..78c35d333f 100644 --- a/src/storm-conv-cli/storm-conv.cpp +++ b/src/storm-conv-cli/storm-conv.cpp @@ -326,18 +326,22 @@ bool parseOptions(const int argc, const char* argv[]) { storm::settings::mutableManager().setFromConfigurationFile(general.getConfigFilename()); } - bool result = true; + bool terminate = false; if (general.isHelpSet()) { storm::settings::manager().printHelp(general.getHelpFilterExpression()); - result = false; + terminate = true; } if (general.isVersionSet()) { storm::cli::printVersion(); - result = false; + terminate = true; + } + if (terminate) { + exit(0); // Terminate after help and version output with success. + // TODO: Issue 674 discusses that this may not be ideal. } - return result; + return true; } /*! diff --git a/src/storm-conv/CMakeLists.txt b/src/storm-conv/CMakeLists.txt index d39af1a331..05d5a98901 100644 --- a/src/storm-conv/CMakeLists.txt +++ b/src/storm-conv/CMakeLists.txt @@ -1,38 +1,25 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-conv/*.h ${PROJECT_SOURCE_DIR}/src/storm-conv/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm-conv) - file(GLOB_RECURSE STORM_CONV_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-conv/*/*.cpp) -file(GLOB_RECURSE STORM_CONV_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-conv/*/*.h) - +file(GLOB_RECURSE STORM_CONV_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-conv" ${PROJECT_SOURCE_DIR}/src/storm-conv/*/*.h) # Create storm-conv. -add_library(storm-conv SHARED ${STORM_CONV_SOURCES} ${STORM_CONV_HEADERS}) +add_library(storm-conv SHARED) +target_sources(storm-conv + PRIVATE + ${STORM_CONV_SOURCES} + PUBLIC + FILE_SET fs_storm_conv_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_CONV_HEADERS}) target_precompile_headers(storm-conv REUSE_FROM storm) +set_target_properties(storm-conv PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) +target_link_libraries(storm-conv PUBLIC storm) +set_target_properties(storm-conv PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. -# Remove define symbol for shared libstorm. -set_target_properties(storm-conv PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-conv) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-conv PUBLIC storm ${STORM_CONV_LINK_LIBRARIES}) - -# Install storm headers to include directory. -foreach(HEADER ${STORM_CONV_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_CONV_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_conv_headers DEPENDS ${STORM_CONV_OUTPUT_HEADERS} ${STORM_CONV_HEADERS}) -add_dependencies(storm-conv copy_storm_conv_headers) # installation -install(TARGETS storm-conv EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) - +install(TARGETS storm-conv EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_conv_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm-counterexamples/CMakeLists.txt b/src/storm-counterexamples/CMakeLists.txt index d86e5d1b92..a07c4aa316 100644 --- a/src/storm-counterexamples/CMakeLists.txt +++ b/src/storm-counterexamples/CMakeLists.txt @@ -1,38 +1,25 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm-counterexamples) - file(GLOB_RECURSE STORM_CEX_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.cpp) -file(GLOB_RECURSE STORM_CEX_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.h) +file(GLOB_RECURSE STORM_CEX_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-counterexamples" ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.h) - -# Create storm-counterexamples. add_library(storm-counterexamples SHARED ${STORM_CEX_SOURCES} ${STORM_CEX_HEADERS}) +target_sources(storm-counterexamples + PRIVATE + ${STORM_CEX_SOURCES} + PUBLIC + FILE_SET fs_storm_cex_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_CEX_HEADERS}) target_precompile_headers(storm-counterexamples REUSE_FROM storm) +set_target_properties(storm-counterexamples PROPERTIES + VERSION ${STORM_VERSION} + SOVERSION ${STORM_VERSION}) +target_link_libraries(storm-counterexamples PUBLIC storm) +set_target_properties(storm-counterexamples PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. -# Remove define symbol for shared libstorm. -set_target_properties(storm-counterexamples PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-counterexamples) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-counterexamples PUBLIC storm) - -# Install storm headers to include directory. -foreach(HEADER ${STORM_CEX_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_CEX_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_cex_headers DEPENDS ${STORM_CEX_OUTPUT_HEADERS} ${STORM_CEX_HEADERS}) -add_dependencies(storm-counterexamples copy_storm_cex_headers) - # installation -install(TARGETS storm-counterexamples EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) - +install(TARGETS storm-counterexamples EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_cex_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index 4c01771dff..b3e6ce4b3c 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -1,38 +1,24 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-dft/*.h ${PROJECT_SOURCE_DIR}/src/storm-dft/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm-dft) - file(GLOB_RECURSE STORM_DFT_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.cpp) -file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h) - +file(GLOB_RECURSE STORM_DFT_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-dft" ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h) # Create storm-dft. -add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS}) +add_library(storm-dft SHARED) +target_sources(storm-dft + PRIVATE + ${STORM_DFT_SOURCES} + PUBLIC + FILE_SET fs_storm_dft_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_DFT_HEADERS}) target_precompile_headers(storm-dft REUSE_FROM storm) +set_target_properties(storm-dft PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) +target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-conv storm-parsers storm-pars ${STORM_DFT_LINK_LIBRARIES}) +set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. -# Remove define symbol for shared libstorm. -set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-dft) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-conv storm-parsers storm-pars ${STORM_DFT_LINK_LIBRARIES}) - -# Install storm headers to include directory. -foreach(HEADER ${STORM_DFT_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_DFT_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_dft_headers DEPENDS ${STORM_DFT_OUTPUT_HEADERS} ${STORM_DFT_HEADERS}) -add_dependencies(storm-dft copy_storm_dft_headers) - # installation -install(TARGETS storm-dft EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) - +install(TARGETS storm-dft EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_dft_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm-gamebased-ar/CMakeLists.txt b/src/storm-gamebased-ar/CMakeLists.txt index f1809e592c..fa87ccf25f 100644 --- a/src/storm-gamebased-ar/CMakeLists.txt +++ b/src/storm-gamebased-ar/CMakeLists.txt @@ -1,38 +1,23 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*.h ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm-gamebased-ar) - file(GLOB_RECURSE STORM_GBAR_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*/*.cpp) -file(GLOB_RECURSE STORM_GBAR_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*/*.h) - - -# Create storm-gamebased-ar. -add_library(storm-gamebased-ar SHARED ${STORM_GBAR_SOURCES} ${STORM_GBAR_HEADERS}) +file(GLOB_RECURSE STORM_GBAR_HEADERS RELATIVE " ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar" ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*/*.h) + +add_library(storm-gamebased-ar SHARED) +target_sources(storm-gamebased-ar + PRIVATE + ${STORM_GBAR_SOURCES} + PUBLIC + FILE_SET fs_storm_gbar_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_GBAR_HEADERS}) target_precompile_headers(storm-gamebased-ar REUSE_FROM storm) +set_target_properties(storm-gamebased-ar PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) +target_link_libraries(storm-gamebased-ar PUBLIC storm) +set_target_properties(storm-gamebased-ar PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux.a -# Remove define symbol for shared libstorm. -set_target_properties(storm-gamebased-ar PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-gamebased-ar) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-gamebased-ar PUBLIC storm) - -# Install storm headers to include directory. -foreach (HEADER ${STORM_GBAR_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_GBAR_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_gbar_headers DEPENDS ${STORM_GBAR_OUTPUT_HEADERS} ${STORM_GBAR_HEADERS}) -add_dependencies(storm-gamebased-ar copy_storm_gbar_headers) - # installation -install(TARGETS storm-gamebased-ar EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) - +install(TARGETS storm-gamebased-ar EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_gbar_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm-gspn/CMakeLists.txt b/src/storm-gspn/CMakeLists.txt index 0b61ef9cb1..086b5e217d 100644 --- a/src/storm-gspn/CMakeLists.txt +++ b/src/storm-gspn/CMakeLists.txt @@ -1,38 +1,24 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-gspn/*.h ${PROJECT_SOURCE_DIR}/src/storm-gspn/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm-gspn) - file(GLOB_RECURSE STORM_GSPN_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.cpp) -file(GLOB_RECURSE STORM_GSPN_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.h) - - -# Create storm-gspn. -add_library(storm-gspn SHARED ${STORM_GSPN_SOURCES} ${STORM_GSPN_HEADERS}) +file(GLOB_RECURSE STORM_GSPN_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-gspn" ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.h) + +add_library(storm-gspn SHARED) +target_sources(storm-gspn + PRIVATE + ${STORM_GSPN_SOURCES} + PUBLIC + FILE_SET fs_storm_gspn_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_GSPN_HEADERS}) target_precompile_headers(storm-gspn REUSE_FROM storm) +set_target_properties(storm-gspn PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) +target_link_libraries(storm-gspn PUBLIC storm storm-conv storm-parsers ${STORM_GSPN_LINK_LIBRARIES}) +set_target_properties(storm-gspn PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. # Remove define symbol for shared libstorm. -set_target_properties(storm-gspn PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-gspn) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-gspn PUBLIC storm storm-conv storm-parsers ${STORM_GSPN_LINK_LIBRARIES}) - -# Install storm headers to include directory. -foreach(HEADER ${STORM_GSPN_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_GSPN_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_gspn_headers DEPENDS ${STORM_GSPN_OUTPUT_HEADERS} ${STORM_GSPN_HEADERS}) -add_dependencies(storm-gspn copy_storm_gspn_headers) - # installation -install(TARGETS storm-gspn EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) - +install(TARGETS storm-gspn EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_gspn_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm-pars/CMakeLists.txt b/src/storm-pars/CMakeLists.txt index 8dca2969b6..5ceba61162 100644 --- a/src/storm-pars/CMakeLists.txt +++ b/src/storm-pars/CMakeLists.txt @@ -1,38 +1,25 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-pars/*.h ${PROJECT_SOURCE_DIR}/src/storm-pars/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm-pars) - file(GLOB_RECURSE STORM_PARS_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-pars/*/*.cpp) -file(GLOB_RECURSE STORM_PARS_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pars/*/*.h) - +file(GLOB_RECURSE STORM_PARS_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-pars" ${PROJECT_SOURCE_DIR}/src/storm-pars/*/*.h) # Create storm-pars. -add_library(storm-pars SHARED ${STORM_PARS_SOURCES} ${STORM_PARS_HEADERS}) +add_library(storm-pars SHARED) +target_sources(storm-pars + PRIVATE + ${STORM_PARS_SOURCES} + PUBLIC + FILE_SET fs_storm_pars_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_PARS_HEADERS}) target_precompile_headers(storm-pars REUSE_FROM storm) +set_target_properties(storm-pars PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) +set_target_properties(storm-pars PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. +target_link_libraries(storm-pars PUBLIC storm) + -# Remove define symbol for shared libstorm. -set_target_properties(storm-pars PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-pars) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-pars PUBLIC storm ${STORM_PARS_LINK_LIBRARIES}) - -# Install storm headers to include directory. -foreach(HEADER ${STORM_PARS_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_PARS_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_pars_headers DEPENDS ${STORM_PARS_OUTPUT_HEADERS} ${STORM_PARS_HEADERS}) -add_dependencies(storm-pars copy_storm_pars_headers) - # installation -install(TARGETS storm-pars EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) - +install(TARGETS storm-pars EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_pars_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm-parsers/CMakeLists.txt b/src/storm-parsers/CMakeLists.txt index 3832c90d7e..8564131b35 100644 --- a/src/storm-parsers/CMakeLists.txt +++ b/src/storm-parsers/CMakeLists.txt @@ -1,41 +1,27 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-parsers/*.h ${PROJECT_SOURCE_DIR}/src/storm-parsers/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm-parsers) - file(GLOB_RECURSE STORM_PARSER_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-parsers/*/*.cpp) -file(GLOB_RECURSE STORM_PARSER_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-parsers/*/*.h) - +file(GLOB_RECURSE STORM_PARSER_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-parsers" ${PROJECT_SOURCE_DIR}/src/storm-parsers/*/*.h) # Disable Debug compiler flags for PrismParser to lessen memory consumption during compilation SET_SOURCE_FILES_PROPERTIES(${PROJECT_SOURCE_DIR}/src/storm-parsers/parser/PrismParser.cpp PROPERTIES COMPILE_FLAGS -g0) # Create storm-parsers. -add_library(storm-parsers SHARED ${STORM_PARSER_SOURCES} ${STORM_PARSER_HEADERS}) +add_library(storm-parsers SHARED) +target_sources(storm-parsers + PRIVATE + ${STORM_PARSER_SOURCES} + PUBLIC + FILE_SET fs_storm_parsers_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_PARSER_HEADERS}) target_precompile_headers(storm-parsers REUSE_FROM storm) +set_target_properties(storm-parsers PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) +set_target_properties(storm-parsers PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. +target_link_libraries(storm-parsers PUBLIC storm) -# Remove define symbol for shared libstorm. -set_target_properties(storm-parsers PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-parsers) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-parsers PUBLIC storm) - -# Install storm headers to include directory. -foreach(HEADER ${STORM_PARSER_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_PARSER_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_parser_headers DEPENDS ${STORM_PARSER_OUTPUT_HEADERS} ${STORM_PARSER_HEADERS}) -add_dependencies(storm-parsers copy_storm_parser_headers) - # installation -install(TARGETS storm-parsers EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) - +install(TARGETS storm-parsers EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_parsers_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm-permissive/CMakeLists.txt b/src/storm-permissive/CMakeLists.txt index 7a25c23ff7..1b5138ce8b 100644 --- a/src/storm-permissive/CMakeLists.txt +++ b/src/storm-permissive/CMakeLists.txt @@ -1,38 +1,24 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-permissive/*.h ${PROJECT_SOURCE_DIR}/src/storm-permissive/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm-permissive) - file(GLOB_RECURSE STORM_PERMISSIVE_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-permissive/*/*.cpp) -file(GLOB_RECURSE STORM_PERMISSIVE_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-permissive/*/*.h) - +file(GLOB_RECURSE STORM_PERMISSIVE_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-permissive" ${PROJECT_SOURCE_DIR}/src/storm-permissive/*/*.h) # Create storm-permissive. -add_library(storm-permissive SHARED ${STORM_PERMISSIVE_SOURCES} ${STORM_PERMISSIVE_HEADERS}) +add_library(storm-permissive SHARED) +target_sources(storm-permissive + PRIVATE + ${STORM_PERMISSIVE_SOURCES} + PUBLIC + FILE_SET fs_storm_permissive_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_PERMISSIVE_HEADERS}) target_precompile_headers(storm-permissive REUSE_FROM storm) +set_target_properties(storm-permissive PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) +set_target_properties(storm-permissive PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. +target_link_libraries(storm-permissive PUBLIC storm) -# Remove define symbol for shared libstorm. -set_target_properties(storm-permissive PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-permissive) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-permissive PUBLIC storm) - -# Install storm headers to include directory. -foreach (HEADER ${STORM_PERMISSIVE_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_PERMISSIVE_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_permissive_headers DEPENDS ${STORM_PERMISSIVE_OUTPUT_HEADERS} ${STORM_PERMISSIVE_HEADERS}) -add_dependencies(storm-permissive copy_storm_permissive_headers) - # installation -install(TARGETS storm-permissive EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) - +install(TARGETS storm-permissive EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_permissive_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm-pomdp/CMakeLists.txt b/src/storm-pomdp/CMakeLists.txt index 2a9b8cdfe6..019585a307 100644 --- a/src/storm-pomdp/CMakeLists.txt +++ b/src/storm-pomdp/CMakeLists.txt @@ -1,38 +1,24 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*.h ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm-pomdp) - file(GLOB_RECURSE STORM_POMDP_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*/*.cpp) -file(GLOB_RECURSE STORM_POMDP_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*/*.h) - +file(GLOB_RECURSE STORM_POMDP_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-pomdp" ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*/*.h) # Create storm-pomdp. -add_library(storm-pomdp SHARED ${STORM_POMDP_SOURCES} ${STORM_POMDP_HEADERS}) +add_library(storm-pomdp SHARED) +target_sources(storm-pomdp + PRIVATE + ${STORM_POMDP_SOURCES} + PUBLIC + FILE_SET fs_storm_pomdp_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_POMDP_HEADERS}) target_precompile_headers(storm-pomdp REUSE_FROM storm) +set_target_properties(storm-pomdp PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) +set_target_properties(storm-pomdp PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. +target_link_libraries(storm-pomdp PUBLIC storm storm-parsers storm-pars) -# Remove define symbol for shared libstorm. -set_target_properties(storm-pomdp PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-pomdp) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-pomdp PUBLIC storm storm-parsers storm-pars ${STORM_POMDP_LINK_LIBRARIES}) - -# Install storm headers to include directory. -foreach(HEADER ${STORM_POMDP_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_POMDP_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_pomdp_headers DEPENDS ${STORM_POMDP_OUTPUT_HEADERS} ${STORM_POMDP_HEADERS}) -add_dependencies(storm-pomdp copy_storm_pomdp_headers) - # installation -install(TARGETS storm-pomdp RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) - +install(TARGETS storm-pomdp EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_pomdp_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm-version-info/CMakeLists.txt b/src/storm-version-info/CMakeLists.txt index 272c176e35..8b916b29c2 100644 --- a/src/storm-version-info/CMakeLists.txt +++ b/src/storm-version-info/CMakeLists.txt @@ -1,9 +1,5 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-version-info/*.h ${PROJECT_SOURCE_DIR}/src/storm-version-info/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm-version-info) - file(GLOB_RECURSE STORM_VERSION_INFO_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-version-info/*.cpp) -file(GLOB_RECURSE STORM_VERSION_INFO_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-version-info/*.h) +file(GLOB_RECURSE STORM_VERSION_INFO_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-version-info" ${PROJECT_SOURCE_DIR}/src/storm-version-info/*.h) # Configure a source file to pass the Storm version to the source code configure_file ( @@ -14,33 +10,27 @@ configure_file ( # Add the generated source file list(APPEND STORM_VERSION_INFO_SOURCES "${PROJECT_BINARY_DIR}/storm-version.cpp") - # Create storm-version-info lib -add_library(storm-version-info SHARED ${STORM_VERSION_INFO_SOURCES} ${STORM_VERSION_INFO_HEADERS}) - -# Remove define symbol for shared libstorm. -set_target_properties(storm-version-info PROPERTIES DEFINE_SYMBOL "") -# Add dependency to core storm libary. We are not going to link against it to avoid unnecessary linking steps, but we still want to build storm-version-info as often as possible. +add_library(storm-version-info SHARED) +target_sources(storm-version-info + PRIVATE + ${STORM_VERSION_INFO_SOURCES} + PUBLIC + FILE_SET fs_storm_version_info_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_VERSION_INFO_HEADERS}) +set_target_properties(storm-version-info PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) + +# Add dependency to core storm libary. +# We are not going to link against it to avoid unnecessary linking steps, +# but we still want to build storm-version-info as often as possible. add_dependencies(storm storm-version-info) + list(APPEND STORM_TARGETS storm-version-info) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -# Install storm headers to include directory. -foreach(HEADER ${STORM_VERSION_INFO_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_VERSION_INFO_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_version_info_headers DEPENDS ${STORM_VERSION_INFO_OUTPUT_HEADERS} ${STORM_VERSION_INFO_HEADERS}) -add_dependencies(storm-version-info copy_storm_version_info_headers) - # installation -install(TARGETS storm-version-info EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-version-info EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_version_info_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm-version-info/storm-version.cpp.in b/src/storm-version-info/storm-version.cpp.in index c63deab0f0..79c7896563 100644 --- a/src/storm-version-info/storm-version.cpp.in +++ b/src/storm-version-info/storm-version.cpp.in @@ -16,9 +16,9 @@ namespace storm { const std::string StormVersion::systemVersion = "@CMAKE_SYSTEM_VERSION@"; const std::string StormVersion::cxxCompiler = "@STORM_COMPILER_ID@ @CMAKE_CXX_COMPILER_VERSION@"; #ifdef NDEBUG - const std::string StormVersion::cxxFlags = "@CMAKE_CXX_FLAGS@" " " "@CMAKE_CXX_FLAGS_RELEASE@"; + const std::string StormVersion::cxxFlags = "compiled with NDEBUG"; #else - const std::string StormVersion::cxxFlags = "@CMAKE_CXX_FLAGS@" " " "@CMAKE_CXX_FLAGS_DEBUG@"; + const std::string StormVersion::cxxFlags = "compiled without NDEBUG"; #endif } diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 0775be6e10..62eb4671e9 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -1,69 +1,38 @@ -file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm/*.h ${PROJECT_SOURCE_DIR}/src/storm/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" storm) - ############################################################# ## ## Source file aggregation and clustering ## ############################################################# file(GLOB_RECURSE STORM_SOURCES ${PROJECT_SOURCE_DIR}/src/storm/*/*.cpp) -file(GLOB_RECURSE STORM_HEADERS ${PROJECT_SOURCE_DIR}/src/storm/*.h) +file(GLOB_RECURSE STORM_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm" ${PROJECT_SOURCE_DIR}/src/storm/*.h ) # Additional include files like the storm-config.h -file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h) - -# Add custom additional include or link directories -if (ADDITIONAL_INCLUDE_DIRS) - message(STATUS "Storm - Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}") - include_directories(${ADDITIONAL_INCLUDE_DIRS}) -endif(ADDITIONAL_INCLUDE_DIRS) -if (ADDITIONAL_LINK_DIRS) - message(STATUS "Storm - Using additional link directories ${ADDITIONAL_LINK_DIRS}") - link_directories(${ADDITIONAL_LINK_DIRS}) -endif(ADDITIONAL_LINK_DIRS) - +file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/storm-config.h) ############################################################################### ## -## Binary creation (All link_directories() calls must be made before this point.) +## Binary creation ## ############################################################################### - # Create libstorm. -add_library(storm SHARED ${STORM_3RDPARTY_SOURCES} ${STORM_SOURCES} ${STORM_HEADERS}) +add_library(storm SHARED) +target_sources(storm PRIVATE ${STORM_SOURCES}) +target_sources(storm PUBLIC FILE_SET fs_storm_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_HEADERS}) +target_sources(storm PUBLIC FILE_SET fs_storm_configured_headers TYPE HEADERS BASE_DIRS "${PROJECT_BINARY_DIR}/include" FILES ${STORM_BUILD_HEADERS}) target_precompile_headers(storm PRIVATE ${STORM_PRECOMPILED_HEADERS}) -# Remove define symbol for shared libstorm. -set_target_properties(storm PROPERTIES DEFINE_SYMBOL "") -add_dependencies(storm resources) +set_target_properties(storm PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION}) +set_target_properties(storm PROPERTIES DEFINE_SYMBOL "") # to avoid problems with pch on linux. +add_dependencies(storm storm_resources) #The library that needs symbols must be first, then the library that resolves the symbol. -target_link_libraries(storm PUBLIC ${STORM_DEP_TARGETS} ${STORM_DEP_IMP_TARGETS} ${STORM_LINK_LIBRARIES}) -#target_include_directories(storm PUBLIC "$$") -target_include_directories(storm PUBLIC "$$") -target_include_directories(storm PUBLIC "$$") # the interface loc is not right -# Add base folder for better inclusion paths +target_link_libraries(storm PUBLIC ${STORM_DEP_TARGETS} ${STORM_DEP_IMP_TARGETS} ${STORM_FETCHED_TARGETS}) list(APPEND STORM_TARGETS storm) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -# Install storm headers to include directory. -foreach(HEADER ${STORM_HEADERS}) - string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) - string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) - string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) - add_custom_command( - OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} - COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} - DEPENDS ${HEADER} - ) - list(APPEND STORM_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") -endforeach() -add_custom_target(copy_storm_headers DEPENDS ${STORM_OUTPUT_HEADERS} ${STORM_HEADERS}) -add_dependencies(storm copy_storm_headers) -add_dependencies(storm copy_resources_headers) - - # installation -install(TARGETS storm EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib) -install(DIRECTORY ${CMAKE_BINARY_DIR}/include/ DESTINATION include/storm - FILES_MATCHING PATTERN "*.h") +install(TARGETS storm + EXPORT storm_Targets + RUNTIME DESTINATION ${STORM_BIN_INSTALL_DIR} + LIBRARY DESTINATION ${STORM_LIB_INSTALL_DIR} + FRAMEWORK DESTINATION ${STORM_LIB_INSTALL_DIR} + FILE_SET fs_storm_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR} + FILE_SET fs_storm_configured_headers DESTINATION ${STORM_INCLUDE_INSTALL_DIR}) diff --git a/src/storm/adapters/MathsatExpressionAdapter.cpp b/src/storm/adapters/MathsatExpressionAdapter.cpp index 9672aa9f80..d83fef8687 100644 --- a/src/storm/adapters/MathsatExpressionAdapter.cpp +++ b/src/storm/adapters/MathsatExpressionAdapter.cpp @@ -1,6 +1,6 @@ #include "storm/adapters/MathsatExpressionAdapter.h" -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT bool operator==(msat_decl decl1, msat_decl decl2) { return decl1.repr == decl2.repr; } diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h index c2eefae45b..3f14acd36a 100644 --- a/src/storm/adapters/MathsatExpressionAdapter.h +++ b/src/storm/adapters/MathsatExpressionAdapter.h @@ -5,7 +5,7 @@ #include -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT #include "mathsat.h" #endif @@ -19,7 +19,7 @@ #include "storm/utility/constants.h" #include "storm/utility/macros.h" -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT namespace std { // Define hashing operator for MathSAT's declarations. template<> @@ -37,7 +37,7 @@ bool operator==(msat_decl decl1, msat_decl decl2); namespace storm { namespace adapters { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT class MathsatExpressionAdapter : public storm::expressions::ExpressionVisitor { public: diff --git a/src/storm/solver/MathsatSmtSolver.cpp b/src/storm/solver/MathsatSmtSolver.cpp index d50227f9fd..4c79b5c44d 100644 --- a/src/storm/solver/MathsatSmtSolver.cpp +++ b/src/storm/solver/MathsatSmtSolver.cpp @@ -7,7 +7,7 @@ namespace storm { namespace solver { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT MathsatSmtSolver::MathsatAllsatModelReference::MathsatAllsatModelReference( storm::expressions::ExpressionManager const& manager, msat_env const& env, msat_term* model, std::unordered_map const& variableToSlotMapping) @@ -115,14 +115,14 @@ std::string MathsatSmtSolver::MathsatModelReference::toString() const { MathsatSmtSolver::MathsatSmtSolver(storm::expressions::ExpressionManager& manager, Options const& options) : SmtSolver(manager) -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT , expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown) #endif { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT msat_config config = msat_create_config(); if (options.enableInterpolantGeneration) { msat_set_option(config, "interpolation", "true"); @@ -147,7 +147,7 @@ MathsatSmtSolver::MathsatSmtSolver(storm::expressions::ExpressionManager& manage } MathsatSmtSolver::~MathsatSmtSolver() { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT if (!MSAT_ERROR_ENV(env)) { msat_destroy_env(env); } else { @@ -159,7 +159,7 @@ MathsatSmtSolver::~MathsatSmtSolver() { } void MathsatSmtSolver::push() { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT msat_push_backtrack_point(env); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); @@ -167,7 +167,7 @@ void MathsatSmtSolver::push() { } void MathsatSmtSolver::pop() { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT msat_pop_backtrack_point(env); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); @@ -175,7 +175,7 @@ void MathsatSmtSolver::pop() { } void MathsatSmtSolver::pop(uint_fast64_t n) { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT SmtSolver::pop(n); #else (void)n; @@ -184,7 +184,7 @@ void MathsatSmtSolver::pop(uint_fast64_t n) { } void MathsatSmtSolver::reset() { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT msat_reset_env(env); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); @@ -192,7 +192,7 @@ void MathsatSmtSolver::reset() { } void MathsatSmtSolver::add(storm::expressions::Expression const& e) { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT msat_term expression = expressionAdapter->translateExpression(e); msat_assert_formula(env, expression); if (expressionAdapter->hasAdditionalConstraints()) { @@ -207,7 +207,7 @@ void MathsatSmtSolver::add(storm::expressions::Expression const& e) { } SmtSolver::CheckResult MathsatSmtSolver::check() { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT lastCheckAssumptions = false; switch (msat_solve(env)) { case MSAT_SAT: @@ -227,7 +227,7 @@ SmtSolver::CheckResult MathsatSmtSolver::check() { } SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::set const& assumptions) { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT lastCheckAssumptions = true; std::vector mathSatAssumptions; mathSatAssumptions.reserve(assumptions.size()); @@ -255,7 +255,7 @@ SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::set const& assumptions) { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT lastCheckAssumptions = true; std::vector mathSatAssumptions; mathSatAssumptions.reserve(assumptions.size()); @@ -283,7 +283,7 @@ SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::initializer_l } storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation() { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); return this->convertMathsatModelToValuation(); @@ -293,7 +293,7 @@ storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation() { } std::shared_ptr MathsatSmtSolver::getModel() { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); return std::shared_ptr(new MathsatModelReference(this->getManager(), env, *expressionAdapter)); @@ -302,7 +302,7 @@ std::shared_ptr MathsatSmtSolver::getModel() { #endif } -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() { storm::expressions::SimpleValuation stormModel(this->getManager().getSharedPointer()); @@ -332,7 +332,7 @@ storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValua #endif std::vector MathsatSmtSolver::allSat(std::vector const& important) { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT std::vector valuations; this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); @@ -345,7 +345,7 @@ std::vector MathsatSmtSolver::allSat(std::v #endif } -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT class AllsatValuationCallbackUserData { public: AllsatValuationCallbackUserData(storm::expressions::ExpressionManager const& manager, storm::adapters::MathsatExpressionAdapter& adapter, msat_env& env, @@ -426,7 +426,7 @@ class AllsatModelReferenceCallbackUserData { uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure. this->push(); @@ -454,7 +454,7 @@ uint_fast64_t MathsatSmtSolver::allSat(std::vector uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure. this->push(); @@ -483,7 +483,7 @@ uint_fast64_t MathsatSmtSolver::allSat(std::vector } std::vector MathsatSmtSolver::getUnsatAssumptions() { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable."); STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException, @@ -506,7 +506,7 @@ std::vector MathsatSmtSolver::getUnsatAssumption } void MathsatSmtSolver::setInterpolationGroup(uint64_t group) { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT auto groupIter = this->interpolationGroups.find(group); if (groupIter == this->interpolationGroups.end()) { int newGroup = msat_create_itp_group(env); @@ -521,7 +521,7 @@ void MathsatSmtSolver::setInterpolationGroup(uint64_t group) { } storm::expressions::Expression MathsatSmtSolver::getInterpolant(std::vector const& groupsA) { -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate interpolant, because the last check did not determine the formulas to be unsatisfiable."); STORM_LOG_THROW(!lastCheckAssumptions, storm::exceptions::InvalidStateException, diff --git a/src/storm/solver/MathsatSmtSolver.h b/src/storm/solver/MathsatSmtSolver.h index 3444a1995d..4383864716 100644 --- a/src/storm/solver/MathsatSmtSolver.h +++ b/src/storm/solver/MathsatSmtSolver.h @@ -6,7 +6,7 @@ #include "storm/adapters/MathsatExpressionAdapter.h" #include "storm/solver/SmtSolver.h" -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT #include "mathsat.h" #endif @@ -33,7 +33,7 @@ class MathsatSmtSolver : public SmtSolver { bool enableInterpolantGeneration = false; }; -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT class MathsatAllsatModelReference : public SmtSolver::ModelReference { public: MathsatAllsatModelReference(storm::expressions::ExpressionManager const& manager, msat_env const& env, msat_term* model, @@ -51,7 +51,7 @@ class MathsatSmtSolver : public SmtSolver { }; #endif -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT class MathsatModelReference : public SmtSolver::ModelReference { public: MathsatModelReference(storm::expressions::ExpressionManager const& manager, msat_env const& env, @@ -110,7 +110,7 @@ class MathsatSmtSolver : public SmtSolver { private: storm::expressions::SimpleValuation convertMathsatModelToValuation(); -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT // The MathSAT environment. msat_env env; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp index dcd24495b8..7a14c34bba 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -122,13 +122,11 @@ InternalAdd InternalDdManager(this, sylvan::Mtbdd::stormRationalNumberTerminal(storm::utility::one())); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalDdManager::getAddOne() const { return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::one())); } -#endif InternalBdd InternalDdManager::getBddZero() const { return InternalBdd(this, sylvan::Bdd::bddZero()); diff --git a/src/storm/storage/expressions/ToCppVisitor.cpp b/src/storm/storage/expressions/ToCppVisitor.cpp deleted file mode 100644 index 61c4234644..0000000000 --- a/src/storm/storage/expressions/ToCppVisitor.cpp +++ /dev/null @@ -1,350 +0,0 @@ -#include "storm/storage/expressions/ToCppVisitor.h" - -#include "storm/storage/expressions/Expressions.h" - -#include "storm/adapters/RationalFunctionAdapter.h" - -#include "storm/exceptions/NotSupportedException.h" -#include "storm/utility/macros.h" - -namespace storm { -namespace expressions { - -ToCppTranslationOptions::ToCppTranslationOptions(std::unordered_map const& prefixes, - std::unordered_map const& names, ToCppTranslationMode mode) - : prefixes(prefixes), names(names), mode(mode) { - // Intentionally left empty. -} - -std::unordered_map const& ToCppTranslationOptions::getPrefixes() const { - return prefixes.get(); -} - -std::unordered_map const& ToCppTranslationOptions::getNames() const { - return names.get(); -} - -ToCppTranslationMode const& ToCppTranslationOptions::getMode() const { - return mode; -} - -std::string ToCppVisitor::translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options) { - expression.accept(*this, options); - std::string result = stream.str(); - stream.str(""); - return result; -} - -boost::any ToCppVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { - ToCppTranslationOptions const& options = boost::any_cast(data); - - // Clear the type cast for the condition. - ToCppTranslationOptions conditionOptions(options.getPrefixes(), options.getNames()); - stream << "("; - expression.getCondition()->accept(*this, conditionOptions); - stream << " ? "; - expression.getThenExpression()->accept(*this, data); - stream << " : "; - expression.getElseExpression()->accept(*this, data); - stream << ")"; - return boost::none; -} - -boost::any ToCppVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { - ToCppTranslationOptions newOptions = boost::any_cast(data); - - switch (expression.getOperatorType()) { - case BinaryBooleanFunctionExpression::OperatorType::And: - stream << "("; - expression.getFirstOperand()->accept(*this, newOptions); - stream << " && "; - expression.getSecondOperand()->accept(*this, newOptions); - stream << ")"; - break; - case BinaryBooleanFunctionExpression::OperatorType::Or: - stream << "("; - expression.getFirstOperand()->accept(*this, newOptions); - stream << " || "; - expression.getSecondOperand()->accept(*this, newOptions); - stream << ")"; - break; - case BinaryBooleanFunctionExpression::OperatorType::Xor: - stream << "("; - expression.getFirstOperand()->accept(*this, newOptions); - stream << " ^ "; - expression.getSecondOperand()->accept(*this, newOptions); - stream << ")"; - break; - case BinaryBooleanFunctionExpression::OperatorType::Implies: - stream << "(!"; - expression.getFirstOperand()->accept(*this, newOptions); - stream << " || "; - expression.getSecondOperand()->accept(*this, newOptions); - stream << ")"; - break; - case BinaryBooleanFunctionExpression::OperatorType::Iff: - stream << "!("; - expression.getFirstOperand()->accept(*this, newOptions); - stream << " ^ "; - expression.getSecondOperand()->accept(*this, newOptions); - stream << ")"; - break; - } - return boost::none; -} - -boost::any ToCppVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { - switch (expression.getOperatorType()) { - case BinaryNumericalFunctionExpression::OperatorType::Plus: - stream << "("; - expression.getFirstOperand()->accept(*this, data); - stream << " + "; - expression.getSecondOperand()->accept(*this, data); - stream << ")"; - break; - case BinaryNumericalFunctionExpression::OperatorType::Minus: - stream << "("; - expression.getFirstOperand()->accept(*this, data); - stream << " - "; - expression.getSecondOperand()->accept(*this, data); - stream << ")"; - break; - case BinaryNumericalFunctionExpression::OperatorType::Times: - stream << "("; - expression.getFirstOperand()->accept(*this, data); - stream << " * "; - expression.getSecondOperand()->accept(*this, data); - stream << ")"; - break; - case BinaryNumericalFunctionExpression::OperatorType::Divide: - stream << "("; - expression.getFirstOperand()->accept(*this, data); - stream << " / "; - expression.getSecondOperand()->accept(*this, data); - stream << ")"; - break; - case BinaryNumericalFunctionExpression::OperatorType::Min: - stream << "std::min("; - expression.getFirstOperand()->accept(*this, data); - stream << ", "; - expression.getSecondOperand()->accept(*this, data); - stream << ")"; - break; - case BinaryNumericalFunctionExpression::OperatorType::Max: - stream << "std::max("; - expression.getFirstOperand()->accept(*this, data); - stream << ", "; - expression.getSecondOperand()->accept(*this, data); - stream << ")"; - break; - case BinaryNumericalFunctionExpression::OperatorType::Power: - stream << "std::pow("; - expression.getFirstOperand()->accept(*this, data); - stream << ", "; - expression.getSecondOperand()->accept(*this, data); - stream << ")"; - break; - case BinaryNumericalFunctionExpression::OperatorType::Modulo: - stream << "("; - expression.getFirstOperand()->accept(*this, data); - stream << " % "; - expression.getSecondOperand()->accept(*this, data); - stream << ")"; - break; - case BinaryNumericalFunctionExpression::OperatorType::Logarithm: - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Log expressions not implemented for C++ translation."); - } - return boost::none; -} - -boost::any ToCppVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { - ToCppTranslationOptions newOptions = boost::any_cast(data); - - switch (expression.getRelationType()) { - case RelationType::Equal: - stream << "("; - expression.getFirstOperand()->accept(*this, newOptions); - stream << " == "; - expression.getSecondOperand()->accept(*this, newOptions); - stream << ")"; - break; - case RelationType::NotEqual: - stream << "("; - expression.getFirstOperand()->accept(*this, newOptions); - stream << " != "; - expression.getSecondOperand()->accept(*this, newOptions); - stream << ")"; - break; - case RelationType::Less: - stream << "("; - expression.getFirstOperand()->accept(*this, newOptions); - stream << " < "; - expression.getSecondOperand()->accept(*this, newOptions); - stream << ")"; - break; - case RelationType::LessOrEqual: - stream << "("; - expression.getFirstOperand()->accept(*this, newOptions); - stream << " <= "; - expression.getSecondOperand()->accept(*this, newOptions); - stream << ")"; - break; - case RelationType::Greater: - stream << "("; - expression.getFirstOperand()->accept(*this, newOptions); - stream << " > "; - expression.getSecondOperand()->accept(*this, newOptions); - stream << ")"; - break; - case RelationType::GreaterOrEqual: - stream << "("; - expression.getFirstOperand()->accept(*this, newOptions); - stream << " >= "; - expression.getSecondOperand()->accept(*this, newOptions); - stream << ")"; - break; - } - return boost::none; -} - -std::string getVariableName(storm::expressions::Variable const& variable, std::unordered_map const& prefixes, - std::unordered_map const& names) { - auto prefixIt = prefixes.find(variable); - if (prefixIt != prefixes.end()) { - auto nameIt = names.find(variable); - if (nameIt != names.end()) { - return prefixIt->second + nameIt->second; - } else { - return prefixIt->second + variable.getName(); - } - } else { - auto nameIt = names.find(variable); - if (nameIt != names.end()) { - return nameIt->second; - } else { - return variable.getName(); - } - } -} - -boost::any ToCppVisitor::visit(VariableExpression const& expression, boost::any const& data) { - ToCppTranslationOptions const& options = boost::any_cast(data); - storm::expressions::Variable const& variable = expression.getVariable(); - std::string variableName = getVariableName(variable, options.getPrefixes(), options.getNames()); - - if (variable.hasBooleanType()) { - stream << variableName; - } else { - switch (options.getMode()) { - case ToCppTranslationMode::KeepType: - stream << variableName; - break; - case ToCppTranslationMode::CastDouble: - stream << "static_cast(" << variableName << ")"; - break; - case ToCppTranslationMode::CastRationalNumber: - stream << "carl::rationalize(" << variableName << ")"; - break; - case ToCppTranslationMode::CastRationalFunction: - // Here, we rely on the variable name mapping to a rational function representing the variable being available. - stream << variableName; - break; - } - } - return boost::none; -} - -boost::any ToCppVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { - ToCppTranslationOptions newOptions = boost::any_cast(data); - - switch (expression.getOperatorType()) { - case UnaryBooleanFunctionExpression::OperatorType::Not: - stream << "!("; - expression.getOperand()->accept(*this, newOptions); - stream << ")"; - break; - } - return boost::none; -} - -boost::any ToCppVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { - ToCppTranslationOptions const& options = boost::any_cast(data); - switch (expression.getOperatorType()) { - case UnaryNumericalFunctionExpression::OperatorType::Minus: - stream << "-("; - expression.getOperand()->accept(*this, data); - stream << ")"; - break; - case UnaryNumericalFunctionExpression::OperatorType::Floor: - STORM_LOG_THROW(options.getMode() != ToCppTranslationMode::CastRationalFunction, storm::exceptions::NotSupportedException, - "Floor is not supported by rational functions."); - if (options.getMode() != ToCppTranslationMode::CastRationalNumber) { - stream << "std::floor"; - } else { - stream << "carl::floor"; - } - stream << "("; - expression.getOperand()->accept(*this, data); - stream << ")"; - break; - case UnaryNumericalFunctionExpression::OperatorType::Ceil: - STORM_LOG_THROW(options.getMode() != ToCppTranslationMode::CastRationalFunction, storm::exceptions::NotSupportedException, - "Ceil is not supported by rational functions."); - if (options.getMode() != ToCppTranslationMode::CastRationalNumber) { - stream << "std::ceil"; - } else { - stream << "carl::ceil"; - } - stream << "("; - expression.getOperand()->accept(*this, data); - stream << ")"; - break; - } - return boost::none; -} - -boost::any ToCppVisitor::visit(BooleanLiteralExpression const& expression, boost::any const&) { - stream << std::boolalpha << expression.getValue(); - return boost::none; -} - -boost::any ToCppVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { - ToCppTranslationOptions const& options = boost::any_cast(data); - switch (options.getMode()) { - case ToCppTranslationMode::KeepType: - stream << expression.getValue(); - break; - case ToCppTranslationMode::CastDouble: - stream << "static_cast(" << expression.getValue() << ")"; - break; - case ToCppTranslationMode::CastRationalNumber: - stream << "carl::rationalize(\"" << expression.getValue() << "\")"; - break; - case ToCppTranslationMode::CastRationalFunction: - stream << "storm::RationalFunction(carl::rationalize(\"" << expression.getValue() << "\"))"; - break; - } - return boost::none; -} - -boost::any ToCppVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { - ToCppTranslationOptions const& options = boost::any_cast(data); - switch (options.getMode()) { - case ToCppTranslationMode::KeepType: - stream << "(static_cast(" << carl::getNum(expression.getValue()) << ")/" << carl::getDenom(expression.getValue()) << ")"; - break; - case ToCppTranslationMode::CastDouble: - stream << "static_cast(" << expression.getValueAsDouble() << ")"; - break; - case ToCppTranslationMode::CastRationalNumber: - stream << "carl::rationalize(\"" << expression.getValue() << "\")"; - break; - case ToCppTranslationMode::CastRationalFunction: - stream << "storm::RationalFunction(carl::rationalize(\"" << expression.getValue() << "\"))"; - break; - } - return boost::none; -} - -} // namespace expressions -} // namespace storm diff --git a/src/storm/storage/expressions/ToCppVisitor.h b/src/storm/storage/expressions/ToCppVisitor.h deleted file mode 100644 index 64c7828e8d..0000000000 --- a/src/storm/storage/expressions/ToCppVisitor.h +++ /dev/null @@ -1,51 +0,0 @@ -#pragma once - -#include -#include - -#include "storm/storage/expressions/ExpressionVisitor.h" -#include "storm/storage/expressions/Variable.h" - -namespace storm { -namespace expressions { -class Expression; - -enum class ToCppTranslationMode { KeepType, CastDouble, CastRationalNumber, CastRationalFunction }; - -class ToCppTranslationOptions { - public: - ToCppTranslationOptions(std::unordered_map const& prefixes, - std::unordered_map const& names, - ToCppTranslationMode mode = ToCppTranslationMode::KeepType); - - std::unordered_map const& getPrefixes() const; - std::unordered_map const& getNames() const; - ToCppTranslationMode const& getMode() const; - - private: - std::reference_wrapper const> prefixes; - std::reference_wrapper const> names; - ToCppTranslationMode mode; -}; - -class ToCppVisitor : public ExpressionVisitor { - public: - std::string translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options); - - virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; - virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; - virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; - virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override; - virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override; - virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; - virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; - virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; - virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; - virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; - - private: - std::stringstream stream; -}; - -} // namespace expressions -} // namespace storm diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index 1ce9b35d3b..db86fd1b31 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -128,7 +128,7 @@ std::unique_ptr SmtSolverFactory::create(storm::expres } else { #ifdef STORM_HAVE_Z3 smtSolverType = storm::solver::SmtSolverType::Z3; -#elif STORM_HAVE_MSAT +#elif defined STORM_HAVE_MATHSAT smtSolverType = storm::solver::SmtSolverType::Mathsat; #else STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Requested an SMT solver but none was installed."); diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 1389a9d53c..7b35ae2cdf 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -1,6 +1,8 @@ +if (PROJECT_IS_TOP_LEVEL) add_subdirectory(storm) add_subdirectory(storm-dft) add_subdirectory(storm-gamebased-ar) add_subdirectory(storm-pars) add_subdirectory(storm-permissive) -add_subdirectory(storm-pomdp) \ No newline at end of file +add_subdirectory(storm-pomdp) +endif() \ No newline at end of file diff --git a/src/test/storm-dft/CMakeLists.txt b/src/test/storm-dft/CMakeLists.txt index 0989aa7e1a..36cdc53caf 100644 --- a/src/test/storm-dft/CMakeLists.txt +++ b/src/test/storm-dft/CMakeLists.txt @@ -1,10 +1,6 @@ # Base path for test files set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm-dft") -# Test Sources -file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" test) # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) diff --git a/src/test/storm-gamebased-ar/CMakeLists.txt b/src/test/storm-gamebased-ar/CMakeLists.txt index 5c60afd405..6dd7ddae5f 100644 --- a/src/test/storm-gamebased-ar/CMakeLists.txt +++ b/src/test/storm-gamebased-ar/CMakeLists.txt @@ -1,10 +1,6 @@ # Base path for test files set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm-gamebased-ar") -# Test Sources -file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" test) # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) diff --git a/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp b/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp index 3b29126e8b..70e7cf9361 100644 --- a/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp +++ b/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp @@ -37,7 +37,7 @@ class GraphTestAR : public ::testing::Test { protected: void SetUp() override { -#ifndef STORM_HAVE_MSAT +#ifndef STORM_HAVE_MATHSAT GTEST_SKIP() << "MathSAT not available."; #endif } diff --git a/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp b/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp index 4330f09e9e..dd31841ce2 100644 --- a/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp +++ b/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp @@ -30,7 +30,7 @@ class PrismMenuGame : public ::testing::Test { protected: void SetUp() override { -#ifndef STORM_HAVE_MSAT +#ifndef STORM_HAVE_MATHSAT GTEST_SKIP() << "MathSAT not available."; #endif } diff --git a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp index 358f2794f0..ece1d57547 100644 --- a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp +++ b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp @@ -32,7 +32,7 @@ class GameBasedDtmcModelCheckerTest : public ::testing::Test { protected: void SetUp() override { -#ifndef STORM_HAVE_MSAT +#ifndef STORM_HAVE_MATHSAT GTEST_SKIP() << "MathSAT not available."; #endif } diff --git a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp index fa17d4cb8a..32b1801e55 100644 --- a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp +++ b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp @@ -30,7 +30,7 @@ class GameBasedMdpModelCheckerTest : public ::testing::Test { protected: void SetUp() override { -#ifndef STORM_HAVE_MSAT +#ifndef STORM_HAVE_MATHSAT GTEST_SKIP() << "MathSAT not available."; #endif } diff --git a/src/test/storm-pars/CMakeLists.txt b/src/test/storm-pars/CMakeLists.txt index 1f5f94beb2..671bc394da 100644 --- a/src/test/storm-pars/CMakeLists.txt +++ b/src/test/storm-pars/CMakeLists.txt @@ -1,11 +1,6 @@ # Base path for test files set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm-pars") -# Test Sources -file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" test) - # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) diff --git a/src/test/storm-permissive/CMakeLists.txt b/src/test/storm-permissive/CMakeLists.txt index 96f0afb1e5..ac5ffe6407 100644 --- a/src/test/storm-permissive/CMakeLists.txt +++ b/src/test/storm-permissive/CMakeLists.txt @@ -1,10 +1,6 @@ # Base path for test files set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm-permissive") -# Test Sources -file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" test) # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) diff --git a/src/test/storm-pomdp/CMakeLists.txt b/src/test/storm-pomdp/CMakeLists.txt index 4087389a58..cc53dc9962 100644 --- a/src/test/storm-pomdp/CMakeLists.txt +++ b/src/test/storm-pomdp/CMakeLists.txt @@ -1,10 +1,6 @@ # Base path for test files set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm-pomdp") -# Test Sources -file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" test) # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) diff --git a/src/test/storm/CMakeLists.txt b/src/test/storm/CMakeLists.txt index 5aa1014fdd..7ab000ecd1 100755 --- a/src/test/storm/CMakeLists.txt +++ b/src/test/storm/CMakeLists.txt @@ -1,11 +1,6 @@ # Base path for test files set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm") -# Test Sources -file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp) - -register_source_groups_from_filestructure("${ALL_FILES}" test) - # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) diff --git a/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp b/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp index df2d2c4c71..45943e85de 100644 --- a/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp +++ b/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp @@ -1,7 +1,7 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT #include "mathsat.h" #include "storm/adapters/MathsatExpressionAdapter.h" #include "storm/settings/SettingsManager.h" diff --git a/src/test/storm/solver/LpSolverTest.cpp b/src/test/storm/solver/LpSolverTest.cpp index 46a6668714..4838b9de89 100644 --- a/src/test/storm/solver/LpSolverTest.cpp +++ b/src/test/storm/solver/LpSolverTest.cpp @@ -22,7 +22,11 @@ class DefaultEnvironment { static const bool strictRelationSupport = true; static bool skip() { +#ifdef STORM_HAVE_LP_SOLVER return false; +#else + return true; +#endif } }; diff --git a/src/test/storm/solver/MathsatSmtSolverTest.cpp b/src/test/storm/solver/MathsatSmtSolverTest.cpp index ac5f88cee5..a30ad9c0e4 100644 --- a/src/test/storm/solver/MathsatSmtSolverTest.cpp +++ b/src/test/storm/solver/MathsatSmtSolverTest.cpp @@ -1,7 +1,7 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT #include "storm/solver/MathsatSmtSolver.h" TEST(MathsatSmtSolver, CheckSat) { diff --git a/src/test/storm/storage/JaniModelTest.cpp b/src/test/storm/storage/JaniModelTest.cpp index 7e3393a6b6..445c438f58 100644 --- a/src/test/storm/storage/JaniModelTest.cpp +++ b/src/test/storm/storage/JaniModelTest.cpp @@ -6,7 +6,7 @@ #include "storm/storage/jani/Model.h" -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT TEST(JaniModelTest, FlattenComposition) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm")); diff --git a/src/test/storm/storage/PrismProgramTest.cpp b/src/test/storm/storage/PrismProgramTest.cpp index feddcbb002..75590784d9 100644 --- a/src/test/storm/storage/PrismProgramTest.cpp +++ b/src/test/storm/storage/PrismProgramTest.cpp @@ -6,7 +6,7 @@ #include "storm/storage/jani/Model.h" #include "storm/utility/solver.h" -#ifdef STORM_HAVE_MSAT +#ifdef STORM_HAVE_MATHSAT TEST(PrismProgramTest, FlattenModules) { storm::prism::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));