Skip to content
forked from hexhex/core

DLVHEX solver: core system and plugin API

License

LGPL-2.1, GPL-2.0 licenses found

Licenses found

LGPL-2.1
COPYING.LESSER
GPL-2.0
COPYING
Notifications You must be signed in to change notification settings

Mustafa226/core

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

DLVHEX Core ===========

This file provides some hints how to install and run dlvhex.

You just want to use the binary

We provide pre-compiled Debian/Ubuntu packages of dlvhex and its plugins at https://launchpad.net/~tkren/+archive/asp. Just run

$ sudo add-apt-repository ppa:tkren/asp

and then you can install dlvhex and the plugins using your favorite package management tool.

You want to build and install from source

dlvhex uses the standard

$ ./configure && make && make install

approach for installation. In any case, you probably need to install additional packages to satisfy all required software dependencies.

Dependencies

libgringo / libclasp (shipped with this package, default)

If you just run ./configure without extra parameters, it will unpack gringo and clasp which is contained in this package, and build it and configure dlvhex to use it as solver engine (if dlv is present, both can be used with the –solver argument).

This uses gringo and clasp as genuine grounder resp. solver for hex.

If something fails, see the followg information.

You can also use the script checkout_build_potassco.sh in this package to prepare gringo and clasp libraries to be used by dlvhex.

Use the configure option `–with-libgringo=<gringo-trunk-dir>’ resp. `–with-libclasp=<clasp-trunk-dir>’ to specify the directory where you have built clingo-app resp. clasp.app.

IMPORTANT:

  • use the same boost library as dlvhex, 1.43 works for us
  • you might need to hack CMakeLists.txt to accept your boost version
  • CMakeLists.txt should be modified to force the usage of multithreaded boost (change OFF to ON in the respective line) because dlvhex requires multithreaded boost libraries

DLV (optional)

dlvhex uses the answer-set solver DLV, which can be downloaded from http://www.dlvsystem.com/. Put the downloaded binary in your path so that it is executable on your system (don’t forget to “chmod +x” it!). dlvhex is looking for `dlv’, so you might want to rename the downloaded binary or create a softlink to it.

libclingo (optional)

Alternatively, you can use libclingo as background model builder. Use the configure option `–with-libclingo=<gringo-trunk-dir>’ to specify the directory where you have built clingo-app.

How to build a working clingo-app:

  • checkout 3.0.4 tag of gringo $ svn co https://potassco.svn.sourceforge.net/svnroot/potassco/tags/gringo-3.0.4 $ cd gringo-3.0.4
  • create release directory $ mkdir -p build/release
  • cmake (specify your boost root) $ BOOST_ROOT=<yourboost> cmake ../.. -DCMAKE_CXX_FLAGS=-Wall -DCMAKE_BUILD_TYPE=release
  • make (specify your boost root) $ BOOST_ROOT=<yourboost> make clingo-app

Now configure dlvhex with

$ ./configure –with-libclingo=/path/to/gringo-3.0.4

IMPORTANT:

  • use the same boost library as dlvhex, 1.43 works for us
  • you might need to hack CMakeLists.txt to accept your boost version

There is also a script which does everything automatically: checkout_build_potassco.sh

DLVDB

currently unsupported

libdlv

currently unsupported

boost

Boost is a collection of portable C++ source libraries, which are intended to be widely useful, and usable across a broad spectrum of applications. You will need a version >= 1.43. See http://www.boost.org/.

dlvhex needs the following Boost libraries: Boost.Graph Boost.Iostreams Boost.Smart_Ptr Boost.Spirit Boost.String_Algo Boost.Tokenizer Boost.Thread Boost.UnitTestFramework

Popular Linux and Unix distributions such as Fedora, Debian, and NetBSD include pre-built Boost packages. E.g., in Debian/Ubuntu just run

$ sudo apt-get install libboost-all-dev

or

$ sudo apt-get install libboostN.NN-all-dev

for boost version N.NN.

If your Debian/Ubuntu system did not provide recent boost packages, have a look at https://launchpad.net/~boost-latest/+archive/ppa.

Installation instructions are given in the INSTALL file found in the boost distributions tarball. In order to install boost-iostream, install libbz2-dev. Here is a quick-start guide for compiling boost (if you have multiple cpus available, call the 2nd b2 with -j<N>, where <N> is the number of cpus):

$ ./bootstrap.h –prefix=/path/to/install/boost $ ./b2 –build-type=complete –layout=tagged threading=single,multi variant=release $ ./b2 install –layout=tagged

If you have compiled boost by yourself, you have to tell the dlvhex configure script where you have installed it with

$ ./configure –with-boost=/path/to/boost-prefix

Under Windows, configure the boost libraries as follows: > b2.exe –toolset=msvc-10.0 –build-type=complete –with-python link=static

libcurl

libcurl is a multi-protocol file transfer library. dlvhex uses it to retrieve programs specified by http-scheme URLs. This library is standard for most operating systems (see http://curl.haxx.se/libcurl/ for source packages).

Debian/Ubuntu provides packages called libcurl-dev, libcurlN-openssl-dev, and libcurlN-gnutls-dev (or libcurlN-dev) for some N; install one of these and you will be able to compile dlvhex.

Configuration

Run `configure’ to create the necessary Makefiles. As usual, use the –prefix switch to specify a custom installation location. dlvhex uses pkg-config to share build-related configuration with plugins. So if you also intend to compile plugins and use a custom prefix for dlvhex, make sure to adjust the PKG_CONFIG_PATH environment variable appropriately, otherwise the configuration of the plugins will not work. E.g., if your prefix is /usr/local (the default), then PKG_CONFIG_PATH needs to be set to /usr/local/lib/pkgconfig like this:

$ ./configure PKG_CONFIG_PATH=/usr/local/lib/pkgconfig

If you installed boost in a non-standard folder, add `–with-boost=/path/to/boost-prefix’ to the configure switches to specify the location of the header files (see above).

If you compile with special model building libraries, consult the section Dependencies above for configuring dlvhex.

If `configure’ complains, then something vital for building dlvhex is missing in your system. If you get complaints about missing boost-headers, make sure that you have the necesary parts of boost installed and that their version is sufficiently recent (see Dependencies above).

On Apple OS X, it is recommended to use GNU CC instead of the compiler shipped with OS X. Moreover, you will need to install the GNU tools cmake, wget, automake, pkgconfig, scons and re2c. For this, before starting with the installation procedure described above, install MacPorts (http://www.macports.org) and type

sudo port install cmake wget automake gcc48 pkgconfig sudo port select –set gcc mp-gcc48

In order to support Python-implemented plugins, pass the option –enable-python

If you installed the Python development files from source, make sure that you configured with –enable-unicode=ucs4

Documentation

Run `make doxygen-doc’ to create the html documentation (a subdirectory `doc’ will be created). By default, only the html-docs will be built. To enable other formats, you have to give additional configure-switches, e.g., by calling

$ ./configure –enable-doxygen-pdf […]

you get a pdf-version of the documentation.

Testing

Run `make check’ to build and execute the cppunit-based regression testsuite. Note that the testsuite is only being built if cppunit is installed.

Installation

Run `make install’ to install the binary dlvhex, its libraries and the corresponding header files, which are needed for developing plugins. Sometimes it is necessary to run

$ sudo ldconfig

after the first installation to refresh the shared library cache.

Running dlvhex

Using dlvhex is very similar to working with the answer-set solver dlv. `dlvhex –help’ displays a short help with available command-line parameters. For an introduction how to write HEX-programs, see the documentation provided at http://http://www.kr.tuwien.ac.at/research/systems/dlvhex/ or look at the `examples’ directory here. DLV programs are described at http://www.dbai.tuwien.ac.at/proj/dlv/#docs.

Implementing your own plugins and external computations

For documentation on plugin writing, please consult the doxygen documentation in header files include/dlvhex2/PluginInterface.h and include/dlvhex2/ComfortPluginInterface.h. You might also want to have a look at testsuite/TestPlugin.cpp, the internal plugins of dlvhex (classes QueryPlugin, StrongNegationPlugin, and HigherOrderPlugin) and existing plugins like dlvhex-stringplugin and dlvhex-scriptplugin in the same repository as dlvhex.

vim:ts=4:tw=75:

About

DLVHEX solver: core system and plugin API

Resources

License

LGPL-2.1, GPL-2.0 licenses found

Licenses found

LGPL-2.1
COPYING.LESSER
GPL-2.0
COPYING

Stars

Watchers

Forks

Packages

No packages published

Languages

  • C++ 96.2%
  • C 1.9%
  • Shell 1.3%
  • Makefile 0.6%
  • Python 0.0%
  • Prolog 0.0%