slightly underdocumented

[DvonHolten]

i read the source-code from allocate.c to witness.h - i found just one line of comment - a copyright notice.
is that going to change - maybe after the competition?

[arminbiere]

Unlikely for those data-structures and algorithms which are similar to Kissat/CaDiCaL/Satch. For those you should read the source code of CaDiCaL and Satch in parallel. I might add some more comments to the Gimsatul specific parts, particularly related to sharing clauses etc. However, note that I do have extensive logging which I consider as executable, active comments (which can also crash BTW). I even consider reading those logging messages (with '-l') and of course before the verbose messages (with '-v -v -v') in the source code and during runs as even more instructive than any comments.

[arminbiere]

I started some documentation and as promised first for the most important data-structures and algorithms used in propagate.c which are also slightly different than in other solvers (have another indirection).