From 5c6146e5f6c6fa84d5d7793d2545ad1a0a1f376a Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Thu, 4 Apr 2024 11:35:13 +1100 Subject: [PATCH] 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,