Skip to content

Commit

Permalink
Make solve methods return solution/fail (reference) objects
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Dekker1 committed Oct 28, 2024
1 parent e8da0d4 commit 5510ca1
Show file tree
Hide file tree
Showing 10 changed files with 394 additions and 530 deletions.
28 changes: 14 additions & 14 deletions crates/pindakaas-build-macros/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
Expand Down
Loading

0 comments on commit 5510ca1

Please sign in to comment.