From 9835e2ae736235810b4ea1c162ca5e65c547e770 Mon Sep 17 00:00:00 2001 From: Daniel Baumann Date: Sat, 18 May 2024 04:49:50 +0200 Subject: Merging upstream version 1.71.1+dfsg1. Signed-off-by: Daniel Baumann --- vendor/varisat/src/glue.rs | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 vendor/varisat/src/glue.rs (limited to 'vendor/varisat/src/glue.rs') diff --git a/vendor/varisat/src/glue.rs b/vendor/varisat/src/glue.rs new file mode 100644 index 000000000..2036cdd99 --- /dev/null +++ b/vendor/varisat/src/glue.rs @@ -0,0 +1,36 @@ +//! Compute glue levels of clauses. +//! +//! The glue level of a propagating clause is the number of distinct decision levels of the clause's +//! variables. This is also called the literal block distance (LBD). For each clause the smallest +//! glue level observed is used as an indicator of how useful that clause is. + +use partial_ref::{partial, PartialRef}; + +use varisat_formula::Lit; + +use crate::context::{parts::*, Context}; + +/// Compute the glue level of a clause. +pub fn compute_glue(mut ctx: partial!(Context, mut TmpFlagsP, ImplGraphP), lits: &[Lit]) -> usize { + let (tmp_flags, ctx) = ctx.split_part_mut(TmpFlagsP); + let impl_graph = ctx.part(ImplGraphP); + let flags = &mut tmp_flags.flags; + + let mut glue = 0; + + for &lit in lits { + let level = impl_graph.level(lit.var()); + let flag = &mut flags[level]; + if !*flag { + *flag = true; + glue += 1 + } + } + + for &lit in lits { + let level = impl_graph.level(lit.var()); + flags[level] = false; + } + + glue +} -- cgit v1.2.3