1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130

//! 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};
use crate::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;
}