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
+}