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