From f22734d5e4b2423f13b53d8fbff5fd93f72c1344 Mon Sep 17 00:00:00 2001 From: Alexandre Dubray Date: Tue, 31 Oct 2023 07:18:34 +0100 Subject: [PATCH] Add comments on new files --- README.md | 36 ++++++++++++++++++----- src/core/clause.rs | 55 ++++++++++++++++++++++++++++------- src/core/components.rs | 7 +++-- src/core/distribution.rs | 29 +++++++++++++------ src/core/flags.rs | 15 ++++++++++ src/core/graph.rs | 4 +-- src/core/literal.rs | 15 ++++++++++ src/core/variable.rs | 59 +++++++++++++++++++++----------------- src/core/watched_vector.rs | 26 +++++++++++++++++ src/propagator.rs | 4 +-- 10 files changed, 192 insertions(+), 58 deletions(-) diff --git a/README.md b/README.md index c6a234b..f354219 100644 --- a/README.md +++ b/README.md @@ -9,10 +9,7 @@ Schlandals is a projected weighted model counter which targets inference in prob Current known probability queries that can be solved with the solver include - Computing the probability of some target variables (given some evidences) in a Bayesian network - Computing the probability that two nodes are connected in a probabilistic graph - -The solver currently supports two types of solving - - Search based solving with a DPLL-style backtracing search - - Compiling into (or read from a file) an arithmetic circuit with distributions as leaf + - A mapping from [ProbLog](https://github.com/ML-KULeuven/problog) programs to Schlandals # Problem specification @@ -28,9 +25,9 @@ Schlandals takes as input a file using a modified version of the [DIMACS](https: c Lines starting with `c` alone are comments. c The first line must be the head in the form of "p cnf p cnf 16 11 -c Following the header, must be the definition of the distributions. Note that the lines starts with "c p distribution" which is similar to how weights are encoded in DIMACS (c p weight). -c /!\ The definition of the distribution MUST be before the clauses and induce an implicit numbering on the variable. Below, the first distribution will have -c variable with index 1 and 2. The second has the variables with index 3 and 4, etc. +c The distribution are defined by lines starting with "c p distribution" +c Each value in a distribution is assigned to a variable, starting from 1. Hence, the first N variables +c are used for the distributions. c p distribution 0.2 0.8 c p distribution 0.3 0.7 c p distribution 0.4 0.6 @@ -84,3 +81,28 @@ The circuit can be stored in the file given by the `fdac` argument and a DOT vis ### Reading a compiled file A previously compiled file can be read using `schlandals read-compiled -i [--dotfile . +//! Representation of a clause in Schlandals. All clauses used in Schlandals are Horn clause, which +//! means that they have at most one positive literal, the head of the clause. +//! The literals of the clause (head included) are stored in a vector that implements the 2-watch literals +//! method. +//! However, the specific needs of Schlandals for the propagation impose that each clause is watched by two pairs +//! of watched literals. +//! One pair is composed of deterministic literals, and the other of probabilistic ones. +//! In this way the propagator can, at any time, query a boud on the number of unfixed deterministic/probabilistic +//! variables in the clause. + use search_trail::StateManager; use super::graph::ClauseIndex; use super::sparse_set::SparseSet; @@ -24,6 +34,7 @@ use super::graph::{DistributionIndex, VariableIndex, Graph}; #[derive(Debug)] pub struct Clause { + /// id of the clause in the input problem id: usize, /// If the clause is not learned, this is the literal which is the head of the clause. Otherwise, None head: Option, @@ -35,6 +46,7 @@ pub struct Clause { pub parents: SparseSet, /// Random bitstring used for hash computation hash: u64, + /// Has the clause been learned during the search is_learned: bool, } @@ -52,42 +64,58 @@ impl Clause { } } + /// Adds a child to the current clause. The child clause has the head of the current clause + /// as a negative literals in it. pub fn add_child(&mut self, child: ClauseIndex, state: &mut StateManager) { self.children.add(child, state); } + /// Adds a parent to the current clause. The parent clause has its head as a negative literal + /// in the current clause. pub fn add_parent(&mut self, parent: ClauseIndex, state: &mut StateManager) { self.parents.add(parent, state); } + /// Remove a child from the children of this clause. Not that this operation is reverted when + /// the state manager restore the state pub fn remove_child(&mut self, child: ClauseIndex, state: &mut StateManager) { self.children.remove(child, state); } + /// Remove a parent from the parents of this clause. Not that this operation is reverted when + /// the state manager restore the state pub fn remove_parent(&mut self, parent: ClauseIndex, state: &mut StateManager) { self.parents.remove(parent, state); } + /// Returns a bound on the number ofdeterministic (first element) and probabilistic (second element) + /// unfixed variable in the clause pub fn get_bounds_watcher(&self, state: &StateManager) -> (usize, usize) { self.literals.get_bounds(state) } + /// Returns true if the clause still has unfixed probabilistic variables in it pub fn has_probabilistic(&self, state: &StateManager) -> bool { self.literals.get_alive_end_watcher(state).is_some() } + /// Set the clause as unconstrained. This operation is reverted when the state manager restore its state. pub fn set_unconstrained(&self, state: &mut StateManager) { self.literals.set_unconstrained(state); } + /// Returns true iff the clause is constrained pub fn is_constrained(&self, state: &StateManager) -> bool { self.literals.is_constrained(state) } + /// Returns the hash of the clause pub fn hash(&self) -> u64 { self.hash } + /// If the clause still has unfixed probabilisitc variables, return the distribution of the first watcher. + /// Else, return None. pub fn get_constrained_distribution(&self, state: &StateManager, g: &Graph) -> Option { match self.literals.get_alive_end_watcher(state) { None => None, @@ -95,26 +123,32 @@ impl Clause { } } + /// Returns the number of parents of the clause in the initial problem pub fn number_parents(&self) -> usize { self.parents.capacity() } + /// Returns the number of children of the clause in the initial problem pub fn number_children(&self) -> usize { self.children.capacity() } + /// Returns the number of constrained parent of the clause pub fn number_constrained_parents(&self, state: &StateManager) -> usize { self.parents.len(state) } + /// Returns the number of constrained children of the clause pub fn number_constrained_children(&self, state: &StateManager) -> usize { self.children.len(state) } + /// Return the head of the clause pub fn head(&self) -> Option { self.head } + /// Returns true iff the variable is the head of the clause pub fn is_head(&self, variable: VariableIndex) -> bool { match self.head { None => false, @@ -122,6 +156,7 @@ impl Clause { } } + /// Notify the clause that the given variable has taken the given value. Updates the watchers accordingly. pub fn notify_variable_value(&mut self, variable: VariableIndex, value: bool, probabilistic: bool, state: &mut StateManager) -> VariableIndex { if !probabilistic { self.literals.update_watcher_start(variable, value, state) @@ -130,6 +165,7 @@ impl Clause { } } + /// Returns true iff the clause is unit pub fn is_unit(&self, state: &StateManager) -> bool { if !self.is_constrained(state) { return false; @@ -138,6 +174,7 @@ impl Clause { bounds.0 + bounds.1 == 1 } + /// Returns the last unfixed literal in the unit clause pub fn get_unit_assigment(&self, state: &StateManager) -> Literal { debug_assert!(self.is_unit(state)); let bounds = self.literals.get_bounds(state); @@ -148,16 +185,7 @@ impl Clause { } } - pub fn has_probabilistic_in_body(&self, state: &StateManager) -> bool { - let bound_probabilistic = self.literals.get_bounds(state).1; - for i in 0..bound_probabilistic { - if !self.literals[self.literals.limit() + i].is_positive() { - return true; - } - } - return false; - } - + /// Returns true iff the clause stil has unfixed deterministic variables in its body pub fn has_deterministic_in_body(&self, state: &StateManager) -> bool { let bound_deterministic = self.literals.get_bounds(state).0; for i in 0..bound_deterministic { @@ -168,34 +196,41 @@ impl Clause { return false; } + /// Returns true iff the clause is learned pub fn is_learned(&self) -> bool { self.is_learned } // --- ITERATORRS --- // + /// Returns an iterator on the (constrained) parents of the clause pub fn iter_parents(&self, state: &StateManager) -> impl Iterator + '_ { self.parents.iter(state) } + /// Returns an iterator on the (constrained) children of the clause pub fn iter_children(&self, state: &StateManager) -> impl Iterator + '_ { self.children.iter(state) } + /// Returns an interator on the literals of the clause pub fn iter(&self) -> impl Iterator + '_ { self.literals.iter() } + /// Returns an iterator on the variables represented by the literals of the clause pub fn iter_variables(&self) -> impl Iterator + '_ { self.literals.iter().map(|l| l.to_variable()) } + /// Returns an iterator on the probabilistic varaibles in the clause pub fn iter_probabilistic_variables(&self) -> impl Iterator + '_ { self.literals.iter_end().map(|l| l.to_variable()) } } +// Writes a clause as C{id}: l1 l2 ... ln impl std::fmt::Display for Clause { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { diff --git a/src/core/components.rs b/src/core/components.rs index da9e091..322c715 100644 --- a/src/core/components.rs +++ b/src/core/components.rs @@ -150,6 +150,7 @@ impl ComponentExtractor { g[clause].is_constrained(state) && !(comp_start <= clause_pos && clause_pos < (comp_start + *comp_size)) } + /// Returns true if the distribution has not yet been visited during the component exploration fn is_distribution_visitable(&self, distribution: DistributionIndex, distribution_start: usize, distribution_size: &usize) -> bool { let distribution_pos = self.distribution_positions[distribution.0]; !(distribution_start <= distribution_pos && distribution_pos < (distribution_start + *distribution_size)) @@ -210,10 +211,10 @@ impl ComponentExtractor { *comp_number_distribution += 1; for v in g[distribution].iter_variables() { if !g[v].is_fixed(state) { - for c in g[v].iter_clause_negative_occurence() { + for c in g[v].iter_clauses_negative_occurence() { self.explore_component(g, c, comp_start, comp_size, comp_distribution_start, comp_number_distribution, hash, state); } - for c in g[v].iter_clause_positive_occurence() { + for c in g[v].iter_clauses_positive_occurence() { self.explore_component(g, c, comp_start, comp_size, comp_distribution_start, comp_number_distribution, hash, state); } } @@ -325,6 +326,8 @@ impl ComponentExtractor { self.distributions[start..end].iter().copied() } + /// Adds a clause to a component. This function is called when the solver encounters an UNSAT and needs to learn a clause. + /// During this process we ensure that the learned clause is horn and can be safely added in the component for further detections. pub fn add_clause_to_component(&mut self, component: ComponentIndex, clause: ClauseIndex) { debug_assert!(clause.0 == self.clause_positions.len()); let start = self.components[component.0].start; diff --git a/src/core/distribution.rs b/src/core/distribution.rs index ea3bb0b..e24d6d0 100644 --- a/src/core/distribution.rs +++ b/src/core/distribution.rs @@ -14,20 +14,19 @@ //You should have received a copy of the GNU Affero General Public License //along with this program. If not, see . +//! This module provide the implementation of a distribution in Schlandals. +//! A distribution is a set of variable that respects the following constraints: +//! 1. Every variable must have a weight +//! 2. The sum of the variables' weight must sum to 1 +//! 3. In each model of the input formula, exactly one of the variables is set to true + use super::graph::VariableIndex; use search_trail::{StateManager, ReversibleUsize, UsizeManager}; -/// Represents a set of variable in a same distribution. This assume that the variable of a distribution -/// are inserted in the graph one after the other (i.e. that their `VariableIndex` are consecutive). -/// Since no variable should be removed from the graph once constructed, this should not be a problem. -/// Thus a distribution is identified by the first `VariableIndex` and the number of variable in it. -/// -/// We also store the number of clauses in which the distribution appears. This is usefull to compute -/// the unconstrained probability during the propagation. -/// In the same manner, the number of variable assigned to false in the distribution is kept, allowing us -/// to efficiently detect that only one variable remains in a distribution. +/// A distribution of the input problem #[derive(Debug, Clone, Copy, PartialEq)] pub struct Distribution { + /// Id of the distribution in the problem id: usize, /// First variable in the distribution pub first: VariableIndex, @@ -35,6 +34,7 @@ pub struct Distribution { pub size: usize, /// Number of constrained clauses in which the distribution appears pub number_clause_unconstrained: ReversibleUsize, + /// Number of clauses in which the distribution appears number_clause: usize, /// Number of variables assigned to F in the distribution pub number_false: ReversibleUsize, @@ -53,32 +53,43 @@ impl Distribution { } } + /// Increments the number of clauses in which the distribution appears pub fn increment_clause(&mut self) { self.number_clause += 1; } + /// Decrements the number of constrained clause in which the distribution appears. This + /// operation is reversed when the trail restore its state. + /// Returns the remaining number of constrained clauses in which it appears. pub fn decrement_constrained(&self, state: &mut StateManager) -> usize { self.number_clause - state.increment_usize(self.number_clause_unconstrained) } + /// Icrements the number of variable assigned to false in the distribution. This operation + /// is reversed when the trail restore its state. pub fn increment_number_false(&self, state: &mut StateManager) -> usize { state.increment_usize(self.number_false) } + /// Returns the number of unfixed variables in the distribution. This assume that the distribution + /// has no variable set to true (otherwise there is no need to consider it). pub fn number_unfixed(&self, state: &StateManager) -> usize { self.size - state.get_usize(self.number_false) } + /// Returns the number of variable set to false in the distribution. pub fn number_false(&self, state: &StateManager) -> usize { state.get_usize(self.number_false) } + /// Returns the start of the distribution in the vector of variables in the graph. pub fn start(&self) -> VariableIndex { self.first } // --- ITERATOR --- // + /// Returns an iterator on the variables of the distribution pub fn iter_variables(&self) -> impl Iterator { (self.first.0..(self.first.0 + self.size)).map(VariableIndex) } diff --git a/src/core/flags.rs b/src/core/flags.rs index 70e9980..15b7b75 100644 --- a/src/core/flags.rs +++ b/src/core/flags.rs @@ -14,10 +14,19 @@ //You should have received a copy of the GNU Affero General Public License //along with this program. If not, see . +///! This modules provide flags for the clauses and the literals. They are used during the propagation to set +/// various information + + // Inspired from @xgillard rsolve (https://www.github.com/xgillard/rsolve) + +/// Flags that a clause can take pub enum ClauseFlag { + /// No flags Clear = 0, + /// The clause is reachable from a clause whose implicant might be true TrueReachable = 1, + /// The clause is reachable from a clause whose consequence might be false FalseReachable = 2, } @@ -57,11 +66,17 @@ impl ClauseFlags { } } +/// Flags that a literal can take pub enum LitFlag { + /// No flags Clear = 0, + /// The literal has been marked during the clause learning procedure IsMarked = 1, + /// The literal has been analyzed as implied in the learned clause IsImplied = 2, + /// The literal has been analyzed as not implied in the learned clause IsNotImplied = 4, + /// The literal is in the conflict clause IsInConflictClause = 8, } diff --git a/src/core/graph.rs b/src/core/graph.rs index e39ec85..f422e84 100644 --- a/src/core/graph.rs +++ b/src/core/graph.rs @@ -190,7 +190,7 @@ impl Graph { if literal.is_positive() { self[variable].add_clause_positive_occurence(cid); if !is_learned { - for child in self[variable].iter_clause_negative_occurence().collect::>() { + for child in self[variable].iter_clauses_negative_occurence().collect::>() { clause.add_child(child, state); self[child].add_parent(cid, state); } @@ -198,7 +198,7 @@ impl Graph { } else { self[variable].add_clause_negative_occurence(cid); if !is_learned { - for parent in self[variable].iter_clause_positive_occurence().collect::>() { + for parent in self[variable].iter_clauses_positive_occurence().collect::>() { clause.add_parent(parent, state); self[parent].add_child(cid, state); } diff --git a/src/core/literal.rs b/src/core/literal.rs index e574fe8..26f1ad6 100644 --- a/src/core/literal.rs +++ b/src/core/literal.rs @@ -14,6 +14,14 @@ //You should have received a copy of the GNU Affero General Public License //along with this program. If not, see . +//! An implementation of a literal in Schlandals. That is, a variable an a +//! polarity. This is represented by a signed integer. +//! In addition to the variable and its polarity (the isize), each literal has the +//! reversible boolean representing the fact that the associated variable is fixed or +//! not. +//! This is done so that each literal can query on its own the state of its associated variable +//! (bypassing problems with the borrow checker). + use super::graph::VariableIndex; use search_trail::{StateManager, OptionBoolManager, ReversibleOptionBool}; @@ -22,18 +30,22 @@ pub struct Literal(isize, ReversibleOptionBool); impl Literal { + /// Returns true iff the literal has a positive polarity pub fn is_positive(&self) -> bool { self.0 > 0 } + /// Returns the varaible represented by the literal pub fn to_variable(&self) -> VariableIndex { VariableIndex(self.0.abs() as usize - 1) } + /// Returns a literal from its string representation pub fn from_str(value: &str, fixed: ReversibleOptionBool) -> Self { Literal(value.parse::().unwrap(), fixed) } + /// Returns the literal representing the variable with the given polarity pub fn from_variable(variable: VariableIndex, polarity: bool, fixed: ReversibleOptionBool) -> Self { if polarity { Literal(variable.0 as isize + 1, fixed) @@ -42,10 +54,13 @@ impl Literal { } } + /// Returns the opposite of the current literal. That is, a literal representing the same + /// variable but with opposite polarity pub fn opposite(&self) -> Literal { Literal(-self.0, self.1) } + /// Returns true iff the associated variable is fixed pub fn is_variable_fixed(&self, state: &StateManager) -> bool { state.get_option_bool(self.1).is_some() } diff --git a/src/core/variable.rs b/src/core/variable.rs index 56d0d39..00b21f3 100644 --- a/src/core/variable.rs +++ b/src/core/variable.rs @@ -14,6 +14,9 @@ //You should have received a copy of the GNU Affero General Public License //along with this program. If not, see . +//! An implementation of a variable in Schlandals. A variable is the core unit +//! for reasoning in schlandals as they define the distributions. + use search_trail::*; use crate::core::graph::{ClauseIndex, DistributionIndex}; @@ -26,12 +29,11 @@ pub enum Reason { /// Data structure that actually holds the data of a variable of the input problem #[derive(Debug)] pub struct Variable { + /// The id of the variable in the input problem id: usize, - /// If `probabilistic` is `true`, then this is the weight associated to the variable. Otherwise, - /// this is None. + /// The weight of the variable. None if the variable is deterministic weight: Option, - /// If `probabilistic` is `true`, this is the index of the distribution containing this node. Otherwise, - /// this is None. + /// The distribution in which the variable is. None if the variable is deterministic distribution: Option, /// The clauses in which the variable appears with positive polarity clauses_positive: Vec, @@ -41,13 +43,14 @@ pub struct Variable { value: ReversibleOptionBool, /// Level at which the decision was made for this variable decision: isize, + /// Index in the assignment stack at which the decision has been made for the variable assignment_position: ReversibleUsize, /// The clause that set the variable, if any reason: Option, + /// True if the variable has been implied during BUP is_implied: ReversibleBool, /// Random u64 associated to the variable, used for hash computation hash: u64, - marked: bool, } impl Variable { @@ -65,70 +68,80 @@ impl Variable { reason: None, is_implied: state.manage_bool(false), hash: rand::random(), - marked: false, } } + /// Sets the weight of the variable to the given value pub fn set_weight(&mut self, weight: f64) { self.weight = Some(weight); } + /// Set the distribution of the variable to the given distribution pub fn set_distribution(&mut self, distribution: DistributionIndex) { self.distribution = Some(distribution); } + /// Returns the distribution of the variable pub fn distribution(&self) -> Option { self.distribution } + /// Returns true iff the variable is probabilistic pub fn is_probabilitic(&self) -> bool { self.weight.is_some() } + /// Returns the weight of the variable pub fn weight(&self) -> Option { self.weight } + /// Sets the variable to the given value. This operation is reverted when + /// the trail is restored pub fn set_value(&self, value: bool, state: &mut StateManager) { state.set_option_bool(self.value, value); } + /// Returns the value of the variable pub fn value(&self, state: &StateManager) -> Option { state.get_option_bool(self.value) } + /// Returns the reversible boolean representing the value assignment + /// of the variable pub fn get_value_index(&self) -> ReversibleOptionBool { self.value } + /// Returns true iff the variable is fixed pub fn is_fixed(&self, state: &StateManager) -> bool { state.get_option_bool(self.value).is_some() } + /// Adds the clause in the positive occurence list pub fn add_clause_positive_occurence(&mut self, clause: ClauseIndex) { self.clauses_positive.push(clause); } + /// Adds the clause in the negative occurence list pub fn add_clause_negative_occurence(&mut self, clause: ClauseIndex) { self.clauses_negative.push(clause); } - pub fn iter_clause_positive_occurence(&self) -> impl Iterator + '_ { - self.clauses_positive.iter().copied() - } - - pub fn iter_clause_negative_occurence(&self) -> impl Iterator + '_ { - self.clauses_negative.iter().copied() - } - + /// Sets the decision level for the variable to the given level pub fn set_decision_level(&mut self, level: isize) { self.decision = level } + /// Returns the decision level for the variable. This function assume that the query is done + /// only on fixed variable since the level is not reversible. Since this function is used in + /// clause learning, it should always be the case pub fn decision_level(&self) -> isize { self.decision } + /// Sets the reason of the variable. The reason is either a clause or a distribution which forced, + /// during boolean unit propagation, the variable to take a given value. pub fn set_reason(&mut self, reason: Option, state: &mut StateManager) { if reason.is_some() { state.set_bool(self.is_implied, true); @@ -138,6 +151,7 @@ impl Variable { self.reason = reason; } + /// Returns the reason, if any, of the variable. pub fn reason(&self, state: &StateManager) -> Option { if !state.get_bool(self.is_implied) { None @@ -146,36 +160,29 @@ impl Variable { } } + /// Returns the hash of the variable pub fn hash(&self) -> u64 { self.hash } - pub fn is_marked(&self) -> bool { - self.marked - } - - pub fn mark(&mut self) { - self.marked = true; - } - - pub fn unmark(&mut self) { - self.marked = false; - } - + /// Sets the assignment position (in the assignment stack) of the variable to the given value pub fn set_assignment_position(&self, position: usize, state: &mut StateManager) { state.set_usize(self.assignment_position, position); } + /// Returns the assignment position (in the assignment stack) of the variable pub fn get_assignment_position(&self, state: &StateManager) -> usize { state.get_usize(self.assignment_position) } // --- ITERATOR --- // + /// Returns an iterator on the clauses in which the variable appears with a positive polarity pub fn iter_clauses_positive_occurence(&self) -> impl Iterator + '_ { self.clauses_positive.iter().copied() } + /// Returns an iterator on the clauses in which the variable appears with a negative polarity pub fn iter_clauses_negative_occurence(&self) -> impl Iterator + '_ { self.clauses_negative.iter().copied() } diff --git a/src/core/watched_vector.rs b/src/core/watched_vector.rs index 0df3f50..20ee8bb 100644 --- a/src/core/watched_vector.rs +++ b/src/core/watched_vector.rs @@ -14,14 +14,27 @@ //You should have received a copy of the GNU Affero General Public License //along with this program. If not, see . +//! Implementation of a two-literal based watch vector. This vector differ from classical watched vector +//! in the following way. +//! Traditionnal two-watch literal implementaiton imposes that each clause is watched by two of its literals. +//! However, in order to do its additional propagation, Schlandals needs to know when a clause has deterministic +//! variable in its body. +//! Hence, the variable in the vector are sorted by type. First, the deterministic variable and after the probabilistic +//! variables. They are stored in the same vector, but are considered as two separated watched vector. +//! This means that the vector is watched by four literals. +//! The operations are done in a manner such that the first two literals are always wathing the vector + use search_trail::{StateManager, BoolManager, ReversibleBool}; use super::literal::Literal; use super::graph::VariableIndex; #[derive(Debug)] pub struct WatchedVector { + /// The literals in the clause that owns the vector literals: Vec, + /// The index the the first probabilistic literal in the clause limit: usize, + /// Is the clause constrained constrained: ReversibleBool, } @@ -36,24 +49,30 @@ impl WatchedVector { vector } + /// Returns the number of literals in the vector pub fn len(&self) -> usize { self.literals.len() } + /// Returns the number of unfixed deterministic/probabilistic watchers for this vector pub fn get_bounds(&self, state: &StateManager) -> (usize, usize) { let bound_deterministic = (0..self.limit.min(2)).filter(|i| !self.literals[*i].is_variable_fixed(state)).count(); let bound_probabilistic = (self.limit..(self.limit + 2).min(self.literals.len())).filter(|i| !self.literals[*i].is_variable_fixed(state)).count(); (bound_deterministic, bound_probabilistic) } + /// Returns true iff the clause that owns the vector is constrained pub fn is_constrained(&self, state: &StateManager) -> bool { state.get_bool(self.constrained) } + /// Set the vector (and the clause that owns it) as unconstrained pub fn set_unconstrained(&self, state: &mut StateManager) { state.set_bool(self.constrained, false); } + /// Update, if possible, the watcher that is not alive anymore and returns the variable that is the new watcher. + /// If the watcher was not updated, return watcher. fn update_watcher(&mut self, watcher: VariableIndex, value: bool, start: usize, end: usize, bound: usize, state: &mut StateManager) -> VariableIndex { let id = if self.literals[start].to_variable() == watcher { start } else { (start + 1).min(end - 1)}; if (self.literals[id].is_positive() && value) || (!self.literals[id].is_positive() && !value) { @@ -78,16 +97,20 @@ impl WatchedVector { } } + /// Updates the deterministic watchers pub fn update_watcher_start(&mut self, watcher: VariableIndex, value: bool, state: &mut StateManager) -> VariableIndex { let (bound, _) = self.get_bounds(state); self.update_watcher(watcher, value, 0, self.limit, bound, state) } + /// Updates the probabilistic watchers pub fn update_watcher_end(&mut self, watcher: VariableIndex, value: bool, state: &mut StateManager) -> VariableIndex { let (_, bound) = self.get_bounds(state); self.update_watcher(watcher, value, self.limit, self.literals.len(), bound, state) } + /// If there exists an unassigned probabilistic variable in the vector, returns it (This is equivalent to looking + /// at the watchers). pub fn get_alive_end_watcher(&self, state: &StateManager) -> Option { if self.limit >= self.literals.len() { return None; @@ -99,16 +122,19 @@ impl WatchedVector { } } + /// Returns the index of the first probabilistic variable in the clause. pub fn limit(&self) -> usize { self.limit } // --- ITERATOR --- // + /// Returns an interator on the variable in the vector pub fn iter(&self) -> impl Iterator + '_ { self.literals.iter().copied() } + /// Returns an iterator on the probabilistic variables in the vector pub fn iter_end(&self) -> impl Iterator + '_ { self.literals.iter().skip(self.limit).copied() } diff --git a/src/propagator.rs b/src/propagator.rs index 79f7bf1..f854f44 100644 --- a/src/propagator.rs +++ b/src/propagator.rs @@ -226,11 +226,11 @@ impl Propagator { g.set_variable(variable, value, level, reason, state); if value { - for clause in g[variable].iter_clause_positive_occurence() { + for clause in g[variable].iter_clauses_positive_occurence() { g[clause].set_unconstrained(state); } } else { - for clause in g[variable].iter_clause_negative_occurence() { + for clause in g[variable].iter_clauses_negative_occurence() { g[clause].set_unconstrained(state); } }