From 3100f4a73399148285c3c99acc7fb80e18094abc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Mon, 21 Nov 2016 17:51:14 +0100 Subject: [PATCH] Initial commit. --- .gitattributes | 4 +++ .gitmodules | 6 ++++ .travis.yml | 47 +++++++++++++++++++++++++++++++ CMakeLists.txt | 33 ++++++++++++++++++++++ LICENSE.md | 21 ++++++++++++++ README.md | 31 +++++++++++++++++++++ app/CMakeLists.txt | 13 +++++++++ app/main.cpp | 58 +++++++++++++++++++++++++++++++++++++++ lib/catch | 1 + lib/clingo | 1 + src/CMakeLists.txt | 26 ++++++++++++++++++ tests/CMakeLists.txt | 17 ++++++++++++ tests/TestTranslation.cpp | 2 ++ tests/main.cpp | 2 ++ 14 files changed, 262 insertions(+) create mode 100644 .gitattributes create mode 100644 .gitmodules create mode 100644 .travis.yml create mode 100644 CMakeLists.txt create mode 100644 LICENSE.md create mode 100644 README.md create mode 100644 app/CMakeLists.txt create mode 100644 app/main.cpp create mode 160000 lib/catch create mode 160000 lib/clingo create mode 100644 src/CMakeLists.txt create mode 100644 tests/CMakeLists.txt create mode 100644 tests/TestTranslation.cpp create mode 100644 tests/main.cpp diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..cac16e3 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,4 @@ +.gitignore export-ignore +.gitattributes export-ignore +.gitmodules export-ignore +.travis.yml export-ignore diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..c09da0b --- /dev/null +++ b/.gitmodules @@ -0,0 +1,6 @@ +[submodule "lib/clingo"] + path = lib/clingo + url = https://github.com/potassco/clingo +[submodule "lib/catch"] + path = lib/catch + url = https://github.com/philsquared/Catch diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 0000000..5c48372 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,47 @@ +# Use container-based distribution +sudo: false +language: c++ +addons: + apt: + sources: &default_sources + - ubuntu-toolchain-r-test + - boost-latest + packages: &default_packages + - libboost-program-options1.55-dev + - libboost-iostreams1.55-dev + - libboost-system1.55-dev + - libboost-filesystem1.55-dev + - re2c +matrix: + include: + - env: COMPILER_NAME=g++ _CXX=g++-5 _CC=gcc-5 + os: linux + language: cpp + addons: + apt: + sources: + - *default_sources + packages: + - *default_packages + - g++-5 + - env: COMPILER_NAME=g++ _CXX=g++-6 _CC=gcc-6 + os: linux + language: cpp + addons: + apt: + sources: + - *default_sources + packages: + - *default_packages + - g++-6 +script: + - if [[ "${TRAVIS_OS_NAME}" == "linux" ]]; then + CMAKE_URL="http://www.cmake.org/files/v3.7/cmake-3.7.0-Linux-x86_64.tar.gz"; + mkdir cmake-bin && wget --quiet --no-check-certificate -O - ${CMAKE_URL} | tar --strip-components=1 -xz -C cmake-bin; + export PATH=${PWD}/cmake-bin/bin:${PATH}; + fi + - git submodule update --init --recursive + - mkdir -p build/debug + - cd build/debug + - cmake ../.. -DCMAKE_BUILD_TYPE=Debug -DCMAKE_CXX_COMPILER=$_CXX -DCMAKE_C_COMPILER=$_CC -DANTHEM_BUILD_TESTS=ON + - make -j3 anthem-app && make -j3 run-tests diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 0000000..6432d1a --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,33 @@ +cmake_minimum_required(VERSION 2.6) +project(anthem CXX) + +option(ANTHEM_BUILD_TESTS "Build unit tests" OFF) + +find_package(Boost 1.55.0 COMPONENTS program_options iostreams system filesystem REQUIRED) + +set(CMAKE_CXX_FLAGS "-Wall -Wpedantic") +set(CMAKE_CXX_FLAGS_DEBUG "-g") + +set(CMAKE_CXX_STANDARD 14) +set(CMAKE_CXX_STANDARD_REQUIRED ON) +set(CMAKE_CXX_EXTENSIONS OFF) + +set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) +set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) +set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) + +set(CLASP_BUILD_APP OFF CACHE BOOL "whether or not to build the clasp application") +set(CLASP_BUILD_TEST OFF CACHE BOOL "whether or not to build clasp unit tests (requires CppUnit)") +set(CLINGO_BUILD_SHARED OFF CACHE BOOL "build clingo library shared") +set(CLINGO_BUILD_WITH_LUA OFF CACHE BOOL "enable lua support") +set(CLINGO_BUILD_WITH_PYTHON OFF CACHE BOOL "enable python support") +set(LIB_POTASSCO_BUILD_APP OFF CACHE BOOL "whether or not to build lpconvert tool") +set(LIB_POTASSCO_BUILD_TESTS OFF CACHE BOOL "whether or not to build tests") + +add_subdirectory(lib/clingo) +add_subdirectory(src) +add_subdirectory(app) + +if(ANTHEM_BUILD_TESTS) + add_subdirectory(tests) +endif() diff --git a/LICENSE.md b/LICENSE.md new file mode 100644 index 0000000..cf01b76 --- /dev/null +++ b/LICENSE.md @@ -0,0 +1,21 @@ +# The MIT License (MIT) + +Copyright © 2016 Patrick Lühne + +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. diff --git a/README.md b/README.md new file mode 100644 index 0000000..3a57c18 --- /dev/null +++ b/README.md @@ -0,0 +1,31 @@ +# anthem [![GitHub Release](https://img.shields.io/github/release/potassco/anthem.svg?maxAge=3600)](https://github.com/potassco/anthem/releases) [![Build Status](https://img.shields.io/travis/potassco/anthem/develop.svg?maxAge=3600&label=build (master))](https://travis-ci.org/potassco/anthem?branch=master) [![Build Status](https://img.shields.io/travis/potassco/anthem/develop.svg?maxAge=3600&label=build (develop))](https://travis-ci.org/potassco/anthem?branch=develop) + +> Translate answer set programs to first-order theorem prover language + +## Overview + +`anthem` translates ASP programs (in the input language of [`clingo`](https://github.com/potassco/clingo)) to the language of first-order theorem provers such as [Prover9](https://www.cs.unm.edu/~mccune/mace4/). + +## Usage + +```bash +$ anthem [files] [options] +``` + +## Building + +`anthem` is built with `cmake` and requires a C++14 compiler (preferrably GCC ≥ 6.1 or clang ≥ 3.8). + +```bash +$ git clone https://github.com/potassco/anthem.git +$ git submodule update --init --recursive +$ cd anthem +$ mkdir -p build/release +$ cd build/release +$ cmake ../.. -DCMAKE_BUILD_TYPE=Release +$ make +``` + +## Contributors + +* [Patrick Lühne](https://www.luehne.de) diff --git a/app/CMakeLists.txt b/app/CMakeLists.txt new file mode 100644 index 0000000..6729d25 --- /dev/null +++ b/app/CMakeLists.txt @@ -0,0 +1,13 @@ +set(target anthem-app) + +file(GLOB core_sources "*.cpp") +file(GLOB core_headers "*.h") + +set(sources + ${core_sources} + ${core_headers} +) + +add_executable(${target} ${sources}) +target_link_libraries(${target} anthem) +set_target_properties(${target} PROPERTIES OUTPUT_NAME anthem) diff --git a/app/main.cpp b/app/main.cpp new file mode 100644 index 0000000..1b55f0e --- /dev/null +++ b/app/main.cpp @@ -0,0 +1,58 @@ +#include + +#include + +int main(int argc, char **argv) +{ + namespace po = boost::program_options; + + po::options_description description("Allowed options"); + description.add_options() + ("help,h", "display this help message") + ("version,v", "Display version information.") + ("input,i", po::value>(), "Specify the PDDL or SAS input file."); + + po::positional_options_description positionalOptionsDescription; + positionalOptionsDescription.add("input", -1); + + po::variables_map variablesMap; + + const auto printHelp = + [&]() + { + std::cout << "Usage: anthem [files] [options]" << std::endl; + std::cout << "Translate ASP programs to the language of first-order theorem provers." << std::endl << std::endl; + + std::cout << description; + }; + + try + { + po::store(po::command_line_parser(argc, argv) + .options(description) + .positional(positionalOptionsDescription) + .run(), + variablesMap); + po::notify(variablesMap); + } + catch (const po::error &e) + { + std::cerr << e.what() << std::endl; + printHelp(); + return EXIT_FAILURE; + } + + if (variablesMap.count("help")) + { + printHelp(); + return EXIT_SUCCESS; + } + + if (variablesMap.count("version")) + { + std::cout << "anthem version 0.1.0-git" << std::endl; + return EXIT_SUCCESS; + } + + return EXIT_SUCCESS; +} diff --git a/lib/catch b/lib/catch new file mode 160000 index 0000000..e27c4ee --- /dev/null +++ b/lib/catch @@ -0,0 +1 @@ +Subproject commit e27c4ee04282f60aefcc9b1062a74f92cf6c1a2b diff --git a/lib/clingo b/lib/clingo new file mode 160000 index 0000000..3a704a6 --- /dev/null +++ b/lib/clingo @@ -0,0 +1 @@ +Subproject commit 3a704a64f848eb6207591690cd9a2193ae9f9fb8 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt new file mode 100644 index 0000000..4ac8a63 --- /dev/null +++ b/src/CMakeLists.txt @@ -0,0 +1,26 @@ +set(target anthem) + +file(GLOB core_sources "anthem/*.cpp") +file(GLOB core_headers "../include/anthem/*.h") + +set(sources + ${core_sources} + ${core_headers} +) + +set(includes + ${PROJECT_SOURCE_DIR}/include + ${Boost_INCLUDE_DIRS} +) + +set(libraries + ${Boost_LIBRARIES} + libclasp + libclingo + libgringo + pthread +) + +add_library(${target} ${sources}) +target_include_directories(${target} PUBLIC ${includes}) +target_link_libraries(${target} ${libraries}) diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt new file mode 100644 index 0000000..c156220 --- /dev/null +++ b/tests/CMakeLists.txt @@ -0,0 +1,17 @@ +set(target tests) + +file(GLOB core_sources "*.cpp") + +set(includes + ${PROJECT_SOURCE_DIR}/lib/catch/single_include +) + +add_executable(${target} ${core_sources}) +target_include_directories(${target} PRIVATE ${includes}) +target_link_libraries(${target} anthem) + +add_custom_target(run-tests + COMMAND ${CMAKE_BINARY_DIR}/bin/tests + DEPENDS ${target} + WORKING_DIRECTORY ${CMAKE_BINARY_DIR} +) diff --git a/tests/TestTranslation.cpp b/tests/TestTranslation.cpp new file mode 100644 index 0000000..4044d51 --- /dev/null +++ b/tests/TestTranslation.cpp @@ -0,0 +1,2 @@ +#include + diff --git a/tests/main.cpp b/tests/main.cpp new file mode 100644 index 0000000..b3143fb --- /dev/null +++ b/tests/main.cpp @@ -0,0 +1,2 @@ +#define CATCH_CONFIG_MAIN +#include