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
|
//! Clause activity.
use partial_ref::{partial, PartialRef};
use crate::{
config::SolverConfig,
context::{parts::*, Context},
};
use super::ClauseRef;
/// Clause activity.
///
/// The individual clause activities are stored in the clause allocator. This stores global metadata
/// used for bumping and decaying activities.
pub struct ClauseActivity {
/// The value to add on bumping.
bump: f32,
/// The inverse of the decay factor.
inv_decay: f32,
}
impl Default for ClauseActivity {
fn default() -> ClauseActivity {
ClauseActivity {
bump: 1.0,
inv_decay: 1.0 / SolverConfig::default().clause_activity_decay,
}
}
}
impl ClauseActivity {
/// Change the decay factor.
pub fn set_decay(&mut self, decay: f32) {
assert!(decay < 1.0);
assert!(decay > 1.0 / 16.0);
self.inv_decay = 1.0 / decay;
}
}
/// Rescale activities if any value exceeds this value.
fn rescale_limit() -> f32 {
std::f32::MAX / 16.0
}
/// Increase a clause's activity.
pub fn bump_clause_activity(
mut ctx: partial!(
Context,
mut ClauseActivityP,
mut ClauseAllocP,
mut ClauseDbP,
),
cref: ClauseRef,
) {
let bump = ctx.part(ClauseActivityP).bump;
let header = ctx.part_mut(ClauseAllocP).header_mut(cref);
let activity = header.activity() + bump;
header.set_activity(activity);
if activity > rescale_limit() {
rescale_clause_activities(ctx.borrow());
}
}
/// Rescale all values to avoid an overflow.
fn rescale_clause_activities(
mut ctx: partial!(
Context,
mut ClauseActivityP,
mut ClauseAllocP,
mut ClauseDbP,
),
) {
let rescale_factor = 1.0 / rescale_limit();
let (db, mut ctx) = ctx.split_part_mut(ClauseDbP);
let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP);
db.clauses.retain(|&cref| {
let header = alloc.header_mut(cref);
if header.deleted() {
false
} else {
let activity = header.activity() * rescale_factor;
header.set_activity(activity);
true
}
});
ctx.part_mut(ClauseActivityP).bump *= rescale_factor;
}
/// Decay the clause activities.
pub fn decay_clause_activities(
mut ctx: partial!(
Context,
mut ClauseActivityP,
mut ClauseAllocP,
mut ClauseDbP,
),
) {
let activities = ctx.part_mut(ClauseActivityP);
activities.bump *= activities.inv_decay;
if activities.bump >= rescale_limit() {
rescale_clause_activities(ctx.borrow());
}
}
|
