Skip to content

Commit

Permalink
Change the IPASIR UP implementation to directly use C callback functions
Browse files Browse the repository at this point in the history 
This removes one layer of indirection
  • Loading branch information
@Dekker1
Dekker1 committed Aug 14, 2024
1 parent 180c3dc commit 0e6cfbb
Show file tree
Hide file tree
Showing 8 changed files with 184 additions and 360 deletions.
121 changes: 51 additions & 70 deletions crates/pindakaas-build-macros/src/ipasir_up.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,57 @@ extern "C" {
// require (VALID)
// ensure (VALID)
//
void ipasir_connect_external_propagator(void *solver, void *propagator);
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),
// 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
Expand Down Expand Up @@ -63,75 +113,6 @@ void ipasir_reset_observed_vars(void *solver);
//
bool ipasir_is_decision(void *solver, int32_t lit);

void *ipasir_prop_init(void *state);
void ipasir_prop_release(void *prop);

// This flag is currently checked only when the propagator is connected.
// lazy propagator only checks complete assignments
void ipasir_prop_lazy(void *prop, bool is_lazy);

// 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 ipasir_prop_set_notify_assignment(
void *prop,
void (*notify_assignment)(void *state, int32_t lit, bool is_fixed));
void ipasir_prop_set_notify_new_decision_level(
void *prop, void (*notify_new_decision_level)(void *state));
void ipasir_prop_set_notify_backtrack(
void *prop, void (*notify_backtrack)(void *state, size_t new_level));

// 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.
void ipasir_prop_set_check_model(void *prop,
bool (*check_model)(void *state, size_t size,
const int32_t *model));

// Ask the external propagator for the next decision literal. If it
// returns 0, the solver makes its own choice.
void ipasir_prop_set_decide(void *prop, int32_t (*decide)(void *state));

// 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.
void ipasir_prop_set_propagate(void *prop, int32_t (*propagate)(void *state));

// 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.
void ipasir_prop_set_add_reason_clause_lit(
void *prop,
int32_t (*add_reason_clause_lit)(void *state, int propagated_lit));

// 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.
void ipasir_prop_set_has_external_clause(
void *prop, bool (*has_external_clause)(void *state));

// The actual function called to add the external clause.
void ipasir_prop_set_add_external_clause_lit(
void *prop, int32_t (*add_external_clause_lit)(void *state));

/*------------------------------------------------------------------------*/
#ifdef __cplusplus
}
Expand Down
97 changes: 33 additions & 64 deletions crates/pindakaas-build-macros/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,27 +74,43 @@ macro_rules! ipasir_up_definitions {
($prefix:ident) => {
paste! {
extern "C" {
pub fn [<$prefix _connect_external_propagator>](slv: *mut std::ffi::c_void, prop: *mut std::ffi::c_void);
#[allow(clippy::too_many_arguments)]
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_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),
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_add_external_clause_lit: unsafe extern "C" fn(*mut std::ffi::c_void) -> i32,
is_lazy: 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,
);
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 _prop_init>](state: *mut std::ffi::c_void) -> *mut std::ffi::c_void;
pub fn [<$prefix _prop_release>](prop: *mut std::ffi::c_void);
pub fn [<$prefix _prop_lazy>](prop: *mut std::ffi::c_void, is_lazy: bool);
pub fn [<$prefix _prop_set_notify_assignment>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, i32, bool)>);
pub fn [<$prefix _prop_set_notify_new_decision_level>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void)>);
pub fn [<$prefix _prop_set_notify_backtrack>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, usize)>);
pub fn [<$prefix _prop_set_check_model>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, usize, *const i32) -> bool>);
pub fn [<$prefix _prop_set_decide>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> i32>);
pub fn [<$prefix _prop_set_propagate>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> i32>);
pub fn [<$prefix _prop_set_add_reason_clause_lit>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, i32) -> i32>);
pub fn [<$prefix _prop_set_has_external_clause>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> bool>);
pub fn [<$prefix _prop_set_add_external_clause_lit>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> i32>);
}
pub unsafe fn ipasir_connect_external_propagator(slv: *mut std::ffi::c_void, prop: *mut std::ffi::c_void) {
[<$prefix _connect_external_propagator>](slv, prop)
}
#[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_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),
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_add_external_clause_lit: unsafe extern "C" fn(*mut std::ffi::c_void) -> i32,
is_lazy: 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,
){
[<$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)
}
pub unsafe fn ipasir_disconnect_external_propagator(slv: *mut std::ffi::c_void) {
[<$prefix _disconnect_external_propagator>](slv)
Expand All @@ -111,42 +127,6 @@ 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_prop_init(state: *mut std::ffi::c_void) -> *mut std::ffi::c_void {
[<$prefix _prop_init>](state)
}
pub unsafe fn ipasir_prop_release(prop: *mut std::ffi::c_void) {
[<$prefix _prop_release>](prop)
}
pub unsafe fn ipasir_prop_lazy(prop: *mut std::ffi::c_void, is_lazy: bool) {
[<$prefix _prop_lazy>](prop, is_lazy)
}
pub unsafe fn ipasir_prop_set_notify_assignment(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, i32, bool)>) {
[<$prefix _prop_set_notify_assignment>](prop, cb)
}
pub unsafe fn ipasir_prop_set_notify_new_decision_level(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void)>) {
[<$prefix _prop_set_notify_new_decision_level>](prop, cb)
}
pub unsafe fn ipasir_prop_set_notify_backtrack(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, usize)>) {
[<$prefix _prop_set_notify_backtrack>](prop, cb)
}
pub unsafe fn ipasir_prop_set_check_model(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, usize, *const i32) -> bool>) {
[<$prefix _prop_set_check_model>](prop, cb)
}
pub unsafe fn ipasir_prop_set_decide(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> i32>) {
[<$prefix _prop_set_decide>](prop, cb)
}
pub unsafe fn ipasir_prop_set_propagate(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> i32>) {
[<$prefix _prop_set_propagate>](prop, cb)
}
pub unsafe fn ipasir_prop_set_add_reason_clause_lit(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, i32) -> i32>) {
[<$prefix _prop_set_add_reason_clause_lit>](prop, cb)
}
pub unsafe fn ipasir_prop_set_has_external_clause(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> bool>) {
[<$prefix _prop_set_has_external_clause>](prop, cb)
}
pub unsafe fn ipasir_prop_set_add_external_clause_lit(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> i32>) {
[<$prefix _prop_set_add_external_clause_lit>](prop, cb)
}
}
}
}
Expand All @@ -166,23 +146,12 @@ pub fn change_ipasir_prefix(build: &mut Build, prefix: &str) {
"_set_terminate",
"_set_learn",
"_connect_external_propagator",
"_get_external_propagator",
"_disconnect_external_propagator",
"_add_observed_var",
"_remove_observed_var",
"_reset_observed_vars",
"_is_decision",
"_prop_init",
"_prop_release",
"_prop_lazy",
"_prop_set_notify_assignment",
"_prop_set_notify_new_decision_level",
"_prop_set_notify_backtrack",
"_prop_set_check_model",
"_prop_set_decide",
"_prop_set_propagate",
"_prop_set_add_reason_clause_lit",
"_prop_set_has_external_clause",
"_prop_set_add_external_clause_lit",
] {
build.define(&format!("ipasir{f}"), format!("{prefix}{f}").as_ref());
}
Expand Down
Loading

0 comments on commit 0e6cfbb

Please sign in to comment.