1 files changed, 100 insertions, 0 deletions
diff --git a/vendor/varisat/src/binary.rs b/vendor/varisat/src/binary.rs
new file mode 100644
index 000000000..f39d04676
--- /dev/null
+++ b/vendor/varisat/src/binary.rs
@@ -0,0 +1,100 @@
+//! Binary clauses.
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+use varisat_internal_proof::{DeleteClauseProof, ProofStep};
+
+use crate::{
+    context::{parts::*, Context},
+    proof,
+};
+
+/// Binary clauses.
+#[derive(Default)]
+pub struct BinaryClauses {
+    by_lit: Vec<Vec<Lit>>,
+    count: usize,
+}
+
+impl BinaryClauses {
+    /// Update structures for a new variable count.
+    pub fn set_var_count(&mut self, count: usize) {
+        self.by_lit.resize(count * 2, vec![]);
+    }
+
+    /// Add a binary clause.
+    pub fn add_binary_clause(&mut self, lits: [Lit; 2]) {
+        for i in 0..2 {
+            self.by_lit[(!lits[i]).code()].push(lits[i ^ 1]);
+        }
+        self.count += 1;
+    }
+
+    /// Implications of a given literal
+    pub fn implied(&self, lit: Lit) -> &[Lit] {
+        &self.by_lit[lit.code()]
+    }
+
+    /// Number of binary clauses.
+    pub fn count(&self) -> usize {
+        self.count
+    }
+}
+
+/// Remove binary clauses that have an assigned literal.
+pub fn simplify_binary<'a>(
+    mut ctx: partial!(Context<'a>, mut BinaryClausesP, mut ProofP<'a>, mut SolverStateP, AssignmentP, VariablesP),
+) {
+    let (binary_clauses, mut ctx) = ctx.split_part_mut(BinaryClausesP);
+    let (assignment, mut ctx) = ctx.split_part(AssignmentP);
+
+    let mut double_count = 0;
+
+    for (code, implied) in binary_clauses.by_lit.iter_mut().enumerate() {
+        let lit = Lit::from_code(code);
+
+        if !assignment.lit_is_unk(lit) {
+            if ctx.part(ProofP).is_active() {
+                for &other_lit in implied.iter() {
+                    // This check avoids deleting binary clauses twice if both literals are assigned.
+                    if (!lit) < other_lit {
+                        let lits = [!lit, other_lit];
+                        proof::add_step(
+                            ctx.borrow(),
+                            true,
+                            &ProofStep::DeleteClause {
+                                clause: &lits[..],
+                                proof: DeleteClauseProof::Satisfied,
+                            },
+                        );
+                    }
+                }
+            }
+
+            implied.clear();
+        } else {
+            implied.retain(|&other_lit| {
+                let retain = assignment.lit_is_unk(other_lit);
+                // This check avoids deleting binary clauses twice if both literals are assigned.
+                if ctx.part(ProofP).is_active() && !retain && (!lit) < other_lit {
+                    let lits = [!lit, other_lit];
+                    proof::add_step(
+                        ctx.borrow(),
+                        true,
+                        &ProofStep::DeleteClause {
+                            clause: &lits[..],
+                            proof: DeleteClauseProof::Satisfied,
+                        },
+                    );
+                }
+
+                retain
+            });
+
+            double_count += implied.len();
+        }
+    }
+
+    binary_clauses.count = double_count / 2;
+}