Skip to content

Commit

Permalink
Update Cadical to version 2.1.0
Browse files Browse the repository at this point in the history 
This includes several changes to the IPASIR-UP interface
  • Loading branch information
@Dekker1
Dekker1 committed Oct 10, 2024
1 parent e9a239a commit 90631db
Show file tree
Hide file tree
Showing 10 changed files with 184 additions and 187 deletions.
122 changes: 0 additions & 122 deletions crates/pindakaas-build-macros/src/ipasir_up.h
View file

This file was deleted.

21 changes: 16 additions & 5 deletions crates/pindakaas-build-macros/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
}
}
}
}
Expand All @@ -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());
}
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas-cadical/Cargo.toml
View file
Original file line number Diff line number Diff line change
@@ -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"]
Expand Down
18 changes: 12 additions & 6 deletions crates/pindakaas-cadical/src/ccadical_override.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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);
Expand Down
10 changes: 7 additions & 3 deletions crates/pindakaas-cadical/src/ccadical_up.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas-cadical/vendor/cadical
Submodule cadical updated 45 files
+32 −0 NEWS.md
+32 −22 README.md
+1 −1 VERSION
+7 −1 configure
+55 −47 contrib/craigtracer.cpp
+6 −7 contrib/craigtracer.hpp
+36 −0 contrib/craigtracer.md
+27 −28 makefile.in
+1 −1 scripts/make-build-header.sh
+1 −1 scripts/make-src-release.sh
+2 −1 scripts/prepare-sc2021-submission.sh
+1 −1 src/backtrack.cpp
+68 −10 src/cadical.hpp
+29 −5 src/clause.cpp
+16 −6 src/decide.cpp
+2 −2 src/decompose.cpp
+10 −0 src/elim.cpp
+4 −8 src/extend.cpp
+119 −18 src/external.cpp
+31 −14 src/external.hpp
+323 −80 src/external_propagate.cpp
+2 −2 src/file.cpp
+11 −6 src/flags.cpp
+7 −0 src/flip.cpp
+55 −8 src/internal.cpp
+15 −1 src/internal.hpp
+1 −1 src/lratbuilder.cpp
+1 −1 src/lratchecker.cpp
+1 −1 src/minimize.cpp
+220 −98 src/mobical.cpp
+3 −3 src/options.hpp
+9 −1 src/probe.cpp
+2 −1 src/profile.hpp
+1 −0 src/propagate.cpp
+2 −1 src/queue.cpp
+1 −0 src/random.cpp
+1 −1 src/random.hpp
+3 −2 src/shrink.cpp
+3 −3 src/solution.cpp
+83 −8 src/solver.cpp
+10 −0 src/subsume.cpp
+1 −1 src/version.cpp
+3 −0 src/vivify.cpp
+4 −0 test/api/ctest.c
+8 −2 test/api/example.cpp
17 changes: 15 additions & 2 deletions crates/pindakaas-derive/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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::<P, #actions_ident>,
crate::solver::libloading::ipasir_notify_assignments_cb::<P, #actions_ident>,
crate::solver::libloading::ipasir_notify_new_decision_level_cb::<P, #actions_ident>,
crate::solver::libloading::ipasir_notify_backtrack_cb::<P, #actions_ident>,
crate::solver::libloading::ipasir_check_model_cb::<P, #actions_ident>,
crate::solver::libloading::ipasir_has_external_clause_cb::<P, #actions_ident>,
crate::solver::libloading::ipasir_add_external_clause_lit_cb::<P, #actions_ident>,
is_lazy,
forgettable_reasons,
notify_fixed,
crate::solver::libloading::ipasir_decide_cb::<P, #actions_ident>,
crate::solver::libloading::ipasir_propagate_cb::<P, #actions_ident>,
crate::solver::libloading::ipasir_add_reason_clause_lit_cb::<P, #actions_ident>,
crate::solver::libloading::ipasir_notify_persistent_assignments_cb::<P, #actions_ident>,
)
};
}
Expand Down Expand Up @@ -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")]
Expand Down
Loading

0 comments on commit 90631db

Please sign in to comment.