use partial_ref::{partial, PartialRef};
use varisat_formula::Lit;
use crate::{
clause::{db, ClauseRef},
context::{parts::*, Context},
glue::compute_glue,
};
use super::{bump_clause_activity, ClauseHeader, Tier};
pub fn assess_learned_clause(
mut ctx: partial!(Context, mut TmpFlagsP, ImplGraphP),
lits: &[Lit],
) -> ClauseHeader {
let glue = compute_glue(ctx.borrow(), lits) - 1;
let mut header = ClauseHeader::new();
header.set_glue(glue);
header.set_tier(select_tier(glue));
header
}
fn select_tier(glue: usize) -> Tier {
if glue <= 2 {
Tier::Core
} else if glue <= 6 {
Tier::Mid
} else {
Tier::Local
}
}
pub fn bump_clause(
mut ctx: partial!(
Context,
mut ClauseActivityP,
mut ClauseAllocP,
mut ClauseDbP,
mut TmpFlagsP,
ImplGraphP
),
cref: ClauseRef,
) {
bump_clause_activity(ctx.borrow(), cref);
let (alloc, mut ctx_2) = ctx.split_part_mut(ClauseAllocP);
let clause = alloc.clause_mut(cref);
let glue = compute_glue(ctx_2.borrow(), clause.lits());
clause.header_mut().set_active(true);
if glue < clause.header().glue() {
clause.header_mut().set_glue(glue);
db::set_clause_tier(ctx.borrow(), cref, select_tier(glue));
}
}