Alternate equality logic theory solver.

.gitignore

@@ -12,3 +12,4 @@ aries_fzn/share/aries_fzn
 __pycache__/
 *.profraw
 lcov.info
+profile.json.gz

solver/src/collections/ref_store.rs

@@ -399,6 +399,9 @@ impl<K, V> Default for RefMap<K, V> {
 impl<K: Ref, V> RefMap<K, V> {
     pub fn insert(&mut self, k: K, v: V) {
         let index = k.into();
+        if index > self.entries.len() {
+            self.entries.reserve_exact(index - self.entries.len());
+        }
         while self.entries.len() <= index {
             self.entries.push(None);
         }
@@ -442,7 +445,8 @@ impl<K: Ref, V> RefMap<K, V> {
         if index >= self.entries.len() {
             None
         } else {
-            self.entries[index].as_ref()
+            let res: &Option<V> = &self.entries[index];
+            res.as_ref()
         }
     }
 
@@ -451,9 +455,13 @@ impl<K: Ref, V> RefMap<K, V> {
         if index >= self.entries.len() {
             None
         } else {
-            self.entries[index].as_mut()
+            let res: &mut Option<V> = &mut self.entries[index];
+            res.as_mut()
         }
     }
+
+    // pub fn get_many_mut_or_insert<const N: usize>(&mut self, ks: [K; N], default: impl Fn() -> V) -> [&mut V; N] {}
+
     pub fn get_or_insert(&mut self, k: K, default: impl FnOnce() -> V) -> &V {
         if !self.contains(k) {
             self.insert(k, default())
@@ -562,6 +570,11 @@ impl<K: Ref, V> IterableRefMap<K, V> {
         self.map.insert(k, v)
     }
 
+    pub fn remove(&mut self, k: K) {
+        self.map.remove(k);
+        self.keys.retain(|e| *e != k);
+    }
+
     /// Removes all elements from the Map.
     #[inline(never)]
     pub fn clear(&mut self) {

solver/src/collections/set.rs

@@ -61,6 +61,16 @@ impl<K: Ref> Default for RefSet<K> {
     }
 }
 
+impl<K: Ref> FromIterator<K> for IterableRefSet<K> {
+    fn from_iter<T: IntoIterator<Item = K>>(iter: T) -> Self {
+        let mut set = Self::new();
+        for i in iter {
+            set.insert(i);
+        }
+        set
+    }
+}
+
 /// A set of values that can be converted into small unsigned integers.
 /// This extends `RefSet` with a vector of all elements of the set, allowing for fast iteration
 /// and clearing.
@@ -89,6 +99,10 @@ impl<K: Ref> IterableRefSet<K> {
         self.set.insert(k, ());
     }
 
+    pub fn remove(&mut self, k: K) {
+        self.set.remove(k);
+    }
+
     pub fn clear(&mut self) {
         self.set.clear()
     }

solver/src/core/state/domain.rs

@@ -1,5 +1,5 @@
 use crate::{
-    core::{cst_int_to_long, IntCst, LongCst, INT_CST_MAX, INT_CST_MIN},
+    core::{cst_int_to_long, IntCst, Lit, LongCst, INT_CST_MAX, INT_CST_MIN},
     model::lang::Rational,
 };
 use std::fmt::{Display, Formatter};
@@ -53,6 +53,11 @@ impl IntDomain {
     pub fn disjoint(&self, other: &IntDomain) -> bool {
         self.ub < other.lb || other.ub < self.lb
     }
+
+    pub fn entails(&self, literal: Lit) -> bool {
+        literal.svar().is_plus() && literal.variable().leq(self.ub).entails(literal)
+            || literal.svar().is_minus() && literal.variable().geq(self.lb).entails(literal)
+    }
 }
 
 impl std::ops::Mul for IntDomain {

solver/src/core/state/domains.rs

@@ -187,6 +187,15 @@ impl Domains {
         self.lb(var) >= self.ub(var)
     }
 
+    pub fn get_bound(&self, var: VarRef) -> Option<IntCst> {
+        let (lb, ub) = self.bounds(var);
+        if lb == ub {
+            Some(lb)
+        } else {
+            None
+        }
+    }
+
     pub fn entails(&self, lit: Lit) -> bool {
         debug_assert!(!self.doms.entails(lit) || !self.doms.entails(!lit));
         self.doms.entails(lit)

solver/src/core/state/snapshot.rs

@@ -2,6 +2,8 @@ use crate::backtrack::{DecLvl, EventIndex};
 use crate::core::state::{Domains, Event, Term};
 use crate::core::{IntCst, Lit, SignedVar};
 
+use super::IntDomain;
+
 /// View of the domains at a given point in time.
 ///
 /// This is primarily intended to query the state as it was when a literal was inferred.
@@ -60,11 +62,27 @@ impl<'a> DomainsSnapshot<'a> {
         -self.ub(-var.into())
     }
 
+    pub fn int_domain(&self, var: impl Into<SignedVar>) -> IntDomain {
+        let (lb, ub) = self.bounds(var.into());
+        IntDomain::new(lb, ub)
+    }
+
     pub fn bounds(&self, var: impl Into<SignedVar>) -> (IntCst, IntCst) {
         let var = var.into();
         (self.lb(var), self.ub(var))
     }
 
+    /// Returns Some(bound) is ub = lb
+    pub fn get_bound(&self, var: impl Into<SignedVar>) -> Option<IntCst> {
+        let var = var.into();
+        let (lb, ub) = self.bounds(var);
+        if lb == ub {
+            Some(lb)
+        } else {
+            None
+        }
+    }
+
     /// Returns true if the given literal is entailed by the current state;
     pub fn entails(&self, lit: Lit) -> bool {
         let curr_ub = self.ub(lit.svar());

solver/src/reasoners/eq_alt/constraints.rs

@@ -0,0 +1,151 @@
+use hashbrown::HashMap;
+use std::fmt::Debug;
+
+use crate::{
+    collections::ref_store::RefVec,
+    core::{literals::Watches, Lit},
+    create_ref_type,
+};
+
+use super::{node::Node, relation::EqRelation};
+
+// TODO: Identical to STN, maybe identify some other common logic and bump up to reasoner module
+
+/// Enabling information for a propagator.
+/// A propagator should be enabled iff both literals `active` and `valid` are true.
+#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
+pub struct Enabler {
+    /// A literal that is true (but not necessarily present) when the propagator must be active if present
+    pub active: Lit,
+    /// A literal that is true when the propagator is within its validity scope, i.e.,
+    /// when is known to be sound to propagate a change from the source to the target.
+    ///
+    /// In the simplest case, we have `valid = presence(active)` since by construction
+    /// `presence(active)` is true iff both variables of the constraint are present.
+    ///
+    /// `valid` might a more specific literal but always with the constraints that
+    /// `presence(active) => valid`
+    pub valid: Lit,
+}
+
+impl Enabler {
+    pub fn new(active: Lit, valid: Lit) -> Enabler {
+        Enabler { active, valid }
+    }
+}
+
+#[derive(Debug, Clone, Copy)]
+pub struct ActivationEvent {
+    /// the edge to enable
+    pub prop_id: ConstraintId,
+}
+
+impl ActivationEvent {
+    pub(crate) fn new(prop_id: ConstraintId) -> Self {
+        Self { prop_id }
+    }
+}
+
+create_ref_type!(ConstraintId);
+
+impl Debug for ConstraintId {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        writeln!(f, "Propagator {}", self.to_u32())
+    }
+}
+
+/// One direction of a semi-reified eq or neq constraint.
+///
+/// Formally enabler.active => a (relation) b
+/// with enabler.valid = presence(b) => presence(a)
+#[derive(Clone, Hash, Debug, PartialEq, Eq)]
+pub struct Constraint {
+    pub a: Node,
+    pub b: Node,
+    pub relation: EqRelation,
+    pub enabler: Enabler,
+}
+
+impl Constraint {
+    pub fn new(a: Node, b: Node, relation: EqRelation, active: Lit, valid: Lit) -> Self {
+        Self {
+            a,
+            b,
+            relation,
+            enabler: Enabler::new(active, valid),
+        }
+    }
+
+    pub fn new_pair(a: Node, b: Node, relation: EqRelation, active: Lit, ab_valid: Lit, ba_valid: Lit) -> (Self, Self) {
+        (
+            Self::new(a, b, relation, active, ab_valid),
+            Self::new(b, a, relation, active, ba_valid),
+        )
+    }
+}
+
+// #[derive(Debug, Clone, Copy)]
+// enum Event {
+//     PropagatorAdded,
+//     WatchAdded(ConstraintId, Lit),
+// }
+
+/// Data structures to store propagators.
+#[derive(Clone, Default)]
+pub struct ConstraintStore {
+    constraints: RefVec<ConstraintId, Constraint>,
+    // constraint_lookup: HashMap<(Node, Node), Vec<ConstraintId>>,
+    in_constraints: HashMap<Node, Vec<ConstraintId>>,
+    out_constraints: HashMap<Node, Vec<ConstraintId>>,
+    watches: Watches<(Enabler, ConstraintId)>,
+    // trail: Trail<Event>,
+}
+
+impl ConstraintStore {
+    pub fn add_constraint(&mut self, constraint: Constraint) -> ConstraintId {
+        // assert_eq!(self.current_decision_level(), DecLvl::ROOT);
+        // self.trail.push(Event::PropagatorAdded);
+        let id = self.constraints.len().into();
+        self.constraints.push(constraint.clone());
+        self.out_constraints
+            .entry(constraint.a)
+            .and_modify(|v| v.push(id))
+            .or_insert(vec![id]);
+        self.in_constraints
+            .entry(constraint.b)
+            .and_modify(|v| v.push(id))
+            .or_insert(vec![id]);
+        id
+    }
+
+    pub fn add_watch(&mut self, id: ConstraintId, literal: Lit) {
+        let enabler = self.constraints[id].enabler;
+        self.watches.add_watch((enabler, id), literal);
+        // self.trail.push(Event::WatchAdded(id, literal));
+    }
+
+    pub fn get_constraint(&self, constraint_id: ConstraintId) -> &Constraint {
+        &self.constraints[constraint_id]
+    }
+
+    // Get valid propagators by source and target
+    // pub fn get_constraints_between(&self, source: Node, target: Node) -> Vec<ConstraintId> {
+    //     self.constraint_lookup.get(&(source, target)).cloned().unwrap_or(vec![])
+    // }
+
+    pub fn get_out_constraints(&self, source: Node) -> Vec<ConstraintId> {
+        self.out_constraints.get(&source).cloned().unwrap_or_default()
+    }
+
+    pub fn get_in_constraints(&self, source: Node) -> Vec<ConstraintId> {
+        self.in_constraints.get(&source).cloned().unwrap_or_default()
+    }
+
+    pub fn enabled_by(&self, literal: Lit) -> impl Iterator<Item = (Enabler, ConstraintId)> + '_ {
+        self.watches.watches_on(literal)
+    }
+
+    pub fn iter(&self) -> impl Iterator<Item = (ConstraintId, &Constraint)> + use<'_> {
+        self.constraints.entries()
+    }
+}

solver/src/reasoners/eq_alt/graph/adj_list.rs

@@ -0,0 +1,68 @@
+use std::fmt::{Debug, Formatter};
+
+use crate::collections::ref_store::IterableRefMap;
+
+use super::{Edge, NodeId};
+
+#[derive(Default, Clone)]
+pub struct EqAdjList(IterableRefMap<NodeId, Vec<Edge>>);
+
+impl Debug for EqAdjList {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        writeln!(f)?;
+        for (node, edges) in self.0.entries() {
+            if !edges.is_empty() {
+                writeln!(f, "{:?}:", node)?;
+                for edge in edges {
+                    writeln!(f, "  -> {:?}    {:?}", edge.target, edge)?;
+                }
+            }
+        }
+        Ok(())
+    }
+}
+
+impl EqAdjList {
+    /// Insert a node if not present
+    fn insert_node(&mut self, node: NodeId) {
+        if !self.0.contains(node) {
+            self.0.insert(node, Default::default());
+        }
+    }
+
+    /// Possibly insert an edge and both nodes
+    /// Returns true if edge was inserted
+    pub fn insert_edge(&mut self, edge: Edge) -> bool {
+        self.insert_node(edge.source);
+        self.insert_node(edge.target);
+        let edges = self.get_edges_mut(edge.source).unwrap();
+        if edges.contains(&edge) {
+            false
+        } else {
+            edges.push(edge);
+            true
+        }
+    }
+
+    pub fn iter_edges(&self, node: NodeId) -> impl Iterator<Item = &Edge> {
+        self.0.get(node).into_iter().flat_map(|v| v.iter())
+    }
+
+    pub fn get_edges_mut(&mut self, node: NodeId) -> Option<&mut Vec<Edge>> {
+        self.0.get_mut(node)
+    }
+
+    pub fn iter_all_edges(&self) -> impl Iterator<Item = Edge> + use<'_> {
+        self.0.entries().flat_map(|(_, e)| e.iter().cloned())
+    }
+
+    pub fn iter_nodes(&self) -> impl Iterator<Item = NodeId> + use<'_> {
+        self.0.entries().map(|(n, _)| n)
+    }
+
+    pub fn remove_edge(&mut self, edge: Edge) {
+        if let Some(set) = self.0.get_mut(edge.source) {
+            set.retain(|e| *e != edge)
+        }
+    }
+}