<commit_before>PROJECT(metaSMT)
cmake_minimum_required(VERSION 2.8.9)

option(metaSMT_REQUIRE_CXX11 "make C++11 a requirement" on)

if ( NOT metaSMT_REQUIRE_CXX11 AND WIN32 )
  message(FATAL_ERROR "Windows build requires CXX11")
endif()

include(CheckCXXCompilerFlag)

if (metaSMT_REQUIRE_CXX11)
  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()
endif()

include(CheckIncludeFileCXX)
include(FeatureSummary)

include(CTest)

set(CMAKE_MODULE_PATH ${CMAKE_SOURCE_DIR}/cmake/Modules )

set(Boost_NO_BOOST_CMAKE true)
set(Boost_NO_SYSTEM_PATHS true)
find_package(Boost REQUIRED)

# From v1.57.0 Boost.Any does not require RTTI
if (${Boost_VERSION} VERSION_LESS 105700)
  message( STATUS "metaSMT requires RTTI" )
  set(metaSMT_REQUIRE_RTTI true)
else()
  message( STATUS "metaSMT does not require RTTI" )
  set(metaSMT_REQUIRE_RTTI false)
endif()

set_package_info(Boost "Portable C++ libraries")
include_directories(${Boost_INCLUDE_DIRS})

list(INSERT CMAKE_PREFIX_PATH 0 "${CMAKE_SOURCE_DIR}/cmake")

# Set the default version number, but try to calculate
# a proper version from git.
SET(metaSMT_VERSION 4)
include(cmake/get_git_version.cmake)

include(cmake/build_type.cmake)
include(cmake/default_compliler_flags.cmake)
include(cmake/config_file.cmake)

###  
# Options to force disable certain solvers. 
# set all solvers to "on" with good support and experimental or
# work in progress to "off"
###
option(metaSMT_USE_SWORD      "try to use SWORD solver" on)
option(metaSMT_USE_Boolector  "try to use Boolector solver" on)
option(metaSMT_USE_Z3         "try to use Z3 solver" on)
option(metaSMT_USE_STP        "try to use STP solver" on)
option(metaSMT_USE_CVC4        "try to use CVC4 solver" on)
option(metaSMT_USE_YICES2     "try to use Yices2 solver" on)
option(metaSMT_USE_CUDD       "try to use CUDD BDD package" on )
option(metaSMT_USE_MiniSat    "try to use minisat SAT solver" on)
option(metaSMT_USE_picosat    "try to use picosat SAT solver" on)
option(metaSMT_USE_lingeling  "try to use lingeling SAT solver" on)
option(metaSMT_USE_Aiger      "try to use aiger" on)
option(metaSMT_USE_CW         "try to use clause writers" on)

option(metaSMT_DOC_Doxygen    "try to build doxygen documentation" off)
option(metaSMT_ENABLE_TESTS   "build tests (recommended)" on)

set(metaSMT_CONFIG_DIR "share/metaSMT" CACHE PATH 
  "where to install CMake and Make Config files")

if ( NOT TIMEOUT )
  set(TIMEOUT 5 CACHE STRING "The timeout for tests")
endif()

if ( WIN32 )
  message(STATUS "Windows build: disable all solvers except z3!" )
  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_CUDD 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()

if(metaSMT_USE_SWORD AND NOT APPLE)
  find_package(SWORD QUIET)
else()
  set(SWORD_FOUND 0)
endif()
set_package_info(SWORD "solver for SMT QF_BV")

if(metaSMT_USE_Boolector)
  find_package(Boolector QUIET)
  list(APPEND Boolector_INCLUDE_DIR ${boolector_INCLUDE_DIRS})
  list(APPEND Boolector_LIBRARIES ${boolector_LIBRARIES})
else()
  set(Boolector_FOUND 0)
endif()
set_package_info(Boolector "solver for SMT QF_BV and Arrays")

if (metaSMT_USE_Z3)
  find_package(Z3 QUIET)
else()
  set(Z3_FOUND 0)
endif()
set_package_info(Z3 "solver for various SMT theories")

if (metaSMT_USE_YICES2)
  find_package(YICES2 QUIET)
else()
  set(YICES2_FOUND 0)
endif()
set_package_info(YICES2 "solver for various SMT theories")

if(metaSMT_USE_STP)
  find_package(STP QUIET)
else()
  set(STP_FOUND 0)
endif()
set_package_info(STP "solver for SMT QF_BV and Arrays")

if(metaSMT_USE_CVC4)
  find_package(CVC4 QUIET)
else()
  set(CVC4_FOUND 0)
endif()
set_package_info(CVC4 "solver for various SMT theories")

if (metaSMT_USE_CUDD)
  find_package(CUDD QUIET)
else ()
  set(CUDD_FOUND 0)
endif ()
set_package_info(CUDD "binary decision diagrams")

if (metaSMT_USE_Aiger)
  find_package(Aiger QUIET) 
  list(APPEND Aiger_LIBRARIES Aiger)
else ()
  set(Aiger_FOUND 0)
endif()
set_package_info(Aiger "And Inverter Graph libraries")

if (metaSMT_USE_MiniSat)
  find_package(MiniSat QUIET)
else ()
  set(MiniSat_FOUND 0)
endif ()
set_package_info(MiniSat "SAT solver MiniSAT")

if (metaSMT_USE_picosat )
  find_package (PicoSAT QUIET)
endif()
set_package_info(PicoSat "SAT solver PicoSat")

if( metaSMT_USE_lingeling )
  find_package( Lingeling QUIET)
endif()
set_package_info(Lingeling "SAT solver lingeling")

find_package(GMP QUIET)
set_package_info(GMP "optional, required by some backends")
if(NOT GMP_FOUND)
  find_library(GMP_LIBRARIES gmp PATHS ${GMP_DIR})
  find_library(GMPXX_LIBRARIES gmpxx PATHS ${GMP_DIR})
else()
  set(GMP_LIBRARIES "")
  set(GMPXX_LIBRARIES "")
endif()

if(Z3_FOUND)
  find_package(OpenMP)
  if (OPENMP_FOUND)
    set(Z3_CXXFLAGS ${OpenMP_CXX_FLAGS})
    if (UNIX OR MSYS)
      list(APPEND Z3_LIBRARIES ${OpenMP_CXX_FLAGS})
    endif()
    message(STATUS "Use Z3 with OpenMP")
  else()
    message(STATUS "Use Z3 without OpenMP")
  endif()

  if (UNIX)
    find_package(Threads QUIET)
    find_library(RT_LIB rt)
    set(Z3_LIBRARIES ${Z3_LIBRARIES} ${RT_LIB} ${CMAKE_THREAD_LIBS_INIT})
  endif()

  include(CheckCXXSourceRuns)

  set(CMAKE_REQUIRED_FLAGS ${Z3_CXXFLAGS})
  set(CMAKE_REQUIRED_INCLUDES ${Z3_INCLUDE_DIR})
  set(CMAKE_REQUIRED_LIBRARIES ${Z3_LIBRARIES})

  check_CXX_source_runs("#include <z3++.h>
int main(int argc, const char *argv[]) {
  z3::context c;<commit_msg>Boolector 3 needs to be linked with pthread<commit_after>PROJECT(metaSMT)
cmake_minimum_required(VERSION 2.8.9)

option(metaSMT_REQUIRE_CXX11 "make C++11 a requirement" on)

if ( NOT metaSMT_REQUIRE_CXX11 AND WIN32 )
  message(FATAL_ERROR "Windows build requires CXX11")
endif()

include(CheckCXXCompilerFlag)

if (metaSMT_REQUIRE_CXX11)
  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()
endif()

include(CheckIncludeFileCXX)
include(FeatureSummary)

include(CTest)

set(CMAKE_MODULE_PATH ${CMAKE_SOURCE_DIR}/cmake/Modules )

set(Boost_NO_BOOST_CMAKE true)
set(Boost_NO_SYSTEM_PATHS true)
find_package(Boost REQUIRED)

# From v1.57.0 Boost.Any does not require RTTI
if (${Boost_VERSION} VERSION_LESS 105700)
  message( STATUS "metaSMT requires RTTI" )
  set(metaSMT_REQUIRE_RTTI true)
else()
  message( STATUS "metaSMT does not require RTTI" )
  set(metaSMT_REQUIRE_RTTI false)
endif()

set_package_info(Boost "Portable C++ libraries")
include_directories(${Boost_INCLUDE_DIRS})

list(INSERT CMAKE_PREFIX_PATH 0 "${CMAKE_SOURCE_DIR}/cmake")

# Set the default version number, but try to calculate
# a proper version from git.
SET(metaSMT_VERSION 4)
include(cmake/get_git_version.cmake)

include(cmake/build_type.cmake)
include(cmake/default_compliler_flags.cmake)
include(cmake/config_file.cmake)

###  
# Options to force disable certain solvers. 
# set all solvers to "on" with good support and experimental or
# work in progress to "off"
###
option(metaSMT_USE_SWORD      "try to use SWORD solver" on)
option(metaSMT_USE_Boolector  "try to use Boolector solver" on)
option(metaSMT_USE_Z3         "try to use Z3 solver" on)
option(metaSMT_USE_STP        "try to use STP solver" on)
option(metaSMT_USE_CVC4        "try to use CVC4 solver" on)
option(metaSMT_USE_YICES2     "try to use Yices2 solver" on)
option(metaSMT_USE_CUDD       "try to use CUDD BDD package" on )
option(metaSMT_USE_MiniSat    "try to use minisat SAT solver" on)
option(metaSMT_USE_picosat    "try to use picosat SAT solver" on)
option(metaSMT_USE_lingeling  "try to use lingeling SAT solver" on)
option(metaSMT_USE_Aiger      "try to use aiger" on)
option(metaSMT_USE_CW         "try to use clause writers" on)

option(metaSMT_DOC_Doxygen    "try to build doxygen documentation" off)
option(metaSMT_ENABLE_TESTS   "build tests (recommended)" on)

set(metaSMT_CONFIG_DIR "share/metaSMT" CACHE PATH 
  "where to install CMake and Make Config files")

if ( NOT TIMEOUT )
  set(TIMEOUT 5 CACHE STRING "The timeout for tests")
endif()

if ( WIN32 )
  message(STATUS "Windows build: disable all solvers except z3!" )
  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_CUDD 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()

if(metaSMT_USE_SWORD AND NOT APPLE)
  find_package(SWORD QUIET)
else()
  set(SWORD_FOUND 0)
endif()
set_package_info(SWORD "solver for SMT QF_BV")

if(metaSMT_USE_Boolector)
  find_package(Boolector QUIET)
  list(APPEND Boolector_INCLUDE_DIR ${boolector_INCLUDE_DIRS})
  list(APPEND Boolector_LIBRARIES ${boolector_LIBRARIES})
else()
  set(Boolector_FOUND 0)
endif()
set_package_info(Boolector "solver for SMT QF_BV and Arrays")

if (metaSMT_USE_Z3)
  find_package(Z3 QUIET)
else()
  set(Z3_FOUND 0)
endif()
set_package_info(Z3 "solver for various SMT theories")

if (metaSMT_USE_YICES2)
  find_package(YICES2 QUIET)
else()
  set(YICES2_FOUND 0)
endif()
set_package_info(YICES2 "solver for various SMT theories")

if(metaSMT_USE_STP)
  find_package(STP QUIET)
else()
  set(STP_FOUND 0)
endif()
set_package_info(STP "solver for SMT QF_BV and Arrays")

if(metaSMT_USE_CVC4)
  find_package(CVC4 QUIET)
else()
  set(CVC4_FOUND 0)
endif()
set_package_info(CVC4 "solver for various SMT theories")

if (metaSMT_USE_CUDD)
  find_package(CUDD QUIET)
else ()
  set(CUDD_FOUND 0)
endif ()
set_package_info(CUDD "binary decision diagrams")

if (metaSMT_USE_Aiger)
  find_package(Aiger QUIET) 
  list(APPEND Aiger_LIBRARIES Aiger)
else ()
  set(Aiger_FOUND 0)
endif()
set_package_info(Aiger "And Inverter Graph libraries")

if (metaSMT_USE_MiniSat)
  find_package(MiniSat QUIET)
else ()
  set(MiniSat_FOUND 0)
endif ()
set_package_info(MiniSat "SAT solver MiniSAT")

if (metaSMT_USE_picosat )
  find_package (PicoSAT QUIET)
endif()
set_package_info(PicoSat "SAT solver PicoSat")

if( metaSMT_USE_lingeling )
  find_package( Lingeling QUIET)
endif()
set_package_info(Lingeling "SAT solver lingeling")

find_package(GMP QUIET)
set_package_info(GMP "optional, required by some backends")
if(NOT GMP_FOUND)
  find_library(GMP_LIBRARIES gmp PATHS ${GMP_DIR})
  find_library(GMPXX_LIBRARIES gmpxx PATHS ${GMP_DIR})
else()
  set(GMP_LIBRARIES "")
  set(GMPXX_LIBRARIES "")
endif()

if(Boolector_FOUND AND (Boolector_VERSION VERSION_GREATER 2))
  find_package(Threads)
  set(Boolector_LIBRARIES ${Boolector_LIBRARIES} ${CMAKE_THREAD_LIBS_INIT})
endif()

if(Z3_FOUND)
  find_package(OpenMP)
  if (OPENMP_FOUND)
    set(Z3_CXXFLAGS ${OpenMP_CXX_FLAGS})
    if (UNIX OR MSYS)
      list(APPEND Z3_LIBRARIES ${OpenMP_CXX_FLAGS})
    endif()
    message(STATUS "Use Z3 with OpenMP")
  else()
    message(STATUS "Use Z3 without OpenMP")
  endif()

  if (UNIX)
    find_package(Threads QUIET)
    find_library(RT_LIB rt)
    set(Z3_LIBRARIES ${Z3_LIBRARIES} ${RT_LIB} ${CMAKE_THREAD_LIBS_INIT})
  endif()

  include(CheckCXXSourceRuns)

  set(CMAKE_REQUIRED_FLAGS ${Z3_CXXFLAGS})
  set(CMAKE_REQUIRED_INCLUDES ${Z3_INCLUDE_DIR})
  set(CMAKE_REQUIRED_LIBRARIES ${Z3_LIBRARIES})

  check_CXX_source_runs("#include <z3++.h>
int main(int argc, const char *argv[]) {
  z3::context c;
{'fraction_non_alphanumeric': 0.09350869749681799, 'fraction_numerical': 0.014085702163767502, 'mean_word_length': 5.888369374634716, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1945490', 'n_tokens_mistral': 4921, 'n_tokens_neox': 4722, 'n_words': 1050}