From e8da0d4caae377d78e2361276d9da4b5af1e9101 Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <jip@dekker.one>
Date: Thu, 17 Oct 2024 14:09:12 +1100
Subject: [PATCH] Simplify the variable management and add `new_lits`
 convenience feature

---
 crates/pindakaas-derive/src/lib.rs          |  37 +++----
 crates/pindakaas/src/bool_linear.rs         | 111 ++++----------------
 crates/pindakaas/src/cardinality.rs         |  14 +--
 crates/pindakaas/src/cardinality_one.rs     |  38 ++-----
 crates/pindakaas/src/lib.rs                 |  97 ++++++++++++-----
 crates/pindakaas/src/propositional_logic.rs |  72 +++----------
 crates/pindakaas/src/solver.rs              |  67 +++++-------
 crates/pindakaas/src/solver/cadical.rs      |   4 +-
 crates/pindakaas/src/solver/libloading.rs   |   8 +-
 crates/pindakaas/src/solver/splr.rs         |  13 ++-
 crates/pindakaas/src/sorted.rs              |  18 ++--
 11 files changed, 184 insertions(+), 295 deletions(-)

diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs
index e8d385a157..37964d74ab 100644
--- a/crates/pindakaas-derive/src/lib.rs
+++ b/crates/pindakaas-derive/src/lib.rs
@@ -259,7 +259,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 			#[cfg(feature = "external-propagation")]
 			impl crate::solver::propagation::SolvingActions for #actions_ident {
 				fn new_var(&mut self) -> crate::Var {
-					self.vars.as_ref().lock().unwrap().next().expect("variable pool exhaused")
+					self.vars.as_ref().lock().unwrap().next_var()
 				}
 				fn add_observed_var(&mut self, var: crate::Var) {
 					unsafe { #krate::ipasir_add_observed_var( self.ptr, var.0.get()) };
@@ -332,34 +332,29 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 		quote! {
 			fn new_var(&mut self) -> crate::Var {
 				#[cfg(feature = "external-propagation")]
-				let var = #vars .as_ref().lock().unwrap().next().expect("variable pool exhaused");
+				let var = #vars .as_ref().lock().unwrap().next_var();
 				#[cfg(not(feature = "external-propagation"))]
-				let var = #vars .next().expect("variable pool exhaused");
+				let var = #vars .next_var();
 				var
 			}
-		}
-	} else {
-		quote! {
-			fn new_var(&mut self) -> crate::Var {
-				#vars .next().expect("variable pool exhaused")
-			}
-		}
-	};
 
-	let next_var_range = if opts.ipasir_up {
-		quote! {
-			fn next_var_range(&mut self, size: usize) -> Option<crate::VarRange> {
+			fn new_var_range(&mut self, len: usize) -> crate::VarRange {
 				#[cfg(feature = "external-propagation")]
-				let r = #vars .as_ref().lock().unwrap().next_var_range(size);
+				let var = #vars .as_ref().lock().unwrap().next_var_range(len);
 				#[cfg(not(feature = "external-propagation"))]
-				let r = #vars .next_var_range(size);
-				r
+				let var = #vars .next_var_range(len);
+				var
 			}
 		}
 	} else {
 		quote! {
-			fn next_var_range(&mut self, size: usize) -> Option<crate::VarRange> {
-				#vars .next_var_range(size)
+			fn new_var(&mut self) -> crate::Var {
+				#vars .next_var()
+			}
+
+			fn new_var_range(&mut self, len: usize) -> crate::VarRange {
+				let var = #vars .next_var_range(len);
+				var
 			}
 		}
 	};
@@ -441,10 +436,6 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 			}
 		}
 
-		impl crate::solver::NextVarRange for #ident {
-			#next_var_range
-		}
-
 		impl crate::solver::Solver for #ident {
 			type ValueFn = #sol_ident;
 
diff --git a/crates/pindakaas/src/bool_linear.rs b/crates/pindakaas/src/bool_linear.rs
index 41b2a8d9fc..99e1001bd5 100644
--- a/crates/pindakaas/src/bool_linear.rs
+++ b/crates/pindakaas/src/bool_linear.rs
@@ -2126,9 +2126,8 @@ mod tests {
 		cardinality::{tests::card_test_suite, Cardinality},
 		cardinality_one::{tests::card1_test_suite, CardinalityOne, PairwiseEncoder},
 		helpers::tests::{assert_checker, assert_encoding, assert_solutions, expect_file},
-		solver::NextVarRange,
 		sorted::SortedEncoder,
-		Cnf, Coeff, Encoder, Lit, Unsatisfiable,
+		ClauseDatabase, Cnf, Coeff, Encoder, Lit, Unsatisfiable,
 	};
 
 	pub(crate) fn construct_terms<L: Into<Lit> + Clone>(terms: &[(L, Coeff)]) -> Vec<Part> {
@@ -2141,12 +2140,7 @@ mod tests {
 	#[test]
 	fn test_aggregator_at_least_one_negated() {
 		let mut cnf = Cnf::default();
-		let (a, b, c, d) = cnf
-			.next_var_range(4)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d) = cnf.new_lits();
 		// Correctly detect that all but one literal can be set to true
 		assert_eq!(
 			BoolLinAggregator::default().aggregate(
@@ -2166,12 +2160,7 @@ mod tests {
 
 		// Correctly detect equal k
 		let mut cnf = Cnf::default();
-		let (a, b, c) = cnf
-			.next_var_range(3)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c) = cnf.new_lits();
 		assert_eq!(
 			BoolLinAggregator::default().aggregate(
 				&mut cnf,
@@ -2192,12 +2181,7 @@ mod tests {
 	#[test]
 	fn test_aggregator_combine() {
 		let mut cnf = Cnf::default();
-		let (a, b, c) = cnf
-			.next_var_range(3)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c) = cnf.new_lits();
 		// Simple aggregation of multiple occurrences of the same literal
 		assert_eq!(
 			BoolLinAggregator::default().aggregate(
@@ -2260,12 +2244,7 @@ mod tests {
 	#[test]
 	fn test_aggregator_detection() {
 		let mut cnf = Cnf::default();
-		let (a, b, c, d) = cnf
-			.next_var_range(4)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d) = cnf.new_lits();
 
 		// Correctly detect at most one
 		assert_eq!(
@@ -2412,7 +2391,7 @@ mod tests {
 	#[test]
 	fn test_aggregator_equal_one() {
 		let mut cnf = Cnf::default();
-		let vars = cnf.next_var_range(3).unwrap().iter_lits().collect_vec();
+		let vars = cnf.new_var_range(3).iter_lits().collect_vec();
 		// An exactly one constraint adds an exactly one constraint
 		assert_eq!(
 			BoolLinAggregator::default().aggregate(
@@ -2434,12 +2413,7 @@ mod tests {
 	#[test]
 	fn test_aggregator_false_trivial_unsat() {
 		let mut cnf = Cnf::default();
-		let (a, b, c, d, e, f, g) = cnf
-			.next_var_range(7)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d, e, f, g) = cnf.new_lits();
 		assert_eq!(
 			BoolLinAggregator::default().aggregate(
 				&mut cnf,
@@ -2469,12 +2443,7 @@ mod tests {
 	#[test]
 	fn test_aggregator_neg_coeff() {
 		let mut cnf = Cnf::default();
-		let (a, b, c) = cnf
-			.next_var_range(3)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c) = cnf.new_lits();
 
 		// Correctly convert a negative coefficient
 		assert_eq!(
@@ -2526,12 +2495,7 @@ mod tests {
 
 		// Correctly convert multiple negative coefficients with AMO constraints
 		let mut cnf = Cnf::default();
-		let (a, b, c, d, e, f) = cnf
-			.next_var_range(6)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d, e, f) = cnf.new_lits();
 		assert_eq!(
 			BoolLinAggregator::default().aggregate(
 				&mut cnf,
@@ -2563,12 +2527,7 @@ mod tests {
 
 		// Correctly convert multiple negative coefficients with side constraints
 		let mut cnf = Cnf::default();
-		let (a, b, c, d, e, f) = cnf
-			.next_var_range(6)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d, e, f) = cnf.new_lits();
 		assert_eq!(
 			BoolLinAggregator::default().aggregate(
 				&mut cnf,
@@ -2605,12 +2564,7 @@ mod tests {
 
 		// Correctly convert GreaterEq into LessEq with side constrains
 		let mut cnf = Cnf::default();
-		let (a, b, c, d, e, f) = cnf
-			.next_var_range(6)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d, e, f) = cnf.new_lits();
 		assert_eq!(
 			BoolLinAggregator::default().aggregate(
 				&mut cnf,
@@ -2642,12 +2596,7 @@ mod tests {
 
 		// Correctly convert GreaterEq into LessEq with side constrains
 		let mut cnf = Cnf::default();
-		let (a, b, c, d, e, f) = cnf
-			.next_var_range(6)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d, e, f) = cnf.new_lits();
 		assert_eq!(
 			BoolLinAggregator::default().aggregate(
 				&mut cnf,
@@ -2676,12 +2625,7 @@ mod tests {
 
 		// Correctly account for the coefficient in the Dom bounds
 		let mut cnf = Cnf::default();
-		let (a, b, c) = cnf
-			.next_var_range(3)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c) = cnf.new_lits();
 		assert_eq!(
 			BoolLinAggregator::default().aggregate(
 				&mut cnf,
@@ -2708,12 +2652,7 @@ mod tests {
 
 		// Correctly convert GreaterEq into LessEq with side constrains
 		let mut cnf = Cnf::default();
-		let (a, b, c, d, e) = cnf
-			.next_var_range(5)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d, e) = cnf.new_lits();
 		assert_eq!(
 			BoolLinAggregator::default().aggregate(
 				&mut cnf,
@@ -2751,12 +2690,7 @@ mod tests {
 	#[test]
 	fn test_aggregator_sort_same_coefficients() {
 		let mut cnf = Cnf::default();
-		let (a, b, c, d) = cnf
-			.next_var_range(4)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d) = cnf.new_lits();
 
 		assert_eq!(
 			BoolLinAggregator::default()
@@ -2787,7 +2721,7 @@ mod tests {
 	#[test]
 	fn test_aggregator_sort_same_coefficients_using_minimal_chain() {
 		let mut cnf = Cnf::default();
-		let vars = cnf.next_var_range(5).unwrap().iter_lits().collect_vec();
+		let vars = cnf.new_var_range(5).iter_lits().collect_vec();
 		assert_eq!(
 			BoolLinAggregator::default()
 				.sort_same_coefficients(SortedEncoder::default(), 2)
@@ -2816,7 +2750,7 @@ mod tests {
 	#[test]
 	fn test_aggregator_unsat() {
 		let mut db = Cnf::default();
-		let vars = db.next_var_range(3).unwrap().iter_lits().collect_vec();
+		let vars = db.new_var_range(3).iter_lits().collect_vec();
 
 		// Constant cannot be reached
 		assert_eq!(
@@ -2870,12 +2804,7 @@ mod tests {
 	#[test]
 	fn test_encoders() {
 		let mut cnf = Cnf::default();
-		let (a, b, c, d) = cnf
-			.next_var_range(4)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d) = cnf.new_lits();
 		// TODO encode this if encoder does not support constraint
 		PairwiseEncoder::default()
 			.encode(
@@ -2919,7 +2848,7 @@ mod tests {
 	#[test]
 	fn test_pb_encode() {
 		let mut cnf = Cnf::default();
-		let vars = cnf.next_var_range(4).unwrap().iter_lits().collect_vec();
+		let vars = cnf.new_var_range(4).iter_lits().collect_vec();
 		LinearEncoder::<StaticLinEncoder>::default()
 			.encode(
 				&mut cnf,
@@ -2938,7 +2867,7 @@ mod tests {
 	#[test]
 	fn test_sort_same_coefficients_2() {
 		let mut db = Cnf::default();
-		let vars = db.next_var_range(5).unwrap().iter_lits().collect_vec();
+		let vars = db.new_var_range(5).iter_lits().collect_vec();
 		let mut agg = BoolLinAggregator::default();
 		let _ = agg.sort_same_coefficients(SortedEncoder::default(), 3);
 		let mut encoder = LinearEncoder::<StaticLinEncoder<TotalizerEncoder>>::default();
diff --git a/crates/pindakaas/src/cardinality.rs b/crates/pindakaas/src/cardinality.rs
index 304d470e40..0da24ace7f 100644
--- a/crates/pindakaas/src/cardinality.rs
+++ b/crates/pindakaas/src/cardinality.rs
@@ -107,7 +107,7 @@ pub(crate) mod tests {
 			#[test]
 			fn test_card_le_2_3() {
 				let mut cnf = Cnf::default();
-				let vars = cnf.next_var_range(3).unwrap().iter_lits().collect_vec();
+				let vars = cnf.new_var_range(3).iter_lits().collect_vec();
 				$encoder
 					.encode(
 						&mut cnf,
@@ -129,7 +129,7 @@ pub(crate) mod tests {
 			#[test]
 			fn test_card_eq_1_3() {
 				let mut cnf = Cnf::default();
-				let vars = cnf.next_var_range(3).unwrap().iter_lits().collect_vec();
+				let vars = cnf.new_var_range(3).iter_lits().collect_vec();
 				$encoder
 					.encode(
 						&mut cnf,
@@ -151,7 +151,7 @@ pub(crate) mod tests {
 			#[test]
 			fn test_card_eq_2_3() {
 				let mut cnf = Cnf::default();
-				let vars = cnf.next_var_range(3).unwrap().iter_lits().collect_vec();
+				let vars = cnf.new_var_range(3).iter_lits().collect_vec();
 				$encoder
 					.encode(
 						&mut cnf,
@@ -173,7 +173,7 @@ pub(crate) mod tests {
 			#[test]
 			fn test_card_eq_2_4() {
 				let mut cnf = Cnf::default();
-				let vars = cnf.next_var_range(4).unwrap().iter_lits().collect_vec();
+				let vars = cnf.new_var_range(4).iter_lits().collect_vec();
 				$encoder
 					.encode(
 						&mut cnf,
@@ -195,7 +195,7 @@ pub(crate) mod tests {
 			#[test]
 			fn test_card_eq_3_5() {
 				let mut cnf = Cnf::default();
-				let vars = cnf.next_var_range(5).unwrap().iter_lits().collect_vec();
+				let vars = cnf.new_var_range(5).iter_lits().collect_vec();
 				$encoder
 					.encode(
 						&mut cnf,
@@ -226,7 +226,7 @@ pub(crate) mod tests {
 				cardinality::{Cardinality, SortingNetworkEncoder},
 				helpers::tests::assert_solutions,
 				sorted::{SortedEncoder, SortedStrategy},
-				Cnf, Encoder, NextVarRange,
+				ClauseDatabase, Cnf, Encoder,
 			};
 
 			#[test]
@@ -289,7 +289,7 @@ pub(crate) mod tests {
 	macro_rules! test_card {
 		($encoder:expr,$n:expr,$cmp:expr,$k:expr) => {
 			let mut cnf = Cnf::default();
-			let vars = cnf.next_var_range($n).unwrap().iter_lits().collect_vec();
+			let vars = cnf.new_var_range($n).iter_lits().collect_vec();
 			$encoder
 				.encode(
 					&mut cnf,
diff --git a/crates/pindakaas/src/cardinality_one.rs b/crates/pindakaas/src/cardinality_one.rs
index 1a3aba695c..786c836db0 100644
--- a/crates/pindakaas/src/cardinality_one.rs
+++ b/crates/pindakaas/src/cardinality_one.rs
@@ -145,7 +145,7 @@ pub(crate) mod tests {
 					bool_linear::LimitComp,
 					cardinality_one::CardinalityOne,
 					helpers::tests::{assert_checker, assert_solutions, expect_file},
-					ClauseDatabase, Cnf, Encoder, NextVarRange,
+					ClauseDatabase, Cnf, Encoder,
 				};
 
 				const LARGE_N: usize = 50;
@@ -238,11 +238,7 @@ pub(crate) mod tests {
 				#[test]
 				fn test_amo_large() {
 					let mut cnf = Cnf::default();
-					let vars = cnf
-						.next_var_range(LARGE_N)
-						.unwrap()
-						.iter_lits()
-						.collect_vec();
+					let vars = cnf.new_var_range(LARGE_N).iter_lits().collect_vec();
 					let con = CardinalityOne {
 						lits: vars.clone(),
 						cmp: LimitComp::LessEq,
@@ -254,11 +250,7 @@ pub(crate) mod tests {
 				#[test]
 				fn test_amo_large_neg() {
 					let mut cnf = Cnf::default();
-					let vars = cnf
-						.next_var_range(LARGE_N)
-						.unwrap()
-						.iter_lits()
-						.collect_vec();
+					let vars = cnf.new_var_range(LARGE_N).iter_lits().collect_vec();
 					let con = CardinalityOne {
 						lits: vars.clone().into_iter().map(|l| !l).collect_vec(),
 						cmp: LimitComp::LessEq,
@@ -270,11 +262,7 @@ pub(crate) mod tests {
 				#[test]
 				fn test_amo_large_mix() {
 					let mut cnf = Cnf::default();
-					let vars = cnf
-						.next_var_range(LARGE_N)
-						.unwrap()
-						.iter_lits()
-						.collect_vec();
+					let vars = cnf.new_var_range(LARGE_N).iter_lits().collect_vec();
 
 					let con = CardinalityOne {
 						lits: vars
@@ -378,11 +366,7 @@ pub(crate) mod tests {
 				#[test]
 				fn test_eo_large() {
 					let mut cnf = Cnf::default();
-					let vars = cnf
-						.next_var_range(LARGE_N)
-						.unwrap()
-						.iter_lits()
-						.collect_vec();
+					let vars = cnf.new_var_range(LARGE_N).iter_lits().collect_vec();
 					let con = CardinalityOne {
 						lits: vars.clone(),
 						cmp: LimitComp::Equal,
@@ -394,11 +378,7 @@ pub(crate) mod tests {
 				#[test]
 				fn test_eo_large_neg() {
 					let mut cnf = Cnf::default();
-					let vars = cnf
-						.next_var_range(LARGE_N)
-						.unwrap()
-						.iter_lits()
-						.collect_vec();
+					let vars = cnf.new_var_range(LARGE_N).iter_lits().collect_vec();
 					let con = CardinalityOne {
 						lits: vars.clone().iter().map(|l| !l).collect_vec(),
 						cmp: LimitComp::Equal,
@@ -410,11 +390,7 @@ pub(crate) mod tests {
 				#[test]
 				fn test_eo_large_mix() {
 					let mut cnf = Cnf::default();
-					let vars = cnf
-						.next_var_range(LARGE_N)
-						.unwrap()
-						.iter_lits()
-						.collect_vec();
+					let vars = cnf.new_var_range(LARGE_N).iter_lits().collect_vec();
 					let con = CardinalityOne {
 						lits: vars
 							.clone()
diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs
index 343673ba22..715091d05e 100755
--- a/crates/pindakaas/src/lib.rs
+++ b/crates/pindakaas/src/lib.rs
@@ -32,12 +32,9 @@ use std::{
 	path::Path,
 };
 
-use itertools::Itertools;
+use itertools::{traits::HomogeneousTuple, Itertools};
 
-use crate::{
-	helpers::subscript_number,
-	solver::{NextVarRange, VarFactory},
-};
+use crate::{helpers::subscript_number, solver::VarFactory};
 
 /// Checker is a trait implemented by types that represent constraints. The
 /// [`Checker::check`] methods checks whether an assignment (often referred to
@@ -78,15 +75,54 @@ pub trait ClauseDatabase {
 		encoder.encode(self, constraint)
 	}
 
-	/// Method used to receive a new Boolean variable in the form of a positive
-	/// literal. This is a convenience method on top of [`Self::new_var`].
+	/// Create a new Boolean variable in the form of a positive literal.
 	fn new_lit(&mut self) -> Lit {
 		self.new_var().into()
 	}
 
+	/// Create multiple new Boolean literals and capture them in a tuple.
+	///
+	/// # Example
+	/// ```
+	/// # use crate::Cnf;
+	/// # let mut db = Cnf::default();
+	/// let (a, b, c) = db.new_lits();
+	/// ```
+	fn new_lits<T>(&mut self) -> T
+	where
+		T: HomogeneousTuple<Item = Lit>,
+	{
+		let range = self.new_var_range(T::num_items());
+		range.map(Lit::from).collect_tuple().unwrap()
+	}
+
+	/// Create a new Boolean variable that can be used in the encoding of a problem
+	/// or constraint.
+	fn new_var(&mut self) -> Var {
+		let mut range = self.new_var_range(1);
+		debug_assert_eq!(range.len(), 1);
+		range.next().unwrap()
+	}
+
 	/// Method to be used to receive a new Boolean variable that can be used in
 	/// the encoding of a problem or constraint.
-	fn new_var(&mut self) -> Var;
+	fn new_var_range(&mut self, len: usize) -> VarRange;
+
+	/// Create multiple new Boolean variables and capture them in a tuple.
+	///
+	/// # Example
+	/// ```
+	/// # use crate::Cnf;
+	/// # let mut db = Cnf::default();
+	/// let (a, b, c) = db.new_vars();
+	/// ```
+	fn new_vars<T>(&mut self) -> T
+	where
+		T: HomogeneousTuple<Item = Var>,
+	{
+		let range = self.new_var_range(T::num_items());
+		range.collect_tuple().unwrap()
+	}
 
 	fn with_conditions(&mut self, conditions: Vec<Lit>) -> ConditionalDatabase<Self::CondDB>;
 }
@@ -366,9 +402,15 @@ impl ClauseDatabase for Cnf {
 			Ok(())
 		}
 	}
+
 	fn new_var(&mut self) -> Var {
-		self.nvar.next().expect("exhausted variable pool")
+		self.nvar.next_var()
+	}
+
+	fn new_var_range(&mut self, len: usize) -> VarRange {
+		self.nvar.next_var_range(len)
 	}
+
 	fn with_conditions(&mut self, conditions: Vec<Lit>) -> ConditionalDatabase<Self::CondDB> {
 		ConditionalDatabase {
 			db: self,
@@ -395,12 +437,6 @@ impl Display for Cnf {
 	}
 }
 
-impl NextVarRange for Cnf {
-	fn next_var_range(&mut self, size: usize) -> Option<VarRange> {
-		self.nvar.next_var_range(size)
-	}
-}
-
 impl<'a> ExactSizeIterator for CnfIterator<'a> {}
 
 impl<'a> Iterator for CnfIterator<'a> {
@@ -443,6 +479,10 @@ impl<'a, DB: ClauseDatabase + ?Sized> ClauseDatabase for ConditionalDatabase<'a,
 		self.db.new_var()
 	}
 
+	fn new_var_range(&mut self, len: usize) -> VarRange {
+		self.db.new_var_range(len)
+	}
+
 	fn with_conditions(&mut self, mut conditions: Vec<Lit>) -> ConditionalDatabase<DB> {
 		conditions.extend(self.conditions.iter().copied());
 		ConditionalDatabase {
@@ -549,6 +589,8 @@ impl Display for Unsatisfiable {
 impl Error for Unsatisfiable {}
 
 impl Var {
+	const MAX_VARS: usize = NonZeroI32::MAX.get() as usize;
+
 	fn checked_add(&self, b: NonZeroI32) -> Option<Var> {
 		self.0
 			.get()
@@ -792,9 +834,15 @@ impl ClauseDatabase for Wcnf {
 	fn add_clause<I: IntoIterator<Item = Lit>>(&mut self, cl: I) -> Result {
 		self.add_weighted_clause(cl, None)
 	}
+
 	fn new_var(&mut self) -> Var {
 		self.cnf.new_var()
 	}
+
+	fn new_var_range(&mut self, len: usize) -> VarRange {
+		self.cnf.new_var_range(len)
+	}
+
 	fn with_conditions(&mut self, conditions: Vec<Lit>) -> ConditionalDatabase<Self::CondDB> {
 		ConditionalDatabase {
 			db: self,
@@ -831,12 +879,6 @@ impl From<Cnf> for Wcnf {
 	}
 }
 
-impl NextVarRange for Wcnf {
-	fn next_var_range(&mut self, size: usize) -> Option<VarRange> {
-		self.cnf.next_var_range(size)
-	}
-}
-
 impl From<Lit> for i32 {
 	fn from(val: Lit) -> Self {
 		val.0.get()
@@ -853,28 +895,25 @@ impl From<Var> for i32 {
 mod tests {
 	use std::num::NonZeroI32;
 
-	use crate::{
-		solver::{NextVarRange, VarFactory},
-		Lit, Var,
-	};
+	use crate::{solver::VarFactory, Lit, Var};
 
 	#[test]
 	fn test_var_range() {
 		let mut factory = VarFactory::default();
 
-		let range = factory.next_var_range(0).unwrap();
+		let range = factory.next_var_range(0);
 		assert_eq!(range.len(), 0);
 		assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(1).unwrap())));
 
-		let range = factory.next_var_range(1).unwrap();
+		let range = factory.next_var_range(1);
 		assert_eq!(range.len(), 1);
 		assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(2).unwrap())));
 
-		let range = factory.next_var_range(2).unwrap();
+		let range = factory.next_var_range(2);
 		assert_eq!(range.len(), 2);
 		assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(4).unwrap())));
 
-		let range = factory.next_var_range(100).unwrap();
+		let range = factory.next_var_range(100);
 		assert_eq!(range.len(), 100);
 		assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(104).unwrap())));
 	}
diff --git a/crates/pindakaas/src/propositional_logic.rs b/crates/pindakaas/src/propositional_logic.rs
index 14c6e17e02..2368eb85cd 100644
--- a/crates/pindakaas/src/propositional_logic.rs
+++ b/crates/pindakaas/src/propositional_logic.rs
@@ -349,7 +349,6 @@ mod tests {
 	use crate::{
 		helpers::tests::{assert_encoding, assert_solutions, expect_file},
 		propositional_logic::{Formula, TseitinEncoder},
-		solver::NextVarRange,
 		ClauseDatabase, Cnf, Encoder,
 	};
 
@@ -357,12 +356,7 @@ mod tests {
 	fn encode_prop_and() {
 		// Simple conjunction
 		let mut cnf = Cnf::default();
-		let (a, b, c) = cnf
-			.next_var_range(3)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c) = cnf.new_lits();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -382,12 +376,7 @@ mod tests {
 
 		// Reified conjunction
 		let mut cnf = Cnf::default();
-		let (a, b, c) = cnf
-			.next_var_range(3)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c) = cnf.new_lits();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -433,7 +422,7 @@ mod tests {
 	fn encode_prop_equiv() {
 		// Simple equivalence
 		let mut cnf = Cnf::default();
-		let vars = cnf.next_var_range(4).unwrap().iter_lits().collect_vec();
+		let vars = cnf.new_var_range(4).iter_lits().collect_vec();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -453,12 +442,7 @@ mod tests {
 
 		// Reified equivalence
 		let mut cnf = Cnf::default();
-		let (a, b, c) = cnf
-			.next_var_range(3)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c) = cnf.new_lits();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -505,12 +489,7 @@ mod tests {
 
 		// Reified implication
 		let mut cnf = Cnf::default();
-		let (a, b, c) = cnf
-			.next_var_range(3)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c) = cnf.new_lits();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -536,12 +515,7 @@ mod tests {
 	fn encode_prop_ite() {
 		// Simple if-then-else
 		let mut cnf = Cnf::default();
-		let (a, b, c) = cnf
-			.next_var_range(3)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c) = cnf.new_lits();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -565,12 +539,7 @@ mod tests {
 
 		// Reified if-then-else
 		let mut cnf = Cnf::default();
-		let (a, b, c, d) = cnf
-			.next_var_range(4)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d) = cnf.new_lits();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -627,12 +596,7 @@ mod tests {
 	fn encode_prop_or() {
 		// Simple disjunction
 		let mut cnf = Cnf::default();
-		let (a, b, c) = cnf
-			.next_var_range(3)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c) = cnf.new_lits();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -652,12 +616,7 @@ mod tests {
 
 		// Reified disjunction
 		let mut cnf = Cnf::default();
-		let (a, b, c) = cnf
-			.next_var_range(3)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c) = cnf.new_lits();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -703,7 +662,7 @@ mod tests {
 	fn encode_prop_xor() {
 		// Simple XOR
 		let mut cnf = Cnf::default();
-		let vars = cnf.next_var_range(3).unwrap().iter_lits().collect_vec();
+		let vars = cnf.new_var_range(3).iter_lits().collect_vec();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -723,12 +682,7 @@ mod tests {
 
 		// Reified XOR
 		let mut cnf = Cnf::default();
-		let (a, b, c, d) = cnf
-			.next_var_range(4)
-			.unwrap()
-			.iter_lits()
-			.collect_tuple()
-			.unwrap();
+		let (a, b, c, d) = cnf.new_lits();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -773,7 +727,7 @@ mod tests {
 		);
 		// Regression test: negated XOR (negated args)
 		let mut cnf = Cnf::default();
-		let vars = cnf.next_var_range(3).unwrap().iter_lits().collect_vec();
+		let vars = cnf.new_var_range(3).iter_lits().collect_vec();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
@@ -790,7 +744,7 @@ mod tests {
 		);
 		// Regression test: negated XOR (negated binding)
 		let mut cnf = Cnf::default();
-		let vars = cnf.next_var_range(4).unwrap().iter_lits().collect_vec();
+		let vars = cnf.new_var_range(4).iter_lits().collect_vec();
 		TseitinEncoder
 			.encode(
 				&mut cnf,
diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs
index d431747652..20ff55f3d5 100644
--- a/crates/pindakaas/src/solver.rs
+++ b/crates/pindakaas/src/solver.rs
@@ -52,15 +52,6 @@ pub trait LearnCallback: Solver {
 	);
 }
 
-/// Allow request for sequential ranges of variables.
-pub trait NextVarRange {
-	/// Request the next sequential range of variables.
-	///
-	/// The method is can return [`None`] if the range of the requested [`size`] is not
-	/// available.
-	fn next_var_range(&mut self, size: usize) -> Option<VarRange>;
-}
-
 #[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)]
 pub enum SlvTermSignal {
 	Continue,
@@ -206,61 +197,59 @@ impl Drop for FFIPointer {
 }
 
 impl VarFactory {
-	const MAX_VARS: usize = NonZeroI32::MAX.get() as usize;
-
 	pub fn emited_vars(&self) -> usize {
 		if let Some(x) = self.next_var {
 			x.0.get() as usize - 1
 		} else {
-			Self::MAX_VARS
-		}
-	}
-}
-
-impl Default for VarFactory {
-	fn default() -> Self {
-		Self {
-			next_var: Some(Var(NonZeroI32::new(1).unwrap())),
+			Var::MAX_VARS
 		}
 	}
-}
-
-impl Iterator for VarFactory {
-	type Item = Var;
 
-	fn next(&mut self) -> Option<Self::Item> {
-		let var = self.next_var;
-		if let Some(var) = var {
-			self.next_var = var.next_var();
+	pub(crate) fn next_var(&mut self) -> Var {
+		if let Some(x) = self.next_var {
+			self.next_var = x.next_var();
+			x
+		} else {
+			panic!("unable to create more than `Var::MAX_VARS` variables")
 		}
-		var
 	}
-}
 
-impl NextVarRange for VarFactory {
-	fn next_var_range(&mut self, size: usize) -> Option<VarRange> {
-		let start = self.next_var?;
+	pub(crate) fn next_var_range(&mut self, size: usize) -> VarRange {
+		let Some(start) = self.next_var else {
+			panic!("unable to create more than `Var::MAX_VARS` variables")
+		};
 		match size {
-			0 => Some(VarRange::new(
+			0 => VarRange::new(
 				Var(NonZeroI32::new(2).unwrap()),
 				Var(NonZeroI32::new(1).unwrap()),
-			)),
+			),
 			1 => {
 				self.next_var = start.next_var();
-				Some(VarRange::new(start, start))
+				VarRange::new(start, start)
+			}
+			_ if size > Var::MAX_VARS => {
+				panic!("unable to create more than `Var::MAX_VARS` variables")
 			}
-			_ if size > NonZeroI32::MAX.get() as usize => None,
 			_ => {
 				// 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) {
 					// Set self.next_var to one after end
 					self.next_var = end.next_var();
-					Some(VarRange::new(start, end))
+					VarRange::new(start, end)
 				} else {
-					None
+					// If end is None, then the range is too large
+					panic!("unable to create more than `Var::MAX_VARS` variables")
 				}
 			}
 		}
 	}
 }
+
+impl Default for VarFactory {
+	fn default() -> Self {
+		Self {
+			next_var: Some(Var(NonZeroI32::new(1).unwrap())),
+		}
+	}
+}
diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs
index 832e5cc1b8..5ec659cba3 100644
--- a/crates/pindakaas/src/solver/cadical.rs
+++ b/crates/pindakaas/src/solver/cadical.rs
@@ -169,14 +169,14 @@ mod tests {
 					ClausePersistence, PropagatingSolver, Propagator, PropagatorAccess,
 					SolvingActions,
 				},
-				NextVarRange, VarRange,
+				VarRange,
 			},
 			Lit,
 		};
 
 		let mut slv = Cadical::default();
 
-		let vars = slv.next_var_range(5).unwrap();
+		let vars = slv.new_var_range(5);
 
 		struct Dist2 {
 			vars: VarRange,
diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs
index 3652de14d9..2b6c5a3f39 100644
--- a/crates/pindakaas/src/solver/libloading.rs
+++ b/crates/pindakaas/src/solver/libloading.rs
@@ -238,9 +238,15 @@ impl<'lib> ClauseDatabase for IpasirSolver<'lib> {
 		}
 		Ok(())
 	}
+
 	fn new_var(&mut self) -> Var {
-		self.vars.next().expect("variable pool exhaused")
+		self.vars.next_var()
+	}
+
+	fn new_var_range(&mut self, len: usize) -> crate::VarRange {
+		self.vars.next_var_range(len)
 	}
+
 	fn with_conditions(&mut self, conditions: Vec<Lit>) -> ConditionalDatabase<Self::CondDB> {
 		ConditionalDatabase {
 			db: self,
diff --git a/crates/pindakaas/src/solver/splr.rs b/crates/pindakaas/src/solver/splr.rs
index d29aba1a68..5533d16835 100644
--- a/crates/pindakaas/src/solver/splr.rs
+++ b/crates/pindakaas/src/solver/splr.rs
@@ -6,7 +6,7 @@ use splr::{Certificate, SatSolverIF, SolveIF, VERSION};
 use crate::{
 	helpers::const_concat,
 	solver::{SolveResult, Solver},
-	ClauseDatabase, Cnf, ConditionalDatabase, Lit, Valuation, Var,
+	ClauseDatabase, Cnf, ConditionalDatabase, Lit, Valuation, Var, VarRange,
 };
 
 impl Valuation for Certificate {
@@ -52,6 +52,17 @@ impl ClauseDatabase for Splr {
 		Var(NonZeroI32::new(var).expect("variables cannot use the value zero"))
 	}
 
+	fn new_var_range(&mut self, len: usize) -> VarRange {
+		let start = self.new_var();
+		let mut last = start;
+		for _ in 1..len {
+			let x = self.new_var();
+			debug_assert_eq!(i32::from(last) + 1, i32::from(x));
+			last = x;
+		}
+		VarRange::new(start, last)
+	}
+
 	fn with_conditions(&mut self, conditions: Vec<Lit>) -> ConditionalDatabase<Self::CondDB> {
 		ConditionalDatabase {
 			db: self,
diff --git a/crates/pindakaas/src/sorted.rs b/crates/pindakaas/src/sorted.rs
index b1e3646ca8..56c05760a3 100644
--- a/crates/pindakaas/src/sorted.rs
+++ b/crates/pindakaas/src/sorted.rs
@@ -571,7 +571,6 @@ mod tests {
 		bool_linear::LimitComp,
 		helpers::tests::{assert_solutions, expect_file},
 		integer::{IntVarEnc, IntVarOrd, TernLeConstraint},
-		solver::NextVarRange,
 		sorted::{Sorted, SortedEncoder, SortedStrategy},
 		ClauseDatabase, Cnf, Encoder, Var, VarRange,
 	};
@@ -672,7 +671,7 @@ mod tests {
 	#[test]
 	fn test_4_sorted_eq() {
 		let mut cnf = Cnf::default();
-		let lits = cnf.next_var_range(4).unwrap().iter_lits().collect_vec();
+		let lits = cnf.new_var_range(4).iter_lits().collect_vec();
 		let y: IntVarEnc = IntVarOrd::from_bounds(&mut cnf, 0, 4, String::from("y")).into();
 		let vars = VarRange::new(
 			Var(NonZeroI32::new(1).unwrap()),
@@ -691,7 +690,7 @@ mod tests {
 	#[test]
 	fn test_4_2_sorted_eq() {
 		let mut cnf = Cnf::default();
-		let lits = cnf.next_var_range(4).unwrap().iter_lits().collect_vec();
+		let lits = cnf.new_var_range(4).iter_lits().collect_vec();
 		let y: IntVarEnc = IntVarOrd::from_bounds(&mut cnf, 0, 2, String::from("y")).into();
 		let vars = VarRange::new(
 			Var(NonZeroI32::new(1).unwrap()),
@@ -710,7 +709,7 @@ mod tests {
 	#[test]
 	fn test_4_3_sorted_eq() {
 		let mut cnf = Cnf::default();
-		let lits = cnf.next_var_range(4).unwrap().iter_lits().collect_vec();
+		let lits = cnf.new_var_range(4).iter_lits().collect_vec();
 		let y: IntVarEnc = IntVarOrd::from_bounds(&mut cnf, 0, 3, String::from("y")).into();
 		let vars = VarRange::new(
 			Var(NonZeroI32::new(1).unwrap()),
@@ -729,7 +728,7 @@ mod tests {
 	#[test]
 	fn test_5_sorted_eq() {
 		let mut cnf = Cnf::default();
-		let lits = cnf.next_var_range(5).unwrap().iter_lits().collect_vec();
+		let lits = cnf.new_var_range(5).iter_lits().collect_vec();
 		let y: IntVarEnc = IntVarOrd::from_bounds(&mut cnf, 0, 5, String::from("y")).into();
 		let vars = VarRange::new(
 			Var(NonZeroI32::new(1).unwrap()),
@@ -748,7 +747,7 @@ mod tests {
 	#[test]
 	fn test_5_3_sorted_eq() {
 		let mut cnf = Cnf::default();
-		let lits = cnf.next_var_range(5).unwrap().iter_lits().collect_vec();
+		let lits = cnf.new_var_range(5).iter_lits().collect_vec();
 		let y: IntVarEnc = IntVarOrd::from_bounds(&mut cnf, 0, 3, String::from("y")).into();
 		let vars = VarRange::new(
 			Var(NonZeroI32::new(1).unwrap()),
@@ -767,12 +766,7 @@ mod tests {
 	#[test]
 	fn test_5_1_sorted_eq_negated() {
 		let mut cnf = Cnf::default();
-		let lits = cnf
-			.next_var_range(5)
-			.unwrap()
-			.iter_lits()
-			.map(|l| !l)
-			.collect_vec();
+		let lits = cnf.new_var_range(5).iter_lits().map(|l| !l).collect_vec();
 		let y: IntVarEnc = IntVarOrd::from_bounds(&mut cnf, 0, 1, String::from("y")).into();
 		let vars = VarRange::new(
 			Var(NonZeroI32::new(1).unwrap()),