Initial commit.

This commit is contained in:
Patrick Lühne 2016-11-21 17:51:14 +01:00
commit 3100f4a733
No known key found for this signature in database
GPG Key ID: 05F3611E97A70ABF
14 changed files with 262 additions and 0 deletions

4
.gitattributes vendored Normal file
View File

@ -0,0 +1,4 @@
.gitignore export-ignore
.gitattributes export-ignore
.gitmodules export-ignore
.travis.yml export-ignore

6
.gitmodules vendored Normal file
View File

@ -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

47
.travis.yml Normal file
View File

@ -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

33
CMakeLists.txt Normal file
View File

@ -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()

21
LICENSE.md Normal file
View File

@ -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.

31
README.md Normal file
View File

@ -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)

13
app/CMakeLists.txt Normal file
View File

@ -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)

58
app/main.cpp Normal file
View File

@ -0,0 +1,58 @@
#include <iostream>
#include <boost/program_options.hpp>
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<std::vector<std::string>>(), "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;
}

1
lib/catch Submodule

@ -0,0 +1 @@
Subproject commit e27c4ee04282f60aefcc9b1062a74f92cf6c1a2b

1
lib/clingo Submodule

@ -0,0 +1 @@
Subproject commit 3a704a64f848eb6207591690cd9a2193ae9f9fb8

26
src/CMakeLists.txt Normal file
View File

@ -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})

17
tests/CMakeLists.txt Normal file
View File

@ -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}
)

View File

@ -0,0 +1,2 @@
#include <catch.hpp>

2
tests/main.cpp Normal file
View File

@ -0,0 +1,2 @@
#define CATCH_CONFIG_MAIN
#include <catch.hpp>