[−][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.

puts_clause	Write the some literals in DIMACS format to stdout.
puts_clause_with_id	Write the clause ID and literals to stdout, like [<ID] 0.
puts_clause_with_id_and_witness	Write the clause ID, literals and a witness to stdout, like [<ID] 0.
write_clause	Write some literals in DIMACS format.

The type that backs Clause.