SAT Debugging

Fixing stateless code

Comments are moderated. It may take a few minutes before your comment appears.
Markdown is supported in your comments.

Pure declarative programs are generally very weird to debug. They don't have instructions, so there is nothing to step through. They don't have state, so there is no memory to examine. The solving engine for a declarative program (in our case, Minisat) will have instructions and state, but a highly optimized backend works with an intermediate form that is many steps removed from the input program.

Mail: (not shown)

Please type this: