1 files changed, 135 insertions, 0 deletions
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 Sörensson and Niklas Eé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]]);
+    }
+}