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 4245595
Show file tree
Hide file tree
Showing 12 changed files with 398 additions and 534 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/rust.yml
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ jobs:
cache: false
channel: ${{ env.RUST_COV_CHANNEL }}
- name: Run cargo test
run: cargo test -p pindakaas --features splr,cadical,ipasir-up,tracing
run: cargo test -p pindakaas --features splr,cadical,external-propagation,tracing
if: matrix.os == 'windows-latest'
- name: Run cargo test
run: cargo test --all-features
Expand Down
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 4245595

Please sign in to comment.