ASPTOOLS/MISC: Miscellaneous Tools for ASP

We have implemented a number of subsidiary tools when developing solvers, verification tools, and translators in the context of answer set programming (ASP). This page collects many of them for potential users' convenience.

Index of the Tools

• classic: compute classical models and SE-models for programs
• dencode: encode disjunctive rules
• disclose: reveal hidden atoms by giving them names
• drop: delete rules from a program (randomly)
• igen: add an input generator to a module with external (input) atoms
• interpret: map atom numbers back to symbolic names
• len: calculate the length of a logic program
• lpcat: concatenate two or more logic programs (or modules)
• lplist: produce a source code listing of a logic program
• lpshift: shift disjunctive rules into normal rules
• modlist: split logic program into modules
• modrun: execute a command for each module in turn
• planar: generate random planar graphs
• redr: check the redundancy of individual rules in a ground logic program (module)
• rsat: generate a random 3-SAT instance as a logic program
• shuffle: scramble literals in rules and rules in a program
• support: compute supported models for programs
• testsm: verify if a program has a particular stable model

This software has been designed to be used with smodels (versions 2.*) and the front-end lparse which are are available here. Many of the programs list their command line options when invoked with option flag -h or --help. Version information is printed with --version. Many of the tools understand "-" as a shorthand for standard input.

Download (newer versions)

Download (historical versions)

Usage in Brief

• classic changes the semantics of rules to the classical one using a syntactic transformation. With option flag -s one may compute SE-models or, more generally, VSE-models.

  $ lparse program.lp | classic | smodels 0 $ gringo program.lp | classic -s | clasp 0

• dencode changes the internal encoding of disjunctive rules in disjunctive programs solved with GnT:

  $ dencode {-o|-n} program

  Option flags -o and -n choose which format (old or new) is used for disjunctive rules. Optionally, disjunctive rules can be shifted based on strongly connected components using -s. In this case, body compression is controlled with option flags -bc and -nb.

• disclose adds entries of the form _1, _2, ... to the symbol table of the program for atoms having no name.

  disclose [-pprefix] program

  The prefix can be set freely using option -p. This program may be useful, e.g., when splitting a ground program into modules. By giving auxiliary atoms names, the finest granularity of modules can be obtained. However, the meaning of such newly introduced atoms varies from program to program which may hinder equivalence checking altogether.

• drop deletes (random) rules from a program:

  $ drop [-v] [-sseed] [-nnumber of rules] [-wwhere to start] program

  Drops randomly the given number of rules from the program. The internal format of smodels is used. Given the option -v, the program is printed in a textual format. Optionally, -w specifies the index of the rule from where the (non-random) deletion of rules starts.

• igen adds an input generator to a program module:

  $ igen [-i|-g|-s|-r] module | smodels 0

  Programs (or modules) may contain external (input) atoms that are not defined by the rules of the program. Program igen adds a choice rule that creates all truth value combinations for such atoms and hence enables the computation of stable models for a module in separation from the rest of the program. Option -i can be used to introduce external atoms implicitly if your grounder does not support this concept. Then atoms without defining rules (no head occurrences) are treated as input atoms. Option -g selects a random input for the module in question. The seed can be set using -s. Finally, input atoms can also be removed by supplying option -r.

• interpret translates atom numbers into symbolic names which are retrieved from a ground program:

  $ cat file | interpret [-p|-n|-d] program

  A typical SAT solver prints out the satisfying assignment using indices of atoms rather than their symbolic names. This goes back to the DIMACS format using which it is difficult to preserve symbolic names except in an ad-hoc way in comments. As a workaround, interpret acts as a filter which detects atom numbers and maps them back into symbolic names. Other symbols are deleted by default or printed as such (option flag -p). Also negative numbers can be treated as negations using -n. Symbolic names can be retrieved from the ground program (stored in a file) or its truncated version (see the option -s of lpcat). The cat file command above can be replaced by a pipeline which eventually calls a SAT solver and produces an assignment (if any) to be mapped by interpret.

• len calculates the numbers of atoms, rules, and integers (internal file format) for a ground logic program:

  $ len [-a|-r|-l] [-d] program

  Individual parameter values can be calculated using option flags -a (atoms), -r (rules), and -l (integers). A set of clauses in the DIMACS format is assumed if -d is specified.

• lp2normal removes cardinality, choice, and weight rules from a ground smodels program by translating them into basic/normal rules.

  $ lp2normal [-ca|-cb|-cu|-k|-kc|-kw] program

  Option flags -ca, -cb, and -cu activate alternative encodings based on adders, binary numbers, and unary numbers, respectively, for cardinality rules. The scheme proposed by Eén and Sörensson is used by default. Weight rules are treated using binary counters for now. The latter option flags of the form -k* request the tool to preserve choice rules, cardinality rules, and weight rules untouched, e.g., for later processing.

• lpcat links any number of logic programs together:

  $ lpcat [-f files] [-r] [-m] program ...

  The check for module conditions is activated if -m is specified (arbitrary programs cannot be linked together under this option). Files/streams are consulted recursively in order to load a set of modules with option flag -r. File names can be read in from a file specified with -f. The old version (1.8) is able to handle two programs only.

• lplist produces a source code listing for a ground logic program in the internal file format:

  $ lparse program.lp | lplist | less
$ lparse program.lp | lplist | enscript

• lpshift shifts the disjunctive rules of a ground logic program (in the internal file format) into normal rules (subject to limitations):

  $ gringo --output smodels program.lp | lpshift | clasp
  

• modlist splits a logic program into its modules on the basis of strongly connected components and occurrences of hidden atoms (having no name). Modules can be rejoined using lpcat -r.

  $ gringo --output smodels program.lp | modlist
$ gringo --output smodels program.lp | modlist | lpcat -r

  The option -z creates a sequence of shell commands that can be used to create a zipfile of the modules. This enables random access to individual modules. The following commands will create an archive program.zip containing the modules mod_1.sm, mod_2.sm, ... The last command line creates a stream of modules from the zipfile and builds the entire program in program.sm.

  $ lparse program.lp | modlist -z > program.sh
$ source program.sh program.zip mod
$ unzip -q -c program.zip | lpcat -r > program.sm

• modrun executes a given command for each module in a stream of modules (created, e.g., using modlist). The tool can also be used to modularlize program transformations. In the examples below, the command transform is assumed to implement some program tranformation of interest for a single program/module.

  $ lparse program.lp | modlist | modrun "len -r"
$ lparse program.lp | modlist | modrun transform | lpcat -r
$ (for p in *.lp; do lparse $p; done) | modrun transform | lpcat -r

• planar produces a random planar graph having the given number of nodes:

  $ planar number_of_nodes seed

  Consult the Stanford GraphBase library for details.

• redr creates a translation which can be used to check the redundancy of a particular rule in a ground logic program:

  $ redr [-rwhich rule] [-c] [-m] [-i] program

  The number of the rule to check is specified with -r. This number is 1 by default, i.e., the first rule is subject to study. In contrast to redundancy in classical logic, a two-way search is required in principle. For the redundancy of the first rule, for instance, the following commands should not yield stable models:

  $ redr program | smodels 1 $ redr -c program | smodels 1

  The option -m provides support for program modules produced by modlist. In this setting, the flag -i inserts the required input generator automatically and hence smodels can be used to decide the redundancy of individual rules residing in a module.

• rsat creates random 3-SAT problem instances encoded as a logic programs:

  $ rsat [-sseed] [-r] [-d] vars_per_clause vars clauses

  The option -r enables several occurrences of the same variable in a clause. Variables are distinct by default. Option -d produces a disjunctive logic program for GnT or any compatible disjunctive answer set solver.

• shuffle scrambles rules and literals in a logic program:

  $ shuffle [-sseed] file

  You may set the seed of the random number generator using option -s.

• support changes the semantics of rules to the supported model semantics [Apt et al., 1990] using a syntactic transformation.

  $ lparse program.lp | support | smodels 0

• testsm is used to check the existence of a stable model (represented as a list of atoms):

  $ lparse program.lp > program.sm
$ testsm program.sm list_of_atoms | smodels 1
  

  The program adds a compute statement to the program which requires the given atoms to be true and others false by default. Option flags -t and -f change the default action to only marking atoms true and false, respectively. For really big sets of atoms (answer sets) which do not easily fit to a shell command line, the symbolic names of atoms can be read from a file using option flag -a.