Module batsat::clause

source ·

Modules

Generic interface for objects printable in DIMACS

Structs

Main clause allocator. It stores a set of clauses efficiently.
Metadata of a clause
Packs together an occurrence list and the filtering predicate
List of occurrences of objects of type K (e.g. literals) in values of type V (e.g. clauses)
A ternary boolean (true, false, undefined) used for partial assignments.

Traits

Anything that can be considered as a list of literals.
Predicate that decides whether a value V is deleted or not

Type Definitions