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