diff --git a/crates/pindakaas-build-macros/src/ipasir_up.h b/crates/pindakaas-build-macros/src/ipasir_up.h deleted file mode 100644 index d450a890a9..0000000000 --- a/crates/pindakaas-build-macros/src/ipasir_up.h +++ /dev/null @@ -1,122 +0,0 @@ -#ifndef _ipasir_up_h_INCLUDED -#define _ipasir_up_h_INCLUDED - -#include -#include - -/*------------------------------------------------------------------------*/ -#ifdef __cplusplus -extern "C" { -#endif -/*------------------------------------------------------------------------*/ - -// Add call-back which allows to learn, propagate and backtrack based on -// external constraints. Only one external propagator can be connected -// and after connection every related variables must be 'observed' (use -// 'add_observed_var' function). -// Disconnection of the external propagator resets all the observed -// variables. -// -// require (VALID) -// ensure (VALID) -// -void ipasir_connect_external_propagator( - void *solver, - void *propagator_data, - // Notify the propagator about assignments to observed variables. - // The notification is not necessarily eager. It usually happens before - // the call of propagator callbacks and when a driving clause is leading - // to an assignment. - void (*prop_notify_assignment) (void* prop, int lit, bool is_fixed), - void (*prop_notify_new_decision_level) (void* prop), - void (*prop_notify_backtrack) (void* prop, size_t new_level, bool restart), - // Check by the external propagator the found complete solution (after - // solution reconstruction). If it returns false, the propagator must - // provide an external clause during the next callback. - bool (*prop_cb_check_found_model) (void* prop, const int* model, size_t size), - // The following two functions are used to add external clauses to the - // solver during the CDCL loop. The external clause is added - // literal-by-literal and learned by the solver as an irredundant - // (original) input clause. The clause can be arbitrary, but if it is - // root-satisfied or tautology, the solver will ignore it without learning - // it. Root-falsified literals are eagerly removed from the clause. - // Falsified clauses trigger conflict analysis, propagating clauses - // trigger propagation. In case chrono is 0, the solver backtracks to - // propagate the new literal on the right decision level, otherwise it - // potentially will be an out-of-order assignment on the current level. - // Unit clauses always (unless root-satisfied, see above) trigger - // backtracking (independently from the value of the chrono option and - // independently from being falsified or satisfied or unassigned) to level - // 0. Empty clause (or root falsified clause, see above) makes the problem - // unsat and stops the search immediately. A literal 0 must close the - // clause. - // - // The external propagator indicates that there is a clause to add. - bool (*prop_cb_has_external_clause) (void* prop), - // The actual function called to add the external clause. - int (*prop_cb_add_external_clause_lit) (void* prop), - /// lazy propagator only checks complete assignments - bool is_lazy, - // Ask the external propagator for the next decision literal. If it - // returns 0, the solver makes its own choice. - int (*prop_cb_decide) (void* prop), - // Ask the external propagator if there is an external propagation to make - // under the current assignment. It returns either a literal to be - // propagated or 0, indicating that there is no external propagation under - // the current assignment. - int (*prop_cb_propagate) (void* prop), - // Ask the external propagator for the reason clause of a previous - // external propagation step (done by cb_propagate). The clause must be - // added literal-by-literal closed with a 0. Further, the clause must - // contain the propagated literal. - int (*prop_cb_add_reason_clause_lit) (void* prop, int propagated_lit) -); -void ipasir_disconnect_external_propagator(void *solver); - -// Mark as 'observed' those variables that are relevant to the external -// propagator. External propagation, clause addition during search and -// notifications are all over these observed variabes. -// A variable can not be observed witouth having an external propagator -// connected. Observed variables are "frozen" internally, and so -// inprocessing will not consider them as candidates for elimination. -// An observed variable is allowed to be a fresh variable and it can be -// added also during solving. -// -// require (VALID_OR_SOLVING) -// ensure (VALID_OR_SOLVING) -// -void ipasir_add_observed_var(void *solver, int32_t var); - -// Removes the 'observed' flag from the given variable. A variable can be -// set unobserved only between solve calls, not during it (to guarantee -// that no yet unexplained external propagation involves it). -// -// require (VALID) -// ensure (VALID) -// -void ipasir_remove_observed_var(void *solver, int32_t var); - -// Removes all the 'observed' flags from the variables. Disconnecting the -// propagator invokes this step as well. -// -// require (VALID) -// ensure (VALID) -// -void ipasir_reset_observed_vars(void *solver); - -// Get reason of valid observed literal (true = it is an observed variable -// and it got assigned by a decision during the CDCL loop. Otherwise: -// false. -// -// require (VALID_OR_SOLVING) -// ensure (VALID_OR_SOLVING) -// -bool ipasir_is_decision(void *solver, int32_t lit); - -/*------------------------------------------------------------------------*/ -#ifdef __cplusplus -} -#endif -/*------------------------------------------------------------------------*/ - -#endif diff --git a/crates/pindakaas-build-macros/src/lib.rs b/crates/pindakaas-build-macros/src/lib.rs index 281ccf0977..315435fdc6 100644 --- a/crates/pindakaas-build-macros/src/lib.rs +++ b/crates/pindakaas-build-macros/src/lib.rs @@ -78,39 +78,46 @@ macro_rules! ipasir_up_definitions { pub fn [<$prefix _connect_external_propagator>]( slv: *mut std::ffi::c_void, propagator_data: *mut std::ffi::c_void, - prop_notify_assignment: unsafe extern "C" fn(*mut std::ffi::c_void, i32, bool), + 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) -> 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), ); pub fn [<$prefix _disconnect_external_propagator>](slv: *mut std::ffi::c_void); pub fn [<$prefix _add_observed_var>](slv: *mut std::ffi::c_void, var: i32); pub fn [<$prefix _remove_observed_var>](slv: *mut std::ffi::c_void, var: i32); pub fn [<$prefix _reset_observed_vars>](slv: *mut std::ffi::c_void); pub fn [<$prefix _is_decision>](slv: *mut std::ffi::c_void, lit: i32) -> bool; + pub fn [<$prefix _force_backtrack>](slv: *mut std::ffi::c_void, new_level: usize); } #[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_assignment: unsafe extern "C" fn(*mut std::ffi::c_void, i32, bool), + 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) -> 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_assignment, 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, prop_cb_decide, prop_cb_propagate, prop_cb_add_reason_clause_lit) + [<$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) } pub unsafe fn ipasir_disconnect_external_propagator(slv: *mut std::ffi::c_void) { [<$prefix _disconnect_external_propagator>](slv) @@ -127,6 +134,9 @@ macro_rules! ipasir_up_definitions { pub unsafe fn ipasir_is_decision(slv: *mut std::ffi::c_void, lit: i32) -> bool { [<$prefix _is_decision>](slv, lit) } + pub unsafe fn ipasir_force_backtrack(slv: *mut std::ffi::c_void, new_level: usize) { + [<$prefix _force_backtrack>](slv, new_level) + } } } } @@ -152,6 +162,7 @@ pub fn change_ipasir_prefix(build: &mut Build, prefix: &str) { "_remove_observed_var", "_reset_observed_vars", "_is_decision", + "_force_backtrack", ] { let _ = build.define(&format!("ipasir{f}"), format!("{prefix}{f}").as_ref()); } diff --git a/crates/pindakaas-cadical/Cargo.toml b/crates/pindakaas-cadical/Cargo.toml index c41b1d0671..2a98a7d3b7 100644 --- a/crates/pindakaas-cadical/Cargo.toml +++ b/crates/pindakaas-cadical/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "pindakaas-cadical" description = "build of the Cadical SAT solver for the pindakaas crate" -version = "2.0.0" +version = "2.1.0" build = "build.rs" links = "cadical" exclude = ["vendor/cadical"] diff --git a/crates/pindakaas-cadical/src/ccadical_override.cpp b/crates/pindakaas-cadical/src/ccadical_override.cpp index 851c56389a..0bcff23d61 100644 --- a/crates/pindakaas-cadical/src/ccadical_override.cpp +++ b/crates/pindakaas-cadical/src/ccadical_override.cpp @@ -8,22 +8,25 @@ extern "C" { void ccadical_connect_external_propagator( CCaDiCaL *slv, void *propagator_data, - void (*prop_notify_assignment)(void *prop, int lit, bool is_fixed), + void (*prop_notify_assignments)(void *prop, const int *lits, size_t size), void (*prop_notify_new_decision_level)(void *prop), void (*prop_notify_backtrack)(void *prop, size_t new_level, bool restart), bool (*prop_cb_check_found_model)(void *prop, const int *model, size_t size), - bool (*prop_cb_has_external_clause)(void *prop), + bool (*prop_cb_has_external_clause)(void *prop, bool *is_forgettable), int (*prop_cb_add_external_clause_lit)(void *prop), bool is_lazy, + bool forgettable_reasons, bool notify_fixed, int (*prop_cb_decide)(void *prop), int (*prop_cb_propagate)(void *prop), - int (*prop_cb_add_reason_clause_lit)(void *prop, int propagated_lit)) { + int (*prop_cb_add_reason_clause_lit)(void *prop, int propagated_lit), + void (*prop_notify_fixed_assignment)(void *prop, int lit)) { ((Wrapper *)slv) ->solver->connect_external_propagator( - propagator_data, prop_notify_assignment, + 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, prop_cb_decide, - prop_cb_propagate, prop_cb_add_reason_clause_lit); + 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); } void ccadical_disconnect_external_propagator(CCaDiCaL *slv) { ((Wrapper *)slv)->solver->disconnect_external_propagator(); @@ -41,6 +44,9 @@ void ccadical_reset_observed_vars(CCaDiCaL *slv) { bool ccadical_is_decision(CCaDiCaL *slv, int lit) { return ((Wrapper *)slv)->solver->is_decision(lit); } +void ccadical_force_backtrack(CCaDiCaL *slv, size_t new_level) { + return ((Wrapper *)slv)->solver->force_backtrack(new_level); +} void ccadical_phase(CCaDiCaL *slv, int lit) { ((Wrapper *)slv)->solver->phase(lit); diff --git a/crates/pindakaas-cadical/src/ccadical_up.h b/crates/pindakaas-cadical/src/ccadical_up.h index e6ad8ec85b..9d3616a2b5 100644 --- a/crates/pindakaas-cadical/src/ccadical_up.h +++ b/crates/pindakaas-cadical/src/ccadical_up.h @@ -16,23 +16,27 @@ extern "C" { void ccadical_connect_external_propagator( CCaDiCaL *slv, void *propagator_data, - void (*prop_notify_assignment)(void *prop, int lit, bool is_fixed), + void (*prop_notify_assignments)(void *prop, const int *lits, size_t size), void (*prop_notify_new_decision_level)(void *prop), void (*prop_notify_backtrack)(void *prop, size_t new_level, bool restart), bool (*prop_cb_check_found_model)(void *prop, const int *model, size_t size), - bool (*prop_cb_has_external_clause)(void *prop), + bool (*prop_cb_has_external_clause)(void *prop, bool *is_forgettable), int (*prop_cb_add_external_clause_lit)(void *prop), bool is_lazy = false, + bool forgettable_reasons = false, bool notify_fixed = false, int (*prop_cb_decide)(void *prop) = prop_decide_default, int (*prop_cb_propagate)(void *prop) = prop_propagate_default, int (*prop_cb_add_reason_clause_lit)(void *prop, int propagated_lit) = - prop_add_reason_clause_lit_default); + prop_add_reason_clause_lit_default, + void (*prop_notify_fixed_assignment)(void *prop, int lit) = + prop_notify_fixed_assignment_default); void ccadical_disconnect_external_propagator(CCaDiCaL *); void ccadical_add_observed_var(CCaDiCaL *, int var); void ccadical_remove_observed_var(CCaDiCaL *, int var); void ccadical_reset_observed_vars(CCaDiCaL *); bool ccadical_is_decision(CCaDiCaL *, int lit); +void ccadical_force_backtrack(CCaDiCaL *, size_t new_level); // Additional C bindings for C++ Cadical diff --git a/crates/pindakaas-cadical/vendor/cadical b/crates/pindakaas-cadical/vendor/cadical index d45b475de7..a2abeb9c70 160000 --- a/crates/pindakaas-cadical/vendor/cadical +++ b/crates/pindakaas-cadical/vendor/cadical @@ -1 +1 @@ -Subproject commit d45b475de71009e50c9c596eb062db76fc66e3c1 +Subproject commit a2abeb9c7029274de148e92fcd7038928741155c diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs index 1edf467ebb..cecfb40a1c 100644 --- a/crates/pindakaas-derive/src/lib.rs +++ b/crates/pindakaas-derive/src/lib.rs @@ -191,22 +191,28 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } // If new propagator, set it now if let Some(p) = prop { - let is_lazy = p.is_lazy(); + let is_lazy = p.is_check_only(); + let forgettable_reasons = p.reason_persistence() == crate::solver::ClausePersistence::Forgettable; + let notify_fixed = p.enable_persistent_assignments(); + #prop_member = Some(crate::solver::libloading::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::libloading::ipasir_notify_assignment_cb::, + crate::solver::libloading::ipasir_notify_assignments_cb::, crate::solver::libloading::ipasir_notify_new_decision_level_cb::, crate::solver::libloading::ipasir_notify_backtrack_cb::, crate::solver::libloading::ipasir_check_model_cb::, crate::solver::libloading::ipasir_has_external_clause_cb::, crate::solver::libloading::ipasir_add_external_clause_lit_cb::, is_lazy, + forgettable_reasons, + notify_fixed, crate::solver::libloading::ipasir_decide_cb::, crate::solver::libloading::ipasir_propagate_cb::, crate::solver::libloading::ipasir_add_reason_clause_lit_cb::, + crate::solver::libloading::ipasir_notify_persistent_assignments_cb::, ) }; } @@ -263,6 +269,13 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } } + #[cfg(feature = "ipasir-up")] + impl crate::solver::ExtendedSolvingActions for #actions_ident { + fn force_backtrack(&mut self, new_level: usize) { + unsafe { #krate::ipasir_force_backtrack( self.ptr, new_level ) } + } + } + pub struct #sol_ident { ptr: *mut std::ffi::c_void, #[cfg(feature = "ipasir-up")] diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index c3319c38c6..5a48012d1a 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -135,12 +135,62 @@ pub trait MutPropagatorAccess { fn propagator_mut(&mut self) -> Option<&mut P>; } +#[cfg(feature = "ipasir-up")] +#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)] +/// A representation of a search decision made by a propagator. +pub enum SearchDecision { + /// Leave the search decision to the solver. + Free, + /// Make the decision to assign the given literal. + Assign(Lit), + /// Force the solver to backtrack to the given decision level. + Backtrack(usize), +} + +#[cfg(feature = "ipasir-up")] +#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)] +/// Whether a clause could possibly be removed from the clause database. +pub enum ClausePersistence { + /// The clause is to be considered forgettable. Its removal would not affect + /// the solver's correctness (in combination with the propagator), and it can + /// be re-derived if needed. + Forgettable, + /// The clause is to be considered irreduntant. It contains information that + /// can not (easily) be re-derived. + Irreduntant, +} + #[cfg(feature = "ipasir-up")] pub trait Propagator { - /// This method is called checked only when the propagator is connected. When - /// a Propagator is marked as lazy, it is only asked to check complete - /// assignments. - fn is_lazy(&self) -> bool { + /// Check whether the propagator only checks complete assignments. + /// + /// This method is called and checked only when the propagator is connected. If + /// the propagator returns `true`, it is only asked to validate wheter complete + /// assignments produced are correct. + fn is_check_only(&self) -> bool { + false + } + + /// Check whether the propagator's produced reasons are forgettable. + /// + /// This method is called and checked only when the propagator is connected. If + /// the propagator returns [`ClausePersistence::Forgettable`], then the solver + /// might remove the reason clause to save memory. The propagator must be able + /// to re-derive the reason clause at a later point. + fn reason_persistence(&self) -> ClausePersistence { + ClausePersistence::Irreduntant + } + + /// Check whether the propagator wants to be notified about persistent + /// assignments of literals. + /// + /// This method is called and checked only when the propagator is connected. If + /// the propagator returns `true`, then the + /// [`Self::notify_persistent_assignment`] method will be called (in addition + /// to [`Self::notify_assignments`]) to notify the propagator about assignemnts + /// that will persist for the remainder of the search for literals concerning + /// observed variables. + fn enable_persistent_assignments(&self) -> bool { false } @@ -150,18 +200,17 @@ pub trait Propagator { /// The notification is not necessarily eager. It usually happens before the /// call of propagator callbacks and when a driving clause is leading to an /// assignment. - /// - /// If [`persistent`] is set to `true`, then the assignment is known to - /// persist through backtracking. - fn notify_assignment(&mut self, lit: Lit, persistent: bool) { - let _ = lit; - let _ = persistent; + fn notify_assignments(&mut self, lits: &[Lit]) { + let _ = lits; } fn notify_new_decision_level(&mut self) {} fn notify_backtrack(&mut self, new_level: usize, restart: bool) { let _ = new_level; let _ = restart; } + fn notify_persistent_assignment(&mut self, lit: Lit) { + let _ = lit; + } /// Method called to check the found complete solution (after solution /// reconstruction). If it returns false, the propagator must provide an @@ -172,11 +221,14 @@ pub trait Propagator { true } - /// Method called when the solver asks for the next decision literal. If it - /// returns None, the solver makes its own choice. - fn decide(&mut self, slv: &mut dyn SolvingActions) -> Option { + /// Method called when the solver asks for the next search decision. + /// + /// The propagator can either decide to assign a given literal, force the + /// solver to backtrack to a given decision level, or leave the decision to the + /// solver. + fn decide(&mut self, slv: &mut dyn SolvingActions) -> SearchDecision { let _ = slv; - None + SearchDecision::Free } /// Method to ask the propagator if there is an propagation to make under the @@ -197,7 +249,10 @@ pub trait Propagator { } /// Method to ask whether there is an external clause to add to the solver. - fn add_external_clause(&mut self, slv: &mut dyn SolvingActions) -> Option> { + fn add_external_clause( + &mut self, + slv: &mut dyn SolvingActions, + ) -> Option<(Vec, ClausePersistence)> { let _ = slv; None } @@ -251,12 +306,22 @@ pub trait Propagator { } #[cfg(feature = "ipasir-up")] +/// A trait containing the solver methods that are exposed to the propagator +/// during solving. pub trait SolvingActions { fn new_var(&mut self) -> Var; fn add_observed_var(&mut self, var: Var); fn is_decision(&mut self, lit: Lit) -> bool; } +#[cfg(feature = "ipasir-up")] +/// A trait containing additional actions that the solver can perform during +/// solving. In contrast to [`SolvingActions`], these additional actions are not +/// exposed to the propagator. +pub(crate) trait ExtendedSolvingActions: SolvingActions { + fn force_backtrack(&mut self, level: usize); +} + #[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)] pub enum SlvTermSignal { Continue, diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index 57462da2a2..692d418039 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -169,8 +169,8 @@ mod tests { use crate::{ helpers::tests::assert_solutions, solver::{ - cadical::CadicalSol, NextVarRange, PropagatingSolver, Propagator, PropagatorAccess, - SolvingActions, VarRange, + cadical::CadicalSol, ClausePersistence, NextVarRange, PropagatingSolver, + Propagator, PropagatorAccess, SolvingActions, VarRange, }, Lit, }; @@ -184,7 +184,7 @@ mod tests { tmp: Vec>, } impl Propagator for Dist2 { - fn is_lazy(&self) -> bool { + fn is_check_only(&self) -> bool { true } fn check_model( @@ -205,8 +205,11 @@ mod tests { } self.tmp.is_empty() } - fn add_external_clause(&mut self, _slv: &mut dyn SolvingActions) -> Option> { - self.tmp.pop() + fn add_external_clause( + &mut self, + _slv: &mut dyn SolvingActions, + ) -> Option<(Vec, ClausePersistence)> { + self.tmp.pop().map(|c| (c, ClausePersistence::Forgettable)) } fn as_any(&self) -> &dyn Any { diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index fa49dfb648..8fd944c92f 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -9,7 +9,7 @@ use std::{ use libloading::{Library, Symbol}; #[cfg(feature = "ipasir-up")] -use crate::solver::{Propagator, SolvingActions}; +use crate::solver::{ExtendedSolvingActions, Propagator, SolvingActions}; use crate::{ solver::{ FailedAssumtions, LearnCallback, SlvTermSignal, SolveAssuming, SolveResult, Solver, @@ -484,7 +484,7 @@ impl PropagatorPointer { pub(crate) fn new(prop: P, slv: A) -> Self where P: Propagator + 'static, - A: SolvingActions + 'static, + A: ExtendedSolvingActions + 'static, { // Construct wrapping structures let store = IpasirPropStore::new(prop, slv); @@ -517,14 +517,16 @@ impl PropagatorPointer { // --- Callback functions for C propagator interface --- #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( +pub(crate) unsafe extern "C" fn ipasir_notify_assignments_cb( state: *mut c_void, - lit: i32, - is_fixed: bool, + lits: *const i32, + len: usize, ) { let prop = &mut *(state as *mut IpasirPropStore); - let lit = Lit(NonZeroI32::new(lit).unwrap()); - prop.prop.notify_assignment(lit, is_fixed); + if len > 0 { + let lits = std::slice::from_raw_parts(lits as *mut Lit, len); + prop.prop.notify_assignments(lits); + }; } #[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb( @@ -566,15 +568,29 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb( +pub(crate) unsafe extern "C" fn ipasir_notify_persistent_assignments_cb( + state: *mut c_void, + lit: i32, +) { + let prop = &mut *(state as *mut IpasirPropStore); + let lit = Lit(NonZeroI32::new(lit).unwrap()); + prop.prop.notify_persistent_assignment(lit); +} +#[cfg(feature = "ipasir-up")] +pub(crate) unsafe extern "C" fn ipasir_decide_cb( state: *mut c_void, ) -> i32 { + use crate::solver::SearchDecision; + let prop = &mut *(state as *mut IpasirPropStore); let slv = &mut prop.slv; - if let Some(l) = prop.prop.decide(slv) { - l.0.into() - } else { - 0 + match prop.prop.decide(slv) { + SearchDecision::Assign(lit) => lit.0.into(), + SearchDecision::Backtrack(level) => { + slv.force_backtrack(level); + 0 + } + SearchDecision::Free => 0, } } #[cfg(feature = "ipasir-up")] @@ -619,9 +635,15 @@ pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb< #[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_has_external_clause_cb( state: *mut c_void, + is_forgettable: *mut bool, ) -> bool { + use crate::solver::ClausePersistence; + let prop = &mut *(state as *mut IpasirPropStore); - prop.cqueue = prop.prop.add_external_clause(&mut prop.slv).map(Vec::into); + if let Some((clause, p)) = prop.prop.add_external_clause(&mut prop.slv) { + *is_forgettable = p == ClausePersistence::Forgettable; + prop.cqueue = Some(clause.into()); + } prop.cqueue.is_some() } #[cfg(feature = "ipasir-up")] @@ -632,21 +654,16 @@ pub(crate) unsafe extern "C" fn ipasir_add_external_clause_lit_cb< state: *mut c_void, ) -> i32 { let prop = &mut *(state as *mut IpasirPropStore); - if prop.cqueue.is_none() { + let Some(queue) = &mut prop.cqueue else { debug_assert!(false); - // This function shouldn't be called when "has_clause" returned false. - prop.cqueue = prop.prop.add_external_clause(&mut prop.slv).map(Vec::into); - } - if let Some(queue) = &mut prop.cqueue { - if let Some(l) = queue.pop_front() { - l.0.get() - } else { - prop.cqueue = None; - 0 // End of clause - } + // "has_clause" should have been called first and should have returned true. + // Just return 0 to signal empty clause. + return 0; + }; + if let Some(l) = queue.pop_front() { + l.0.get() } else { - debug_assert!(false); - // Even after re-assessing, no additional clause was found. Just return 0 - 0 + prop.cqueue = None; + 0 // End of clause } }