diff options
author | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-05-18 02:49:50 +0000 |
---|---|---|
committer | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-05-18 02:49:50 +0000 |
commit | 9835e2ae736235810b4ea1c162ca5e65c547e770 (patch) | |
tree | 3fcebf40ed70e581d776a8a4c65923e8ec20e026 /vendor/varisat/src/glue.rs | |
parent | Releasing progress-linux version 1.70.0+dfsg2-1~progress7.99u1. (diff) | |
download | rustc-9835e2ae736235810b4ea1c162ca5e65c547e770.tar.xz rustc-9835e2ae736235810b4ea1c162ca5e65c547e770.zip |
Merging upstream version 1.71.1+dfsg1.
Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>
Diffstat (limited to 'vendor/varisat/src/glue.rs')
-rw-r--r-- | vendor/varisat/src/glue.rs | 36 |
1 files changed, 36 insertions, 0 deletions
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 +} |