.\" Automatically generated by Pod::Man 2.1801 (Pod::Simple 3.05)
.\"
.\" Standard preamble:
.\" ========================================================================
.de Sp \" Vertical space (when we can't use .PP)
.if t .sp .5v
.if n .sp
..
.de Vb \" Begin verbatim text
.ft CW
.nf
.ne \\$1
..
.de Ve \" End verbatim text
.ft R
.fi
..
.\" Set up some character translations and predefined strings.  \*(-- will
.\" give an unbreakable dash, \*(PI will give pi, \*(L" will give a left
.\" double quote, and \*(R" will give a right double quote.  \*(C+ will
.\" give a nicer C++.  Capital omega is used to do unbreakable dashes and
.\" therefore won't be available.  \*(C` and \*(C' expand to `' in nroff,
.\" nothing in troff, for use with C<>.
.tr \(*W-
.ds C+ C\v'-.1v'\h'-1p'\s-2+\h'-1p'+\s0\v'.1v'\h'-1p'
.ie n \{\
.    ds -- \(*W-
.    ds PI pi
.    if (\n(.H=4u)&(1m=24u) .ds -- \(*W\h'-12u'\(*W\h'-12u'-\" diablo 10 pitch
.    if (\n(.H=4u)&(1m=20u) .ds -- \(*W\h'-12u'\(*W\h'-8u'-\"  diablo 12 pitch
.    ds L" ""
.    ds R" ""
.    ds C` ""
.    ds C' ""
'br\}
.el\{\
.    ds -- \|\(em\|
.    ds PI \(*p
.    ds L" ``
.    ds R" ''
'br\}
.\"
.\" Escape single quotes in literal strings from groff's Unicode transform.
.ie \n(.g .ds Aq \(aq
.el       .ds Aq '
.\"
.\" If the F register is turned on, we'll generate index entries on stderr for
.\" titles (.TH), headers (.SH), subsections (.SS), items (.Ip), and index
.\" entries marked with X<> in POD.  Of course, you'll have to process the
.\" output yourself in some meaningful fashion.
.ie \nF \{\
.    de IX
.    tm Index:\\$1\t\\n%\t"\\$2"
..
.    nr % 0
.    rr F
.\}
.el \{\
.    de IX
..
.\}
.\"
.\" Accent mark definitions (@(#)ms.acc 1.5 88/02/08 SMI; from UCB 4.2).
.\" Fear.  Run.  Save yourself.  No user-serviceable parts.
.    \" fudge factors for nroff and troff
.if n \{\
.    ds #H 0
.    ds #V .8m
.    ds #F .3m
.    ds #[ \f1
.    ds #] \fP
.\}
.if t \{\
.    ds #H ((1u-(\\\\n(.fu%2u))*.13m)
.    ds #V .6m
.    ds #F 0
.    ds #[ \&
.    ds #] \&
.\}
.    \" simple accents for nroff and troff
.if n \{\
.    ds ' \&
.    ds ` \&
.    ds ^ \&
.    ds , \&
.    ds ~ ~
.    ds /
.\}
.if t \{\
.    ds ' \\k:\h'-(\\n(.wu*8/10-\*(#H)'\'\h"|\\n:u"
.    ds ` \\k:\h'-(\\n(.wu*8/10-\*(#H)'\`\h'|\\n:u'
.    ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'^\h'|\\n:u'
.    ds , \\k:\h'-(\\n(.wu*8/10)',\h'|\\n:u'
.    ds ~ \\k:\h'-(\\n(.wu-\*(#H-.1m)'~\h'|\\n:u'
.    ds / \\k:\h'-(\\n(.wu*8/10-\*(#H)'\z\(sl\h'|\\n:u'
.\}
.    \" troff and (daisy-wheel) nroff accents
.ds : \\k:\h'-(\\n(.wu*8/10-\*(#H+.1m+\*(#F)'\v'-\*(#V'\z.\h'.2m+\*(#F'.\h'|\\n:u'\v'\*(#V'
.ds 8 \h'\*(#H'\(*b\h'-\*(#H'
.ds o \\k:\h'-(\\n(.wu+\w'\(de'u-\*(#H)/2u'\v'-.3n'\*(#[\z\(de\v'.3n'\h'|\\n:u'\*(#]
.ds d- \h'\*(#H'\(pd\h'-\w'~'u'\v'-.25m'\f2\(hy\fP\v'.25m'\h'-\*(#H'
.ds D- D\\k:\h'-\w'D'u'\v'-.11m'\z\(hy\v'.11m'\h'|\\n:u'
.ds th \*(#[\v'.3m'\s+1I\s-1\v'-.3m'\h'-(\w'I'u*2/3)'\s-1o\s+1\*(#]
.ds Th \*(#[\s+2I\s-2\h'-\w'I'u*3/5'\v'-.3m'o\v'.3m'\*(#]
.ds ae a\h'-(\w'a'u*4/10)'e
.ds Ae A\h'-(\w'A'u*4/10)'E
.    \" corrections for vroff
.if v .ds ~ \\k:\h'-(\\n(.wu*9/10-\*(#H)'\s-2\u~\d\s+2\h'|\\n:u'
.if v .ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'\v'-.4m'^\v'.4m'\h'|\\n:u'
.    \" for low resolution devices (crt and lpr)
.if \n(.H>23 .if \n(.V>19 \
\{\
.    ds : e
.    ds 8 ss
.    ds o a
.    ds d- d\h'-1'\(ga
.    ds D- D\h'-1'\(hy
.    ds th \o'bp'
.    ds Th \o'LP'
.    ds ae ae
.    ds Ae AE
.\}
.rm #[ #] #H #V #F C
.\" ========================================================================
.\"
.IX Title "DFG2DFG 1"
.TH DFG2DFG 1 "2010-02-23" "perl v5.10.0" "SPASS"
.\" For nroff, turn off justification.  Always turn off hyphenation; it makes
.\" way too many mistakes in technical documents.
.if n .ad l
.nh
.SH "NAME"
dfg2dfg \- calculate approximations of problems
.SH "SYNOPSIS"
.IX Header "SYNOPSIS"
\&\fBdfg2dfg\fR [\-horn] [\-monadic] [\-linear] [\-shallow] [\fIinfile\fR] [\fIoutfile\fR]
.SH "DESCRIPTION"
.IX Header "DESCRIPTION"
\&\fBdfg2dfg\fR is a program that reads clauses from an input file in \s-1DFG\s0
syntax.
It then calculates an approximation of the clause set depending on the
command line options.
Finally it writes the approximated clause set in \s-1DFG\s0 syntax to a file.
.PP
If neither \fIinfile\fR nor \fIoutfile\fR are given, \fBdfg2dfg\fR reads
from standard input and writes to standard output.
If one file name is given, it reads from that file and writes the output to
standard output.
If more than one file name is given, \fBdfg2dfg\fR reads from the first
file and writes to the second.
.PP
The approximations are described in technical detail in the separate paper 
\&\fBdfg2dfg.ps\fR included in the \s-1SPASS\s0 distribution.
.SH "OPTIONS"
.IX Header "OPTIONS"
\&\fBdfg2dfg\fR has four different command line options that may be combined.
.IP "\-horn" 4
.IX Item "-horn"
This option enables the transformation of non-horn clauses into horn clauses.
Each non-horn clause with \fIn\fR positive literals is transformed into
\&\fIn\fR horn clauses, where the \fIi\fR\-th clause contains the \fIi\fR\-th
positive literal and all negative literals of the non-horn clause.
See also section 3 of the paper.
.IP "\-monadic[=n]" 4
.IX Item "-monadic[=n]"
With this option atoms with non-monadic predicate symbols are transformed into
monadic atoms.
If \fIn\fR is omitted or \fIn\fR=1 a term encoding is applied, i.e., all
non-monadic predicates are moved to the term level.
With \fIn\fR=2 a projection is applied. All non-monadic atoms are replaced
by their monadic argument projections.
See section 4.1 section 4.2 of the paper for more details.
.IP "\-linear" 4
.IX Item "-linear"
This approximation transforms a clause with monadic literals and non-linear
variable occurrences in succedent atoms, into a new clause with possibly
more negative literals, that doesn't contain any non-linear variables in the
succedent.
See section 5 of the paper for details.
.IP "\-shallow[=n]" 4
.IX Item "-shallow[=n]"
This transformation tries to reduce the depth of the terms in positive
literals.
The transformation is applied to horn clauses with monadic literals only.
If \fIn\fR is omitted or \fIn\fR=1 a strict transformation is applied,
that is equivalence preserving, however.
For \fIn\fR=2 some preconditions are removed.
This allows the transformation to be applied more often, but the transformation
isn't equivalence preserving any more.
For \fIn\fR=3 even more preconditions are removed.
Take a look at section 6.\fIn\fR of the paper for the details of the command
line option \fI\-monadic=n\fR.
.SH "SEE ALSO"
.IX Header "SEE ALSO"
\&\s-1\fISPASS\s0\fR\|(1)
.SH "AUTHORS"
.IX Header "AUTHORS"
Enno Keen
.PP
Contact : spass@mpi\-inf.mpg.de