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