From b63baea51748098b18d566d4779c897076bad03a Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Fri, 25 Oct 2024 18:01:53 +1100 Subject: [PATCH] Make `solve` methods return solution/fail (reference) objects This replaces the current functionality that forces the user to use a callback to query the solution or find which assumptions contributed to failure. The usage of (reference) objects generally makes the system easier to use and the user doesn't have to care as much about moving objects. This also changes the IPASIR-UP implementation to exists through separate objects. This solves the problem with dynamic typing. --- crates/pindakaas-build-macros/src/lib.rs | 28 +- crates/pindakaas-derive/src/lib.rs | 414 +++++++++----------- crates/pindakaas/src/bool_linear.rs | 22 +- crates/pindakaas/src/cardinality_one.rs | 3 +- crates/pindakaas/src/helpers.rs | 83 ++-- crates/pindakaas/src/integer.rs | 22 +- crates/pindakaas/src/lib.rs | 6 +- crates/pindakaas/src/propositional_logic.rs | 6 +- crates/pindakaas/src/solver.rs | 26 +- crates/pindakaas/src/solver/cadical.rs | 75 ++-- crates/pindakaas/src/solver/intel_sat.rs | 16 +- crates/pindakaas/src/solver/kissat.rs | 13 +- crates/pindakaas/src/solver/libloading.rs | 54 +-- crates/pindakaas/src/solver/propagation.rs | 223 ++++------- crates/pindakaas/src/solver/splr.rs | 40 +- crates/pindakaas/src/sorted.rs | 10 +- crates/pindakaas/src/trace.rs | 6 +- 17 files changed, 443 insertions(+), 604 deletions(-) diff --git a/crates/pindakaas-build-macros/src/lib.rs b/crates/pindakaas-build-macros/src/lib.rs index 315435fdc6..b1eaf17286 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 37964d74ab..4a2747b606 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/bool_linear.rs b/crates/pindakaas/src/bool_linear.rs index 99e1001bd5..e70f09a287 100644 --- a/crates/pindakaas/src/bool_linear.rs +++ b/crates/pindakaas/src/bool_linear.rs @@ -1,15 +1,3 @@ -use std::{ - cell::RefCell, - collections::{BTreeSet, VecDeque}, - fmt::{self, Display}, - ops::{Add, AddAssign, Deref, DerefMut, Mul, MulAssign, Range}, - rc::Rc, -}; - -use iset::IntervalMap; -use itertools::Itertools; -use rustc_hash::{FxBuildHasher, FxHashMap}; - use crate::{ cardinality::Cardinality, cardinality_one::{CardinalityOne, PairwiseEncoder}, @@ -22,6 +10,16 @@ use crate::{ sorted::{Sorted, SortedEncoder}, Checker, ClauseDatabase, Coeff, Encoder, IntEncoding, Lit, Result, Unsatisfiable, Valuation, }; +use iset::IntervalMap; +use itertools::Itertools; +use rustc_hash::{FxBuildHasher, FxHashMap}; +use std::{ + cell::RefCell, + collections::{BTreeSet, VecDeque}, + fmt::{self, Display}, + ops::{Add, AddAssign, Deref, DerefMut, Mul, MulAssign, Range}, + rc::Rc, +}; #[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] /// Encoder for the linear constraints that ∑ coeffᵢ·litsᵢ ≷ k using a diff --git a/crates/pindakaas/src/cardinality_one.rs b/crates/pindakaas/src/cardinality_one.rs index 786c836db0..0b095dcbb6 100644 --- a/crates/pindakaas/src/cardinality_one.rs +++ b/crates/pindakaas/src/cardinality_one.rs @@ -1,10 +1,9 @@ -use itertools::Itertools; - use crate::{ bool_linear::{LimitComp, NormalizedBoolLinear}, helpers::{emit_clause, new_var}, Checker, ClauseDatabase, Encoder, Lit, Result, Valuation, }; +use itertools::Itertools; /// An encoder for [`CardinalityOne`] constraints that uses a logarithm /// encoded selector variable to ensure the selection of at most one of diff --git a/crates/pindakaas/src/helpers.rs b/crates/pindakaas/src/helpers.rs index 9ff1a64621..d329ae83dd 100644 --- a/crates/pindakaas/src/helpers.rs +++ b/crates/pindakaas/src/helpers.rs @@ -94,15 +94,14 @@ macro_rules! new_var { }}; } -use std::collections::HashSet; - pub(crate) use emit_clause; -use itertools::Itertools; pub(crate) use new_var; #[cfg(feature = "splr")] pub(crate) use {concat_slices, const_concat, maybe_std_concat}; use crate::{bool_linear::PosCoeff, integer::IntVar, ClauseDatabase, Coeff, Lit, Result}; +use itertools::Itertools; +use std::collections::HashSet; const FILTER_TRIVIAL_CLAUSES: bool = false; @@ -201,7 +200,7 @@ pub(crate) mod tests { }; } - use std::{fmt::Display, mem}; + use std::fmt::Display; #[cfg(test)] pub(crate) use expect_file; @@ -220,23 +219,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 +256,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 +298,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/integer.rs b/crates/pindakaas/src/integer.rs index 707a8fb7fc..436733f570 100644 --- a/crates/pindakaas/src/integer.rs +++ b/crates/pindakaas/src/integer.rs @@ -1,15 +1,3 @@ -use std::{ - cell::RefCell, - collections::BTreeSet, - fmt::{self, Display}, - ops::{Not, Range}, - rc::Rc, -}; - -use iset::{interval_map, interval_set, IntervalMap, IntervalSet}; -use itertools::Itertools; -use rustc_hash::{FxBuildHasher, FxHashMap, FxHashSet}; - use crate::{ bool_linear::{BoolLinExp, LimitComp, Part, PosCoeff}, helpers::{ @@ -18,6 +6,16 @@ use crate::{ }, Checker, ClauseDatabase, Coeff, Encoder, Lit, Result, Unsatisfiable, Valuation, }; +use iset::{interval_map, interval_set, IntervalMap, IntervalSet}; +use itertools::Itertools; +use rustc_hash::{FxBuildHasher, FxHashMap, FxHashSet}; +use std::{ + cell::RefCell, + collections::BTreeSet, + fmt::{self, Display}, + ops::{Not, Range}, + rc::Rc, +}; const COUPLE_DOM_PART_TO_ORD: bool = false; const ENCODE_REDUNDANT_X_O_Y_O_Z_B: bool = true; diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs index 715091d05e..96344e08ca 100755 --- a/crates/pindakaas/src/lib.rs +++ b/crates/pindakaas/src/lib.rs @@ -18,6 +18,8 @@ mod sorted; #[cfg(any(feature = "tracing", test))] pub mod trace; +use crate::{helpers::subscript_number, solver::VarFactory}; +use itertools::{traits::HomogeneousTuple, Itertools}; use std::{ clone::Clone, cmp::{max, Eq, Ordering}, @@ -32,10 +34,6 @@ use std::{ path::Path, }; -use itertools::{traits::HomogeneousTuple, Itertools}; - -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 /// as a model) satisfies the constraint. diff --git a/crates/pindakaas/src/propositional_logic.rs b/crates/pindakaas/src/propositional_logic.rs index 2368eb85cd..456068303e 100644 --- a/crates/pindakaas/src/propositional_logic.rs +++ b/crates/pindakaas/src/propositional_logic.rs @@ -1,8 +1,6 @@ -use std::{fmt::Display, iter::once, ops::Not}; - -use itertools::{Itertools, Position}; - use crate::{ClauseDatabase, Cnf, Encoder, Lit, Result, Unsatisfiable}; +use itertools::{Itertools, Position}; +use std::{fmt::Display, iter::once, ops::Not}; /// A propositional logic formula #[derive(Clone, Debug, PartialEq, Eq)] diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 20ff55f3d5..eb1df6c5ba 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -11,9 +11,8 @@ pub mod propagation; #[cfg(feature = "splr")] pub mod splr; -use std::{ffi::c_void, num::NonZeroI32, ptr}; - use crate::{ClauseDatabase, Lit, Valuation, Var, VarRange}; +use std::{ffi::c_void, num::NonZeroI32, ptr}; type CB0 = unsafe extern "C" fn(*mut c_void) -> R; type CB1 = unsafe extern "C" fn(*mut c_void, A) -> R; @@ -59,33 +58,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 +83,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 5ec659cba3..582434e561 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -1,36 +1,22 @@ -#[cfg(feature = "external-propagation")] -use std::sync::{Arc, Mutex}; +use crate::{solver::FFIPointer, Lit, VarFactory}; +use pindakaas_cadical::{ccadical_copy, ccadical_phase, ccadical_unphase}; +use pindakaas_derive::IpasirSolver; use std::{ ffi::{c_void, CString}, fmt, }; -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)] #[ipasir(krate = pindakaas_cadical, assumptions, learn_callback, term_callback, ipasir_up)] 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 +51,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 +66,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 +109,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 +129,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 +144,8 @@ mod tests { solver::{ cadical::CadicalSol, propagation::{ - ClausePersistence, PropagatingSolver, Propagator, PropagatorAccess, - SolvingActions, + ClausePersistence, PropagatingSolver, Propagator, SolvingActions, + WithPropagator, }, VarRange, }, @@ -186,7 +164,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 +188,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 +226,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 2bfa56e720..a2f7c6370c 100644 --- a/crates/pindakaas/src/solver/intel_sat.rs +++ b/crates/pindakaas/src/solver/intel_sat.rs @@ -1,8 +1,6 @@ -use std::ffi::c_void; - -use pindakaas_derive::IpasirSolver; - use crate::{solver::FFIPointer, VarFactory}; +use pindakaas_derive::IpasirSolver; +use std::ffi::c_void; #[derive(Debug, IpasirSolver)] #[ipasir(krate = pindakaas_intel_sat, assumptions, learn_callback, term_callback)] @@ -55,9 +53,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 8594f0179e..d1516904f7 100644 --- a/crates/pindakaas/src/solver/kissat.rs +++ b/crates/pindakaas/src/solver/kissat.rs @@ -1,6 +1,5 @@ -use pindakaas_derive::IpasirSolver; - use crate::VarFactory; +use pindakaas_derive::IpasirSolver; #[derive(Debug, IpasirSolver)] #[ipasir(krate = pindakaas_kissat)] @@ -46,9 +45,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 2b6c5a3f39..6949095a4e 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -1,11 +1,3 @@ -use std::{ - ffi::{c_char, c_int, c_void, CStr}, - num::NonZeroI32, - ptr, -}; - -use libloading::{Library, Symbol}; - use crate::{ solver::{ get_trampoline0, get_trampoline1, ExplIter, FFIPointer, FailedAssumtions, LearnCallback, @@ -13,6 +5,12 @@ use crate::{ }, ClauseDatabase, ConditionalDatabase, Lit, Result, Valuation, Var, }; +use libloading::{Library, Symbol}; +use std::{ + ffi::{c_char, c_int, c_void, CStr}, + num::NonZeroI32, + ptr, +}; #[derive(Debug)] pub struct IpasirFailed<'lib> { @@ -285,34 +283,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 +307,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 1116356bef..84c3235448 100644 --- a/crates/pindakaas/src/solver/propagation.rs +++ b/crates/pindakaas/src/solver/propagation.rs @@ -1,9 +1,8 @@ -use std::{any::Any, collections::VecDeque, ffi::c_void, num::NonZeroI32}; - use crate::{ - solver::{FFIPointer, Solver}, - Lit, Valuation, Var, + solver::{FailedAssumtions, SolveResult}, + ClauseDatabase, Lit, Valuation, Var, }; +use std::{collections::VecDeque, ffi::c_void, num::NonZeroI32}; #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)] /// Whether a clause could possibly be removed from the clause database. @@ -24,58 +23,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 +157,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 +198,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 +214,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 +301,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 +399,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 5533d16835..2d0cf7cb1f 100644 --- a/crates/pindakaas/src/solver/splr.rs +++ b/crates/pindakaas/src/solver/splr.rs @@ -1,13 +1,11 @@ -use std::num::NonZeroI32; - -pub use splr::Solver as Splr; -use splr::{Certificate, SatSolverIF, SolveIF, VERSION}; - use crate::{ helpers::const_concat, solver::{SolveResult, Solver}, ClauseDatabase, Cnf, ConditionalDatabase, Lit, Valuation, Var, VarRange, }; +pub use splr::Solver as Splr; +use splr::{Certificate, SatSolverIF, SolveIF, VERSION}; +use std::num::NonZeroI32; impl Valuation for Certificate { fn value(&self, lit: Lit) -> bool { @@ -93,26 +91,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 +139,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)) + // ); } } diff --git a/crates/pindakaas/src/sorted.rs b/crates/pindakaas/src/sorted.rs index 56c05760a3..c77d6e6565 100644 --- a/crates/pindakaas/src/sorted.rs +++ b/crates/pindakaas/src/sorted.rs @@ -1,15 +1,13 @@ -use std::{hash, mem, sync::Mutex}; - -use iset::interval_map; -use itertools::Itertools; -use rustc_hash::FxHashMap; - use crate::{ bool_linear::{BoolLinExp, LimitComp}, helpers::{add_clauses_for, emit_clause, negate_cnf}, integer::{IntVarEnc, IntVarOrd, TernLeConstraint, TernLeEncoder}, Checker, ClauseDatabase, Coeff, Encoder, Lit, Result, Unsatisfiable, Valuation, }; +use iset::interval_map; +use itertools::Itertools; +use rustc_hash::FxHashMap; +use std::{hash, mem, sync::Mutex}; type SortedCache = FxHashMap<(u128, u128, u128), (SortedStrategy, (u128, u128))>; diff --git a/crates/pindakaas/src/trace.rs b/crates/pindakaas/src/trace.rs index 08b705e83f..0550b91542 100644 --- a/crates/pindakaas/src/trace.rs +++ b/crates/pindakaas/src/trace.rs @@ -1,3 +1,5 @@ +use crate::{helpers::subscript_number, Lit}; +use itertools::join; use std::{ fmt, io::{stderr, BufWriter, Stderr, Write}, @@ -7,8 +9,6 @@ use std::{ }, time::Instant, }; - -use itertools::join; use tracing::{ field::{Field, Visit}, metadata::LevelFilter, @@ -16,8 +16,6 @@ use tracing::{ Event, Id, Level, Metadata, Subscriber, }; -use crate::{helpers::subscript_number, Lit}; - #[derive(Debug)] enum EventKind { NewVar,