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

//! Scheduling of processing and solving steps.
//!
//! The current implementation is temporary and will be replaced with something more flexible.
use log::info;

use partial_ref::{partial, PartialRef};

use crate::cdcl::conflict_step;
use crate::clause::reduce::{reduce_locals, reduce_mids};
use crate::clause::{collect_garbage, Tier};
use crate::context::{parts::*, Context};
use crate::prop::restart;
use crate::state::SatState;

mod luby;

use luby::LubySequence;

/// Scheduling of processing and solving steps.
#[derive(Default)]
pub struct Schedule {
    conflicts: u64,
    next_restart: u64,
    restarts: u64,
    luby: LubySequence,
}

/// Perform one step of the schedule.
pub fn schedule_step<'a>(
    mut ctx: partial!(
        Context<'a>,
        mut AnalyzeConflictP,
        mut AssignmentP,
        mut AssumptionsP,
        mut BinaryClausesP,
        mut ClauseActivityP,
        mut ClauseAllocP,
        mut ClauseDbP,
        mut ImplGraphP,
        mut ModelP,
        mut ProofP<'a>,
        mut ScheduleP,
        mut SolverStateP,
        mut TmpDataP,
        mut TmpFlagsP,
        mut TrailP,
        mut VariablesP,
        mut VsidsP,
        mut WatchlistsP,
        SolverConfigP,
    ),
) -> bool {
    let (schedule, mut ctx) = ctx.split_part_mut(ScheduleP);
    let (config, mut ctx) = ctx.split_part(SolverConfigP);

    if ctx.part(SolverStateP).sat_state != SatState::Unknown {
        false
    } else if ctx.part(SolverStateP).solver_error.is_some() {
        false
    } else {
        if schedule.conflicts > 0 && schedule.conflicts % 5000 == 0 {
            let db = ctx.part(ClauseDbP);
            let units = ctx.part(TrailP).top_level_assignment_count();
            info!(
                "confl: {}k rest: {} vars: {} bin: {} irred: {} core: {} mid: {} local: {}",
                schedule.conflicts / 1000,
                schedule.restarts,
                ctx.part(AssignmentP).assignment().len() - units,
                ctx.part(BinaryClausesP).count(),
                db.count_by_tier(Tier::Irred),
                db.count_by_tier(Tier::Core),
                db.count_by_tier(Tier::Mid),
                db.count_by_tier(Tier::Local)
            );
        }

        if schedule.next_restart == schedule.conflicts {
            restart(ctx.borrow());
            schedule.restarts += 1;
            schedule.next_restart += config.luby_restart_interval_scale * schedule.luby.advance();
        }

        if schedule.conflicts % config.reduce_locals_interval == 0 {
            reduce_locals(ctx.borrow());
        }
        if schedule.conflicts % config.reduce_mids_interval == 0 {
            reduce_mids(ctx.borrow());
        }

        collect_garbage(ctx.borrow());

        conflict_step(ctx.borrow());
        schedule.conflicts += 1;
        true
    }
}