[][src]Function varisat_checker::rup::check_clause_with_hashes

pub fn check_clause_with_hashes<'a>(
    ctx: Const<CheckerStateP, Mut<VariablesP, Mut<RupCheckP, Mut<ProcessingP<'a>, Mut<ClausesP, Mut<ClauseHasherP, Ref<Context<'a>>>>>>>>,
    lits: &[Lit],
    propagation_hashes: &[ClauseHash]
) -> Result<(), CheckerError>

Check whether a clause is implied by clauses of the given hashes.

lits must be sorted and free of duplicates.