release v5.5.2

.gitignore

@@ -12,7 +12,6 @@ ReleaseScript
 *.db
 *.vcxproj.user
 x64
-libgringo/generated
 .nfs*
 examples/clingo/pydoc/clingo.ast.html
 examples/clingo/pydoc/clingo.html
@@ -25,4 +24,3 @@ _skbuild/
 dist
 *.egg-info/
 MANIFEST
-libgringo/gen/

clasp/.gitignore

@@ -0,0 +1,4 @@
+*.swp
+build*
+.vscode*
+CMakeLists.txt.user

clasp/.travis.yml

@@ -0,0 +1,63 @@
+sudo: false
+language: cpp
+matrix:
+  include:
+    - os: linux
+      compiler: gcc
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+            - george-edison55-precise-backports
+          packages:
+            - g++-4.9
+            - cmake
+            - cmake-data
+      env:
+        - COMPILER='g++-4.9'
+    - os: linux
+      compiler: gcc
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+            - george-edison55-precise-backports
+          packages:
+            - g++-5
+            - cmake
+            - cmake-data
+      env:
+        - COMPILER='g++-5'
+    - os: linux
+      compiler: gcc
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+            - george-edison55-precise-backports
+          packages:
+            - g++-8
+            - cmake
+            - cmake-data
+      env:
+        - COMPILER='g++-8'
+    - os: osx
+      osx_image: xcode8
+      env:
+        - COMPILER='clang++'
+
+install:
+  - export CMAKE=cmake  
+  - export CXX=$COMPILER
+  - $CMAKE --version
+  - $CXX --version
+script:
+  - mkdir $CXX-mt && cd $CXX-mt
+  - $CMAKE -DCMAKE_CXX_COMPILER=$CXX -DCLASP_BUILD_TESTS=ON -DCMAKE_BUILD_TYPE=Debug -DCMAKE_CXX_FLAGS="-Wall -Wextra" ../
+  - make -j3 && make test CTEST_OUTPUT_ON_FAILURE=1
+  - cd ../
+  - mkdir $CXX-st && cd $CXX-st
+  - $CMAKE -DCMAKE_CXX_COMPILER=$CXX -DCLASP_BUILD_TESTS=ON -DCLASP_BUILD_WITH_THREADS=OFF -DCMAKE_CXX_FLAGS="-Wall -Wextra" ../
+  - make -j3 && make test CTEST_OUTPUT_ON_FAILURE=1
+  - cd ../
+

clasp/CMakeLists.txt

@@ -0,0 +1,157 @@
+cmake_minimum_required(VERSION 3.1)
+project(CLASP VERSION 3.3.8 LANGUAGES CXX)
+# Enable folders in IDEs like Visual Studio
+set_property(GLOBAL PROPERTY USE_FOLDERS ON)
+if (POLICY CMP0063)
+	cmake_policy(SET CMP0063 NEW)
+endif()
+if (NOT CMAKE_BUILD_TYPE AND NOT CMAKE_CONFIGURATION_TYPES)
+	message(STATUS "No build type selected - using 'Release'")
+	set(CMAKE_BUILD_TYPE "Release")
+endif()
+list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_SOURCE_DIR}/cmake")
+
+include(GNUInstallDirs)
+
+# Configuration options
+option(CLASP_BUILD_APP              "whether or not to build the clasp application" ON)
+option(CLASP_BUILD_STATIC           "whether or not to link statically (if supported)" OFF)
+option(CLASP_BUILD_TESTS            "whether or not to build clasp unit tests" OFF)
+option(CLASP_BUILD_EXAMPLES         "whether or not to build examples" OFF)
+option(CLASP_BUILD_WITH_THREADS     "whether or not to build clasp with threading support (requires C++11)" ON)
+option(CLASP_INSTALL_LIB            "whether or not to install libclasp" OFF)
+option(CLASP_INSTALL_VERSIONED      "whether to use a versioned install layout" OFF)
+option(CLASP_USE_LOCAL_LIB_POTASSCO "whether to use the libpotassco submodule" ON)
+
+if (NOT MSVC)
+	if (NOT CMAKE_ARCHIVE_OUTPUT_DIRECTORY)
+		set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+	endif()
+	if (NOT CMAKE_LIBRARY_OUTPUT_DIRECTORY)
+		set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+	endif()
+	if (NOT CMAKE_RUNTIME_OUTPUT_DIRECTORY)
+		set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+	endif()
+else()
+	set(VC_RELEASE_LINK_OPTIONS /LTCG)
+	SET(CMAKE_EXE_LINKER_FLAGS_RELEASE    "${CMAKE_EXE_LINKER_FLAGS_RELEASE}    ${VC_RELEASE_LINK_OPTIONS}")
+	SET(CMAKE_MODULE_LINKER_FLAGS_RELEASE "${CMAKE_MODULE_LINKER_FLAGS_RELEASE} ${VC_RELEASE_LINK_OPTIONS}")
+	SET(CMAKE_SHARED_LINKER_FLAGS_RELEASE "${CMAKE_SHARED_LINKER_FLAGS_RELEASE} ${VC_RELEASE_LINK_OPTIONS}")
+	SET(CMAKE_STATIC_LINKER_FLAGS_RELEASE "${CMAKE_STATIC_LINKER_FLAGS_RELEASE} ${VC_RELEASE_LINK_OPTIONS}")
+	if (CLASP_BUILD_STATIC)
+		# force static runtime
+		string(REGEX REPLACE "/MD" "/MT" CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE}")
+	endif()
+endif()
+if (CLASP_INSTALL_VERSIONED)
+	set(clasp_include_dest "clasp-${CLASP_VERSION}")
+	set(clasp_library_dest "clasp-${CLASP_VERSION}")
+	set(cmake_dest         "clasp-${CLASP_VERSION}/cmake")
+else()
+	set(clasp_include_dest ".")
+	set(clasp_library_dest ".")
+	set(cmake_dest         "cmake/Clasp")
+endif()
+
+if (CLASP_INSTALL_LIB AND NOT CMAKE_INSTALL_LIBDIR)
+	message(STATUS "LIBDIR no set - using lib")
+	set(CMAKE_INSTALL_LIBDIR lib)
+endif()
+
+
+# C++11 is required for building with threads
+if (CLASP_BUILD_WITH_THREADS)
+	set(CMAKE_CXX_STANDARD 11)
+	set(CMAKE_CXX_STANDARD_REQUIRED ON)
+	set(CMAKE_CXX_EXTENSIONS ON)
+	# some versions of findThreads will fail if C is not enabled
+	enable_language(C)
+	find_package(Threads REQUIRED)
+
+	# Add libatomic if necessary
+	if (CMAKE_CXX_COMPILER_ID MATCHES "Clang" AND CMAKE_USE_PTHREADS_INIT)
+		include (CheckCXXSourceCompiles)
+		set (OLD_CMAKE_REQUIRED_FLAGS ${CMAKE_REQUIRED_FLAGS})
+		set (OLD_CMAKE_REQUIRED_LIBRARIES ${CMAKE_REQUIRED_LIBRARIES})
+		list(APPEND CMAKE_REQUIRED_FLAGS "-std=c++11")
+		list(APPEND CMAKE_REQUIRED_LIBRARIES Threads::Threads)
+		check_cxx_source_compiles("
+#include <atomic>
+#include <cstdint>
+std::atomic<uint64_t> x (0);
+int main() {
+	uint64_t i = x.load(std::memory_order_relaxed);
+	return 0;
+}
+" CLASP_HAS_WORKING_LIBATOMIC)
+		set (CMAKE_REQUIRED_FLAGS ${OLD_CMAKE_REQUIRED_FLAGS})
+		set (CMAKE_REQUIRED_LIBRARIES ${OLD_CMAKE_REQUIRED_LIBRARIES})
+		if (NOT CLASP_HAS_WORKING_LIBATOMIC)
+			check_library_exists(atomic __atomic_fetch_add_4 "" CLASP_HAS_LIBATOMIC)
+			if (CLASP_HAS_LIBATOMIC)
+				set_property(TARGET Threads::Threads APPEND PROPERTY INTERFACE_LINK_LIBRARIES "atomic")
+			endif()
+		endif()
+	endif()
+endif()
+
+# Check for or build external dependency
+if (NOT CLASP_USE_LOCAL_LIB_POTASSCO)
+	find_package(Potassco 1.0 REQUIRED CONFIG)
+else()
+	if (NOT EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/libpotassco/CMakeLists.txt)
+		message(STATUS "Potassco is not installed - fetching submodule")
+		execute_process(COMMAND git submodule update --init WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} OUTPUT_QUIET)
+	else()
+		message(STATUS "Potassco is not installed - using local copy")
+	endif()
+	set(LIB_POTASSCO_BUILD_APP       ${CLASP_BUILD_APP}   CACHE BOOL "")
+	set(LIB_POTASSCO_INSTALL_LIB     ${CLASP_INSTALL_LIB} CACHE BOOL "")
+	add_subdirectory(libpotassco)
+endif()
+
+# Build clasp library
+add_subdirectory(src)
+
+# Build optional targets
+if(CLASP_BUILD_TESTS)
+	enable_testing()
+	add_subdirectory(tests)
+endif()
+# optional doc target
+find_package(Doxygen)
+if(DOXYGEN_FOUND)
+	set(doxyfile "${CMAKE_CURRENT_SOURCE_DIR}/doc/api/clasp.doxy")
+	add_custom_target(doc_clasp
+		COMMAND ${DOXYGEN_EXECUTABLE} ${doxyfile}
+		WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/doc/api"
+		COMMENT "Generating documentation..."
+		VERBATIM)
+	set_target_properties(doc_clasp PROPERTIES FOLDER doc)
+endif()
+
+if(CLASP_BUILD_APP)
+	add_subdirectory(app)
+endif()
+
+if(CLASP_BUILD_EXAMPLES)
+	add_subdirectory(examples)
+endif()
+
+# Export
+if (CLASP_INSTALL_LIB)
+	include(CMakePackageConfigHelpers)
+	configure_package_config_file(
+		${PROJECT_SOURCE_DIR}/cmake/ClaspConfig.cmake.in
+		${CMAKE_CURRENT_BINARY_DIR}/ClaspConfig.cmake
+		INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/${cmake_dest})
+	write_basic_package_version_file(
+		${CMAKE_CURRENT_BINARY_DIR}/ClaspConfigVersion.cmake
+		COMPATIBILITY SameMajorVersion)
+	install(FILES
+		${CMAKE_CURRENT_BINARY_DIR}/ClaspConfig.cmake
+		${CMAKE_CURRENT_BINARY_DIR}/ClaspConfigVersion.cmake
+		DESTINATION ${CMAKE_INSTALL_LIBDIR}/${cmake_dest})
+	install(EXPORT ClaspTargets DESTINATION "${CMAKE_INSTALL_LIBDIR}/${cmake_dest}")
+endif()

clasp/LICENSE

@@ -0,0 +1,22 @@
+The MIT License
+
+Copyright (c) 2015-2017 Benjamin Kaufmann
+
+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.
+

clasp/README.md

@@ -0,0 +1,128 @@
+# clasp
+
+clasp is an answer set solver for (extended) normal and disjunctive logic programs.
+It is part of the [Potassco](https://potassco.org) project for *Answer Set Programming* (ASP).
+The primary algorithm of clasp relies on conflict-driven nogood learning,
+a technique that proved very successful for satisfiability checking (SAT).
+clasp has been genuinely developed for answer set solving but can 
+also be applied as a (Max-)SAT or PB solver or as a C++ library in another program.
+It provides different reasoning modes and other advanced features including:
+
+ - [Enumeration][enum] and [Optimization][opt] of ([Projected][proj]) Solutions,
+ - Cautious and Brave Reasoning,
+ - [Advanced Disjunctive Solving][claspD2],
+ - [Parallel (multithreaded) solving][claspmt],
+ - [Domain heuristic][hclasp] modifications,
+ - [Unsatisfiable-core based optimization][unclasp],
+ - [ASP/SAT/PB modulo acyclicity][acyc],
+ - Different input formats including [smodels][smodels], [aspif][aspif], [dimacs][dimacs] and [opb][opb].
+
+Detailed information (including a User's manual), source code,
+and pre-compiled binaries are available at: http://potassco.org/
+
+## LICENSE
+  clasp is distributed under the MIT License.
+
+  See LICENSE for details regarding the license.
+
+## PACKAGE CONTENTS
+    LICENSE        - The MIT License
+    CHANGES        - Major changes between versions
+    README.md      - This file
+    CMakeLists.txt - Configuration file for building clasp with CMake
+    cmake/         - Module directory for additional CMake scripts
+    app/           - Source code directory of the command-line interface
+    clasp/         - Header directory of the clasp library
+    src/           - Source code directory of the clasp library
+    tests/         - Unit tests of the clasp library
+    examples/      - Examples using the clasp library
+    libpotassco/   - Directory of the potassco library
+    tools/         - Some additional files
+
+
+## BUILDING & INSTALLING
+  The preferred way to build clasp is to use [CMake][cmake] version 3.1 or later
+  together with a C++ compiler that supports C++11.
+
+  The following options can be used to configure the build:
+
+    CLASP_BUILD_APP         : whether or not to build the clasp application
+    CLASP_BUILD_TESTS       : whether or not to build clasp unit tests
+    CLASP_BUILD_EXAMPLES    : whether or not to build examples
+    CLASP_BUILD_WITH_THREADS: whether or not to build clasp with threading support
+                              (requires C++11)
+
+  For example, to build clasp in release mode in directory `<dir>`:
+
+    cmake -H. -B<dir>
+    cmake --build <dir>
+
+  To install clasp afterwards:
+
+    cmake --build <dir> --target install
+
+  To set the installation prefix, run
+  `cmake` with option `-DCMAKE_INSTALL_PREFIX=<path>`.
+
+  Finally, you can always skip installation and simply copy the
+  clasp executable to a directory of your choice.
+
+## DOCUMENTATION
+  A User's Guide is available from http://potassco.org/
+
+  Source code documentation can be generated with [Doxygen][doxygen].
+  Either explicitly:
+
+    cd libclasp/doc/api
+    doxygen clasp.doxy
+
+  or via the `doc_clasp` target when using cmake.
+
+## USAGE
+  clasp reads problem instances either from stdin, e.g
+
+    cat problem | clasp
+
+  or from a given file, e.g
+
+    clasp problem
+
+  Type
+
+    clasp --help
+
+  to get a basic overview of options supported by clasp or
+
+    clasp --help={2,3}
+
+  for a more detailed list.
+
+  In addition to printing status information, clasp also
+  provides information about the computation via its exit status.
+  The exit status is either one or a combination of:
+
+    0  : search was not started because of some option (e.g. '--help')
+    1  : search was interrupted
+    10 : problem was found to be satisfiable
+    20 : problem was proved to be unsatisfiable
+
+  Exit codes 1 and 11 indicate that search was interrupted before
+  the final result was computed. Exit code 30 indicates that either
+  all models were found (enumeration), optimality was proved (optimization),
+  or all consequences were computed (cautious/brave reasoning).
+  Finally, exit codes greater than 32 are used to signal errors.
+
+[enum]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/lpnmr/GebserKNS07
+[proj]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/cpaior/GebserKS09
+[opt]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:journals/tplp/GebserKS11
+[claspmt]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:journals/tplp/GebserKS12
+[claspD2]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/ijcai/GebserKS13
+[hclasp]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/aaai/GebserKROSW13
+[unclasp]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/iclp/AndresKMS12
+[acyc]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:journals/fuin/BomansonGJKS16
+[aspif]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/iclp/GebserKKOSW16x
+[smodels]: http://www.tcs.hut.fi/Software/smodels/lparse.ps
+[dimacs]: http://www.satcompetition.org/2009/format-benchmarks2009.html
+[opb]: https://www.cril.univ-artois.fr/PB09/solver_req.html
+[doxygen]: https://www.stack.nl/~dimitri/doxygen/
+[cmake]: https://cmake.org/