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/prop/assignment.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/prop/assignment.rs')
-rw-r--r-- | vendor/varisat/src/prop/assignment.rs | 237 |
1 files changed, 237 insertions, 0 deletions
diff --git a/vendor/varisat/src/prop/assignment.rs b/vendor/varisat/src/prop/assignment.rs new file mode 100644 index 000000000..a87f60485 --- /dev/null +++ b/vendor/varisat/src/prop/assignment.rs @@ -0,0 +1,237 @@ +//! Partial assignment and backtracking. +use partial_ref::{partial, PartialRef}; + +use varisat_formula::{lit::LitIdx, Lit, Var}; + +use crate::{ + context::{parts::*, Context}, + decision::make_available, +}; + +use super::Reason; + +/// Current partial assignment. +#[derive(Default)] +pub struct Assignment { + assignment: Vec<Option<bool>>, + last_value: Vec<bool>, +} + +/// This compares two `Option<bool>` values as bytes. Workaround for bad code generation. +pub fn fast_option_eq(a: Option<bool>, b: Option<bool>) -> bool { + unsafe { std::mem::transmute::<_, u8>(a) == std::mem::transmute::<_, u8>(b) } +} + +impl Assignment { + /// Update structures for a new variable count. + pub fn set_var_count(&mut self, count: usize) { + self.assignment.resize(count, None); + self.last_value.resize(count, false); + } + + /// Current partial assignment as slice. + pub fn assignment(&self) -> &[Option<bool>] { + &self.assignment + } + + /// Value assigned to a variable. + pub fn var_value(&self, var: Var) -> Option<bool> { + self.assignment[var.index()] + } + + /// Value last assigned to a variable. + /// + /// If the variable is currently assigned this returns the previously assigned value. If the + /// variable was never assigned this returns false. + pub fn last_var_value(&self, var: Var) -> bool { + self.last_value[var.index()] + } + + /// Value assigned to a literal. + pub fn lit_value(&self, lit: Lit) -> Option<bool> { + self.assignment[lit.index()].map(|b| b ^ lit.is_negative()) + } + + pub fn lit_is_true(&self, lit: Lit) -> bool { + fast_option_eq(self.assignment[lit.index()], Some(lit.is_positive())) + } + + pub fn lit_is_false(&self, lit: Lit) -> bool { + fast_option_eq(self.assignment[lit.index()], Some(lit.is_negative())) + } + + pub fn lit_is_unk(&self, lit: Lit) -> bool { + fast_option_eq(self.assignment[lit.index()], None) + } + + pub fn assign_lit(&mut self, lit: Lit) { + self.assignment[lit.index()] = lit.is_positive().into() + } + + pub fn unassign_var(&mut self, var: Var) { + self.assignment[var.index()] = None; + } + + /// Set the assigned/unassigned value of a variable. + pub fn set_var(&mut self, var: Var, assignment: Option<bool>) { + self.assignment[var.index()] = assignment; + } +} + +/// Decision and propagation history. +#[derive(Default)] +pub struct Trail { + /// Stack of all propagated and all enqueued assignments + trail: Vec<Lit>, + /// Next assignment in trail to propagate + queue_head_pos: usize, + /// Decision levels as trail indices. + decisions: Vec<LitIdx>, + /// Number of unit clauses removed from the trail. + units_removed: usize, +} + +impl Trail { + /// Return the next assigned literal to propagate. + pub fn queue_head(&self) -> Option<Lit> { + self.trail.get(self.queue_head_pos).cloned() + } + + /// Return the next assigned literal to propagate and remove it from the queue. + pub fn pop_queue(&mut self) -> Option<Lit> { + let head = self.queue_head(); + if head.is_some() { + self.queue_head_pos += 1; + } + head + } + + /// Re-enqueue all assigned literals. + pub fn reset_queue(&mut self) { + self.queue_head_pos = 0; + } + + /// Assigned literals in assignment order. + pub fn trail(&self) -> &[Lit] { + &self.trail + } + + /// Clear the trail. + /// + /// This simply removes all entries without performing any backtracking. Can only be called with + /// no active decisions. + pub fn clear(&mut self) { + assert!(self.decisions.is_empty()); + self.units_removed += self.trail.len(); + self.trail.clear(); + self.queue_head_pos = 0; + } + + /// Start a new decision level. + /// + /// Does not enqueue the decision itself. + pub fn new_decision_level(&mut self) { + self.decisions.push(self.trail.len() as LitIdx) + } + + /// Current decision level. + pub fn current_level(&self) -> usize { + self.decisions.len() + } + + /// The number of assignments at level 0. + pub fn top_level_assignment_count(&self) -> usize { + self.decisions + .get(0) + .map(|&len| len as usize) + .unwrap_or(self.trail.len()) + + self.units_removed + } + + /// Whether all assignments are processed. + pub fn fully_propagated(&self) -> bool { + self.queue_head_pos == self.trail.len() + } +} + +/// Enqueues the assignment of true to a literal. +/// +/// This updates the assignment and trail, but does not perform any propagation. The literal has to +/// be unassigned when calling this. +pub fn enqueue_assignment( + mut ctx: partial!(Context, mut AssignmentP, mut ImplGraphP, mut TrailP), + lit: Lit, + reason: Reason, +) { + let assignment = ctx.part_mut(AssignmentP); + debug_assert!(assignment.lit_value(lit) == None); + + assignment.assign_lit(lit); + + let (trail, mut ctx) = ctx.split_part_mut(TrailP); + + trail.trail.push(lit); + + let node = &mut ctx.part_mut(ImplGraphP).nodes[lit.index()]; + node.reason = reason; + node.level = trail.decisions.len() as LitIdx; + node.depth = trail.trail.len() as LitIdx; +} + +/// Undo all assignments in decision levels deeper than the given level. +pub fn backtrack( + mut ctx: partial!(Context, mut AssignmentP, mut TrailP, mut VsidsP), + level: usize, +) { + let (assignment, mut ctx) = ctx.split_part_mut(AssignmentP); + let (trail, mut ctx) = ctx.split_part_mut(TrailP); + + // level can actually be greater than the current level. This happens when restart is called + // after a conflict backtracked into the assumptions, but before any assumption was reenqueued. + // TODO should we update assumption_levels on backtracking instead of allowing this here? + if level >= trail.decisions.len() { + return; + } + + let new_trail_len = trail.decisions[level] as usize; + + trail.queue_head_pos = new_trail_len; + trail.decisions.truncate(level); + + let trail_end = &trail.trail[new_trail_len..]; + for &lit in trail_end { + make_available(ctx.borrow(), lit.var()); + let var_assignment = &mut assignment.assignment[lit.index()]; + assignment.last_value[lit.index()] = *var_assignment == Some(true); + *var_assignment = None; + } + trail.trail.truncate(new_trail_len); +} + +/// Undo all decisions and assumptions. +pub fn full_restart( + mut ctx: partial!( + Context, + mut AssignmentP, + mut AssumptionsP, + mut TrailP, + mut VsidsP, + ), +) { + ctx.part_mut(AssumptionsP).full_restart(); + backtrack(ctx.borrow(), 0); +} + +/// Undo all decisions. +pub fn restart( + mut ctx: partial!( + Context, + mut AssignmentP, + mut TrailP, + mut VsidsP, + AssumptionsP + ), +) { + let level = ctx.part(AssumptionsP).assumption_levels(); + backtrack(ctx.borrow(), level); +} |