OnWorks favicon

dfg2dfg - Online in the Cloud

Run dfg2dfg in OnWorks free hosting provider over Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator

This is the command dfg2dfg that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator



dfg2dfg - calculate approximations of problems


dfg2dfg [-horn] [-monadic] [-linear] [-shallow] [infile] [outfile]


dfg2dfg is a program that reads clauses from an input file in DFG syntax. It then
calculates an approximation of the clause set depending on the command line options.
Finally it writes the approximated clause set in DFG syntax to a file.

If neither infile nor outfile are given, dfg2dfg 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, dfg2dfg reads from the first
file and writes to the second.

The approximations are described in technical detail in the separate paper dfg2dfg.ps
included in the SPASS distribution.


dfg2dfg has four different command line options that may be combined.

This option enables the transformation of non-horn clauses into horn clauses. Each
non-horn clause with n positive literals is transformed into n horn clauses, where the
i-th clause contains the i-th positive literal and all negative literals of the non-
horn clause. See also section 3 of the paper.

With this option atoms with non-monadic predicate symbols are transformed into monadic
atoms. If n is omitted or n=1 a term encoding is applied, i.e., all non-monadic
predicates are moved to the term level. With n=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.

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.

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 n is omitted
or n=1 a strict transformation is applied, that is equivalence preserving, however.
For n=2 some preconditions are removed. This allows the transformation to be applied
more often, but the transformation isn't equivalence preserving any more. For n=3
even more preconditions are removed. Take a look at section 6.n of the paper for the
details of the command line option -monadic=n.

Use dfg2dfg online using onworks.net services

Free Servers & Workstations

Download Windows & Linux apps

  • 1
    VBA-M (Archived - Now on Github)
    VBA-M (Archived - Now on Github)
    Project has moved to
    Features:Cheat creationsave statesmulti
    system, supports gba, gbc, gb, sgb,
    Download VBA-M (Archived - Now on Github)
  • 2
    Linux System Optimizer and Monitoring
    Github Repository:
    Audience: End Users/Desktop. User
    interface: Qt. Programming La...
    Download Stacer
  • 3
    Fork of TeamWinRecoveryProject(TWRP)
    with many additional functions, redesign
    and more Features:Supports Treble and
    non-Treble ROMsUp-to-date Oreo kernel,
    Download OrangeFox
  • 4
    itop - ITSM  CMDB OpenSource
    itop - ITSM CMDB OpenSource
    IT Operations Portal: a complete open
    source, ITIL, web based service
    management tool including a fully
    customizable CMDB, a helpdesk system and
    a document man...
    Download itop - ITSM CMDB OpenSource
  • 5
    Clementine is a multi-platform music
    player and library organizer inspired by
    Amarok 1.4. It has a fast and
    easy-to-use interface, and allows you to
    search and ...
    Download Clementine
  • 6
    ATTENTION: Cumulative update 2.4.3 has
    been released!! The update works for any
    previous 2.x.x version. If upgrading
    from version v1.x.x, please download and
    Download XISMuS
  • 7
    Modular headtracking program that
    supports multiple face-trackers, filters
    and game-protocols. Among the trackers
    are the SM FaceAPI, AIC Inertial Head
    Tracker ...
    Download facetracknoir
  • More »

Linux commands