TCS / Software / circ2dlp
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Translating Circumscription to Disjunctive Logic Programming:

CIRC2DLP


[Background] [Examples] [References] [Using the software] [Download] [Troubleshooting]

News

  • A set of diagnosis benchmarks used in [OJ, 2008] available (May 18, 2007)

Using the Software

circ2dlp is used as follows,
usage: circ2dlp <options> <file> [-m <minimized:different:priorities> -v <varying> -f <fixed>]

Default behaviour is that all atoms are falsified with the highest priority, unless explicitly given a priority for minimization or stated to be varying or fixed. Different priorities are separated with a colon, and a lower priority for a certain atom overrides a higher one (see here for examples). Default behaviour can be changed using option --vary. Notice however, that invisible atoms that lparse produces (atoms that have no name in the symbol table) always have the default behaviour being minimized with highest priority and --vary option cannot be applied to programs containing invisible atoms, as the semantics of invisible atoms becomes unclear. Wildcards can be used when giving the set of minimized, varying and fixed atoms or predicates: ? matches any one character, * any character or characters and [ ] one of the characters included inside the brackets.

Command line options for circ2dlp are the following:
  • -h or --help -- print help message
  • -t -- human readable output
  • --dlv -- output in dlv syntax
  • --vary -- vary all atoms by default
  • --version -- print version information

circ2dlp can also be used to programs containing negation. Then the translation yields the ⟨P_1>...>P_k,V,F⟩ -minimal models of the Gelfond-Lifschitz reduct of the original program Π, that is, the ⟨P_1>...>P_k,V,F⟩-stable models of Π in a sense.

For instance, circ2dlp is used as follows in order to compute all ⟨P,V,F⟩-minimal models of program.lp:
lparse --dlp program.lp > program.sm
circ2dlp program.sm -v [atoms in V] -f [atoms in F] | gnt 0
or (when using dlv)
circ2dlp --dlv program.sm -v [atoms in V] -f [atoms in F] | dlv -n=0 --

More examples of the usage of circ2dlp can be found here.


Download

Disclaimer: The software below is provided on "as is" basis, without warranties of any kind or fitness for a particular purpose.

Copyright: The copyright for circ2dlp is held by Emilia Oikarinen and for dencode, lpcat and lplist by Tomi Janhunen. You may freely use this software for academic and research purposes but not redistribute it.

Current version

circ2dlp-2.1 has been designed to be used with GnT (version 2.1 for lparse-1.0.14) and the front-end lparse (version 1.0.14 or later). In addition, there is a support for producing an input file for dlv.

Old versions

  • circ2dlp-2.0, a preliminary version of the linear translation for prioritized circumscription.
  • circ2dlp-1.1 is designed to be used with GnT (version 2.1) and lparse (pre 1.0.14). Note that it is possible to switch between old (pre 1.0.14) and new formats using dencode.
  • Version 1.1 has no direct support for prioritized circumscription. Lifschitz' scheme is implemented as a script prio_circ2dlp (README).
    • lpcat (concatenates two programs)
    • lplist (outputs program in textual format)

Benchmarks


Troubleshooting

  • lparse-1.0.17 produces warning messages of the form

    2: Warning: 0: lower bound (-2147483647) in an extended rule section is bigger than the upper bound (135097400)

    There are spurious warnings and can be neglected. A way to get rid of these messages is to use the -Wnone option of lparse-1.0.17.

  • The newest versions of lparse (1.0.14 and higher) produce disjunctive rules with a new code (number 8) which is not understood by GnT. This results in error messages

    gnt2: error in input

    Therefore circ2dlp should be used with a special compilation of GnT for lparse 1.0.14 .

  • circ2dlp (2.0 and higher) assumes input in the new lparse format, and circ2dlp (1.1) in the old format. If the input file for circ2dlp is in the wrong format, it results in an error message:

    circ2dlp: unknown rule type.

    This can be circumvented with the help of dencode which switches between old (pre 1.0.14) and new (1.0.14 and higher) formats of lparse (options -o and -n).


[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 06 February 2013. Emilia Oikarinen