Skip to content

Commit

Permalink
ipasir-up: fix SolverAction implementation
Browse files Browse the repository at this point in the history
  • Loading branch information
@Dekker1
Dekker1 committed Jun 27, 2024
1 parent 4949be4 commit 69a66c3
Show file tree
Hide file tree
Showing 3 changed files with 138 additions and 51 deletions.
114 changes: 90 additions & 24 deletions crates/pindakaas-derive/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
cb: Option<F>,
) {
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),
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 },
Expand All @@ -226,9 +227,9 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {

#[cfg(feature = "ipasir-up")]
impl #prop_ident {
pub(crate) fn new<P: crate::solver::Propagator + 'static>(prop: P, slv: *mut dyn crate::solver::SolvingActions) -> Self {
pub(crate) fn new<P: crate::solver::Propagator + 'static>(prop: P, slv: #actions_ident) -> Self {
// Construct wrapping structures
let prop = crate::solver::libloading::IpasirPropStore::<P>::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::<P>::from_raw(x as *mut P) };
drop(prop);
Expand All @@ -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::<P>)) };
unsafe { #krate::ipasir_prop_set_notify_new_decision_level(wrapper, Some(crate::solver::libloading::ipasir_notify_new_decision_level_cb::<P>)) };
unsafe { #krate::ipasir_prop_set_notify_backtrack(wrapper, Some(crate::solver::libloading::ipasir_notify_backtrack_cb::<P>)) };
unsafe { #krate::ipasir_prop_set_check_model(wrapper, Some(crate::solver::libloading::ipasir_check_model_cb::<P>)) };
unsafe { #krate::ipasir_prop_set_decide(wrapper, Some(crate::solver::libloading::ipasir_decide_cb::<P>)) };
unsafe { #krate::ipasir_prop_set_propagate(wrapper, Some(crate::solver::libloading::ipasir_propagate_cb::<P>)) };
unsafe { #krate::ipasir_prop_set_add_reason_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_reason_clause_lit_cb::<P>)) };
unsafe { #krate::ipasir_prop_set_has_external_clause(wrapper, Some(crate::solver::libloading::ipasir_has_external_clause_cb::<P>)) };
unsafe { #krate::ipasir_prop_set_add_external_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_external_clause_lit_cb::<P>)) };
unsafe { #krate::ipasir_prop_set_notify_assignment(wrapper, Some(crate::solver::libloading::ipasir_notify_assignment_cb::<P, #actions_ident>)) };
unsafe { #krate::ipasir_prop_set_notify_new_decision_level(wrapper, Some(crate::solver::libloading::ipasir_notify_new_decision_level_cb::<P, #actions_ident>)) };
unsafe { #krate::ipasir_prop_set_notify_backtrack(wrapper, Some(crate::solver::libloading::ipasir_notify_backtrack_cb::<P, #actions_ident>)) };
unsafe { #krate::ipasir_prop_set_check_model(wrapper, Some(crate::solver::libloading::ipasir_check_model_cb::<P, #actions_ident>)) };
unsafe { #krate::ipasir_prop_set_decide(wrapper, Some(crate::solver::libloading::ipasir_decide_cb::<P, #actions_ident>)) };
unsafe { #krate::ipasir_prop_set_propagate(wrapper, Some(crate::solver::libloading::ipasir_propagate_cb::<P, #actions_ident>)) };
unsafe { #krate::ipasir_prop_set_add_reason_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_reason_clause_lit_cb::<P, #actions_ident>)) };
unsafe { #krate::ipasir_prop_set_has_external_clause(wrapper, Some(crate::solver::libloading::ipasir_has_external_clause_cb::<P, #actions_ident>)) };
unsafe { #krate::ipasir_prop_set_add_external_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_external_clause_lit_cb::<P, #actions_ident>)) };

Self { prop: data, drop_prop, access_prop, wrapper, }
}
Expand All @@ -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 ) };
}
}
Expand Down Expand Up @@ -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<Mutex<crate::VarFactory>>,
}

#[cfg(feature = "ipasir-up")]
impl #actions_ident {
pub fn new(ptr: *mut std::ffi::c_void, vars: Arc<Mutex<crate::VarFactory>>) -> 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() ) }
}
}

Expand Down Expand Up @@ -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<crate::helpers::VarRange> {
#[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<crate::helpers::VarRange> {
#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<crate::Cnf> 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<crate::Cnf> for #ident {
fn from(value: crate::Cnf) -> #ident {
let mut slv: #ident = Default::default();
Expand All @@ -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<I: IntoIterator<Item = crate::Lit>>(
&mut self,
Expand All @@ -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<crate::helpers::VarRange> {
#vars .next_var_range(size)
}
#next_var_range
}

impl crate::solver::Solver for #ident {
Expand Down
15 changes: 14 additions & 1 deletion crates/pindakaas/src/solver/cadical.rs
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
#[cfg(feature = "ipasir-up")]
use std::sync::{Arc, Mutex};
use std::{
alloc::Layout,
ffi::{c_void, CString},
Expand All @@ -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<Mutex<VarFactory>>,
/// 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.
Expand All @@ -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")]
Expand All @@ -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")]
Expand Down
60 changes: 34 additions & 26 deletions crates/pindakaas/src/solver/libloading.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -387,11 +387,11 @@ impl Iterator for ExplIter {
}

#[cfg(feature = "ipasir-up")]
pub(crate) struct IpasirPropStore<P> {
pub(crate) struct IpasirPropStore<P, A> {
/// 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<crate::Lit>,
/// Reason clause queue
Expand All @@ -402,8 +402,8 @@ pub(crate) struct IpasirPropStore<P> {
}

#[cfg(feature = "ipasir-up")]
impl<P> IpasirPropStore<P> {
pub(crate) fn new(prop: P, slv: *mut dyn SolvingActions) -> Self {
impl<P, A> IpasirPropStore<P, A> {
pub(crate) fn new(prop: P, slv: A) -> Self {
Self {
prop,
slv,
Expand All @@ -418,41 +418,41 @@ impl<P> IpasirPropStore<P> {
// --- Callback functions for C propagator interface ---

#[cfg(feature = "ipasir-up")]
pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb<P: Propagator>(
pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb<P: Propagator, A>(
state: *mut c_void,
lit: i32,
is_fixed: bool,
) {
let prop = &mut *(state as *mut IpasirPropStore<P>);
let prop = &mut *(state as *mut IpasirPropStore<P, A>);
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<P: Propagator>(
pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb<P: Propagator, A>(
state: *mut c_void,
) {
let prop = &mut *(state as *mut IpasirPropStore<P>);
let prop = &mut *(state as *mut IpasirPropStore<P, A>);
prop.prop.notify_new_decision_level()
}
#[cfg(feature = "ipasir-up")]
pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb<P: Propagator>(
pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb<P: Propagator, A>(
state: *mut c_void,
level: usize,
) {
let prop = &mut *(state as *mut IpasirPropStore<P>);
let prop = &mut *(state as *mut IpasirPropStore<P, A>);
prop.pqueue.clear();
prop.explaining = None;
prop.rqueue.clear();
prop.cqueue = None;
prop.prop.notify_backtrack(level);
}
#[cfg(feature = "ipasir-up")]
pub(crate) unsafe extern "C" fn ipasir_check_model_cb<P: Propagator>(
pub(crate) unsafe extern "C" fn ipasir_check_model_cb<P: Propagator, A: SolvingActions>(
state: *mut c_void,
len: usize,
model: *const i32,
) -> bool {
let prop = &mut *(state as *mut IpasirPropStore<P>);
let prop = &mut *(state as *mut IpasirPropStore<P, A>);
let sol = if len > 0 {
std::slice::from_raw_parts(model, len)
} else {
Expand All @@ -463,22 +463,24 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb<P: Propagator>(
.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<P: Propagator>(state: *mut c_void) -> i32 {
let prop = &mut *(state as *mut IpasirPropStore<P>);
pub(crate) unsafe extern "C" fn ipasir_decide_cb<P: Propagator, A>(state: *mut c_void) -> i32 {
let prop = &mut *(state as *mut IpasirPropStore<P, A>);
if let Some(l) = prop.prop.decide() {
l.0.into()
} else {
0
}
}
#[cfg(feature = "ipasir-up")]
pub(crate) unsafe extern "C" fn ipasir_propagate_cb<P: Propagator>(state: *mut c_void) -> i32 {
let prop = &mut *(state as *mut IpasirPropStore<P>);
pub(crate) unsafe extern "C" fn ipasir_propagate_cb<P: Propagator, A: SolvingActions>(
state: *mut c_void,
) -> i32 {
let prop = &mut *(state as *mut IpasirPropStore<P, A>);
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() {
Expand All @@ -488,11 +490,14 @@ pub(crate) unsafe extern "C" fn ipasir_propagate_cb<P: Propagator>(state: *mut c
}
}
#[cfg(feature = "ipasir-up")]
pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb<P: Propagator>(
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<P>);
let prop = &mut *(state as *mut IpasirPropStore<P, A>);
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()?
Expand All @@ -509,22 +514,25 @@ pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb<P: Propagator>(
}
}
#[cfg(feature = "ipasir-up")]
pub(crate) unsafe extern "C" fn ipasir_has_external_clause_cb<P: Propagator>(
pub(crate) unsafe extern "C" fn ipasir_has_external_clause_cb<P: Propagator, A: SolvingActions>(
state: *mut c_void,
) -> bool {
let prop = &mut *(state as *mut IpasirPropStore<P>);
prop.cqueue = prop.prop.add_external_clause(&mut *prop.slv).map(Vec::into);
let prop = &mut *(state as *mut IpasirPropStore<P, A>);
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<P: Propagator>(
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<P>);
let prop = &mut *(state as *mut IpasirPropStore<P, A>);
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() {
Expand Down

0 comments on commit 69a66c3

Please sign in to comment.