[][src]Function varisat_checker::clauses::store_clause

pub fn store_clause(
    ctx: Const<ClauseHasherP, Mut<VariablesP, Mut<ClausesP, Mut<CheckerStateP, Ref<Context>>>>>,
    lits: &[Lit],
    redundant: bool
) -> (u64, StoreClauseResult)

Adds a clause to the checker data structures.

lits must be sorted and free of duplicates.

Returns the id of the added clause and indicates whether the clause is new or changed from redundant to irredundant.