Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update Cadical to version 2.1.0 #74

Merged
merged 1 commit into from
Oct 10, 2024
Merged

Update Cadical to version 2.1.0 #74

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
122 changes: 0 additions & 122 deletions crates/pindakaas-build-macros/src/ipasir_up.h
View file
Open in desktop

This file was deleted.

21 changes: 16 additions & 5 deletions crates/pindakaas-build-macros/src/lib.rs
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading