Update library to work with the newest version of pindakaas

clippy.toml

@@ -1,4 +1,6 @@
 enforced-import-renames = [
   { path = "pindakaas::Lit", rename = "RawLit" },
   { path = "pindakaas::Var", rename = "RawVar" },
+  { path = "pindakaas::solver::Solver", rename = "SolverTrait" },
+  { path = "pindakaas::Valuation", rename = "SatValuation" },
 ]

crates/huub/src/lib.rs

@@ -8,9 +8,7 @@ pub use solver::{BoolView, IntVal, IntView, LitMeaning, Solver, SolverView, Valu
 
 #[cfg(test)]
 mod tests {
-	use crate::{
-		Constraint, Model, SimplifiedBool, SimplifiedVariable, SolveResult, Solver, Variable,
-	};
+	use crate::{Constraint, Model, SolveResult, Solver, Variable};
 
 	#[test]
 	fn it_works() {

crates/huub/src/model.rs

@@ -6,7 +6,10 @@ mod reformulate;
 use std::ops::AddAssign;
 
 use flatzinc_serde::RangeList;
-use pindakaas::{ClauseDatabase, Cnf, Lit as RawLit, Var as RawVar};
+use pindakaas::{
+	solver::{PropagatorAccess, Solver as SolverTrait},
+	ClauseDatabase, Cnf, Lit as RawLit, Valuation as SatValuation, Var as RawVar,
+};
 
 use self::{
 	bool::{BoolExpr, BoolVar},
@@ -39,7 +42,12 @@ impl Model {
 	}
 
 	// TODO: Make generic on Solver again (need var range trait)
-	pub fn to_solver<Sat: SatSolver>(&self) -> (Solver<Sat>, VariableMap) {
+	pub fn to_solver<
+		Sol: PropagatorAccess + SatValuation,
+		Sat: SatSolver + SolverTrait<ValueFn = Sol>,
+	>(
+		&self,
+	) -> (Solver<Sat>, VariableMap) {
 		let mut map = VariableMap::default();
 
 		// TODO: run SAT simplification
@@ -87,7 +95,14 @@ pub enum Constraint {
 }
 
 impl Constraint {
-	fn to_solver<Sat: SatSolver>(&self, slv: &mut Solver<Sat>, map: &mut VariableMap) {
+	fn to_solver<
+		Sol: PropagatorAccess + SatValuation,
+		Sat: SatSolver + SolverTrait<ValueFn = Sol>,
+	>(
+		&self,
+		slv: &mut Solver<Sat>,
+		map: &mut VariableMap,
+	) {
 		struct Satisfied;
 		match self {
 			Constraint::Clause(v) => {

crates/huub/src/model/bool.rs

@@ -4,7 +4,10 @@ use std::{
 	ops::Not,
 };
 
-use pindakaas::{Lit as RawLit, Var as RawVar};
+use pindakaas::{
+	solver::{PropagatorAccess, Solver as SolverTrait},
+	Lit as RawLit, Valuation as SatValuation, Var as RawVar,
+};
 
 use super::reformulate::{ReifContext, VariableMap};
 use crate::{
@@ -20,10 +23,13 @@ pub enum BoolExpr {
 }
 
 impl BoolExpr {
-	pub(crate) fn to_arg<S: SatSolver>(
+	pub(crate) fn to_arg<
+		Sol: PropagatorAccess + SatValuation,
+		Sat: SatSolver + SolverTrait<ValueFn = Sol>,
+	>(
 		&self,
 		ctx: ReifContext,
-		slv: &mut Solver<S>,
+		slv: &mut Solver<Sat>,
 		map: &mut VariableMap,
 	) -> BoolView {
 		match self {
@@ -33,10 +39,13 @@ impl BoolExpr {
 		}
 	}
 
-	fn to_negated_arg<S: SatSolver>(
+	fn to_negated_arg<
+		Sol: PropagatorAccess + SatValuation,
+		Sat: SatSolver + SolverTrait<ValueFn = Sol>,
+	>(
 		&self,
 		ctx: ReifContext,
-		slv: &mut Solver<S>,
+		slv: &mut Solver<Sat>,
 		map: &mut VariableMap,
 	) -> BoolView {
 		match self {
@@ -54,7 +63,6 @@ impl Not for BoolExpr {
 			BoolExpr::Lit(l) => BoolExpr::Lit(!l),
 			BoolExpr::Val(v) => BoolExpr::Val(!v),
 			BoolExpr::Not(e) => *e,
-			//			e => BoolExpr::Not(Box::new(e)),
 		}
 	}
 }
@@ -66,7 +74,6 @@ impl Not for &BoolExpr {
 			BoolExpr::Lit(l) => BoolExpr::Lit(!*l),
 			BoolExpr::Val(v) => BoolExpr::Val(!*v),
 			BoolExpr::Not(e) => (**e).clone(),
-			//			e => BoolExpr::Not(Box::new(e.clone())),
 		}
 	}
 }

crates/huub/src/model/int.rs

@@ -1,4 +1,8 @@
 use flatzinc_serde::RangeList;
+use pindakaas::{
+	solver::{PropagatorAccess, Solver as SolverTrait},
+	Valuation as SatValuation,
+};
 
 use super::reformulate::{ReifContext, VariableMap};
 use crate::{
@@ -13,10 +17,13 @@ pub enum IntExpr {
 }
 
 impl IntExpr {
-	pub(crate) fn to_arg<S: SatSolver>(
+	pub(crate) fn to_arg<
+		Sol: PropagatorAccess + SatValuation,
+		Sat: SatSolver + SolverTrait<ValueFn = Sol>,
+	>(
 		&self,
 		_ctx: ReifContext,
-		_slv: &mut Solver<S>,
+		_slv: &mut Solver<Sat>,
 		map: &mut VariableMap,
 	) -> IntView {
 		match self {

crates/huub/src/propagator.rs

@@ -7,7 +7,10 @@ pub(crate) mod reason;
 
 use std::fmt::Debug;
 
-use pindakaas::Lit as RawLit;
+use pindakaas::{
+	solver::{PropagatorAccess, Solver as SolverTrait},
+	Lit as RawLit, Valuation as SatValuation,
+};
 
 use crate::{
 	propagator::{
@@ -70,7 +73,13 @@ pub(crate) trait Initialize {
 	///
 	/// This method is generally used to register variable event
 	/// subscriptions with the solver.
-	fn initialize<Sat: SatSolver>(&mut self, actions: &mut InitializationActions<'_, Sat>) -> bool {
+	fn initialize<
+		Sol: PropagatorAccess + SatValuation,
+		Sat: SatSolver + SolverTrait<ValueFn = Sol>,
+	>(
+		&mut self,
+		actions: &mut InitializationActions<'_, Sat>,
+	) -> bool {
 		let _ = actions;
 		false
 	}

crates/huub/src/propagator/all_different.rs

@@ -1,3 +1,7 @@
+use pindakaas::{
+	solver::{PropagatorAccess, Solver as SolverTrait},
+	Valuation as SatValuation,
+};
 use tracing::trace;
 
 use super::reason::ReasonBuilder;
@@ -75,7 +79,13 @@ impl Propagator for AllDifferentValue {
 }
 
 impl Initialize for AllDifferentValue {
-	fn initialize<Sat: SatSolver>(&mut self, actions: &mut InitializationActions<'_, Sat>) -> bool {
+	fn initialize<
+		Sol: PropagatorAccess + SatValuation,
+		Sat: SatSolver + SolverTrait<ValueFn = Sol>,
+	>(
+		&mut self,
+		actions: &mut InitializationActions<'_, Sat>,
+	) -> bool {
 		for (i, v) in self.vars.iter().enumerate() {
 			actions.subscribe_int(*v, IntEvent::Fixed, i as u32)
 		}
@@ -93,8 +103,7 @@ mod tests {
 	};
 
 	use crate::{
-		propagator::all_different::AllDifferentValue,
-		solver::engine::int_var::{IntVal, IntVar},
+		propagator::all_different::AllDifferentValue, solver::engine::int_var::IntVar, IntVal,
 		IntView, Solver,
 	};
 

crates/huub/src/propagator/init_action.rs

@@ -1,17 +1,25 @@
-use pindakaas::solver::PropagatingSolver;
+use pindakaas::{
+	solver::{PropagatingSolver, PropagatorAccess, Solver as SolverTrait},
+	Valuation as SatValuation,
+};
 
 use crate::{
 	propagator::int_event::IntEvent,
 	solver::{engine::PropRef, view::BoolViewInner, BoolView, IntView, SatSolver},
 	Solver,
 };
 
-pub(crate) struct InitializationActions<'a, Sat: SatSolver> {
+pub(crate) struct InitializationActions<'a, Sat: SatSolver>
+where
+	<Sat as SolverTrait>::ValueFn: PropagatorAccess,
+{
 	pub(crate) prop_ref: PropRef,
 	pub(crate) slv: &'a mut Solver<Sat>,
 }
 
-impl<Sat: SatSolver> InitializationActions<'_, Sat> {
+impl<Sol: PropagatorAccess + SatValuation, Sat: SatSolver + SolverTrait<ValueFn = Sol>>
+	InitializationActions<'_, Sat>
+{
 	#[allow(dead_code)] // TODO
 	pub(crate) fn subscribe_bool(&mut self, var: BoolView, data: u32) {
 		match var.0 {