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
|
//! 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,
clause::{
collect_garbage,
reduce::{reduce_locals, reduce_mids},
Tier,
},
context::{parts::*, Context},
prop::restart,
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
|| 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
}
}
|
