varisat/clause/
reduce.rs

1//! Clause database reduction.
2use std::mem::replace;
3
4use ordered_float::OrderedFloat;
5use vec_mut_scan::VecMutScan;
6
7use partial_ref::{partial, PartialRef};
8
9use varisat_internal_proof::{DeleteClauseProof, ProofStep};
10
11use crate::{
12    context::{parts::*, Context},
13    proof,
14};
15
16use super::db::{set_clause_tier, try_delete_clause, Tier};
17
18/// Remove deleted and duplicate entries from the by_tier clause lists.
19///
20/// This has the side effect of setting the mark bit on all clauses of the tier.
21pub fn dedup_and_mark_by_tier(
22    mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP),
23    tier: Tier,
24) {
25    let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP);
26    let by_tier = &mut ctx.part_mut(ClauseDbP).by_tier[tier as usize];
27
28    by_tier.retain(|&cref| {
29        let header = alloc.header_mut(cref);
30        let retain = !header.deleted() && !header.mark() && header.tier() == tier;
31        if retain {
32            header.set_mark(true);
33        }
34        retain
35    })
36}
37
38/// Reduce the number of local tier clauses by deleting half of them.
39pub fn reduce_locals<'a>(
40    mut ctx: partial!(
41        Context<'a>,
42        mut ClauseAllocP,
43        mut ClauseDbP,
44        mut ProofP<'a>,
45        mut SolverStateP,
46        mut WatchlistsP,
47        AssignmentP,
48        ImplGraphP,
49        VariablesP,
50    ),
51) {
52    dedup_and_mark_by_tier(ctx.borrow(), Tier::Local);
53
54    let mut locals = replace(
55        &mut ctx.part_mut(ClauseDbP).by_tier[Tier::Local as usize],
56        vec![],
57    );
58
59    locals.sort_unstable_by_key(|&cref| {
60        (
61            OrderedFloat(ctx.part(ClauseAllocP).header(cref).activity()),
62            cref,
63        )
64    });
65
66    let mut to_delete = locals.len() / 2;
67
68    let mut scan = VecMutScan::new(&mut locals);
69
70    if to_delete > 0 {
71        while let Some(cref) = scan.next() {
72            ctx.part_mut(ClauseAllocP).header_mut(*cref).set_mark(false);
73
74            if try_delete_clause(ctx.borrow(), *cref) {
75                if ctx.part(ProofP).is_active() {
76                    let (alloc, mut ctx) = ctx.split_part(ClauseAllocP);
77                    let lits = alloc.clause(*cref).lits();
78                    proof::add_step(
79                        ctx.borrow(),
80                        true,
81                        &ProofStep::DeleteClause {
82                            clause: lits,
83                            proof: DeleteClauseProof::Redundant,
84                        },
85                    );
86                }
87
88                cref.remove();
89                to_delete -= 1;
90                if to_delete == 0 {
91                    break;
92                }
93            }
94        }
95    }
96
97    // Make sure to clear all marks
98    while let Some(cref) = scan.next() {
99        ctx.part_mut(ClauseAllocP).header_mut(*cref).set_mark(false);
100    }
101
102    drop(scan);
103
104    ctx.part_mut(ClauseDbP).count_by_tier[Tier::Local as usize] = locals.len();
105    ctx.part_mut(ClauseDbP).by_tier[Tier::Local as usize] = locals;
106}
107
108/// Reduce the number of mid tier clauses by moving inactive ones to the local tier.
109pub fn reduce_mids(mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP)) {
110    dedup_and_mark_by_tier(ctx.borrow(), Tier::Mid);
111
112    let mut mids = replace(
113        &mut ctx.part_mut(ClauseDbP).by_tier[Tier::Mid as usize],
114        vec![],
115    );
116
117    mids.retain(|&cref| {
118        let header = ctx.part_mut(ClauseAllocP).header_mut(cref);
119        header.set_mark(false);
120
121        if header.active() {
122            header.set_active(false);
123            true
124        } else {
125            set_clause_tier(ctx.borrow(), cref, Tier::Local);
126            false
127        }
128    });
129
130    ctx.part_mut(ClauseDbP).count_by_tier[Tier::Mid as usize] = mids.len();
131    ctx.part_mut(ClauseDbP).by_tier[Tier::Mid as usize] = mids;
132}
varisat/clause/reduce.rs

varisat/clause/
reduce.rs
