Struct varisat_checker::clauses::Clause

pub struct Clause {
    pub id: u64,
    ref_count: [u32; 2],
    pub lits: ClauseLits,
}

Literals and metadata for non-unit clauses.

Fields

id: u64

LRAT clause id.

ref_count: [u32; 2]

How often the clause is present as irred., red. clause.

For checking the formula is a multiset of clauses. This is necessary as the generating solver might not check for duplicated clauses.

lits: ClauseLits

Clause's literals.