1
.\" Automatically generated by Pod::Man 2.1801 (Pod::Simple 3.05)
4
.\" ========================================================================
5
.de Sp \" Vertical space (when we can't use .PP)
9
.de Vb \" Begin verbatim text
14
.de Ve \" End verbatim text
18
.\" Set up some character translations and predefined strings. \*(-- will
19
.\" give an unbreakable dash, \*(PI will give pi, \*(L" will give a left
20
.\" double quote, and \*(R" will give a right double quote. \*(C+ will
21
.\" give a nicer C++. Capital omega is used to do unbreakable dashes and
22
.\" therefore won't be available. \*(C` and \*(C' expand to `' in nroff,
23
.\" nothing in troff, for use with C<>.
25
.ds C+ C\v'-.1v'\h'-1p'\s-2+\h'-1p'+\s0\v'.1v'\h'-1p'
29
. if (\n(.H=4u)&(1m=24u) .ds -- \(*W\h'-12u'\(*W\h'-12u'-\" diablo 10 pitch
30
. if (\n(.H=4u)&(1m=20u) .ds -- \(*W\h'-12u'\(*W\h'-8u'-\" diablo 12 pitch
43
.\" Escape single quotes in literal strings from groff's Unicode transform.
47
.\" If the F register is turned on, we'll generate index entries on stderr for
48
.\" titles (.TH), headers (.SH), subsections (.SS), items (.Ip), and index
49
.\" entries marked with X<> in POD. Of course, you'll have to process the
50
.\" output yourself in some meaningful fashion.
53
. tm Index:\\$1\t\\n%\t"\\$2"
63
.\" Accent mark definitions (@(#)ms.acc 1.5 88/02/08 SMI; from UCB 4.2).
64
.\" Fear. Run. Save yourself. No user-serviceable parts.
65
. \" fudge factors for nroff and troff
74
. ds #H ((1u-(\\\\n(.fu%2u))*.13m)
80
. \" simple accents for nroff and troff
90
. ds ' \\k:\h'-(\\n(.wu*8/10-\*(#H)'\'\h"|\\n:u"
91
. ds ` \\k:\h'-(\\n(.wu*8/10-\*(#H)'\`\h'|\\n:u'
92
. ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'^\h'|\\n:u'
93
. ds , \\k:\h'-(\\n(.wu*8/10)',\h'|\\n:u'
94
. ds ~ \\k:\h'-(\\n(.wu-\*(#H-.1m)'~\h'|\\n:u'
95
. ds / \\k:\h'-(\\n(.wu*8/10-\*(#H)'\z\(sl\h'|\\n:u'
97
. \" troff and (daisy-wheel) nroff accents
98
.ds : \\k:\h'-(\\n(.wu*8/10-\*(#H+.1m+\*(#F)'\v'-\*(#V'\z.\h'.2m+\*(#F'.\h'|\\n:u'\v'\*(#V'
99
.ds 8 \h'\*(#H'\(*b\h'-\*(#H'
100
.ds o \\k:\h'-(\\n(.wu+\w'\(de'u-\*(#H)/2u'\v'-.3n'\*(#[\z\(de\v'.3n'\h'|\\n:u'\*(#]
101
.ds d- \h'\*(#H'\(pd\h'-\w'~'u'\v'-.25m'\f2\(hy\fP\v'.25m'\h'-\*(#H'
102
.ds D- D\\k:\h'-\w'D'u'\v'-.11m'\z\(hy\v'.11m'\h'|\\n:u'
103
.ds th \*(#[\v'.3m'\s+1I\s-1\v'-.3m'\h'-(\w'I'u*2/3)'\s-1o\s+1\*(#]
104
.ds Th \*(#[\s+2I\s-2\h'-\w'I'u*3/5'\v'-.3m'o\v'.3m'\*(#]
105
.ds ae a\h'-(\w'a'u*4/10)'e
106
.ds Ae A\h'-(\w'A'u*4/10)'E
107
. \" corrections for vroff
108
.if v .ds ~ \\k:\h'-(\\n(.wu*9/10-\*(#H)'\s-2\u~\d\s+2\h'|\\n:u'
109
.if v .ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'\v'-.4m'^\v'.4m'\h'|\\n:u'
110
. \" for low resolution devices (crt and lpr)
111
.if \n(.H>23 .if \n(.V>19 \
124
.\" ========================================================================
126
.IX Title "DFG2DFG 1"
127
.TH DFG2DFG 1 "2010-02-23" "perl v5.10.0" "SPASS"
128
.\" For nroff, turn off justification. Always turn off hyphenation; it makes
129
.\" way too many mistakes in technical documents.
133
dfg2dfg \- calculate approximations of problems
135
.IX Header "SYNOPSIS"
136
\&\fBdfg2dfg\fR [\-horn] [\-monadic] [\-linear] [\-shallow] [\fIinfile\fR] [\fIoutfile\fR]
138
.IX Header "DESCRIPTION"
139
\&\fBdfg2dfg\fR is a program that reads clauses from an input file in \s-1DFG\s0
141
It then calculates an approximation of the clause set depending on the
142
command line options.
143
Finally it writes the approximated clause set in \s-1DFG\s0 syntax to a file.
145
If neither \fIinfile\fR nor \fIoutfile\fR are given, \fBdfg2dfg\fR reads
146
from standard input and writes to standard output.
147
If one file name is given, it reads from that file and writes the output to
149
If more than one file name is given, \fBdfg2dfg\fR reads from the first
150
file and writes to the second.
152
The approximations are described in technical detail in the separate paper
153
\&\fBdfg2dfg.ps\fR included in the \s-1SPASS\s0 distribution.
156
\&\fBdfg2dfg\fR has four different command line options that may be combined.
159
This option enables the transformation of non-horn clauses into horn clauses.
160
Each non-horn clause with \fIn\fR positive literals is transformed into
161
\&\fIn\fR horn clauses, where the \fIi\fR\-th clause contains the \fIi\fR\-th
162
positive literal and all negative literals of the non-horn clause.
163
See also section 3 of the paper.
164
.IP "\-monadic[=n]" 4
165
.IX Item "-monadic[=n]"
166
With this option atoms with non-monadic predicate symbols are transformed into
168
If \fIn\fR is omitted or \fIn\fR=1 a term encoding is applied, i.e., all
169
non-monadic predicates are moved to the term level.
170
With \fIn\fR=2 a projection is applied. All non-monadic atoms are replaced
171
by their monadic argument projections.
172
See section 4.1 section 4.2 of the paper for more details.
175
This approximation transforms a clause with monadic literals and non-linear
176
variable occurrences in succedent atoms, into a new clause with possibly
177
more negative literals, that doesn't contain any non-linear variables in the
179
See section 5 of the paper for details.
180
.IP "\-shallow[=n]" 4
181
.IX Item "-shallow[=n]"
182
This transformation tries to reduce the depth of the terms in positive
184
The transformation is applied to horn clauses with monadic literals only.
185
If \fIn\fR is omitted or \fIn\fR=1 a strict transformation is applied,
186
that is equivalence preserving, however.
187
For \fIn\fR=2 some preconditions are removed.
188
This allows the transformation to be applied more often, but the transformation
189
isn't equivalence preserving any more.
190
For \fIn\fR=3 even more preconditions are removed.
191
Take a look at section 6.\fIn\fR of the paper for the details of the command
192
line option \fI\-monadic=n\fR.
194
.IX Header "SEE ALSO"
195
\&\s-1\fISPASS\s0\fR\|(1)
200
Contact : spass@mpi\-inf.mpg.de
added
removed
doc/man/dfg2dfg.1
