feat(solver): allow plugging external reasoners

examples/scheduling/src/search.rs

@@ -82,7 +82,7 @@ pub fn get_solver(mut base_solver: Solver, strategy: &SearchStrategy, pb: &Encod
                 "focused" => mode = Mode::Focused,
                 x if x.starts_with("+lbd") => {
                     let lvl = x.strip_prefix("+lbd").unwrap().parse().unwrap();
-                    base_solver.reasoners.sat.clauses.params.locked_lbd_level = lvl;
+                    base_solver.reasoners.sat().clauses.params.locked_lbd_level = lvl;
                 }
                 "" => {} // ignore
                 _ => panic!("Unsupported option: {opt}"),

planning/planners/src/solver.rs

@@ -381,7 +381,7 @@ pub fn init_solver(model: Model<VarLabel>) -> Box<Solver> {
     };
 
     let mut solver = Box::new(aries_solver::solver::Solver::new(model));
-    solver.reasoners.diff.config = stn_config;
+    solver.reasoners.diff().config = stn_config;
     solver
 }
 
@@ -446,11 +446,11 @@ impl Strat {
             }
             Strat::ActivityBoolLight => {
                 solver.set_brancher(ActivityBrancher::new_with_heuristic(ActivityBoolFirstHeuristic));
-                solver.reasoners.diff.config.theory_propagation = TheoryPropagationLevel::Bounds;
+                solver.reasoners.diff().config.theory_propagation = TheoryPropagationLevel::Bounds;
             }
             Strat::Forward => {
                 solver.set_brancher(ForwardSearcher::new(problem));
-                solver.reasoners.diff.config.theory_propagation = TheoryPropagationLevel::Bounds;
+                solver.reasoners.diff().config.theory_propagation = TheoryPropagationLevel::Bounds;
             }
             Strat::Causal => {
                 let strat = causal_brancher(problem, encoding);

planning/timelines/src/explain.rs

@@ -46,7 +46,7 @@ impl<T: Ord + Clone> ExplainableSolver<T> {
 
         // enable stronger propagation than default in difference logic solver.
         // this is useful in planning models where bounds are not sufficient to reason on precedence between tasks
-        solver.reasoners.diff.config.theory_propagation = aries_solver::reasoners::stn::TheoryPropagationLevel::Full;
+        solver.reasoners.diff().config.theory_propagation = aries_solver::reasoners::stn::TheoryPropagationLevel::Full;
 
         Self {
             solver,

solver/examples/tsp/main.rs

@@ -202,9 +202,9 @@ fn solve_tsp(pb: &TspProblem, args: &Opt) -> Option<TspSolution> {
     let mut solver = Solver::new(model);
 
     if args.no_lp {
-        solver.reasoners.lp.deactivate();
+        solver.reasoners.lp().deactivate();
     } else {
-        solver.reasoners.lp.activate();
+        solver.reasoners.lp().activate();
     }
 
     let solution_opt = match solver.minimize_with_callback(

solver/src/reasoners/mod.rs

@@ -1,3 +1,5 @@
+use itertools::Itertools;
+
 use crate::backtrack::Backtrack;
 use crate::core::Lit;
 use crate::core::state::{Cause, DomainsSnapshot, Explainer, InferenceCause};
@@ -24,6 +26,7 @@ pub enum ReasonerId {
     Cp,
     Tautologies,
     Lp,
+    Extra(u8),
 }
 
 impl ReasonerId {
@@ -35,6 +38,7 @@ impl ReasonerId {
 impl Display for ReasonerId {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         use ReasonerId::*;
+        let mut _extra_str = String::new();
         write!(
             f,
             "{}",
@@ -44,12 +48,16 @@ impl Display for ReasonerId {
                 Cp => "CP",
                 Tautologies => "Optim",
                 Lp => "LP",
+                Extra(i) => {
+                    _extra_str = format!("Extra({i})");
+                    &_extra_str
+                }
             }
         )
     }
 }
 
-pub trait Theory: Backtrack + Send + 'static {
+pub trait Theory: Backtrack + Send {
     fn identity(&self) -> ReasonerId;
 
     fn propagate(&mut self, model: &mut Domains) -> Result<(), Contradiction>;
@@ -95,52 +103,168 @@ pub(crate) const REASONERS: [ReasonerId; 5] = [
     ReasonerId::Lp,
 ];
 
-/// A set of inference modules for constraint propagation.
-#[derive(Clone)]
-pub struct Reasoners {
+pub(crate) struct ReasonersTheories {
     pub sat: SatSolver,
     pub diff: StnTheory,
     pub(crate) cp: Cp,
     pub(crate) tautologies: Tautologies,
     pub lp: Lp,
+    pub extra: Vec<Option<Box<dyn Theory>>>,
 }
-impl Reasoners {
+impl Clone for ReasonersTheories {
+    fn clone(&self) -> Self {
+        Self {
+            sat: self.sat.clone(),
+            diff: self.diff.clone(),
+            cp: self.cp.clone(),
+            tautologies: self.tautologies.clone(),
+            lp: self.lp.clone(),
+            extra: self
+                .extra
+                .iter()
+                .map(|th| th.as_ref().map(|th| th.clone_box()))
+                .collect(),
+        }
+    }
+}
+impl ReasonersTheories {
     pub fn new() -> Self {
-        Reasoners {
+        ReasonersTheories {
             sat: SatSolver::new(ReasonerId::Sat),
             diff: StnTheory::new(Default::default()),
             cp: Cp::new(ReasonerId::Cp),
             tautologies: Tautologies::default(),
             lp: Lp::default(),
+            extra: vec![],
         }
     }
+    pub fn with_extra(extra: Vec<Box<dyn Theory>>) -> Self {
+        assert!(
+            extra
+                .iter()
+                .map(|r| r.identity())
+                .all(|rid| matches!(rid, ReasonerId::Extra(_)))
+        );
+        assert!(extra.iter().map(|r| r.identity()).all_unique());
+
+        let extra = {
+            let mut res = vec![];
+            for r in extra {
+                let ReasonerId::Extra(i) = r.identity() else {
+                    unreachable!()
+                };
+                let i = i as usize;
+                while res.len() <= i {
+                    res.push(None);
+                }
+                res[i] = Some(r);
+            }
+            res
+        };
 
-    pub fn reasoner(&self, id: ReasonerId) -> &dyn Theory {
+        ReasonersTheories {
+            sat: SatSolver::new(ReasonerId::Sat),
+            diff: StnTheory::new(Default::default()),
+            cp: Cp::new(ReasonerId::Cp),
+            tautologies: Tautologies::default(),
+            lp: Lp::default(),
+            extra,
+        }
+    }
+    pub fn get(&self, id: ReasonerId) -> &dyn Theory {
         match id {
             ReasonerId::Sat => &self.sat,
             ReasonerId::Diff => &self.diff,
             ReasonerId::Cp => &self.cp,
             ReasonerId::Tautologies => &self.tautologies,
             ReasonerId::Lp => &self.lp,
+            ReasonerId::Extra(id) => self.extra.get(id as usize).unwrap().as_ref().unwrap().as_ref(),
         }
     }
-
-    pub fn reasoner_mut(&mut self, id: ReasonerId) -> &mut dyn Theory {
+    pub fn get_mut(&mut self, id: ReasonerId) -> &mut dyn Theory {
         match id {
             ReasonerId::Sat => &mut self.sat,
             ReasonerId::Diff => &mut self.diff,
             ReasonerId::Cp => &mut self.cp,
             ReasonerId::Tautologies => &mut self.tautologies,
             ReasonerId::Lp => &mut self.lp,
+            ReasonerId::Extra(id) => self.extra.get_mut(id as usize).unwrap().as_mut().unwrap().as_mut(),
+        }
+    }
+}
+
+#[derive(Clone)]
+pub(crate) struct ReasonersWriters {
+    writers: Vec<ReasonerId>,
+}
+impl ReasonersWriters {
+    pub fn new() -> Self {
+        Self {
+            writers: REASONERS.to_vec(),
+        }
+    }
+    pub fn with_extra(extra: &[Box<dyn Theory>]) -> Self {
+        assert!(
+            extra
+                .iter()
+                .map(|r| r.identity())
+                .all(|rid| matches!(rid, ReasonerId::Extra(_)))
+        );
+        assert!(extra.iter().map(|r| r.identity()).all_unique());
+
+        Self {
+            writers: REASONERS
+                .into_iter()
+                .chain(extra.iter().map(|r| r.identity()))
+                .collect(),
         }
     }
+    pub fn get(&self) -> &[ReasonerId] {
+        &self.writers
+    }
+}
 
-    pub fn writers(&self) -> &'static [ReasonerId] {
-        &REASONERS
+/// A set of inference modules for constraint propagation.
+#[derive(Clone)]
+pub struct Reasoners {
+    pub(crate) writers: ReasonersWriters,
+    pub(crate) theories: ReasonersTheories,
+}
+impl Reasoners {
+    pub fn new() -> Self {
+        Self {
+            writers: ReasonersWriters::new(),
+            theories: ReasonersTheories::new(),
+        }
+    }
+    pub fn with_extra(extra: Vec<Box<dyn Theory>>) -> Self {
+        Self {
+            writers: ReasonersWriters::with_extra(&extra),
+            theories: ReasonersTheories::with_extra(extra),
+        }
+    }
+
+    pub fn sat(&mut self) -> &mut SatSolver {
+        &mut self.theories.sat
+    }
+    pub fn diff(&mut self) -> &mut StnTheory {
+        &mut self.theories.diff
+    }
+    pub fn cp(&mut self) -> &mut Cp {
+        &mut self.theories.cp
+    }
+    pub fn tautologies(&mut self) -> &mut Tautologies {
+        &mut self.theories.tautologies
+    }
+    pub fn lp(&mut self) -> &mut Lp {
+        &mut self.theories.lp
+    }
+    pub fn extra(&mut self) -> impl Iterator<Item = &mut Box<dyn Theory>> + '_ {
+        self.theories.extra.iter_mut().filter_map(|th| th.as_mut())
     }
 
-    pub fn theories(&self) -> impl Iterator<Item = (ReasonerId, &dyn Theory)> + '_ {
-        self.writers().iter().map(|w| (*w, self.reasoner(*w)))
+    pub fn iter(&self) -> impl Iterator<Item = (ReasonerId, &dyn Theory)> + '_ {
+        self.writers.get().iter().map(|w| (*w, self.theories.get(*w)))
     }
 }
 
@@ -152,7 +276,8 @@ impl Default for Reasoners {
 
 impl Explainer for Reasoners {
     fn explain(&mut self, cause: InferenceCause, literal: Lit, model: &DomainsSnapshot, explanation: &mut Explanation) {
-        self.reasoner_mut(cause.writer)
+        self.theories
+            .get_mut(cause.writer)
             .explain(literal, cause, model, explanation)
     }
 }