diff --git a/.gitignore b/.gitignore index f63dae3a..b45a8355 100644 --- a/.gitignore +++ b/.gitignore @@ -10,3 +10,5 @@ tissat *.gcov gmon.out *~ +*build* +.idea diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 00000000..5521ae84 --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,90 @@ +cmake_minimum_required(VERSION 3.19) +project(kissat VERSION 2.0.1 LANGUAGES C) + +set(CMAKE_C_STANDARD 90) +set(CMAKE_C_VISIBILITY_PRESET hidden) +set(CMAKE_VISIBILITY_INLINES_HIDDEN YES) + +option(BUILD_SHARED_LIBS "Build using shared libraries" OFF) +if (BUILD_SHARED_LIBS) + set(LIBRARY_TYPE_FLAG "SHARED") +else () + set(LIBRARY_TYPE_FLAG "STATIC") +endif () + +# control where the static and shared libraries are built so that on windows +# we don't need to tinker with the path to run the executable +set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${PROJECT_BINARY_DIR}") +set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${PROJECT_BINARY_DIR}") +set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${PROJECT_BINARY_DIR}") + +add_library("${PROJECT_NAME}_compiler_flags" INTERFACE) +target_compile_features("${PROJECT_NAME}_compiler_flags" INTERFACE "c_std_90") + +set(gcc_like "$") +set(msvc "$") +# -g -fsanitize=address -fno-omit-frame-pointer +target_compile_options( + "${PROJECT_NAME}_compiler_flags" + INTERFACE + "$<${gcc_like}:$>" + "$<${msvc}:$>" +) +if (CMAKE_C_COMPILER_ID STREQUAL "Clang" OR CMAKE_C_COMPILER_ID STREQUAL "AppleClang") + set(CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -fno-omit-frame-pointer -fsanitize=address") + set(CMAKE_LINKER_FLAGS_DEBUG "${CMAKE_LINKER_FLAGS_DEBUG} -fno-omit-frame-pointer -fsanitize=address") +endif() + +# configure a header file to pass the version number only +configure_file( + "${CMAKE_CURRENT_SOURCE_DIR}/cmake/config.h.in" + "${PROJECT_NAME}Config.h" +) + +add_subdirectory("src") + +option(BUILD_TESTS "Build tests" OFF) +if (BUILD_TESTS) + add_subdirectory("test") +endif (BUILD_TESTS) + +install( + FILES "${PROJECT_BINARY_DIR}/${PROJECT_NAME}Config.h" + DESTINATION "include" +) + +include(InstallRequiredSystemLibraries) +set(CPACK_BUNDLE_NAME "${PROJECT_NAME}") +set(CPACK_PACKAGE_VENDOR "Armin Biere") +set(CPACK_PACKAGE_DESCRIPTION "Kissat is a "keep it simple and clean bare metal SAT solver" written in C.") +set(CPACK_PACKAGE_DESCRIPTION_SUMMARY "Kissat is a "keep it simple and clean bare metal SAT solver" written in C.") +if (APPLE) + set(CPACK_BUNDLE_PLIST "${CMAKE_CURRENT_SOURCE_DIR}/cmake/Info.plist") + set(CPACK_BUNDLE_ICON "${CMAKE_CURRENT_SOURCE_DIR}/cmake/Info.plist") + set(CPACK_PACKAGE_ICON "${CMAKE_CURRENT_SOURCE_DIR}/cmake/CustomVolumeIcon.icns") +endif() +set(CPACK_RESOURCE_FILE_LICENSE "${CMAKE_CURRENT_SOURCE_DIR}/License") +set(CPACK_PACKAGE_VERSION_MAJOR "${${PROJECT_NAME}_VERSION_MAJOR}") +set(CPACK_PACKAGE_VERSION_MINOR "${${PROJECT_NAME}_VERSION_MINOR}") +set(CPACK_RESOURCE_FILE_README "${CMAKE_CURRENT_SOURCE_DIR}/cmake/README.txt") +set(CPACK_RESOURCE_FILE_WELCOME "${CMAKE_CURRENT_SOURCE_DIR}/cmake/Welcome.txt") +set(CPACK_PACKAGE_CONTACT "https://github.com/attractivechaos/${PROJECT_NAME}") + +include(CPack) +include(CMakePackageConfigHelpers) + +# generate the config file that is includes the exports +configure_package_config_file( + "${CMAKE_CURRENT_SOURCE_DIR}/cmake/Config.cmake.in" + "${CMAKE_CURRENT_BINARY_DIR}/${PROJECT_NAME}Config.cmake" + INSTALL_DESTINATION "lib/cmake/example" + NO_SET_AND_CHECK_MACRO + NO_CHECK_REQUIRED_COMPONENTS_MACRO +) + +# generate the version file for the config file +write_basic_package_version_file( + "${CMAKE_CURRENT_BINARY_DIR}/${PROJECT_NAME}ConfigVersion.cmake" + VERSION "${${PROJECT_NAME}_VERSION_MAJOR}.${${PROJECT_NAME}_VERSION_MINOR}" + COMPATIBILITY AnyNewerVersion +) diff --git a/cmake/BundleIcon.icns b/cmake/BundleIcon.icns new file mode 100644 index 00000000..8808dd62 Binary files /dev/null and b/cmake/BundleIcon.icns differ diff --git a/cmake/CTestConfig.cmake b/cmake/CTestConfig.cmake new file mode 100644 index 00000000..5e588189 --- /dev/null +++ b/cmake/CTestConfig.cmake @@ -0,0 +1,7 @@ +set(CTEST_PROJECT_NAME "kissat") +set(CTEST_NIGHTLY_START_TIME "00:00:00 EST") + +set(CTEST_DROP_METHOD "http") +set(CTEST_DROP_SITE "my.cdash.org") +set(CTEST_DROP_LOCATION "/submit.php?project=kissat") +set(CTEST_DROP_SITE_CDASH TRUE) diff --git a/cmake/Config.cmake.in b/cmake/Config.cmake.in new file mode 100644 index 00000000..d1828298 --- /dev/null +++ b/cmake/Config.cmake.in @@ -0,0 +1,4 @@ + +@PACKAGE_INIT@ + +include ( "${CMAKE_CURRENT_LIST_DIR}/libkissatTargets.cmake" ) diff --git a/cmake/CustomVolumeIcon.icns b/cmake/CustomVolumeIcon.icns new file mode 100644 index 00000000..3862a519 Binary files /dev/null and b/cmake/CustomVolumeIcon.icns differ diff --git a/cmake/Info.plist b/cmake/Info.plist new file mode 100644 index 00000000..e5a7d004 --- /dev/null +++ b/cmake/Info.plist @@ -0,0 +1,14 @@ + + + + + CFBundleExecutable + BundleGeneratorTest + CFBundleIconFile + BundleGeneratorTest.icns + CFBundleInfoDictionaryVersion + 6.0 + CFBundlePackageType + APPL + + diff --git a/cmake/MultiCPackConfig.cmake b/cmake/MultiCPackConfig.cmake new file mode 100644 index 00000000..38c0ec2e --- /dev/null +++ b/cmake/MultiCPackConfig.cmake @@ -0,0 +1,6 @@ +include("release/CPackConfig.cmake") + +set(CPACK_INSTALL_CMAKE_PROJECTS + "debug;Kann;ALL;/" + "release;Kann;ALL;/" +) diff --git a/cmake/README.txt b/cmake/README.txt new file mode 100644 index 00000000..261a13f9 --- /dev/null +++ b/cmake/README.txt @@ -0,0 +1 @@ +Kissat is a "keep it simple and clean bare metal SAT solver" written in C. diff --git a/cmake/Welcome.txt b/cmake/Welcome.txt new file mode 100644 index 00000000..261a13f9 --- /dev/null +++ b/cmake/Welcome.txt @@ -0,0 +1 @@ +Kissat is a "keep it simple and clean bare metal SAT solver" written in C. diff --git a/cmake/config.h.in b/cmake/config.h.in new file mode 100644 index 00000000..d804a5bf --- /dev/null +++ b/cmake/config.h.in @@ -0,0 +1,9 @@ +#ifndef kissat_CONFIG_H +#define kissat_CONFIG_H + +#define kissat_VERSION_MAJOR @kissat_VERSION_MAJOR@ +#define kissat_VERSION_MINOR @kissat_VERSION_MINOR@ +#define kissat_VERSION_PATCH @kissat_VERSION_PATCH@ +#define kissat_VERSION "@kissat_VERSION@" + +#endif /* kissat_CONFIG_H */ diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt new file mode 100644 index 00000000..39a387c8 --- /dev/null +++ b/src/CMakeLists.txt @@ -0,0 +1,268 @@ +set(LIBRARY_NAME "libkissat") +set(EXEC_NAME "kissat") + +set(Header_Files + "allocate.h" + "analyze.h" + "ands.h" + "arena.h" + "array.h" + "assign.h" + "attribute.h" + "autarky.h" + "averages.h" + "backbone.h" + "backtrack.h" + "backward.h" + "bits.h" + "bump.h" + "cache.h" + "check.h" + "clause.h" + "clueue.h" + "collect.h" + "colors.h" + "compact.h" + "config.h" + "cover.h" + "decide.h" + "deduce.h" + "definition.h" + "dense.h" + "dominate.h" + "eliminate.h" + "endianness.h" + "equivalences.h" + "error.h" + "extend.h" + "failed.h" + "fastassign.h" + "file.h" + "flags.h" + "format.h" + "forward.h" + "frames.h" + "gates.h" + "handle.h" + "heap.h" + "ifthenelse.h" + "import.h" + "inline.h" + "inlineassign.h" + "inlineframes.h" + "inlineheap.h" + "inlinequeue.h" + "inlinereap.h" + "inlinescore.h" + "inlinevector.h" + "internal.h" + "kissat.h" + "learn.h" + "limits.h" + "literal.h" + "logging.h" + "minimize.h" + "mode.h" + "nonces.h" + "options.h" + "parse.h" + "phases.h" + "print.h" + "probe.h" + "profile.h" + "promote.h" + "proof.h" + "propdense.h" + "prophyper.h" + "proplit.h" + "proprobe.h" + "propsearch.h" + "queue.h" + "random.h" + "rank.h" + "reap.h" + "reduce.h" + "reference.h" + "reluctant.h" + "rephase.h" + "report.h" + "require.h" + "resize.h" + "resolve.h" + "resources.h" + "restart.h" + "search.h" + "shrink.h" + "smooth.h" + "sort.h" + "stack.h" + "statistics.h" + "strengthen.h" + "substitute.h" + "sweep.h" + "terminate.h" + "ternary.h" + "trail.h" + "transitive.h" + "utilities.h" + "value.h" + "vector.h" + "vivify.h" + "walk.h" + "watch.h" + "weaken.h" + "witness.h" + "xors.h" +) +source_group("Header Files" FILES "${Header_Files}") + +set(Source_Files + "allocate.c" + "analyze.c" + "ands.c" + "arena.c" + "assign.c" + "autarky.c" + "averages.c" + "backbone.c" + "backtrack.c" + "backward.c" + "bits.c" + "build.c" + "bump.c" + "cache.c" + "check.c" + "clause.c" + "clueue.c" + "collect.c" + "colors.c" + "compact.c" + "config.c" + "decide.c" + "deduce.c" + "definition.c" + "dense.c" + "dominate.c" + "dump.c" + "eliminate.c" + "equivalences.c" + "error.c" + "extend.c" + "failed.c" + "file.c" + "flags.c" + "format.c" + "forward.c" + "gates.c" + "handle.c" + "heap.c" + "ifthenelse.c" + "import.c" + "internal.c" + "learn.c" + "limits.c" + "logging.c" + "minimize.c" + "mode.c" + "nonces.c" + "options.c" + "parse.c" + "phases.c" + "print.c" + "probe.c" + "profile.c" + "promote.c" + "proof.c" + "propdense.c" + "prophyper.c" + "proprobe.c" + "propsearch.c" + "queue.c" + "reap.c" + "reduce.c" + "reluctant.c" + "rephase.c" + "report.c" + "resize.c" + "resolve.c" + "resources.c" + "restart.c" + "search.c" + "shrink.c" + "smooth.c" + "sort.c" + "stack.c" + "statistics.c" + "strengthen.c" + "substitute.c" + "sweep.c" + "terminate.c" + "ternary.c" + "trail.c" + "transitive.c" + "utilities.c" + "vector.c" + "vivify.c" + "walk.c" + "watch.c" + "weaken.c" + "witness.c" + "xors.c" +) +source_group("Source Files" FILES "${Source_Files}") + +add_library("${LIBRARY_NAME}" "${Header_Files}" "${Source_Files}") +target_include_directories( + "${LIBRARY_NAME}" + PUBLIC + "$" + "$" +) +set_target_properties( + "${LIBRARY_NAME}" + PROPERTIES + LINKER_LANGUAGE + C +) + +# install rules +set(installable_libs "${LIBRARY_NAME}" "${PROJECT_NAME}_compiler_flags") +install(FILES "${Header_Files}" DESTINATION "include") + +set(exec_targets "application" "kitten" "main") +foreach (target ${exec_targets}) + set(EXEC_NAME "${PROJECT_NAME}_${target}") + + set(Source_Files "${target}.c") + source_group("${target} Source Files" FILES "${Source_Files}") + + if (target STREQUAL "main") + add_executable("${EXEC_NAME}" "${Source_Files}") + else () + set(Header_Files "${target}.h") + source_group("${target} Header Files" FILES "${Header_Files}") + add_executable("${EXEC_NAME}" "${Header_Files}" "${Source_Files}") + install(FILES "${Header_Files}" DESTINATION "include") + endif () + + target_include_directories( + "${EXEC_NAME}" + PRIVATE + "$" + "$" + ) + set_target_properties( + "${EXEC_NAME}" + PROPERTIES + LINKER_LANGUAGE + C + ) + list(APPEND installable_libs "${EXEC_NAME}") +endforeach () + +if (TARGET "${DEPENDANT_LIBRARY}") + list(APPEND installable_libs "${DEPENDANT_LIBRARY}") +endif () +install(TARGETS ${installable_libs} + DESTINATION "bin" + EXPORT "${EXEC_NAME}Targets")