****************************************************************************** * DeltaSMT * ****************************************************************************** This is a release of DeltaSMT which is a delta-debugger for SMT benchmarks. See www.smtlib.org for more details about SMT. For more info about delta-debugging SMT solvers see our paper: 'Robert Brummayer and Armin Biere. Fuzzing and Delta-Debugging SMT Solvers', presented at SMT'09. DeltaSMT is released under GPL. A copy of the license can be found in the file COPYING. The delta-debugger is written in Java 5. My short introduction assumes that you work on a UNIX/LINUX system with Sun's JDK 5 or higher installed. However, it should be easy to follow the introductions and to use DeltaSMT 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 (supporting Java 5 or higher) 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 DeltaSMT and simply type 'ant' to build the delta-debugger. The parser of the delta-debugger is implemented as a recursive descent parser. In order to parse large formulas you have to increase the Java stack size. For UNIX/LINUX systems: I provide a wrapper shell script 'deltasmt' which sets the stack size via 'java -Xss128m' to 128 MB and calls the delta-debugger. 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': 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 'deltasmt'. If you just want to run the delta-debugger, skip the two steps above. I provide the examples ex1.smt to ex4.smt 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 the operator 'and' in the SMT formula, and zero otherwise. Try to call the delta-debugger as follows. I assume you are in the working directory of the deltasmt. ./deltasmt -v -v -v ./examples/ex1.smt ./reduced.smt ./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.smt' is the original SMT file. The argument './reduced.smt' 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.smt' as argument in order to compute the golden exit code which is 1 in this case. Then, the delta-debugger tries to minimize the formula. After each simplification step, the delta-debugger calls 'examples/run1.sh' with a simplified variant of the original formula. 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.smt', 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.smt' you do not have to wait until the delta-debugger has fully finished. However, I recommend you to wait unless the delta-debugger does not need hours. Typical delta-debugging sessions need only some 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=`~/deltasmt/solvers/solver1 $1` res2=`~/deltasmt/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 DeltaSMT'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 formula, 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 the formula 'false'. 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