EnglishFrenchSpanish

Ad


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

PROGRAM:

NAME


dfg2dfg - calculate approximations of problems

SYNOPSIS


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

DESCRIPTION


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.

OPTIONS


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

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

-monadic[=n]
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.

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

-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 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
    AstrOrzPlayer
    AstrOrzPlayer
    AstrOrz Player is a free media player
    software, part based on WMP and VLC. The
    player is in a minimalist style, with
    more than ten theme colors, and can also
    b...
    Download AstrOrzPlayer
  • 2
    movistartv
    movistartv
    Kodi Movistar+ TV es un ADDON para XBMC/
    Kodi que permite disponer de un
    decodificador de los servicios IPTV de
    Movistar integrado en uno de los
    mediacenters ma...
    Download movistartv
  • 3
    Code::Blocks
    Code::Blocks
    Code::Blocks is a free, open-source,
    cross-platform C, C++ and Fortran IDE
    built to meet the most demanding needs
    of its users. It is designed to be very
    extens...
    Download Code::Blocks
  • 4
    Amidst
    Amidst
    Amidst or Advanced Minecraft Interface
    and Data/Structure Tracking is a tool to
    display an overview of a Minecraft
    world, without actually creating it. It
    can ...
    Download Amidst
  • 5
    MSYS2
    MSYS2
    MSYS2 is a collection of tools and
    libraries providing you with an
    easy-to-use environment for building,
    installing and running native Windows
    software. It con...
    Download MSYS2
  • 6
    libjpeg-turbo
    libjpeg-turbo
    libjpeg-turbo is a JPEG image codec
    that uses SIMD instructions (MMX, SSE2,
    NEON, AltiVec) to accelerate baseline
    JPEG compression and decompression on
    x86, x8...
    Download libjpeg-turbo
  • More »

Linux commands

  • 1
    abi-tracker
    abi-tracker
    abi-tracker - visualize ABI changes
    timeline of a C/C++ software library.
    DESCRIPTION: NAME: ABI Tracker
    (abi-tracker) Visualize ABI changes
    timeline of a C/C+...
    Run abi-tracker
  • 2
    abicheck
    abicheck
    abicheck - check application binaries
    for calls to private or evolving symbols
    in libraries and for static linking of
    some system libraries. ...
    Run abicheck
  • 3
    couriermlm
    couriermlm
    couriermlm - The Courier mailing list
    manager ...
    Run couriermlm
  • 4
    couriertcpd
    couriertcpd
    couriertcpd - the Courier mail server
    TCP server daemon ...
    Run couriertcpd
  • 5
    gbklatex
    gbklatex
    bg5latex - Use LaTeX directly on a Big5
    encodedtex file bg5pdflatex - Use
    pdfLaTeX directly on a Big5 encodedtex
    file bg5+latex - Use LaTeX directly on a
    Big5+...
    Run gbklatex
  • 6
    gbkpdflatex
    gbkpdflatex
    bg5latex - Use LaTeX directly on a Big5
    encodedtex file bg5pdflatex - Use
    pdfLaTeX directly on a Big5 encodedtex
    file bg5+latex - Use LaTeX directly on a
    Big5+...
    Run gbkpdflatex
  • More »

Ad