Merging upstream version 1.71.1+dfsg1.

Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>

5 files changed, 709 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);
+}
diff --git a/vendor/varisat/src/prop/binary.rs b/vendor/varisat/src/prop/binary.rs
new file mode 100644
index 000000000..d89347c8a
--- /dev/null
+++ b/vendor/varisat/src/prop/binary.rs
@@ -0,0 +1,36 @@
+//! Propagation of binary clauses.
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+
+use crate::context::{parts::*, Context};
+
+use super::{enqueue_assignment, Conflict, Reason};
+
+/// Propagate all literals implied by the given literal via binary clauses.
+///
+/// On conflict return the binary clause propgating the conflicting assignment.
+pub fn propagate_binary(
+    mut ctx: partial!(
+        Context,
+        mut AssignmentP,
+        mut ImplGraphP,
+        mut TrailP,
+        BinaryClausesP,
+    ),
+    lit: Lit,
+) -> Result<(), Conflict> {
+    let (binary_clauses, mut ctx) = ctx.split_part(BinaryClausesP);
+
+    for &implied in binary_clauses.implied(lit) {
+        let assignment = ctx.part(AssignmentP);
+
+        if assignment.lit_is_false(implied) {
+            return Err(Conflict::Binary([implied, !lit]));
+        } else if !assignment.lit_is_true(implied) {
+            enqueue_assignment(ctx.borrow(), implied, Reason::Binary([!lit]));
+        }
+    }
+
+    Ok(())
+}
diff --git a/vendor/varisat/src/prop/graph.rs b/vendor/varisat/src/prop/graph.rs
new file mode 100644
index 000000000..3a0e3a42d
--- /dev/null
+++ b/vendor/varisat/src/prop/graph.rs
@@ -0,0 +1,137 @@
+//! The implication graph.
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::{lit::LitIdx, Lit, Var};
+
+use crate::{
+    clause::ClauseRef,
+    context::{parts::*, Context},
+};
+
+/// Assignments that caused a propagation.
+#[derive(Copy, Clone, Eq, PartialEq, Debug)]
+pub enum Reason {
+    Unit,
+    Binary([Lit; 1]),
+    Long(ClauseRef),
+}
+
+impl Reason {
+    /// The literals that caused the propagation.
+    pub fn lits<'out, 'a, 'b>(&'a self, ctx: &'b partial!('b Context, ClauseAllocP)) -> &'out [Lit]
+    where
+        'a: 'out,
+        'b: 'out,
+    {
+        match self {
+            Reason::Unit => &[],
+            Reason::Binary(lit) => lit,
+            // The propagated literal is always kept at position 0
+            Reason::Long(cref) => &ctx.part(ClauseAllocP).clause(*cref).lits()[1..],
+        }
+    }
+
+    /// True if a unit clause or assumption and not a propagation.
+    pub fn is_unit(&self) -> bool {
+        match self {
+            Reason::Unit => true,
+            _ => false,
+        }
+    }
+}
+
+/// Propagation that resulted in a conflict.
+#[derive(Copy, Clone, Eq, PartialEq, Debug)]
+pub enum Conflict {
+    Binary([Lit; 2]),
+    Long(ClauseRef),
+}
+
+impl Conflict {
+    /// The literals that caused the conflict.
+    pub fn lits<'out, 'a, 'b>(&'a self, ctx: &'b partial!('b Context, ClauseAllocP)) -> &'out [Lit]
+    where
+        'a: 'out,
+        'b: 'out,
+    {
+        match self {
+            Conflict::Binary(lits) => lits,
+            Conflict::Long(cref) => ctx.part(ClauseAllocP).clause(*cref).lits(),
+        }
+    }
+}
+
+/// Node and incoming edges of the implication graph.
+#[derive(Copy, Clone)]
+pub struct ImplNode {
+    pub reason: Reason,
+    pub level: LitIdx,
+    /// Position in trail when assigned, `LitIdx::max_value()` is used as sentinel for removed
+    /// units.
+    pub depth: LitIdx,
+}
+
+/// The implication graph.
+///
+/// This is a DAG having all assigned variables as nodes. It has unit clauses, assumptions and
+/// decisions as sources. For each propagated assignment it has incomming edges from the literals
+/// whose assignment caused the propagation to happen.
+#[derive(Default)]
+pub struct ImplGraph {
+    /// Contains only valid data for indices of assigned variables.
+    pub nodes: Vec<ImplNode>,
+}
+
+impl ImplGraph {
+    /// Update structures for a new variable count.
+    pub fn set_var_count(&mut self, count: usize) {
+        self.nodes.resize(
+            count,
+            ImplNode {
+                reason: Reason::Unit,
+                level: 0,
+                depth: 0,
+            },
+        );
+    }
+
+    /// Get the reason for an assigned variable.
+    ///
+    /// Returns stale data if the variable isn't assigned.
+    pub fn reason(&self, var: Var) -> &Reason {
+        &self.nodes[var.index()].reason
+    }
+
+    /// Get the decision level of an assigned variable.
+    ///
+    /// Returns stale data if the variable isn't assigned.
+    pub fn level(&self, var: Var) -> usize {
+        self.nodes[var.index()].level as usize
+    }
+
+    /// Get the trail depth of an assigned variable.
+    ///
+    /// Returns stale data if the variable isn't assigned.
+    pub fn depth(&self, var: Var) -> usize {
+        self.nodes[var.index()].depth as usize
+    }
+
+    /// Updates the reason for an assigned variable.
+    ///
+    /// Make sure the reason vars are in front of the assigned variable in the trail.
+    pub fn update_reason(&mut self, var: Var, reason: Reason) {
+        self.nodes[var.index()].reason = reason
+    }
+
+    /// Updates the reason and depth of a unit clause removed from the trail.
+    pub fn update_removed_unit(&mut self, var: Var) {
+        let node = &mut self.nodes[var.index()];
+        node.reason = Reason::Unit;
+        node.depth = LitIdx::max_value();
+    }
+
+    pub fn is_removed_unit(&self, var: Var) -> bool {
+        self.nodes[var.index()].depth == LitIdx::max_value()
+    }
+}
diff --git a/vendor/varisat/src/prop/long.rs b/vendor/varisat/src/prop/long.rs
new file mode 100644
index 000000000..8fde47ec7
--- /dev/null
+++ b/vendor/varisat/src/prop/long.rs
@@ -0,0 +1,164 @@
+//! Propagation of long clauses.
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+
+use crate::context::{parts::*, Context};
+
+use super::{assignment::fast_option_eq, enqueue_assignment, Conflict, Reason, Watch};
+
+/// Propagate all literals implied by long clauses watched by the given literal.
+///
+/// On conflict return the clause propgating the conflicting assignment.
+///
+/// See [`prop::watch`](crate::prop::watch) for the invariants that this has to uphold.
+pub fn propagate_long(
+    mut ctx: partial!(
+        Context,
+        mut AssignmentP,
+        mut ImplGraphP,
+        mut TrailP,
+        mut WatchlistsP,
+        mut ClauseAllocP,
+    ),
+    lit: Lit,
+) -> Result<(), Conflict> {
+    // The code below is heavily optimized and replaces a much nicer but sadly slower version.
+    // Nevertheless it still performs full bound checks. Therefore this function is safe to call
+    // even when some other code violated invariants of for example the clause db.
+    unsafe {
+        let (watchlists, mut ctx) = ctx.split_part_mut(WatchlistsP);
+        let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP);
+
+        let watch_begin;
+        let watch_end;
+        {
+            let watch_list = &mut watchlists.watched_by_mut(lit);
+            watch_begin = watch_list.as_mut_ptr();
+            watch_end = watch_begin.add(watch_list.len());
+        }
+        let mut watch_ptr = watch_begin;
+
+        let false_lit = !lit;
+
+        let mut watch_write = watch_ptr;
+
+        let assignment_limit = ctx.part(AssignmentP).assignment().len();
+        let assignment_ptr = ctx.part(AssignmentP).assignment().as_ptr();
+
+        let is_true = |lit: Lit| {
+            assert!(lit.index() < assignment_limit);
+            fast_option_eq(*assignment_ptr.add(lit.index()), Some(lit.is_positive()))
+        };
+
+        let is_false = |lit: Lit| {
+            assert!(lit.index() < assignment_limit);
+            fast_option_eq(*assignment_ptr.add(lit.index()), Some(lit.is_negative()))
+        };
+
+        'watchers: while watch_ptr != watch_end {
+            let watch = *watch_ptr;
+            watch_ptr = watch_ptr.add(1);
+
+            // If the blocking literal (which is part of the watched clause) is already true, the
+            // watched clause is satisfied and we don't even have to look at it.
+            if is_true(watch.blocking) {
+                *watch_write = watch;
+                watch_write = watch_write.add(1);
+                continue;
+            }
+
+            let cref = watch.cref;
+
+            // Make sure we can access at least 3 lits
+            alloc.check_bounds(cref, 3);
+
+            let clause_ptr = alloc.lits_ptr_mut_unchecked(cref);
+            let &mut header = alloc.header_unchecked_mut(cref);
+
+            // First we ensure that the literal we're currently propagating is at index 1. This
+            // prepares the literal order for further propagations, as the propagating literal has
+            // to be at index 0. Doing this here also avoids a similar check later should the clause
+            // be satisfied by a non-watched literal, as we can just move it to index 1.
+            let mut first = *clause_ptr.add(0);
+            if first == false_lit {
+                let c1 = *clause_ptr.add(1);
+                first = c1;
+                *clause_ptr.add(0) = c1;
+                *clause_ptr.add(1) = false_lit;
+            }
+
+            // We create a new watch with the other watched literal as blocking literal. This will
+            // either replace the currently processed watch or be added to another literals watch
+            // list.
+            let new_watch = Watch {
+                cref,
+                blocking: first,
+            };
+
+            // If the other watched literal (now the first) isn't the blocking literal, check
+            // whether that one is true. If so nothing else needs to be done.
+            if first != watch.blocking && is_true(first) {
+                *watch_write = new_watch;
+                watch_write = watch_write.add(1);
+                continue;
+            }
+
+            // At this point we try to find a non-false unwatched literal to replace our current
+            // literal as the watched literal.
+
+            let clause_len = header.len();
+            let mut lit_ptr = clause_ptr.add(2);
+            let lit_end = clause_ptr.add(clause_len);
+
+            // Make sure we can access all clause literals.
+            alloc.check_bounds(cref, clause_len);
+
+            while lit_ptr != lit_end {
+                let rest_lit = *lit_ptr;
+                if !is_false(rest_lit) {
+                    // We found a non-false literal and make it a watched literal by reordering the
+                    // literals and adding the watch to the corresponding watchlist.
+                    *clause_ptr.offset(1) = rest_lit;
+                    *lit_ptr = false_lit;
+
+                    // We're currently using unsafe to modify the watchlist of lit, so make extra
+                    // sure we're not aliasing.
+                    assert_ne!(!rest_lit, lit);
+                    watchlists.add_watch(!rest_lit, new_watch);
+                    continue 'watchers;
+                }
+                lit_ptr = lit_ptr.add(1);
+            }
+
+            // We didn't find a non-false unwatched literal, so either we're propagating or we have
+            // a conflict.
+            *watch_write = new_watch;
+            watch_write = watch_write.add(1);
+
+            // If the other watched literal is false we have a conflict.
+            if is_false(first) {
+                // We move all unprocessed watches and resize the currentl watchlist.
+                while watch_ptr != watch_end {
+                    *watch_write = *watch_ptr;
+                    watch_write = watch_write.add(1);
+                    watch_ptr = watch_ptr.add(1);
+                }
+                let out_size = ((watch_write as usize) - (watch_begin as usize))
+                    / std::mem::size_of::<Watch>();
+
+                watchlists.watched_by_mut(lit).truncate(out_size as usize);
+
+                return Err(Conflict::Long(cref));
+            }
+
+            // Otherwise we enqueue a new propagation.
+            enqueue_assignment(ctx.borrow(), first, Reason::Long(cref));
+        }
+
+        let out_size =
+            ((watch_write as usize) - (watch_begin as usize)) / std::mem::size_of::<Watch>();
+        watchlists.watched_by_mut(lit).truncate(out_size as usize);
+    }
+    Ok(())
+}
diff --git a/vendor/varisat/src/prop/watch.rs b/vendor/varisat/src/prop/watch.rs
new file mode 100644
index 000000000..095ac86a9
--- /dev/null
+++ b/vendor/varisat/src/prop/watch.rs
@@ -0,0 +1,135 @@
+//! Watchlists to detect clauses that became unit.
+//!
+//! Each (long) clause has always two watches pointing to it. The watches are kept in the watchlists
+//! of two different literals of the clause. Whenever the watches are moved to different literals
+//! the litereals of the clause are permuted so the watched literals are in position 0 and 1.
+//!
+//! When a clause is not unit under the current assignment, the watched literals point at two
+//! non-false literals. When a clause is unit and thus propagating, the true literal is watched and
+//! in position 0, the other watched literal is the one with the largest decision level and kept in
+//! position 1. When a clause becomes satisfied before becoming unit the watches can be kept as they
+//! were.
+//!
+//! When a literal is assigned false that invariant can be invalidated. This can be detected by
+//! scanning the watches of the assigned literal. When the assignment is processed the watches are
+//! moved to restore that invariant. Unless there is a conflict, i.e. a clause with no non-false
+//! literals, this can always be done. This also finds all clauses that became unit. The new unit
+//! clauses are exactly those clauses where no two non-false literals can be found.
+//!
+//! There is no need to update watchlists on backtracking, as unassigning variables cannot
+//! invalidate the invariant.
+//!
+//! See [Section 4.5.1 of the "Handbook of Satisfiability"][handbook-ch4] for more details and
+//! references.
+//!
+//! As a further optimization we use blocking literals. This means that each watch stores a literal
+//! of the clause that is different from the watched literal. It can be the other watched literal or
+//! any unwatched literal. When that literal is true, the clause is already satisfied, meaning that
+//! no watches need to be updated. This can be detected by just looking at the watch, avoiding
+//! access of the clause database. This variant was introduced by [Niklas Sörensson and Niklas Eén
+//! in "MINISAT 2.1 and MINISAT++1.0 — SAT Race 2008 Editions"][minisat-2.1].
+//!
+//! [handbook-ch4]: https://www.satassociation.org/articles/FAIA185-0131.pdf
+//! [minisat-2.1]: https://www.cril.univ-artois.fr/SAT09/solvers/booklet.pdf
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+
+use crate::{
+    clause::{db, ClauseRef},
+    context::{parts::*, Context},
+};
+
+/// A watch on a long clause.
+#[derive(Copy, Clone)]
+pub struct Watch {
+    /// Clause which has the referring lit in position 0 or 1.
+    pub cref: ClauseRef,
+    /// A lit of the clause, different from the referring lit.
+    pub blocking: Lit,
+}
+
+/// Watchlists to detect clauses that became unit.
+pub struct Watchlists {
+    /// Contains only valid data for indices of assigned variables.
+    watches: Vec<Vec<Watch>>,
+    /// Whether watchlists are present
+    enabled: bool,
+}
+
+impl Default for Watchlists {
+    fn default() -> Watchlists {
+        Watchlists {
+            watches: vec![],
+            enabled: true,
+        }
+    }
+}
+
+impl Watchlists {
+    /// Update structures for a new variable count.
+    pub fn set_var_count(&mut self, count: usize) {
+        self.watches.resize(count * 2, vec![]);
+    }
+
+    /// Start watching a clause.
+    ///
+    /// `lits` have to be the first two literals of the given clause.
+    pub fn watch_clause(&mut self, cref: ClauseRef, lits: [Lit; 2]) {
+        if !self.enabled {
+            return;
+        }
+
+        for i in 0..2 {
+            let watch = Watch {
+                cref,
+                blocking: lits[i ^ 1],
+            };
+            self.add_watch(!lits[i], watch);
+        }
+    }
+
+    /// Return watches for a given literal.
+    pub fn watched_by_mut(&mut self, lit: Lit) -> &mut Vec<Watch> {
+        &mut self.watches[lit.code()]
+    }
+
+    /// Make a literal watch a clause.
+    pub fn add_watch(&mut self, lit: Lit, watch: Watch) {
+        self.watches[lit.code()].push(watch)
+    }
+
+    /// Are watchlists enabled.
+    pub fn enabled(&self) -> bool {
+        self.enabled
+    }
+
+    /// Clear and disable watchlists.
+    ///
+    /// Actual clearing of the watchlists is done on re-enabling of the watchlists.
+    pub fn disable(&mut self) {
+        self.enabled = false;
+    }
+}
+
+/// Enable and rebuild watchlists.
+pub fn enable_watchlists(mut ctx: partial!(Context, mut WatchlistsP, ClauseAllocP, ClauseDbP)) {
+    let (watchlists, mut ctx) = ctx.split_part_mut(WatchlistsP);
+    if watchlists.enabled {
+        return;
+    }
+
+    for watchlist in watchlists.watches.iter_mut() {
+        watchlist.clear();
+    }
+
+    watchlists.enabled = true;
+
+    let (alloc, mut ctx) = ctx.split_part(ClauseAllocP);
+
+    for cref in db::clauses_iter(&ctx.borrow()) {
+        let lits = alloc.clause(cref).lits();
+        watchlists.watch_clause(cref, [lits[0], lits[1]]);
+    }
+}