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()),