diff --git a/crates/pindakaas-build-macros/src/lib.rs b/crates/pindakaas-build-macros/src/lib.rs index 315435fdc..b1eaf1728 100644 --- a/crates/pindakaas-build-macros/src/lib.rs +++ b/crates/pindakaas-build-macros/src/lib.rs @@ -102,20 +102,20 @@ macro_rules! ipasir_up_definitions { #[allow(clippy::too_many_arguments)] pub unsafe fn ipasir_connect_external_propagator( slv: *mut std::ffi::c_void, - propagator_data: *mut std::ffi::c_void, - prop_notify_assignments: unsafe extern "C" fn(*mut std::ffi::c_void, *const i32, usize), - prop_notify_new_decision_level: unsafe extern "C" fn(*mut std::ffi::c_void), - prop_notify_backtrack: unsafe extern "C" fn(*mut std::ffi::c_void, usize, bool), - prop_cb_check_found_model: unsafe extern "C" fn(*mut std::ffi::c_void, *const i32, usize) -> bool, - prop_cb_has_external_clause: unsafe extern "C" fn(*mut std::ffi::c_void, *mut bool) -> bool, - prop_cb_add_external_clause_lit: unsafe extern "C" fn(*mut std::ffi::c_void) -> i32, - is_lazy: bool, - forgettable_reasons: bool, - notify_fixed: bool, - prop_cb_decide: unsafe extern "C" fn(*mut std::ffi::c_void) -> i32, - prop_cb_propagate: unsafe extern "C" fn(*mut std::ffi::c_void) -> i32, - prop_cb_add_reason_clause_lit: unsafe extern "C" fn(*mut std::ffi::c_void, i32) -> i32, - prop_notify_fixed_assignment: unsafe extern "C" fn(*mut std::ffi::c_void, i32), + propagator_data: *mut std::ffi::c_void, + prop_notify_assignments: unsafe extern "C" fn(*mut std::ffi::c_void, *const i32, usize), + prop_notify_new_decision_level: unsafe extern "C" fn(*mut std::ffi::c_void), + prop_notify_backtrack: unsafe extern "C" fn(*mut std::ffi::c_void, usize, bool), + prop_cb_check_found_model: unsafe extern "C" fn(*mut std::ffi::c_void, *const i32, usize) -> bool, + prop_cb_has_external_clause: unsafe extern "C" fn(*mut std::ffi::c_void, *mut bool) -> bool, + prop_cb_add_external_clause_lit: unsafe extern "C" fn(*mut std::ffi::c_void) -> i32, + is_lazy: bool, + forgettable_reasons: bool, + notify_fixed: bool, + prop_cb_decide: unsafe extern "C" fn(*mut std::ffi::c_void) -> i32, + prop_cb_propagate: unsafe extern "C" fn(*mut std::ffi::c_void) -> i32, + prop_cb_add_reason_clause_lit: unsafe extern "C" fn(*mut std::ffi::c_void, i32) -> i32, + prop_notify_fixed_assignment: unsafe extern "C" fn(*mut std::ffi::c_void, i32), ){ [<$prefix _connect_external_propagator>](slv, propagator_data, prop_notify_assignments, prop_notify_new_decision_level, prop_notify_backtrack, prop_cb_check_found_model, prop_cb_has_external_clause, prop_cb_add_external_clause_lit, is_lazy, forgettable_reasons, notify_fixed, prop_cb_decide, prop_cb_propagate, prop_cb_add_reason_clause_lit, prop_notify_fixed_assignment) } diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs index 37964d74a..4a2747b60 100644 --- a/crates/pindakaas-derive/src/lib.rs +++ b/crates/pindakaas-derive/src/lib.rs @@ -12,8 +12,6 @@ struct IpasirOpts { #[darling(default)] vars: Option, #[darling(default)] - prop: Option, - #[darling(default)] assumptions: bool, #[darling(default)] learn_callback: bool, @@ -36,59 +34,63 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { let DeriveInput { ident, .. } = input; let krate = opts.krate; - let ptr = match opts.ptr { - Some(x) => quote! { self. #x }, - None => quote! { self.ptr }, + let ptr_attr = match opts.ptr { + Some(x) => quote! { #x }, + None => quote! { ptr }, }; + let ptr = quote! { self. #ptr_attr }; let vars = match opts.vars.clone() { Some(x) => quote! { self. #x }, None => quote! { self.vars }, }; + let sol_ident = format_ident!("{}Sol", ident); - let assumptions = if opts.assumptions { + let (assumptions, fail_type) = if opts.assumptions { let fail_ident = format_ident!("{}Failed", ident); - quote! { - impl crate::solver::SolveAssuming for #ident { - type FailFn = #fail_ident; - - fn solve_assuming< - I: IntoIterator, - SolCb: FnOnce(&Self::ValueFn), - FailCb: FnOnce(&Self::FailFn), - >( - &mut self, - assumptions: I, - on_sol: SolCb, - on_fail: FailCb, - ) -> crate::solver::SolveResult { - use crate::solver::Solver; - for i in assumptions { - unsafe { #krate::ipasir_assume(#ptr, i.into()) } + ( + quote! { + impl #ident { + fn solver_fail_obj(&self) -> #fail_ident { + #fail_ident { slv: self } } - match self.solve(on_sol) { - crate::solver::SolveResult::Unsat => { - let fail_fn = #fail_ident { ptr: #ptr }; - on_fail(&fail_fn); - crate::solver::SolveResult::Unsat + } + + impl crate::solver::SolveAssuming for #ident { + #[allow(refining_impl_trait)] + fn solve_assuming>( + &mut self, + assumptions: I, + ) -> crate::solver::SolveResult<#sol_ident <'_>, #fail_ident <'_>> { + use crate::solver::Solver; + for i in assumptions { + unsafe { #krate::ipasir_assume(#ptr, i.into()) } } - r => r, + self.solve() } } - } - pub struct #fail_ident { - ptr: *mut std::ffi::c_void, - } - impl crate::solver::FailedAssumtions for #fail_ident { - fn fail(&self, lit: crate::Lit) -> bool { - let lit: i32 = lit.into(); - let failed = unsafe { #krate::ipasir_failed(#ptr, lit) }; - failed != 0 + pub struct #fail_ident <'a> { + slv: &'a #ident, } - } - } + impl crate::solver::FailedAssumtions for #fail_ident <'_> { + fn fail(&self, lit: crate::Lit) -> bool { + let lit: i32 = lit.into(); + let failed = unsafe { #krate::ipasir_failed( self.slv. #ptr_attr, lit) }; + failed != 0 + } + } + }, + quote! { #fail_ident <'_> }, + ) } else { - quote!() + ( + quote! { + impl #ident { + fn solver_fail_obj(&self) {} + } + }, + quote! { () }, + ) }; let term_callback = if opts.term_callback { @@ -169,194 +171,158 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { quote!() }; - let sol_ident = format_ident!("{}Sol", ident); let ipasir_up = if opts.ipasir_up { - let actions_ident = format_ident!("{}SolvingActions", ident); - let prop_member = match opts.prop { - Some(x) => quote! { self. #x }, - None => quote! { self.prop }, - }; + let prop_slv = format_ident!("Propagating{}", ident); quote! { #[cfg(feature = "external-propagation")] - impl crate::solver::propagation::PropagatingSolver for #ident { - fn set_external_propagator( - &mut self, - prop: Option

, - ) { - // Store old propagator (setting member to None) - let old = #prop_member.take(); - // Disconnect old propagator (if one was set) - if old.is_some() { - unsafe { #krate::ipasir_disconnect_external_propagator( #ptr ) }; - } - // If new propagator, set it now - if let Some(p) = prop { - let is_lazy = p.is_check_only(); - let forgettable_reasons = p.reason_persistence() == crate::solver::propagation::ClausePersistence::Forgettable; - let notify_fixed = p.enable_persistent_assignments(); + pub struct #prop_slv

{ + container: Box>, + } - #prop_member = Some(crate::solver::propagation::PropagatorPointer::new(p, #actions_ident::new(#ptr, Arc::clone(&#vars)))); - unsafe { - #krate::ipasir_connect_external_propagator( - #ptr, - #prop_member .as_ref().unwrap().get_raw_ptr(), - crate::solver::propagation::ipasir_notify_assignments_cb::, - crate::solver::propagation::ipasir_notify_new_decision_level_cb::, - crate::solver::propagation::ipasir_notify_backtrack_cb::, - crate::solver::propagation::ipasir_check_model_cb::, - crate::solver::propagation::ipasir_has_external_clause_cb::, - crate::solver::propagation::ipasir_add_external_clause_lit_cb::, - is_lazy, - forgettable_reasons, - notify_fixed, - crate::solver::propagation::ipasir_decide_cb::, - crate::solver::propagation::ipasir_propagate_cb::, - crate::solver::propagation::ipasir_add_reason_clause_lit_cb::, - crate::solver::propagation::ipasir_notify_persistent_assignments_cb::, - ) - }; - } + #[cfg(feature = "external-propagation")] + impl crate::solver::propagation::WithPropagator

for #ident { + type PropSlv = #prop_slv

; + fn with_propagator(self, prop: P) -> Self::PropSlv { + let is_lazy = prop.is_check_only(); + let forgettable_reasons = prop.reason_persistence() == crate::solver::propagation::ClausePersistence::Forgettable; + let notify_fixed = prop.enable_persistent_assignments(); + + let mut container = Box::new(crate::solver::propagation::IpasirPropStore::new(prop, self)); + unsafe { + #krate::ipasir_connect_external_propagator( + container.slv. #ptr_attr, + &mut *container as *mut _ as *mut std::ffi::c_void, + crate::solver::propagation::ipasir_notify_assignments_cb::, + crate::solver::propagation::ipasir_notify_new_decision_level_cb::, + crate::solver::propagation::ipasir_notify_backtrack_cb::, + crate::solver::propagation::ipasir_check_model_cb::, + crate::solver::propagation::ipasir_has_external_clause_cb::, + crate::solver::propagation::ipasir_add_external_clause_lit_cb::, + is_lazy, + forgettable_reasons, + notify_fixed, + crate::solver::propagation::ipasir_decide_cb::, + crate::solver::propagation::ipasir_propagate_cb::, + crate::solver::propagation::ipasir_add_reason_clause_lit_cb::, + crate::solver::propagation::ipasir_notify_persistent_assignments_cb::, + ) + }; + + #prop_slv { container } } + } - fn add_observed_var(&mut self, var: crate::Var){ - unsafe { #krate::ipasir_add_observed_var( #ptr, var.0.get()) }; + #[cfg(feature = "external-propagation")] + impl crate::solver::propagation::PropagatingSolver

for #prop_slv

{ + type Slv = #ident; + + fn access_solving(&mut self) -> (&mut dyn crate::solver::propagation::SolvingActions, &mut P) { + (&mut self.container.slv, &mut self.container.prop) } - fn remove_observed_var(&mut self, var: crate::Var){ - unsafe { #krate::ipasir_remove_observed_var( #ptr, var.0.get()) }; + + fn add_observed_var(&mut self, var: crate::Var) { + unsafe { #krate::ipasir_add_observed_var( self.container.slv. #ptr_attr, var.0.get()) }; } - fn reset_observed_vars(&mut self) { - unsafe { #krate::ipasir_reset_observed_vars( #ptr ) }; + + fn into_parts(self) -> (Self::Slv, P) { + unsafe { #krate::ipasir_disconnect_external_propagator( self.container.slv. #ptr_attr ) }; + (self.container.slv, self.container.prop) } - } - #[cfg(feature = "external-propagation")] - impl crate::solver::propagation::PropagatorAccess for #ident { - fn propagator(&self) -> Option<&P> { - #prop_member.as_ref().map(|p| unsafe { p.access_propagator() } ).flatten() + fn propagator(&self) -> &P { + &self.container.prop } - } - #[cfg(feature = "external-propagation")] - impl crate::solver::propagation::MutPropagatorAccess for #ident { - fn propagator_mut(&mut self) -> Option<&mut P> { - #prop_member.as_ref().map(|p| unsafe { p.access_propagator_mut() } ).flatten() + fn propagator_mut(&mut self) -> &mut P { + &mut self.container.prop } - } - #[cfg(feature = "external-propagation")] - pub(crate) struct #actions_ident { - ptr: *mut std::ffi::c_void, - vars: Arc>, - } + fn remove_observed_var(&mut self, var: crate::Var) { + unsafe { #krate::ipasir_remove_observed_var( self.container.slv. #ptr_attr, var.0.get()) }; + } - #[cfg(feature = "external-propagation")] - impl #actions_ident { - pub fn new(ptr: *mut std::ffi::c_void, vars: Arc>) -> Self { - Self { ptr, vars } + fn reset_observed_vars(&mut self) { + unsafe { #krate::ipasir_reset_observed_vars( self.container.slv. #ptr_attr ) }; } - } - #[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_var() + fn solve(&mut self) -> (&P, crate::solver::SolveResult<#sol_ident <'_>, #fail_type >) { + use crate::solver::Solver; + let res = self.container.slv.solve(); + (&self.container.prop, res) } - fn add_observed_var(&mut self, var: crate::Var) { - unsafe { #krate::ipasir_add_observed_var( self.ptr, var.0.get()) }; + + #[allow( + refining_impl_trait, + reason = "user can use more specific type if needed" + )] + fn solve_assuming>( + &mut self, + assumptions: I, + ) -> ( + &P, + crate::solver::SolveResult<#sol_ident <'_>, #fail_type >, + ) { + use crate::solver::SolveAssuming; + let res = self.container.slv.solve_assuming(assumptions); + (&self.container.prop, res) } - fn is_decision(&mut self, lit: crate::Lit) -> bool { - unsafe { #krate::ipasir_is_decision( self.ptr, lit.0.get() ) } + + fn solver(&self) -> &Self::Slv { + &self.container.slv + } + + fn solver_mut(&mut self) -> &mut Self::Slv { + &mut self.container.slv } } #[cfg(feature = "external-propagation")] - impl crate::solver::propagation::ExtendedSolvingActions for #actions_ident { - fn force_backtrack(&mut self, new_level: usize) { - unsafe { #krate::ipasir_force_backtrack( self.ptr, new_level ) } + impl

crate::ClauseDatabase for #prop_slv

{ + fn new_var(&mut self) -> crate::Var { + self.container.slv.new_var() } - } - pub struct #sol_ident { - ptr: *mut std::ffi::c_void, - #[cfg(feature = "external-propagation")] - prop: Option<*mut std::ffi::c_void>, - #[cfg(feature = "external-propagation")] - access_prop: Option *mut dyn std::any::Any>, - } - impl #ident { - fn solver_solution_obj(&mut self) -> #sol_ident { - #sol_ident { - ptr: self.ptr, - #[cfg(feature = "external-propagation")] - prop: #prop_member .as_mut().map(|p| p.get_raw_ptr()), - #[cfg(feature = "external-propagation")] - access_prop: #prop_member .as_ref().map(|p| p.access_prop), - } + fn new_var_range(&mut self, len: usize) -> crate::VarRange { + self.container.slv.new_var_range(len) } - } - #[cfg(feature = "external-propagation")] - impl crate::solver::propagation::PropagatorAccess for #sol_ident { - fn propagator(&self) -> Option<&P> { - if let Some(prop) = self.prop { - unsafe { &*(self.access_prop.unwrap())(prop) }.downcast_ref() - } else { - None + + fn add_clause>( + &mut self, + clause: I, + ) -> crate::Result { + self.container.slv.add_clause(clause) + } + + type CondDB = Self; + fn with_conditions(&mut self, conditions: Vec) -> crate::ConditionalDatabase { + crate::ConditionalDatabase { + db: self, + conditions, } } } + #[cfg(feature = "external-propagation")] - impl crate::solver::propagation::MutPropagatorAccess for #sol_ident { - fn propagator_mut(&mut self) -> Option<&mut P> { - if let Some(prop) = self.prop { - unsafe { &mut *(self.access_prop.unwrap())(prop) }.downcast_mut() - } else { - None - } + impl crate::solver::propagation::SolvingActions for #ident { + fn new_var(&mut self) -> crate::Var { + let var = ::new_var(self); + unsafe { #krate::ipasir_add_observed_var( #ptr , var.0.get()) }; + var } - } - } - } else { - quote! { - pub struct #sol_ident { - ptr: *mut std::ffi::c_void, - } - impl #ident { - fn solver_solution_obj(&self) -> #sol_ident { - #sol_ident { ptr: self.ptr } + fn is_decision(&mut self, lit: crate::Lit) -> bool { + unsafe { #krate::ipasir_is_decision( #ptr, lit.0.get() ) } } } - } - }; - - let new_var = if opts.ipasir_up { - quote! { - fn new_var(&mut self) -> crate::Var { - #[cfg(feature = "external-propagation")] - let var = #vars .as_ref().lock().unwrap().next_var(); - #[cfg(not(feature = "external-propagation"))] - let var = #vars .next_var(); - var - } - fn new_var_range(&mut self, len: usize) -> crate::VarRange { - #[cfg(feature = "external-propagation")] - let var = #vars .as_ref().lock().unwrap().next_var_range(len); - #[cfg(not(feature = "external-propagation"))] - let var = #vars .next_var_range(len); - var + #[cfg(feature = "external-propagation")] + impl crate::solver::propagation::ExtendedSolvingActions for #ident { + fn force_backtrack(&mut self, new_level: usize) { + unsafe { #krate::ipasir_force_backtrack( #ptr, new_level ) } + } } } } else { - quote! { - 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 - } - } + quote!() }; let from_cnf = if opts.has_default { @@ -364,27 +330,8 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { Some(x) => quote! { #x }, None => quote! { vars }, }; - let up_version = if opts.ipasir_up { - quote! { - #[cfg(feature = "external-propagation")] - 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 = "external-propagation"))] - } - } else { - quote!() - }; quote! { - #up_version impl From<&crate::Cnf> for #ident { fn from(value: &crate::Cnf) -> #ident { let mut slv: #ident = Default::default(); @@ -408,7 +355,14 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } impl crate::ClauseDatabase for #ident { - #new_var + 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 + } fn add_clause>( &mut self, @@ -437,27 +391,29 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } impl crate::solver::Solver for #ident { - type ValueFn = #sol_ident; - fn signature(&self) -> &str { unsafe { std::ffi::CStr::from_ptr(#krate::ipasir_signature()) } .to_str() .unwrap() } - fn solve( - &mut self, - on_sol: SolCb, - ) -> crate::solver::SolveResult { + #[allow( + refining_impl_trait, + reason = "user can use more specific type if needed" + )] + fn solve(&mut self) -> crate::solver::SolveResult<#sol_ident <'_>, #fail_type > { let res = unsafe { #krate::ipasir_solve( #ptr ) }; match res { 10 => { // 10 -> Sat - let model = self.solver_solution_obj(); - on_sol(&model); - crate::solver::SolveResult::Sat + let sol = self.solver_solution_obj(); + crate::solver::SolveResult::Satisfied(sol) } - 20 => crate::solver::SolveResult::Unsat, // 20 -> Unsat + 20 => { + // 20 -> Unsat + let fail = self.solver_fail_obj(); + crate::solver::SolveResult::Unsatisfiable(fail) + }, _ => { debug_assert_eq!(res, 0); // According to spec should be 0, unknown crate::solver::SolveResult::Unknown @@ -466,11 +422,21 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } } - impl crate::Valuation for #sol_ident { + pub struct #sol_ident <'a> { + slv: &'a #ident, + } + + impl #ident { + fn solver_solution_obj(&self) -> #sol_ident { + #sol_ident { slv: self } + } + } + + impl crate::Valuation for #sol_ident <'_> { fn value(&self, lit: crate::Lit) -> bool { let var: i32 = lit.var().into(); // WARN: Always ask about variable (positive) literal, otherwise solvers sometimes seem incorrect - let ret = unsafe { #krate::ipasir_val(self.ptr, var) }; + let ret = unsafe { #krate::ipasir_val( self.slv. #ptr_attr, var) }; match ret { _ if ret == var => !lit.is_negated(), _ if ret == -var => lit.is_negated(), diff --git a/crates/pindakaas/src/helpers.rs b/crates/pindakaas/src/helpers.rs index 9ff1a6462..f7c46d597 100644 --- a/crates/pindakaas/src/helpers.rs +++ b/crates/pindakaas/src/helpers.rs @@ -201,7 +201,7 @@ pub(crate) mod tests { }; } - use std::{fmt::Display, mem}; + use std::fmt::Display; #[cfg(test)] pub(crate) use expect_file; @@ -220,23 +220,20 @@ pub(crate) mod tests { pub(crate) fn assert_checker(formula: &Cnf, checker: &impl Checker) { let mut slv = Cadical::from(formula); let vars = formula.get_variables(); - let mut sol = Vec::new(); - while slv.solve(|value| { - assert_eq!(checker.check(value), Ok(())); - sol = vars + while let SolveResult::Satisfied(value) = slv.solve() { + assert_eq!(checker.check(&value), Ok(())); + let no_good: Vec = vars .clone() .map(|v| { let l = v.into(); if value.value(l) { - l - } else { !l + } else { + l } }) .collect(); - }) != SolveResult::Unsat - { - slv.add_clause(sol.iter().map(|l| !l)).unwrap(); + slv.add_clause(no_good).unwrap(); } } @@ -260,29 +257,28 @@ pub(crate) mod tests { .map(|x| BoolLinExp::from(&x.into())) .collect_vec(); let bool_vars = formula.get_variables(); - let mut solutions = Vec::new(); - let mut nogood: Vec = Vec::new(); - while slv.solve(|value| { - nogood = bool_vars + let mut solutions: Vec> = Vec::new(); + while let SolveResult::Satisfied(value) = slv.solve() { + // Collect integer solution + solutions.push( + vars.clone() + .into_iter() + .map(|x| x.value(&value).unwrap()) + .collect(), + ); + // Add nogood clause + let nogood: Vec = bool_vars .clone() .map(|v| { let l = v.into(); if value.value(l) { - l - } else { !l + } else { + l } }) .collect(); - let sol: Vec = vars - .clone() - .into_iter() - .map(|x| x.value(value).unwrap()) - .collect(); - solutions.push(sol); - }) != SolveResult::Unsat - { - slv.add_clause(mem::take(&mut nogood)).unwrap(); + slv.add_clause(nogood).unwrap(); } solutions.sort(); let sol_str = format!( @@ -303,23 +299,21 @@ pub(crate) mod tests { I: IntoIterator + Clone, { let mut slv = Cadical::from(formula); - let mut solutions = Vec::new(); - while slv.solve(|value| { - let sol: Vec = vars - .clone() - .into_iter() - .map(|v| { - let l = v.into(); - if value.value(l) { - l - } else { - !l - } - }) - .collect(); - solutions.push(sol); - }) != SolveResult::Unsat - { + let mut solutions: Vec> = Vec::new(); + while let SolveResult::Satisfied(value) = slv.solve() { + solutions.push( + vars.clone() + .into_iter() + .map(|v| { + let l = v.into(); + if value.value(l) { + l + } else { + !l + } + }) + .collect(), + ); slv.add_clause(solutions.last().unwrap().iter().map(|l| !l)) .unwrap(); } diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 20ff55f3d..18ba3faad 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -59,33 +59,24 @@ pub enum SlvTermSignal { } pub trait SolveAssuming: Solver { - type FailFn: FailedAssumtions; - /// Solve the formula with specified clauses under the given assumptions. /// /// If the search is interrupted (see [`set_terminate_callback`]) the function /// returns unknown - fn solve_assuming< - I: IntoIterator, - SolCb: FnOnce(&Self::ValueFn), - FailCb: FnOnce(&Self::FailFn), - >( + fn solve_assuming>( &mut self, assumptions: I, - on_sol: SolCb, - on_fail: FailCb, - ) -> SolveResult; + ) -> SolveResult; } -#[derive(PartialEq, Eq, Clone, Copy, Hash, Debug)] -pub enum SolveResult { - Sat, - Unsat, +#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)] +pub enum SolveResult { + Satisfied(Sol), + Unsatisfiable(Fail), Unknown, } pub trait Solver: ClauseDatabase { - type ValueFn: Valuation; /// Return the name and the version of SAT solver. fn signature(&self) -> &str; @@ -93,7 +84,7 @@ pub trait Solver: ClauseDatabase { /// /// If the search is interrupted (see [`set_terminate_callback`]) the function /// returns unknown - fn solve(&mut self, on_sol: SolCb) -> SolveResult; + fn solve(&mut self) -> SolveResult; } pub trait TermCallback: Solver { diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index 5ec659cba..9fe16d8d0 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -1,5 +1,3 @@ -#[cfg(feature = "external-propagation")] -use std::sync::{Arc, Mutex}; use std::{ ffi::{c_void, CString}, fmt, @@ -8,8 +6,6 @@ use std::{ use pindakaas_cadical::{ccadical_copy, ccadical_phase, ccadical_unphase}; use pindakaas_derive::IpasirSolver; -#[cfg(feature = "external-propagation")] -use crate::solver::propagation::PropagatorPointer; use crate::{solver::FFIPointer, Lit, VarFactory}; #[derive(IpasirSolver)] @@ -18,19 +14,11 @@ pub struct Cadical { /// The raw pointer to the Cadical solver. ptr: *mut c_void, /// The variable factory for this solver. - #[cfg(not(feature = "external-propagation"))] vars: VarFactory, - /// The variable factory for this solver. - #[cfg(feature = "external-propagation")] - vars: Arc>, /// The callback used when a clause is learned. learn_cb: FFIPointer, /// The callback used to check whether the solver should terminate. term_cb: FFIPointer, - - #[cfg(feature = "external-propagation")] - /// The external propagator called by the solver - prop: Option, } impl Cadical { @@ -65,17 +53,12 @@ impl Clone for Cadical { fn clone(&self) -> Self { // SAFETY: Pointer known to be non-null, no other known safety concerns. let ptr = unsafe { ccadical_copy(self.ptr) }; - #[cfg(not(feature = "external-propagation"))] let vars = self.vars; // Copy - #[cfg(feature = "external-propagation")] - let vars = Arc::new(Mutex::new(*self.vars.as_ref().lock().unwrap())); Self { ptr, vars, learn_cb: FFIPointer::default(), term_cb: FFIPointer::default(), - #[cfg(feature = "external-propagation")] - prop: None, } } } @@ -85,14 +68,9 @@ impl Default for Cadical { Self { // SAFETY: Assume ipasir_init() returns a non-null pointer. ptr: unsafe { pindakaas_cadical::ipasir_init() }, - #[cfg(not(feature = "external-propagation"))] vars: VarFactory::default(), - #[cfg(feature = "external-propagation")] - vars: Arc::default(), learn_cb: FFIPointer::default(), term_cb: FFIPointer::default(), - #[cfg(feature = "external-propagation")] - prop: None, } } } @@ -133,17 +111,19 @@ mod tests { }, ) .unwrap(); - let res = slv.solve(|model| { - assert!((model.value(!a) && model.value(b)) || (model.value(a) && model.value(!b)),); - }); - assert_eq!(res, SolveResult::Sat); + let SolveResult::Satisfied(solution) = slv.solve() else { + unreachable!() + }; + assert!( + (solution.value(!a) && solution.value(b)) || (solution.value(a) && solution.value(!b)) + ); // Test clone implementation let mut cp = slv.clone(); - assert_eq!( - cp.solve(|model| { - assert!((model.value(!a) && model.value(b)) || (model.value(a) && model.value(!b)),); - }), - SolveResult::Sat + let SolveResult::Satisfied(solution) = cp.solve() else { + unreachable!() + }; + assert!( + (solution.value(!a) && solution.value(b)) || (solution.value(a) && solution.value(!b)) ); } @@ -151,7 +131,7 @@ mod tests { fn test_cadical_empty_clause() { let mut slv = Cadical::default(); assert_eq!(slv.add_clause([]), Err(Unsatisfiable)); - assert_eq!(slv.solve(|_| unreachable!()), SolveResult::Unsat); + assert!(matches!(slv.solve(), SolveResult::Unsatisfiable(_))); } #[cfg(feature = "external-propagation")] @@ -166,8 +146,8 @@ mod tests { solver::{ cadical::CadicalSol, propagation::{ - ClausePersistence, PropagatingSolver, Propagator, PropagatorAccess, - SolvingActions, + ClausePersistence, PropagatingSolver, Propagator, SolvingActions, + WithPropagator, }, VarRange, }, @@ -186,7 +166,7 @@ mod tests { fn is_check_only(&self) -> bool { true } - fn check_model( + fn check_solution( &mut self, _slv: &mut dyn SolvingActions, model: &dyn crate::Valuation, @@ -210,34 +190,25 @@ mod tests { ) -> Option<(Vec, ClausePersistence)> { self.tmp.pop().map(|c| (c, ClausePersistence::Forgettable)) } - - fn as_any(&self) -> &dyn Any { - self - } - fn as_mut_any(&mut self) -> &mut dyn Any { - self - } } let p = Dist2 { vars: vars.clone(), tmp: Vec::new(), }; - slv.set_external_propagator(Some(p)); + let mut slv = slv.with_propagator(p); slv.add_clause(vars.clone().map_into()).unwrap(); for v in vars.clone() { PropagatingSolver::add_observed_var(&mut slv, v) } let mut solns: Vec> = Vec::new(); - let push_sol = |model: &CadicalSol, solns: &mut Vec>| { + while let (_, SolveResult::Satisfied(sol)) = slv.solve() { let sol: Vec = vars .clone() - .map(|v| if model.value(v.into()) { v.into() } else { !v }) + .map(|v| if sol.value(v.into()) { v.into() } else { !v }) .collect_vec(); solns.push(sol); - }; - while slv.solve(|model| push_sol(model, &mut solns)) == SolveResult::Sat { slv.add_clause(solns.last().unwrap().iter().map(|l| !l)) .unwrap() } @@ -257,6 +228,6 @@ mod tests { vec![!a, !b, !c, !d, e], ] ); - assert!(slv.propagator::().unwrap().tmp.is_empty()) + assert!(slv.propagator().tmp.is_empty()) } } diff --git a/crates/pindakaas/src/solver/intel_sat.rs b/crates/pindakaas/src/solver/intel_sat.rs index 2bfa56e72..ba7a678f6 100644 --- a/crates/pindakaas/src/solver/intel_sat.rs +++ b/crates/pindakaas/src/solver/intel_sat.rs @@ -55,9 +55,11 @@ mod tests { }, ) .unwrap(); - let res = slv.solve(|model| { - assert!((model.value(!a) && model.value(b)) || (model.value(a) && model.value(!b)),) - }); - assert_eq!(res, SolveResult::Sat); + let SolveResult::Satisfied(solution) = slv.solve() else { + unreachable!() + }; + assert!( + (solution.value(!a) && solution.value(b)) || (solution.value(a) && solution.value(!b)) + ); } } diff --git a/crates/pindakaas/src/solver/kissat.rs b/crates/pindakaas/src/solver/kissat.rs index 8594f0179..141dcab2f 100644 --- a/crates/pindakaas/src/solver/kissat.rs +++ b/crates/pindakaas/src/solver/kissat.rs @@ -46,9 +46,11 @@ mod tests { }, ) .unwrap(); - let res = slv.solve(|model| { - assert!((model.value(!a) && model.value(b)) || (model.value(a) && model.value(!b)),) - }); - assert_eq!(res, SolveResult::Sat); + let SolveResult::Satisfied(solution) = slv.solve() else { + unreachable!() + }; + assert!( + (solution.value(!a) && solution.value(b)) || (solution.value(a) && solution.value(!b)) + ); } } diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index 2b6c5a3f3..3d2869dab 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -285,34 +285,22 @@ impl<'lib> LearnCallback for IpasirSolver<'lib> { } impl<'lib> SolveAssuming for IpasirSolver<'lib> { - type FailFn = IpasirFailed<'lib>; - - fn solve_assuming< - I: IntoIterator, - SolCb: FnOnce(&::ValueFn), - FailCb: FnOnce(&Self::FailFn), - >( + #[allow( + refining_impl_trait, + reason = "user can use more specific type if needed" + )] + fn solve_assuming>( &mut self, assumptions: I, - on_sol: SolCb, - on_fail: FailCb, - ) -> SolveResult { + ) -> SolveResult, IpasirFailed<'_>> { for i in assumptions { (self.assume_fn)(self.slv, i.into()); } - match self.solve(on_sol) { - SolveResult::Unsat => { - on_fail(&self.failed_obj()); - SolveResult::Unsat - } - r => r, - } + self.solve() } } impl<'lib> Solver for IpasirSolver<'lib> { - type ValueFn = IpasirSol<'lib>; - fn signature(&self) -> &str { // SAFETY: We assume that the signature function as part of the IPASIR // interface returns a valid C string. @@ -321,15 +309,15 @@ impl<'lib> Solver for IpasirSolver<'lib> { .unwrap() } - fn solve(&mut self, on_sol: SolCb) -> SolveResult { + #[allow( + refining_impl_trait, + reason = "user can use more specific type if needed" + )] + fn solve(&mut self) -> SolveResult, IpasirFailed<'_>> { let res = (self.solve_fn)(self.slv); match res { - 10 => { - // 10 -> Sat - on_sol(&self.sol_obj()); - SolveResult::Sat - } - 20 => SolveResult::Unsat, // 20 -> Unsat + 10 => SolveResult::Satisfied(self.sol_obj()), // 10 -> Sat + 20 => SolveResult::Unsatisfiable(self.failed_obj()), // 20 -> Unsat _ => { debug_assert_eq!(res, 0); // According to spec should be 0, unknown SolveResult::Unknown diff --git a/crates/pindakaas/src/solver/propagation.rs b/crates/pindakaas/src/solver/propagation.rs index 1116356be..8f22df1a5 100644 --- a/crates/pindakaas/src/solver/propagation.rs +++ b/crates/pindakaas/src/solver/propagation.rs @@ -1,8 +1,8 @@ -use std::{any::Any, collections::VecDeque, ffi::c_void, num::NonZeroI32}; +use std::{collections::VecDeque, ffi::c_void, num::NonZeroI32}; use crate::{ - solver::{FFIPointer, Solver}, - Lit, Valuation, Var, + solver::{FailedAssumtions, SolveResult}, + ClauseDatabase, Lit, Valuation, Var, }; #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)] @@ -24,58 +24,84 @@ pub(crate) trait ExtendedSolvingActions: SolvingActions { fn force_backtrack(&mut self, level: usize); } -/// Trait implemented by the object given to the callback on detecting failure -pub trait FailedAssumtions { - /// Check if the given assumption literal was used to prove the unsatisfiability - /// of the formula under the assumptions used for the last SAT search. - /// - /// Note that for literals 'lit' which are not assumption literals, the behavior - /// of is not specified. - fn fail(&self, lit: Lit) -> bool; -} - -pub(crate) struct IpasirPropStore { +/// Container that is used to store a propagator and all its data required to +/// implement the methods required by the IPASIR-UP interface. +pub(crate) struct IpasirPropStore { /// Rust Propagator pub(crate) prop: P, - /// IPASIR solver pointer - pub(crate) slv: A, + /// IPASIR Solver object + pub(crate) slv: Slv, /// Propagation queue pub(crate) pqueue: VecDeque, /// Reason clause queue pub(crate) rqueue: VecDeque, + /// The current literal that is being explained pub(crate) explaining: Option, /// External clause queue pub(crate) cqueue: Option>, } -/// Get mutable access to the external propagator given the to solver -pub trait MutPropagatorAccess { +pub trait PropagatingSolver: ClauseDatabase { + type Slv; + + /// Access the external propagator together with the solving actions that are + /// available during the solving process. + fn access_solving(&mut self) -> (&mut dyn SolvingActions, &mut P); + + /// Add a variable to the set of observed variables. + /// + /// The external propagator will be notified when the variable is assigned. + fn add_observed_var(&mut self, var: Var); + + /// Destructures the `PropagatingSolver` into a [`Self::Slv`] and the + /// [`Propagator`]. + fn into_parts(self) -> (Self::Slv, P); + + /// Access the external propagator given the to solver + fn propagator(&self) -> &P; + /// Get mutable access to the external propagator given the to solver + fn propagator_mut(&mut self) -> &mut P; + + /// Remove a variable from the set of observed variables. /// - /// This method will return [`None`] if no propagator is set, or if the - /// propagator is not of type [`P`]. - fn propagator_mut(&mut self) -> Option<&mut P>; -} + /// The external propagator will no longer be notified of assignments to + /// the variable. + fn remove_observed_var(&mut self, var: Var); -pub trait PropagatingSolver: Solver + PropagatorAccess + MutPropagatorAccess -where - Self::ValueFn: PropagatorAccess, -{ - /// Set Propagator implementation which allows to learn, propagate and - /// backtrack based on external constraints. + /// Reset the set of observed variables. /// - /// Only one Propagator can be connected, any previous propagator will be - /// overriden. This Propagator is notified of all changes to which it has - /// subscribed, using the [`add_observed_var`] method. + /// The external propagator will no longer be notified of assignments to + /// any variables. + fn reset_observed_vars(&mut self); + + /// Solve the formula with specified clauses,subject to the external + /// propagator. /// - /// # Warning + /// If the search is interrupted (see [`set_terminate_callback`]) the function + /// returns unknown + fn solve(&mut self) -> (&P, SolveResult) { + self.solve_assuming(std::iter::empty()) + } + + /// Solve the formula with specified clauses under the given assumptions, + /// subject to the external propagator. /// - /// Calling this method automatically resets the observed variable set. - fn set_external_propagator(&mut self, prop: Option

); + /// If the search is interrupted (see [`set_terminate_callback`]) the function + /// returns unknown + fn solve_assuming>( + &mut self, + assumptions: I, + ) -> ( + &P, + SolveResult, + ); - fn add_observed_var(&mut self, var: Var); - fn remove_observed_var(&mut self, var: Var); - fn reset_observed_vars(&mut self); + /// Access the underlying solver. + fn solver(&self) -> &Self::Slv; + + /// Get mutable access to the underlying solver. + fn solver_mut(&mut self) -> &mut Self::Slv; } pub trait Propagator { @@ -132,7 +158,7 @@ pub trait Propagator { /// 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, slv: &mut dyn SolvingActions, value: &dyn Valuation) -> bool { + fn check_solution(&mut self, slv: &mut dyn SolvingActions, value: &dyn Valuation) -> bool { let _ = value; let _ = slv; true @@ -173,67 +199,6 @@ pub trait Propagator { let _ = slv; None } - - /// Method to help access to the propagator when given to the solver. - /// - /// See [`PropagatingSolver::propagator`]. - /// - /// # Note - /// - /// This method can generally be implemented as - /// ```rust - /// use std::any::Any; - /// use pindakaas::solver::Propagator; - /// - /// struct A; - /// - /// impl Propagator for A { - /// fn as_any(&self) -> &dyn Any { - /// self - /// } - /// - /// # fn as_mut_any(&mut self) -> &mut dyn Any { self } - /// } - /// - /// ``` - fn as_any(&self) -> &dyn Any; - - /// Method to help access to the propagator when given to the solver. - /// - /// See [`PropagatingSolver::propagator`]. - /// - /// # Note - /// - /// This method can generally be implemented as - /// ```rust - /// use std::any::Any; - /// use pindakaas::solver::Propagator; - /// - /// struct A; - /// - /// impl Propagator for A { - /// fn as_mut_any(&mut self) -> &mut dyn Any { - /// self - /// } - /// # fn as_any(&self) -> &dyn Any { self } - /// } - /// - /// ``` - fn as_mut_any(&mut self) -> &mut dyn Any; -} - -/// Access the external propagator given the to solver -pub trait PropagatorAccess { - /// Access the external propagator given the to solver - /// - /// This method will return [`None`] if no propagator is set, or if the - /// propagator is not of type [`P`]. - fn propagator(&self) -> Option<&P>; -} - -pub(crate) struct PropagatorPointer { - ptr: FFIPointer, - pub(crate) access_prop: fn(*mut c_void) -> *mut dyn Any, } #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)] @@ -250,11 +215,32 @@ pub enum SearchDecision { /// A trait containing the solver methods that are exposed to the propagator /// during solving. pub trait SolvingActions { + /// Add a new observed variable to the solver. fn new_var(&mut self) -> Var; - fn add_observed_var(&mut self, var: Var); + /// Add a new observed literal to the solver. + fn new_lit(&mut self) -> Lit { + self.new_var().into() + } + /// Query whether a literal was assigned as a search decision. fn is_decision(&mut self, lit: Lit) -> bool; } +pub trait WithPropagator { + type PropSlv: PropagatingSolver

; + + /// Set Propagator implementation which allows to learn, propagate and + /// backtrack based on external constraints. + /// + /// Only one Propagator can be connected, any previous propagator will be + /// overriden. This Propagator is notified of all changes to which it has + /// subscribed, using the [`add_observed_var`] method. + /// + /// # Warning + /// + /// Calling this method automatically resets the observed variable set. + fn with_propagator(self, prop: P) -> Self::PropSlv; +} + pub(crate) unsafe extern "C" fn ipasir_add_external_clause_lit_cb< P: Propagator, A: SolvingActions, @@ -316,7 +302,7 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb= 0)) .collect(); let value = |l: Lit| sol.get(&l.var()).copied().unwrap_or(false); - prop.prop.check_model(&mut prop.slv, &value) + prop.prop.check_solution(&mut prop.slv, &value) } pub(crate) unsafe extern "C" fn ipasir_decide_cb( @@ -414,37 +400,3 @@ impl IpasirPropStore { } } } - -impl PropagatorPointer { - pub(crate) unsafe fn access_propagator(&self) -> Option<&P> { - (*(self.access_prop)(self.get_raw_ptr())).downcast_ref::

() - } - - pub(crate) unsafe fn access_propagator_mut(&self) -> Option<&mut P> { - (*(self.access_prop)(self.get_raw_ptr())).downcast_mut::

() - } - - pub(crate) fn get_raw_ptr(&self) -> *mut c_void { - self.ptr.get_ptr() - } - - pub(crate) fn new(prop: P, slv: A) -> Self - where - P: Propagator + 'static, - A: ExtendedSolvingActions + 'static, - { - // Construct wrapping structures - let store = IpasirPropStore::new(prop, slv); - let prop = FFIPointer::new(store); - let access_prop = |x: *mut c_void| -> *mut dyn Any { - // SAFETY: The pointer is known to be created using - // Box::>::leak() - let store = unsafe { &mut *(x as *mut IpasirPropStore) }; - &mut store.prop - }; - Self { - ptr: prop, - access_prop, - } - } -} diff --git a/crates/pindakaas/src/solver/splr.rs b/crates/pindakaas/src/solver/splr.rs index 5533d1683..7e8941a34 100644 --- a/crates/pindakaas/src/solver/splr.rs +++ b/crates/pindakaas/src/solver/splr.rs @@ -93,26 +93,25 @@ impl From<&Cnf> for Splr { } impl Solver for Splr { - type ValueFn = Certificate; - fn signature(&self) -> &str { const SPLR_SIG: &str = const_concat!("SPLR-", VERSION); SPLR_SIG } - fn solve(&mut self, on_sol: SolCb) -> SolveResult { + #[allow( + refining_impl_trait, + reason = "user can use more specific type if needed" + )] + fn solve(&mut self) -> SolveResult { use splr::SolverError::*; match SolveIF::solve(self) { - Ok(Certificate::UNSAT) => SolveResult::Unsat, - Ok(cert @ Certificate::SAT(_)) => { - on_sol(&cert); - SolveResult::Sat - } + Ok(Certificate::UNSAT) => SolveResult::Unsatisfiable(()), + Ok(cert @ Certificate::SAT(_)) => SolveResult::Satisfied(cert), Err(e) => match e { InvalidLiteral => panic!("clause referenced a non-existing variable"), - Inconsistent => SolveResult::Unsat, - RootLevelConflict(_) => SolveResult::Unsat, + Inconsistent => SolveResult::Unsatisfiable(()), + RootLevelConflict(_) => SolveResult::Unsatisfiable(()), TimeOut | OutOfMemory => SolveResult::Unknown, _ => panic!("an error occurred within the splr solver"), }, @@ -142,12 +141,11 @@ mod tests { // }, // ) // .unwrap(); - // let res = Solver::solve(&mut slv, |value| { - // assert!( - // (value(!a).unwrap() && value(b).unwrap()) - // || (value(a).unwrap() && value(!b).unwrap()), - // ) - // }); - // assert_eq!(res, SolveResult::Sat); + // let SolveResult::Satisfied(solution) = slv.solve() else { + // unreachable!() + // }; + // assert!( + // (solution.value(!a) && solution.value(b)) || (solution.value(a) && solution.value(!b)) + // ); } }