cmake_minimum_required(VERSION 3.18)
project(cadical VERSION %version% LANGUAGES C CXX)

# Collect all library sources: everything in src/ except the two standalone
# application entry points (cadical.cpp = solver binary, mobical.cpp = tester).
file(GLOB cadical_sources CONFIGURE_DEPENDS
    "${CMAKE_CURRENT_SOURCE_DIR}/src/*.c"
    "${CMAKE_CURRENT_SOURCE_DIR}/src/*.cpp"
    "${CMAKE_CURRENT_SOURCE_DIR}/contrib/*.cpp")
list(FILTER cadical_sources EXCLUDE REGEX "/(cadical|mobical)\\.cpp$")

add_library(cadical SHARED ${cadical_sources})
set_target_properties(cadical PROPERTIES POSITION_INDEPENDENT_CODE ON VERSION 0.0.0 SOVERSION 0)

# Public headers are in src/: cadical.hpp plus internal headers that
# downstream projects (cadiback, CryptoMiniSat) need (resources.hpp, etc.).
target_include_directories(cadical PUBLIC
    $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/src>
    $<INSTALL_INTERFACE:include/cadical>)

target_compile_features(cadical PUBLIC cxx_std_17)

# Fixed feature set: no API contracts, no tracing.
# NBUILD skips the build.hpp generation step (version.cpp handles this).
target_compile_definitions(cadical PRIVATE
    NCONTRACTS
    NTRACING
    NBUILD
    NCLOSEFROM
    NUNLOCKED
    $<$<NOT:$<CONFIG:Debug>>:NDEBUG>)

add_executable(cadical_bin src/cadical.cpp)
set_target_properties(cadical_bin PROPERTIES OUTPUT_NAME "cadical")
target_link_libraries(cadical_bin PUBLIC cadical)
target_compile_definitions(cadical_bin PRIVATE
    NCONTRACTS
    NTRACING
    NBUILD
    NCLOSEFROM
    NUNLOCKED
    $<$<NOT:$<CONFIG:Debug>>:NDEBUG>)

add_executable(mobical src/mobical.cpp)
target_link_libraries(mobical PUBLIC cadical)
target_compile_definitions(mobical PRIVATE
    NCONTRACTS
    NTRACING
    NBUILD
    NCLOSEFROM
    NUNLOCKED
    $<$<NOT:$<CONFIG:Debug>>:NDEBUG>)

# ---- Install / cmake package export ----
include(GNUInstallDirs)

install(TARGETS cadical EXPORT cadicalTargets
    LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR})
install(TARGETS cadical_bin mobical RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR})

# Export for build-tree usage (lets dependents point CMAKE_PREFIX_PATH at build/)
# Use export(TARGETS ...) rather than export(EXPORT ...) so the file is written
# immediately at configure time (export(EXPORT) defers to the generate phase).
export(TARGETS cadical
    FILE "${CMAKE_CURRENT_BINARY_DIR}/cadicalTargets.cmake")
# Install all public headers flat into include/cadical/
install(DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/src/"
    DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}/cadical"
    FILES_MATCHING PATTERN "*.hpp" PATTERN "*.h")
install(EXPORT cadicalTargets
    FILE cadicalTargets.cmake
    DESTINATION "${CMAKE_INSTALL_LIBDIR}/cmake/cadical")
# Minimal Config file — just imports the targets
file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/cadicalConfig.cmake"
    "include(\"\${CMAKE_CURRENT_LIST_DIR}/cadicalTargets.cmake\")\n")
install(FILES "${CMAKE_CURRENT_BINARY_DIR}/cadicalConfig.cmake"
    DESTINATION "${CMAKE_INSTALL_LIBDIR}/cmake/cadical")

# ---- Tests ----
include(CTest)
add_test(NAME api COMMAND ${CMAKE_SOURCE_DIR}/test/api/run.sh)
add_test(NAME cnf COMMAND ${CMAKE_SOURCE_DIR}/test/cnf/run.sh)
add_test(NAME icnf COMMAND ${CMAKE_SOURCE_DIR}/test/icnf/run.sh)
add_test(NAME trace COMMAND ${CMAKE_SOURCE_DIR}/test/trace/run.sh)
add_test(NAME usage COMMAND ${CMAKE_SOURCE_DIR}/test/usage/run.sh)
add_test(NAME contrib COMMAND ${CMAKE_SOURCE_DIR}/test/contrib/run.sh)
# Skip the mobical tests
# They randomly fail due to exceeding time or memory limits
