diff options
author | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-05-18 02:49:50 +0000 |
---|---|---|
committer | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-05-18 02:49:50 +0000 |
commit | 9835e2ae736235810b4ea1c162ca5e65c547e770 (patch) | |
tree | 3fcebf40ed70e581d776a8a4c65923e8ec20e026 /vendor/varisat/src/clause/activity.rs | |
parent | Releasing progress-linux version 1.70.0+dfsg2-1~progress7.99u1. (diff) | |
download | rustc-9835e2ae736235810b4ea1c162ca5e65c547e770.tar.xz rustc-9835e2ae736235810b4ea1c162ca5e65c547e770.zip |
Merging upstream version 1.71.1+dfsg1.
Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>
Diffstat (limited to 'vendor/varisat/src/clause/activity.rs')
-rw-r--r-- | vendor/varisat/src/clause/activity.rs | 107 |
1 files changed, 107 insertions, 0 deletions
diff --git a/vendor/varisat/src/clause/activity.rs b/vendor/varisat/src/clause/activity.rs new file mode 100644 index 000000000..8404c7e75 --- /dev/null +++ b/vendor/varisat/src/clause/activity.rs @@ -0,0 +1,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()); + } +} |