From 5a889041062a61ac8a2c87fbeb36f60fd37b22b9 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 16 Jan 2024 20:53:37 +1100 Subject: [PATCH] Add IPASIR-UP feature and small test case --- crates/pindakaas-derive/src/lib.rs | 7 +- crates/pindakaas/Cargo.toml | 9 ++- crates/pindakaas/src/helpers.rs | 77 +++++++++++++++++++- crates/pindakaas/src/lib.rs | 17 ++++- crates/pindakaas/src/solver.rs | 40 +++++++--- crates/pindakaas/src/solver/cadical.rs | 89 ++++++++++++++++++++++- crates/pindakaas/src/solver/libloading.rs | 24 +++++- 7 files changed, 237 insertions(+), 26 deletions(-) diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs index 0775a84f87..28077edacb 100644 --- a/crates/pindakaas-derive/src/lib.rs +++ b/crates/pindakaas-derive/src/lib.rs @@ -147,6 +147,7 @@ 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, @@ -154,12 +155,14 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { 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, 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 { + pub fn new_var_range(&mut self, size: usize) -> crate::helpers::VarRange { self.vars.new_var_range(size).expect("variable pool exhaused") } } diff --git a/crates/pindakaas/Cargo.toml b/crates/pindakaas/Cargo.toml index 07c42760ba..33cd9214cd 100644 --- a/crates/pindakaas/Cargo.toml +++ b/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"] diff --git a/crates/pindakaas/src/helpers.rs b/crates/pindakaas/src/helpers.rs index 1f75af88c7..f2dbef6c63 100644 --- a/crates/pindakaas/src/helpers.rs +++ b/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 { + 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) { + 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 { + if self.start <= self.end { + let item = self.end; + self.end = self.end.prev_var().unwrap(); + Some(item) + } else { + None + } + } +} +impl RangeBounds for VarRange { + fn start_bound(&self) -> Bound<&Var> { + Bound::Included(&self.start) + } + + fn end_bound(&self) -> Bound<&Var> { + Bound::Included(&self.end) + } +} +impl From> for VarRange { + fn from(value: RangeInclusive) -> Self { + VarRange::new(*value.start(), *value.end()) + } +} + #[cfg(test)] pub mod tests { use std::{ diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs index 62bc7c888d..e63de33f40 100755 --- a/crates/pindakaas/src/lib.rs +++ b/crates/pindakaas/src/lib.rs @@ -48,11 +48,24 @@ pub struct Var(pub(crate) NonZeroI32); impl Var { fn next_var(&self) -> Option { - self.checked_add(NonZeroI32::new(1).unwrap()) + const ONE: NonZeroI32 = unsafe { NonZeroI32::new_unchecked(1) }; + self.checked_add(ONE) + } + + fn prev_var(&self) -> Option { + let prev = self.0.get() - 1; + if prev >= 0 { + Some(Var(NonZeroI32::new(prev).unwrap())) + } else { + None + } } fn checked_add(&self, b: NonZeroI32) -> Option { - 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())) } } diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 60c94fd179..4fcb32b3c9 100644 --- a/crates/pindakaas/src/solver.rs +++ b/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 SlvTermSignal>(&mut self, cb: Option); } +#[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 { + fn propagate(&mut self, slv: &mut dyn SolvingActions) -> Vec { + 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 { + fn add_reason_clause(&mut self, propagated_lit: Lit) -> Vec { + 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> { + pub fn new_var_range(&mut self, size: usize) -> Option { 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 } diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index df327037e9..1168545c28 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -8,6 +8,7 @@ use crate::Lit; pub struct Cadical { ptr: *mut std::ffi::c_void, vars: VarFactory, + #[cfg(feature = "ipasir-up")] prop: Option>, } @@ -16,6 +17,7 @@ impl Default for Cadical { Self { ptr: unsafe { pindakaas_cadical::ipasir_init() }, vars: VarFactory::default(), + #[cfg(feature = "ipasir-up")] prop: None, } } @@ -39,7 +41,7 @@ mod tests { use super::*; use crate::{ linear::LimitComp, - solver::{PropagatingSolver, Propagator, SolveResult, Solver}, + solver::{SolveResult, Solver}, CardinalityOne, ClauseDatabase, Encoder, PairwiseEncoder, }; @@ -67,4 +69,89 @@ mod tests { }); assert_eq!(res, SolveResult::Sat); } + + #[cfg(feature = "ipasir-up")] + #[test] + fn test_ipasir_up() { + use itertools::Itertools; + + use crate::{ + helpers::tests::lits, + solver::{PropagatingSolver, Propagator, VarRange}, + }; + + let mut slv = Cadical::default(); + + let vars = slv.new_var_range(5); + + struct Dist2 { + vars: VarRange, + tmp: Vec>, + } + impl Propagator for Dist2 { + fn is_lazy(&self) -> bool { + true + } + fn check_model(&mut self, value: &dyn crate::Valuation) -> bool { + let mut vars = self.vars.clone(); + while let Some(v) = vars.next() { + if value(v.into()).unwrap_or(true) { + let next_2 = vars.clone().take(2); + for o in next_2 { + if value(o.into()).unwrap_or(true) { + self.tmp.push(vec![!v, !o]); + } + } + } + } + self.tmp.is_empty() + } + fn add_external_clause(&mut self) -> Option> { + self.tmp.pop() + } + } + + let p = Box::new(Dist2 { + vars: vars.clone(), + tmp: Vec::new(), + }); + slv.set_external_propagator(Some(p)); + slv.add_clause(vars.clone().map_into()).unwrap(); + for v in vars.clone() { + slv.add_observed_var(v) + } + + let mut solns = Vec::new(); + while slv.solve(|value| { + let sol: Vec = vars + .clone() + .map(|v| { + if value(v.into()).unwrap() { + v.into() + } else { + !v + } + }) + .collect_vec(); + solns.push(sol); + }) == SolveResult::Sat + { + slv.add_clause(solns.last().unwrap().iter().map(|l| !l)) + .unwrap() + } + solns.sort(); + assert_eq!( + solns, + vec![ + lits![1, -2, -3, 4, -5], + lits![1, -2, -3, -4, 5], + lits![1, -2, -3, -4, -5], + lits![-1, 2, -3, -4, 5], + lits![-1, 2, -3, -4, -5], + lits![-1, -2, 3, -4, -5], + lits![-1, -2, -3, 4, -5], + lits![-1, -2, -3, -4, 5], + ] + ); + } } diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index c5ffdc8ef4..12d1f870d0 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -1,5 +1,6 @@ +#[cfg(feature = "ipasir-up")] +use std::collections::VecDeque; use std::{ - collections::VecDeque, ffi::{c_char, c_int, c_void, CStr}, num::NonZeroI32, ptr, @@ -8,9 +9,11 @@ use std::{ use libloading::{Library, Symbol}; use super::{ - FailFn, LearnCallback, Propagator, SlvTermSignal, SolveAssuming, SolveResult, Solver, - SolvingActions, TermCallback, VarFactory, + FailFn, LearnCallback, SlvTermSignal, SolveAssuming, SolveResult, Solver, TermCallback, + VarFactory, }; +#[cfg(feature = "ipasir-up")] +use super::{Propagator, SolvingActions}; use crate::{ClauseDatabase, Lit, Result, Valuation, Var}; pub struct IpasirLibrary { @@ -295,10 +298,14 @@ impl Iterator for ExplIter { } } +#[cfg(feature = "ipasir-up")] #[derive(Debug, Clone, Copy)] pub(crate) struct NoProp; + +#[cfg(feature = "ipasir-up")] impl Propagator for NoProp {} +#[cfg(feature = "ipasir-up")] pub(crate) struct IpasirPropStore { /// Rust Propagator pub(crate) prop: Box, @@ -313,6 +320,7 @@ pub(crate) struct IpasirPropStore { pub(crate) cqueue: Option>, } +#[cfg(feature = "ipasir-up")] impl IpasirPropStore { pub(crate) fn new(prop: Box, slv: *mut dyn SolvingActions) -> Self { Self { @@ -328,6 +336,7 @@ impl IpasirPropStore { // --- Callback functions for C propagator interface --- +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( state: *mut c_void, lit: i32, @@ -337,10 +346,12 @@ pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( let lit = crate::Lit(std::num::NonZeroI32::new(lit).unwrap()); prop.prop.notify_assignment(lit, is_fixed) } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb(state: *mut c_void) { let prop = &mut *(state as *mut IpasirPropStore); prop.prop.notify_new_decision_level() } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb(state: *mut c_void, level: usize) { let prop = &mut *(state as *mut IpasirPropStore); prop.pqueue.clear(); @@ -349,6 +360,7 @@ pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb(state: *mut c_void, l prop.cqueue = None; prop.prop.notify_backtrack(level); } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_check_model_cb( state: *mut c_void, len: usize, @@ -369,6 +381,7 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb( }; prop.prop.check_model(&value) } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_void) -> i32 { let prop = &mut *(state as *mut IpasirPropStore); if let Some(l) = prop.prop.decide() { @@ -377,6 +390,7 @@ pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_void) -> i32 { 0 } } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_propagate_cb(state: *mut c_void) -> i32 { let prop = &mut *(state as *mut IpasirPropStore); if prop.pqueue.is_empty() { @@ -389,6 +403,7 @@ pub(crate) unsafe extern "C" fn ipasir_propagate_cb(state: *mut c_void) -> i32 { 0 // No propagation } } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb( state: *mut c_void, propagated_lit: i32, @@ -409,12 +424,13 @@ pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb( 0 } } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_has_external_clause_cb(state: *mut c_void) -> bool { let prop = &mut *(state as *mut IpasirPropStore); prop.cqueue = prop.prop.add_external_clause().map(Vec::into); prop.cqueue.is_some() } - +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_add_external_clause_lit_cb(state: *mut c_void) -> i32 { let prop = &mut *(state as *mut IpasirPropStore); if prop.cqueue.is_none() {