From 69a66c31b99cd0bcd6b7f5052d6e19233a03182a Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Thu, 27 Jun 2024 10:16:23 +1000 Subject: [PATCH] ipasir-up: fix SolverAction implementation --- crates/pindakaas-derive/src/lib.rs | 114 +++++++++++++++++----- crates/pindakaas/src/solver/cadical.rs | 15 ++- crates/pindakaas/src/solver/libloading.rs | 60 +++++++----- 3 files changed, 138 insertions(+), 51 deletions(-) diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs index 2fd5e8f289..59058f8325 100644 --- a/crates/pindakaas-derive/src/lib.rs +++ b/crates/pindakaas-derive/src/lib.rs @@ -106,7 +106,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { cb: Option, ) { if let Some(mut cb) = cb { - let mut wrapped_cb = move || -> std::ffi::c_int { + let wrapped_cb = move || -> std::ffi::c_int { match cb() { crate::solver::SlvTermSignal::Continue => std::ffi::c_int::from(0), crate::solver::SlvTermSignal::Terminate => std::ffi::c_int::from(1), @@ -159,7 +159,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { ) { const MAX_LEN: std::ffi::c_int = 512; if let Some(mut cb) = cb { - let mut wrapped_cb = move |clause: *const i32| { + let wrapped_cb = move |clause: *const i32| { let mut iter = crate::solver::libloading::ExplIter(clause) .map(|i: i32| crate::Lit(std::num::NonZeroI32::new(i).unwrap())); cb(&mut iter) @@ -201,6 +201,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { let sol_ident = format_ident!("{}Sol", ident); let ipasir_up = if opts.ipasir_up { let prop_ident = format_ident!("{}Prop", ident); + let actions_ident = format_ident!("{}SolvingActions", ident); let prop_member = match opts.prop { Some(x) => quote! { self. #x }, None => quote! { self.prop }, @@ -226,9 +227,9 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { #[cfg(feature = "ipasir-up")] impl #prop_ident { - pub(crate) fn new(prop: P, slv: *mut dyn crate::solver::SolvingActions) -> Self { + pub(crate) fn new(prop: P, slv: #actions_ident) -> Self { // Construct wrapping structures - let prop = crate::solver::libloading::IpasirPropStore::

::new(prop, slv); + let prop = crate::solver::libloading::IpasirPropStore::new(prop, slv); let drop_prop = |x: *mut std::ffi::c_void| { let prop = unsafe { Box::

::from_raw(x as *mut P) }; drop(prop); @@ -240,15 +241,15 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { let wrapper = unsafe { #krate::ipasir_prop_init(data as *mut std::ffi::c_void) }; // Set function pointers for methods - unsafe { #krate::ipasir_prop_set_notify_assignment(wrapper, Some(crate::solver::libloading::ipasir_notify_assignment_cb::

)) }; - unsafe { #krate::ipasir_prop_set_notify_new_decision_level(wrapper, Some(crate::solver::libloading::ipasir_notify_new_decision_level_cb::

)) }; - unsafe { #krate::ipasir_prop_set_notify_backtrack(wrapper, Some(crate::solver::libloading::ipasir_notify_backtrack_cb::

)) }; - unsafe { #krate::ipasir_prop_set_check_model(wrapper, Some(crate::solver::libloading::ipasir_check_model_cb::

)) }; - unsafe { #krate::ipasir_prop_set_decide(wrapper, Some(crate::solver::libloading::ipasir_decide_cb::

)) }; - unsafe { #krate::ipasir_prop_set_propagate(wrapper, Some(crate::solver::libloading::ipasir_propagate_cb::

)) }; - unsafe { #krate::ipasir_prop_set_add_reason_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_reason_clause_lit_cb::

)) }; - unsafe { #krate::ipasir_prop_set_has_external_clause(wrapper, Some(crate::solver::libloading::ipasir_has_external_clause_cb::

)) }; - unsafe { #krate::ipasir_prop_set_add_external_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_external_clause_lit_cb::

)) }; + unsafe { #krate::ipasir_prop_set_notify_assignment(wrapper, Some(crate::solver::libloading::ipasir_notify_assignment_cb::)) }; + unsafe { #krate::ipasir_prop_set_notify_new_decision_level(wrapper, Some(crate::solver::libloading::ipasir_notify_new_decision_level_cb::)) }; + unsafe { #krate::ipasir_prop_set_notify_backtrack(wrapper, Some(crate::solver::libloading::ipasir_notify_backtrack_cb::)) }; + unsafe { #krate::ipasir_prop_set_check_model(wrapper, Some(crate::solver::libloading::ipasir_check_model_cb::)) }; + unsafe { #krate::ipasir_prop_set_decide(wrapper, Some(crate::solver::libloading::ipasir_decide_cb::)) }; + unsafe { #krate::ipasir_prop_set_propagate(wrapper, Some(crate::solver::libloading::ipasir_propagate_cb::)) }; + unsafe { #krate::ipasir_prop_set_add_reason_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_reason_clause_lit_cb::)) }; + unsafe { #krate::ipasir_prop_set_has_external_clause(wrapper, Some(crate::solver::libloading::ipasir_has_external_clause_cb::)) }; + unsafe { #krate::ipasir_prop_set_add_external_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_external_clause_lit_cb::)) }; Self { prop: data, drop_prop, access_prop, wrapper, } } @@ -268,7 +269,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } // If new propagator, set it now if let Some(p) = prop { - #prop_member = Some(#prop_ident ::new(p, (self as *mut _))); + #prop_member = Some(#prop_ident ::new(p, #actions_ident::new(#ptr, Arc::clone(&#vars)))); unsafe { #krate::ipasir_connect_external_propagator( #ptr, #prop_member .as_ref().unwrap().wrapper ) }; } } @@ -299,15 +300,28 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } #[cfg(feature = "ipasir-up")] - impl crate::solver::SolvingActions for #ident { + pub(crate) struct #actions_ident { + ptr: *mut std::ffi::c_void, + vars: Arc>, + } + + #[cfg(feature = "ipasir-up")] + impl #actions_ident { + pub fn new(ptr: *mut std::ffi::c_void, vars: Arc>) -> Self { + Self { ptr, vars } + } + } + + #[cfg(feature = "ipasir-up")] + impl crate::solver::SolvingActions for #actions_ident { fn new_var(&mut self) -> crate::Var { - <#ident as crate::ClauseDatabase>::new_var(self) + self.vars.as_ref().lock().unwrap().next().expect("variable pool exhaused") } fn add_observed_var(&mut self, var: crate::Var) { - <#ident as crate::solver::PropagatingSolver>::add_observed_var(self, var) + unsafe { #krate::ipasir_add_observed_var( self.ptr, var.0.get()) }; } fn is_decision(&mut self, lit: crate::Lit) -> bool { - unsafe { #krate::ipasir_is_decision( #ptr, lit.0.get() ) } + unsafe { #krate::ipasir_is_decision( self.ptr, lit.0.get() ) } } } @@ -363,12 +377,68 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } }; + let new_var = if opts.ipasir_up { + quote! { + fn new_var(&mut self) -> crate::Var { + #[cfg(feature = "ipasir-up")] + let var = #vars .as_ref().lock().unwrap().next().expect("variable pool exhaused"); + #[cfg(not(feature = "ipasir-up"))] + let var = #vars .next().expect("variable pool exhaused"); + 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 { + #[cfg(feature = "ipasir-up")] + let r = #vars .as_ref().lock().unwrap().next_var_range(size); + #[cfg(not(feature = "ipasir-up"))] + let r = #vars .next_var_range(size); + r + } + } + } else { + quote! { + fn next_var_range(&mut self, size: usize) -> Option { + #vars .next_var_range(size) + } + } + }; + let from_cnf = if opts.has_default { let var_member = match opts.vars { Some(x) => quote! { #x }, None => quote! { vars }, }; + let up_version = if opts.ipasir_up { + quote! { + #[cfg(feature = "ipasir-up")] + impl From for #ident { + fn from(value: crate::Cnf) -> #ident { + let mut slv: #ident = Default::default(); + slv. #var_member = Arc::new(Mutex::new(value.nvar)); + for cl in value.iter() { + let _ = crate::ClauseDatabase::add_clause(&mut slv, cl.iter().copied()); + } + slv + } + } + #[cfg(not(feature = "ipasir-up"))] + } + } else { + quote!() + }; + quote! { + #up_version impl From for #ident { fn from(value: crate::Cnf) -> #ident { let mut slv: #ident = Default::default(); @@ -394,9 +464,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } impl crate::ClauseDatabase for #ident { - fn new_var(&mut self) -> crate::Var { - #vars .next().expect("variable pool exhaused") - } + #new_var fn add_clause>( &mut self, @@ -423,9 +491,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } impl crate::solver::NextVarRange for #ident { - fn next_var_range(&mut self, size: usize) -> Option { - #vars .next_var_range(size) - } + #next_var_range } impl crate::solver::Solver for #ident { diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index 7f2891c3fe..f582e3d353 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -1,3 +1,5 @@ +#[cfg(feature = "ipasir-up")] +use std::sync::{Arc, Mutex}; use std::{ alloc::Layout, ffi::{c_void, CString}, @@ -16,7 +18,11 @@ pub struct Cadical { /// The raw pointer to the Cadical solver. ptr: *mut c_void, /// The variable factory for this solver. + #[cfg(not(feature = "ipasir-up"))] vars: VarFactory, + /// The variable factory for this solver. + #[cfg(feature = "ipasir-up")] + vars: Arc>, /// The callback used when a clause is learned. learn_cb: Option<(*mut c_void, Layout)>, /// The callback used to check whether the solver should terminate. @@ -31,7 +37,10 @@ impl Default for Cadical { fn default() -> Self { Self { ptr: unsafe { pindakaas_cadical::ipasir_init() }, + #[cfg(not(feature = "ipasir-up"))] vars: VarFactory::default(), + #[cfg(feature = "ipasir-up")] + vars: Arc::default(), learn_cb: None, term_cb: None, #[cfg(feature = "ipasir-up")] @@ -43,9 +52,13 @@ impl Default for Cadical { impl Clone for Cadical { fn clone(&self) -> Self { let ptr = unsafe { ccadical_copy(self.ptr) }; + #[cfg(not(feature = "ipasir-up"))] + let vars = self.vars; // Copy + #[cfg(feature = "ipasir-up")] + let vars = Arc::new(Mutex::new(*self.vars.as_ref().lock().unwrap())); Self { ptr, - vars: self.vars, + vars, learn_cb: None, term_cb: None, #[cfg(feature = "ipasir-up")] diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index 42bdaae7e4..cf41e3210b 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -387,11 +387,11 @@ impl Iterator for ExplIter { } #[cfg(feature = "ipasir-up")] -pub(crate) struct IpasirPropStore

{ +pub(crate) struct IpasirPropStore { /// Rust Propagator pub(crate) prop: P, /// IPASIR solver pointer - pub(crate) slv: *mut dyn SolvingActions, + pub(crate) slv: A, /// Propagation queue pub(crate) pqueue: VecDeque, /// Reason clause queue @@ -402,8 +402,8 @@ pub(crate) struct IpasirPropStore

{ } #[cfg(feature = "ipasir-up")] -impl

IpasirPropStore

{ - pub(crate) fn new(prop: P, slv: *mut dyn SolvingActions) -> Self { +impl IpasirPropStore { + pub(crate) fn new(prop: P, slv: A) -> Self { Self { prop, slv, @@ -418,28 +418,28 @@ impl

IpasirPropStore

{ // --- Callback functions for C propagator interface --- #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( +pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( state: *mut c_void, lit: i32, is_fixed: bool, ) { - let prop = &mut *(state as *mut IpasirPropStore

); + let prop = &mut *(state as *mut IpasirPropStore); 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( +pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb( state: *mut c_void, ) { - let prop = &mut *(state as *mut IpasirPropStore

); + 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( +pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb( state: *mut c_void, level: usize, ) { - let prop = &mut *(state as *mut IpasirPropStore

); + let prop = &mut *(state as *mut IpasirPropStore); prop.pqueue.clear(); prop.explaining = None; prop.rqueue.clear(); @@ -447,12 +447,12 @@ pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb( prop.prop.notify_backtrack(level); } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_check_model_cb( +pub(crate) unsafe extern "C" fn ipasir_check_model_cb( state: *mut c_void, len: usize, model: *const i32, ) -> bool { - let prop = &mut *(state as *mut IpasirPropStore

); + let prop = &mut *(state as *mut IpasirPropStore); let sol = if len > 0 { std::slice::from_raw_parts(model, len) } else { @@ -463,11 +463,11 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb( .map(|&i| (Var(NonZeroI32::new(i.abs()).unwrap()), i >= 0)) .collect(); let value = |l: Lit| sol.get(&l.var()).copied(); - prop.prop.check_model(&mut *prop.slv, &value) + prop.prop.check_model(&mut prop.slv, &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

); +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() { l.0.into() } else { @@ -475,10 +475,12 @@ pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_vo } } #[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

); +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() { - let slv = &mut *prop.slv; + let slv = &mut prop.slv; prop.pqueue = prop.prop.propagate(slv).into() } if let Some(l) = prop.pqueue.pop_front() { @@ -488,11 +490,14 @@ pub(crate) unsafe extern "C" fn ipasir_propagate_cb(state: *mut c } } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb( +pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb< + P: Propagator, + A: SolvingActions, +>( state: *mut c_void, propagated_lit: i32, ) -> i32 { - let prop = &mut *(state as *mut IpasirPropStore

); + let prop = &mut *(state as *mut IpasirPropStore); let lit = crate::Lit(std::num::NonZeroI32::new(propagated_lit).unwrap()); debug_assert!(prop.explaining.is_none() || prop.explaining == Some(lit)); // TODO: Can this be prop.explaining.is_none()? @@ -509,22 +514,25 @@ pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb( } } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_has_external_clause_cb( +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(&mut *prop.slv).map(Vec::into); + let prop = &mut *(state as *mut IpasirPropStore); + prop.cqueue = prop.prop.add_external_clause(&mut prop.slv).map(Vec::into); prop.cqueue.is_some() } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_add_external_clause_lit_cb( +pub(crate) unsafe extern "C" fn ipasir_add_external_clause_lit_cb< + P: Propagator, + A: SolvingActions, +>( state: *mut c_void, ) -> i32 { - let prop = &mut *(state as *mut IpasirPropStore

); + let prop = &mut *(state as *mut IpasirPropStore); if prop.cqueue.is_none() { debug_assert!(false); // This function shouldn't be called when "has_clause" returned false. - prop.cqueue = prop.prop.add_external_clause(&mut *prop.slv).map(Vec::into); + prop.cqueue = prop.prop.add_external_clause(&mut prop.slv).map(Vec::into); } if let Some(queue) = &mut prop.cqueue { if let Some(l) = queue.pop_front() {