[−][src]Module rate_common::clause

Data structures for the checker

Structs

Clause	An index uniquely identifying a clause or lemma during the lifetime of the program
GRATLiteral	A literal for the GRAT proof output
LRATDependency	An intermediate representation of an LRAT hint
LRATLiteral	A literal in the LRAT proof output
ProofStep	A clause introduction or deletion
Reason	The reason for assigning a literal
Tagged32	Value with 30 bit payload with 2 flag bits
TaggedUSize	Value with `size_of::<usize>() - 2` bits of payload and 2 flag bits

The redundancy property to use for inference checks.

Write a clause-like data type in DIMACS format.

The type that backs Clause.