Add IPASIR-UP feature and small test case

crates/pindakaas-derive/src/lib.rs

@@ -147,19 +147,22 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 			None => quote! { self.prop },
 		};
 		quote! {
+			#[cfg(feature = "ipasir-up")]
 			pub(crate) struct #prop_ident {
 				/// Rust Propagator Storage
 				prop: Box<crate::solver::libloading::IpasirPropStore>,
 				/// C Wrapper Object
 				wrapper: *mut std::ffi::c_void,
 			}
 
+			#[cfg(feature = "ipasir-up")]
 			impl Drop for #prop_ident {
 				fn drop(&mut self) {
 					unsafe { #krate::ipasir_prop_release(self.wrapper) };
 				}
 			}
 
+			#[cfg(feature = "ipasir-up")]
 			impl #prop_ident {
 				pub(crate) fn new(prop: Box<dyn crate::solver::Propagator>, slv: *mut dyn crate::solver::SolvingActions) -> Self {
 					// Construct wrapping structures
@@ -182,6 +185,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 				}
 			}
 
+			#[cfg(feature = "ipasir-up")]
 			impl crate::solver::PropagatingSolver for #ident {
 				fn set_external_propagator(
 					&mut self,
@@ -220,6 +224,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 				}
 			}
 
+			#[cfg(feature = "ipasir-up")]
 			impl crate::solver::SolvingActions for #ident {
 				fn new_var(&mut self) -> crate::Var {
 					<#ident as crate::ClauseDatabase>::new_var(self)
@@ -266,7 +271,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 
 		impl #ident {
 			/// Return the next [`size`] variables that can be stored as an inclusive range.
-			pub fn new_var_range(&mut self, size: usize) -> std::ops::RangeInclusive<crate::Var> {
+			pub fn new_var_range(&mut self, size: usize) -> crate::helpers::VarRange {
 				self.vars.new_var_range(size).expect("variable pool exhaused")
 			}
 		}

crates/pindakaas/Cargo.toml

@@ -14,7 +14,6 @@ edition = "2021"
 cached = "0.46"
 iset = "0.2"
 itertools = "0.12.0"
-pindakaas-derive = { path = "../pindakaas-derive" }
 rustc-hash = "1.1"
 # Dynamically load solver libraries (through IPASIR interfaces)
 libloading = "0.8"
@@ -24,6 +23,7 @@ tracing = { version = "0.1", optional = true }
 
 # Optional Solver Interfaces
 pindakaas-cadical = { path = "../pindakaas-cadical", optional = true }
+pindakaas-derive = { path = "../pindakaas-derive", optional = true }
 pindakaas-intel-sat = { path = "../pindakaas-intel-sat", optional = true }
 pindakaas-kissat = { path = "../pindakaas-kissat", optional = true }
 splr = { version = "0.17", optional = true }
@@ -33,8 +33,9 @@ splr = { version = "0.17", features = ["incremental_solver"] }
 traced_test = { path = "../traced_test" }
 
 [features]
-cadical = ["pindakaas-cadical"]
-intel-sat = ["pindakaas-intel-sat"]
-kissat = ["pindakaas-kissat"]
+cadical = ["pindakaas-cadical", "pindakaas-derive"]
+intel-sat = ["pindakaas-intel-sat", "pindakaas-derive"]
+kissat = ["pindakaas-kissat", "pindakaas-derive"]
 trace = ["tracing"]
 default = ["cadical"]
+ipasir-up = ["cadical"]

crates/pindakaas/src/helpers.rs

@@ -1,10 +1,15 @@
-use std::collections::HashSet;
+use std::{
+	cmp::max,
+	collections::HashSet,
+	iter::FusedIterator,
+	ops::{Bound, RangeBounds, RangeInclusive},
+};
 
 use itertools::Itertools;
 
 use crate::{
 	int::IntVar, linear::PosCoeff, trace::emit_clause, CheckError, Checker, ClauseDatabase, Coeff,
-	Encoder, LinExp, Lit, Result, Unsatisfiable, Valuation,
+	Encoder, LinExp, Lit, Result, Unsatisfiable, Valuation, Var,
 };
 
 #[allow(unused_macros)]
@@ -196,6 +201,74 @@ impl<'a> Checker for XorConstraint<'a> {
 	}
 }
 
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct VarRange {
+	start: Var,
+	end: Var,
+}
+
+impl VarRange {
+	pub fn new(start: Var, end: Var) -> Self {
+		Self { start, end }
+	}
+}
+
+impl Iterator for VarRange {
+	type Item = Var;
+
+	fn next(&mut self) -> Option<Self::Item> {
+		if self.start <= self.end {
+			let item = self.start;
+			self.start = self.start.next_var().unwrap();
+			Some(item)
+		} else {
+			None
+		}
+	}
+	fn size_hint(&self) -> (usize, Option<usize>) {
+		let size = max(self.end.0.get() - self.start.0.get(), 0) as usize;
+		(size, Some(size))
+	}
+	fn count(self) -> usize {
+		let (lower, upper) = self.size_hint();
+		debug_assert_eq!(upper, Some(lower));
+		lower
+	}
+}
+impl FusedIterator for VarRange {}
+impl ExactSizeIterator for VarRange {
+	fn len(&self) -> usize {
+		let (lower, upper) = self.size_hint();
+		debug_assert_eq!(upper, Some(lower));
+		lower
+	}
+}
+impl DoubleEndedIterator for VarRange {
+	fn next_back(&mut self) -> Option<Self::Item> {
+		if self.start <= self.end {
+			let item = self.end;
+			self.end = self.end.prev_var().unwrap();
+			Some(item)
+		} else {
+			None
+		}
+	}
+}
+impl RangeBounds<Var> for VarRange {
+	fn start_bound(&self) -> Bound<&Var> {
+		Bound::Included(&self.start)
+	}
+
+	fn end_bound(&self) -> Bound<&Var> {
+		Bound::Included(&self.end)
+	}
+}
+impl From<RangeInclusive<Var>> for VarRange {
+	fn from(value: RangeInclusive<Var>) -> Self {
+		VarRange::new(*value.start(), *value.end())
+	}
+}
+
 #[cfg(test)]
 pub mod tests {
 	use std::{

crates/pindakaas/src/lib.rs

@@ -48,11 +48,24 @@ pub struct Var(pub(crate) NonZeroI32);
 
 impl Var {
 	fn next_var(&self) -> Option<Var> {
-		self.checked_add(NonZeroI32::new(1).unwrap())
+		const ONE: NonZeroI32 = unsafe { NonZeroI32::new_unchecked(1) };
+		self.checked_add(ONE)
+	}
+
+	fn prev_var(&self) -> Option<Var> {
+		let prev = self.0.get() - 1;
+		if prev >= 0 {
+			Some(Var(NonZeroI32::new(prev).unwrap()))
+		} else {
+			None
+		}
 	}
 
 	fn checked_add(&self, b: NonZeroI32) -> Option<Var> {
-		self.0.get().checked_add(b.get()).map(|v| Var(NonZeroI32::new(v).unwrap()))
+		self.0
+			.get()
+			.checked_add(b.get())
+			.map(|v| Var(NonZeroI32::new(v).unwrap()))
 	}
 }
 

crates/pindakaas/src/solver.rs

@@ -1,6 +1,6 @@
-use std::{num::NonZeroI32, ops::RangeInclusive};
+use std::num::NonZeroI32;
 
-use crate::{ClauseDatabase, Lit, Valuation, Var};
+use crate::{helpers::VarRange, ClauseDatabase, Lit, Valuation, Var};
 
 pub mod libloading;
 
@@ -74,6 +74,7 @@ pub trait TermCallback: Solver {
 	fn set_terminate_callback<F: FnMut() -> SlvTermSignal>(&mut self, cb: Option<F>);
 }
 
+#[cfg(feature = "ipasir-up")]
 pub trait PropagatingSolver: Solver {
 	/// Set Propagator implementation which allows to learn, propagate and
 	/// backtrack based on external constraints.
@@ -96,6 +97,7 @@ pub trait PropagatingSolver: Solver {
 	fn reset_observed_vars(&mut self);
 }
 
+#[cfg(feature = "ipasir-up")]
 pub trait Propagator {
 	/// This method is called checked only when the propagator is connected. When
 	/// a Propagator is marked as lazy, it is only asked to check complete
@@ -108,14 +110,20 @@ pub trait Propagator {
 	/// variables. The notification is not necessarily eager. It usually happens
 	/// before the call of propagator callbacks and when a driving clause is
 	/// leading to an assignment.
-	fn notify_assignment(&mut self, _lit: Lit, _is_fixed: bool) {}
+	fn notify_assignment(&mut self, lit: Lit, is_fixed: bool) {
+		let _ = lit;
+		let _ = is_fixed;
+	}
 	fn notify_new_decision_level(&mut self) {}
-	fn notify_backtrack(&mut self, _new_level: usize) {}
+	fn notify_backtrack(&mut self, new_level: usize) {
+		let _ = new_level;
+	}
 
 	/// Method called to check the found complete solution (after solution
 	/// reconstruction). If it returns false, the propagator must provide an
 	/// external clause during the next callback.
-	fn check_model(&mut self, _value: &dyn Valuation) -> bool {
+	fn check_model(&mut self, value: &dyn Valuation) -> bool {
+		let _ = value;
 		true
 	}
 
@@ -129,14 +137,16 @@ pub trait Propagator {
 	/// current assignment. It returns queue of literals to be propagated in order,
 	/// if an empty queue is returned it indicates that there is no propagation
 	/// under the current assignment.
-	fn propagate(&mut self, _slv: &mut dyn SolvingActions) -> Vec<Lit> {
+	fn propagate(&mut self, slv: &mut dyn SolvingActions) -> Vec<Lit> {
+		let _ = slv;
 		Vec::new()
 	}
 
 	/// Ask the external propagator for the reason clause of a previous external
 	/// propagation step (done by [`Propagator::propagate`]). The clause must
 	/// contain the propagated literal.
-	fn add_reason_clause(&mut self, _propagated_lit: Lit) -> Vec<Lit> {
+	fn add_reason_clause(&mut self, propagated_lit: Lit) -> Vec<Lit> {
+		let _ = propagated_lit;
 		Vec::new()
 	}
 
@@ -146,6 +156,7 @@ pub trait Propagator {
 	}
 }
 
+#[cfg(feature = "ipasir-up")]
 pub trait SolvingActions {
 	fn new_var(&mut self) -> Var;
 	fn add_observed_var(&mut self, var: Var);
@@ -174,18 +185,23 @@ impl VarFactory {
 	}
 
 	/// Return the next [`size`] variables that can be stored as an inclusive range.
-	pub fn new_var_range(&mut self, size: usize) -> Option<RangeInclusive<Var>> {
+	pub fn new_var_range(&mut self, size: usize) -> Option<VarRange> {
 		let Some(start) = self.next_var else {
 			return None;
 		};
 		match size {
-			0 => Some(Var(NonZeroI32::new(2).unwrap())..=Var(NonZeroI32::new(1).unwrap())),
+			0 => Some(VarRange::new(
+				Var(NonZeroI32::new(2).unwrap()),
+				Var(NonZeroI32::new(1).unwrap()),
+			)),
 			_ if size > NonZeroI32::MAX.get() as usize => None,
 			_ => {
-				let size = NonZeroI32::new(size as i32).unwrap();
+				// Size is reduced by 1 since it includes self.next_var
+				let size = NonZeroI32::new((size - 1) as i32).unwrap();
 				if let Some(end) = start.checked_add(size) {
-					self.next_var = end.checked_add(NonZeroI32::new(1).unwrap());
-					Some(start..=end)
+					// Set self.next_var to one after end
+					self.next_var = end.next_var();
+					Some(VarRange::new(start, end))
 				} else {
 					None
 				}