[−][src]Function varisat_checker::clauses::delete_clause
pub fn delete_clause(
ctx: Const<ClauseHasherP, Const<CheckerStateP, Mut<VariablesP, Mut<ClausesP, Ref<Context>>>>>,
lits: &[Lit],
redundant: bool
) -> Result<(u64, DeleteClauseResult), CheckerError>
Delete a clause from the current formula.
lits
must be sorted and free of duplicates.
Returns the id of the deleted clause and whether the ref_count (or irredundant ref_count) became zero.