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

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)
set(Boost_ADDITIONAL_VERSIONS "1.50.0")
find_package(Boost COMPONENTS iostreams thread system python filesystem)

if(NOT ${Boost_FOUND})
  message(FATAL_ERROR "Boost could not be found.")
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_SMT2       "try to use SMTLIB2 solver" on)
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_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_USE_ExprSolver "try to use expression solver" on)

option(metaSMT_DOC_Doxygen    "try to build doxygen documentation" off)
option(metaSMT_ENABLE_TESTS   "build tests (recommended)" on)
option(metaSMT_ENABLE_BINDINGS "build bindings" on)
option(metaSMT_ENABLE_TOOLBOX "build toolbox projects" 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(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_STP)
  find_package(STP QUIET)
  find_package(cryptominisat4 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()

find_package(OMP QUIET)
set_package_info(OMP "optional, required by some backends")
## later versions of GMP link against libomp
if(NOT OMP_FOUND)
  find_library(OMP_LIBRARIES gomp PATHS ${OMP_DIR})
else()
  set(OMP_LIBRARIES "")
endif()

if(Z3_FOUND)
  if( GMPXX_LIBRARIES )
    set(Z3_LIBRARIES ${Z3_LIBRARIES} ${GMPXX_LIBRARIES})
  else ()
    set(Z3_LIBRARIES ${Z3_LIBRARIES} gmpxx)
  endif()

  if( GMP_LIBRARIES )
    set(Z3_LIBRARIES ${Z3_LIBRARIES} ${GMP_LIBRARIES})
  else ()
    set(Z3_LIBRARIES ${Z3_LIBRARIES} gmp)
  endif()

  if( OMP_LIBRARIES )
    set(Z3_LIBRARIES ${Z3_LIBRARIES} ${OMP_LIBRARIES})
  else ()
    set(Z3_LIBRARIES ${Z3_LIBRARIES} gomp)
  endif()

  set(Z3_LIBRARIES ${Z3_LIBRARIES} rt pthread)

  include(CheckCXXSourceRuns)

  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;
  z3::solver s(c);
  s.check();
  return 0;
}"
  Z3_WORKS)

  if( NOT Z3_WORKS )
    message(WARNING "Disabling Z3. A version of Z3 >= 4.0 is required.")
    set( Z3_FOUND 0)
  endif()
endif()

if(CVC4_FOUND)
  if( GMPXX_LIBRARIES )
    set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${GMPXX_LIBRARIES})
  else ()<commit_msg>Update CMakeLists.txt<commit_after>PROJECT(metaSMT)
cmake_minimum_required(VERSION 2.8.9)

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)
set(Boost_ADDITIONAL_VERSIONS "1.50.0")
find_package(Boost COMPONENTS iostreams thread system python filesystem)

if(NOT ${Boost_FOUND})
  message(FATAL_ERROR "Boost could not be found.")
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_SMT2       "try to use SMTLIB2 solver" on)
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_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_USE_ExprSolver "try to use expression solver" on)

option(metaSMT_DOC_Doxygen    "try to build doxygen documentation" off)
option(metaSMT_ENABLE_TESTS   "build tests (recommended)" on)
option(metaSMT_ENABLE_BINDINGS "build bindings" on)
option(metaSMT_ENABLE_TOOLBOX "build toolbox projects" 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(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_STP)
  find_package(STP QUIET)
  find_package(cryptominisat4 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()

find_package(OMP QUIET)
set_package_info(OMP "optional, required by some backends")
## later versions of GMP link against libomp
if(NOT OMP_FOUND)
  find_library(OMP_LIBRARIES gomp PATHS ${OMP_DIR})
else()
  set(OMP_LIBRARIES "")
endif()

if(Z3_FOUND)
  if( GMPXX_LIBRARIES )
    set(Z3_LIBRARIES ${Z3_LIBRARIES} ${GMPXX_LIBRARIES})
  else ()
    set(Z3_LIBRARIES ${Z3_LIBRARIES} gmpxx)
  endif()

  if( GMP_LIBRARIES )
    set(Z3_LIBRARIES ${Z3_LIBRARIES} ${GMP_LIBRARIES})
  else ()
    set(Z3_LIBRARIES ${Z3_LIBRARIES} gmp)
  endif()

  if( OMP_LIBRARIES )
    set(Z3_LIBRARIES ${Z3_LIBRARIES} ${OMP_LIBRARIES})
  else ()
    set(Z3_LIBRARIES ${Z3_LIBRARIES} gomp)
  endif()

  find_package(Threads QUIET)

  set(Z3_LIBRARIES ${Z3_LIBRARIES} rt ${CMAKE_THREAD_LIBS_INIT})

  include(CheckCXXSourceRuns)

  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;
  z3::solver s(c);
  s.check();
  return 0;
}"
  Z3_WORKS)

  if( NOT Z3_WORKS )
    message(WARNING "Disabling Z3. A version of Z3 >= 4.0 is required.")
    set( Z3_FOUND 0)
  endif()
endif()

if(CVC4_FOUND)
  if( GMPXX_LIBRARIES )
    set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${GMPXX_LIBRARIES})
  else ()
{'fraction_non_alphanumeric': 0.09766022380467955, 'fraction_numerical': 0.012022565430500324, 'mean_word_length': 5.792713567839196, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 7, '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': '4083154', 'n_tokens_mistral': 4569, 'n_tokens_neox': 4323, 'n_words': 973}