dlvhex

Getting started with dlvhex

You can invoke dlvhex directly on the command-line. Depending on the version you are using, executing dlvhex (or dlvhex2) on the commandline looks similar to the following.

DLVHEX  2.0.0 [build Mar  6 2012   gcc 4.2.1 Compatible Clang 3.0 (144389)]

Usage: ./dlvhex2 [OPTION] FILENAME [FILENAME ...]

   or: ./dlvhex2 [OPTION] --

Specify -h or --help for more detailed usage information.

The first line will most probably look different with your installation. It first tells you which program this is, then it gives information about the version. This consists of the date when the binary was built and the identifier of the compiler. Usually, you will not have to bother with these details, but please include this information when you are reporting a bug or asking for support.

If you do not want to see this status line, use the --silent option, which suppresses various informational output and blank lines.

Since we did not specify any input file, dlvhex just prints a brief usage message. Let's try with an empty file:

$ dlvhex --silent empty
{}

The "{}" tells you that the input (no program) admits the model in which nothing is true (and as a matter of fact, in which nothing is false either in this case).

A more detailed introduction and some examples and code snippets can be found in the User Guide.

Caution: It is very important to note the difference between an empty model (as above) and no model: If a program has no model, it is contradictory or inconsistent in some sense, while this is not the case with an empty model.

Search this Website

General
dlvhex source code @ github.com
Description-Of-A-Project

Documentation
User Guide
README
doxygen
Writing Plugins in C++
Writing Plugins in Python