1 files changed, 132 insertions, 0 deletions
diff --git a/vendor/varisat/src/clause/reduce.rs b/vendor/varisat/src/clause/reduce.rs
new file mode 100644
index 000000000..1252ca50b
--- /dev/null
+++ b/vendor/varisat/src/clause/reduce.rs
@@ -0,0 +1,132 @@
+//! Clause database reduction.
+use std::mem::replace;
+
+use ordered_float::OrderedFloat;
+use vec_mut_scan::VecMutScan;
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_internal_proof::{DeleteClauseProof, ProofStep};
+
+use crate::{
+    context::{parts::*, Context},
+    proof,
+};
+
+use super::db::{set_clause_tier, try_delete_clause, Tier};
+
+/// Remove deleted and duplicate entries from the by_tier clause lists.
+///
+/// This has the side effect of setting the mark bit on all clauses of the tier.
+pub fn dedup_and_mark_by_tier(
+    mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP),
+    tier: Tier,
+) {
+    let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP);
+    let by_tier = &mut ctx.part_mut(ClauseDbP).by_tier[tier as usize];
+
+    by_tier.retain(|&cref| {
+        let header = alloc.header_mut(cref);
+        let retain = !header.deleted() && !header.mark() && header.tier() == tier;
+        if retain {
+            header.set_mark(true);
+        }
+        retain
+    })
+}
+
+/// Reduce the number of local tier clauses by deleting half of them.
+pub fn reduce_locals<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut ClauseAllocP,
+        mut ClauseDbP,
+        mut ProofP<'a>,
+        mut SolverStateP,
+        mut WatchlistsP,
+        AssignmentP,
+        ImplGraphP,
+        VariablesP,
+    ),
+) {
+    dedup_and_mark_by_tier(ctx.borrow(), Tier::Local);
+
+    let mut locals = replace(
+        &mut ctx.part_mut(ClauseDbP).by_tier[Tier::Local as usize],
+        vec![],
+    );
+
+    locals.sort_unstable_by_key(|&cref| {
+        (
+            OrderedFloat(ctx.part(ClauseAllocP).header(cref).activity()),
+            cref,
+        )
+    });
+
+    let mut to_delete = locals.len() / 2;
+
+    let mut scan = VecMutScan::new(&mut locals);
+
+    if to_delete > 0 {
+        while let Some(cref) = scan.next() {
+            ctx.part_mut(ClauseAllocP).header_mut(*cref).set_mark(false);
+
+            if try_delete_clause(ctx.borrow(), *cref) {
+                if ctx.part(ProofP).is_active() {
+                    let (alloc, mut ctx) = ctx.split_part(ClauseAllocP);
+                    let lits = alloc.clause(*cref).lits();
+                    proof::add_step(
+                        ctx.borrow(),
+                        true,
+                        &ProofStep::DeleteClause {
+                            clause: lits,
+                            proof: DeleteClauseProof::Redundant,
+                        },
+                    );
+                }
+
+                cref.remove();
+                to_delete -= 1;
+                if to_delete == 0 {
+                    break;
+                }
+            }
+        }
+    }
+
+    // Make sure to clear all marks
+    while let Some(cref) = scan.next() {
+        ctx.part_mut(ClauseAllocP).header_mut(*cref).set_mark(false);
+    }
+
+    drop(scan);
+
+    ctx.part_mut(ClauseDbP).count_by_tier[Tier::Local as usize] = locals.len();
+    ctx.part_mut(ClauseDbP).by_tier[Tier::Local as usize] = locals;
+}
+
+/// Reduce the number of mid tier clauses by moving inactive ones to the local tier.
+pub fn reduce_mids(mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP)) {
+    dedup_and_mark_by_tier(ctx.borrow(), Tier::Mid);
+
+    let mut mids = replace(
+        &mut ctx.part_mut(ClauseDbP).by_tier[Tier::Mid as usize],
+        vec![],
+    );
+
+    mids.retain(|&cref| {
+        let header = ctx.part_mut(ClauseAllocP).header_mut(cref);
+        header.set_mark(false);
+
+        if header.active() {
+            header.set_active(false);
+            true
+        } else {
+            set_clause_tier(ctx.borrow(), cref, Tier::Local);
+            false
+        }
+    });
+
+    ctx.part_mut(ClauseDbP).count_by_tier[Tier::Mid as usize] = mids.len();
+    ctx.part_mut(ClauseDbP).by_tier[Tier::Mid as usize] = mids;
+}