pyDelta: delta debugging for SMT-LIBΒΆ

pyDelta is a delta debugger for SMT-LIB files. It is heavily inspired by other similar tools like ddSMT, DeltaSMT or delta. pyDelta is based on a few fundamental ideas:

  • parse generic S-expressions. This is very robust against changes to SMT-LIB or solver specific extensions. It also allows for a small parser and simple node structure. Most semantic information that is required for simplification can be recovered cheaply.
  • parallel execution. Running multiple checks in parallel allows for significant speedups when minimizing faulty inputs.
  • easy to extend. It should be fairly easy to add new simplifications by implementing new mutators.
  • fixed-point iteration. Simplifications are applied until no simplificationss are possible anywhere. Rerunning pyDelta on a minimized input should not yield further improvements.
  • flexible to use. The options should cover most use cases, including checking for the exit code or checking for specific patterns in the (regular or error) output.