[−][src]Module splr::cdb

Crate cdb provides Clause object and its manager ClauseDB.

Structs

Clause	A representation of 'clause'
ClauseDB	Clause database
ClauseId	Clause identifier, or clause index, starting with one. Note: ids are re-used after 'garbage collection'.
Watch	'Watch literal' structure

Record of clause operations to build DRAT certifications.

ClauseDBIF	API for clause management like `check_and_reduce`, `new_clause`, `watcher_list`, and so on.
ClauseIF	API for Clause, providing literal accessors.
ClauseIdIF	API for Clause Id.
LBDIF	API to calculate LBD.
WatchDBIF	API for 'watcher list' like `register`, `detach`, `update_blocker` and so on.