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