the construction process of solver->watches

[kblkzl]

Hello,

I am puzzled the construction process of the solver->watches data structure in the Kissat. I couldn't locate the corresponding part in the code. Could you please enlighten me on where construction is carried out?

Thank you for your.

Best regards,

kyrie.

[arminbiere]

So grepping for '(watches' gave the following:

compact.c: memset (solver->watches + 2 * vars, 0, 2 * reduced * sizeof (watches));
internal.c: DEALLOC_LITERAL_INDEXED (watches);
resize.c: CREALLOC_LITERAL_INDEXED (watches, watches);
resize.c: NREALLOC_LITERAL_INDEXED (watches, watches);

where watches are allocated and cleared (I removed two more lines).

The actual code is in 'watch.h' which is rather complex (uses union and
assumes a specific mapping to actual bytes - depending on little and
big endian). It is for sure one of the toughest parts of Kissat to understand
(engineered to improve on Lingeling by allowing simple iterators without
sacrifying performance and also keeping low memory usage).

You could check out 'test/testreferences.c' for some unit tests
(executed by ./build/tissat or make test).

Alternatively you could try read up on watches in satch or tabularasat.
Their code has more comments, easier to get into and tabularasat is actually
even considered slightly improved compared in this regard
(the arena for keeping watcher stacks is better).

[kblkzl]

Thank you so much for taking the time answer my question,I look forward to learning more from you the future!