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-checker/src/hash.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-checker/src/hash.rs')
-rw-r--r-- | vendor/varisat-checker/src/hash.rs | 74 |
1 files changed, 74 insertions, 0 deletions
diff --git a/vendor/varisat-checker/src/hash.rs b/vendor/varisat-checker/src/hash.rs new file mode 100644 index 000000000..40474ff8e --- /dev/null +++ b/vendor/varisat-checker/src/hash.rs @@ -0,0 +1,74 @@ +//! Computation of clause hashes. +use std::mem::take; + +use partial_ref::{partial, PartialRef}; +use rustc_hash::FxHashMap as HashMap; + +use varisat_formula::{Lit, Var}; +use varisat_internal_proof::{lit_code_hash, lit_hash, ClauseHash}; + +use crate::context::{parts::*, Context}; + +pub struct ClauseHasher { + /// How many bits are used for storing clause hashes. + pub hash_bits: u32, + /// Changed solver names that are not yet reflected in the checkers current clause hashes. + pub buffered_solver_var_names: Vec<(Var, Option<Var>)>, + /// Does buffered_solver_var_names contain a new name? + /// + /// If it contains only deletes, there is no need to rehash + pub rename_in_buffered_solver_var_names: bool, + /// Current mapping from global var names to solver var names, used for hashing. + solver_var_names: HashMap<Var, Var>, +} + +impl Default for ClauseHasher { + fn default() -> ClauseHasher { + ClauseHasher { + hash_bits: 64, + buffered_solver_var_names: vec![], + rename_in_buffered_solver_var_names: false, + solver_var_names: Default::default(), + } + } +} + +impl ClauseHasher { + /// Compute a clause hash of the current bit size + pub fn clause_hash(&self, lits: &[Lit]) -> ClauseHash { + let shift_bits = ClauseHash::max_value().count_ones() - self.hash_bits; + let mut hash = 0; + for &lit in lits.iter() { + match self.solver_var_names.get(&lit.var()) { + Some(var) => hash ^= lit_hash(var.lit(lit.is_positive())), + None => hash ^= lit_code_hash(lit.code() + Var::max_count() * 2), + } + } + hash >> shift_bits + } +} + +/// Recompute all clause hashes if necessary +pub fn rehash(mut ctx: partial!(Context, mut ClauseHasherP, mut ClausesP)) { + let (hasher, mut ctx) = ctx.split_part_mut(ClauseHasherP); + let clauses = ctx.part_mut(ClausesP); + + for (global, solver) in hasher.buffered_solver_var_names.drain(..) { + if let Some(solver) = solver { + hasher.solver_var_names.insert(global, solver); + } else { + hasher.solver_var_names.remove(&global); + } + } + hasher.rename_in_buffered_solver_var_names = false; + + let mut old_clauses = take(&mut clauses.clauses); + + for (_, mut candidates) in old_clauses.drain() { + for clause in candidates.drain(..) { + let hash = hasher.clause_hash(clause.lits.slice(&clauses.literal_buffer)); + let candidates = clauses.clauses.entry(hash).or_default(); + candidates.push(clause); + } + } +} |