diff --git a/.clang-format b/.clang-format new file mode 100644 index 0000000..8cfe5f7 --- /dev/null +++ b/.clang-format @@ -0,0 +1,4 @@ +BasedOnStyle: Google +ColumnLimit: 120 +# Prevent breaking doxygen +CommentPragmas: '^\*|^/|^!' diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..f41d3d4 --- /dev/null +++ b/.gitignore @@ -0,0 +1,10 @@ +build*/ +deps*/ +*~ +*.swp +*.cfg +lcov_output/ +logs/ +doc/crave-doxygen/ +crave_package_deps.tar.gz + diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml new file mode 100644 index 0000000..f84218b --- /dev/null +++ b/.gitlab-ci.yml @@ -0,0 +1,210 @@ +before_script: + - scripts/show_linux_distribution_and_install_packages.sh + - NUM_JOBS=$[`nproc`-1] + - if [ "$NUM_JOBS" -lt 1 ]; then NUM_JOBS=1; fi + - GIT_SSL_NO_VERIFY=true git submodule sync + - GIT_SSL_NO_VERIFY=true git submodule update --init + +### templates for docker images +.ubuntu16: &ubuntu16 + image: ubuntu:xenial + variables: + JDK_PACKAGE_NAME: openjdk-8-jdk + tags: + - docker + +.ubuntu16_x86: &ubuntu16_x86 + image: m0elnx/ubuntu-32bit:latest + variables: + JDK_PACKAGE_NAME: openjdk-8-jdk + tags: + - docker + +.ubuntu14: &ubuntu14 + image: ubuntu:trusty + variables: + JDK_PACKAGE_NAME: openjdk-7-jdk + tags: + - docker + +.centos7: ¢os7 + image: centos:centos7 + variables: + JDK_PACKAGE_NAME: java-1.8.0-openjdk + tags: + - docker + +.debian8: &debian8 + image: debian:jessie + variables: + JDK_PACKAGE_NAME: openjdk-8-jdk + tags: + - docker + +.fedora25: &fedora25 + image: fedora:25 + variables: + JDK_PACKAGE_NAME: java-1.8.0-openjdk + tags: + - docker + +### template and jobs for the default build (currently with Boolector and CUDD) that should be testes on all images +.build_default: + script: &build_default + - make -j $NUM_JOBS + - make test + +build_default_ubuntu16: + <<: *ubuntu16 + except: + - /.*_fastci$/ + script: *build_default + +build_default_ubuntu14: + <<: *ubuntu14 + only: + - development + - /.*_ci$/ + script: *build_default + +build_default_centos7: + <<: *centos7 + only: + - development + - /.*_ci$/ + script: *build_default + +build_default_debian8: + <<: *debian8 + only: + - development + - /.*_ci$/ + script: *build_default + +build_default_fedora25: + <<: *fedora25 + only: + - development + - /.*_ci$/ + script: *build_default + +### template and jobs for a fast build +.fast_build: + script: &fast_build + - ./bootstrap.sh -d deps -b cudd -b sword build -DCRAVE_TIMEOUT=60 -DCRAVE_BUILD_EXAMPLES=off + - cd build + - make -j $NUM_JOBS + - ctest --schedule-random + +fast_build_ubuntu14: + <<: *ubuntu14 + script: *fast_build + +### template and jobs for a build in RELEASE mode +.build_release: + script: &build_release + - ./bootstrap.sh -d deps -m RELEASE --systemc -b cudd -b sword build -DCRAVE_TIMEOUT=60 -DCRAVE_EXAMPLES_TIMEOUT=180 + - make -j $NUM_JOBS + - make test + +build_release_centos7: + <<: *centos7 + only: + - development + script: *build_release + +### template and jobs for a very fast build with installation +.build_install: + script: &build_install + - ./bootstrap.sh -d deps --systemc -b cudd -b sword build -DCRAVE_BUILD_EXAMPLES=off -DCRAVE_ENABLE_TESTS=off + - cd build + - make -j $NUM_JOBS install + - CRAVE_INSTALL_DIR=`pwd`/root/share/crave + - git clone --depth 1 https://github.com/hoangmle/test-crave-install.git + - cd test-crave-install + - cmake . -Dcrave_DIR=$CRAVE_INSTALL_DIR + - make -j $NUM_JOBS + - ./main 2>result || true + - cat result + - TMP=`grep 'German' result` + - if [ "$TMP" == "" ]; then exit 1; fi + +build_install_centos7: + <<: *centos7 + only: + - development + script: *build_install + +### optional builds in the following + +build_default_stp: + <<: *ubuntu16 + only: + - development + script: + - CRAVE_SOLVERS='cudd stp' make -j $NUM_JOBS + - make test + allow_failure: true + +build_cvc4: + <<: *ubuntu16 + only: + - development + script: + - ./bootstrap.sh -d deps --systemc -b cudd -b cvc4 build -DCRAVE_TIMEOUT=60 -DCRAVE_EXAMPLES_TIMEOUT=180 + - cd build + - make -j $NUM_JOBS + - ctest --schedule-random + allow_failure: true + +build_yices2: + <<: *ubuntu16 + only: + - development + script: + - ./bootstrap.sh -d deps --systemc -b cudd -b yices2 build -DCRAVE_TIMEOUT=60 -DCRAVE_EXAMPLES_TIMEOUT=180 + - cd build + - make -j $NUM_JOBS + - ctest --schedule-random + allow_failure: true + +build_z3: + <<: *ubuntu16 + only: + - development + script: + - ./bootstrap.sh -d deps --systemc -b cudd -b z3 build -DCRAVE_TIMEOUT=60 -DCRAVE_EXAMPLES_TIMEOUT=180 + - cd build + - make -j $NUM_JOBS + - ctest --schedule-random + allow_failure: true + +build_ubuntu16_x86: + <<: *ubuntu16_x86 + only: + - development + script: + - ./bootstrap.sh -d deps -b cudd -b boolector build -DCRAVE_TIMEOUT=60 -DCRAVE_EXAMPLES_TIMEOUT=180 + - cd build + - make -j $NUM_JOBS + - ctest --schedule-random + allow_failure: true + +### Windows build with Visual Studio +build_windows: + except: + - /.*_fastci$/ + before_script: + - git submodule sync + - git submodule update --init + script: + - call "%VS140COMNTOOLS%VsDevCmd.bat" + - rmdir build /s /q + - mkdir build + - cd build + - cmake .. -DBOOST_ROOT="C:\deps\boost_1_60_0" -DmetaSMT_ENABLE_TESTS=off -DZ3_DIR="C:\deps\z3-4.5.0-x86-win" -DCRAVE_TIMEOUT=60 -DCRAVE_EXAMPLES_TIMEOUT=180 + - cmake --build . --config Debug + - ctest + tags: + - windows + diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..e69de29 diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 0000000..f8a9587 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,15 @@ +language: cpp +dist: trusty +sudo: false + +compiler: + - gcc + - clang + +cache: + apt: true + +script: make && make test + +os: + - linux diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 0000000..2c3f221 --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,51 @@ +######################################################################################## +## MIT License +######################################################################################## +## Copyright (c) 2012-2020 University of Bremen, Germany. +## Copyright (c) 2015-2020 DFKI GmbH Bremen, Germany. +## Copyright (c) 2020 Johannes Kepler University Linz, Austria. +## +## 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. +########################################################################################## + + + +project ( crave2uvm ) +cmake_minimum_required(VERSION 2.8) + +set (CMAKE_RUNTIME_OUTPUT_DIRECTORY ${PROJECT_SOURCE_DIR}/build/bin) +set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${PROJECT_SOURCE_DIR}/build/lib) +set (CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake) + +#SystemC +find_package(SystemC REQUIRED) + +#CRAVE +find_package(CRAVE REQUIRED) + +#UVM-SystemC +find_package(UVM-SystemC REQUIRED) + +#Includes setzen +include_directories (${SystemC_INCLUDE_DIRS} ${CRAVE_INCLUDE_DIRS} ${UVM_SystemC_INCLUDE_DIRS} ${PROJECT_SOURCE_DIR}/src/include) + +#Compiler flags +SET( CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -pthread -g -ggdb") + +add_subdirectory (examples) diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..8b8bf2f --- /dev/null +++ b/LICENSE @@ -0,0 +1,24 @@ +MIT License + +Copyright (c) 2012-2020 University of Bremen, Germany. +Copyright (c) 2015-2020 DFKI GmbH Bremen, Germany. +Copyright (c) 2020 Johannes Kepler University Linz, Austria. + +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. + diff --git a/README.md b/README.md index a59a27c..35d5d75 100644 --- a/README.md +++ b/README.md @@ -1 +1,43 @@ -# crave \ No newline at end of file +# CRAVE2UVM prototype + +This projects contains a prototypical integration of CRAVE with UVM-SystemC to provide access to constrained randomization and coverage. +For demonstration, we ported the SystemVerilog example UBUS to UVM-SystemC and included it in this distribution. + +## Requirements + +Make sure all pre install requirements of CRAVE and UVM-SystemC are met: + +* CMake (at least v2.8.9) +* GNU Make +* g++ (at least v4.7.2) +* SystemC (the environment variable SYSTEMC_HOME must be set accordingly) +* Boost (at least v1.50.0 and the environment variable BOOST_ROOT must be set accordingly) +* zlib development libraries (e.g. zlib1g-dev). + +The version of CRAVE included in this distribution by default will build a minimal configuration (Glog and 2 solver backends: CUDD and Z3). +Other configurations with additional backends (e.g. Boolector, SWORD, CVC4, etc.) are also possible. +If download is permitted, CRAVE can automatically download and build these backends. +Otherwise, the user needs to provide appropriate source or binary archive in deps/cache. +For more detailed instructions , please refer to the CRAVE README or contact us. + +## Installation + +To install and run the example, use the buildscript on the toplevel of this repository. It currently executes three common tasks: + +1. ./buildscript install: this will install CRAVE (shipped with this distribution) into ./crave, locally compiles UVM-SystemC into ../.. and setup the Makefile for the example "Ubus". + +2. ./buildscript compile: this will compile the example and put the executables into build/bin. + +3. ./buildscript run: this will run the Ubus example. + +## Tested OS + +This distribution has been tested on the following 64-bit Linux (x86_64) systems: + +* Fedora 22 with g++-5.3.1 +* Ubuntu 14.04.4 LTS with g++-4.8.4 +* Debian 7.0 with g++-4.7.2 + +## Contact +For bugreport and feedback: crave@systemc-verification.org + diff --git a/buildscript b/buildscript new file mode 100755 index 0000000..913474e --- /dev/null +++ b/buildscript @@ -0,0 +1,194 @@ +#!/bin/bash + +NUM_THREADS=1 + +install_dependencies () { + echo "Install dependencies using $NUM_THREADS thread(s)" + + #SystemC + echo -n "SystemC: " + if [ -z "$SYSTEMC_HOME" ] + then + echo "NOT FOUND - Please set SYSTEMC_HOME to a valid SystemC installation" + echo -n "Otherwise type "y" to check and install SystemC now: " + read line + if [ "$line" = "y" ] + then + echo "Installing SystemC (or just setting the SYSTEMC_HOME variable for installation)" + if [ ! -d systemc-2.3.1 ] + then + wget http://accellera.org/images/downloads/standards/systemc/systemc-2.3.1.tgz + mv systemc-2.3.1.tgz systemc-2.3.1.tar + tar xvf systemc-2.3.1.tar + cd systemc-2.3.1 + mkdir objdir + cd objdir + ../configure + make + make install + cd ../.. + fi + cd systemc-2.3.1 + export SYSTEMC_HOME=`pwd` + echo "SYSTEMC_HOME set to $SYSTEMC_HOME" + cd .. + else + exit 1 + fi + else + echo "found SystemC at $SYSTEMC_HOME" + fi + + #crave + echo -n "CRAVE: " + if [ -d crave ] + then + cd crave + if [ ! -d build ] + then + echo "Installing CRAVE." + export GLOG_ROOT=/do/not/use + export CRAVE_SOLVERS='cudd z3' + echo "Build CRAVE using $NUM_THREADS thread(s)" + make -j $NUM_THREADS + make install -j $NUM_THREADS + cd .. + else + echo "CRAVE already installed." + fi + else + echo "CRAVE not found" + fi + + #uvm-systemc + echo -n "uvm-systemc-1.0-beta2: " + if [ ! -d ../include ] && [ -z "$UVM_SYSTEMC_HOME" ] + then + echo "install" + cd .. + export CXXFLAGS=-std=c++11 + export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$SYSTEMC_HOME/lib-linux64:$SYSTEMC_HOME/lib-linux + config/bootstrap + mkdir objdir + cd objdir + ../configure --enable-debug + echo "Build UVM-SystemC using $NUM_THREADS thread(s)" + make -j $NUM_THREADS + make install -j $NUM_THREADS + # export UVM_SYSTEMC_HOME=`pwd` + # echo "UVM_SYSTEMC_HOME set to $UVM_SYSTEMC_HOME" + cd .. + #rm -rf objdir + cd crave + else + echo "found UVM-SystemC" + fi +} + +if [ "$1" = '' ] + then + echo " Usage: ./buildscript [Options]" + echo " Tasks: " + echo -e " install [-j n]\t - Install the UBUS example and all dependencies" + echo -e " compile [-j n]\t - (Re)compile the example after changes (You may use -j n to be faster with make)" + echo -e " run \t - Run the UBUS example" + echo -e " tarball \t - Create a tarball of the repository" + else + if [ "$2" == "-j" ] + then + case $3 in + ''|*[!0-9]*) ;; + *) NUM_THREADS=$3 ;; + esac + fi + case "$1" in + install) + install_dependencies + echo "Dependencies installed." + if [ -d build ] + then + rm -r build + fi + mkdir build + cd build + echo "Unix Makefiles process..." + cmake -G "Unix Makefiles" .. + cd .. + ;; + compile) + cd build + make -j $NUM_THREADS + cd .. + ;; + run) + build/bin/ubus + ;; + tarball) + name_date=crave2uvm_$(date +"%Y%m%d_%H%M") + name_pre=contrib + name=$name_pre/crave + + CRAVE_ARCHIVE_LOCAL=`ls crave-*.tar.gz -t` + if [ -z "$CRAVE_ARCHIVE_LOCAL" ] + then + echo "Error: missing crave tarball. Please, put a crave tarball to create a uvm-systemc-crave layer tarball." + else + mkdir -p $name + mkdir -p $name/cmake + mkdir -p $name/examples + mkdir -p $name/src + mkdir -p $name/presentation + + cp -R cmake/* $name/cmake + cp -R examples/* $name/examples + cp -R src/* $name/src + cp presentation/UVM-CRAVE.pdf $name/presentation/UVM-CRAVE.pdf + cp CMakeLists.txt $name/CMakeLists.txt + CRAVE_ARCHIVE=`ls crave-*.tar.gz -t | head -1` + cp $CRAVE_ARCHIVE $name/$CRAVE_ARCHIVE + cp buildscript $name/buildscript + cp README.md $name/README.md + + tar -cvzf $name_date.tar.gz $name + rm -rf $name_pre + fi + ;; + getcrave) + name_date=crave-$(date +"%Y-%m-%d") + name=crave + git clone --recursive -b crave-z3-convers git@gitlab.informatik.uni-bremen.de:crave-wg/convers.git $name + cd $name/ + + mkdir -p $name + mkdir -p $name/cmake + mkdir -p $name/dependencies + mkdir -p $name/doc + mkdir -p $name/examples + mkdir -p $name/metaSMT + mkdir -p $name/src + mkdir -p $name/tests + + cp -R cmake/* $name/cmake + cp -R dependencies/* $name/dependencies + cp -R doc/* $name/doc + cp -R examples/* $name/examples + cp -R metaSMT/* $name/metaSMT + cp -R src/* $name/src + cp -R tests/* $name/tests + + cp bootstrap.sh $name/ + cp CMakeLists.txt $name/ + cp LICENSE $name/ + cp Makefile $name + cp README.md $name/README.md + + tar -cvzf $name_date.tar.gz $name + rm -rf $name + cp $name_date.tar.gz ../ + cd .. + + rm -rf $name + + ;; + esac +fi diff --git a/cmake/FindCRAVE.cmake b/cmake/FindCRAVE.cmake new file mode 100644 index 0000000..9ab7cc7 --- /dev/null +++ b/cmake/FindCRAVE.cmake @@ -0,0 +1,29 @@ +#______________________________________________________________________________ +# +# This CMake package creates a CRAVE target with all its dependencies +#______________________________________________________________________________ +# +# CRAVE_FOUND - system has CRAVE +# CRAVE_INCLUDE_DIRS - the CRAVE include directory and include directories of all dependencies +# CRAVE_LIBRARIES - Link these to use CRAVE. Contains CRAVE and dependencies + +SET(crave_DIR ${PROJECT_SOURCE_DIR}/crave/build/root/share/crave/) +find_package(crave QUIET) +IF(crave_FOUND) + SET(CRAVE_FOUND TRUE) + SET(CRAVE_INCLUDE_DIRS ${crave_INCLUDE_DIR}) + SET(CRAVE_LIBRARIES ${crave_LIBRARIES}) +ENDIF() + +IF(CRAVE_FOUND) + IF(NOT CRAVE_FIND_QUIETLY) + MESSAGE(STATUS "Found CRAVE: ${CRAVE_LIBRARIES}") + ENDIF(NOT CRAVE_FIND_QUIETLY) +ELSE(CRAVE_FOUND) + IF(CRAVE_FIND_REQUIRED) + MESSAGE(FATAL_ERROR "Could not find CRAVE") + ENDIF(CRAVE_FIND_REQUIRED) +ENDIF(CRAVE_FOUND) + +MARK_AS_ADVANCED(CRAVE_INCLUDE_DIRS CRAVE_LIBRARIES) + diff --git a/cmake/FindSystemC.cmake b/cmake/FindSystemC.cmake new file mode 100644 index 0000000..fd17911 --- /dev/null +++ b/cmake/FindSystemC.cmake @@ -0,0 +1,55 @@ +#______________________________________________________________________________ +# +# This CMake package creates a SystemC target +#______________________________________________________________________________ +# +# SystemC_FOUND - system has SystemC +# SystemC_INCLUDE_DIRS - the SystemC include directory +# SystemC_LIBRARIES - Link these to use SystemC + +IF(SystemC_LIBRARIES AND SystemC_INCLUDE_DIRS) + SET(SystemC_FOUND TRUE) +ELSE(SystemC_LIBRARIES AND SystemC_INCLUDE_DIRS) + FIND_PATH(SystemC_INCLUDE_DIR + HINTS + ${SYSTEMC_HOME}/include + $ENV{SYSTEMC_HOME}/include + NAMES + systemc.h + ) + + FIND_LIBRARY(SystemC_LIBRARY + HINTS + ${SYSTEMC_HOME}/lib + ${SYSTEMC_HOME}/lib-linux + ${SYSTEMC_HOME}/lib-linux64 + ${SYSTEMC_HOME}/lib-macos + $ENV{SYSTEMC_HOME}/lib + $ENV{SYSTEMC_HOME}/lib-linux + $ENV{SYSTEMC_HOME}/lib-linux64 + $ENV{SYSTEMC_HOME}/lib-macos + NAMES + systemc + ) + +SET(SystemC_INCLUDE_DIRS ${SystemC_INCLUDE_DIR}) +SET(SystemC_LIBRARIES ${SystemC_LIBRARY}) + +IF(SystemC_INCLUDE_DIRS AND SystemC_LIBRARIES) + SET(SystemC_FOUND TRUE) +ENDIF(SystemC_INCLUDE_DIRS AND SystemC_LIBRARIES) + +IF(SystemC_FOUND) + IF(NOT SystemC_FIND_QUIETLY) + MESSAGE(STATUS "Found SystemC: ${SystemC_LIBRARIES}") + ENDIF(NOT SystemC_FIND_QUIETLY) +ELSE(SystemC_FOUND) + IF(SystemC_FIND_REQUIRED) + MESSAGE(FATAL_ERROR "Could not find SystemC") + ENDIF(SystemC_FIND_REQUIRED) +ENDIF(SystemC_FOUND) + +# show the SystemC_INCLUDE_DIRS and SystemC_LIBRARIES variables only in the advanced view +MARK_AS_ADVANCED(SystemC_INCLUDE_DIRS SystemC_LIBRARIES) + +ENDIF(SystemC_LIBRARIES AND SystemC_INCLUDE_DIRS) diff --git a/cmake/FindUVM-SystemC.cmake b/cmake/FindUVM-SystemC.cmake new file mode 100644 index 0000000..53ca2af --- /dev/null +++ b/cmake/FindUVM-SystemC.cmake @@ -0,0 +1,59 @@ +#______________________________________________________________________________ +# +# This CMake package creates a UVM-SystemC target +#______________________________________________________________________________ +# +# UVM_SystemC_FOUND - system has UVM-SystemC +# UVM_SystemC_INCLUDE_DIRS - the UVM-SystemC include directory +# UVM_SystemC_LIBRARIES - Link these to use UVM-SystemC + +message("UVM_SYSTEMC_HOME:" $ENV{UVM_SYSTEMC_HOME}) +IF(NOT EXISTS "$ENV{UVM_SYSTEMC_HOME}") + SET(UVM_SYSTEMC_HOME ${PROJECT_SOURCE_DIR}/../) +ENDIF(NOT EXISTS "$ENV{UVM_SYSTEMC_HOME}") + +IF(UVM_SystemC_LIBRARIES AND UVM_SystemC_INCLUDE_DIRS) + SET(UVM_SystemC_FOUND TRUE) +ELSE(UVM_SystemC_LIBRARIES AND UVM_SystemC_INCLUDE_DIRS) + FIND_PATH(UVM_SystemC_INCLUDE_DIR + HINTS + ${UVM_SYSTEMC_HOME}/include + $ENV{UVM_SYSTEMC_HOME}/include + NAMES + uvm.h + ) + + FIND_LIBRARY(UVM_SystemC_LIBRARY + HINTS + ${UVM_SYSTEMC_HOME}/lib + ${UVM_SYSTEMC_HOME}/lib-linux + ${UVM_SYSTEMC_HOME}/lib-linux64 + ${UVM_SYSTEMC_HOME}/lib-macos + $ENV{UVM_SYSTEMC_HOME}/lib + $ENV{UVM_SYSTEMC_HOME}/lib-linux + $ENV{UVM_SYSTEMC_HOME}/lib-linux64 + $ENV{UVM_SYSTEMC_HOME}/lib-macos + NAMES + uvm-systemc + ) + +SET(UVM_SystemC_INCLUDE_DIRS ${UVM_SystemC_INCLUDE_DIR}) +SET(UVM_SystemC_LIBRARIES ${UVM_SystemC_LIBRARY}) + +IF(UVM_SystemC_INCLUDE_DIRS AND UVM_SystemC_LIBRARIES) + SET(UVM_SystemC_FOUND TRUE) +ENDIF(UVM_SystemC_INCLUDE_DIRS AND UVM_SystemC_LIBRARIES) + +IF(UVM_SystemC_FOUND) + IF(NOT UVM_SystemC_FIND_QUIETLY) + MESSAGE(STATUS "Found UVM_SystemC: ${UVM_SystemC_LIBRARIES}") + ENDIF(NOT UVM_SystemC_FIND_QUIETLY) +ELSE(UVM_SystemC_FOUND) + IF(UVM_SystemC_FIND_REQUIRED) + MESSAGE(FATAL_ERROR "Could not find UVM_SystemC") + ENDIF(UVM_SystemC_FIND_REQUIRED) +ENDIF(UVM_SystemC_FOUND) + +MARK_AS_ADVANCED(UVM_SystemC_INCLUDE_DIRS UVM_SystemC_LIBRARIES) + +ENDIF(UVM_SystemC_LIBRARIES AND UVM_SystemC_INCLUDE_DIRS) diff --git a/crave/CMakeLists.txt b/crave/CMakeLists.txt new file mode 100644 index 0000000..3ebb6a8 --- /dev/null +++ b/crave/CMakeLists.txt @@ -0,0 +1,319 @@ +######################################################################################## +## MIT License +######################################################################################## +## Copyright (c) 2012-2020 University of Bremen, Germany. +## Copyright (c) 2015-2020 DFKI GmbH Bremen, Germany. +## Copyright (c) 2020 Johannes Kepler University Linz, Austria. +## +## 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. +########################################################################################## + + + +project(crave) +cmake_minimum_required(VERSION 2.8.9) + +set(${PROJECT_NAME}_CONFIG_DIR "share/${PROJECT_NAME}" CACHE PATH + "where to install CMake and Make Config files") + +set(CMAKE_BUILD_TYPE Debug) +############################################################ +## CRAVE settings ## +############################################################ + +option(CRAVE_ENABLE_EXPERIMENTAL "enable experimental extensions of CRAVE" on) +option(CRAVE_ENABLE_TESTS "build tests" on) +option(CRAVE_BUILD_EXAMPLES "build and test examples" on) + +### C++11 required +include(CheckCXXCompilerFlag) +CHECK_CXX_COMPILER_FLAG("-std=c++11" COMPILER_SUPPORTS_CXX11) +if(COMPILER_SUPPORTS_CXX11) + add_definitions(-std=c++11) +else() + message(FATAL_ERROR "The compiler ${CMAKE_CXX_COMPILER} does not support -std=c++11. Please use a different C++ compiler.") +endif() +if (MINGW) + add_definitions(-Wa,-mbig-obj) +endif() + +### packages +set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake) + +set(Boost_NO_BOOST_CMAKE true) +set(Boost_NO_SYSTEM_PATHS true) + +if (WIN32 AND (NOT MINGW)) + if (MSVC AND (NOT MSVC_VERSION LESS 1900)) + find_package(Boost REQUIRED) + else() + message(FATAL_ERROR "CRAVE Windows build only supports Visual Studio C++ 2015 or newer version") + endif() +else() + find_package(Boost REQUIRED COMPONENTS system filesystem) +endif() + +find_package(GLOG) + +if (GLOG_FOUND) + add_definitions(-DCRAVE_HAVE_GLOG) +endif() + +if (WITH_SYSTEMC) + find_package(SystemC REQUIRED) + find_package(Threads REQUIRED) +endif() + +add_subdirectory(metaSMT) +list(INSERT CMAKE_PREFIX_PATH 0 "${CMAKE_BINARY_DIR}") +find_package(metaSMT REQUIRED) +string(REPLACE " " ";" metaSMT_DEFINITIONS "${metaSMT_CXXFLAGS}") +add_definitions(${metaSMT_DEFINITIONS}) + +### FIXME this should not be necessary, reuse variables set by metaSMT instead +if ( WIN32 ) + message(STATUS "CRAVE Windows build: explicitly disable all solvers except z3 or CUDD!" ) + set(metaSMT_USE_SWORD off) + set(metaSMT_USE_Boolector off) + set(metaSMT_USE_STP off) + set(metaSMT_USE_CVC4 off) + set(metaSMT_USE_YICES2 off) + set(metaSMT_USE_MiniSat off) + set(metaSMT_USE_picosat off) + set(metaSMT_USE_lingeling off) + set(metaSMT_USE_Aiger off) + set(metaSMT_USE_CW off) +endif() + +### SMT solvers +if (metaSMT_USE_Boolector) + add_definitions(-DmetaSMT_USE_Boolector) +endif() +if (metaSMT_USE_CVC4) + add_definitions(-DmetaSMT_USE_CVC4) +endif() +if (metaSMT_USE_STP) + add_definitions(-DmetaSMT_USE_STP) +endif() +if (metaSMT_USE_SWORD) + add_definitions(-DmetaSMT_USE_SWORD) +endif() +if (metaSMT_USE_YICES2) + add_definitions(-DmetaSMT_USE_YICES2) +endif() +if (metaSMT_USE_Z3) + add_definitions(-DmetaSMT_USE_Z3) +endif() + +### BDD +if (metaSMT_USE_CUDD) + add_definitions(-DmetaSMT_USE_CUDD) +endif() + +if (WITH_SYSTEMC) + add_definitions(-DWITH_SYSTEMC) +endif() + +### includes +include_directories(${metaSMT_INCLUDE_DIR}) +include_directories(${Boost_INCLUDE_DIRS}) + +if (GLOG_FOUND) + include_directories(${GLOG_INCLUDE_DIRS}) +endif() + +if(SystemC_FOUND) + include_directories(${SystemC_INCLUDE_DIR}) +endif(SystemC_FOUND) + +### libs +SET(ALL_EXTERNAL_LIBS "") + +if (GLOG_FOUND) + LIST(APPEND ALL_EXTERNAL_LIBS ${GLOG_LIBRARIES}) +endif() + +if(SystemC_FOUND) + LIST(APPEND ALL_EXTERNAL_LIBS ${SystemC_LIBRARY} ${CMAKE_THREAD_LIBS_INIT}) +endif(SystemC_FOUND) + +if( Boost_FILESYSTEM_FOUND ) + list(APPEND ALL_EXTERNAL_LIBS ${Boost_FILESYSTEM_LIBRARY}) +endif() + +if( Boost_SYSTEM_FOUND ) + list(APPEND ALL_EXTERNAL_LIBS ${Boost_SYSTEM_LIBRARY}) +endif() + +### build +add_subdirectory(src) + +### tests +if (CRAVE_ENABLE_TESTS) + enable_testing() + add_subdirectory(tests) +endif() + +if (CRAVE_BUILD_EXAMPLES) + enable_testing() + add_subdirectory(examples) +endif() + +### config +set(${PROJECT_NAME}_LIBS ${CMAKE_INSTALL_PREFIX}/lib/lib${PROJECT_NAME}.a ${ALL_EXTERNAL_LIBS} ${metaSMT_LIBRARIES}) + +GET_DIRECTORY_PROPERTY(ALL_INCLUDES INCLUDE_DIRECTORIES) +set(${PROJECT_NAME}_INCLUDE ${CMAKE_INSTALL_PREFIX}/include ${ALL_INCLUDES}) + +GET_DIRECTORY_PROPERTY(${PROJECT_NAME}_DEFS COMPILE_DEFINITIONS) + +## create CRAVE CMake config file +file(WRITE ${PROJECT_BINARY_DIR}/${PROJECT_NAME}Config.cmake +"set(${PROJECT_NAME}_FOUND 1) +set(${PROJECT_NAME}_INCLUDE_DIR ${${PROJECT_NAME}_INCLUDE}) +set(${PROJECT_NAME}_LIBRARIES ${${PROJECT_NAME}_LIBS}) +set(${PROJECT_NAME}_DEFINITIONS ${${PROJECT_NAME}_DEFS}) +") + +## create CRAVE py config file +file(WRITE ${PROJECT_BINARY_DIR}/${PROJECT_NAME}Config.py +"${PROJECT_NAME}_INCLUDES = '${${PROJECT_NAME}_INCLUDE}' +${PROJECT_NAME}_LIBRARIES = '${${PROJECT_NAME}_LIBS}' +${PROJECT_NAME}_DEFINITIONS = '${${PROJECT_NAME}_DEFS}' +") + +string(REPLACE ";" " " ${PROJECT_NAME}_MLIBS "${${PROJECT_NAME}_LIBS}") +string(REPLACE ";" " -I" ${PROJECT_NAME}_MINCLUDE "${${PROJECT_NAME}_INCLUDE}") +string(REPLACE ";" " -D" ${PROJECT_NAME}_MDEFS "${${PROJECT_NAME}_DEFS}") +set(${PROJECT_NAME}_RPATH "") +foreach(LIBPATH ${${PROJECT_NAME}_LIBS}) + get_filename_component(LIBDIR ${LIBPATH} PATH) + LIST(APPEND ${PROJECT_NAME}_RPATH -Wl,-rpath=${LIBDIR}) +endforeach() +string(REPLACE ";" " " ${PROJECT_NAME}_RPATH "${${PROJECT_NAME}_RPATH}") + +## create CRAVE CMake make config file +file(WRITE ${PROJECT_BINARY_DIR}/${PROJECT_NAME}.makefile +"${PROJECT_NAME}_INCLUDES := ${${PROJECT_NAME}_MINCLUDE} +${PROJECT_NAME}_DEFINITIONS := ${${PROJECT_NAME}_MDEFS} +${PROJECT_NAME}_LIBRARIES := ${${PROJECT_NAME}_MLIBS} +${PROJECT_NAME}_RPATH := ${${PROJECT_NAME}_RPATH} +") + +## create CRAVE pkgconfig make config file +string(REPLACE ";" " " ${PROJECT_NAME}_MLIBS "${${PROJECT_NAME}_LIBS}") +file(WRITE ${PROJECT_BINARY_DIR}/${PROJECT_NAME}.pc +"Name: ${PROJECT_NAME} +Description: Constraint Solver library +Cflags: -I${${PROJECT_NAME}_MINCLUDE} -D${${PROJECT_NAME}_MDEFS} +Libs: ${${PROJECT_NAME}_MLIBS} +") + +## install +INSTALL( FILES + ${PROJECT_BINARY_DIR}/${PROJECT_NAME}Config.cmake + ${PROJECT_BINARY_DIR}/${PROJECT_NAME}Config.py + ${PROJECT_BINARY_DIR}/${PROJECT_NAME}.makefile + DESTINATION ${${PROJECT_NAME}_CONFIG_DIR}) +INSTALL( FILES + ${PROJECT_BINARY_DIR}/${PROJECT_NAME}.pc + DESTINATION lib/pkgconfig/) + +############################################################ +## CPack settings ## +############################################################ + +option( CRAVE_BUNDLE_PACKAGE_BY_DATE "use date for package name instead of git description" on) + +if( CRAVE_BUNDLE_PACKAGE_BY_DATE ) + + # CPack version numbers for release tarball name. + if(UNIX) + execute_process(COMMAND date +%Y OUTPUT_VARIABLE CPACK_PACKAGE_VERSION_MAJOR ERROR_QUIET OUTPUT_STRIP_TRAILING_WHITESPACE) + execute_process(COMMAND date +%m OUTPUT_VARIABLE CPACK_PACKAGE_VERSION_MINOR ERROR_QUIET OUTPUT_STRIP_TRAILING_WHITESPACE) + execute_process(COMMAND date +%d OUTPUT_VARIABLE CPACK_PACKAGE_VERSION_PATCH ERROR_QUIET OUTPUT_STRIP_TRAILING_WHITESPACE) + endif() + set(VERSION "${CPACK_PACKAGE_VERSION_MAJOR}-${CPACK_PACKAGE_VERSION_MINOR}-${CPACK_PACKAGE_VERSION_PATCH}") +else() + include(cmake/get_git_version.cmake) + get_git_version(VERSION crave-bundle-) +endif() + +message(STATUS "crave-bundle VERSION: ${VERSION}") + +set(CPACK_PACKAGE_DESCRIPTION_SUMMARY "CRAVE - Constrained RAndom Verification Environment for SystemC/C++") +set(CPACK_PACKAGE_VENDOR "CRAVE development team") +set(CPACK_PACKAGE_DESCRIPTION_FILE ${CMAKE_CURRENT_SOURCE_DIR}/README.md) +set(CPACK_GENERATOR TGZ) +set( +CPACK_SOURCE_PACKAGE_FILE_NAME +"${PROJECT_NAME}-${VERSION}" +CACHE INTERNAL "tarball basename" +) +set(CPACK_SOURCE_GENERATOR TGZ) + +set(CPACK_SOURCE_IGNORE_FILES +"/\\\\.git" +"/deps.*/" +"/build.*/" +"/root.*/" +"/crave-doxygen/" +"/logs/" +"crave.cfg" +"jenkins_run_crave_check.sh" +"~$" +"^${PROJECT_SOURCE_DIR}/scripts/" +"^${PROJECT_SOURCE_DIR}/crave.*" +"^${PROJECT_SOURCE_DIR}/.*.user" +) + +if (NOT CRAVE_ENABLE_EXPERIMENTAL) + LIST(APPEND CPACK_SOURCE_IGNORE_FILES "crave/experimental/" "lib/experimental") +endif() + +include(CPack) + +############################################################ +## CMAKE flags settings ## +############################################################ + +SET( CMAKE_CXX_FLAGS_PROFILING "-O0 -g -Wall -Wextra -pedantic --coverage" CACHE STRING + "Flags used by the C++ compiler during maintainer builds." + FORCE ) +SET( CMAKE_C_FLAGS_PROFILING "${CMAKE_CXX_FLAGS_PROFILING}" CACHE STRING + "Flags used by the C compiler during maintainer builds." + FORCE ) +SET( CMAKE_EXE_LINKER_FLAGS_PROFILING + "--coverage" CACHE STRING + "Flags used for linking binaries during maintainer builds." + FORCE ) +SET( CMAKE_SHARED_LINKER_FLAGS_PROFILING + " --coverage" CACHE STRING + "Flags used by the shared libraries linker during maintainer builds." + FORCE ) +MARK_AS_ADVANCED( + CMAKE_CXX_FLAGS_PROFILING + CMAKE_C_FLAGS_PROFILING + CMAKE_EXE_LINKER_FLAGS_PROFILING + CMAKE_SHARED_LINKER_FLAGS_PROFILING ) +# Update the documentation string of CMAKE_BUILD_TYPE for GUIs +SET( CMAKE_BUILD_TYPE "${CMAKE_BUILD_TYPE}" CACHE STRING + "Choose the type of build, options are: None Debug Release RelWithDebInfo MinSizeRel Profiling." + FORCE ) + diff --git a/crave/LICENSE b/crave/LICENSE new file mode 100644 index 0000000..8cd6150 --- /dev/null +++ b/crave/LICENSE @@ -0,0 +1,28 @@ +*DISCLAIMER*: The following license applies to the CRAVE source code only. +Please make sure that you can comply with the license of the dependencies, +which might be much more restricting. + +MIT License + +Copyright (c) 2012-2020 University of Bremen, Germany. +Copyright (c) 2015-2020 DFKI GmbH Bremen, Germany. +Copyright (c) 2020 Johannes Kepler University Linz, Austria. + +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. + diff --git a/crave/Makefile b/crave/Makefile new file mode 100644 index 0000000..7455fe5 --- /dev/null +++ b/crave/Makefile @@ -0,0 +1,66 @@ +CRAVE_SOLVERS ?= cudd z3 + +SRCDIR:=$(shell pwd) +BUILD:=$(SRCDIR)/build +LCOVDIR:=$(BUILD)/lcov_output +DEPS_CLEAN:=$(BUILD)/deps-clean +PARENTDIR:=$(shell dirname ${SRCDIR}) + +ifndef MAKECMDGOALS +MAKECMDGOALS=all +endif + +${MAKECMDGOALS}: ${BUILD}/Makefile + @${MAKE} -q -s -C ${BUILD} ${MAKECMDGOALS}|| ${MAKE} -s -C ${BUILD} ${MAKECMDGOALS} + +BOOSTRAP_ARGS := --systemc $(foreach SOLVER, $(CRAVE_SOLVERS), -b $(SOLVER)) + +ifdef CMAKE + BOOSTRAP_ARGS += --cmake=${CMAKE} +endif + +ifdef CACHE + BOOSTRAP_ARGS += --cache ${CACHE} +endif + +${BUILD}/Makefile: + ./bootstrap.sh -d ${SRCDIR}/deps ${BUILD} ${BOOSTRAP_ARGS} + +.PHONY: update +update: + git pull + git submodule update + +.PHONY: distclean +distclean: + rm -rf $(BUILD) + +.PHONY: doxygen +doxygen: + doxygen doc/Doxyfile + +$(BUILD)/deps-clean: + CRAVE_OFFLINE_BUILD=OFF ./bootstrap.sh --boost=do/not/download -d ${DEPS_CLEAN} --download-only ${BOOSTRAP_ARGS} + +.PHONY: cleandeps +cleandeps: + rm -rf ${DEPS_CLEAN} + +.PHONY: package_deps +package_deps: $(BUILD)/deps-clean + cd $(BUILD) && tar -czf crave_package_deps.tar.gz deps-clean && cd $(SRCDIR) + +.PHONY: lcov_with_bc +lcov_with_bc: + @rm ${LCOVDIR} -Rf + @mkdir ${LCOVDIR} + @lcov --quiet --capture --rc lcov_branch_coverage=1 --directory ${BUILD} --base-directory ${SRCDIR}/src --no-external --output-file ${LCOVDIR}/coverage.info + @genhtml ${LCOVDIR}/coverage.info --branch-coverage --output-directory ${LCOVDIR} + +.PHONY: lcov +lcov: + @rm ${LCOVDIR} -Rf + @mkdir ${LCOVDIR} + @lcov --quiet --capture --directory ${BUILD} --base-directory ${SRCDIR}/src --no-external --output-file ${LCOVDIR}/coverage.info + @genhtml ${LCOVDIR}/coverage.info --output-directory ${LCOVDIR} + diff --git a/crave/README.md b/crave/README.md new file mode 100644 index 0000000..37a75c4 --- /dev/null +++ b/crave/README.md @@ -0,0 +1,122 @@ + Constrained RAndom Verification Enviroment - CRAVE +==================================================== + +For feedback and bug reports: crave@systemc-verification.org + + Preparations +-------------- + +When installing directly from the git repository some additional steps are +required. These are not necessary when using the packaged source code. Both +require some packages to be installed on the system. + +To get CRAVE from the git repository execute the following commands: + + git clone --recursive [crave-git-URL] + +This will download crave and its direct dependencies. External dependencies +will be downloaded by the bootstrap script when executing make. + +Please install the following packages to ensure the external packages will +build correctly: + +* zlib and bzip2 development libraries (e.g. zlib1g-dev, libbz2-dev) +* CMake (at least v2.8.9) + + + SystemC Support +----------------- + +You need to set the environment variable SYSTEMC_HOME to your SystemC installation +directory (which also must contains a static library). Otherwise, CRAVE will automatically +download and build systemc-2.3.1 from GitHub. + + + Other external dependencies +----------------------- + +CRAVE uses the following external dependencies: + +* [Boost] - you need at least version 1.50.0, set the environment variable BOOST_ROOT to your +boost installation directory (e.g. /usr) or CRAVE will automatically download and build boost-1.55.0. +For faster build, it is recommended to choose the first option. +* [Glog] - similarly, set GLOG_ROOT or CRAVE will automatically download and build glog. GLOG_ROOT can be set to an invalid path (e.g. 'export GLOG_ROOT=do/not/use') to disable Glog. In this case a very simple logger will be used instead. +* [Boolector] - Boolector can be disabled by via the environment variable CRAVE_SOLVERS (see below). +* [CUDD] - CUDD can be disabled by by via the environment variable CRAVE_SOLVERS (see below), but this is not recommended. +* [SWORD] - SWORD can be enabled by via the environment variable CRAVE_SOLVERS (see below). It is only available as pre-compiled binary for Linux x86 and x86_64 and might be incompatible with some platforms such as RHEL 5. +* [CVC4] - CVC4 can be enabled by by via the environment variable CRAVE_SOLVERS (see below). Building CVC4 takes considerable time so it is disabled by default. +* [Z3] - Z3 can be enabled by via the environment variable CRAVE_SOLVERS (see below). Building Z3 takes considerable time so it is disabled by default. +* [STP] - STP can be enabled by via the environment variable CRAVE_SOLVERS (see below). Building STP takes considerable time so it is disabled by default. +* [Yices2] - Yices2 can be enabled by via the environment variable CRAVE_SOLVERS (see below). Building Yices2 takes considerable time so it is disabled by default. + +If the environment variable CRAVE_SOLVERS is not set, Boolector and CUDD will be used. +For example, to build CRAVE with CUDD, STP and Z3, call 'export CRAVE_SOLVERS='cudd stp z3'' before 'make'. +Please make sure that at least one SMT backend is enabled. + + + Build and install CRAVE +------------------------- + +1. Call 'make' to build CRAVE, the dependencies should + automatically download and build. +2. Call 'make test', all tests should pass (with very few execeptions). +3. Call 'make install'. + +To clean CRAVE you can delete the build directory (e.g. 'rm -Rf build') and call 'make' again. + + Examples +---------- + +You will find several examples in the examples/ directory. These will +demonstrate the core features of CRAVE using CRAVE-2.0 API (subdirectory crave2_api/) +as well as the new experimental API (subdirectory experimental_api/, requires compiler +support for C++11). The basic examples are available in both APIs as listed below: + + * ex1_seed_dist : global seed and simple distribution. + * ex2_constr_ref : constraints and references. + * ex3_inh_soft_next : constraint inheritance, soft constraints and custom next()/randomize(). + * ex4_constr_mng : enable/disable constraints. + * ex5_vec_constr : vector constraints. + * ex6_inline_gen : inline generator. + * ex7_rand_enum : constraints on enumeration types. + * ex8_make_expression : expression layer usage. + +to execute these examples look into the build/examples directory. +See also the other examples and the test cases in crave/tests, which cover all implemented features. + + Documentation +------------------------- + +The doxygen documentation can be generated in doc/crave-doxygen by calling 'make doxygen'. + + Configuration file +----------------------- + +CRAVE will try to find and if not found, create a configuration file crave.cfg in +the executing directory. The default configuration is shown in the following: + + + auto + 0 + + + crave + ./logs + 2 + 100 + + +The value 'auto' means that CRAVE will automatically select a backend among +the available SMT solvers. Other possible values are for example 'boolector', 'sword', 'z3', etc. +Change the seed to a positive integer, if you want to use this integer as the fixed seed. +For further information, especially on the logger, please refer to the doxygen documentation. + +[Boost]: http://www.boost.org +[CUDD]: http://vlsi.colorado.edu/~fabio/CUDD/ +[SWORD]: http://www.informatik.uni-bremen.de/agra/eng/sword.php +[Z3]: https://github.com/Z3Prover/z3 +[Boolector]: http://fmv.jku.at/boolector/ +[CVC4]: http://cvc4.cs.nyu.edu +[Yices2]: http://yices.csl.sri.com/ +[STP]: https://github.com/stp/stp +[Glog]: https://code.google.com/p/google-glog/ diff --git a/crave/bootstrap.sh b/crave/bootstrap.sh new file mode 100755 index 0000000..ef6a9f9 --- /dev/null +++ b/crave/bootstrap.sh @@ -0,0 +1,270 @@ +#!/bin/bash +SRC_DIR=$( cd $(dirname $0) && pwd) + +BUILD_DIR=$PWD/build +DEPS=$PWD/deps + +BOOST=boost-1_55_0-fs + +GLOG=glog-git-0.3.3 +SYSTEMC=systemc-2.3.1 + +BOOLECTOR=boolector-2.2.0 +CVC4=cvc4-unstable +STP=stp-git-basic +SWORD=SWORD-1.1 +YICES2=yices-2.5.1 +Z3=Z3-4.6.0 + +MINISAT=minisat-git +LINGELING=lingeling-ayv-86bf266-140429 + +CUDD=cudd-3.0.0 + +CMAKE=cmake +BUILD_CMAKE="no" +CMAKE_PACKAGE=cmake-2.8.4 + +CMAKE_ARGS=" + -DmetaSMT_ENABLE_TESTS=off +" + + +usage() { + cat << EOF +$0 sets up a CRAVE build folder. +usage: $0 [--free] [--non-free] build + --boost=/p/t/b use this version of the Boost libraries + --backend val use the backend val, following backends can be + -b val activated: boolector, cvc4, stp, sword, yices2, z3 and cudd + --systemc build SystemC + --systemc=/p/t/s use this version of SystemC + --clean delete build folder before creating a new one + --deps build dependencies in this folder + -d can be shared in different projects + --download-only Only download dependencies but not build. Might override other options. + --install configure cmake to install to this directory + -i + --mode the CMake build type to configure, types are + -m RELEASE, MINSIZEREL, RELWITHDEBINFO, DEBUG + -Dvar=val pass options to cmake + --cmake=/p/t/c use this version of cmake + --cmake build a custom cmake version + --cache specify the path to the sources, if a + -ca download is not wanted + -j number of threads to compile the dependencies + the folder to setup the build environment in +EOF + exit 1 +} + +if ! [[ "$1" ]]; then + usage +fi + + +while [[ "$@" ]]; do + case $1 in + --usage|--help|-h) usage;; + --boost=*) BOOST=""; BOOST_ROOT="${1#--boost=}";; + --backend|-b) BACKENDS="$2 $BACKENDS"; shift;; + --systemc=*) WITH_SYSTEMC="yes"; SYSTEMC_HOME="${1#--systemc=}";; + --systemc) WITH_SYSTEMC="yes";; + --deps|-d) DEPS="$2"; shift;; + --install|-i) INSTALL="$2"; shift;; + --mode|-m) CMAKE_ARGS="$CMAKE_ARGS -DCMAKE_BUILD_TYPE=$2"; shift;; + -D*) CMAKE_ARGS="$CMAKE_ARGS $1";; + --download-only) DL_ONLY=-d;; + --clean|-c) CLEAN="true";; + --cmake=*) CMAKE="${1#--cmake=}";; + --cmake) BUILD_CMAKE="yes";; + --cache|-ca) CACHE="$2"; shift;; + -j) NUM_THREADS=$2; shift;; + *) ## assume build dir + BUILD_DIR="$1" ;; + esac + shift; +done + +if [[ "$CLEAN" ]]; then + rm -rf $BUILD_DIR +fi + +BACKENDS="${BACKENDS:-boolector cvc4 stp sword yices2 z3 cudd}" +echo "activated backends are: $BACKENDS" + +if [[ "$CRAVE_OFFLINE_BUILD" = "ON" ]]; then + # Check variables + echo "Offline build activated." + if [[ -z "$BOOST_ROOT" ]]; then + echo "BOOST_ROOT must be set for offline build." + exit 1; + fi + if [[ -z "$SYSTEMC_HOME" ]]; then + echo "SYSTEMC_HOME must be set for offline build." + exit 1; + fi + if [ "$BUILD_CMAKE" = "yes" ]; then + echo "Building cmake in offline build is not allowed." + exit 1; + fi + + if ! [ -f crave_package_deps.tar.gz ]; then + echo "Could not find the dependency cache crave_package_deps.tar.gz. Please provide crave_package_deps.tar.gz or switch to online build" + exit 1; + fi + + mkdir -p $DEPS + tar --strip-components=1 -C $DEPS -xzf crave_package_deps.tar.gz + CACHE=$DEPS +else + echo "Regular build activated. Dependencies will be downloaded and built automatically." + echo "Offline build can be activated by setting the environment variable CRAVE_OFFLINE_BUILD to ON." +fi + +DIS_BOOLECTOR="yes" +DIS_CVC4="yes" +DIS_STP="yes" +DIS_SWORD="yes" +DIS_YICES2="yes" +DIS_Z3="yes" + +DIS_CUDD="yes" + +for BACKEND in $BACKENDS +do + if [[ "$BACKEND" = "boolector" ]]; then + REQUIRES="$LINGELING $BOOLECTOR $REQUIRES" + CMAKE_ARGS="-DmetaSMT_USE_Boolector=on $CMAKE_ARGS" + DIS_BOOLECTOR="no" + fi + if [[ "$BACKEND" = "cvc4" ]]; then + REQUIRES="$CVC4 $REQUIRES" + CMAKE_ARGS="-DmetaSMT_USE_CVC4=on $CMAKE_ARGS" + DIS_CVC4="no" + fi + if [[ "$BACKEND" = "stp" ]]; then + REQUIRES="$STP $REQUIRES" + CMAKE_ARGS="-DmetaSMT_USE_STP=on $CMAKE_ARGS" + DIS_STP="no" + fi + if [[ "$BACKEND" = "sword" ]]; then + REQUIRES="$SWORD $REQUIRES" + CMAKE_ARGS="-DmetaSMT_USE_SWORD=on $CMAKE_ARGS" + DIS_SWORD="no" + fi + if [[ "$BACKEND" = "yices2" ]]; then + REQUIRES="$YICES2 $REQUIRES" + CMAKE_ARGS="-DmetaSMT_USE_YICES2=on $CMAKE_ARGS" + DIS_YICES2="no" + fi + if [[ "$BACKEND" = "z3" ]]; then + REQUIRES="$Z3 $REQUIRES" + CMAKE_ARGS="-DmetaSMT_USE_Z3=on $CMAKE_ARGS" + DIS_Z3="no" + fi + + if [[ "$BACKEND" = "cudd" ]]; then + REQUIRES="$CUDD $REQUIRES" + CMAKE_ARGS="-DmetaSMT_USE_CUDD=on $CMAKE_ARGS" + DIS_CUDD="no" + fi +done + +if [[ "$DIS_BOOLECTOR" = "yes" ]]; then + CMAKE_ARGS="-DmetaSMT_USE_Boolector=off $CMAKE_ARGS" +fi +if [[ "$DIS_CVC4" = "yes" ]]; then + CMAKE_ARGS="-DmetaSMT_USE_CVC4=off $CMAKE_ARGS" +fi +if [[ "$DIS_STP" = "yes" ]]; then + CMAKE_ARGS="-DmetaSMT_USE_STP=off $CMAKE_ARGS" +fi +if [[ "$DIS_SWORD" = "yes" ]]; then + CMAKE_ARGS="-DmetaSMT_USE_SWORD=off $CMAKE_ARGS" +fi +if [[ "$DIS_YICES2" = "yes" ]]; then + CMAKE_ARGS="-DmetaSMT_USE_YICES2=off $CMAKE_ARGS" +fi +if [[ "$DIS_Z3" = "yes" ]]; then + CMAKE_ARGS="-DmetaSMT_USE_Z3=off $CMAKE_ARGS" +fi +if [[ "$DIS_CUDD" = "yes" ]]; then + CMAKE_ARGS="-DmetaSMT_USE_CUDD=off $CMAKE_ARGS" +fi + +mk_and_abs_dir() { + mkdir -p $1 && + cd $1 &>/dev/null && + pwd +} +BUILD_DIR=$(mk_and_abs_dir $BUILD_DIR) && +INSTALL=$(mk_and_abs_dir ${INSTALL:-$BUILD_DIR/root}) && +DEPS=$(mk_and_abs_dir ${DEPS:-$BUILD_DIR}) && + +if [ "$WITH_SYSTEMC" = "yes" ]; then + if [ "$SYSTEMC_HOME" = "" ]; then + REQUIRES="$SYSTEMC $REQUIRES" + SYSTEMC_HOME="$DEPS/$SYSTEMC" + fi +fi +if [ -z "$GLOG_ROOT" ]; then + REQUIRES="$GLOG $REQUIRES" + GLOG_ROOT="$DEPS/$GLOG" +fi && +if [ -z "$BOOST_ROOT" ]; then + REQUIRES="$BOOST $REQUIRES" + BOOST_ROOT="$DEPS/$BOOST" + export DEPS_BOOST=$BOOST + +fi + +if [ -n "$CACHE" ]; then + CACHE="-c $(mk_and_abs_dir ${CACHE})" +fi + +if ! [ -d dependencies ]; then + # packaged mode + echo "could not find the dependency repository" + exit 2 +fi + +cd dependencies + +if [ "$BUILD_CMAKE" = "yes" ]; then + ./build "$DEPS" $CMAKE_PACKAGE && + CMAKE=$DEPS/$CMAKE_PACKAGE/bin/cmake +fi + +if [ -x "$CMAKE" ]; then + export PATH="$(dirname $CMAKE):$PATH" +fi + +if ! ./build -j ${NUM_THREADS:-1} $DL_ONLY "$DEPS" $CACHE $REQUIRES; then + echo "Building dependencies failed. Please see above for error" + exit 3 +fi + +cd $BUILD_DIR && + +PREFIX_PATH=$(echo " $REQUIRES"| sed "s@[ ^] *@;$DEPS/@g") + +eval_echo() { + $@ + echo "$@" +} + +if [ -z "$DL_ONLY" ]; then + cd $BUILD_DIR + eval_echo $CMAKE $SRC_DIR \ + -DCMAKE_INSTALL_PREFIX="$INSTALL" \ + -DCMAKE_PREFIX_PATH="$PREFIX_PATH" \ + $CMAKE_ARGS \ + -DBOOST_ROOT="$BOOST_ROOT" \ + -DWITH_SYSTEMC="$WITH_SYSTEMC" \ + -DSYSTEMC_HOME="$SYSTEMC_HOME" \ + -DGLOG_ROOT="$GLOG_ROOT" + echo "finished bootstrap, you can now call make in $BUILD_DIR" +fi + + diff --git a/crave/cmake/FindGLOG.cmake b/crave/cmake/FindGLOG.cmake new file mode 100644 index 0000000..a5d8086 --- /dev/null +++ b/crave/cmake/FindGLOG.cmake @@ -0,0 +1,60 @@ +#______________________________________________________________________________ +# +# This CMake package creates a Glog target +#______________________________________________________________________________ +# +# GLOG_FOUND - system has Glog +# GLOG_INCLUDE_DIRS - the Glog include directory +# GLOG_LIBRARIES - Link these to use Glog +# GLOG_DEFINITIONS - Compiler switches required for using Glog + +IF(GLOG_LIBRARIES AND GLOG_INCLUDE_DIRS) + SET(GLOG_FOUND TRUE) +ELSE(GLOG_LIBRARIES AND GLOG_INCLUDE_DIRS) + FIND_PATH(GLOG_INCLUDE_DIR + HINTS + $ENV{GLOG_ROOT}/include + ${GLOG_ROOT}/include + NAMES + glog/logging.h + PATHS + /usr/include + /usr/local/include + /opt/include/glog/include + PATH_SUFFIXES + glog + ) + + FIND_LIBRARY(GLOG_LIBRARY + HINTS + $ENV{GLOG_ROOT}/lib + ${GLOG_ROOT}/lib + NAMES + glog + PATHS + /usr/lib + /usr/local/lib + /opt/include/glog/lib + ) + +SET(GLOG_INCLUDE_DIRS ${GLOG_INCLUDE_DIR}) +SET(GLOG_LIBRARIES ${GLOG_LIBRARY}) + +IF(GLOG_INCLUDE_DIRS AND GLOG_LIBRARIES) + SET(GLOG_FOUND TRUE) +ENDIF(GLOG_INCLUDE_DIRS AND GLOG_LIBRARIES) + +IF(GLOG_FOUND) + IF(NOT Glog_FIND_QUIETLY) + MESSAGE(STATUS "Found Glog: ${GLOG_LIBRARIES}") + ENDIF(NOT Glog_FIND_QUIETLY) +ELSE(GLOG_FOUND) + IF(Glog_FIND_REQUIRED) + MESSAGE(FATAL_ERROR "Could not find Glog") + ENDIF(Glog_FIND_REQUIRED) +ENDIF(GLOG_FOUND) + +# show the GLOG_INCLUDE_DIRS and GLOG_LIBRARIES variables only in the advanced view +MARK_AS_ADVANCED(GLOG_INCLUDE_DIRS GLOG_LIBRARIES) + +ENDIF(GLOG_LIBRARIES AND GLOG_INCLUDE_DIRS) diff --git a/crave/cmake/FindSystemC.cmake b/crave/cmake/FindSystemC.cmake new file mode 100644 index 0000000..1f9a9d4 --- /dev/null +++ b/crave/cmake/FindSystemC.cmake @@ -0,0 +1,57 @@ +#______________________________________________________________________________ +# +# This CMake package creates a SystemC target +#______________________________________________________________________________ +# +# SystemC_FOUND - system has SystemC +# SystemC_INCLUDE_DIRS - the SystemC include directory +# SystemC_LIBRARIES - Link these to use SystemC + +IF(SystemC_LIBRARIES AND SystemC_INCLUDE_DIRS) + SET(SystemC_FOUND TRUE) +ELSE(SystemC_LIBRARIES AND SystemC_INCLUDE_DIRS) + FIND_PATH(SystemC_INCLUDE_DIR + HINTS + ${SYSTEMC_HOME}/include + $ENV{SYSTEMC_HOME}/include + NAMES + systemc.h + ) + + FIND_LIBRARY(SystemC_LIBRARY + HINTS + ${SYSTEMC_HOME}/lib + ${SYSTEMC_HOME}/lib-linux + ${SYSTEMC_HOME}/lib-linux64 + ${SYSTEMC_HOME}/lib-macos + $ENV{SYSTEMC_HOME}/lib + $ENV{SYSTEMC_HOME}/lib-linux + $ENV{SYSTEMC_HOME}/lib-linux64 + $ENV{SYSTEMC_HOME}/lib-mingw64 + $ENV{SYSTEMC_HOME}/lib-mingw-w64 + $ENV{SYSTEMC_HOME}/lib-macos + NAMES + libsystemc.a + ) + +SET(SystemC_INCLUDE_DIRS ${SystemC_INCLUDE_DIR}) +SET(SystemC_LIBRARIES ${SystemC_LIBRARY}) + +IF(SystemC_INCLUDE_DIRS AND SystemC_LIBRARIES) + SET(SystemC_FOUND TRUE) +ENDIF(SystemC_INCLUDE_DIRS AND SystemC_LIBRARIES) + +IF(SystemC_FOUND) + IF(NOT SystemC_FIND_QUIETLY) + MESSAGE(STATUS "Found SystemC: ${SystemC_LIBRARIES}") + ENDIF(NOT SystemC_FIND_QUIETLY) +ELSE(SystemC_FOUND) + IF(SystemC_FIND_REQUIRED) + MESSAGE(FATAL_ERROR "Could not find SystemC") + ENDIF(SystemC_FIND_REQUIRED) +ENDIF(SystemC_FOUND) + +# show the SystemC_INCLUDE_DIRS and SystemC_LIBRARIES variables only in the advanced view +MARK_AS_ADVANCED(SystemC_INCLUDE_DIRS SystemC_LIBRARIES) + +ENDIF(SystemC_LIBRARIES AND SystemC_INCLUDE_DIRS) diff --git a/crave/cmake/get_git_version.cmake b/crave/cmake/get_git_version.cmake new file mode 100644 index 0000000..c027f00 --- /dev/null +++ b/crave/cmake/get_git_version.cmake @@ -0,0 +1,22 @@ + +function( get_git_version OUTPUT_VARIABLE TAG_PREFIX ) + + find_package(Git QUIET) + if( GIT_FOUND ) + execute_process( + COMMAND ${GIT_EXECUTABLE} describe --tags --match "${TAG_PREFIX}*" HEAD + OUTPUT_VARIABLE _GIT_VERSION_DESCRIPTION + OUTPUT_STRIP_TRAILING_WHITESPACE + WORKING_DIRECTORY ${PROJECT_SOURCE_DIR} + ERROR_QUIET + RESULT_VARIABLE _GIT_DESCRIBE_RESULT + ) + + if(_GIT_DESCRIBE_RESULT EQUAL 0) + string(REPLACE "${TAG_PREFIX}" "" _git_VERSiON "${_GIT_VERSION_DESCRIPTION}") + endif() + + set(${OUTPUT_VARIABLE} ${_git_VERSiON} PARENT_SCOPE) + endif() + +endfunction(get_git_version) diff --git a/crave/dependencies/Python-2.7.10/setup.sh b/crave/dependencies/Python-2.7.10/setup.sh new file mode 100644 index 0000000..e163bb1 --- /dev/null +++ b/crave/dependencies/Python-2.7.10/setup.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +version=2.7.10 + +source "$base_dir/Python-2.7.10/shared.sh" + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/Python-2.7.10/shared.sh b/crave/dependencies/Python-2.7.10/shared.sh new file mode 100644 index 0000000..73c5f70 --- /dev/null +++ b/crave/dependencies/Python-2.7.10/shared.sh @@ -0,0 +1,35 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + error '$build is undefined' +fi + +package=Python +source=${package}-$version.tar.xz +build_dir=$build/${package}-$version +url=https://www.python.org/ftp/python/$version/$source + +unpack() { + cd $cache && + message "unpacking $package" && + tar -Jxvf $source && + message "finished unpacking $package" +} + +pre_build() { + rm -rf $build_dir && + mv -f $cache/${package}-$version $build_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + ./configure --prefix=$target && + make -j$num_threads && + make -j$num_threads install +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/Python-3.3.6/setup.sh b/crave/dependencies/Python-3.3.6/setup.sh new file mode 100644 index 0000000..0400757 --- /dev/null +++ b/crave/dependencies/Python-3.3.6/setup.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +version=3.3.6 + +source "$base_dir/Python-2.7.10/shared.sh" + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/README b/crave/dependencies/README new file mode 100644 index 0000000..aecc6c9 --- /dev/null +++ b/crave/dependencies/README @@ -0,0 +1,7 @@ +a set of scripts to create and/or build various external libraries. + +call + ./build /some/target/folder "package-version" "package-version" ... +to install the packages to that directory or call setup_cmake_src with +the same parameters to setup directories suitable for inclusion in cmake +projects. diff --git a/crave/dependencies/SWORD-1.1/SWORDConfig.cmake b/crave/dependencies/SWORD-1.1/SWORDConfig.cmake new file mode 100644 index 0000000..f1389f6 --- /dev/null +++ b/crave/dependencies/SWORD-1.1/SWORDConfig.cmake @@ -0,0 +1,7 @@ +set(SWORD_VERSION) +get_filename_component(SWORD_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(SWORD_BIN_DIRS ${SWORD_DIR}/bin ) +set(SWORD_BIN_DIR ${SWORD_BIN_DIRS} ) +set(SWORD_INCLUDE_DIRS ${SWORD_DIR}/include ) +set(SWORD_INCLUDE_DIR ${SWORD_INCLUDE_DIRS} ) +set(SWORD_LIBRARIES ${SWORD_DIR}/lib/libsword.a ) diff --git a/crave/dependencies/SWORD-1.1/setup.sh b/crave/dependencies/SWORD-1.1/setup.sh new file mode 100755 index 0000000..d242400 --- /dev/null +++ b/crave/dependencies/SWORD-1.1/setup.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +version=1.1 + +cmake_files_dir=$base_dir/SWORD-1.1 + +source $base_dir/SWORD-1.1/shared.sh + +# vim: ts=2 sw=2 et \ No newline at end of file diff --git a/crave/dependencies/SWORD-1.1/shared.sh b/crave/dependencies/SWORD-1.1/shared.sh new file mode 100644 index 0000000..d714b05 --- /dev/null +++ b/crave/dependencies/SWORD-1.1/shared.sh @@ -0,0 +1,46 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=SWORD +bits=32 + +case "$ARCH" in + i?86) source="sword-${version}-32bit.tar.gz"; bits=32;; + x86_64|x86-64) source="sword-${version}-64bit.tar.gz"; bits=64;; + *) error "$package not avaiable for architechture $ARCH"; ;; +esac + +build_dir=$build/${source/.tar.gz} +url=http://www.informatik.uni-bremen.de/agra/doc/software/$source + +unpack() { + cd $cache && + tar -xf $source && + rm -rf $build_dir && + mv -f $cache/sword-$version-${bits}bit $build_dir +} + +pre_build() { + cd $build_dir && + install_cmake_files $cmake_files_dir && + sed -i 1s/SWORD_VERSION/"SWORD_VERSION $version"/ $build_dir/SWORDConfig.cmake +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + mkdir -p $target && + cp -r $build_dir/* $target +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/Z3-4.6.0/setup.sh b/crave/dependencies/Z3-4.6.0/setup.sh new file mode 100644 index 0000000..6cecc8e --- /dev/null +++ b/crave/dependencies/Z3-4.6.0/setup.sh @@ -0,0 +1,8 @@ +#!/bin/sh + +version=4.6.0 +branch=z3-4.6.0 + +cmake_files_dir=$base_dir/Z3-git + +source $base_dir/Z3-git/shared.sh diff --git a/crave/dependencies/Z3-git/Z3Config.cmake b/crave/dependencies/Z3-git/Z3Config.cmake new file mode 100644 index 0000000..70e063a --- /dev/null +++ b/crave/dependencies/Z3-git/Z3Config.cmake @@ -0,0 +1,9 @@ +get_filename_component(Z3_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(Z3_BIN_DIRS ${Z3_DIR}/bin ) +set(Z3_INCLUDE_DIRS ${Z3_DIR}/include ) +set(Z3_INCLUDE_DIR ${Z3_INCLUDE_DIRS} ) +if(NOT MINGW) +set(Z3_LIBRARIES ${Z3_DIR}/lib/libz3.a ) +else () +set(Z3_LIBRARIES ${Z3_DIR}/lib/libz3.lib ) +endif() diff --git a/crave/dependencies/Z3-git/setup.sh b/crave/dependencies/Z3-git/setup.sh new file mode 100644 index 0000000..14b9272 --- /dev/null +++ b/crave/dependencies/Z3-git/setup.sh @@ -0,0 +1,8 @@ +#!/bin/sh + +version=git +branch=master + +cmake_files_dir=$base_dir/Z3-git + +source $base_dir/Z3-git/shared.sh diff --git a/crave/dependencies/Z3-git/shared.sh b/crave/dependencies/Z3-git/shared.sh new file mode 100644 index 0000000..efc4939 --- /dev/null +++ b/crave/dependencies/Z3-git/shared.sh @@ -0,0 +1,48 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=Z3 +source=nosourcefile +build_dir=$build/$package-$version +url='https://github.com/Z3Prover/z3.git' + +download() { + mkdir -p $cache/$package-$version && + cd $cache/$package-$version && + if [ -d .git ]; then + git pull + else + git clone $url . + git checkout $branch + fi +} + +unpack() { + cp -R $cache/$package-$version $build_dir +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd "$build_dir" && + ./configure --staticlib --prefix="$target" && + cd build && + make -j $num_threads && + make install && + install_cmake_files $cmake_files_dir && + cp Z3Config.cmake "$target" +} diff --git a/crave/dependencies/aiger-20071012/CMakeLists.txt b/crave/dependencies/aiger-20071012/CMakeLists.txt new file mode 100644 index 0000000..61d2177 --- /dev/null +++ b/crave/dependencies/aiger-20071012/CMakeLists.txt @@ -0,0 +1,51 @@ +project(Aiger) + +cmake_minimum_required(VERSION 2.8) + +set(STATIC_OR_SHARED SHARED CACHE STRING "Build STATIC or SHARED libaries") + + +add_library(Aiger + ${STATIC_OR_SHARED} + aiger.c +) + + +file(WRITE ${PROJECT_BINARY_DIR}/AigerConfig.cmake +"set(Aiger_FOUND 1) +set(Aiger_VERSION 20071012) +get_filename_component(Aiger_CONFIG_DIR "\${CMAKE_CURRENT_LIST_FILE}" PATH) +set(Aiger_INCLUDE_DIR \${Aiger_CONFIG_DIR}/../../include) +include("\${Aiger_CONFIG_DIR}/Aiger.cmake" ) +") +file(WRITE ${PROJECT_BINARY_DIR}/AigerConfigVersion.cmake +"if(\"\${PACKAGE_FIND_VERSION}\" VERSION_EQUAL 20071012) + set(PACKAGE_VERSION_EXACT 1) + set(PACKAGE_VERSION_COMPATIBLE 1) +endif(\"\${PACKAGE_FIND_VERSION}\" VERSION_EQUAL 20071012) +") +## create libAiger config file for internal use +file(WRITE ${PROJECT_BINARY_DIR}/Aiger.cmake +"set(Aiger_INCLUDE_DIR + ${PROJECT_SOURCE_DIR} +) +") +## export target with install +INSTALL( FILES + ${PROJECT_BINARY_DIR}/AigerConfig.cmake + ${PROJECT_BINARY_DIR}/AigerConfigVersion.cmake + DESTINATION share/Aiger) +install(EXPORT Aiger DESTINATION share/Aiger) + +install(TARGETS + Aiger + EXPORT Aiger + LIBRARY DESTINATION lib + RUNTIME DESTINATION bin + ARCHIVE DESTINATION lib +) + +install(FILES + aiger.h + DESTINATION include +) diff --git a/crave/dependencies/aiger-20071012/setup.sh b/crave/dependencies/aiger-20071012/setup.sh new file mode 100755 index 0000000..3854aa7 --- /dev/null +++ b/crave/dependencies/aiger-20071012/setup.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +version=20071012 + +cmake_files_dir=$base_dir/aiger-20071012 + +source $base_dir/aiger-20071012/shared.sh + +# vim: ts=2 sw=2 et \ No newline at end of file diff --git a/crave/dependencies/aiger-20071012/shared.sh b/crave/dependencies/aiger-20071012/shared.sh new file mode 100644 index 0000000..63374cf --- /dev/null +++ b/crave/dependencies/aiger-20071012/shared.sh @@ -0,0 +1,43 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + + +package=aiger + +source=$package-$version.zip +build_dir=$build/$package-$version +url=http://fmv.jku.at/aiger/$source + +unpack() { + cd $cache && + unzip -o $source && + rm -rf build_dir && + mv -f $cache/$package-$version $build_dir +} + +pre_build() { + cd $build_dir && + install_cmake_files $cmake_files_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + mkdir -p build && + cd build && + cmake .. -DCMAKE_INSTALL_PREFIX=$target && + make install +} + +# vim: ts=2 sw=2 et \ No newline at end of file diff --git a/crave/dependencies/boolector-2.2.0/0014-workaround-on-shifting-conditions.patch b/crave/dependencies/boolector-2.2.0/0014-workaround-on-shifting-conditions.patch new file mode 100644 index 0000000..70a55fa --- /dev/null +++ b/crave/dependencies/boolector-2.2.0/0014-workaround-on-shifting-conditions.patch @@ -0,0 +1,87 @@ +--- a/boolector.c 2015-11-29 18:40:12.000000000 +0100 ++++ b/boolector.c 2016-10-21 16:20:58.480747682 +0200 +@@ -1947,12 +1947,27 @@ + BTOR_ABORT_NOT_BV_BOOLECTOR (e0); + BTOR_ABORT_NOT_BV_BOOLECTOR (e1); + len = btor_get_exp_width (btor, e0); ++ int len1= btor_get_exp_width (btor, e1); ++ if( !btor_is_power_of_2_util (len) ++ || btor_log_2_util (len) != btor_get_exp_width (btor, e1) ) ++ { ++ int tolen = btor_next_power_of_2_util(len); ++ int loglen = btor_log_2_util(tolen); ++ res = btor_slice_exp(btor, btor_sll_exp ( btor, ++ btor_uext_exp(btor, e0, tolen-len), ++ (len1 > loglen) ? btor_slice_exp(btor, e1, loglen-1, 0): e1 ), ++ len-1, 0); ++ ++ } ++ else ++ { + BTOR_ABORT_BOOLECTOR (!btor_is_power_of_2_util (len), + "bit-width of 'e0' must be a power of 2"); + BTOR_ABORT_BOOLECTOR ( + btor_log_2_util (len) != btor_get_exp_width (btor, e1), + "bit-width of 'e1' must be equal to log2(bit-width of 'e0')"); + res = btor_sll_exp (btor, e0, e1); ++ } + inc_exp_ext_ref_counter (btor, res); + BTOR_TRAPI_RETURN_NODE (res); + #ifndef NDEBUG +@@ -1980,12 +1995,27 @@ + BTOR_ABORT_NOT_BV_BOOLECTOR (e0); + BTOR_ABORT_NOT_BV_BOOLECTOR (e1); + len = btor_get_exp_width (btor, e0); ++ int len1= btor_get_exp_width (btor, e1); ++ if( !btor_is_power_of_2_util (len) ++ || btor_log_2_util (len) != btor_get_exp_width (btor, e1) ) ++ { ++ int tolen = btor_next_power_of_2_util(len); ++ int loglen = btor_log_2_util(tolen); ++ res = btor_slice_exp(btor, btor_srl_exp ( btor, ++ btor_uext_exp(btor, e0, tolen-len), ++ (len1 > loglen) ? btor_slice_exp(btor, e1, loglen-1, 0): e1 ), ++ len-1, 0); ++ ++ } ++ else ++ { + BTOR_ABORT_BOOLECTOR (!btor_is_power_of_2_util (len), + "bit-width of 'e0' must be a power of 2"); + BTOR_ABORT_BOOLECTOR ( + btor_log_2_util (len) != btor_get_exp_width (btor, e1), + "bit-width of 'e1' must be equal to log2(bit-width of 'e0')"); + res = btor_srl_exp (btor, e0, e1); ++ } + inc_exp_ext_ref_counter (btor, res); + BTOR_TRAPI_RETURN_NODE (res); + #ifndef NDEBUG +@@ -2013,12 +2043,28 @@ + BTOR_ABORT_NOT_BV_BOOLECTOR (e0); + BTOR_ABORT_NOT_BV_BOOLECTOR (e1); + len = btor_get_exp_width (btor, e0); ++ int len1= btor_get_exp_width (btor, e1); ++ if( !btor_is_power_of_2_util (len) ++ || btor_log_2_util (len) != btor_get_exp_width (btor, e1) ) ++ { ++ int tolen = btor_next_power_of_2_util(len); ++ int loglen = btor_log_2_util(tolen); ++ res = btor_slice_exp(btor, btor_sra_exp ( btor, ++ btor_uext_exp(btor, e0, tolen-len), ++ (len1 > loglen) ? btor_slice_exp(btor, e1, loglen-1, 0): e1 ), ++ len-1, 0); ++ ++ } ++ else ++ { ++ len = btor_get_exp_width (btor, e0); + BTOR_ABORT_BOOLECTOR (!btor_is_power_of_2_util (len), + "bit-width of 'e0' must be a power of 2"); + BTOR_ABORT_BOOLECTOR ( + btor_log_2_util (len) != btor_get_exp_width (btor, e1), + "bit-width of 'e1' must be equal to log2(bit-width of 'e0')"); + res = btor_sra_exp (btor, e0, e1); ++ } + inc_exp_ext_ref_counter (btor, res); + BTOR_TRAPI_RETURN_NODE (res); + #ifndef NDEBUG diff --git a/crave/dependencies/boolector-2.2.0/CMakeLists.txt b/crave/dependencies/boolector-2.2.0/CMakeLists.txt new file mode 100644 index 0000000..3e007bb --- /dev/null +++ b/crave/dependencies/boolector-2.2.0/CMakeLists.txt @@ -0,0 +1,145 @@ +project(Boolector) + +cmake_minimum_required(VERSION 2.8) + +find_package(Lingeling REQUIRED) +include_directories( ${Lingeling_INCLUDE_DIR} ) + +find_package(MiniSat REQUIRED) +include_directories( ${MiniSat_INCLUDE_DIR} ) + +set(STATIC_OR_SHARED SHARED CACHE STRING "Build STATIC or SHARED libaries") + +set(OS $ENV{HOSTNAME}) +if("${CMAKE_VERSION}" VERSION_GREATER 2.8.10) + string(TIMESTAMP COMPILED_TIMESTAMP) +endif() + +set(BTOR_C_FLAGS "-DBTOR_USE_LINGELING -DBTOR_USE_MINISAT -DBTOR_ENABLE_BETA_REDUCTION_PROBING") + +set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -DNDEBUG -DNBTORLOG ${BTOR_C_FLAGS}") + +set(SRC_PREFIX boolector-src) + +file(READ ${CMAKE_CURRENT_SOURCE_DIR}/${SRC_PREFIX}/VERSION Boolector_VERSION) +configure_file(${CMAKE_CURRENT_SOURCE_DIR}/btorconfig.h.cmake ${CMAKE_CURRENT_BINARY_DIR}/${SRC_PREFIX}/btorconfig.h) + + +include_directories(${CMAKE_CURRENT_SOURCE_DIR}/${SRC_PREFIX}) + +set( libboolector_HEADER +${SRC_PREFIX}/boolector.h +${SRC_PREFIX}/btortypes.h +) + +set( libboolector_SRC +${SRC_PREFIX}/boolector.c +${SRC_PREFIX}/btor2horn.c +${SRC_PREFIX}/btoraig.c +${SRC_PREFIX}/btoraigvec.c +${SRC_PREFIX}/btorass.c +${SRC_PREFIX}/btorbeta.c +${SRC_PREFIX}/btorbitvec.c +${SRC_PREFIX}/btorchkclone.c +${SRC_PREFIX}/btorclone.c +${SRC_PREFIX}/btorconst.c +${SRC_PREFIX}/btorcore.c +${SRC_PREFIX}/btordbg.c +${SRC_PREFIX}/btordcr.c +${SRC_PREFIX}/btorexp.c +${SRC_PREFIX}/btorfmt.c +${SRC_PREFIX}/utils/btorhash.c +${SRC_PREFIX}/utils/btorinthash.c +${SRC_PREFIX}/utils/btoriter.c +${SRC_PREFIX}/btormain.c +${SRC_PREFIX}/utils/btormap.c +${SRC_PREFIX}/btormc.c +${SRC_PREFIX}/utils/btormem.c +${SRC_PREFIX}/utils/btormisc.c +${SRC_PREFIX}/btormodel.c +${SRC_PREFIX}/btormsg.c +${SRC_PREFIX}/btoropt.c +${SRC_PREFIX}/utils/btorparamcache.c +${SRC_PREFIX}/btorparse.c +${SRC_PREFIX}/btorprintmodel.c +${SRC_PREFIX}/btorrewrite.c +${SRC_PREFIX}/btorsat.c +${SRC_PREFIX}/btorsort.c +${SRC_PREFIX}/btortrapi.c +${SRC_PREFIX}/utils/btorutil.c +${SRC_PREFIX}/parser/btorsmt2.c +${SRC_PREFIX}/parser/btorsmt.c +${SRC_PREFIX}/parser/btorbtor.c +${SRC_PREFIX}/dumper/btordumpbtor.c +${SRC_PREFIX}/dumper/btordumpsmt.c +${SRC_PREFIX}/dumper/btordumpaig.c +${SRC_PREFIX}/simplifier/btorelimslices.c +${SRC_PREFIX}/simplifier/btorextract.c +${SRC_PREFIX}/simplifier/btormerge.c +${SRC_PREFIX}/simplifier/btorelimapplies.c +${SRC_PREFIX}/simplifier/btorack.c +${SRC_PREFIX}/simplifier/btorskel.c +${SRC_PREFIX}/simplifier/btorunconstrained.c +${SRC_PREFIX}/btorminisat.cc +) + +set_source_files_properties(${SRC_PREFIX}/btorminisat.cc PROPERTIES LANGUAGE C ) + +add_library(Boolector_libboolector + ${STATIC_OR_SHARED} + ${libboolector_SRC} +) +target_link_libraries(Boolector_libboolector ${Lingeling_LIBRARIES} ${MiniSat_LIBRARIES} m) +set_target_properties(Boolector_libboolector PROPERTIES OUTPUT_NAME boolector) + +add_executable(Boolector_boolector + ${SRC_PREFIX}/boolectormain.c +) +target_link_libraries(Boolector_boolector Boolector_libboolector) +SET_TARGET_PROPERTIES( Boolector_boolector PROPERTIES + OUTPUT_NAME boolector +) + +file(WRITE ${PROJECT_BINARY_DIR}/BoolectorConfig.cmake +"set(Boolector_FOUND 1) +set(Boolector_VERSION ${Boolector_VERSION}) +get_filename_component(Boolector_CONFIG_DIR \"\${CMAKE_CURRENT_LIST_FILE}\" PATH) +set(Boolector_INCLUDE_DIR \${Boolector_CONFIG_DIR}/../../include) +set(Boolector_LIBRARIES Boolector_libboolector) +set(Boolector_CXXFLAGS \"${BTOR_C_FLAGS}\") +include(\"\${Boolector_CONFIG_DIR}/Boolector.cmake\" ) +") +file(WRITE ${PROJECT_BINARY_DIR}/BoolectorConfigVersion.cmake +"if(\"\${PACKAGE_FIND_VERSION}\" VERSION_EQUAL ${Boolector_VERSION}) +set(PACKAGE_VERSION_EXACT 1) +set(PACKAGE_VERSION_COMPATIBLE 1) +endif(\"\${PACKAGE_FIND_VERSION}\" VERSION_EQUAL ${Boolector_VERSION}) +") +## create libBoolector config file for internal use +file(WRITE ${PROJECT_BINARY_DIR}/Boolector.cmake +"set(Boolector_INCLUDE_DIR + ${PROJECT_SOURCE_DIR}/include +) +") +## export target with install +INSTALL( FILES + ${PROJECT_BINARY_DIR}/BoolectorConfig.cmake + ${PROJECT_BINARY_DIR}/BoolectorConfigVersion.cmake + DESTINATION share/Boolector) +install(EXPORT Boolector DESTINATION share/Boolector) + +install(TARGETS + Boolector_libboolector + Boolector_boolector + EXPORT Boolector + LIBRARY DESTINATION lib + RUNTIME DESTINATION bin + ARCHIVE DESTINATION lib +) + +install(FILES + ${libboolector_HEADER} + DESTINATION include +) + +# vim: sw=2 ts=2 et: diff --git a/crave/dependencies/boolector-2.2.0/btorconfig.h.cmake b/crave/dependencies/boolector-2.2.0/btorconfig.h.cmake new file mode 100644 index 0000000..ab9c7b0 --- /dev/null +++ b/crave/dependencies/boolector-2.2.0/btorconfig.h.cmake @@ -0,0 +1,9 @@ +#define BTOR_CC "@CMAKE_CXX_COMPILER_ID@" +#define BTOR_CXX "@CMAKE_CXX_COMPILER@" +#define BTOR_CFLAGS "@CMAKE_C_FLAGS@" +#define BTOR_OS "@OS@" +#define BTOR_COMPILED "@COMPILED_TIMESTAMP@") +#define BTOR_RELEASED "Fri Mar 6 13:49:55 CET 2015" +#define BTOR_VERSION "@Bollector_VERSION@" +#define BTOR_ID "1dd339d27a93ba49b69aa0808f127005dee6c8fd" + diff --git a/crave/dependencies/boolector-2.2.0/lingeling_include_path.patch b/crave/dependencies/boolector-2.2.0/lingeling_include_path.patch new file mode 100644 index 0000000..ec851b5 --- /dev/null +++ b/crave/dependencies/boolector-2.2.0/lingeling_include_path.patch @@ -0,0 +1,49 @@ +*** a/btorsat.c 2015-11-29 18:40:12.000000000 +0100 +--- btorsat.c 2016-03-07 19:28:35.821854674 +0100 +*************** +*** 16,22 **** + #endif + + #ifdef BTOR_USE_LINGELING +! #include "lglib.h" + #endif + + #ifdef BTOR_USE_MINISAT +--- 16,22 ---- + #endif + + #ifdef BTOR_USE_LINGELING +! #include + #endif + + #ifdef BTOR_USE_MINISAT +*** a/btorsat.h 2016-03-07 19:40:34.149416668 +0100 +--- btorsat_patch.h 2016-03-07 19:41:24.373665717 +0100 +*************** +*** 83,89 **** + }; + + #if defined(BTOR_USE_LINGELING) +! #include "../lingeling/lglib.h" + typedef struct BtorLGL BtorLGL; + + struct BtorLGL +--- 83,89 ---- + }; + + #if defined(BTOR_USE_LINGELING) +! #include + typedef struct BtorLGL BtorLGL; + + struct BtorLGL +--- a/btorminisat.cc 2015-11-29 18:40:12.000000000 +0100 ++++ btorminisat.cc 2016-03-22 12:00:12.878664501 +0100 +@@ -19,7 +19,7 @@ + #define __STDC_FORMAT_MACROS + #endif + +-#include "../minisat/minisat/simp/SimpSolver.h" ++#include + + #include + #include diff --git a/crave/dependencies/boolector-2.2.0/setup.sh b/crave/dependencies/boolector-2.2.0/setup.sh new file mode 100755 index 0000000..2d81546 --- /dev/null +++ b/crave/dependencies/boolector-2.2.0/setup.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +version=2.2.0 + +dependencies="lingeling-ayv-86bf266-140429 minisat-git" + +patches_dir=$base_dir/boolector-$version +cmake_files_dir=$base_dir/boolector-$version + +source $base_dir/boolector-$version/shared.sh diff --git a/crave/dependencies/boolector-2.2.0/shared.sh b/crave/dependencies/boolector-2.2.0/shared.sh new file mode 100644 index 0000000..144d614 --- /dev/null +++ b/crave/dependencies/boolector-2.2.0/shared.sh @@ -0,0 +1,48 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$package_dir is undefined' + exit 1 +fi + +package=boolector +version=2.2.0-with-lingeling-bal +source=$package-$version.tar.bz2 +build_dir=$build/$package-$version +url=http://fmv.jku.at/$package/$source + +boolector_package=boolector-2.2.0-8209e6e-151129 +boolector_prefix=boolector-src + +unpack(){ + cd $cache && + tar -xf $source && + rm -rf $build_dir && + tar -xf $package-$version/archives/$boolector_package.tar.gz -C $package-$version/ && + cd $package-$version && + ln -sf $boolector_package ${boolector_prefix} && + mv -f $cache/$package-$version $build_dir + cd $build_dir/${boolector_prefix} && + patch -p1 -i $patches_dir/lingeling_include_path.patch && + patch -p1 < $patches_dir/0014*.patch +} + +pre_build() { + cd $build_dir && + install_cmake_files $cmake_files_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + cmake_build_install +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/boolector-3.0.0/BoolectorConfig.cmake b/crave/dependencies/boolector-3.0.0/BoolectorConfig.cmake new file mode 100644 index 0000000..93c450e --- /dev/null +++ b/crave/dependencies/boolector-3.0.0/BoolectorConfig.cmake @@ -0,0 +1,6 @@ +get_filename_component(Boolector_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(Boolector_BIN_DIRS ${Boolector_DIR}/bin ) +set(Boolector_INCLUDE_DIRS ${Boolector_DIR}/include/ ) +set(Boolector_INCLUDE_DIR ${Boolector_INCLUDE_DIRS} ) +set(Boolector_LIBRARIES ${Boolector_DIR}/lib/libboolector.a ${Boolector_DIR}/lib/libbtor2parser.a ${Boolector_DIR}/lib/libcadical.a ${Boolector_DIR}/lib/liblgl.a) +set(Boolector_VERSION 3.0.0) diff --git a/crave/dependencies/boolector-3.0.0/setup.sh b/crave/dependencies/boolector-3.0.0/setup.sh new file mode 100644 index 0000000..b11d03d --- /dev/null +++ b/crave/dependencies/boolector-3.0.0/setup.sh @@ -0,0 +1,55 @@ +#!/bin/sh +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=boolector +version=3.0.0 +branch=3.0.0 +source=nosourcefile +build_dir=$build/$package-$version +url='https://github.com/Boolector/boolector.git' + +download() { + mkdir -p $cache/$package-$version && + cd $cache/$package-$version && + if [ -d .git ]; then + git pull + else + git clone $url . + git checkout $branch + git cherry-pick 0f35472c9b171818523dbfad2a7374cbaf45835d + fi +} + +unpack() { + cp -R $cache/$package-$version $build_dir +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd "$build_dir" && + contrib/setup-btor2tools.sh && + contrib/setup-lingeling.sh && + contrib/setup-cadical.sh && + ./configure.sh --prefix "$target" && + cd build && + make -j $num_threads && + make install && + cp ../deps/btor2tools/build/libbtor2parser.a $target/lib && + cp ../deps/cadical/build/libcadical.a $target/lib && + cp ../deps/lingeling/liblgl.a $target/lib && + cp $base_dir/boolector-3.0.0/BoolectorConfig.cmake "$target" +} diff --git a/crave/dependencies/boolector-git/BoolectorConfig.cmake b/crave/dependencies/boolector-git/BoolectorConfig.cmake new file mode 100644 index 0000000..7503e61 --- /dev/null +++ b/crave/dependencies/boolector-git/BoolectorConfig.cmake @@ -0,0 +1,6 @@ +get_filename_component(Boolector_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(Boolector_BIN_DIRS ${Boolector_DIR}/bin ) +set(Boolector_INCLUDE_DIRS ${Boolector_DIR}/include/boolector ) +set(Boolector_INCLUDE_DIR ${Boolector_INCLUDE_DIRS} ) +set(Boolector_LIBRARIES ${Boolector_DIR}/lib/libboolector.a ${Boolector_DIR}/lib/libbtor2parser.a ${Boolector_DIR}/lib/libcadical.a ${Boolector_DIR}/lib/liblgl.a) +set(Boolector_VERSION 3.0.0) diff --git a/crave/dependencies/boolector-git/setup.sh b/crave/dependencies/boolector-git/setup.sh new file mode 100644 index 0000000..b49b59f --- /dev/null +++ b/crave/dependencies/boolector-git/setup.sh @@ -0,0 +1,8 @@ +#!/bin/sh + +version=git +branch=master + +cmake_files_dir=$base_dir/boolector-git + +source $base_dir/boolector-git/shared.sh diff --git a/crave/dependencies/boolector-git/shared.sh b/crave/dependencies/boolector-git/shared.sh new file mode 100644 index 0000000..b0ba8d5 --- /dev/null +++ b/crave/dependencies/boolector-git/shared.sh @@ -0,0 +1,54 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=boolector +source=nosourcefile +build_dir=$build/$package-$version +url='https://github.com/Boolector/boolector.git' + +download() { + mkdir -p $cache/$package-$version && + cd $cache/$package-$version && + if [ -d .git ]; then + git pull + else + git clone $url . + git checkout $branch + fi +} + +unpack() { + cp -R $cache/$package-$version $build_dir +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd "$build_dir" && + contrib/setup-btor2tools.sh && + contrib/setup-lingeling.sh && + contrib/setup-cadical.sh && + ./configure.sh --prefix "$target" && + cd build && + make -j $num_threads && + make install && + cp ../deps/install/lib/libbtor2parser.a $target/lib && + cp ../deps/install/lib/libcadical.a $target/lib && + cp ../deps/install/lib/liblgl.a $target/lib && + install_cmake_files $cmake_files_dir && + cp BoolectorConfig.cmake "$target" +} diff --git a/crave/dependencies/boost-1_55_0-fs/setup.sh b/crave/dependencies/boost-1_55_0-fs/setup.sh new file mode 100644 index 0000000..6c4ec08 --- /dev/null +++ b/crave/dependencies/boost-1_55_0-fs/setup.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +version=1_55_0 + +source "$base_dir/boost-1_55_0-fs/shared.sh" + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/boost-1_55_0-fs/shared.sh b/crave/dependencies/boost-1_55_0-fs/shared.sh new file mode 100644 index 0000000..0adc2d3 --- /dev/null +++ b/crave/dependencies/boost-1_55_0-fs/shared.sh @@ -0,0 +1,58 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + error '$build is undefined' +fi + +package=boost +source=${package}_$version.tar.bz2 +build_dir=$build/${package}_$version +url=http://sourceforge.net/projects/boost/files/boost/${version//_/.}/$source/download + +unpack() { + cd $cache && + message "unpacking $package" && + tar -xf $source && + message "finished unpacking $package" +} + +pre_build() { + rm -rf $build_dir && + mv -f $cache/${package}_$version $build_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + COMMON_OPTS=" + --prefix=$target + --layout=system + variant=release + link=shared + toolset=gcc + " + LIBRARIES=" + --with-filesystem + --with-system + " + cd $build_dir && + test -x bjam || ./bootstrap.sh && + ./bjam -q $COMMON_OPTS $LIBRARIES -j$num_threads install || { + local needed="false" + if [ ! -f /usr/include/zlib.h ] ; then + echo 'zlib.h was not found.' + needed="true" + fi + if [ ! -f /usr/include/bzlib.h ] ; then + echo 'bzlib.h was not found' + needed="true" + fi + if [ "$needed" = "true" ] ; then + echo "Install the packages containing the above header files to compile boost properly." + fi + exit 1 + } +} + diff --git a/crave/dependencies/build b/crave/dependencies/build new file mode 100755 index 0000000..ec1e061 --- /dev/null +++ b/crave/dependencies/build @@ -0,0 +1,115 @@ +#!/bin/bash + +base_dir=$( cd $(dirname $0) && pwd ) +source $base_dir/common.sh + +usage() { + message "usage: " + message " ./build {options} {}" + message " ./build {options} {}" + message " ./build ( --help | -h )" + message "options:" + message " --build build packages in this folder" + message " -b " + message " --cache specify the directory to the sources" + message " -c and skips the downloads" + message " --download only download the packages" + message " -d (won't work together with cache option)" + message " -j defines the number of compiling threads" +} + +if [ $# -lt 2 ]; then + usage + if [[ $1 == *-h* ]]; then + exit 0 + fi + exit 21 +fi + +from_cache="no" +dl_only="no" +num_threads=1 + +while [ -n "$1" ]; do + case $1 in + --build|-b) + build="$(mkdir -p $2 && cd $2 && pwd)" + shift;; + --cache|-c) + if [ $dl_only = "yes" ]; then + message "illegal usage of options" + usage; + exit 22; + fi + from_cache="yes"; + cache="$(mkdir -p $2 && cd $2 && pwd)"; + shift;; + --download|-d) + if [ $from_cache = "yes" ]; then + message "illegal usage of options" + usage; + exit 22; + fi + dl_only="yes"; + cache=${root:-$(mkdir -p $2 && cd $2 && pwd)};; + --help|-h) + usage; + exit 0;; + -j) + num_threads="$2"; + shift;; + -j*) + num_threads="${1/-j}";; + -*) + message "unknown parameter: $1"; + usage; + exit 22;; + *) # first time is target, further are packages + if [ -z $root ]; then + root="$(mkdir -p $1 && cd $1 && pwd)" + else + packages="$packages $1" + fi ;; + esac + shift; +done + +target="$root" + +cache="${cache:-$root/cache}" +build="${build:-$root/build}" + +mkdir -p "$target" +mkdir -p "$cache" +if [ $dl_only = "no" ]; then + mkdir -p "$build" +fi + +packages=$( with_deps $packages ) + +for p in $packages; do + target="$root/$p" + export CMAKE_PREFIX_PATH="$CMAKE_PREFIX_PATH:$target" + if [ -d "$target" ] ; then + if [ $duplicate = "skip" ]; then + message "skipping $p" && + continue + elif [ $duplicate = "remove" ]; then + message "removing existing package $p" && + rm -r "$target" + elif [ $duplicate = "rebuild" ]; then + message "rebuilding existing package $p" && + run_scripts build_install + continue + else + error "directory for $p already exists" + fi + fi + if [ $dl_only = "yes" ]; then + run_scripts download + elif [ $from_cache = "yes" ]; then + run_scripts unpack pre_build build_install + else + run_scripts download unpack pre_build build_install + fi +done diff --git a/crave/dependencies/cmake-2.8.4/setup.sh b/crave/dependencies/cmake-2.8.4/setup.sh new file mode 100644 index 0000000..13fdb27 --- /dev/null +++ b/crave/dependencies/cmake-2.8.4/setup.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +version=2.8.4 + +source $base_dir/cmake-2.8.4/shared.sh + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/cmake-2.8.4/shared.sh b/crave/dependencies/cmake-2.8.4/shared.sh new file mode 100644 index 0000000..2e56a02 --- /dev/null +++ b/crave/dependencies/cmake-2.8.4/shared.sh @@ -0,0 +1,33 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + error '$build is undefined' +fi +if [ -z "$package_dir" ] ; then + error '$build is undefined' +fi + +package=cmake +source=${package}-$version.tar.gz +build_dir=$build/${package}-$version +url="http://www.cmake.org/files/v${version:0:3}/$source" + +unpack() { + cd $cache && + tar -xf $source && + rm -rf $build_dir && + mv -f $cache/$package-$version $build_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + ./configure --prefix=$target && + make -j$num_threads && + make install +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/common.sh b/crave/dependencies/common.sh new file mode 100755 index 0000000..8cd9232 --- /dev/null +++ b/crave/dependencies/common.sh @@ -0,0 +1,105 @@ + +error() { + echo "ERROR: $@" >&2 + echo "TERMINATING" >&2 + exit 1 +} + +message() { + echo "$@" +} + +run_scripts() { + cd $base_dir + package_dir=$base_dir/$p + source functions.sh + source $p/setup.sh + for s in $@; do + echo "calling $s for $p" + $s || error "$s failed for $p" + done +} + +with_deps() { + build="-" + local i + local dependencies + for i in $@; do + package_dir=$i + source $package_dir/setup.sh + with_deps $dependencies + echo $i + done +} + + +download_http() { + url="$2" + name="$1" + if type -p wget &>/dev/null; then + wget -c -O "$name" "$url" + elif type -p curl &>/dev/null; then + curl -C - -o "$name" "$url" + else + error "no tool for http download found" + fi +} + +download_git() { + dir="$1" + url="$2" + branch="$3" + + mkdir -p $dir && + cd $dir && + if [ -d .git ]; then + git set-url origin "$url" + git fetch origin + else + git clone -b "$branch" "$url" . + fi + git reset --hard "origin/$branch" +} + + +# +# install all CMakeLists.txt files from the package to the current folder. +# includes subfolders and keeps hierarchy +# +# currently all files are symlinked. +# +install_cmake_files() { + find ${1:-$package_dir} -name CMakeLists.txt -o -name "*.cmake"| while read f + do + ln -sf $f $(echo "$f" |sed "s@^${1:-$package_dir}/*@@") + done +} + +cmake_build_install() { + local src=${1:-..} + shift + mkdir -p build && + cd build && + + echo cmake -DCMAKE_INSTALL_PREFIX=$target -DCMAKE_BUILD_TYPE=${BUILD_TYPE} $@ ${src} && + cmake -DCMAKE_INSTALL_PREFIX=$target -DCMAKE_BUILD_TYPE=${BUILD_TYPE} $@ ${src} && + make -j$num_threads install +} + +setup_environment() { + ARCH=${ARCH:-$(uname -m)} + duplicate=${duplicate:-skip} + BUILD_TYPE=${BUILD_TYPE:-RELEASE} + + case "$ARCH" in + i?86) + export CFLAGS="-m32 $CFLAGS" + export CXXFLAGS="-m32 $CXXFLAGS" + ;; + esac +} + +setup_environment + + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/cryptominisat-git/setup.sh b/crave/dependencies/cryptominisat-git/setup.sh new file mode 100755 index 0000000..12bd0ca --- /dev/null +++ b/crave/dependencies/cryptominisat-git/setup.sh @@ -0,0 +1,44 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +version=git +package=cryptominisat +source=$package-$version.tar.bz2 +build_dir=$build/${package}-${version} +url="https://github.com/msoos/cryptominisat.git" + +dependencies="m4ri-20140914" + +download() { + download_git "$build_dir" "$url" "master" +} + +unpack() { + true +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefinded' + exit 1 + fi + # Note that the directory is packaged with an additional '4' in the name + cd "$build_dir" && + export CMAKE_PREFIX_PATH="$root/m4ri-20140914" && + cmake_build_install .. \ + -DCMAKE_DISABLE_FIND_PACKAGE_PythonInterp=true \ + -DCMAKE_DISABLE_FIND_PACKAGE_PythonLibs=true \ + -DONLY_SIMPLE=ON +} diff --git a/crave/dependencies/cudd-3.0.0/CUDDConfig.cmake b/crave/dependencies/cudd-3.0.0/CUDDConfig.cmake new file mode 100644 index 0000000..91b24aa --- /dev/null +++ b/crave/dependencies/cudd-3.0.0/CUDDConfig.cmake @@ -0,0 +1,5 @@ +set(CUDD_VERSION 3.0.0) +get_filename_component(CUDD_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(CUDD_INCLUDE_DIRS ${CUDD_DIR}/include ) +set(CUDD_INCLUDE_DIR ${CUDD_INCLUDE_DIRS} ) +set(CUDD_LIBRARIES ${CUDD_DIR}/lib/libcudd.a ) diff --git a/crave/dependencies/cudd-3.0.0/setup.sh b/crave/dependencies/cudd-3.0.0/setup.sh new file mode 100755 index 0000000..4ad8ddc --- /dev/null +++ b/crave/dependencies/cudd-3.0.0/setup.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +version=3.0.0 +branch=cudd-3.0.0 + +cmake_files_dir=$base_dir/cudd-3.0.0 + +source $base_dir/cudd-3.0.0/shared.sh + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/cudd-3.0.0/shared.sh b/crave/dependencies/cudd-3.0.0/shared.sh new file mode 100644 index 0000000..ca9b569 --- /dev/null +++ b/crave/dependencies/cudd-3.0.0/shared.sh @@ -0,0 +1,51 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=cudd +source=$package-$version.tar.gz +build_dir=$build/$package-$version +url='https://github.com/nbruns1/cudd.git' + +download() { + mkdir -p $cache/$package-$version && + cd $cache/$package-$version && + if [ -d .git ]; then + git checkout $branch + else + git clone $url . + git checkout $branch + fi +} + +unpack() { + cp -R $cache/$package-$version $build_dir +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + touch configure.ac aclocal.m4 configure Makefile.am Makefile.in && + mkdir -p build && + cd build && + ../configure --enable-obj --enable-dddmp --prefix=$target && + make -j$num_threads install && + install_cmake_files $cmake_files_dir && + cp CUDDConfig.cmake "$target" +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/cvc4-1.5/CVC4Config.cmake b/crave/dependencies/cvc4-1.5/CVC4Config.cmake new file mode 100644 index 0000000..21f8f74 --- /dev/null +++ b/crave/dependencies/cvc4-1.5/CVC4Config.cmake @@ -0,0 +1,5 @@ +get_filename_component(CVC4_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(CVC4_BIN_DIRS ${CVC4_DIR}/bin ) +set(CVC4_INCLUDE_DIRS ${CVC4_DIR}/include ) +set(CVC4_INCLUDE_DIR ${CVC4_INCLUDE_DIRS} ) +set(CVC4_LIBRARIES ${CVC4_DIR}/lib/libcvc4.so ) diff --git a/crave/dependencies/cvc4-1.5/setup.sh b/crave/dependencies/cvc4-1.5/setup.sh new file mode 100644 index 0000000..8f10662 --- /dev/null +++ b/crave/dependencies/cvc4-1.5/setup.sh @@ -0,0 +1,4 @@ +#!/bin/sh + +version="1.5" +source $base_dir/cvc4-1.5/shared.sh diff --git a/crave/dependencies/cvc4-1.5/shared.sh b/crave/dependencies/cvc4-1.5/shared.sh new file mode 100644 index 0000000..baa6de7 --- /dev/null +++ b/crave/dependencies/cvc4-1.5/shared.sh @@ -0,0 +1,47 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$package_dir is undefined' + exit 1 +fi + +package=cvc4 +source="$package-$version.tar.gz" +build_dir=$build/$package-$version +url="http://cvc4.cs.stanford.edu/downloads/builds/src/$source" + +if [ -z "$BOOST_ROOT" ]; then + dependencies="$DEPS_BOOST" + boost_path="$root/$DEPS_BOOST" +else + boost_path="$BOOST_ROOT" +fi + +unpack() { + cd $cache && + tar -xf $source && + mv -f $package-$version $build_dir + cd $build_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + + cd "$build_dir" && + # build libantlr3c with provided script + contrib/get-antlr-3.4 + # build CVC4 with --bsd to allow usage under the terms of + # the modified BSD license. + ./configure --prefix="$target" --bsd --with-antlr-dir=$build_dir/antlr-3.4 --with-boost=$boost_path ANTLR=$build_dir/antlr-3.4/bin/antlr3 && + make -j $num_threads && + make install && + cp -f "$package_dir/CVC4Config.cmake" "$target/CVC4Config.cmake" +} + diff --git a/crave/dependencies/cvc4-1.5pre-smtcomp2016/CVC4Config.cmake b/crave/dependencies/cvc4-1.5pre-smtcomp2016/CVC4Config.cmake new file mode 100644 index 0000000..21f8f74 --- /dev/null +++ b/crave/dependencies/cvc4-1.5pre-smtcomp2016/CVC4Config.cmake @@ -0,0 +1,5 @@ +get_filename_component(CVC4_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(CVC4_BIN_DIRS ${CVC4_DIR}/bin ) +set(CVC4_INCLUDE_DIRS ${CVC4_DIR}/include ) +set(CVC4_INCLUDE_DIR ${CVC4_INCLUDE_DIRS} ) +set(CVC4_LIBRARIES ${CVC4_DIR}/lib/libcvc4.so ) diff --git a/crave/dependencies/cvc4-1.5pre-smtcomp2016/setup.sh b/crave/dependencies/cvc4-1.5pre-smtcomp2016/setup.sh new file mode 100644 index 0000000..4f7e1bd --- /dev/null +++ b/crave/dependencies/cvc4-1.5pre-smtcomp2016/setup.sh @@ -0,0 +1,49 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$package_dir is undefined' + exit 1 +fi + +package=cvc4 +version=1.5pre-smtcomp2016 +source="$package-$version.tar.gz" +build_dir=$build/$package-$version +url="http://cvc4.cs.nyu.edu/builds/src/$source" + +unpack() { + cd $cache && + src_dir=`tar --exclude="*/*" -tf $source` && + echo $src_dir && + tar -xf $source && + mv -f $src_dir $build_dir && + cd $build_dir +} + +if [ -z "$BOOST_ROOT" ]; then + dependencies="libantlr3c-3.4 $DEPS_BOOST" + boost_path="$root/$DEPS_BOOST" +else + dependencies="libantlr3c-3.4" + boost_path="$BOOST_ROOT" +fi + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + + cd "$build_dir" && + # build CVC4 with --bsd to allow usage under the terms of + # the modified BSD license. + ./configure --prefix="$target" --bsd --with-antlr-dir=$root/libantlr3c-3.4 --with-boost=$boost_path && + make -j $num_threads && + make install && + cp -f "$package_dir/CVC4Config.cmake" "$target/CVC4Config.cmake" +} + diff --git a/crave/dependencies/cvc4-1.6/CVC4Config.cmake b/crave/dependencies/cvc4-1.6/CVC4Config.cmake new file mode 100644 index 0000000..21f8f74 --- /dev/null +++ b/crave/dependencies/cvc4-1.6/CVC4Config.cmake @@ -0,0 +1,5 @@ +get_filename_component(CVC4_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(CVC4_BIN_DIRS ${CVC4_DIR}/bin ) +set(CVC4_INCLUDE_DIRS ${CVC4_DIR}/include ) +set(CVC4_INCLUDE_DIR ${CVC4_INCLUDE_DIRS} ) +set(CVC4_LIBRARIES ${CVC4_DIR}/lib/libcvc4.so ) diff --git a/crave/dependencies/cvc4-1.6/setup.sh b/crave/dependencies/cvc4-1.6/setup.sh new file mode 100644 index 0000000..ff82679 --- /dev/null +++ b/crave/dependencies/cvc4-1.6/setup.sh @@ -0,0 +1,5 @@ +#!/bin/sh + +version="1.6" +source $base_dir/cvc4-1.5/shared.sh + diff --git a/crave/dependencies/cvc4-smtcomp2015-stable/CVC4Config.cmake b/crave/dependencies/cvc4-smtcomp2015-stable/CVC4Config.cmake new file mode 100644 index 0000000..21f8f74 --- /dev/null +++ b/crave/dependencies/cvc4-smtcomp2015-stable/CVC4Config.cmake @@ -0,0 +1,5 @@ +get_filename_component(CVC4_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(CVC4_BIN_DIRS ${CVC4_DIR}/bin ) +set(CVC4_INCLUDE_DIRS ${CVC4_DIR}/include ) +set(CVC4_INCLUDE_DIR ${CVC4_INCLUDE_DIRS} ) +set(CVC4_LIBRARIES ${CVC4_DIR}/lib/libcvc4.so ) diff --git a/crave/dependencies/cvc4-smtcomp2015-stable/setup.sh b/crave/dependencies/cvc4-smtcomp2015-stable/setup.sh new file mode 100644 index 0000000..79ab22f --- /dev/null +++ b/crave/dependencies/cvc4-smtcomp2015-stable/setup.sh @@ -0,0 +1,50 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$package_dir is undefined' + exit 1 +fi + +package=cvc4 +version=smtcomp2015-stable +source="$version.tar.gz" +build_dir=$build/$package-$version +url="https://github.com/CVC4/CVC4/archive/$source" + +unpack() { + cd $cache && + src_dir=`tar --exclude="*/*" -tf $source` && + echo $src_dir && + tar -xf $source && + mv -f $src_dir $build_dir && + cd $build_dir +} + +if [ -z "$BOOST_ROOT" ]; then + dependencies="$DEPS_BOOST" + boost_path="$root/$DEPS_BOOST" +else + boost_path="$BOOST_ROOT" +fi + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + + cd "$build_dir" && + ./autogen.sh && + contrib/get-antlr-3.4 && + # build CVC4 with --bsd to allow usage under the terms of + # the modified BSD license. + ./configure --prefix="$target" --bsd --with-antlr-dir=$build_dir/antlr-3.4 ANTLR=$build_dir/antlr-3.4/bin/antlr3 --with-boost=$boost_path && + make -j $num_threads && + make install && + cp -f "$package_dir/CVC4Config.cmake" "$target/CVC4Config.cmake" +} + diff --git a/crave/dependencies/cvc4-unstable/CVC4Config.cmake b/crave/dependencies/cvc4-unstable/CVC4Config.cmake new file mode 100644 index 0000000..21f8f74 --- /dev/null +++ b/crave/dependencies/cvc4-unstable/CVC4Config.cmake @@ -0,0 +1,5 @@ +get_filename_component(CVC4_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(CVC4_BIN_DIRS ${CVC4_DIR}/bin ) +set(CVC4_INCLUDE_DIRS ${CVC4_DIR}/include ) +set(CVC4_INCLUDE_DIR ${CVC4_INCLUDE_DIRS} ) +set(CVC4_LIBRARIES ${CVC4_DIR}/lib/libcvc4.so ) diff --git a/crave/dependencies/cvc4-unstable/setup.sh b/crave/dependencies/cvc4-unstable/setup.sh new file mode 100644 index 0000000..dce9d10 --- /dev/null +++ b/crave/dependencies/cvc4-unstable/setup.sh @@ -0,0 +1,50 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$package_dir is undefined' + exit 1 +fi + +package=cvc4 +version=unstable +source="latest-unstable.tar.gz" +build_dir=$build/$package-$version +url="http://cvc4.cs.stanford.edu/downloads/builds/src/unstable/$source" + +unpack() { + cd $cache && + src_dir=`tar --exclude="*/*" -tf $source` && + echo $src_dir && + tar -xf $source && + mv -f $src_dir $build_dir && + cd $build_dir +} + +if [ -z "$BOOST_ROOT" ]; then + dependencies="$DEPS_BOOST" + boost_path="$root/$DEPS_BOOST" +else + boost_path="$BOOST_ROOT" +fi + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + + cd "$build_dir" && + # build libantlr3c with provided script + contrib/get-antlr-3.4 + # build CVC4 with --bsd to allow usage under the terms of + # the modified BSD license. + ./configure --prefix="$target" --bsd --with-antlr-dir=$build_dir/antlr-3.4 --with-boost=$boost_path ANTLR=$build_dir/antlr-3.4/bin/antlr3 && + make -j $num_threads && + make install && + cp -f "$package_dir/CVC4Config.cmake" "$target/CVC4Config.cmake" +} + diff --git a/crave/dependencies/functions.sh b/crave/dependencies/functions.sh new file mode 100644 index 0000000..eb2cffd --- /dev/null +++ b/crave/dependencies/functions.sh @@ -0,0 +1,32 @@ +#!/bin/sh + +# download() downloads the sources for the package. +download () { + if [ -z $url ] || [ -z $source ]; then + error "no url or source is defined" + fi + if ! [ ${url:0:7} == http:// ] && ! [ ${url:0:6} == ftp:// ] && ! [ ${url:0:8} == https:// ]; then + error "automatic downloading is only supported for http(s) and ftp urls." + fi + + cd $cache + download_http $source "$url" + cd - +} + +# unpack() defines the routine for unpack the package. +unpack() { + false +} + +# pre_build() prepare the package to complie properly. +pre_build() { + true +} + +# build_install() executes the compile-process and afterwards install the package. +build_install() { + false +} + +# vim: ts=2 sw=2 et \ No newline at end of file diff --git a/crave/dependencies/gcc-4.6.4/setup.sh b/crave/dependencies/gcc-4.6.4/setup.sh new file mode 100644 index 0000000..ca3c616 --- /dev/null +++ b/crave/dependencies/gcc-4.6.4/setup.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +version="4.6.4" + +version_gmp="4.3.2" +version_mpfr="2.4.2" +version_mpc="0.8.1" + +source $base_dir/gcc-4.8.1/shared.sh diff --git a/crave/dependencies/gcc-4.8.1/setup.sh b/crave/dependencies/gcc-4.8.1/setup.sh new file mode 100644 index 0000000..a0573d7 --- /dev/null +++ b/crave/dependencies/gcc-4.8.1/setup.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +version="4.8.1" + +version_gmp="4.3.2" +version_mpfr="2.4.2" +version_mpc="0.8.1" + +source $base_dir/gcc-4.8.1/shared.sh diff --git a/crave/dependencies/gcc-4.8.1/shared.sh b/crave/dependencies/gcc-4.8.1/shared.sh new file mode 100644 index 0000000..ea0bf08 --- /dev/null +++ b/crave/dependencies/gcc-4.8.1/shared.sh @@ -0,0 +1,76 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$package_dir is undefined' + exit 1 +fi + +package=gcc +source="gcc-$version.tar.bz2" +build_dir=$build/$package-$version +url="http://ftp.gwdg.de/pub/misc/gcc/releases/$package-$version/$source" + +MPFR="mpfr-${version_mpfr}" +GMP="gmp-${version_gmp}" +MPC="mpc-${version_mpc}" + +MPFR_URL="ftp://gcc.gnu.org/pub/gcc/infrastructure/$MPFR.tar.bz2" +GMP_URL="ftp://gcc.gnu.org/pub/gcc/infrastructure/$GMP.tar.bz2" +MPC_URL="ftp://gcc.gnu.org/pub/gcc/infrastructure/$MPC.tar.gz" + +download () { + cd $cache && + download_http $source "$url" && + download_http "$MPFR.tar.bz2" "$MPFR_URL" && + download_http "$GMP.tar.bz2" "$GMP_URL" && + download_http "$MPC.tar.gz" "$MPC_URL" && + cd - +} + +unpack() { + cd $cache && + tar -xf $source && + rm -rf $build_dir && + mv -f $package-$version $build_dir && + + tar -xf "${MPFR}.tar.bz2" && + mv -f "${MPFR}" "${build_dir}/mpfr" && + + tar -xf "${GMP}.tar.bz2" && + mv -f "${GMP}" "${build_dir}/gmp" && + + tar -xf "${MPC}.tar.gz" && + mv -f "${MPC}" "${build_dir}/mpc" +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd "$build_dir" && + GCCMACHINE=`gcc -dumpmachine` + GCCVERSION=`gcc -dumpversion` + export CFLAGS="-O2 -I/usr/include/$GCCMACHINE" + export LDFLAGS="-O2 -B/usr/lib/$GCCMACHINE -L/usr/lib/$GCCMACHINE" + export LIBRARY_PATH=/usr/lib/$GCCMACHINE + #make distclean + local OPTS=" + --prefix=$target + --disable-multilib + --enable-languages=c,c++ + " + echo ./configure $OPTS && + ./configure $OPTS && + make -j5$num_threads && + make install +} + diff --git a/crave/dependencies/gcc-4.9.2/setup.sh b/crave/dependencies/gcc-4.9.2/setup.sh new file mode 100644 index 0000000..bd48c3e --- /dev/null +++ b/crave/dependencies/gcc-4.9.2/setup.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +version="4.9.2" + +version_gmp="4.3.2" +version_mpfr="2.4.2" +version_mpc="0.8.1" + +source $base_dir/gcc-4.8.1/shared.sh diff --git a/crave/dependencies/gcc-5.1.0/setup.sh b/crave/dependencies/gcc-5.1.0/setup.sh new file mode 100644 index 0000000..c68e215 --- /dev/null +++ b/crave/dependencies/gcc-5.1.0/setup.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +version="5.1.0" + +version_gmp="4.3.2" +version_mpfr="2.4.2" +version_mpc="0.8.1" + +source $base_dir/gcc-4.8.1/shared.sh diff --git a/crave/dependencies/git-2.1.0/setup.sh b/crave/dependencies/git-2.1.0/setup.sh new file mode 100644 index 0000000..9f4b71a --- /dev/null +++ b/crave/dependencies/git-2.1.0/setup.sh @@ -0,0 +1,5 @@ +#!/bin/sh + +version="2.1.0" + +source $base_dir/git-2.1.0/shared.sh diff --git a/crave/dependencies/git-2.1.0/shared.sh b/crave/dependencies/git-2.1.0/shared.sh new file mode 100644 index 0000000..720392a --- /dev/null +++ b/crave/dependencies/git-2.1.0/shared.sh @@ -0,0 +1,39 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=git +source="$package-$version.tar.gz" +build_dir=$build/$package-$version +url="https://www.kernel.org/pub/software/scm/git/$source" + +unpack() { + cd $cache && + tar -xf $source && + mv -f $package-$version $build_dir +} + + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + + cd "$build_dir" && + ./configure --prefix=$target && + make -j $num_threads && + make install +} + diff --git a/crave/dependencies/glog-git-0.3.3/setup.sh b/crave/dependencies/glog-git-0.3.3/setup.sh new file mode 100644 index 0000000..1276a2a --- /dev/null +++ b/crave/dependencies/glog-git-0.3.3/setup.sh @@ -0,0 +1,44 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +version=git-0.3.3 +package=glog +source=nosourcefile +branch=v0.3.3 +build_dir=$build/$package-$version +url=https://github.com/google/glog.git + +download() { + mkdir -p $build_dir && + cd $build_dir && + if [ -d .git ]; then + git pull + else + git clone -b $branch $url . + fi + git reset --hard HEAD +} + +unpack() { + true +} + +build_install() { + if [ -z "$target" ] ; then + error '$target is undefined' + fi + cd "$build_dir" && + + ./autogen.sh && ./configure --prefix="$target" && + make -j && make install +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/gmp-5.0.5/setup.sh b/crave/dependencies/gmp-5.0.5/setup.sh new file mode 100644 index 0000000..02c8604 --- /dev/null +++ b/crave/dependencies/gmp-5.0.5/setup.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +version=5.0.5 + +source $base_dir/gmp-5.0.5/shared.sh + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/gmp-5.0.5/shared.sh b/crave/dependencies/gmp-5.0.5/shared.sh new file mode 100644 index 0000000..6241097 --- /dev/null +++ b/crave/dependencies/gmp-5.0.5/shared.sh @@ -0,0 +1,41 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=gmp +source="$package-$version.tar.bz2" +build_dir=$build/$package-$version +url="ftp://ftp.gmplib.org/pub/$package-$version/$source" + +unpack(){ + cd $cache && + message "unpacking $package" && + tar -xf $source && + message "finished unpacking $package" && + rm -rf $build_dir && + mv -f $cache/$package-$version $build_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + + # build mpfr + cd "$build_dir" && + mkdir -p build && + cd build && + ../configure --prefix=$target && + make -j$num_threads && + make install +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/libantlr3c-3.4/setup.sh b/crave/dependencies/libantlr3c-3.4/setup.sh new file mode 100644 index 0000000..d6a4e04 --- /dev/null +++ b/crave/dependencies/libantlr3c-3.4/setup.sh @@ -0,0 +1,4 @@ +#!/bin/sh + +version="3.4" +source $base_dir/libantlr3c-3.4/shared.sh diff --git a/crave/dependencies/libantlr3c-3.4/shared.sh b/crave/dependencies/libantlr3c-3.4/shared.sh new file mode 100644 index 0000000..b3c7a9a --- /dev/null +++ b/crave/dependencies/libantlr3c-3.4/shared.sh @@ -0,0 +1,38 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=libantlr3c +source="$package-$version.tar.gz" +build_dir=$build/$package-$version +url="http://www.antlr3.org/download/C/$source" + +unpack() { + cd $cache && + tar -xf $source && + mv -f $package-$version $build_dir +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + + cd "$build_dir" && + ./configure --prefix="$target" --disable-abiflags && + make && + make install +} + diff --git a/crave/dependencies/lingeling-ayv-86bf266-140429/CMakeLists.txt b/crave/dependencies/lingeling-ayv-86bf266-140429/CMakeLists.txt new file mode 100644 index 0000000..45dade8 --- /dev/null +++ b/crave/dependencies/lingeling-ayv-86bf266-140429/CMakeLists.txt @@ -0,0 +1,96 @@ +project(Lingeling) + +cmake_minimum_required(VERSION 2.8) + +set(STATIC_OR_SHARED SHARED CACHE STRING "Build STATIC or SHARED libaries") + +set (Lingeling_VERSION ayv-86bf266-140429) + +include_directories(${CMAKE_CURRENT_BINARY_DIR}) +include_directories(${CMAKE_CURRENT_SOURCE_DIR}/code) + +set(HOSTNAME $ENV{HOSTNAME}) +if("${CMAKE_VERSION}" VERSION_GREATER 2.8.10) + STRING(TIMESTAMP COMPILATION_TIMESTAMP "%Y-%m-%dT%H:%M:%S") +endif() +set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -DNDBLSCR -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLPICOSAT -DNLGLDRUPLIG -DNLGLYALSAT") + +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/lglcfg.h.in.cmake + ${CMAKE_CURRENT_SOURCE_DIR}/code/lglcfg.h + @ONLY +) + +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/lglcflags.h.in.cmake + ${CMAKE_CURRENT_SOURCE_DIR}/code/lglcflags.h + @ONLY +) + + +add_library(Lingeling_liblingeling + ${STATIC_OR_SHARED} + code/lglbnr.c + code/lgldimacs.c + code/lglib.c +) +set_target_properties(Lingeling_liblingeling PROPERTIES OUTPUT_NAME lingeling) + +add_executable(Lingeling_lingeling + code/lglbnr.c + code/lgldimacs.c + code/lglib.c + code/lglmain.c +) +target_link_libraries(Lingeling_lingeling m) + +SET_TARGET_PROPERTIES( Lingeling_lingeling PROPERTIES + OUTPUT_NAME lingeling +) + + +file(WRITE ${PROJECT_BINARY_DIR}/LingelingConfig.cmake +"set(Lingeling_FOUND 1) +set(Lingeling_VERSION ${Lingeling_VERSION}) +get_filename_component(Lingeling_CONFIG_DIR \${CMAKE_CURRENT_LIST_FILE} PATH) +set(Lingeling_INCLUDE_DIR \${Lingeling_CONFIG_DIR}/../../include) +set(Lingeling_LIBRARIES Lingeling_liblingeling) +include(\"\${Lingeling_CONFIG_DIR}/Lingeling.cmake\" ) +") +file(WRITE ${PROJECT_BINARY_DIR}/LingelingConfigVersion.cmake +"if(\"\${PACKAGE_FIND_VERSION}\" VERSION_EQUAL ${Lingeling_VERSION}) +set(PACKAGE_VERSION_EXACT 1) +set(PACKAGE_VERSION_COMPATIBLE 1) +endif(\"\${PACKAGE_FIND_VERSION}\" VERSION_EQUAL ${Lingeling_VERSION}) +") +## create libLingeling config file for internal use +file(WRITE ${PROJECT_BINARY_DIR}/Lingeling.cmake +"set(Lingeling_INCLUDE_DIR + ${PROJECT_SOURCE_DIR}/include +) +") +## export target with install +INSTALL( FILES + ${PROJECT_BINARY_DIR}/LingelingConfig.cmake + ${PROJECT_BINARY_DIR}/LingelingConfigVersion.cmake + DESTINATION share/Lingeling) +install(EXPORT Lingeling DESTINATION share/Lingeling) + +install(TARGETS + Lingeling_liblingeling + Lingeling_lingeling + EXPORT Lingeling + LIBRARY DESTINATION lib + RUNTIME DESTINATION bin + ARCHIVE DESTINATION lib +) + +install(FILES + code/lglcfg.h + code/lglcflags.h + code/lgldimacs.h + code/lglib.h + DESTINATION include +) + +# vim: sw=2 tabstop=2 expandtab: diff --git a/crave/dependencies/lingeling-ayv-86bf266-140429/lglcfg.h.in.cmake b/crave/dependencies/lingeling-ayv-86bf266-140429/lglcfg.h.in.cmake new file mode 100644 index 0000000..fb4aff2 --- /dev/null +++ b/crave/dependencies/lingeling-ayv-86bf266-140429/lglcfg.h.in.cmake @@ -0,0 +1,6 @@ +#define LGL_OS "@HOSTNAME@" +#define LGL_COMPILED "@COMPILATION_TIMESTAMP@" +#define LGL_RELEASED "Tue Apr 29 19:18:48 CEST 2014" +#define LGL_VERSION "ayv" +#define LGL_ID "86bf266b9332599f1b876e28a02fe8427aeaa2db" + diff --git a/crave/dependencies/lingeling-ayv-86bf266-140429/lglcflags.h.in.cmake b/crave/dependencies/lingeling-ayv-86bf266-140429/lglcflags.h.in.cmake new file mode 100644 index 0000000..e7ac581 --- /dev/null +++ b/crave/dependencies/lingeling-ayv-86bf266-140429/lglcflags.h.in.cmake @@ -0,0 +1,3 @@ +#define LGL_CC "@CMAKE_SYSTEM@" +#define LGL_CFLAGS "@CMAKE_C_FLAGS@" + diff --git a/crave/dependencies/lingeling-ayv-86bf266-140429/setup.sh b/crave/dependencies/lingeling-ayv-86bf266-140429/setup.sh new file mode 100755 index 0000000..b0854cd --- /dev/null +++ b/crave/dependencies/lingeling-ayv-86bf266-140429/setup.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +version=ayv-86bf266-140429 + +cmake_files_dir=$base_dir/lingeling-${version} + +source $base_dir/lingeling-${version}/shared.sh diff --git a/crave/dependencies/lingeling-ayv-86bf266-140429/shared.sh b/crave/dependencies/lingeling-ayv-86bf266-140429/shared.sh new file mode 100644 index 0000000..1d271df --- /dev/null +++ b/crave/dependencies/lingeling-ayv-86bf266-140429/shared.sh @@ -0,0 +1,39 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$package_dir is undefined' + exit 1 +fi + +package=lingeling +version=ayv-86bf266-140429 +source=$package-$version.zip +build_dir=$build/$package-$version +url=http://fmv.jku.at/$package/$source + +unpack(){ + cd $cache && + unzip $source -d $package-$version && + rm -rf $build_dir && + mv -f $cache/$package-$version $build_dir +} + +pre_build() { + cd $build_dir && + install_cmake_files $cmake_files_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + cmake_build_install +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/llvm+clang-3.0/setup.sh b/crave/dependencies/llvm+clang-3.0/setup.sh new file mode 100644 index 0000000..7cef4f1 --- /dev/null +++ b/crave/dependencies/llvm+clang-3.0/setup.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +version=3.0 + +source_llvm="llvm-$version.tar.gz" +source_clang="clang-$version.tar.gz" + +source $base_dir/llvm+clang-3.0/shared.sh + +# vim: ts=2 sw=2 et \ No newline at end of file diff --git a/crave/dependencies/llvm+clang-3.0/shared.sh b/crave/dependencies/llvm+clang-3.0/shared.sh new file mode 100644 index 0000000..6df7dc5 --- /dev/null +++ b/crave/dependencies/llvm+clang-3.0/shared.sh @@ -0,0 +1,58 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=llvm+clang +build_dir=$build/$package-$version.build +source_dir=$cache/llvm-${version}.src +url_llvm="http://llvm.org/releases/$version/$source_llvm" +url_clang="http://llvm.org/releases/$version/$source_clang" + +unset -f download +download () { + cd $cache + download_http $source_llvm $url_llvm && + download_http $source_clang $url_clang && + cd - +} + +unpack(){ + cd $cache && + tar -xf $source_llvm && + tar -xf $source_clang && + mv clang-$version.src $source_dir/tools/clang && + rm -rf $build_dir && + mv -f $source_dir $build_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + COMMON_OPS=" + --disable-assertions + --disable-debug-runtime + --disable-debug-symbols + --disable-docs + --disable-profiling + --enable-optimized + --enable-targets=host + --prefix=$target + " + cd "$build_dir" && + mkdir -p build && + cd build && + ../configure $COMMON_OPS && + make -j$num_threads && + make install +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/llvm+clang-3.1/setup.sh b/crave/dependencies/llvm+clang-3.1/setup.sh new file mode 100644 index 0000000..d9d7e1d --- /dev/null +++ b/crave/dependencies/llvm+clang-3.1/setup.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +version=3.1 + +source_llvm="llvm-$version.src.tar.gz" +source_clang="clang-$version.src.tar.gz" + +source $base_dir/llvm+clang-3.0/shared.sh + +# vim: ts=2 sw=2 et \ No newline at end of file diff --git a/crave/dependencies/llvm+clang-3.2/setup.sh b/crave/dependencies/llvm+clang-3.2/setup.sh new file mode 100644 index 0000000..5945f76 --- /dev/null +++ b/crave/dependencies/llvm+clang-3.2/setup.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +version=3.2 + +source_llvm="llvm-$version.src.tar.gz" +source_clang="clang-$version.src.tar.gz" + +source $base_dir/llvm+clang-3.0/shared.sh + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/llvm+clang-3.3/setup.sh b/crave/dependencies/llvm+clang-3.3/setup.sh new file mode 100644 index 0000000..ecdc68f --- /dev/null +++ b/crave/dependencies/llvm+clang-3.3/setup.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +version=3.3 + +source_llvm="llvm-$version.src.tar.gz" +source_clang="cfe-$version.src.tar.gz" + +source $base_dir/llvm+clang-3.3/shared.sh + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/llvm+clang-3.3/shared.sh b/crave/dependencies/llvm+clang-3.3/shared.sh new file mode 100644 index 0000000..6559127 --- /dev/null +++ b/crave/dependencies/llvm+clang-3.3/shared.sh @@ -0,0 +1,46 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=llvm+clang +build_dir=$build/$package-$version.build +source_dir=$cache/llvm-${version}.src +url_llvm="http://llvm.org/releases/$version/$source_llvm" +url_clang="http://llvm.org/releases/$version/$source_clang" + +unset -f download +download () { + cd $cache + download_http $source_llvm $url_llvm && + download_http $source_clang $url_clang && + cd - +} + +unpack(){ + cd $cache && + tar -xf $source_llvm && + tar -xf $source_clang && + mv cfe-$version.src $source_dir/tools/clang && + rm -rf $build_dir && + mv -f $source_dir $build_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + cmake_build_install && + ## install scan-build tools + true +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/m4ri-20140914/setup.sh b/crave/dependencies/m4ri-20140914/setup.sh new file mode 100755 index 0000000..9a13929 --- /dev/null +++ b/crave/dependencies/m4ri-20140914/setup.sh @@ -0,0 +1,42 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +version=20140914 +package=m4ri +source=$package-$version.tar.gz +build_dir=$build/$package-$version +url="https://bitbucket.org/malb/m4ri/downloads/$source" + +download() { + cd $cache && + if [ ! -f $source ]; then + download_http $source $url + fi +} + +unpack() { + echo $PWD && + mkdir -p $build_dir && + tar xfz $source -C $build_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefinded' + exit 1 + fi + cd "$build_dir" && + cd $package-$version + ./configure --prefix="$target" && + make && + make install +} + diff --git a/crave/dependencies/minisat-2.2.0/CMakeLists.txt b/crave/dependencies/minisat-2.2.0/CMakeLists.txt new file mode 100644 index 0000000..91ec477 --- /dev/null +++ b/crave/dependencies/minisat-2.2.0/CMakeLists.txt @@ -0,0 +1,90 @@ +project(MiniSat) +cmake_minimum_required(VERSION 2.8) +set(MiniSat_VERSION 2.2.0) + +set(STATIC_OR_SHARED SHARED CACHE STRING "Build STATIC or SHARED libaries") + + +file(GLOB UTILS_SRCS minisat/utils/*.cc) +file(GLOB MTL_HDRS minisat/mtl/*.h) +file(GLOB CORE_HDRS minisat/core/*.h) +file(GLOB SIMP_HDRS minisat/simp/*.h) +file(GLOB UTILS_HDRS minisat/utils/*.h) + +include_directories(${PROJECT_SOURCE_DIR}) +include_directories(${PROJECT_SOURCE_DIR}/minisat) +message(STATUS ${PROJECT_SOURCE_DIR}}) + +set(MiniSat_CXXFLAGS "-D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS") + +add_definitions( ${MiniSat_CXXFLAGS} ) + +add_library(MiniSat_libMiniSat + ${STATIC_OR_SHARED} + minisat/core/Solver.cc + minisat/simp/SimpSolver.cc + ${UTILS_SRCS} +) + +find_library(LIBZ z) + +SET_TARGET_PROPERTIES( MiniSat_libMiniSat PROPERTIES + VERSION 2.2.0 + SOVERSION 2.2.0 + OUTPUT_NAME minisat_core +) + +add_executable(MiniSat_core + ${UTILS_SRCS} + minisat/core/Solver.cc + minisat/core/Main.cc +) +target_link_libraries(MiniSat_core ${LIBZ}) + +SET_TARGET_PROPERTIES( MiniSat_core PROPERTIES + OUTPUT_NAME minisat_core +) + +add_executable(MiniSat_simp + ${UTILS_SRCS} + minisat/core/Solver.cc + minisat/simp/SimpSolver.cc + minisat/simp/Main.cc +) +target_link_libraries(MiniSat_simp ${LIBZ}) + +SET_TARGET_PROPERTIES( MiniSat_simp PROPERTIES + OUTPUT_NAME minisat +) + +set(MiniSat_LIBRARIES MiniSat_libMiniSat) + +configure_file(MiniSatConfig.cmake ${PROJECT_BINARY_DIR}/MiniSatConfig.cmake @ONLY) +configure_file(MiniSatConfigVersion.cmake ${PROJECT_BINARY_DIR}/MiniSatConfigVersion.cmake @ONLY) +## create libMiniSat config file for internal use +file(WRITE ${PROJECT_BINARY_DIR}/MiniSat.cmake +"set(MiniSat_INCLUDE_DIR + ${PROJECT_SOURCE_DIR} +) +") +## export target with install +INSTALL( FILES + ${PROJECT_BINARY_DIR}/MiniSatConfig.cmake + ${PROJECT_BINARY_DIR}/MiniSatConfigVersion.cmake + DESTINATION share/MiniSat) +install(EXPORT MiniSat DESTINATION share/MiniSat) + +install(TARGETS + MiniSat_libMiniSat + MiniSat_core + MiniSat_simp + EXPORT MiniSat + ARCHIVE DESTINATION lib + LIBRARY DESTINATION lib + RUNTIME DESTINATION bin +) + +install(FILES ${MTL_HDRS} DESTINATION include/minisat/mtl) +install(FILES ${CORE_HDRS} DESTINATION include/minisat/core) +install(FILES ${SIMP_HDRS} DESTINATION include/minisat/simp) +install(FILES ${UTILS_HDRS} DESTINATION include/minisat/utils) diff --git a/crave/dependencies/minisat-2.2.0/MiniSatConfig.cmake b/crave/dependencies/minisat-2.2.0/MiniSatConfig.cmake new file mode 100644 index 0000000..0d92f79 --- /dev/null +++ b/crave/dependencies/minisat-2.2.0/MiniSatConfig.cmake @@ -0,0 +1,9 @@ +set(MiniSat_FOUND 1) +set(MiniSat_VERSION @MiniSat_VERSION@) +get_filename_component(MiniSat_CONFIG_DIR "${CMAKE_CURRENT_LIST_FILE}" PATH) +set(MiniSat_INCLUDE_DIR ${MiniSat_CONFIG_DIR}/../../include) +set(MiniSat_INCLUDE_DIRS ${MiniSat_INCLUDE_DIR}) +set(MiniSat_LIBRARIES @MiniSat_LIBRARIES@) +set(MiniSat_CXXFLAGS "@MiniSat_CXXFLAGS@") +include("${MiniSat_CONFIG_DIR}/MiniSat.cmake" ) + diff --git a/crave/dependencies/minisat-2.2.0/MiniSatConfigVersion.cmake b/crave/dependencies/minisat-2.2.0/MiniSatConfigVersion.cmake new file mode 100644 index 0000000..c2d4f35 --- /dev/null +++ b/crave/dependencies/minisat-2.2.0/MiniSatConfigVersion.cmake @@ -0,0 +1,4 @@ +if("${PACKAGE_FIND_VERSION}" VERSION_EQUAL @MiniSat_VERSION@) +set(PACKAGE_VERSION_EXACT 1) +set(PACKAGE_VERSION_COMPATIBLE 1) +endif("${PACKAGE_FIND_VERSION}" VERSION_EQUAL @MiniSat_VERSION@) diff --git a/crave/dependencies/minisat-2.2.0/setup.sh b/crave/dependencies/minisat-2.2.0/setup.sh new file mode 100755 index 0000000..b597ce3 --- /dev/null +++ b/crave/dependencies/minisat-2.2.0/setup.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +version=2.2.0 + +cmake_files_dir=$base_dir/minisat-2.2.0 + +source $base_dir/minisat-2.2.0/shared.sh + +# vim: ts=2 sw=2 et \ No newline at end of file diff --git a/crave/dependencies/minisat-2.2.0/shared.sh b/crave/dependencies/minisat-2.2.0/shared.sh new file mode 100644 index 0000000..f2f1903 --- /dev/null +++ b/crave/dependencies/minisat-2.2.0/shared.sh @@ -0,0 +1,39 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=minisat +source=$package-$version.tar.gz +build_dir=$build/$package-$version +url=http://minisat.se/downloads/$source + +unpack() { + cd $cache && + tar -xzf $source && + rm -rf $build_dir && + mkdir -p $build_dir && + mv -f $cache/$package $build_dir/$package +} + +pre_build() { + cd $build_dir && + install_cmake_files $cmake_files_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + cmake_build_install +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/minisat-git/MiniSatConfig.cmake b/crave/dependencies/minisat-git/MiniSatConfig.cmake new file mode 100644 index 0000000..df53b4a --- /dev/null +++ b/crave/dependencies/minisat-git/MiniSatConfig.cmake @@ -0,0 +1,7 @@ +set(MiniSat_VERSION git) +get_filename_component(MiniSat_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(MiniSat_BIN_DIRS ${MiniSat_DIR}/bin ) +set(MiniSat_INCLUDE_DIRS ${MiniSat_DIR}/include ) +set(MiniSat_INCLUDE_DIR ${MiniSat_INCLUDE_DIRS} ) +set(MiniSat_LIBRARIES ${MiniSat_DIR}/lib/libminisat.so ) +set(MiniSat_CXXFLAGS "-D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS") diff --git a/crave/dependencies/minisat-git/setup.sh b/crave/dependencies/minisat-git/setup.sh new file mode 100755 index 0000000..a5bed91 --- /dev/null +++ b/crave/dependencies/minisat-git/setup.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +version=git + +cmake_files_dir=$base_dir/minisat-2.2.0 + +source $base_dir/minisat-git/shared-git.sh + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/minisat-git/shared-git.sh b/crave/dependencies/minisat-git/shared-git.sh new file mode 100644 index 0000000..9820b6b --- /dev/null +++ b/crave/dependencies/minisat-git/shared-git.sh @@ -0,0 +1,33 @@ +#!/bin/sh + +package=minisat +version=git +build_dir=$build/$package-$version +url=https://github.com/stp/minisat.git + +unset -f download +download() { + mkdir -p $build_dir && + cd $build_dir && + if [ -d .git ]; then + env GIT_SSL_NO_VERIFY=true git pull + else + env GIT_SSL_NO_VERIFY=true git clone $url . + fi +} + +unpack() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + cmake_build_install && + cp $package_dir/MiniSatConfig.cmake $target/ +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/mpc-0.9/setup.sh b/crave/dependencies/mpc-0.9/setup.sh new file mode 100644 index 0000000..ee862e9 --- /dev/null +++ b/crave/dependencies/mpc-0.9/setup.sh @@ -0,0 +1,8 @@ +#!/bin/sh + +version="0.9" + +version_gmp="5.0.5" +version_mpfr="3.1.2" + +source $base_dir/mpc-0.9/shared.sh diff --git a/crave/dependencies/mpc-0.9/shared.sh b/crave/dependencies/mpc-0.9/shared.sh new file mode 100644 index 0000000..3d07697 --- /dev/null +++ b/crave/dependencies/mpc-0.9/shared.sh @@ -0,0 +1,40 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=mpc +source="$package-$version.tar.gz" +build_dir=$build/$package-$version +url="http://www.multiprecision.org/mpc/download/$source" + +dependencies="gmp-$version_gmp mpfr-$version_mpfr" + +unpack() { + cd $cache && + tar -xf $source && + mv -f $package-$version $build_dir +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + + cd "$build_dir" && + ./configure --prefix=$target --with-gmp="$root/gmp-$version_gmp" --with-mpfr="$root/mpfr-$version_mpfr" && + make && + make install +} + diff --git a/crave/dependencies/mpfr-3.1.2/setup.sh b/crave/dependencies/mpfr-3.1.2/setup.sh new file mode 100644 index 0000000..2f247f7 --- /dev/null +++ b/crave/dependencies/mpfr-3.1.2/setup.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +version="3.1.2" +version_gmp="5.0.5" + +source $base_dir/mpfr-3.1.2/shared.sh diff --git a/crave/dependencies/mpfr-3.1.2/shared.sh b/crave/dependencies/mpfr-3.1.2/shared.sh new file mode 100644 index 0000000..0920d25 --- /dev/null +++ b/crave/dependencies/mpfr-3.1.2/shared.sh @@ -0,0 +1,40 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=mpfr +source="$package-$version.tar.bz2" +build_dir=$build/$package-$version +url="http://www.mpfr.org/mpfr-current/$source" + +dependencies="gmp-$version_gmp" + +unpack() { + cd $cache && + tar -xf $source && + mv -f $package-$version $build_dir +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + + # build mpfr + cd "$build_dir" && + CFLAGS="-O2" ./configure --prefix=$target --with-gmp="$root/gmp-$version_gmp" && + make -j$num_threads && + make install +} diff --git a/crave/dependencies/ninja-git/setup.sh b/crave/dependencies/ninja-git/setup.sh new file mode 100755 index 0000000..6ab5dd4 --- /dev/null +++ b/crave/dependencies/ninja-git/setup.sh @@ -0,0 +1,18 @@ +#!/bin/sh + +version=git + +source $base_dir/ninja-release/shared.sh + +unset -f download +download() { + mkdir -p $build_dir && + cd $build_dir && + if [ -d .git ]; then + git pull + else + git clone $url . + fi +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/ninja-release/setup.sh b/crave/dependencies/ninja-release/setup.sh new file mode 100755 index 0000000..239440a --- /dev/null +++ b/crave/dependencies/ninja-release/setup.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +version=release + +source $base_dir/ninja-release/shared.sh + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/ninja-release/shared.sh b/crave/dependencies/ninja-release/shared.sh new file mode 100644 index 0000000..18e84a0 --- /dev/null +++ b/crave/dependencies/ninja-release/shared.sh @@ -0,0 +1,41 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=ninja +source=nosourcefile +build_dir=$build/$package-$version +url=git://github.com/martine/ninja.git + +download() { + mkdir -p $build_dir && + cd $build_dir && + if [ -d .git ]; then + git pull + else + git clone $url . -b $version + fi +} + +unpack() { + true +} + +build_install() { + if [ -z "$target" ] ; then + error '$target is undefined' + fi + cd "$build_dir" && + python bootstrap.py && + mkdir -p "$target/bin" + cp "$package" "$target/bin" +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/picosat-936/CMakeLists.txt b/crave/dependencies/picosat-936/CMakeLists.txt new file mode 100644 index 0000000..655028c --- /dev/null +++ b/crave/dependencies/picosat-936/CMakeLists.txt @@ -0,0 +1,83 @@ +project(PicoSAT) + +cmake_minimum_required(VERSION 2.8) + +set(STATIC_OR_SHARED SHARED CACHE STRING "Build STATIC or SHARED libaries") + +file(STRINGS ${CMAKE_CURRENT_SOURCE_DIR}/VERSION PicoSAT_VERSION) +file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/config.h +"#define PICOSAT_CC \"${CMAKE_C_COMPILER}\" +#define PICOSAT_CFLAGS \"${CMAKE_C_FLAGS}\" +#define PICOSAT_VERSION \"${PicoSAT_VERSION}\" +") + +include_directories(${CMAKE_CURRENT_BINARY_DIR}) + +add_library(PicoSAT_libpicosat + ${STATIC_OR_SHARED} + picosat.c + version.c +) +set_target_properties(PicoSAT_libpicosat PROPERTIES OUTPUT_NAME picosat) + +add_executable(PicoSAT_picosat + picosat.c + version.c + app.c + main.c +) +SET_TARGET_PROPERTIES( PicoSAT_picosat PROPERTIES + OUTPUT_NAME picosat +) + +add_executable(PicoSAT_picomus + picomus.c + picosat.c + version.c +) +SET_TARGET_PROPERTIES( PicoSAT_picomus PROPERTIES + OUTPUT_NAME picomus +) + + +file(WRITE ${PROJECT_BINARY_DIR}/PicoSATConfig.cmake +"set(PicoSAT_FOUND 1) +set(PicoSAT_VERSION ${PicoSAT_VERSION}) +get_filename_component(PicoSAT_CONFIG_DIR \"\${CMAKE_CURRENT_LIST_FILE}\" PATH) +set(PicoSAT_INCLUDE_DIR \${PicoSAT_CONFIG_DIR}/../../include) +set(PicoSAT_LIBRARIES PicoSAT_libpicosat) +include(\${PicoSAT_CONFIG_DIR}/PicoSAT.cmake) +") +file(WRITE ${PROJECT_BINARY_DIR}/PicoSATConfigVersion.cmake +"if(\"\${PACKAGE_FIND_VERSION}\" VERSION_EQUAL ${PicoSAT_VERSION}) +set(PACKAGE_VERSION_EXACT 1) +set(PACKAGE_VERSION_COMPATIBLE 1) +endif(\"\${PACKAGE_FIND_VERSION}\" VERSION_EQUAL ${PicoSAT_VERSION}) +") +## create libPicoSAT config file for internal use +file(WRITE ${PROJECT_BINARY_DIR}/PicoSAT.cmake +"set(PicoSAT_INCLUDE_DIR + ${PROJECT_SOURCE_DIR}/include +) +") +## export target with install +INSTALL( FILES + ${PROJECT_BINARY_DIR}/PicoSATConfig.cmake + ${PROJECT_BINARY_DIR}/PicoSATConfigVersion.cmake + DESTINATION share/PicoSAT) +install(EXPORT PicoSAT DESTINATION share/PicoSAT) + +install(TARGETS + PicoSAT_libpicosat + PicoSAT_picosat + PicoSAT_picomus + EXPORT PicoSAT + LIBRARY DESTINATION lib + RUNTIME DESTINATION bin + ARCHIVE DESTINATION lib +) + +install(FILES + picosat.h + DESTINATION include +) diff --git a/crave/dependencies/picosat-936/setup.sh b/crave/dependencies/picosat-936/setup.sh new file mode 100755 index 0000000..7f94c0f --- /dev/null +++ b/crave/dependencies/picosat-936/setup.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +version=936 + +cmake_files_dir=$base_dir/picosat-936 + +source $base_dir/picosat-936/shared.sh diff --git a/crave/dependencies/picosat-936/shared.sh b/crave/dependencies/picosat-936/shared.sh new file mode 100644 index 0000000..07370a0 --- /dev/null +++ b/crave/dependencies/picosat-936/shared.sh @@ -0,0 +1,39 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$package_dir is undefined' + exit 1 +fi + + +package=picosat +source=$package-$version.tar.gz +build_dir=$build/$package-$version +url=http://fmv.jku.at/$package/$source + +unpack(){ + cd $cache && + tar -xf $source && + rm -rf $build_dir && + mv -f $cache/$package-$version $build_dir +} + +pre_build() { + cd $build_dir && + install_cmake_files $cmake_files_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + cmake_build_install +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/picosat-965/setup.sh b/crave/dependencies/picosat-965/setup.sh new file mode 100755 index 0000000..d041b89 --- /dev/null +++ b/crave/dependencies/picosat-965/setup.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +version=965 + +cmake_files_dir=$base_dir/picosat-936 + +source $base_dir/picosat-936/shared.sh diff --git a/crave/dependencies/puma-2.23/setup.sh b/crave/dependencies/puma-2.23/setup.sh new file mode 100644 index 0000000..95cb21f --- /dev/null +++ b/crave/dependencies/puma-2.23/setup.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +version=2.23 + +source $base_dir/puma-2.23/shared.sh + +# vim: ts=2 sw=2 et \ No newline at end of file diff --git a/crave/dependencies/puma-2.23/shared.sh b/crave/dependencies/puma-2.23/shared.sh new file mode 100644 index 0000000..6c94d56 --- /dev/null +++ b/crave/dependencies/puma-2.23/shared.sh @@ -0,0 +1,38 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + error '$build is undefined' +fi + +package=puma +source="$package-$version.tar.gz" +build_dir=$build/$package-$version +url="http://www.informatik.uni-bremen.de/revkit/files/$source" + +unpack() { + cd $cache && + message "unpacking $package" && + tar -xf $source && + mv -f $cache/$package $build_dir && + message "finished unpacking $package" +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + + # target directories + mkdir -p $target/{include,lib} + + # build + cd "$build_dir/bin" && + make -j$num_threads puma && + cd .. && + cp include/*.h $target/include && + cp lib/lib_puma.a $target/lib && + cd .. +} + +# vim: ts=2 sw=2 et \ No newline at end of file diff --git a/crave/dependencies/runlim-1.7/setup.sh b/crave/dependencies/runlim-1.7/setup.sh new file mode 100644 index 0000000..9f19fb3 --- /dev/null +++ b/crave/dependencies/runlim-1.7/setup.sh @@ -0,0 +1,8 @@ +#!/bin/sh + +version=1.7 + +source $base_dir/runlim-1.7/shared.sh + +# vim: ts=2 sw=2 et + diff --git a/crave/dependencies/runlim-1.7/shared.sh b/crave/dependencies/runlim-1.7/shared.sh new file mode 100644 index 0000000..17d0c8c --- /dev/null +++ b/crave/dependencies/runlim-1.7/shared.sh @@ -0,0 +1,37 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=runlim +source="${package}-$version.tar.gz" +build_dir="$build/${package}-$version" +url="http://fmv.jku.at/runlim/$source" + +unpack() { + cd $cache && + tar -xf $source && + rm -rf $build_dir && + mv -f $cache/$package-$version $build_dir +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + ./configure && + make -j$num_threads && + mkdir -p "$target" && + cp runlim "$target" +} + +# vim: ts=2 sw=2 et + diff --git a/crave/dependencies/setup_cmake_src b/crave/dependencies/setup_cmake_src new file mode 100755 index 0000000..beb6997 --- /dev/null +++ b/crave/dependencies/setup_cmake_src @@ -0,0 +1,18 @@ +#!/bin/bash + +base_dir=$( cd $(dirname $0) && pwd ) +source $base_dir/common.sh + +if [ $# -lt 2 ]; then + echo "usage: $0 package {package ...}" + exit 21 +fi + +build="$1" +shift; + +mkdir -p "$build" + +for p in $@; do + run_scripts download_unpack pre_build +done diff --git a/crave/dependencies/stp-2.3.3-basic/setup.sh b/crave/dependencies/stp-2.3.3-basic/setup.sh new file mode 100755 index 0000000..ab8b859 --- /dev/null +++ b/crave/dependencies/stp-2.3.3-basic/setup.sh @@ -0,0 +1,48 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=stp +version=2.3.3 +source=nosourcefile +build_dir=$build/$package-$version +url=https://github.com/stp/stp.git + +dependencies="minisat-git" + +download() { + mkdir -p $build_dir && + cd $build_dir && + if [ -d .git ]; then + git pull + else + git clone -b $version --single-branch $url . + fi + git reset --hard HEAD +} + +unset -f unpack +unpack() { + true +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd "$build_dir" && + export CMAKE_PREFIX_PATH="$root/minisat-git" && + cmake_build_install .. -DENABLE_PYTHON_INTERFACE=off -DONLY_SIMPLE=on -DNOCRYPTOMINISAT=on +} diff --git a/crave/dependencies/stp-git-basic/setup.sh b/crave/dependencies/stp-git-basic/setup.sh new file mode 100755 index 0000000..ae38e38 --- /dev/null +++ b/crave/dependencies/stp-git-basic/setup.sh @@ -0,0 +1,48 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=stp +version=git-basic +source=nosourcefile +build_dir=$build/$package-$version +url=https://github.com/stp/stp.git + +dependencies="minisat-git" + +download() { + mkdir -p $build_dir && + cd $build_dir && + if [ -d .git ]; then + git pull + else + git clone $url . + fi + git reset --hard HEAD +} + +unset -f unpack +unpack() { + true +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd "$build_dir" && + export CMAKE_PREFIX_PATH="$root/minisat-git" && + cmake_build_install .. -DENABLE_PYTHON_INTERFACE=off -DONLY_SIMPLE=on -DNOCRYPTOMINISAT=on +} diff --git a/crave/dependencies/stp-git/setup.sh b/crave/dependencies/stp-git/setup.sh new file mode 100755 index 0000000..c3873f2 --- /dev/null +++ b/crave/dependencies/stp-git/setup.sh @@ -0,0 +1,48 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=stp +version=git +source=nosourcefile +build_dir=$build/$package-$version +url=https://github.com/stp/stp.git + +dependencies="cryptominisat-git minisat-git" + +download() { + mkdir -p $build_dir && + cd $build_dir && + if [ -d .git ]; then + git pull + else + git clone $url . + fi + git reset --hard HEAD +} + +unset -f unpack +unpack() { + true +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd "$build_dir" && + export CMAKE_PREFIX_PATH="$root/cryptominisat-git:$root/minisat-git" && + cmake_build_install .. -DENABLE_PYTHON_INTERFACE=off -DONLY_SIMPLE=on +} diff --git a/crave/dependencies/swig-2.0.2/setup.sh b/crave/dependencies/swig-2.0.2/setup.sh new file mode 100644 index 0000000..f9e3609 --- /dev/null +++ b/crave/dependencies/swig-2.0.2/setup.sh @@ -0,0 +1,8 @@ +#!/bin/sh + +version=2.0.2 +pcre_version=8.30 + +source $base_dir/swig-2.0.2/shared.sh + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/swig-2.0.2/shared.sh b/crave/dependencies/swig-2.0.2/shared.sh new file mode 100644 index 0000000..2242233 --- /dev/null +++ b/crave/dependencies/swig-2.0.2/shared.sh @@ -0,0 +1,54 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=swig +source=${package}-$version.tar.gz +build_dir=$build/${package}-$version +url=http://ovh.dl.sourceforge.net/project/${package}/${package}/${package}-${version}/$source + +unset -f download +download() { + cd $cache && + wget -c -O $source $url && + wget -c ftp://ftp.csx.cam.ac.uk/pub/software/programming/pcre/pcre-${pcre_version}.tar.gz && + cd - +} + +unpack() { + cd $cache && + tar -xf $source && + rm -rf $build_dir && + mv -f $cache/$package-$version $build_dir +} + +pre_build() { + cd $build_dir && + mkdir -p build && + cd build && + cp $cache/pcre-${pcre_version}.tar.gz . +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + COMMON_OPTS=" + --prefix=$target + " + cd $build_dir/build && + ../Tools/pcre-build.sh && + ../configure $COMMON_OPTS && + make -j$num_threads && + make install +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/systemc-2.3.1/setup.sh b/crave/dependencies/systemc-2.3.1/setup.sh new file mode 100644 index 0000000..930603e --- /dev/null +++ b/crave/dependencies/systemc-2.3.1/setup.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +version=2.3.1 +branch=v2.3.1 +package=systemc +source=nosourcefile +build_dir=$build/$package-$version +url=https://github.com/ArchC/SystemC.git + +source "$base_dir/systemc-2.3/shared.sh" diff --git a/crave/dependencies/yices-2.5.1/setup.sh b/crave/dependencies/yices-2.5.1/setup.sh new file mode 100644 index 0000000..8ebffff --- /dev/null +++ b/crave/dependencies/yices-2.5.1/setup.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +version=2.5.1 + +config_files_dir=$base_dir/yices-2.4.2 + +source $base_dir/yices-2.4.2/shared.sh diff --git a/crave/dependencies/yices-git/setup.sh b/crave/dependencies/yices-git/setup.sh new file mode 100755 index 0000000..355a88b --- /dev/null +++ b/crave/dependencies/yices-git/setup.sh @@ -0,0 +1,8 @@ +#!/bin/sh + +version=git +branch=master + +config_files_dir=$base_dir/yices-git + +source $base_dir/yices-git/shared.sh diff --git a/crave/dependencies/yices-git/shared.sh b/crave/dependencies/yices-git/shared.sh new file mode 100644 index 0000000..9397bc3 --- /dev/null +++ b/crave/dependencies/yices-git/shared.sh @@ -0,0 +1,48 @@ +#!/bin/sh + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$package_dir is undefined' + exit 1 +fi + +package=yices +source=nosourcefile +build_dir=$build/$package-$version +url='https://github.com/SRI-CSL/yices2' + +download() { + mkdir -p $cache/$package-$version && + cd $cache/$package-$version && + if [ -d .git ]; then + git pull + else + git clone $url . + git checkout $branch + fi +} + +unpack() { + cp -R $cache/$package-$version $build_dir +} + +pre_build() { + true +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + autoconf && + ./configure --prefix="$target" && + make && + make install && + cp $config_files_dir/yices2-config.cmake "$target" +} + diff --git a/crave/dependencies/yices-git/yices2-config.cmake b/crave/dependencies/yices-git/yices2-config.cmake new file mode 100644 index 0000000..c5cf59b --- /dev/null +++ b/crave/dependencies/yices-git/yices2-config.cmake @@ -0,0 +1,5 @@ +get_filename_component(YICES2_DIR ${CMAKE_CURRENT_LIST_FILE} PATH) +set(YICES2_BIN_DIRS ${YICES2_DIR}/bin ) +set(YICES2_INCLUDE_DIRS ${YICES2_DIR}/include ) +set(YICES2_INCLUDE_DIR ${YICES2_INCLUDE_DIRS} ) +set(YICES2_LIBRARIES ${YICES2_DIR}/lib/libyices.so ) diff --git a/crave/dependencies/zchaff-2007.3.12/CMakeLists.txt b/crave/dependencies/zchaff-2007.3.12/CMakeLists.txt new file mode 100644 index 0000000..e346c69 --- /dev/null +++ b/crave/dependencies/zchaff-2007.3.12/CMakeLists.txt @@ -0,0 +1,105 @@ +project(zChaff) +cmake_minimum_required(VERSION 2.8) +set(zChaff_VERSION) + +set(STATIC_OR_SHARED SHARED CACHE STRING "Build STATIC or SHARED libaries") + +add_custom_command( + OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/zchaff_c_wrapper.cpp + COMMAND sed 's/EXTERN/extern \"C\"/' ${CMAKE_CURRENT_SOURCE_DIR}/zchaff_wrapper.wrp > ${CMAKE_CURRENT_BINARY_DIR}/zchaff_c_wrapper.cpp + DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/zchaff_wrapper.wrp +) +add_custom_command( + OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/zchaff_cpp_wrapper.cpp + COMMAND sed 's/EXTERN//' ${CMAKE_CURRENT_SOURCE_DIR}/zchaff_wrapper.wrp > ${CMAKE_CURRENT_BINARY_DIR}/zchaff_cpp_wrapper.cpp + DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/zchaff_wrapper.wrp +) + +include_directories( ${CMAKE_CURRENT_SOURCE_DIR} ) + +set( zChaff_SOURCES + zchaff_solver.cpp + zchaff_base.cpp + zchaff_dbase.cpp + zchaff_utils.cpp + ${CMAKE_CURRENT_BINARY_DIR}/zchaff_c_wrapper.cpp + ${CMAKE_CURRENT_BINARY_DIR}/zchaff_cpp_wrapper.cpp +) + +add_library(zChaff_libzChaff + ${STATIC_OR_SHARED} + ${zChaff_SOURCES} +) +SET_TARGET_PROPERTIES( zChaff_libzChaff PROPERTIES + OUTPUT_NAME zchaff +) + +add_executable(zChaff + sat_solver.cpp + ${zChaff_SOURCES} +) +SET_TARGET_PROPERTIES( zChaff PROPERTIES + OUTPUT_NAME zchaff +) + +add_executable(zChaff_verify_df + zverify_df.cpp +) +SET_TARGET_PROPERTIES( zChaff_verify_df PROPERTIES + OUTPUT_NAME zverify_df +) + +add_executable(zChaff_zminimal + zminimal.cpp + ${zChaff_SOURCES} +) +SET_TARGET_PROPERTIES( zChaff_zminimal PROPERTIES + OUTPUT_NAME zminimal +) + +add_executable(zChaff_cnf_stats + cnf_stats.cpp +) +SET_TARGET_PROPERTIES( zChaff_cnf_stats PROPERTIES + OUTPUT_NAME cnf_stats +) + +set(zChaff_LIBRARIES zChaff_libzChaff) + +configure_file(zChaffConfig.cmake ${PROJECT_BINARY_DIR}/zChaffConfig.cmake @ONLY) +configure_file(zChaffConfigVersion.cmake ${PROJECT_BINARY_DIR}/zChaffConfigVersion.cmake @ONLY) +## create libzChaff config file for internal use +file(WRITE ${PROJECT_BINARY_DIR}/zChaff.cmake +"set(zChaff_INCLUDE_DIR + ${PROJECT_SOURCE_DIR} +) +") +## export target with install +INSTALL( FILES + ${PROJECT_BINARY_DIR}/zChaffConfig.cmake + ${PROJECT_BINARY_DIR}/zChaffConfigVersion.cmake + DESTINATION share/zChaff) +install(EXPORT zChaff DESTINATION share/zChaff) + +install(TARGETS + zChaff_libzChaff + zChaff + zChaff_verify_df + zChaff_zminimal + zChaff_cnf_stats + EXPORT zChaff + ARCHIVE DESTINATION lib + LIBRARY DESTINATION lib + RUNTIME DESTINATION bin +) + + +install(FILES + SAT.h + zchaff_clsgen.h + zchaff_header.h + zchaff_version.h + zchaff_base.h + zchaff_dbase.h + zchaff_solver.h + DESTINATION include) diff --git a/crave/dependencies/zchaff-2007.3.12/missing_includes.patch b/crave/dependencies/zchaff-2007.3.12/missing_includes.patch new file mode 100644 index 0000000..5deee99 --- /dev/null +++ b/crave/dependencies/zchaff-2007.3.12/missing_includes.patch @@ -0,0 +1,57 @@ +diff -ur zchaff64/cnf_stats.cpp zchaff-2007.3.12/cnf_stats.cpp +--- zchaff64/cnf_stats.cpp 2007-03-14 03:48:02.000000000 +0100 ++++ zchaff-2007.3.12/cnf_stats.cpp 2011-04-08 13:44:00.014474533 +0200 +@@ -2,6 +2,7 @@ + #include + #include + #include ++#include + + #include + #include +diff -ur zchaff64/sat_solver.cpp zchaff-2007.3.12/sat_solver.cpp +--- zchaff64/sat_solver.cpp 2007-03-14 03:48:02.000000000 +0100 ++++ zchaff-2007.3.12/sat_solver.cpp 2011-04-08 13:44:00.014474533 +0200 +@@ -38,6 +38,7 @@ + #include + #include + #include ++#include + + #include + #include +diff -ur zchaff64/zchaff_dbase.cpp zchaff-2007.3.12/zchaff_dbase.cpp +--- zchaff64/zchaff_dbase.cpp 2007-03-14 03:48:27.000000000 +0100 ++++ zchaff-2007.3.12/zchaff_dbase.cpp 2011-04-08 13:44:00.015557772 +0200 +@@ -36,6 +36,7 @@ + #include + #include + #include ++#include + + using namespace std; + +diff -ur zchaff64/zminimal.cpp zchaff-2007.3.12/zminimal.cpp +--- zchaff64/zminimal.cpp 2007-03-14 03:48:02.000000000 +0100 ++++ zchaff-2007.3.12/zminimal.cpp 2011-04-08 13:49:40.343011798 +0200 +@@ -39,6 +39,7 @@ + #include + #include + #include ++#include + + using namespace std; + +diff -ur zchaff64/zverify_df.cpp zchaff-2007.3.12/zverify_df.cpp +--- zchaff64/zverify_df.cpp 2007-04-11 20:49:33.000000000 +0200 ++++ zchaff-2007.3.12/zverify_df.cpp 2011-04-08 13:44:00.016557463 +0200 +@@ -40,6 +40,9 @@ + #include + #include + #include ++#include ++#include ++#include + + using namespace std; + diff --git a/crave/dependencies/zchaff-2007.3.12/setup.sh b/crave/dependencies/zchaff-2007.3.12/setup.sh new file mode 100755 index 0000000..a5ce923 --- /dev/null +++ b/crave/dependencies/zchaff-2007.3.12/setup.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +version=2007.3.12 + +patches_dir=$base_dir/zchaff-2007.3.12 +cmake_files_dir=$base_dir/zchaff-2007.3.12 + +source $base_dir/zchaff-2007.3.12/shared.sh + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/zchaff-2007.3.12/shared.sh b/crave/dependencies/zchaff-2007.3.12/shared.sh new file mode 100644 index 0000000..39d415f --- /dev/null +++ b/crave/dependencies/zchaff-2007.3.12/shared.sh @@ -0,0 +1,50 @@ +#!/bin/sh + + +if [ -z "$build" ] ; then + echo '$build is undefined' + exit 1 +fi +if [ -z "$package_dir" ] ; then + echo '$build is undefined' + exit 1 +fi + +package=zchaff +case "$ARCH" in + i?86) + source="${package}.${version}.zip" + export CFLAGS=-m32 + export CXXFLAGS=-m32 + ;; + x86_64|x86-64) + source="${package}.64bit.${version}.zip"; bits=64;; + *) error "$package not avaiable for architechture $ARCH"; ;; +esac +build_dir=$build/$package-$version +url=http://www.princeton.edu/~chaff/zchaff/$source + +unpack() { + cd $cache && + unzip $source && + patch -p0 < $patches_dir/missing_includes.patch && + rm -rf $build_dir && + mv -f $cache/$package${bits:-""} $build_dir +} + +pre_build() { + cd $build_dir && + install_cmake_files $cmake_files_dir && + sed -i 3s/zChaff_VERSION/"zChaff_VERSION $version"/ $build_dir/CMakeLists.txt +} + +build_install() { + if [ -z "$target" ] ; then + echo '$target is undefined' + exit 1 + fi + cd $build_dir && + cmake_build_install +} + +# vim: ts=2 sw=2 et diff --git a/crave/dependencies/zchaff-2007.3.12/zChaffConfig.cmake b/crave/dependencies/zchaff-2007.3.12/zChaffConfig.cmake new file mode 100644 index 0000000..b6f5e55 --- /dev/null +++ b/crave/dependencies/zchaff-2007.3.12/zChaffConfig.cmake @@ -0,0 +1,16 @@ +set(zChaff_FOUND 1) +set(zChaff_VERSION @zChaff_VERSION@) +get_filename_component(zChaff_CONFIG_DIR "${CMAKE_CURRENT_LIST_FILE}" PATH) + +set(zChaff_INCLUDE_DIR ${zChaff_CONFIG_DIR}/../../include) +set(zChaff_INCLUDE_DIRS ${zChaff_INCLUDE_DIR}) +set(zChaff_LIBRARIES @zChaff_LIBRARIES@) + +set(zchaff_BIN_DIR @CMAKE_INSTALL_PREFIX@/bin ) +set(zchaff_BIN_DIRS ${zchaff_BIN_DIR} ) +set(zchaff_INCLUDE_DIR ${zChaff_INCLUDE_DIR} ) +set(zchaff_INCLUDE_DIRS ${zChaff_INCLUDE_DIR} ) +set(zchaff_LIBRARIES ${zChaff_LIBRARIES} ) + +include("${zChaff_CONFIG_DIR}/zChaff.cmake" ) + diff --git a/crave/dependencies/zchaff-2007.3.12/zChaffConfigVersion.cmake b/crave/dependencies/zchaff-2007.3.12/zChaffConfigVersion.cmake new file mode 100644 index 0000000..faaca4d --- /dev/null +++ b/crave/dependencies/zchaff-2007.3.12/zChaffConfigVersion.cmake @@ -0,0 +1,4 @@ +if("${PACKAGE_FIND_VERSION}" VERSION_EQUAL @zChaff_VERSION@) +set(PACKAGE_VERSION_EXACT 1) +set(PACKAGE_VERSION_COMPATIBLE 1) +endif("${PACKAGE_FIND_VERSION}" VERSION_EQUAL @zChaff_VERSION@) diff --git a/crave/doc/Doxyfile b/crave/doc/Doxyfile new file mode 100644 index 0000000..5763a6b --- /dev/null +++ b/crave/doc/Doxyfile @@ -0,0 +1,2404 @@ +# Doxyfile 1.8.8 + +# This file describes the settings to be used by the documentation system +# doxygen (www.doxygen.org) for a project. +# +# All text after a double hash (##) is considered a comment and is placed in +# front of the TAG it is preceding. +# +# All text after a single hash (#) is considered a comment and will be ignored. +# The format is: +# TAG = value [value, ...] +# For lists, items can also be appended using: +# TAG += value [value, ...] +# Values that contain spaces should be placed between quotes (\" \"). + +#--------------------------------------------------------------------------- +# Project related configuration options +#--------------------------------------------------------------------------- + +# This tag specifies the encoding used for all characters in the config file +# that follow. The default is UTF-8 which is also the encoding used for all text +# before the first occurrence of this tag. Doxygen uses libiconv (or the iconv +# built into libc) for the transcoding. See http://www.gnu.org/software/libiconv +# for the list of possible encodings. +# The default value is: UTF-8. + +DOXYFILE_ENCODING = UTF-8 + +# The PROJECT_NAME tag is a single word (or a sequence of words surrounded by +# double-quotes, unless you are using Doxywizard) that should identify the +# project for which the documentation is generated. This name is used in the +# title of most generated pages and in a few other places. +# The default value is: My Project. + +PROJECT_NAME = crave + +# The PROJECT_NUMBER tag can be used to enter a project or revision number. This +# could be handy for archiving the generated documentation or if some version +# control system is used. + +PROJECT_NUMBER = + +# Using the PROJECT_BRIEF tag one can provide an optional one line description +# for a project that appears at the top of each page and should give viewer a +# quick idea about the purpose of the project. Keep the description short. + +PROJECT_BRIEF = + +# With the PROJECT_LOGO tag one can specify an logo or icon that is included in +# the documentation. The maximum height of the logo should not exceed 55 pixels +# and the maximum width should not exceed 200 pixels. Doxygen will copy the logo +# to the output directory. + +PROJECT_LOGO = + +# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute) path +# into which the generated documentation will be written. If a relative path is +# entered, it will be relative to the location where doxygen was started. If +# left blank the current directory will be used. + +OUTPUT_DIRECTORY = doc/crave-doxygen/ + +# If the CREATE_SUBDIRS tag is set to YES, then doxygen will create 4096 sub- +# directories (in 2 levels) under the output directory of each output format and +# will distribute the generated files over these directories. Enabling this +# option can be useful when feeding doxygen a huge amount of source files, where +# putting all generated files in the same directory would otherwise causes +# performance problems for the file system. +# The default value is: NO. + +CREATE_SUBDIRS = NO + +# If the ALLOW_UNICODE_NAMES tag is set to YES, doxygen will allow non-ASCII +# characters to appear in the names of generated files. If set to NO, non-ASCII +# characters will be escaped, for example _xE3_x81_x84 will be used for Unicode +# U+3044. +# The default value is: NO. + +ALLOW_UNICODE_NAMES = NO + +# The OUTPUT_LANGUAGE tag is used to specify the language in which all +# documentation generated by doxygen is written. Doxygen will use this +# information to generate all constant output in the proper language. +# Possible values are: Afrikaans, Arabic, Armenian, Brazilian, Catalan, Chinese, +# Chinese-Traditional, Croatian, Czech, Danish, Dutch, English (United States), +# Esperanto, Farsi (Persian), Finnish, French, German, Greek, Hungarian, +# Indonesian, Italian, Japanese, Japanese-en (Japanese with English messages), +# Korean, Korean-en (Korean with English messages), Latvian, Lithuanian, +# Macedonian, Norwegian, Persian (Farsi), Polish, Portuguese, Romanian, Russian, +# Serbian, Serbian-Cyrillic, Slovak, Slovene, Spanish, Swedish, Turkish, +# Ukrainian and Vietnamese. +# The default value is: English. + +OUTPUT_LANGUAGE = English + +# If the BRIEF_MEMBER_DESC tag is set to YES doxygen will include brief member +# descriptions after the members that are listed in the file and class +# documentation (similar to Javadoc). Set to NO to disable this. +# The default value is: YES. + +BRIEF_MEMBER_DESC = YES + +# If the REPEAT_BRIEF tag is set to YES doxygen will prepend the brief +# description of a member or function before the detailed description +# +# Note: If both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the +# brief descriptions will be completely suppressed. +# The default value is: YES. + +REPEAT_BRIEF = YES + +# This tag implements a quasi-intelligent brief description abbreviator that is +# used to form the text in various listings. Each string in this list, if found +# as the leading text of the brief description, will be stripped from the text +# and the result, after processing the whole list, is used as the annotated +# text. Otherwise, the brief description is used as-is. If left blank, the +# following values are used ($name is automatically replaced with the name of +# the entity):The $name class, The $name widget, The $name file, is, provides, +# specifies, contains, represents, a, an and the. + +ABBREVIATE_BRIEF = "The $name class" \ + "The $name widget" \ + "The $name file" \ + is \ + provides \ + specifies \ + contains \ + represents \ + a \ + an \ + the + +# If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then +# doxygen will generate a detailed section even if there is only a brief +# description. +# The default value is: NO. + +ALWAYS_DETAILED_SEC = NO + +# If the INLINE_INHERITED_MEMB tag is set to YES, doxygen will show all +# inherited members of a class in the documentation of that class as if those +# members were ordinary class members. Constructors, destructors and assignment +# operators of the base classes will not be shown. +# The default value is: NO. + +INLINE_INHERITED_MEMB = NO + +# If the FULL_PATH_NAMES tag is set to YES doxygen will prepend the full path +# before files name in the file list and in the header files. If set to NO the +# shortest path that makes the file name unique will be used +# The default value is: YES. + +FULL_PATH_NAMES = YES + +# The STRIP_FROM_PATH tag can be used to strip a user-defined part of the path. +# Stripping is only done if one of the specified strings matches the left-hand +# part of the path. The tag can be used to show relative paths in the file list. +# If left blank the directory from which doxygen is run is used as the path to +# strip. +# +# Note that you can specify absolute paths here, but also relative paths, which +# will be relative from the directory where doxygen is started. +# This tag requires that the tag FULL_PATH_NAMES is set to YES. + +STRIP_FROM_PATH = + +# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of the +# path mentioned in the documentation of a class, which tells the reader which +# header file to include in order to use a class. If left blank only the name of +# the header file containing the class definition is used. Otherwise one should +# specify the list of include paths that are normally passed to the compiler +# using the -I flag. + +STRIP_FROM_INC_PATH = + +# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter (but +# less readable) file names. This can be useful is your file systems doesn't +# support long names like on DOS, Mac, or CD-ROM. +# The default value is: NO. + +SHORT_NAMES = NO + +# If the JAVADOC_AUTOBRIEF tag is set to YES then doxygen will interpret the +# first line (until the first dot) of a Javadoc-style comment as the brief +# description. If set to NO, the Javadoc-style will behave just like regular Qt- +# style comments (thus requiring an explicit @brief command for a brief +# description.) +# The default value is: NO. + +JAVADOC_AUTOBRIEF = NO + +# If the QT_AUTOBRIEF tag is set to YES then doxygen will interpret the first +# line (until the first dot) of a Qt-style comment as the brief description. If +# set to NO, the Qt-style will behave just like regular Qt-style comments (thus +# requiring an explicit \brief command for a brief description.) +# The default value is: NO. + +QT_AUTOBRIEF = NO + +# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make doxygen treat a +# multi-line C++ special comment block (i.e. a block of //! or /// comments) as +# a brief description. This used to be the default behavior. The new default is +# to treat a multi-line C++ comment block as a detailed description. Set this +# tag to YES if you prefer the old behavior instead. +# +# Note that setting this tag to YES also means that rational rose comments are +# not recognized any more. +# The default value is: NO. + +MULTILINE_CPP_IS_BRIEF = NO + +# If the INHERIT_DOCS tag is set to YES then an undocumented member inherits the +# documentation from any documented member that it re-implements. +# The default value is: YES. + +INHERIT_DOCS = YES + +# If the SEPARATE_MEMBER_PAGES tag is set to YES, then doxygen will produce a +# new page for each member. If set to NO, the documentation of a member will be +# part of the file/class/namespace that contains it. +# The default value is: NO. + +SEPARATE_MEMBER_PAGES = NO + +# The TAB_SIZE tag can be used to set the number of spaces in a tab. Doxygen +# uses this value to replace tabs by spaces in code fragments. +# Minimum value: 1, maximum value: 16, default value: 4. + +TAB_SIZE = 4 + +# This tag can be used to specify a number of aliases that act as commands in +# the documentation. An alias has the form: +# name=value +# For example adding +# "sideeffect=@par Side Effects:\n" +# will allow you to put the command \sideeffect (or @sideeffect) in the +# documentation, which will result in a user-defined paragraph with heading +# "Side Effects:". You can put \n's in the value part of an alias to insert +# newlines. + +ALIASES = + +# This tag can be used to specify a number of word-keyword mappings (TCL only). +# A mapping has the form "name=value". For example adding "class=itcl::class" +# will allow you to use the command class in the itcl::class meaning. + +TCL_SUBST = + +# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C sources +# only. Doxygen will then generate output that is more tailored for C. For +# instance, some of the names that are used will be different. The list of all +# members will be omitted, etc. +# The default value is: NO. + +OPTIMIZE_OUTPUT_FOR_C = NO + +# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java or +# Python sources only. Doxygen will then generate output that is more tailored +# for that language. For instance, namespaces will be presented as packages, +# qualified scopes will look different, etc. +# The default value is: NO. + +OPTIMIZE_OUTPUT_JAVA = NO + +# Set the OPTIMIZE_FOR_FORTRAN tag to YES if your project consists of Fortran +# sources. Doxygen will then generate output that is tailored for Fortran. +# The default value is: NO. + +OPTIMIZE_FOR_FORTRAN = NO + +# Set the OPTIMIZE_OUTPUT_VHDL tag to YES if your project consists of VHDL +# sources. Doxygen will then generate output that is tailored for VHDL. +# The default value is: NO. + +OPTIMIZE_OUTPUT_VHDL = NO + +# Doxygen selects the parser to use depending on the extension of the files it +# parses. With this tag you can assign which parser to use for a given +# extension. Doxygen has a built-in mapping, but you can override or extend it +# using this tag. The format is ext=language, where ext is a file extension, and +# language is one of the parsers supported by doxygen: IDL, Java, Javascript, +# C#, C, C++, D, PHP, Objective-C, Python, Fortran (fixed format Fortran: +# FortranFixed, free formatted Fortran: FortranFree, unknown formatted Fortran: +# Fortran. In the later case the parser tries to guess whether the code is fixed +# or free formatted code, this is the default for Fortran type files), VHDL. For +# instance to make doxygen treat .inc files as Fortran files (default is PHP), +# and .f files as C (default is Fortran), use: inc=Fortran f=C. +# +# Note For files without extension you can use no_extension as a placeholder. +# +# Note that for custom extensions you also need to set FILE_PATTERNS otherwise +# the files are not read by doxygen. + +EXTENSION_MAPPING = + +# If the MARKDOWN_SUPPORT tag is enabled then doxygen pre-processes all comments +# according to the Markdown format, which allows for more readable +# documentation. See http://daringfireball.net/projects/markdown/ for details. +# The output of markdown processing is further processed by doxygen, so you can +# mix doxygen, HTML, and XML commands with Markdown formatting. Disable only in +# case of backward compatibilities issues. +# The default value is: YES. + +MARKDOWN_SUPPORT = YES + +# When enabled doxygen tries to link words that correspond to documented +# classes, or namespaces to their corresponding documentation. Such a link can +# be prevented in individual cases by by putting a % sign in front of the word +# or globally by setting AUTOLINK_SUPPORT to NO. +# The default value is: YES. + +AUTOLINK_SUPPORT = YES + +# If you use STL classes (i.e. std::string, std::vector, etc.) but do not want +# to include (a tag file for) the STL sources as input, then you should set this +# tag to YES in order to let doxygen match functions declarations and +# definitions whose arguments contain STL classes (e.g. func(std::string); +# versus func(std::string) {}). This also make the inheritance and collaboration +# diagrams that involve STL classes more complete and accurate. +# The default value is: NO. + +BUILTIN_STL_SUPPORT = NO + +# If you use Microsoft's C++/CLI language, you should set this option to YES to +# enable parsing support. +# The default value is: NO. + +CPP_CLI_SUPPORT = NO + +# Set the SIP_SUPPORT tag to YES if your project consists of sip (see: +# http://www.riverbankcomputing.co.uk/software/sip/intro) sources only. Doxygen +# will parse them like normal C++ but will assume all classes use public instead +# of private inheritance when no explicit protection keyword is present. +# The default value is: NO. + +SIP_SUPPORT = NO + +# For Microsoft's IDL there are propget and propput attributes to indicate +# getter and setter methods for a property. Setting this option to YES will make +# doxygen to replace the get and set methods by a property in the documentation. +# This will only work if the methods are indeed getting or setting a simple +# type. If this is not the case, or you want to show the methods anyway, you +# should set this option to NO. +# The default value is: YES. + +IDL_PROPERTY_SUPPORT = YES + +# If member grouping is used in the documentation and the DISTRIBUTE_GROUP_DOC +# tag is set to YES, then doxygen will reuse the documentation of the first +# member in the group (if any) for the other members of the group. By default +# all members of a group must be documented explicitly. +# The default value is: NO. + +DISTRIBUTE_GROUP_DOC = NO + +# Set the SUBGROUPING tag to YES to allow class member groups of the same type +# (for instance a group of public functions) to be put as a subgroup of that +# type (e.g. under the Public Functions section). Set it to NO to prevent +# subgrouping. Alternatively, this can be done per class using the +# \nosubgrouping command. +# The default value is: YES. + +SUBGROUPING = YES + +# When the INLINE_GROUPED_CLASSES tag is set to YES, classes, structs and unions +# are shown inside the group in which they are included (e.g. using \ingroup) +# instead of on a separate page (for HTML and Man pages) or section (for LaTeX +# and RTF). +# +# Note that this feature does not work in combination with +# SEPARATE_MEMBER_PAGES. +# The default value is: NO. + +INLINE_GROUPED_CLASSES = NO + +# When the INLINE_SIMPLE_STRUCTS tag is set to YES, structs, classes, and unions +# with only public data fields or simple typedef fields will be shown inline in +# the documentation of the scope in which they are defined (i.e. file, +# namespace, or group documentation), provided this scope is documented. If set +# to NO, structs, classes, and unions are shown on a separate page (for HTML and +# Man pages) or section (for LaTeX and RTF). +# The default value is: NO. + +INLINE_SIMPLE_STRUCTS = NO + +# When TYPEDEF_HIDES_STRUCT tag is enabled, a typedef of a struct, union, or +# enum is documented as struct, union, or enum with the name of the typedef. So +# typedef struct TypeS {} TypeT, will appear in the documentation as a struct +# with name TypeT. When disabled the typedef will appear as a member of a file, +# namespace, or class. And the struct will be named TypeS. This can typically be +# useful for C code in case the coding convention dictates that all compound +# types are typedef'ed and only the typedef is referenced, never the tag name. +# The default value is: NO. + +TYPEDEF_HIDES_STRUCT = NO + +# The size of the symbol lookup cache can be set using LOOKUP_CACHE_SIZE. This +# cache is used to resolve symbols given their name and scope. Since this can be +# an expensive process and often the same symbol appears multiple times in the +# code, doxygen keeps a cache of pre-resolved symbols. If the cache is too small +# doxygen will become slower. If the cache is too large, memory is wasted. The +# cache size is given by this formula: 2^(16+LOOKUP_CACHE_SIZE). The valid range +# is 0..9, the default is 0, corresponding to a cache size of 2^16=65536 +# symbols. At the end of a run doxygen will report the cache usage and suggest +# the optimal cache size from a speed point of view. +# Minimum value: 0, maximum value: 9, default value: 0. + +LOOKUP_CACHE_SIZE = 0 + +#--------------------------------------------------------------------------- +# Build related configuration options +#--------------------------------------------------------------------------- + +# If the EXTRACT_ALL tag is set to YES doxygen will assume all entities in +# documentation are documented, even if no documentation was available. Private +# class members and static file members will be hidden unless the +# EXTRACT_PRIVATE respectively EXTRACT_STATIC tags are set to YES. +# Note: This will also disable the warnings about undocumented members that are +# normally produced when WARNINGS is set to YES. +# The default value is: NO. + +EXTRACT_ALL = YES + +# If the EXTRACT_PRIVATE tag is set to YES all private members of a class will +# be included in the documentation. +# The default value is: NO. + +EXTRACT_PRIVATE = NO + +# If the EXTRACT_PACKAGE tag is set to YES all members with package or internal +# scope will be included in the documentation. +# The default value is: NO. + +EXTRACT_PACKAGE = NO + +# If the EXTRACT_STATIC tag is set to YES all static members of a file will be +# included in the documentation. +# The default value is: NO. + +EXTRACT_STATIC = NO + +# If the EXTRACT_LOCAL_CLASSES tag is set to YES classes (and structs) defined +# locally in source files will be included in the documentation. If set to NO +# only classes defined in header files are included. Does not have any effect +# for Java sources. +# The default value is: YES. + +EXTRACT_LOCAL_CLASSES = YES + +# This flag is only useful for Objective-C code. When set to YES local methods, +# which are defined in the implementation section but not in the interface are +# included in the documentation. If set to NO only methods in the interface are +# included. +# The default value is: NO. + +EXTRACT_LOCAL_METHODS = NO + +# If this flag is set to YES, the members of anonymous namespaces will be +# extracted and appear in the documentation as a namespace called +# 'anonymous_namespace{file}', where file will be replaced with the base name of +# the file that contains the anonymous namespace. By default anonymous namespace +# are hidden. +# The default value is: NO. + +EXTRACT_ANON_NSPACES = NO + +# If the HIDE_UNDOC_MEMBERS tag is set to YES, doxygen will hide all +# undocumented members inside documented classes or files. If set to NO these +# members will be included in the various overviews, but no documentation +# section is generated. This option has no effect if EXTRACT_ALL is enabled. +# The default value is: NO. + +HIDE_UNDOC_MEMBERS = NO + +# If the HIDE_UNDOC_CLASSES tag is set to YES, doxygen will hide all +# undocumented classes that are normally visible in the class hierarchy. If set +# to NO these classes will be included in the various overviews. This option has +# no effect if EXTRACT_ALL is enabled. +# The default value is: NO. + +HIDE_UNDOC_CLASSES = NO + +# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, doxygen will hide all friend +# (class|struct|union) declarations. If set to NO these declarations will be +# included in the documentation. +# The default value is: NO. + +HIDE_FRIEND_COMPOUNDS = NO + +# If the HIDE_IN_BODY_DOCS tag is set to YES, doxygen will hide any +# documentation blocks found inside the body of a function. If set to NO these +# blocks will be appended to the function's detailed documentation block. +# The default value is: NO. + +HIDE_IN_BODY_DOCS = NO + +# The INTERNAL_DOCS tag determines if documentation that is typed after a +# \internal command is included. If the tag is set to NO then the documentation +# will be excluded. Set it to YES to include the internal documentation. +# The default value is: NO. + +INTERNAL_DOCS = NO + +# If the CASE_SENSE_NAMES tag is set to NO then doxygen will only generate file +# names in lower-case letters. If set to YES upper-case letters are also +# allowed. This is useful if you have classes or files whose names only differ +# in case and if your file system supports case sensitive file names. Windows +# and Mac users are advised to set this option to NO. +# The default value is: system dependent. + +CASE_SENSE_NAMES = NO + +# If the HIDE_SCOPE_NAMES tag is set to NO then doxygen will show members with +# their full class and namespace scopes in the documentation. If set to YES the +# scope will be hidden. +# The default value is: NO. + +HIDE_SCOPE_NAMES = NO + +# If the SHOW_INCLUDE_FILES tag is set to YES then doxygen will put a list of +# the files that are included by a file in the documentation of that file. +# The default value is: YES. + +SHOW_INCLUDE_FILES = NO + +# If the SHOW_GROUPED_MEMB_INC tag is set to YES then Doxygen will add for each +# grouped member an include statement to the documentation, telling the reader +# which file to include in order to use the member. +# The default value is: NO. + +SHOW_GROUPED_MEMB_INC = NO + +# If the FORCE_LOCAL_INCLUDES tag is set to YES then doxygen will list include +# files with double quotes in the documentation rather than with sharp brackets. +# The default value is: NO. + +FORCE_LOCAL_INCLUDES = NO + +# If the INLINE_INFO tag is set to YES then a tag [inline] is inserted in the +# documentation for inline members. +# The default value is: YES. + +INLINE_INFO = YES + +# If the SORT_MEMBER_DOCS tag is set to YES then doxygen will sort the +# (detailed) documentation of file and class members alphabetically by member +# name. If set to NO the members will appear in declaration order. +# The default value is: YES. + +SORT_MEMBER_DOCS = YES + +# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the brief +# descriptions of file, namespace and class members alphabetically by member +# name. If set to NO the members will appear in declaration order. Note that +# this will also influence the order of the classes in the class list. +# The default value is: NO. + +SORT_BRIEF_DOCS = NO + +# If the SORT_MEMBERS_CTORS_1ST tag is set to YES then doxygen will sort the +# (brief and detailed) documentation of class members so that constructors and +# destructors are listed first. If set to NO the constructors will appear in the +# respective orders defined by SORT_BRIEF_DOCS and SORT_MEMBER_DOCS. +# Note: If SORT_BRIEF_DOCS is set to NO this option is ignored for sorting brief +# member documentation. +# Note: If SORT_MEMBER_DOCS is set to NO this option is ignored for sorting +# detailed member documentation. +# The default value is: NO. + +SORT_MEMBERS_CTORS_1ST = NO + +# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the hierarchy +# of group names into alphabetical order. If set to NO the group names will +# appear in their defined order. +# The default value is: NO. + +SORT_GROUP_NAMES = NO + +# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be sorted by +# fully-qualified names, including namespaces. If set to NO, the class list will +# be sorted only by class name, not including the namespace part. +# Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES. +# Note: This option applies only to the class list, not to the alphabetical +# list. +# The default value is: NO. + +SORT_BY_SCOPE_NAME = NO + +# If the STRICT_PROTO_MATCHING option is enabled and doxygen fails to do proper +# type resolution of all parameters of a function it will reject a match between +# the prototype and the implementation of a member function even if there is +# only one candidate or it is obvious which candidate to choose by doing a +# simple string match. By disabling STRICT_PROTO_MATCHING doxygen will still +# accept a match between prototype and implementation in such cases. +# The default value is: NO. + +STRICT_PROTO_MATCHING = NO + +# The GENERATE_TODOLIST tag can be used to enable ( YES) or disable ( NO) the +# todo list. This list is created by putting \todo commands in the +# documentation. +# The default value is: YES. + +GENERATE_TODOLIST = NO + +# The GENERATE_TESTLIST tag can be used to enable ( YES) or disable ( NO) the +# test list. This list is created by putting \test commands in the +# documentation. +# The default value is: YES. + +GENERATE_TESTLIST = NO + +# The GENERATE_BUGLIST tag can be used to enable ( YES) or disable ( NO) the bug +# list. This list is created by putting \bug commands in the documentation. +# The default value is: YES. + +GENERATE_BUGLIST = NO + +# The GENERATE_DEPRECATEDLIST tag can be used to enable ( YES) or disable ( NO) +# the deprecated list. This list is created by putting \deprecated commands in +# the documentation. +# The default value is: YES. + +GENERATE_DEPRECATEDLIST= NO + +# The ENABLED_SECTIONS tag can be used to enable conditional documentation +# sections, marked by \if ... \endif and \cond +# ... \endcond blocks. + +ENABLED_SECTIONS = + +# The MAX_INITIALIZER_LINES tag determines the maximum number of lines that the +# initial value of a variable or macro / define can have for it to appear in the +# documentation. If the initializer consists of more lines than specified here +# it will be hidden. Use a value of 0 to hide initializers completely. The +# appearance of the value of individual variables and macros / defines can be +# controlled using \showinitializer or \hideinitializer command in the +# documentation regardless of this setting. +# Minimum value: 0, maximum value: 10000, default value: 30. + +MAX_INITIALIZER_LINES = 30 + +# Set the SHOW_USED_FILES tag to NO to disable the list of files generated at +# the bottom of the documentation of classes and structs. If set to YES the list +# will mention the files that were used to generate the documentation. +# The default value is: YES. + +SHOW_USED_FILES = YES + +# Set the SHOW_FILES tag to NO to disable the generation of the Files page. This +# will remove the Files entry from the Quick Index and from the Folder Tree View +# (if specified). +# The default value is: YES. + +SHOW_FILES = YES + +# Set the SHOW_NAMESPACES tag to NO to disable the generation of the Namespaces +# page. This will remove the Namespaces entry from the Quick Index and from the +# Folder Tree View (if specified). +# The default value is: YES. + +SHOW_NAMESPACES = YES + +# The FILE_VERSION_FILTER tag can be used to specify a program or script that +# doxygen should invoke to get the current version for each file (typically from +# the version control system). Doxygen will invoke the program by executing (via +# popen()) the command command input-file, where command is the value of the +# FILE_VERSION_FILTER tag, and input-file is the name of an input file provided +# by doxygen. Whatever the program writes to standard output is used as the file +# version. For an example see the documentation. + +FILE_VERSION_FILTER = + +# The LAYOUT_FILE tag can be used to specify a layout file which will be parsed +# by doxygen. The layout file controls the global structure of the generated +# output files in an output format independent way. To create the layout file +# that represents doxygen's defaults, run doxygen with the -l option. You can +# optionally specify a file name after the option, if omitted DoxygenLayout.xml +# will be used as the name of the layout file. +# +# Note that if you run doxygen from a directory containing a file called +# DoxygenLayout.xml, doxygen will parse it automatically even if the LAYOUT_FILE +# tag is left empty. + +LAYOUT_FILE = + +# The CITE_BIB_FILES tag can be used to specify one or more bib files containing +# the reference definitions. This must be a list of .bib files. The .bib +# extension is automatically appended if omitted. This requires the bibtex tool +# to be installed. See also http://en.wikipedia.org/wiki/BibTeX for more info. +# For LaTeX the style of the bibliography can be controlled using +# LATEX_BIB_STYLE. To use this feature you need bibtex and perl available in the +# search path. See also \cite for info how to create references. + +CITE_BIB_FILES = + +#--------------------------------------------------------------------------- +# Configuration options related to warning and progress messages +#--------------------------------------------------------------------------- + +# The QUIET tag can be used to turn on/off the messages that are generated to +# standard output by doxygen. If QUIET is set to YES this implies that the +# messages are off. +# The default value is: NO. + +QUIET = NO + +# The WARNINGS tag can be used to turn on/off the warning messages that are +# generated to standard error ( stderr) by doxygen. If WARNINGS is set to YES +# this implies that the warnings are on. +# +# Tip: Turn warnings on while writing the documentation. +# The default value is: YES. + +WARNINGS = YES + +# If the WARN_IF_UNDOCUMENTED tag is set to YES, then doxygen will generate +# warnings for undocumented members. If EXTRACT_ALL is set to YES then this flag +# will automatically be disabled. +# The default value is: YES. + +WARN_IF_UNDOCUMENTED = YES + +# If the WARN_IF_DOC_ERROR tag is set to YES, doxygen will generate warnings for +# potential errors in the documentation, such as not documenting some parameters +# in a documented function, or documenting parameters that don't exist or using +# markup commands wrongly. +# The default value is: YES. + +WARN_IF_DOC_ERROR = YES + +# This WARN_NO_PARAMDOC option can be enabled to get warnings for functions that +# are documented, but have no documentation for their parameters or return +# value. If set to NO doxygen will only warn about wrong or incomplete parameter +# documentation, but not about the absence of documentation. +# The default value is: NO. + +WARN_NO_PARAMDOC = NO + +# The WARN_FORMAT tag determines the format of the warning messages that doxygen +# can produce. The string should contain the $file, $line, and $text tags, which +# will be replaced by the file and line number from which the warning originated +# and the warning text. Optionally the format may contain $version, which will +# be replaced by the version of the file (if it could be obtained via +# FILE_VERSION_FILTER) +# The default value is: $file:$line: $text. + +WARN_FORMAT = "$file:$line: $text" + +# The WARN_LOGFILE tag can be used to specify a file to which warning and error +# messages should be written. If left blank the output is written to standard +# error (stderr). + +WARN_LOGFILE = + +#--------------------------------------------------------------------------- +# Configuration options related to the input files +#--------------------------------------------------------------------------- + +# The INPUT tag is used to specify the files and/or directories that contain +# documented source files. You may enter file names like myfile.cpp or +# directories like /usr/src/myproject. Separate the files or directories with +# spaces. +# Note: If this tag is empty the current directory is searched. + +INPUT = src/ doc/additionalDocuments/ + +# This tag can be used to specify the character encoding of the source files +# that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses +# libiconv (or the iconv built into libc) for the transcoding. See the libiconv +# documentation (see: http://www.gnu.org/software/libiconv) for the list of +# possible encodings. +# The default value is: UTF-8. + +INPUT_ENCODING = UTF-8 + +# If the value of the INPUT tag contains directories, you can use the +# FILE_PATTERNS tag to specify one or more wildcard patterns (like *.cpp and +# *.h) to filter out the source-files in the directories. If left blank the +# following patterns are tested:*.c, *.cc, *.cxx, *.cpp, *.c++, *.java, *.ii, +# *.ixx, *.ipp, *.i++, *.inl, *.idl, *.ddl, *.odl, *.h, *.hh, *.hxx, *.hpp, +# *.h++, *.cs, *.d, *.php, *.php4, *.php5, *.phtml, *.inc, *.m, *.markdown, +# *.md, *.mm, *.dox, *.py, *.f90, *.f, *.for, *.tcl, *.vhd, *.vhdl, *.ucf, +# *.qsf, *.as and *.js. + +FILE_PATTERNS = *.c \ + *.cc \ + *.cxx \ + *.cpp \ + *.c++ \ + *.dox \ + *.java \ + *.ii \ + *.ixx \ + *.ipp \ + *.i++ \ + *.inl \ + *.idl \ + *.ddl \ + *.odl \ + *.h \ + *.hh \ + *.hxx \ + *.hpp \ + *.h++ \ + *.cs \ + *.d \ + *.php \ + *.php4 \ + *.php5 \ + *.phtml \ + *.inc \ + *.m \ + *.markdown \ + *.md \ + *.mm \ + *.dox \ + *.py \ + *.f90 \ + *.f \ + *.for \ + *.tcl \ + *.vhd \ + *.vhdl \ + *.ucf \ + *.qsf \ + *.as \ + *.js + +# The RECURSIVE tag can be used to specify whether or not subdirectories should +# be searched for input files as well. +# The default value is: NO. + +RECURSIVE = YES + +# The EXCLUDE tag can be used to specify files and/or directories that should be +# excluded from the INPUT source files. This way you can easily exclude a +# subdirectory from a directory tree whose root is specified with the INPUT tag. +# +# Note that relative paths are relative to the directory from which doxygen is +# run. + +EXCLUDE = src/crave/backend src/crave/frontend src/crave/ir + +# The EXCLUDE_SYMLINKS tag can be used to select whether or not files or +# directories that are symbolic links (a Unix file system feature) are excluded +# from the input. +# The default value is: NO. + +EXCLUDE_SYMLINKS = NO + +# If the value of the INPUT tag contains directories, you can use the +# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude +# certain files from those directories. +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories for example use the pattern */test/* + +EXCLUDE_PATTERNS = + +# The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names +# (namespaces, classes, functions, etc.) that should be excluded from the +# output. The symbol name can be a fully qualified name, a word, or if the +# wildcard * is used, a substring. Examples: ANamespace, AClass, +# AClass::ANamespace, ANamespace::*Test +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories use the pattern */test/* + +EXCLUDE_SYMBOLS = crave::graph* CRAVE_EXPERIMENTAL_ENUM* + +# The EXAMPLE_PATH tag can be used to specify one or more files or directories +# that contain example code fragments that are included (see the \include +# command). + +EXAMPLE_PATH = examples/experimental_api + +# If the value of the EXAMPLE_PATH tag contains directories, you can use the +# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp and +# *.h) to filter out the source-files in the directories. If left blank all +# files are included. + +EXAMPLE_PATTERNS = *.cpp + +# If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be +# searched for input files to be used with the \include or \dontinclude commands +# irrespective of the value of the RECURSIVE tag. +# The default value is: NO. + +EXAMPLE_RECURSIVE = NO + +# The IMAGE_PATH tag can be used to specify one or more files or directories +# that contain images that are to be included in the documentation (see the +# \image command). + +IMAGE_PATH = + +# The INPUT_FILTER tag can be used to specify a program that doxygen should +# invoke to filter for each input file. Doxygen will invoke the filter program +# by executing (via popen()) the command: +# +# +# +# where is the value of the INPUT_FILTER tag, and is the +# name of an input file. Doxygen will then use the output that the filter +# program writes to standard output. If FILTER_PATTERNS is specified, this tag +# will be ignored. +# +# Note that the filter must not add or remove lines; it is applied before the +# code is scanned, but not when the output code is generated. If lines are added +# or removed, the anchors will not be placed correctly. + +INPUT_FILTER = + +# The FILTER_PATTERNS tag can be used to specify filters on a per file pattern +# basis. Doxygen will compare the file name with each pattern and apply the +# filter if there is a match. The filters are a list of the form: pattern=filter +# (like *.cpp=my_cpp_filter). See INPUT_FILTER for further information on how +# filters are used. If the FILTER_PATTERNS tag is empty or if none of the +# patterns match the file name, INPUT_FILTER is applied. + +FILTER_PATTERNS = + +# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using +# INPUT_FILTER ) will also be used to filter the input files that are used for +# producing the source files to browse (i.e. when SOURCE_BROWSER is set to YES). +# The default value is: NO. + +FILTER_SOURCE_FILES = NO + +# The FILTER_SOURCE_PATTERNS tag can be used to specify source filters per file +# pattern. A pattern will override the setting for FILTER_PATTERN (if any) and +# it is also possible to disable source filtering for a specific pattern using +# *.ext= (so without naming a filter). +# This tag requires that the tag FILTER_SOURCE_FILES is set to YES. + +FILTER_SOURCE_PATTERNS = + +# If the USE_MDFILE_AS_MAINPAGE tag refers to the name of a markdown file that +# is part of the input, its contents will be placed on the main page +# (index.html). This can be useful if you have a project on for instance GitHub +# and want to reuse the introduction page also for the doxygen output. + +USE_MDFILE_AS_MAINPAGE = + +#--------------------------------------------------------------------------- +# Configuration options related to source browsing +#--------------------------------------------------------------------------- + +# If the SOURCE_BROWSER tag is set to YES then a list of source files will be +# generated. Documented entities will be cross-referenced with these sources. +# +# Note: To get rid of all source code in the generated output, make sure that +# also VERBATIM_HEADERS is set to NO. +# The default value is: NO. + +SOURCE_BROWSER = NO + +# Setting the INLINE_SOURCES tag to YES will include the body of functions, +# classes and enums directly into the documentation. +# The default value is: NO. + +INLINE_SOURCES = NO + +# Setting the STRIP_CODE_COMMENTS tag to YES will instruct doxygen to hide any +# special comment blocks from generated source code fragments. Normal C, C++ and +# Fortran comments will always remain visible. +# The default value is: YES. + +STRIP_CODE_COMMENTS = YES + +# If the REFERENCED_BY_RELATION tag is set to YES then for each documented +# function all documented functions referencing it will be listed. +# The default value is: NO. + +REFERENCED_BY_RELATION = NO + +# If the REFERENCES_RELATION tag is set to YES then for each documented function +# all documented entities called/used by that function will be listed. +# The default value is: NO. + +REFERENCES_RELATION = NO + +# If the REFERENCES_LINK_SOURCE tag is set to YES and SOURCE_BROWSER tag is set +# to YES, then the hyperlinks from functions in REFERENCES_RELATION and +# REFERENCED_BY_RELATION lists will link to the source code. Otherwise they will +# link to the documentation. +# The default value is: YES. + +REFERENCES_LINK_SOURCE = YES + +# If SOURCE_TOOLTIPS is enabled (the default) then hovering a hyperlink in the +# source code will show a tooltip with additional information such as prototype, +# brief description and links to the definition and documentation. Since this +# will make the HTML file larger and loading of large files a bit slower, you +# can opt to disable this feature. +# The default value is: YES. +# This tag requires that the tag SOURCE_BROWSER is set to YES. + +SOURCE_TOOLTIPS = YES + +# If the USE_HTAGS tag is set to YES then the references to source code will +# point to the HTML generated by the htags(1) tool instead of doxygen built-in +# source browser. The htags tool is part of GNU's global source tagging system +# (see http://www.gnu.org/software/global/global.html). You will need version +# 4.8.6 or higher. +# +# To use it do the following: +# - Install the latest version of global +# - Enable SOURCE_BROWSER and USE_HTAGS in the config file +# - Make sure the INPUT points to the root of the source tree +# - Run doxygen as normal +# +# Doxygen will invoke htags (and that will in turn invoke gtags), so these +# tools must be available from the command line (i.e. in the search path). +# +# The result: instead of the source browser generated by doxygen, the links to +# source code will now point to the output of htags. +# The default value is: NO. +# This tag requires that the tag SOURCE_BROWSER is set to YES. + +USE_HTAGS = NO + +# If the VERBATIM_HEADERS tag is set the YES then doxygen will generate a +# verbatim copy of the header file for each class for which an include is +# specified. Set to NO to disable this. +# See also: Section \class. +# The default value is: YES. + +VERBATIM_HEADERS = YES + +# If the CLANG_ASSISTED_PARSING tag is set to YES, then doxygen will use the +# clang parser (see: http://clang.llvm.org/) for more accurate parsing at the +# cost of reduced performance. This can be particularly helpful with template +# rich C++ code for which doxygen's built-in parser lacks the necessary type +# information. +# Note: The availability of this option depends on whether or not doxygen was +# compiled with the --with-libclang option. +# The default value is: NO. + +CLANG_ASSISTED_PARSING = NO + +# If clang assisted parsing is enabled you can provide the compiler with command +# line options that you would normally use when invoking the compiler. Note that +# the include paths will already be set by doxygen for the files and directories +# specified with INPUT and INCLUDE_PATH. +# This tag requires that the tag CLANG_ASSISTED_PARSING is set to YES. + +CLANG_OPTIONS = + +#--------------------------------------------------------------------------- +# Configuration options related to the alphabetical class index +#--------------------------------------------------------------------------- + +# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index of all +# compounds will be generated. Enable this if the project contains a lot of +# classes, structs, unions or interfaces. +# The default value is: YES. + +ALPHABETICAL_INDEX = NO + +# The COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns in +# which the alphabetical index list will be split. +# Minimum value: 1, maximum value: 20, default value: 5. +# This tag requires that the tag ALPHABETICAL_INDEX is set to YES. + +COLS_IN_ALPHA_INDEX = 5 + +# In case all classes in a project start with a common prefix, all classes will +# be put under the same header in the alphabetical index. The IGNORE_PREFIX tag +# can be used to specify a prefix (or a list of prefixes) that should be ignored +# while generating the index headers. +# This tag requires that the tag ALPHABETICAL_INDEX is set to YES. + +IGNORE_PREFIX = + +#--------------------------------------------------------------------------- +# Configuration options related to the HTML output +#--------------------------------------------------------------------------- + +# If the GENERATE_HTML tag is set to YES doxygen will generate HTML output +# The default value is: YES. + +GENERATE_HTML = YES + +# The HTML_OUTPUT tag is used to specify where the HTML docs will be put. If a +# relative path is entered the value of OUTPUT_DIRECTORY will be put in front of +# it. +# The default directory is: html. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_OUTPUT = html + +# The HTML_FILE_EXTENSION tag can be used to specify the file extension for each +# generated HTML page (for example: .htm, .php, .asp). +# The default value is: .html. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_FILE_EXTENSION = .html + +# The HTML_HEADER tag can be used to specify a user-defined HTML header file for +# each generated HTML page. If the tag is left blank doxygen will generate a +# standard header. +# +# To get valid HTML the header file that includes any scripts and style sheets +# that doxygen needs, which is dependent on the configuration options used (e.g. +# the setting GENERATE_TREEVIEW). It is highly recommended to start with a +# default header using +# doxygen -w html new_header.html new_footer.html new_stylesheet.css +# YourConfigFile +# and then modify the file new_header.html. See also section "Doxygen usage" +# for information on how to generate the default header that doxygen normally +# uses. +# Note: The header is subject to change so you typically have to regenerate the +# default header when upgrading to a newer version of doxygen. For a description +# of the possible markers and block names see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_HEADER = + +# The HTML_FOOTER tag can be used to specify a user-defined HTML footer for each +# generated HTML page. If the tag is left blank doxygen will generate a standard +# footer. See HTML_HEADER for more information on how to generate a default +# footer and what special commands can be used inside the footer. See also +# section "Doxygen usage" for information on how to generate the default footer +# that doxygen normally uses. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_FOOTER = + +# The HTML_STYLESHEET tag can be used to specify a user-defined cascading style +# sheet that is used by each HTML page. It can be used to fine-tune the look of +# the HTML output. If left blank doxygen will generate a default style sheet. +# See also section "Doxygen usage" for information on how to generate the style +# sheet that doxygen normally uses. +# Note: It is recommended to use HTML_EXTRA_STYLESHEET instead of this tag, as +# it is more robust and this tag (HTML_STYLESHEET) will in the future become +# obsolete. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_STYLESHEET = + +# The HTML_EXTRA_STYLESHEET tag can be used to specify additional user-defined +# cascading style sheets that are included after the standard style sheets +# created by doxygen. Using this option one can overrule certain style aspects. +# This is preferred over using HTML_STYLESHEET since it does not replace the +# standard style sheet and is therefor more robust against future updates. +# Doxygen will copy the style sheet files to the output directory. +# Note: The order of the extra stylesheet files is of importance (e.g. the last +# stylesheet in the list overrules the setting of the previous ones in the +# list). For an example see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_STYLESHEET = + +# The HTML_EXTRA_FILES tag can be used to specify one or more extra images or +# other source files which should be copied to the HTML output directory. Note +# that these files will be copied to the base HTML output directory. Use the +# $relpath^ marker in the HTML_HEADER and/or HTML_FOOTER files to load these +# files. In the HTML_STYLESHEET file, use the file name only. Also note that the +# files will be copied as-is; there are no commands or markers available. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_FILES = + +# The HTML_COLORSTYLE_HUE tag controls the color of the HTML output. Doxygen +# will adjust the colors in the stylesheet and background images according to +# this color. Hue is specified as an angle on a colorwheel, see +# http://en.wikipedia.org/wiki/Hue for more information. For instance the value +# 0 represents red, 60 is yellow, 120 is green, 180 is cyan, 240 is blue, 300 +# purple, and 360 is red again. +# Minimum value: 0, maximum value: 359, default value: 220. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_HUE = 220 + +# The HTML_COLORSTYLE_SAT tag controls the purity (or saturation) of the colors +# in the HTML output. For a value of 0 the output will use grayscales only. A +# value of 255 will produce the most vivid colors. +# Minimum value: 0, maximum value: 255, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_SAT = 100 + +# The HTML_COLORSTYLE_GAMMA tag controls the gamma correction applied to the +# luminance component of the colors in the HTML output. Values below 100 +# gradually make the output lighter, whereas values above 100 make the output +# darker. The value divided by 100 is the actual gamma applied, so 80 represents +# a gamma of 0.8, The value 220 represents a gamma of 2.2, and 100 does not +# change the gamma. +# Minimum value: 40, maximum value: 240, default value: 80. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_GAMMA = 80 + +# If the HTML_TIMESTAMP tag is set to YES then the footer of each generated HTML +# page will contain the date and time when the page was generated. Setting this +# to NO can help when comparing the output of multiple runs. +# The default value is: YES. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_TIMESTAMP = YES + +# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML +# documentation will contain sections that can be hidden and shown after the +# page has loaded. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_DYNAMIC_SECTIONS = NO + +# With HTML_INDEX_NUM_ENTRIES one can control the preferred number of entries +# shown in the various tree structured indices initially; the user can expand +# and collapse entries dynamically later on. Doxygen will expand the tree to +# such a level that at most the specified number of entries are visible (unless +# a fully collapsed tree already exceeds this amount). So setting the number of +# entries 1 will produce a full collapsed tree by default. 0 is a special value +# representing an infinite number of entries and will result in a full expanded +# tree by default. +# Minimum value: 0, maximum value: 9999, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_INDEX_NUM_ENTRIES = 100 + +# If the GENERATE_DOCSET tag is set to YES, additional index files will be +# generated that can be used as input for Apple's Xcode 3 integrated development +# environment (see: http://developer.apple.com/tools/xcode/), introduced with +# OSX 10.5 (Leopard). To create a documentation set, doxygen will generate a +# Makefile in the HTML output directory. Running make will produce the docset in +# that directory and running make install will install the docset in +# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find it at +# startup. See http://developer.apple.com/tools/creatingdocsetswithdoxygen.html +# for more information. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_DOCSET = NO + +# This tag determines the name of the docset feed. A documentation feed provides +# an umbrella under which multiple documentation sets from a single provider +# (such as a company or product suite) can be grouped. +# The default value is: Doxygen generated docs. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_FEEDNAME = "Doxygen generated docs" + +# This tag specifies a string that should uniquely identify the documentation +# set bundle. This should be a reverse domain-name style string, e.g. +# com.mycompany.MyDocSet. Doxygen will append .docset to the name. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_BUNDLE_ID = org.doxygen.Project + +# The DOCSET_PUBLISHER_ID tag specifies a string that should uniquely identify +# the documentation publisher. This should be a reverse domain-name style +# string, e.g. com.mycompany.MyDocSet.documentation. +# The default value is: org.doxygen.Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_PUBLISHER_ID = org.doxygen.Publisher + +# The DOCSET_PUBLISHER_NAME tag identifies the documentation publisher. +# The default value is: Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_PUBLISHER_NAME = Publisher + +# If the GENERATE_HTMLHELP tag is set to YES then doxygen generates three +# additional HTML index files: index.hhp, index.hhc, and index.hhk. The +# index.hhp is a project file that can be read by Microsoft's HTML Help Workshop +# (see: http://www.microsoft.com/en-us/download/details.aspx?id=21138) on +# Windows. +# +# The HTML Help Workshop contains a compiler that can convert all HTML output +# generated by doxygen into a single compiled HTML file (.chm). Compiled HTML +# files are now used as the Windows 98 help format, and will replace the old +# Windows help format (.hlp) on all Windows platforms in the future. Compressed +# HTML files also contain an index, a table of contents, and you can search for +# words in the documentation. The HTML workshop also contains a viewer for +# compressed HTML files. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_HTMLHELP = NO + +# The CHM_FILE tag can be used to specify the file name of the resulting .chm +# file. You can add a path in front of the file if the result should not be +# written to the html output directory. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +CHM_FILE = + +# The HHC_LOCATION tag can be used to specify the location (absolute path +# including file name) of the HTML help compiler ( hhc.exe). If non-empty +# doxygen will try to run the HTML help compiler on the generated index.hhp. +# The file has to be specified with full path. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +HHC_LOCATION = + +# The GENERATE_CHI flag controls if a separate .chi index file is generated ( +# YES) or that it should be included in the master .chm file ( NO). +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +GENERATE_CHI = NO + +# The CHM_INDEX_ENCODING is used to encode HtmlHelp index ( hhk), content ( hhc) +# and project file content. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +CHM_INDEX_ENCODING = + +# The BINARY_TOC flag controls whether a binary table of contents is generated ( +# YES) or a normal table of contents ( NO) in the .chm file. Furthermore it +# enables the Previous and Next buttons. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +BINARY_TOC = NO + +# The TOC_EXPAND flag can be set to YES to add extra items for group members to +# the table of contents of the HTML help documentation and to the tree view. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +TOC_EXPAND = NO + +# If the GENERATE_QHP tag is set to YES and both QHP_NAMESPACE and +# QHP_VIRTUAL_FOLDER are set, an additional index file will be generated that +# can be used as input for Qt's qhelpgenerator to generate a Qt Compressed Help +# (.qch) of the generated HTML documentation. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_QHP = NO + +# If the QHG_LOCATION tag is specified, the QCH_FILE tag can be used to specify +# the file name of the resulting .qch file. The path specified is relative to +# the HTML output folder. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QCH_FILE = + +# The QHP_NAMESPACE tag specifies the namespace to use when generating Qt Help +# Project output. For more information please see Qt Help Project / Namespace +# (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#namespace). +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_NAMESPACE = org.doxygen.Project + +# The QHP_VIRTUAL_FOLDER tag specifies the namespace to use when generating Qt +# Help Project output. For more information please see Qt Help Project / Virtual +# Folders (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#virtual- +# folders). +# The default value is: doc. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_VIRTUAL_FOLDER = doc + +# If the QHP_CUST_FILTER_NAME tag is set, it specifies the name of a custom +# filter to add. For more information please see Qt Help Project / Custom +# Filters (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#custom- +# filters). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_CUST_FILTER_NAME = + +# The QHP_CUST_FILTER_ATTRS tag specifies the list of the attributes of the +# custom filter to add. For more information please see Qt Help Project / Custom +# Filters (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#custom- +# filters). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_CUST_FILTER_ATTRS = + +# The QHP_SECT_FILTER_ATTRS tag specifies the list of the attributes this +# project's filter section matches. Qt Help Project / Filter Attributes (see: +# http://qt-project.org/doc/qt-4.8/qthelpproject.html#filter-attributes). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_SECT_FILTER_ATTRS = + +# The QHG_LOCATION tag can be used to specify the location of Qt's +# qhelpgenerator. If non-empty doxygen will try to run qhelpgenerator on the +# generated .qhp file. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHG_LOCATION = + +# If the GENERATE_ECLIPSEHELP tag is set to YES, additional index files will be +# generated, together with the HTML files, they form an Eclipse help plugin. To +# install this plugin and make it available under the help contents menu in +# Eclipse, the contents of the directory containing the HTML and XML files needs +# to be copied into the plugins directory of eclipse. The name of the directory +# within the plugins directory should be the same as the ECLIPSE_DOC_ID value. +# After copying Eclipse needs to be restarted before the help appears. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_ECLIPSEHELP = NO + +# A unique identifier for the Eclipse help plugin. When installing the plugin +# the directory name containing the HTML and XML files should also have this +# name. Each documentation set should have its own identifier. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_ECLIPSEHELP is set to YES. + +ECLIPSE_DOC_ID = org.doxygen.Project + +# If you want full control over the layout of the generated HTML pages it might +# be necessary to disable the index and replace it with your own. The +# DISABLE_INDEX tag can be used to turn on/off the condensed index (tabs) at top +# of each HTML page. A value of NO enables the index and the value YES disables +# it. Since the tabs in the index contain the same information as the navigation +# tree, you can set this option to YES if you also set GENERATE_TREEVIEW to YES. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +DISABLE_INDEX = NO + +# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index +# structure should be generated to display hierarchical information. If the tag +# value is set to YES, a side panel will be generated containing a tree-like +# index structure (just like the one that is generated for HTML Help). For this +# to work a browser that supports JavaScript, DHTML, CSS and frames is required +# (i.e. any modern browser). Windows users are probably better off using the +# HTML help feature. Via custom stylesheets (see HTML_EXTRA_STYLESHEET) one can +# further fine-tune the look of the index. As an example, the default style +# sheet generated by doxygen has an example that shows how to put an image at +# the root of the tree instead of the PROJECT_NAME. Since the tree basically has +# the same information as the tab index, you could consider setting +# DISABLE_INDEX to YES when enabling this option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_TREEVIEW = NO + +# The ENUM_VALUES_PER_LINE tag can be used to set the number of enum values that +# doxygen will group on one line in the generated HTML documentation. +# +# Note that a value of 0 will completely suppress the enum values from appearing +# in the overview section. +# Minimum value: 0, maximum value: 20, default value: 4. +# This tag requires that the tag GENERATE_HTML is set to YES. + +ENUM_VALUES_PER_LINE = 4 + +# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be used +# to set the initial width (in pixels) of the frame in which the tree is shown. +# Minimum value: 0, maximum value: 1500, default value: 250. +# This tag requires that the tag GENERATE_HTML is set to YES. + +TREEVIEW_WIDTH = 250 + +# When the EXT_LINKS_IN_WINDOW option is set to YES doxygen will open links to +# external symbols imported via tag files in a separate window. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +EXT_LINKS_IN_WINDOW = NO + +# Use this tag to change the font size of LaTeX formulas included as images in +# the HTML documentation. When you change the font size after a successful +# doxygen run you need to manually remove any form_*.png images from the HTML +# output directory to force them to be regenerated. +# Minimum value: 8, maximum value: 50, default value: 10. +# This tag requires that the tag GENERATE_HTML is set to YES. + +FORMULA_FONTSIZE = 10 + +# Use the FORMULA_TRANPARENT tag to determine whether or not the images +# generated for formulas are transparent PNGs. Transparent PNGs are not +# supported properly for IE 6.0, but are supported on all modern browsers. +# +# Note that when changing this option you need to delete any form_*.png files in +# the HTML output directory before the changes have effect. +# The default value is: YES. +# This tag requires that the tag GENERATE_HTML is set to YES. + +FORMULA_TRANSPARENT = YES + +# Enable the USE_MATHJAX option to render LaTeX formulas using MathJax (see +# http://www.mathjax.org) which uses client side Javascript for the rendering +# instead of using prerendered bitmaps. Use this if you do not have LaTeX +# installed or if you want to formulas look prettier in the HTML output. When +# enabled you may also need to install MathJax separately and configure the path +# to it using the MATHJAX_RELPATH option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +USE_MATHJAX = NO + +# When MathJax is enabled you can set the default output format to be used for +# the MathJax output. See the MathJax site (see: +# http://docs.mathjax.org/en/latest/output.html) for more details. +# Possible values are: HTML-CSS (which is slower, but has the best +# compatibility), NativeMML (i.e. MathML) and SVG. +# The default value is: HTML-CSS. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_FORMAT = HTML-CSS + +# When MathJax is enabled you need to specify the location relative to the HTML +# output directory using the MATHJAX_RELPATH option. The destination directory +# should contain the MathJax.js script. For instance, if the mathjax directory +# is located at the same level as the HTML output directory, then +# MATHJAX_RELPATH should be ../mathjax. The default value points to the MathJax +# Content Delivery Network so you can quickly see the result without installing +# MathJax. However, it is strongly recommended to install a local copy of +# MathJax from http://www.mathjax.org before deployment. +# The default value is: http://cdn.mathjax.org/mathjax/latest. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_RELPATH = http://cdn.mathjax.org/mathjax/latest + +# The MATHJAX_EXTENSIONS tag can be used to specify one or more MathJax +# extension names that should be enabled during MathJax rendering. For example +# MATHJAX_EXTENSIONS = TeX/AMSmath TeX/AMSsymbols +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_EXTENSIONS = + +# The MATHJAX_CODEFILE tag can be used to specify a file with javascript pieces +# of code that will be used on startup of the MathJax code. See the MathJax site +# (see: http://docs.mathjax.org/en/latest/output.html) for more details. For an +# example see the documentation. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_CODEFILE = + +# When the SEARCHENGINE tag is enabled doxygen will generate a search box for +# the HTML output. The underlying search engine uses javascript and DHTML and +# should work on any modern browser. Note that when using HTML help +# (GENERATE_HTMLHELP), Qt help (GENERATE_QHP), or docsets (GENERATE_DOCSET) +# there is already a search function so this one should typically be disabled. +# For large projects the javascript based search engine can be slow, then +# enabling SERVER_BASED_SEARCH may provide a better solution. It is possible to +# search using the keyboard; to jump to the search box use + S +# (what the is depends on the OS and browser, but it is typically +# , /