******************************************************************************
 *                            DeltaASP                                        *
 ******************************************************************************

  This is a release of DeltaASP, which is a delta-debugger for answer
  set solver development. It expects the input to be in lparse format.
  DeltaASP is released under GPL. A copy of the license can be found in
  the file COPYING.

  The delta-debugger is written in Java. My short introduction assumes
  that you work on a UNIX/LINUX system with Sun's JDK installed.  However,
  it should be easy to follow the introductions and to use DeltaASP on any
  other operating system that supports Java. Note that if you do not want
  to compile the delta-debugger yourself, you just need a compatible Java
  runtime environment in order to run the delta-debugger.

  If you want to build the delta-debugger yourself: I use Apache Ant as
  a build system and I also provide the build-file 'build.xml'. So, if
  you want to build the delta-debugger, you have to install Ant. Then,
  go to the working directory of DeltaASP and simply type 'ant' to build
  the delta-debugger.

  For UNIX/LINUX systems: I provide a wrapper shell script 'deltaasp'.
  I recommend using this script, it is much more comfortable.

  If you want to enable the debugging code of the delta-debugger itself,
  then enable compilation with debugging info in the build file 'build.xml':

  <javac debug="yes" srcdir="${src}" destdir="${build}"/>

  The code of the delta-debugger contains assertions. If you want to enable
  these assertions at run time, you have to call the java interpreter with
  the option '-ea'. Simply add this option to the script 'deltaasp'. If
  you just want to run the delta-debugger, skip the two steps above.

  I provide the examples ex1.lp and ex2.lp in the directory 'examples' so
  that you can play with the delta-debugger and get a feeling how it works.
  For each example there is a shell script 'run*.sh' that you can use with
  this example. For instance, run1.sh returns the exit code 1 if it can
  find an integrity constraint in the program, and zero otherwise. Try
  to call the delta-debugger as follows. I assume you are in the working
  directory of deltaasp.

  ./deltaasp -v -v -v ./examples/ex1.lp ./reduced.lp ./examples/run1.sh

  The argument '-v' increases verbosity, so you can see each simplification
  step that the delta-debugger tries to do. At verbosity level 3 the
  delta-debugger uses some color codes. If you have problems, e.g. you are
  not using a shell such as bash, you can disable the color output with
  the argument '-no-colors'. The argument 'examples/ex1.lp' is the original
  file. The argument './reduced.lp' is where the simplified output should
  be written to. Finally, './examples/run1.sh' is the executable that the
  delta-debugger calls.

  First, the delta-debugger executes 'examples/run1.sh' with
  'examples/ex1.lp' as argument in order to compute the golden exit code,
  which is 1 in this case. Then, the delta-debugger tries to minimize
  the input.  After each simplification step, the delta-debugger calls
  'examples/run1.sh' with a simplified variant of the original input. If
  'examples/run1.sh' returns the same exit code as the golden exit code,
  then the delta-debugger treats the simplification as success, immediately
  writes the intermediate result into './reduced.lp', and continues
  simplifying. Otherwise, the delta-debugger treats the simplification as
  failure, and tries another simplification.

  As the delta-debugger immediately writes each simplified intermediate
  result into './reduced.lp' you do not have to wait until the
  delta-debugger has fully finished. Notice that typical delta-debugging
  sessions only need a few seconds or minutes.

  Delta-debugging discrepancies between solvers can also be debugged with
  a script. Just write a script which returns 1 if the solvers disagree
  if called with the argument, and returns 0 otherwise. A small example
  is as follows:

#!/bin/bash
# adapt these two lines to call the solvers you want to consider
res1=`~/deltaasp/solvers/solver1 $1`
res2=`~/deltaasp/solvers/solver2 $1`

if [[ $res1 != sat ]] && [[ $res1 != unsat ]]; then
  exit 0
fi 
if [[ $res2 != sat ]] && [[ $res2 != unsat ]]; then
  exit 0
fi
if [[ $res1 != $res2 ]]; then
  exit 1
fi
exit 0

  If you have problems with solvers that do not seem to terminate, you can
  use DeltaASP's timeout feature. If you enable a timeout, e.g. '-t 10',
  a timeout of 10 seconds is used. If, after each simplification step, the
  delta-debugger calls the executable with the simplified variant and the
  executable times out, then the delta-debugger treats this case as if the
  simplification has failed and continues.  Without this timeout feature,
  the delta-debugger would wait forever for the solver to complete.

  Troubleshooting: Some bugs that you try to delta-debug may have
  a non-deterministic nature.  So, it may happen that when you call your
  script outside the delta-debugger with the original input, it returns the
  expected exit code. But, when it is called from inside the delta-debugger,
  then it returns a different exit code and the delta-debugger simplifies
  the input to a trivial program. It may also happen that the simplified
  variant does not trigger the bug when the script is called outside the
  delta-debugger, or the delta-debugger returns different results when called
  multiple times.  If this is due to the non-deterministic nature of the
  bug, then there is hardly anything you can do. If you have memory problems
  that cause non-deterministic behavior, try to use Valgrind and eliminate
  memory bugs first. Valgrind can be downloaded from http://valgrind.org

  If you have comments, questions, improvements or bug reports, then just
  send them to my mail address: robert.brummayer@gmail.com 
  I will try to answer your mails as soon as possible.

  Robert