From 378f6b2f9f1bbbbefda28dce21a484fe4343ca78 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Thu, 4 Apr 2024 11:17:50 +1100 Subject: [PATCH 1/2] Fix next_var_range for length 1 and add test cases --- crates/pindakaas/src/solver.rs | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 30055537f6..e2d7ef6d5d 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -260,6 +260,10 @@ impl VarFactory { Var(NonZeroI32::new(2).unwrap()), Var(NonZeroI32::new(1).unwrap()), )), + 1 => { + self.next_var = start.next_var(); + Some(VarRange::new(start, start)) + } _ if size > NonZeroI32::MAX.get() as usize => None, _ => { // Size is reduced by 1 since it includes self.next_var @@ -295,3 +299,33 @@ impl Iterator for VarFactory { var } } + +#[cfg(test)] +mod tests { + use std::num::NonZeroI32; + + use crate::Var; + + use super::VarFactory; + + #[test] + fn test_var_range() { + let mut factory = VarFactory::default(); + + let range = factory.new_var_range(0).unwrap(); + assert_eq!(range.len(), 0); + assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(1).unwrap()))); + + let range = factory.new_var_range(1).unwrap(); + assert_eq!(range.len(), 1); + assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(2).unwrap()))); + + let range = factory.new_var_range(2).unwrap(); + assert_eq!(range.len(), 2); + assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(4).unwrap()))); + + let range = factory.new_var_range(100).unwrap(); + assert_eq!(range.len(), 100); + assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(104).unwrap()))); + } +} From 5c6146e5f6c6fa84d5d7793d2545ad1a0a1f376a Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Thu, 4 Apr 2024 11:35:13 +1100 Subject: [PATCH 2/2] Add trait for creating VarRange objects --- crates/pindakaas-derive/src/lib.rs | 7 ++- crates/pindakaas/src/lib.rs | 20 ++++---- crates/pindakaas/src/solver.rs | 69 +++++++++++++++----------- crates/pindakaas/src/solver/cadical.rs | 4 +- 4 files changed, 56 insertions(+), 44 deletions(-) diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs index f993f40869..cd76b64b07 100644 --- a/crates/pindakaas-derive/src/lib.rs +++ b/crates/pindakaas-derive/src/lib.rs @@ -299,10 +299,9 @@ 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) -> crate::helpers::VarRange { - #vars .new_var_range(size).expect("variable pool exhaused") + impl crate::solver::NextVarRange for #ident { + fn next_var_range(&mut self, size: usize) -> Option { + #vars .next_var_range(size) } } diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs index 9804fb76db..e606755b6f 100755 --- a/crates/pindakaas/src/lib.rs +++ b/crates/pindakaas/src/lib.rs @@ -22,7 +22,7 @@ use std::{ use helpers::VarRange; use itertools::{Itertools, Position}; -use solver::VarFactory; +use solver::{NextVarRange, VarFactory}; mod cardinality; mod cardinality_one; @@ -382,11 +382,11 @@ impl Cnf { pub fn literals(&self) -> usize { self.size.iter().sum() } +} - pub fn new_var_range(&mut self, size: usize) -> VarRange { - self.nvar - .new_var_range(size) - .expect("exhausted variable pool") +impl NextVarRange for Cnf { + fn next_var_range(&mut self, size: usize) -> Option { + self.nvar.next_var_range(size) } } @@ -656,10 +656,6 @@ impl Wcnf { pub fn iter(&self) -> impl Iterator)> { self.cnf.iter().zip(self.weights.iter()) } - - pub fn new_var_range(&mut self, size: usize) -> VarRange { - self.cnf.new_var_range(size) - } } impl ClauseDatabase for Wcnf { @@ -671,6 +667,12 @@ impl ClauseDatabase for Wcnf { } } +impl NextVarRange for Wcnf { + fn next_var_range(&mut self, size: usize) -> Option { + self.cnf.next_var_range(size) + } +} + impl Cnf { pub fn iter(&self) -> CnfIterator<'_> { CnfIterator { diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index e2d7ef6d5d..5cdcf3db5e 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -251,9 +251,39 @@ impl VarFactory { Self::MAX_VARS } } +} + +impl Default for VarFactory { + fn default() -> Self { + Self { + next_var: Some(Var(NonZeroI32::new(1).unwrap())), + } + } +} + +impl Iterator for VarFactory { + type Item = Var; - /// Return the next [`size`] variables that can be stored as an inclusive range. - pub fn new_var_range(&mut self, size: usize) -> Option { + fn next(&mut self) -> Option { + let var = self.next_var; + if let Some(var) = var { + self.next_var = var.next_var(); + } + var + } +} + +/// 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; +} + +impl NextVarRange for VarFactory { + fn next_var_range(&mut self, size: usize) -> Option { let start = self.next_var?; match size { 0 => Some(VarRange::new( @@ -280,51 +310,32 @@ impl VarFactory { } } -impl Default for VarFactory { - fn default() -> Self { - Self { - next_var: Some(Var(NonZeroI32::new(1).unwrap())), - } - } -} - -impl Iterator for VarFactory { - type Item = Var; - - fn next(&mut self) -> Option { - let var = self.next_var; - if let Some(var) = var { - self.next_var = var.next_var(); - } - var - } -} - #[cfg(test)] mod tests { use std::num::NonZeroI32; - use crate::Var; - - use super::VarFactory; + use crate::{ + solver::{NextVarRange, VarFactory}, + Var, + }; #[test] fn test_var_range() { let mut factory = VarFactory::default(); - let range = factory.new_var_range(0).unwrap(); + let range = factory.next_var_range(0).unwrap(); assert_eq!(range.len(), 0); assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(1).unwrap()))); - let range = factory.new_var_range(1).unwrap(); + let range = factory.next_var_range(1).unwrap(); assert_eq!(range.len(), 1); assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(2).unwrap()))); - let range = factory.new_var_range(2).unwrap(); + let range = factory.next_var_range(2).unwrap(); assert_eq!(range.len(), 2); assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(4).unwrap()))); - let range = factory.new_var_range(100).unwrap(); + let range = factory.next_var_range(100).unwrap(); assert_eq!(range.len(), 100); assert_eq!(factory.next_var, Some(Var(NonZeroI32::new(104).unwrap()))); } diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index db261fd0dd..8cd19a1c25 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -100,12 +100,12 @@ mod tests { use crate::{ helpers::tests::lits, - solver::{PropagatingSolver, Propagator, VarRange}, + solver::{NextVarRange, PropagatingSolver, Propagator, VarRange}, }; let mut slv = Cadical::default(); - let vars = slv.new_var_range(5); + let vars = slv.next_var_range(5).unwrap(); struct Dist2 { vars: VarRange,