usage:  dlv {FRONTEND} {OPTIONS} [filename [filename [...]]]

Frontends:

-FB           Brave reasoning
-FC           Cautious reasoning
-FD           Abductive diagnosis
-FDmin        Abductive diagnosis, subset minimal
-FDsingle     Abductive diagnosis, single error
-FR           Reiter's diagnosis
-FRmin        Reiter's diagnosis, subset minimal
-FRsingle     Reiter's diagnosis, single error
-FP           Planning with "K" Action Language
-FPopt        ...find optimistic plans in batch mode
-FPsec        ...find secure plans in batch mode
-FPc          Planning with "C" Action Language
-FPcheck=<n>  Secure Check method <n>. Currently implemented: 1,2
-FPsoundcheck=<n>    A sound secure check method.    
-FPcompletecheck=<n> A complete secure check method. 
-planlength=<N> Maximum plan length for planning frontend
-plancache=<N>  Size of the plan cache (number of plans, defaults to 10000)
-FS           SQL3

General Options:

--            Also read input from stdin.
-costbound=<N,..,N> Find models with cost <= <N,..,N> (N=_ indicates that no bound is required).
-det          Only compute the deterministic consequences.
-instantiate  Only ground and print the instantiation.
-n=<n>        Compute at most <n> stable models (-n=0 and -n=all give all).
-N=<N>        Limit integers to [0,<N>].
-wait         Before terminating, wait until Return is pressed.

Output Options:

-filter=<X>   Include only instances of predicate <X> in output.
 -pfilter=<X> Include only positive instances of predicate <X> in output.
-facts        Include facts as part of the output.
 -nofacts     Don't include facts as part of the output.
-license      Print the license of this program.
-silent       Suppress the startup banner and blank lines.
-stats        Print statistics and timings regarding the computation.
-v            Be a bit more verbose than usual.
-wctrace      Print all (possibly not optimal) models 
              during computation of weak constraints.

Optimizations:

-O0           Disable all optimizations.
-OR[-]        Input rewriting.
-OGp[-]       Use special grounder for propositional input.
-OGo(0|1|2)   Grounding performs (no|simple|advanced)
              dynamic body reordering.
-OGs          Grounding employs semi-naive evaluation.
-OH[-]        Heuristics.
-OM-          Special Model Checker mode. Not for general use!
-OMb[-]       Model-checking employs novel backtracking technique.
-OP-          Disable partial model checking.
-OPf          Partial model checking ``forwards''.
-OPb          Partial model checking during backtracking.

Default options: -OR -OGp -OGo2 -OGs -OH -OMb -OPb