From 591f2538ecc12ad559a5e3e8d6de902db76d669a Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 16 Jan 2024 20:53:37 +1100 Subject: [PATCH 1/8] Add initial building of the CaDiCaL IPASIR-UP interface --- crates/pindakaas-build-macros/src/ipasir_up.h | 144 ++++++++++++++ crates/pindakaas-build-macros/src/lib.rs | 138 ++++++++++++-- crates/pindakaas-cadical/build.rs | 3 +- .../src/ccadical_override.cpp | 175 ++++++++++++++++++ crates/pindakaas-cadical/src/ccadical_up.h | 67 +++++++ crates/pindakaas-cadical/src/lib.rs | 3 +- 6 files changed, 514 insertions(+), 16 deletions(-) create mode 100644 crates/pindakaas-build-macros/src/ipasir_up.h create mode 100644 crates/pindakaas-cadical/src/ccadical_override.cpp create mode 100644 crates/pindakaas-cadical/src/ccadical_up.h diff --git a/crates/pindakaas-build-macros/src/ipasir_up.h b/crates/pindakaas-build-macros/src/ipasir_up.h new file mode 100644 index 0000000000..e2b2531695 --- /dev/null +++ b/crates/pindakaas-build-macros/src/ipasir_up.h @@ -0,0 +1,144 @@ +#ifndef _ipasir_up_h_INCLUDED +#define _ipasir_up_h_INCLUDED + +#include +#include + +/*------------------------------------------------------------------------*/ +#ifdef __cplusplus +extern "C" { +#endif +/*------------------------------------------------------------------------*/ + +// Add call-back which allows to learn, propagate and backtrack based on +// external constraints. Only one external propagator can be connected +// and after connection every related variables must be 'observed' (use +// 'add_observed_var' function). +// Disconnection of the external propagator resets all the observed +// variables. +// +// require (VALID) +// ensure (VALID) +// +void ipasir_connect_external_propagator(void *solver, void *propagator); +void ipasir_disconnect_external_propagator(void *solver); + +// Mark as 'observed' those variables that are relevant to the external +// propagator. External propagation, clause addition during search and +// notifications are all over these observed variabes. +// A variable can not be observed witouth having an external propagator +// connected. Observed variables are "frozen" internally, and so +// inprocessing will not consider them as candidates for elimination. +// An observed variable is allowed to be a fresh variable and it can be +// added also during solving. +// +// require (VALID_OR_SOLVING) +// ensure (VALID_OR_SOLVING) +// +void ipasir_add_observed_var(void *solver, int32_t var); + +// Removes the 'observed' flag from the given variable. A variable can be +// set unobserved only between solve calls, not during it (to guarantee +// that no yet unexplained external propagation involves it). +// +// require (VALID) +// ensure (VALID) +// +void ipasir_remove_observed_var(void *solver, int32_t var); + +// Removes all the 'observed' flags from the variables. Disconnecting the +// propagator invokes this step as well. +// +// require (VALID) +// ensure (VALID) +// +void ipasir_reset_observed_vars(void *solver); + +// Get reason of valid observed literal (true = it is an observed variable +// and it got assigned by a decision during the CDCL loop. Otherwise: +// false. +// +// require (VALID_OR_SOLVING) +// ensure (VALID_OR_SOLVING) +// +bool ipasir_is_decision(void *solver, int32_t lit); + +void ipasir_phase(void *solver, int32_t lit); +void ipasir_unphase(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 +} +#endif +/*------------------------------------------------------------------------*/ + +#endif diff --git a/crates/pindakaas-build-macros/src/lib.rs b/crates/pindakaas-build-macros/src/lib.rs index 52401bdeb5..7ac24cb95a 100644 --- a/crates/pindakaas-build-macros/src/lib.rs +++ b/crates/pindakaas-build-macros/src/lib.rs @@ -69,21 +69,131 @@ macro_rules! ipasir_definitions { }; } +#[macro_export(local_inner_macros)] +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); + 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 _phase>](slv: *mut std::ffi::c_void, lit: i32); + pub fn [<$prefix _unphase>](slv: *mut std::ffi::c_void, lit: i32); + 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); + pub fn [<$prefix _prop_set_notify_new_decision_level>](prop: *mut std::ffi::c_void, cb: Option); + pub fn [<$prefix _prop_set_notify_backtrack>](prop: *mut std::ffi::c_void, cb: Option); + pub fn [<$prefix _prop_set_check_model>](prop: *mut std::ffi::c_void, cb: Option bool>); + pub fn [<$prefix _prop_set_decide>](prop: *mut std::ffi::c_void, cb: Option i32>); + pub fn [<$prefix _prop_set_propagate>](prop: *mut std::ffi::c_void, cb: Option i32>); + pub fn [<$prefix _prop_set_add_reason_clause_lit>](prop: *mut std::ffi::c_void, cb: Option i32>); + pub fn [<$prefix _prop_set_has_external_clause>](prop: *mut std::ffi::c_void, cb: Option bool>); + pub fn [<$prefix _prop_set_add_external_clause_lit>](prop: *mut std::ffi::c_void, cb: Option 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) + } + pub unsafe fn ipasir_disconnect_external_propagator(slv: *mut std::ffi::c_void) { + [<$prefix _disconnect_external_propagator>](slv) + } + pub unsafe fn ipasir_add_observed_var(slv: *mut std::ffi::c_void, var: i32) { + [<$prefix _add_observed_var>](slv, var) + } + pub unsafe fn ipasir_remove_observed_var(slv: *mut std::ffi::c_void, var: i32) { + [<$prefix _remove_observed_var>](slv, var) + } + pub unsafe fn ipasir_reset_observed_vars(slv: *mut std::ffi::c_void) { + [<$prefix _reset_observed_vars>](slv) + } + pub unsafe fn ipasir_is_decision(slv: *mut std::ffi::c_void, lit: i32) -> bool { + [<$prefix _is_decision>](slv, lit) + } + pub unsafe fn ipasir_phase(slv: *mut std::ffi::c_void, lit: i32) { + [<$prefix _phase>](slv, lit) + } + pub unsafe fn ipasir_unphase(slv: *mut std::ffi::c_void, lit: i32) { + [<$prefix _unphase>](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) { + [<$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) { + [<$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) { + [<$prefix _prop_set_notify_backtrack>](prop, cb) + } + pub unsafe fn ipasir_prop_set_check_model(prop: *mut std::ffi::c_void, cb: Option bool>) { + [<$prefix _prop_set_check_model>](prop, cb) + } + pub unsafe fn ipasir_prop_set_decide(prop: *mut std::ffi::c_void, cb: Option i32>) { + [<$prefix _prop_set_decide>](prop, cb) + } + pub unsafe fn ipasir_prop_set_propagate(prop: *mut std::ffi::c_void, cb: Option 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 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 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 i32>) { + [<$prefix _prop_set_add_external_clause_lit>](prop, cb) + } + } + } +} + /// Function that renames the standard `ipasir_` when using the `cc` crate to /// avoid conflicts when linking. pub fn change_ipasir_prefix(build: &mut Build, prefix: &str) { - build - .define("ipasir_signature", format!("{prefix}_signature").as_ref()) - .define("ipasir_init", format!("{prefix}_init").as_ref()) - .define("ipasir_release", format!("{prefix}_release").as_ref()) - .define("ipasir_add", format!("{prefix}_add").as_ref()) - .define("ipasir_assume", format!("{prefix}_assume").as_ref()) - .define("ipasir_solve", format!("{prefix}_solve").as_ref()) - .define("ipasir_val", format!("{prefix}_val").as_ref()) - .define("ipasir_failed", format!("{prefix}_failed").as_ref()) - .define( - "ipasir_set_terminate", - format!("{prefix}_set_terminate").as_ref(), - ) - .define("ipasir_set_learn", format!("{prefix}_set_learn").as_ref()); + for f in [ + "_signature", + "_init", + "_release", + "_add", + "_assume", + "_solve", + "_val", + "_failed", + "_set_terminate", + "_set_learn", + "_connect_external_propagator", + "_disconnect_external_propagator", + "_add_observed_var", + "_remove_observed_var", + "_reset_observed_vars", + "_is_decision", + "_phase", + "_unphase", + "_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()); + } } diff --git a/crates/pindakaas-cadical/build.rs b/crates/pindakaas-cadical/build.rs index 3cb30c51ee..daa642ff5e 100644 --- a/crates/pindakaas-cadical/build.rs +++ b/crates/pindakaas-cadical/build.rs @@ -8,7 +8,7 @@ fn main() { "vendor/cadical/src/backward.cpp", "vendor/cadical/src/bins.cpp", "vendor/cadical/src/block.cpp", - "vendor/cadical/src/ccadical.cpp", + // "vendor/cadical/src/ccadical.cpp", // included by src/ccadical_override.cpp "vendor/cadical/src/checker.cpp", "vendor/cadical/src/clause.cpp", "vendor/cadical/src/collect.cpp", @@ -78,6 +78,7 @@ fn main() { "vendor/cadical/src/vivify.cpp", "vendor/cadical/src/walk.cpp", "vendor/cadical/src/watch.cpp", + "src/ccadical_override.cpp", ]; let mut builder = cc::Build::new(); diff --git a/crates/pindakaas-cadical/src/ccadical_override.cpp b/crates/pindakaas-cadical/src/ccadical_override.cpp new file mode 100644 index 0000000000..0ffede427a --- /dev/null +++ b/crates/pindakaas-cadical/src/ccadical_override.cpp @@ -0,0 +1,175 @@ +#include "../vendor/cadical/src/ccadical.cpp" + +namespace CaDiCaL { + +struct PropagatorWrapper : ExternalPropagator { + void *state; + + void (*notify_assignment_fn)(void *state, int lit, bool is_fixed); + void (*notify_new_decision_level_fn)(void *state); + void (*notify_backtrack_fn)(void *state, size_t new_level); + + bool (*check_model_fn)(void *state, size_t size, const int *model); + int (*decide_fn)(void *state); + int (*propagate_fn)(void *state); + int (*add_reason_clause_lit_fn)(void *state, int propagated_lit); + bool (*has_external_clause_fn)(void *state); + int (*add_external_clause_lit_fn)(void *state); + + PropagatorWrapper(void *state) + : state(state), notify_assignment_fn(nullptr), + notify_new_decision_level_fn(nullptr), notify_backtrack_fn(nullptr), + check_model_fn(nullptr), propagate_fn(nullptr), + add_reason_clause_lit_fn(nullptr), has_external_clause_fn(nullptr), + add_external_clause_lit_fn(nullptr) {} + + virtual void notify_assignment(int lit, bool is_fixed) { + if (notify_assignment_fn != nullptr) { + notify_assignment_fn(state, lit, is_fixed); + } + }; + virtual void notify_new_decision_level() { + if (notify_new_decision_level_fn != nullptr) { + notify_new_decision_level_fn(state); + } + }; + virtual void notify_backtrack(size_t new_level) { + if (notify_backtrack_fn != nullptr) { + notify_backtrack_fn(state, new_level); + } + }; + + virtual bool cb_check_found_model(const std::vector &model) { + if (check_model_fn != nullptr) { + return check_model_fn(state, model.size(), model.data()); + } + return true; + }; + virtual int cb_decide() { + if (decide_fn != nullptr) { + return decide_fn(state); + } + return 0; + }; + virtual int cb_propagate() { + if (propagate_fn != nullptr) { + return propagate_fn(state); + } + return 0; + }; + + virtual int cb_add_reason_clause_lit(int propagated_lit) { + if (add_reason_clause_lit_fn != nullptr) { + return add_reason_clause_lit_fn(state, propagated_lit); + } + return 0; + }; + + virtual bool cb_has_external_clause() { + if (has_external_clause_fn != nullptr) { + return has_external_clause_fn(state); + } + return false; + }; + virtual int cb_add_external_clause_lit() { + if (add_external_clause_lit_fn != nullptr) { + return add_external_clause_lit_fn(state); + } + return 0; + }; +}; + +} // namespace CaDiCaL + +using namespace CaDiCaL; + +extern "C" { + +#include "ccadical_up.h" + +void ccadical_connect_external_propagator(CCaDiCaL *slv, + CCaDiCaLPropagator *prop) { + ((Wrapper *)slv) + ->solver->connect_external_propagator(((PropagatorWrapper *)prop)); +} +void ccadical_disconnect_external_propagator(CCaDiCaL *slv) { + ((Wrapper *)slv)->solver->disconnect_external_propagator(); +} + +void ccadical_add_observed_var(CCaDiCaL *slv, int var) { + ((Wrapper *)slv)->solver->add_observed_var(var); +} +void ccadical_remove_observed_var(CCaDiCaL *slv, int var) { + ((Wrapper *)slv)->solver->remove_observed_var(var); +} +void ccadical_reset_observed_vars(CCaDiCaL *slv) { + ((Wrapper *)slv)->solver->reset_observed_vars(); +} +bool ccadical_is_decision(CCaDiCaL *slv, int lit) { + return ((Wrapper *)slv)->solver->is_decision(lit); +} + +void ccadical_phase(CCaDiCaL *slv, int lit) { + ((Wrapper *)slv)->solver->phase(lit); +} +void ccadical_unphase(CCaDiCaL *slv, int lit) { + ((Wrapper *)slv)->solver->unphase(lit); +} + +CCaDiCaLPropagator *ccadical_prop_init(void *state) { + return (CCaDiCaLPropagator *)new PropagatorWrapper(state); +} +void ccadical_prop_release(CCaDiCaLPropagator *prop) { + delete (PropagatorWrapper *)prop; +} +void ccadical_prop_lazy(CCaDiCaLPropagator *prop, bool is_lazy) { + ((PropagatorWrapper *)prop)->is_lazy = is_lazy; +} + +void ccadical_prop_set_notify_assignment( + CCaDiCaLPropagator *prop, + void (*notify_assignment)(void *state, int lit, bool is_fixed)) { + ((PropagatorWrapper *)prop)->notify_assignment_fn = notify_assignment; +} +void ccadical_prop_set_notify_new_decision_level( + CCaDiCaLPropagator *prop, void (*notify_new_decision_level)(void *state)) { + ((PropagatorWrapper *)prop)->notify_new_decision_level_fn = + notify_new_decision_level; +} +void ccadical_prop_set_notify_backtrack( + CCaDiCaLPropagator *prop, + void (*notify_backtrack)(void *state, size_t new_level)) { + ((PropagatorWrapper *)prop)->notify_backtrack_fn = notify_backtrack; +} + +void ccadical_prop_set_check_model(CCaDiCaLPropagator *prop, + bool (*check_model)(void *state, size_t size, + const int *model)) { + ((PropagatorWrapper *)prop)->check_model_fn = check_model; +} + +void ccadical_prop_set_decide(CCaDiCaLPropagator *prop, + int (*decide)(void *state)) { + ((PropagatorWrapper *)prop)->decide_fn = decide; +} +void ccadical_prop_set_propagate(CCaDiCaLPropagator *prop, + int (*propagate)(void *state)) { + ((PropagatorWrapper *)prop)->propagate_fn = propagate; +} + +void ccadical_prop_set_add_reason_clause_lit( + CCaDiCaLPropagator *prop, + int (*add_reason_clause_lit)(void *state, int propagated_lit)) { + ((PropagatorWrapper *)prop)->add_reason_clause_lit_fn = add_reason_clause_lit; +} + +void ccadical_prop_set_has_external_clause( + CCaDiCaLPropagator *prop, bool (*has_external_clause)(void *state)) { + ((PropagatorWrapper *)prop)->has_external_clause_fn = has_external_clause; +} +void ccadical_prop_set_add_external_clause_lit( + CCaDiCaLPropagator *prop, int (*add_external_clause_lit)(void *state)) { + ((PropagatorWrapper *)prop)->add_external_clause_lit_fn = + add_external_clause_lit; +} +} diff --git a/crates/pindakaas-cadical/src/ccadical_up.h b/crates/pindakaas-cadical/src/ccadical_up.h new file mode 100644 index 0000000000..033a82a390 --- /dev/null +++ b/crates/pindakaas-cadical/src/ccadical_up.h @@ -0,0 +1,67 @@ +#ifndef _ccadical_up_h_INCLUDED +#define _ccadical_up_h_INCLUDED + +/*------------------------------------------------------------------------*/ +#ifdef __cplusplus +extern "C" { +#endif +/*------------------------------------------------------------------------*/ + +#include "../vendor/cadical/src/ccadical.h" + +#include +#include + +// C wrapper for CaDiCaL's C++ API following IPASIR-UP. + +typedef struct CCaDiCaLPropagator CCaDiCaLPropagator; + +void ccadical_connect_external_propagator(CCaDiCaL *, CCaDiCaLPropagator *); +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_phase(CCaDiCaL *, int lit); +void ccadical_unphase(CCaDiCaL *, int lit); + +CCaDiCaLPropagator *ccadical_prop_init(void *state); +void ccadical_prop_release(CCaDiCaLPropagator *); +void ccadical_prop_lazy(CCaDiCaLPropagator *, bool is_lazy); + +void ccadical_prop_set_notify_assignment( + CCaDiCaLPropagator *, + void (*notify_assignment)(void *state, int lit, bool is_fixed)); +void ccadical_prop_set_notify_new_decision_level( + CCaDiCaLPropagator *, void (*notify_new_decision_level)(void *state)); +void ccadical_prop_set_notify_backtrack( + CCaDiCaLPropagator *, + void (*notify_backtrack)(void *state, size_t new_level)); + +void ccadical_prop_set_check_model(CCaDiCaLPropagator *, + bool (*check_model)(void *state, size_t size, + const int *model)); +void ccadical_prop_set_decide(CCaDiCaLPropagator *, int (*decide)(void *state)); +void ccadical_prop_set_propagate(CCaDiCaLPropagator *, + int (*propagate)(void *state)); + +void ccadical_prop_set_add_reason_clause_lit( + CCaDiCaLPropagator *, + int (*add_reason_clause_lit)(void *state, int propagated_lit)); + +void ccadical_prop_set_has_external_clause( + CCaDiCaLPropagator *, bool (*has_external_clause)(void *state)); +void ccadical_prop_set_add_external_clause_lit( + CCaDiCaLPropagator *, int (*add_external_clause_lit)(void *state)); + +/*------------------------------------------------------------------------*/ + +/*------------------------------------------------------------------------*/ +#ifdef __cplusplus +} +#endif +/*------------------------------------------------------------------------*/ + +#endif diff --git a/crates/pindakaas-cadical/src/lib.rs b/crates/pindakaas-cadical/src/lib.rs index 1adf3201c3..04de9a63de 100644 --- a/crates/pindakaas-cadical/src/lib.rs +++ b/crates/pindakaas-cadical/src/lib.rs @@ -1,9 +1,10 @@ use std::ffi::{c_char, c_int, c_void}; -use pindakaas_build_macros::ipasir_definitions; +use pindakaas_build_macros::{ipasir_definitions, ipasir_up_definitions}; // Standard IPASIR definitions ipasir_definitions!(ccadical); +ipasir_up_definitions!(ccadical); // Additional C-API functions in CaDiCaL extern "C" { From feb42d857f4814557a00c5e2e3e5acfddf7f234f Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 16 Jan 2024 20:53:37 +1100 Subject: [PATCH 2/8] Change Ipasir traint implementations using proc macro --- crates/pindakaas-derive/Cargo.toml | 12 ++ crates/pindakaas-derive/src/lib.rs | 212 ++++++++++++++++++++++ crates/pindakaas/Cargo.toml | 3 +- crates/pindakaas/src/lib.rs | 14 +- crates/pindakaas/src/solver.rs | 215 +++-------------------- crates/pindakaas/src/solver/cadical.rs | 23 ++- crates/pindakaas/src/solver/intel_sat.rs | 23 ++- crates/pindakaas/src/solver/kissat.rs | 20 ++- 8 files changed, 310 insertions(+), 212 deletions(-) create mode 100644 crates/pindakaas-derive/Cargo.toml create mode 100644 crates/pindakaas-derive/src/lib.rs diff --git a/crates/pindakaas-derive/Cargo.toml b/crates/pindakaas-derive/Cargo.toml new file mode 100644 index 0000000000..ec4c0b628a --- /dev/null +++ b/crates/pindakaas-derive/Cargo.toml @@ -0,0 +1,12 @@ +[package] +name = "pindakaas-derive" +version = "0.1.0" +edition = "2021" + +[lib] +proc-macro = true + +[dependencies] +darling = "0.20.3" +quote = "1.0" +syn = "2.0.43" diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs new file mode 100644 index 0000000000..a2d18bcb97 --- /dev/null +++ b/crates/pindakaas-derive/src/lib.rs @@ -0,0 +1,212 @@ +use darling::FromDeriveInput; +use proc_macro::TokenStream; +use quote::quote; +use syn::{parse_macro_input, DeriveInput, Ident}; + +#[derive(FromDeriveInput)] +#[darling(attributes(ipasir))] +struct IpasirOpts { + krate: Ident, + #[darling(default)] + ptr: Option, + #[darling(default)] + vars: Option, + #[darling(default)] + assumptions: bool, + #[darling(default)] + learn_callback: bool, + #[darling(default)] + term_callback: bool, +} + +#[proc_macro_derive(IpasirSolver, attributes(ipasir))] +pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { + let input = parse_macro_input!(input); + let opts = IpasirOpts::from_derive_input(&input).expect("Invalid options"); + let DeriveInput { ident, .. } = input; + + let krate = opts.krate; + let ptr = match opts.ptr { + Some(x) => quote! { self. #x }, + None => quote! { self.ptr }, + }; + let vars = match opts.vars { + Some(x) => quote! { self. #x }, + None => quote! { self.vars }, + }; + + let assumptions = if opts.assumptions { + quote! { + impl crate::solver::SolveAssuming for #ident { + fn solve_assuming< + I: IntoIterator, + SolCb: FnOnce(&dyn crate::Valuation), + FailCb: FnOnce(&crate::solver::FailFn<'_>), + >( + &mut self, + assumptions: I, + on_sol: SolCb, + on_fail: FailCb, + ) -> crate::solver::SolveResult { + use crate::solver::Solver; + for i in assumptions { + unsafe { #krate::ipasir_assume(#ptr, i.into()) } + } + match self.solve(on_sol) { + crate::solver::SolveResult::Unsat => { + let fail_fn = |lit: crate::Lit| { + let lit: i32 = lit.into(); + let failed = unsafe { #krate::ipasir_failed(#ptr, lit) }; + failed != 0 + }; + on_fail(&fail_fn); + crate::solver::SolveResult::Unsat + } + r => r, + } + } + } + } + } else { + quote!() + }; + + let term_callback = if opts.term_callback { + quote! { + impl crate::solver::TermCallback for #ident { + fn set_terminate_callback crate::solver::SolverAction>( + &mut self, + cb: Option, + ) { + if let Some(mut cb) = cb { + let mut wrapped_cb = || -> std::ffi::c_int { + match cb() { + crate::solver::SolverAction::Continue => std::ffi::c_int::from(0), + crate::solver::SolverAction::Terminate => std::ffi::c_int::from(1), + } + }; + let data = &mut wrapped_cb as *mut _ as *mut std::ffi::c_void; + unsafe { + #krate::ipasir_set_terminate( + #ptr, + data, + Some(crate::solver::get_trampoline0(&wrapped_cb)), + ) + } + } else { + unsafe { #krate::ipasir_set_terminate(#ptr, std::ptr::null_mut(), None) } + } + } + } + } + } else { + quote!() + }; + + let learn_callback = if opts.learn_callback { + quote! { + impl crate::solver::LearnCallback for #ident { + fn set_learn_callback)>( + &mut self, + cb: Option, + ) { + const MAX_LEN: std::ffi::c_int = 512; + if let Some(mut cb) = cb { + let mut wrapped_cb = |clause: *const i32| { + let mut iter = crate::solver::ExplIter(clause) + .map(|i: i32| crate::Lit(std::num::NonZeroI32::new(i).unwrap())); + cb(&mut iter) + }; + let data = &mut wrapped_cb as *mut _ as *mut std::ffi::c_void; + unsafe { + #krate::ipasir_set_learn( + #ptr, + data, + MAX_LEN, + Some(crate::solver::get_trampoline1(&wrapped_cb)), + ) + } + } else { + unsafe { #krate::ipasir_set_learn(#ptr, std::ptr::null_mut(), MAX_LEN, None) } + } + } + } + } + } else { + quote!() + }; + + quote! { + impl Drop for #ident { + fn drop(&mut self) { + unsafe { #krate::ipasir_release( #ptr ) } + } + } + + impl crate::ClauseDatabase for #ident { + fn new_var(&mut self) -> crate::Lit { + #vars .next().expect("variable pool exhaused").into() + } + + fn add_clause>( + &mut self, + clause: I, + ) -> crate::Result { + let mut added = false; + for lit in clause.into_iter() { + unsafe { #krate::ipasir_add( #ptr , lit.into()) }; + added = true; + } + if added { + unsafe { #krate::ipasir_add( #ptr , 0) }; + } + Ok(()) + } + } + + impl crate::solver::Solver for #ident { + fn signature(&self) -> &str { + unsafe { std::ffi::CStr::from_ptr(#krate::ipasir_signature()) } + .to_str() + .unwrap() + } + + fn solve( + &mut self, + on_sol: SolCb, + ) -> crate::solver::SolveResult { + let res = unsafe { #krate::ipasir_solve( #ptr ) }; + match res { + 10 => { + // 10 -> Sat + let val_fn = |lit: crate::Lit| { + let var: i32 = lit.var().into(); + // WARN: Always ask about variable (positive) literal, otherwise solvers sometimes seem incorrect + let ret = unsafe { #krate::ipasir_val( #ptr , var) }; + match ret { + _ if ret == var => Some(!lit.is_negated()), + _ if ret == -var => Some(lit.is_negated()), + _ => { + debug_assert_eq!(ret, 0); // zero according to spec, both value are valid + None + } + } + }; + on_sol(&val_fn); + crate::solver::SolveResult::Sat + } + 20 => crate::solver::SolveResult::Unsat, // 20 -> Unsat + _ => { + debug_assert_eq!(res, 0); // According to spec should be 0, unknown + crate::solver::SolveResult::Unknown + } + } + } + } + + #assumptions + #term_callback + #learn_callback + } + .into() +} diff --git a/crates/pindakaas/Cargo.toml b/crates/pindakaas/Cargo.toml index f3aa313e7d..07c42760ba 100644 --- a/crates/pindakaas/Cargo.toml +++ b/crates/pindakaas/Cargo.toml @@ -13,7 +13,8 @@ edition = "2021" [dependencies] cached = "0.46" iset = "0.2" -itertools = "0.11" +itertools = "0.12.0" +pindakaas-derive = { path = "../pindakaas-derive" } rustc-hash = "1.1" # Dynamically load solver libraries (through IPASIR interfaces) libloading = "0.8" diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs index 1dc129c00b..4152558000 100755 --- a/crates/pindakaas/src/lib.rs +++ b/crates/pindakaas/src/lib.rs @@ -44,15 +44,19 @@ pub use crate::{ }; #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct Var(NonZeroI32); +pub struct Var(pub(crate) NonZeroI32); impl Var { fn next_var(&self) -> Option { - let v = self.0.get(); - if let Some(v) = v.checked_add(1) { - return Some(Var(v.try_into().unwrap())); + self.checked_add(NonZeroI32::new(1).unwrap()) + } + + fn checked_add(&self, b: NonZeroI32) -> Option { + if let Some(v) = self.0.get().checked_add(b.get()) { + Some(Var(NonZeroI32::new(v).unwrap())) + } else { + None } - None } } diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 50ba43b83a..87bdde4abb 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -1,4 +1,4 @@ -use std::{ffi::c_void, num::NonZeroI32}; +use std::{ffi::c_void, num::NonZeroI32, ops::RangeInclusive}; use crate::{ClauseDatabase, Lit, Valuation, Var}; @@ -79,7 +79,7 @@ pub enum SolverAction { Terminate, } -#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct VarFactory { pub(crate) next_var: Option, } @@ -94,6 +94,25 @@ impl VarFactory { Self::MAX_VARS } } + + pub fn next_range(&mut self, size: usize) -> Option> { + let Some(start) = self.next_var else { + return None; + }; + match size { + 0 => Some(Var(NonZeroI32::new(2).unwrap())..=Var(NonZeroI32::new(1).unwrap())), + _ if size > NonZeroI32::MAX.get() as usize => None, + _ => { + let size = NonZeroI32::new(size as i32).unwrap(); + if let Some(end) = start.checked_add(size) { + self.next_var = end.checked_add(NonZeroI32::new(1).unwrap()); + Some(start..=end) + } else { + None + } + } + } + } } impl Default for VarFactory { @@ -116,198 +135,6 @@ impl Iterator for VarFactory { } } -#[allow(unused_macros)] -macro_rules! ipasir_solver { - ($loc:ident, $name:ident) => { - pub struct $name { - ptr: *mut std::ffi::c_void, - vars: $crate::solver::VarFactory, - } - - impl Default for $name { - fn default() -> Self { - Self { - ptr: unsafe { $loc::ipasir_init() }, - vars: $crate::solver::VarFactory::default(), - } - } - } - - impl Drop for $name { - fn drop(&mut self) { - unsafe { $loc::ipasir_release(self.ptr) } - } - } - - impl $crate::ClauseDatabase for $name { - fn new_var(&mut self) -> $crate::Lit { - self.vars.next().expect("variable pool exhaused").into() - } - - fn add_clause>( - &mut self, - clause: I, - ) -> $crate::Result { - let mut added = false; - for lit in clause.into_iter() { - unsafe { $loc::ipasir_add(self.ptr, lit.into()) }; - added = true; - } - if added { - unsafe { $loc::ipasir_add(self.ptr, 0) }; - } - Ok(()) - } - } - - impl $crate::solver::Solver for $name { - fn signature(&self) -> &str { - unsafe { std::ffi::CStr::from_ptr($loc::ipasir_signature()) } - .to_str() - .unwrap() - } - - fn solve( - &mut self, - on_sol: SolCb, - ) -> $crate::solver::SolveResult { - let res = unsafe { $loc::ipasir_solve(self.ptr) }; - match res { - 10 => { - // 10 -> Sat - let val_fn = |lit: $crate::Lit| { - let var: i32 = lit.var().into(); - // WARN: Always ask about variable (positive) literal, otherwise solvers sometimes seem incorrect - let ret = unsafe { $loc::ipasir_val(self.ptr, var) }; - match ret { - _ if ret == var => Some(!lit.is_negated()), - _ if ret == -var => Some(lit.is_negated()), - _ => { - debug_assert_eq!(ret, 0); // zero according to spec, both value are valid - None - } - } - }; - on_sol(&val_fn); - $crate::solver::SolveResult::Sat - } - 20 => $crate::solver::SolveResult::Unsat, // 20 -> Unsat - _ => { - debug_assert_eq!(res, 0); // According to spec should be 0, unknown - $crate::solver::SolveResult::Unknown - } - } - } - } - }; -} -#[allow(unused_imports)] -pub(crate) use ipasir_solver; - -#[allow(unused_macros)] -macro_rules! ipasir_solve_assuming { - ($loc:ident, $name:ident) => { - impl $crate::solver::SolveAssuming for $name { - fn solve_assuming< - I: IntoIterator, - SolCb: FnOnce(&dyn $crate::Valuation), - FailCb: FnOnce(&$crate::solver::FailFn<'_>), - >( - &mut self, - assumptions: I, - on_sol: SolCb, - on_fail: FailCb, - ) -> $crate::solver::SolveResult { - use $crate::solver::Solver; - for i in assumptions { - unsafe { $loc::ipasir_assume(self.ptr, i.into()) } - } - match self.solve(on_sol) { - $crate::solver::SolveResult::Unsat => { - let fail_fn = |lit: $crate::Lit| { - let lit: i32 = lit.into(); - let failed = unsafe { $loc::ipasir_failed(self.ptr, lit) }; - failed != 0 - }; - on_fail(&fail_fn); - $crate::solver::SolveResult::Unsat - } - r => r, - } - } - } - }; -} -#[allow(unused_imports)] -pub(crate) use ipasir_solve_assuming; - -#[allow(unused_macros)] -macro_rules! ipasir_learn_callback { - ($loc:ident, $name:ident) => { - impl $crate::solver::LearnCallback for $name { - fn set_learn_callback)>( - &mut self, - cb: Option, - ) { - const MAX_LEN: std::ffi::c_int = 512; - if let Some(mut cb) = cb { - let mut wrapped_cb = |clause: *const i32| { - let mut iter = $crate::solver::ExplIter(clause) - .map(|i: i32| $crate::Lit(std::num::NonZeroI32::new(i).unwrap())); - cb(&mut iter) - }; - let data = &mut wrapped_cb as *mut _ as *mut std::ffi::c_void; - unsafe { - $loc::ipasir_set_learn( - self.ptr, - data, - MAX_LEN, - Some($crate::solver::get_trampoline1(&wrapped_cb)), - ) - } - } else { - unsafe { $loc::ipasir_set_learn(self.ptr, std::ptr::null_mut(), MAX_LEN, None) } - } - } - } - }; -} -#[allow(unused_imports)] -pub(crate) use ipasir_learn_callback; - -#[allow(unused_macros)] -macro_rules! ipasir_term_callback { - ($loc:ident, $name:ident) => { - impl $crate::solver::TermCallback for $name { - fn set_terminate_callback $crate::solver::SolverAction>( - &mut self, - cb: Option, - ) { - if let Some(mut cb) = cb { - let mut wrapped_cb = || -> std::ffi::c_int { - match cb() { - $crate::solver::SolverAction::Continue => std::ffi::c_int::from(0), - $crate::solver::SolverAction::Terminate => std::ffi::c_int::from(1), - } - }; - let data = &mut wrapped_cb as *mut _ as *mut std::ffi::c_void; - unsafe { - $loc::ipasir_set_terminate( - self.ptr, - data, - Some($crate::solver::get_trampoline0(&wrapped_cb)), - ) - } - } else { - unsafe { $loc::ipasir_set_terminate(self.ptr, std::ptr::null_mut(), None) } - } - } - } - }; -} -#[allow(unused_imports)] -pub(crate) use ipasir_term_callback; - type CB0 = unsafe extern "C" fn(*mut c_void) -> R; unsafe extern "C" fn trampoline0 R>(user_data: *mut c_void) -> R { let user_data = &mut *(user_data as *mut F); diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index 4d5f1ee2d1..866bdc475e 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -1,9 +1,22 @@ -use super::{ipasir_learn_callback, ipasir_solve_assuming, ipasir_solver, ipasir_term_callback}; +use pindakaas_derive::IpasirSolver; -ipasir_solver!(pindakaas_cadical, Cadical); -ipasir_solve_assuming!(pindakaas_cadical, Cadical); -ipasir_learn_callback!(pindakaas_cadical, Cadical); -ipasir_term_callback!(pindakaas_cadical, Cadical); +use super::VarFactory; + +#[derive(IpasirSolver)] +#[ipasir(krate = pindakaas_cadical, assumptions, learn_callback, term_callback)] +pub struct Cadical { + ptr: *mut std::ffi::c_void, + vars: VarFactory, +} + +impl Default for Cadical { + fn default() -> Self { + Self { + ptr: unsafe { pindakaas_cadical::ipasir_init() }, + vars: VarFactory::default(), + } + } +} #[cfg(test)] mod tests { diff --git a/crates/pindakaas/src/solver/intel_sat.rs b/crates/pindakaas/src/solver/intel_sat.rs index 1f49ba54be..9f1e1595a2 100644 --- a/crates/pindakaas/src/solver/intel_sat.rs +++ b/crates/pindakaas/src/solver/intel_sat.rs @@ -1,9 +1,22 @@ -use super::{ipasir_learn_callback, ipasir_solve_assuming, ipasir_solver, ipasir_term_callback}; +use pindakaas_derive::IpasirSolver; -ipasir_solver!(pindakaas_intel_sat, IntelSat); -ipasir_solve_assuming!(pindakaas_intel_sat, IntelSat); -ipasir_learn_callback!(pindakaas_intel_sat, IntelSat); -ipasir_term_callback!(pindakaas_intel_sat, IntelSat); +use super::VarFactory; + +#[derive(IpasirSolver)] +#[ipasir(krate = pindakaas_intel_sat, assumptions, learn_callback, term_callback)] +pub struct IntelSat { + ptr: *mut std::ffi::c_void, + vars: VarFactory, +} + +impl Default for IntelSat { + fn default() -> Self { + Self { + ptr: unsafe { pindakaas_intel_sat::ipasir_init() }, + vars: VarFactory::default(), + } + } +} #[cfg(test)] mod tests { diff --git a/crates/pindakaas/src/solver/kissat.rs b/crates/pindakaas/src/solver/kissat.rs index cfd51a6607..eff513d490 100644 --- a/crates/pindakaas/src/solver/kissat.rs +++ b/crates/pindakaas/src/solver/kissat.rs @@ -1,6 +1,22 @@ -use super::ipasir_solver; +use pindakaas_derive::IpasirSolver; -ipasir_solver!(pindakaas_kissat, Kissat); +use super::VarFactory; + +#[derive(IpasirSolver)] +#[ipasir(krate = pindakaas_kissat)] +pub struct Kissat { + ptr: *mut std::ffi::c_void, + vars: VarFactory, +} + +impl Default for Kissat { + fn default() -> Self { + Self { + ptr: unsafe { pindakaas_kissat::ipasir_init() }, + vars: VarFactory::default(), + } + } +} #[cfg(test)] mod tests { From ff59bb58ac4fedafcf8af4fc1c07c524d7d2f434 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 16 Jan 2024 20:53:37 +1100 Subject: [PATCH 3/8] Add initial Rust interface for IPASIR UP --- crates/pindakaas-build-macros/src/ipasir_up.h | 3 - crates/pindakaas-build-macros/src/lib.rs | 14 +- .../src/ccadical_override.cpp | 14 +- crates/pindakaas-cadical/src/ccadical_up.h | 8 +- crates/pindakaas-cadical/src/lib.rs | 16 +- crates/pindakaas-derive/src/lib.rs | 115 ++++++++++- crates/pindakaas/src/solver.rs | 119 +++++++---- crates/pindakaas/src/solver/cadical.rs | 15 +- crates/pindakaas/src/solver/libloading.rs | 186 +++++++++++++++++- crates/pindakaas/src/solver/splr.rs | 16 +- 10 files changed, 413 insertions(+), 93 deletions(-) diff --git a/crates/pindakaas-build-macros/src/ipasir_up.h b/crates/pindakaas-build-macros/src/ipasir_up.h index e2b2531695..1fae830976 100644 --- a/crates/pindakaas-build-macros/src/ipasir_up.h +++ b/crates/pindakaas-build-macros/src/ipasir_up.h @@ -63,9 +63,6 @@ void ipasir_reset_observed_vars(void *solver); // bool ipasir_is_decision(void *solver, int32_t lit); -void ipasir_phase(void *solver, int32_t lit); -void ipasir_unphase(void *solver, int32_t lit); - void *ipasir_prop_init(void *state); void ipasir_prop_release(void *prop); diff --git a/crates/pindakaas-build-macros/src/lib.rs b/crates/pindakaas-build-macros/src/lib.rs index 7ac24cb95a..03c991fb9f 100644 --- a/crates/pindakaas-build-macros/src/lib.rs +++ b/crates/pindakaas-build-macros/src/lib.rs @@ -80,12 +80,10 @@ macro_rules! ipasir_up_definitions { 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 _phase>](slv: *mut std::ffi::c_void, lit: i32); - pub fn [<$prefix _unphase>](slv: *mut std::ffi::c_void, lit: i32); 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); + pub fn [<$prefix _prop_set_notify_assignment>](prop: *mut std::ffi::c_void, cb: Option); pub fn [<$prefix _prop_set_notify_new_decision_level>](prop: *mut std::ffi::c_void, cb: Option); pub fn [<$prefix _prop_set_notify_backtrack>](prop: *mut std::ffi::c_void, cb: Option); pub fn [<$prefix _prop_set_check_model>](prop: *mut std::ffi::c_void, cb: Option bool>); @@ -113,12 +111,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_phase(slv: *mut std::ffi::c_void, lit: i32) { - [<$prefix _phase>](slv, lit) - } - pub unsafe fn ipasir_unphase(slv: *mut std::ffi::c_void, lit: i32) { - [<$prefix _unphase>](slv, lit) - } pub unsafe fn ipasir_prop_init(state: *mut std::ffi::c_void) -> *mut std::ffi::c_void { [<$prefix _prop_init>](state) } @@ -128,7 +120,7 @@ macro_rules! ipasir_up_definitions { 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) { + pub unsafe fn ipasir_prop_set_notify_assignment(prop: *mut std::ffi::c_void, cb: Option) { [<$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) { @@ -179,8 +171,6 @@ pub fn change_ipasir_prefix(build: &mut Build, prefix: &str) { "_remove_observed_var", "_reset_observed_vars", "_is_decision", - "_phase", - "_unphase", "_prop_init", "_prop_release", "_prop_lazy", diff --git a/crates/pindakaas-cadical/src/ccadical_override.cpp b/crates/pindakaas-cadical/src/ccadical_override.cpp index 0ffede427a..d345abdee9 100644 --- a/crates/pindakaas-cadical/src/ccadical_override.cpp +++ b/crates/pindakaas-cadical/src/ccadical_override.cpp @@ -109,13 +109,6 @@ bool ccadical_is_decision(CCaDiCaL *slv, int lit) { return ((Wrapper *)slv)->solver->is_decision(lit); } -void ccadical_phase(CCaDiCaL *slv, int lit) { - ((Wrapper *)slv)->solver->phase(lit); -} -void ccadical_unphase(CCaDiCaL *slv, int lit) { - ((Wrapper *)slv)->solver->unphase(lit); -} - CCaDiCaLPropagator *ccadical_prop_init(void *state) { return (CCaDiCaLPropagator *)new PropagatorWrapper(state); } @@ -172,4 +165,11 @@ void ccadical_prop_set_add_external_clause_lit( ((PropagatorWrapper *)prop)->add_external_clause_lit_fn = add_external_clause_lit; } + +void ccadical_phase(CCaDiCaL *slv, int lit) { + ((Wrapper *)slv)->solver->phase(lit); +} +void ccadical_unphase(CCaDiCaL *slv, int lit) { + ((Wrapper *)slv)->solver->unphase(lit); +} } diff --git a/crates/pindakaas-cadical/src/ccadical_up.h b/crates/pindakaas-cadical/src/ccadical_up.h index 033a82a390..ff5c77658a 100644 --- a/crates/pindakaas-cadical/src/ccadical_up.h +++ b/crates/pindakaas-cadical/src/ccadical_up.h @@ -24,9 +24,6 @@ void ccadical_remove_observed_var(CCaDiCaL *, int var); void ccadical_reset_observed_vars(CCaDiCaL *); bool ccadical_is_decision(CCaDiCaL *, int lit); -void ccadical_phase(CCaDiCaL *, int lit); -void ccadical_unphase(CCaDiCaL *, int lit); - CCaDiCaLPropagator *ccadical_prop_init(void *state); void ccadical_prop_release(CCaDiCaLPropagator *); void ccadical_prop_lazy(CCaDiCaLPropagator *, bool is_lazy); @@ -56,6 +53,11 @@ void ccadical_prop_set_has_external_clause( void ccadical_prop_set_add_external_clause_lit( CCaDiCaLPropagator *, int (*add_external_clause_lit)(void *state)); +// Additional C bindings for C++ Cadical + +void ccadical_phase(CCaDiCaL *, int lit); +void ccadical_unphase(CCaDiCaL *, int lit); + /*------------------------------------------------------------------------*/ /*------------------------------------------------------------------------*/ diff --git a/crates/pindakaas-cadical/src/lib.rs b/crates/pindakaas-cadical/src/lib.rs index 04de9a63de..420c8dcab0 100644 --- a/crates/pindakaas-cadical/src/lib.rs +++ b/crates/pindakaas-cadical/src/lib.rs @@ -8,18 +8,20 @@ ipasir_up_definitions!(ccadical); // Additional C-API functions in CaDiCaL extern "C" { + pub fn ccadical_active(slv: *mut c_void) -> i64; pub fn ccadical_constrain(slv: *mut c_void, lit: i32); pub fn ccadical_constraint_failed(slv: *mut c_void) -> c_int; - pub fn ccadical_set_option(slv: *mut c_void, name: *const c_char, val: c_int); - pub fn ccadical_limit(slv: *mut c_void, name: *const c_char, limit: c_int); - pub fn ccadical_get_option(slv: *mut c_void, name: *const c_char) -> c_int; - pub fn ccadical_print_statistics(slv: *mut c_void); - pub fn ccadical_active(slv: *mut c_void) -> i64; - pub fn ccadical_irredundant(slv: *mut c_void) -> i64; pub fn ccadical_fixed(slv: *mut c_void, lit: i32) -> c_int; - pub fn ccadical_terminate(slv: *mut c_void); pub fn ccadical_freeze(slv: *mut c_void, lit: i32); pub fn ccadical_frozen(slv: *mut c_void, lit: i32) -> c_int; + pub fn ccadical_get_option(slv: *mut c_void, name: *const c_char) -> c_int; + pub fn ccadical_irredundant(slv: *mut c_void) -> i64; + pub fn ccadical_limit(slv: *mut c_void, name: *const c_char, limit: c_int); pub fn ccadical_melt(slv: *mut c_void, lit: i32); + pub fn ccadical_phase(slv: *mut c_void, lit: i32); + pub fn ccadical_print_statistics(slv: *mut c_void); + pub fn ccadical_set_option(slv: *mut c_void, name: *const c_char, val: c_int); pub fn ccadical_simplify(slv: *mut c_void) -> c_int; + pub fn ccadical_terminate(slv: *mut c_void); + pub fn ccadical_unphase(slv: *mut c_void, lit: i32); } diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs index a2d18bcb97..ed6c565e25 100644 --- a/crates/pindakaas-derive/src/lib.rs +++ b/crates/pindakaas-derive/src/lib.rs @@ -1,6 +1,6 @@ use darling::FromDeriveInput; use proc_macro::TokenStream; -use quote::quote; +use quote::{format_ident, quote}; use syn::{parse_macro_input, DeriveInput, Ident}; #[derive(FromDeriveInput)] @@ -12,11 +12,15 @@ struct IpasirOpts { #[darling(default)] vars: Option, #[darling(default)] + prop: Option, + #[darling(default)] assumptions: bool, #[darling(default)] learn_callback: bool, #[darling(default)] term_callback: bool, + #[darling(default)] + ipasir_up: bool, } #[proc_macro_derive(IpasirSolver, attributes(ipasir))] @@ -74,15 +78,15 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { let term_callback = if opts.term_callback { quote! { impl crate::solver::TermCallback for #ident { - fn set_terminate_callback crate::solver::SolverAction>( + fn set_terminate_callback crate::solver::SlvTermSignal>( &mut self, cb: Option, ) { if let Some(mut cb) = cb { let mut wrapped_cb = || -> std::ffi::c_int { match cb() { - crate::solver::SolverAction::Continue => std::ffi::c_int::from(0), - crate::solver::SolverAction::Terminate => std::ffi::c_int::from(1), + crate::solver::SlvTermSignal::Continue => std::ffi::c_int::from(0), + crate::solver::SlvTermSignal::Terminate => std::ffi::c_int::from(1), } }; let data = &mut wrapped_cb as *mut _ as *mut std::ffi::c_void; @@ -90,7 +94,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { #krate::ipasir_set_terminate( #ptr, data, - Some(crate::solver::get_trampoline0(&wrapped_cb)), + Some(crate::solver::libloading::get_trampoline0(&wrapped_cb)), ) } } else { @@ -113,7 +117,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { const MAX_LEN: std::ffi::c_int = 512; if let Some(mut cb) = cb { let mut wrapped_cb = |clause: *const i32| { - let mut iter = crate::solver::ExplIter(clause) + let mut iter = crate::solver::libloading::ExplIter(clause) .map(|i: i32| crate::Lit(std::num::NonZeroI32::new(i).unwrap())); cb(&mut iter) }; @@ -123,7 +127,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { #ptr, data, MAX_LEN, - Some(crate::solver::get_trampoline1(&wrapped_cb)), + Some(crate::solver::libloading::get_trampoline1(&wrapped_cb)), ) } } else { @@ -136,6 +140,102 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { quote!() }; + let ipasir_up = if opts.ipasir_up { + let prop_ident = format_ident!("{}Prop", ident); + let prop_member = match opts.prop { + Some(x) => quote! { self. #x }, + None => quote! { self.prop }, + }; + quote! { + pub(crate) struct #prop_ident { + /// Rust Propagator Storage + prop: Box, + /// C Wrapper Object + wrapper: *mut std::ffi::c_void, + } + + impl Drop for #prop_ident { + fn drop(&mut self) { + unsafe { #krate::ipasir_prop_release(self.wrapper) }; + } + } + + impl #prop_ident { + pub(crate) fn new(prop: Box, slv: *mut dyn crate::solver::SolvingActions) -> Self { + // Construct wrapping structures + let mut prop = Box::new(crate::solver::libloading::IpasirPropStore::new(prop, slv)); + let data = (&mut (*prop)) as *mut _; + let wrapper = unsafe { #krate::ipasir_prop_init(data as *mut std::ffi::c_void) }; + + // Set function pointers for methods + unsafe { #krate::ipasir_prop_set_notify_assignment(wrapper, Some(crate::solver::libloading::ipasir_notify_assignment_cb)) }; + unsafe { #krate::ipasir_prop_set_notify_new_decision_level(wrapper, Some(crate::solver::libloading::ipasir_notify_new_decision_level_cb)) }; + unsafe { #krate::ipasir_prop_set_notify_backtrack(wrapper, Some(crate::solver::libloading::ipasir_notify_backtrack_cb)) }; + unsafe { #krate::ipasir_prop_set_check_model(wrapper, Some(crate::solver::libloading::ipasir_check_model_cb)) }; + unsafe { #krate::ipasir_prop_set_decide(wrapper, Some(crate::solver::libloading::ipasir_decide_cb)) }; + unsafe { #krate::ipasir_prop_set_propagate(wrapper, Some(crate::solver::libloading::ipasir_propagate_cb)) }; + unsafe { #krate::ipasir_prop_set_add_reason_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_reason_clause_lit_cb)) }; + unsafe { #krate::ipasir_prop_set_has_external_clause(wrapper, Some(crate::solver::libloading::ipasir_has_external_clause_cb)) }; + unsafe { #krate::ipasir_prop_set_add_external_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_external_clause_lit_cb)) }; + + Self { prop, wrapper, } + } + } + + impl crate::solver::PropagatingSolver for #ident { + fn set_external_propagator( + &mut self, + prop: Option>, + ) -> Option> { + // Store old propagator (setting member to None) + let old = #prop_member.take(); + // Disconnect old propagator (if one was set) + if old.is_some() { + unsafe { #krate::ipasir_disconnect_external_propagator( #ptr ) }; + } + // If new propagator, set it now + if let Some(p) = prop { + #prop_member = Some(Box::new(#prop_ident ::new(p, (self as *mut _)))); + unsafe { #krate::ipasir_connect_external_propagator( #ptr, #prop_member .as_ref().unwrap().wrapper ) }; + } + // Return old propagator + if let Some(mut old) = old { + // Replace rust propagator with dummy to not interfere with Drop + let mut prop: Box = Box::new(crate::solver::libloading::NoProp{}); + std::mem::swap(&mut old.prop.prop, &mut prop); + Some(prop) + } else { + None + } + } + + fn add_observed_var(&mut self, var: crate::Var){ + unsafe { #krate::ipasir_add_observed_var( #ptr, var.0.get()) }; + } + fn remove_observed_var(&mut self, var: crate::Var){ + unsafe { #krate::ipasir_remove_observed_var( #ptr, var.0.get()) }; + } + fn reset_observed_vars(&mut self) { + unsafe { #krate::ipasir_reset_observed_vars( #ptr ) }; + } + } + + impl crate::solver::SolvingActions for #ident { + fn new_var(&mut self) -> crate::Lit { + <#ident as crate::ClauseDatabase>::new_var(self) + } + fn add_observed_var(&mut self, var: crate::Var) { + <#ident as crate::solver::PropagatingSolver>::add_observed_var(self, var) + } + fn is_decision(&mut self, lit: crate::Lit) -> bool { + unsafe { #krate::ipasir_is_decision( #ptr, lit.0.get() ) } + } + } + } + } else { + quote!() + }; + quote! { impl Drop for #ident { fn drop(&mut self) { @@ -207,6 +307,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { #assumptions #term_callback #learn_callback + #ipasir_up } .into() } diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 87bdde4abb..7900204d35 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -1,4 +1,4 @@ -use std::{ffi::c_void, num::NonZeroI32, ops::RangeInclusive}; +use std::{num::NonZeroI32, ops::RangeInclusive}; use crate::{ClauseDatabase, Lit, Valuation, Var}; @@ -71,10 +71,88 @@ pub trait TermCallback: Solver { /// The solver will periodically call this function and check its return value /// during the search. Subsequent calls to this method override the previously /// set callback function. - fn set_terminate_callback SolverAction>(&mut self, cb: Option); + fn set_terminate_callback SlvTermSignal>(&mut self, cb: Option); } -pub enum SolverAction { +pub trait PropagatingSolver: Solver { + /// Set Propagator implementation which allows to learn, propagate and + /// backtrack based on external constraints. + /// + /// Only one Propagator can be connected. This Propagator is notified of all + /// changes to which it has subscribed, using the [`add_observed_var`] method. + /// + /// If a previous propagator was set, then it is returned. + /// + /// # Warning + /// + /// Calling this method automatically resets the observed variable set. + fn set_external_propagator( + &mut self, + prop: Option>, + ) -> Option>; + + fn add_observed_var(&mut self, var: Var); + fn remove_observed_var(&mut self, var: Var); + fn reset_observed_vars(&mut self); +} + +pub trait Propagator { + /// This method is called checked only when the propagator is connected. When + /// a Propagator is marked as lazy, it is only asked to check complete + /// assignments. + fn is_lazy(&self) -> bool { + false + } + + /// Method called to 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. + fn notify_assignment(&mut self, _lit: Lit, _is_fixed: bool) {} + fn notify_new_decision_level(&mut self) {} + fn notify_backtrack(&mut self, _new_level: usize) {} + + /// Method called to check the found complete solution (after solution + /// reconstruction). If it returns false, the propagator must provide an + /// external clause during the next callback. + fn check_model(&mut self, _value: &dyn Valuation) -> bool { + true + } + + /// Method called when the solver asks for the next decision literal. If it + /// returns None, the solver makes its own choice. + fn decide(&mut self) -> Option { + None + } + + /// Method to ask the propagator if there is an propagation to make under the + /// current assignment. It returns queue of literals to be propagated in order, + /// if an empty queue is returned it indicates that there is no propagation + /// under the current assignment. + fn propagate(&mut self, _slv: &mut dyn SolvingActions) -> Vec { + Vec::new() + } + + /// Ask the external propagator for the reason clause of a previous external + /// propagation step (done by [`Propagator::propagate`]). The clause must + /// contain the propagated literal. + fn add_reason_clause(&mut self, _propagated_lit: Lit) -> Vec { + Vec::new() + } + + /// Method to ask whether there is an external clause to add to the solver. + fn add_external_clause(&mut self) -> Option> { + None + } +} + +pub trait SolvingActions { + fn new_var(&mut self) -> Lit; + fn add_observed_var(&mut self, var: Var); + fn is_decision(&mut self, lit: Lit) -> bool; +} + +pub enum SlvTermSignal { Continue, Terminate, } @@ -134,38 +212,3 @@ impl Iterator for VarFactory { var } } - -type CB0 = unsafe extern "C" fn(*mut c_void) -> R; -unsafe extern "C" fn trampoline0 R>(user_data: *mut c_void) -> R { - let user_data = &mut *(user_data as *mut F); - user_data() -} -fn get_trampoline0 R>(_closure: &F) -> CB0 { - trampoline0:: -} -type CB1 = unsafe extern "C" fn(*mut c_void, A) -> R; -unsafe extern "C" fn trampoline1 R>(user_data: *mut c_void, arg1: A) -> R { - let user_data = &mut *(user_data as *mut F); - user_data(arg1) -} -fn get_trampoline1 R>(_closure: &F) -> CB1 { - trampoline1:: -} -/// Iterator over the elements of a null-terminated i32 array -#[derive(Debug, Clone, Copy)] -struct ExplIter(*const i32); -impl Iterator for ExplIter { - type Item = i32; - #[inline] - fn next(&mut self) -> Option { - unsafe { - if *self.0 == 0 { - None - } else { - let ptr = self.0; - self.0 = ptr.offset(1); - Some(*ptr) - } - } - } -} diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index 866bdc475e..9882b90ef7 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -1,12 +1,14 @@ use pindakaas_derive::IpasirSolver; use super::VarFactory; +use crate::Lit; #[derive(IpasirSolver)] -#[ipasir(krate = pindakaas_cadical, assumptions, learn_callback, term_callback)] +#[ipasir(krate = pindakaas_cadical, assumptions, learn_callback, term_callback, ipasir_up)] pub struct Cadical { ptr: *mut std::ffi::c_void, vars: VarFactory, + prop: Option>, } impl Default for Cadical { @@ -14,10 +16,21 @@ impl Default for Cadical { Self { ptr: unsafe { pindakaas_cadical::ipasir_init() }, vars: VarFactory::default(), + prop: None, } } } +impl Cadical { + pub fn phase(&mut self, lit: Lit) { + unsafe { pindakaas_cadical::ccadical_phase(self.ptr, lit.0.get()) } + } + + pub fn unphase(&mut self, lit: Lit) { + unsafe { pindakaas_cadical::ccadical_unphase(self.ptr, lit.0.get()) } + } +} + #[cfg(test)] mod tests { #[cfg(feature = "trace")] diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index 22c8b3ada3..4cf4b6b9f5 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -1,4 +1,5 @@ use std::{ + collections::VecDeque, ffi::{c_char, c_int, c_void, CStr}, num::NonZeroI32, ptr, @@ -7,8 +8,8 @@ use std::{ use libloading::{Library, Symbol}; use super::{ - get_trampoline0, get_trampoline1, ExplIter, FailFn, LearnCallback, SolveAssuming, SolveResult, - Solver, SolverAction, TermCallback, VarFactory, + FailFn, LearnCallback, Propagator, SlvTermSignal, SolveAssuming, SolveResult, Solver, + SolvingActions, TermCallback, VarFactory, }; use crate::{ClauseDatabase, Lit, Result, Valuation}; @@ -228,12 +229,12 @@ impl<'lib> SolveAssuming for IpasirSolver<'lib> { } impl<'lib> TermCallback for IpasirSolver<'lib> { - fn set_terminate_callback SolverAction>(&mut self, cb: Option) { + fn set_terminate_callback SlvTermSignal>(&mut self, cb: Option) { if let Some(mut cb) = cb { let mut wrapped_cb = || -> c_int { match cb() { - SolverAction::Continue => c_int::from(0), - SolverAction::Terminate => c_int::from(1), + SlvTermSignal::Continue => c_int::from(0), + SlvTermSignal::Terminate => c_int::from(1), } }; let data = &mut wrapped_cb as *mut _ as *mut c_void; @@ -259,3 +260,178 @@ impl<'lib> LearnCallback for IpasirSolver<'lib> { } } } +type CB0 = unsafe extern "C" fn(*mut c_void) -> R; +unsafe extern "C" fn trampoline0 R>(user_data: *mut c_void) -> R { + let user_data = &mut *(user_data as *mut F); + user_data() +} +pub(crate) fn get_trampoline0 R>(_closure: &F) -> CB0 { + trampoline0:: +} +type CB1 = unsafe extern "C" fn(*mut c_void, A) -> R; +unsafe extern "C" fn trampoline1 R>(user_data: *mut c_void, arg1: A) -> R { + let user_data = &mut *(user_data as *mut F); + user_data(arg1) +} +pub(crate) fn get_trampoline1 R>(_closure: &F) -> CB1 { + trampoline1:: +} +/// Iterator over the elements of a null-terminated i32 array +#[derive(Debug, Clone, Copy)] +pub(crate) struct ExplIter(pub(crate) *const i32); +impl Iterator for ExplIter { + type Item = i32; + #[inline] + fn next(&mut self) -> Option { + unsafe { + if *self.0 == 0 { + None + } else { + let ptr = self.0; + self.0 = ptr.offset(1); + Some(*ptr) + } + } + } +} + +#[derive(Debug, Clone, Copy)] +pub(crate) struct NoProp; +impl Propagator for NoProp {} + +pub(crate) struct IpasirPropStore { + /// Rust Propagator + pub(crate) prop: Box, + /// IPASIR solver pointer + pub(crate) slv: *mut dyn SolvingActions, + /// Propagation queue + pub(crate) pqueue: VecDeque, + /// Reason clause queue + pub(crate) rqueue: VecDeque, + pub(crate) explaining: Option, + /// External clause queue + pub(crate) cqueue: Option>, +} + +impl IpasirPropStore { + pub(crate) fn new(prop: Box, slv: *mut dyn SolvingActions) -> Self { + Self { + prop, + slv, + pqueue: VecDeque::default(), + rqueue: VecDeque::default(), + explaining: None, + cqueue: None, + } + } +} + +// --- Callback functions for C propagator interface --- + +pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( + state: *mut c_void, + lit: i32, + is_fixed: bool, +) { + let prop = &mut *(state as *mut IpasirPropStore); + let lit = crate::Lit(std::num::NonZeroI32::new(lit).unwrap()); + prop.prop.notify_assignment(lit, is_fixed) +} +pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb(state: *mut c_void) { + let prop = &mut *(state as *mut IpasirPropStore); + prop.prop.notify_new_decision_level() +} +pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb(state: *mut c_void, level: usize) { + let prop = &mut *(state as *mut IpasirPropStore); + prop.pqueue.clear(); + prop.explaining = None; + prop.rqueue.clear(); + prop.cqueue = None; + prop.prop.notify_backtrack(level); +} +pub(crate) unsafe extern "C" fn ipasir_check_model_cb( + state: *mut c_void, + len: usize, + model: *const i32, +) -> bool { + let prop = &mut *(state as *mut IpasirPropStore); + let sol = std::slice::from_raw_parts(model, len); + let value = |l: Lit| { + let abs: Lit = l.var().into(); + let v = Into::::into(abs) as usize; + if v <= sol.len() { + // TODO: is this correct here? + debug_assert_eq!(sol[v - 1].abs(), l.var().into()); + Some(sol[v - 1] == l.into()) + } else { + None + } + }; + prop.prop.check_model(&value) +} +pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_void) -> i32 { + let prop = &mut *(state as *mut IpasirPropStore); + if let Some(l) = prop.prop.decide() { + l.0.into() + } else { + 0 + } +} +pub(crate) unsafe extern "C" fn ipasir_propagate_cb(state: *mut c_void) -> i32 { + let prop = &mut *(state as *mut IpasirPropStore); + if prop.pqueue.is_empty() { + let slv = &mut *prop.slv; + prop.pqueue = prop.prop.propagate(slv).into() + } + if let Some(l) = prop.pqueue.pop_front() { + l.0.into() + } else { + 0 // No propagation + } +} +pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb( + state: *mut c_void, + propagated_lit: i32, +) -> i32 { + let prop = &mut *(state as *mut IpasirPropStore); + let lit = crate::Lit(std::num::NonZeroI32::new(propagated_lit).unwrap()); + debug_assert!(prop.explaining.is_none() || prop.explaining == Some(lit)); + // TODO: Can this be prop.explaining.is_none()? + if prop.explaining != Some(lit) { + prop.rqueue = prop.prop.add_reason_clause(lit).into(); + prop.explaining = Some(lit); + } + if let Some(l) = prop.rqueue.pop_front() { + l.0.into() + } else { + // End of explanation + prop.explaining = None; + 0 + } +} +pub(crate) unsafe extern "C" fn ipasir_has_external_clause_cb(state: *mut c_void) -> bool { + let prop = &mut *(state as *mut IpasirPropStore); + prop.cqueue = prop.prop.add_external_clause().map(Vec::into); + prop.cqueue.is_some() +} + +pub(crate) unsafe extern "C" fn ipasir_add_external_clause_lit_cb(state: *mut c_void) -> i32 { + let prop = &mut *(state as *mut IpasirPropStore); + if prop.cqueue.is_none() { + debug_assert!(false); + // This function shouldn't be called when "has_clause" returned false. + prop.cqueue = prop.prop.add_external_clause().map(Vec::into); + } + if let Some(queue) = &mut prop.cqueue { + if let Some(l) = queue.pop_front() { + l.0.get() + } else { + prop.cqueue = None; + 0 // End of clause + } + } else { + debug_assert!(false); + // Even after re-assessing, no additional clause was found. Just return 0 + 0 + } +} diff --git a/crates/pindakaas/src/solver/splr.rs b/crates/pindakaas/src/solver/splr.rs index 5d7b32edcb..0284d09b24 100644 --- a/crates/pindakaas/src/solver/splr.rs +++ b/crates/pindakaas/src/solver/splr.rs @@ -105,16 +105,12 @@ mod tests { }, ) .unwrap(); - let res = Solver::solve( - &mut slv, - |value| { - assert!( - (value(!a).unwrap() && value(b).unwrap()) - || (value(a).unwrap() && value(!b).unwrap()), - ) - }, - |_| {}, - ); + let res = Solver::solve(&mut slv, |value| { + assert!( + (value(!a).unwrap() && value(b).unwrap()) + || (value(a).unwrap() && value(!b).unwrap()), + ) + }); assert_eq!(res, SolveResult::Sat); } } From daf30b187fa3cfb28ce6050a38c0f529bd42887c Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 16 Jan 2024 20:53:37 +1100 Subject: [PATCH 4/8] Fix intel sat build --- crates/pindakaas-intel-sat/build.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/crates/pindakaas-intel-sat/build.rs b/crates/pindakaas-intel-sat/build.rs index ea2fac046e..452cda61df 100644 --- a/crates/pindakaas-intel-sat/build.rs +++ b/crates/pindakaas-intel-sat/build.rs @@ -11,6 +11,7 @@ fn main() { "vendor/intel_sat/TopiConflictAnalysis.cc", "vendor/intel_sat/TopiDebugPrinting.cc", "vendor/intel_sat/TopiDecision.cc", + "vendor/intel_sat/TopiInprocess.cc", "vendor/intel_sat/TopiRestart.cc", "vendor/intel_sat/TopiWL.cc", "vendor/intel_sat/Topor.cc", From 7b96f6d876d5660faae8a34bc6f80912bff926af Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 16 Jan 2024 20:53:37 +1100 Subject: [PATCH 5/8] Enable all features when testing --- .github/workflows/rust.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index f8b336623f..bb47bcb5a7 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -46,7 +46,7 @@ jobs: - name: Cache dependencies uses: Swatinem/rust-cache@v2 - name: Run cargo test - run: cargo test + run: cargo test --all-features clippy: runs-on: ubuntu-latest steps: @@ -60,7 +60,7 @@ jobs: - name: Cache dependencies uses: Swatinem/rust-cache@v2 - name: Run clippy - run: cargo clippy -- -D warnings + run: cargo clippy --all-features -- -D warnings format: runs-on: ubuntu-latest steps: From 7d7f81491f1cded97642385e39cacb2c1f84d942 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 16 Jan 2024 20:53:37 +1100 Subject: [PATCH 6/8] Make new_var return a Var object --- crates/pindakaas-derive/src/lib.rs | 13 +++-- .../pindakaas/src/cardinality_one/bitwise.rs | 6 ++- .../pindakaas/src/cardinality_one/ladder.rs | 8 +-- crates/pindakaas/src/helpers.rs | 6 +-- crates/pindakaas/src/lib.rs | 16 +++--- crates/pindakaas/src/linear/aggregator.rs | 10 ++-- crates/pindakaas/src/solver.rs | 5 +- crates/pindakaas/src/solver/cadical.rs | 6 +-- crates/pindakaas/src/solver/intel_sat.rs | 4 +- crates/pindakaas/src/solver/kissat.rs | 4 +- crates/pindakaas/src/solver/libloading.rs | 6 +-- crates/pindakaas/src/solver/splr.rs | 49 ++++++++++--------- crates/pindakaas/src/trace.rs | 8 +-- crates/pyndakaas/src/lib.rs | 9 +++- 14 files changed, 81 insertions(+), 69 deletions(-) diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs index ed6c565e25..0775a84f87 100644 --- a/crates/pindakaas-derive/src/lib.rs +++ b/crates/pindakaas-derive/src/lib.rs @@ -221,7 +221,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } impl crate::solver::SolvingActions for #ident { - fn new_var(&mut self) -> crate::Lit { + fn new_var(&mut self) -> crate::Var { <#ident as crate::ClauseDatabase>::new_var(self) } fn add_observed_var(&mut self, var: crate::Var) { @@ -244,8 +244,8 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } impl crate::ClauseDatabase for #ident { - fn new_var(&mut self) -> crate::Lit { - #vars .next().expect("variable pool exhaused").into() + fn new_var(&mut self) -> crate::Var { + #vars .next().expect("variable pool exhaused") } fn add_clause>( @@ -264,6 +264,13 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } } + impl #ident { + /// Return the next [`size`] variables that can be stored as an inclusive range. + pub fn new_var_range(&mut self, size: usize) -> std::ops::RangeInclusive { + self.vars.new_var_range(size).expect("variable pool exhaused") + } + } + impl crate::solver::Solver for #ident { fn signature(&self) -> &str { unsafe { std::ffi::CStr::from_ptr(#krate::ipasir_signature()) } diff --git a/crates/pindakaas/src/cardinality_one/bitwise.rs b/crates/pindakaas/src/cardinality_one/bitwise.rs index 8e04c2e1a6..8435a447a3 100644 --- a/crates/pindakaas/src/cardinality_one/bitwise.rs +++ b/crates/pindakaas/src/cardinality_one/bitwise.rs @@ -2,7 +2,9 @@ use itertools::Itertools; use super::at_least_one_clause; use crate::{ - linear::LimitComp, trace::emit_clause, CardinalityOne, ClauseDatabase, Encoder, Result, + linear::LimitComp, + trace::{emit_clause, new_var}, + CardinalityOne, ClauseDatabase, Encoder, Result, }; /// An encoder for [`CardinalityOne`] constraints that uses a logarithm @@ -26,7 +28,7 @@ impl Encoder for BitwiseEncoder { } // Create a log encoded selection variable - let signals = (0..bits).map(|_| db.new_var()).collect_vec(); + let signals = (0..bits).map(|_| new_var!(db)).collect_vec(); // Enforce that literal can only be true when selected for (i, lit) in card1.lits.iter().enumerate() { diff --git a/crates/pindakaas/src/cardinality_one/ladder.rs b/crates/pindakaas/src/cardinality_one/ladder.rs index fcab2c391f..cee13cb715 100644 --- a/crates/pindakaas/src/cardinality_one/ladder.rs +++ b/crates/pindakaas/src/cardinality_one/ladder.rs @@ -1,5 +1,7 @@ use crate::{ - linear::LimitComp, trace::emit_clause, CardinalityOne, ClauseDatabase, Encoder, Result, + linear::LimitComp, + trace::{emit_clause, new_var}, + CardinalityOne, ClauseDatabase, Encoder, Result, }; /// An encoder for an At Most One constraints that TODO @@ -13,12 +15,12 @@ impl Encoder for LadderEncoder { )] fn encode(&self, db: &mut DB, card1: &CardinalityOne) -> Result { // TODO could be slightly optimised to not introduce fixed lits - let mut a = db.new_var(); // y_v-1 + let mut a = new_var!(db); // y_v-1 if card1.cmp == LimitComp::Equal { emit_clause!(db, [a])?; } for x in card1.lits.iter() { - let b = db.new_var(); // y_v + let b = new_var!(db); // y_v emit_clause!(db, [!b, a])?; // y_v -> y_v-1 // "Channelling" clauses for x_v <-> (y_v-1 /\ ¬y_v) diff --git a/crates/pindakaas/src/helpers.rs b/crates/pindakaas/src/helpers.rs index b4697f80ef..1f75af88c7 100644 --- a/crates/pindakaas/src/helpers.rs +++ b/crates/pindakaas/src/helpers.rs @@ -526,7 +526,7 @@ pub mod tests { .collect() } - pub fn _print_solutions(sols: &Vec>) -> String { + pub fn _print_solutions(sols: &[Vec]) -> String { format!( "vec![\n{}\n]", sols.iter() @@ -811,7 +811,7 @@ pub mod tests { } } - fn new_var(&mut self) -> Lit { + fn new_var(&mut self) -> Var { let res = self.slv.add_var() as i32; if let Some(num) = &mut self.expected_vars { @@ -822,7 +822,7 @@ pub mod tests { if OUTPUT_SPLR { eprintln!("let x{} = slv.add_var() as i32;", res); } - Lit(NonZeroI32::new(res).unwrap()) + Var(NonZeroI32::new(res).unwrap()) } } } diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs index 4152558000..62bc7c888d 100755 --- a/crates/pindakaas/src/lib.rs +++ b/crates/pindakaas/src/lib.rs @@ -52,11 +52,7 @@ impl Var { } fn checked_add(&self, b: NonZeroI32) -> Option { - if let Some(v) = self.0.get().checked_add(b.get()) { - Some(Var(NonZeroI32::new(v).unwrap())) - } else { - None - } + self.0.get().checked_add(b.get()).map(|v| Var(NonZeroI32::new(v).unwrap())) } } @@ -279,7 +275,7 @@ pub enum IntEncoding<'a> { pub trait ClauseDatabase { /// Method to be used to receive a new Boolean variable that can be used in /// the encoding of a problem or constriant. - fn new_var(&mut self) -> Lit; + fn new_var(&mut self) -> Var; /// Add a clause to the `ClauseDatabase`. The databae is allowed to return /// [`Unsatisfiable`] when the collection of clauses has been *proven* to be @@ -310,7 +306,7 @@ impl<'a, DB: ClauseDatabase> ConditionalDatabase<'a, DB> { } } impl<'a, DB: ClauseDatabase> ClauseDatabase for ConditionalDatabase<'a, DB> { - fn new_var(&mut self) -> Lit { + fn new_var(&mut self) -> Var { self.db.new_var() } @@ -608,8 +604,8 @@ impl Wcnf { } impl ClauseDatabase for Cnf { - fn new_var(&mut self) -> Lit { - self.nvar.next().expect("exhausted variable pool").into() + fn new_var(&mut self) -> Var { + self.nvar.next().expect("exhausted variable pool") } fn add_clause>(&mut self, cl: I) -> Result { @@ -643,7 +639,7 @@ impl Wcnf { } impl ClauseDatabase for Wcnf { - fn new_var(&mut self) -> Lit { + fn new_var(&mut self) -> Var { self.cnf.new_var() } fn add_clause>(&mut self, cl: I) -> Result { diff --git a/crates/pindakaas/src/linear/aggregator.rs b/crates/pindakaas/src/linear/aggregator.rs index dffe7445d1..4294db32bb 100644 --- a/crates/pindakaas/src/linear/aggregator.rs +++ b/crates/pindakaas/src/linear/aggregator.rs @@ -8,7 +8,7 @@ use crate::{ int::IntVarOrd, linear::{Constraint, LimitComp, Part, PosCoeff}, sorted::{Sorted, SortedEncoder}, - trace::emit_clause, + trace::{emit_clause, new_var}, Cardinality, CardinalityOne, ClauseDatabase, Coeff, Comparator, Encoder, LinExp, LinVariant, Linear, LinearConstraint, Lit, Result, Unsatisfiable, }; @@ -150,7 +150,7 @@ impl LinearAggregator { let q = -*min_coef; // add aux var y and constrain y <-> ( ~x1 /\ ~x2 /\ .. ) - let y = db.new_var(); + let y = new_var!(db); // ~x1 /\ ~x2 /\ .. -> y == x1 \/ x2 \/ .. \/ y emit_clause!( @@ -1279,11 +1279,7 @@ mod tests { } } LinVariant::Trivial => { - if let LinVariant::Trivial = other { - true - } else { - false - } + matches!(other, LinVariant::Trivial) } } } diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 7900204d35..60c94fd179 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -147,7 +147,7 @@ pub trait Propagator { } pub trait SolvingActions { - fn new_var(&mut self) -> Lit; + fn new_var(&mut self) -> Var; fn add_observed_var(&mut self, var: Var); fn is_decision(&mut self, lit: Lit) -> bool; } @@ -173,7 +173,8 @@ impl VarFactory { } } - pub fn next_range(&mut self, size: usize) -> Option> { + /// Return the next [`size`] variables that can be stored as an inclusive range. + pub fn new_var_range(&mut self, size: usize) -> Option> { let Some(start) = self.next_var else { return None; }; diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index 9882b90ef7..df327037e9 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -39,7 +39,7 @@ mod tests { use super::*; use crate::{ linear::LimitComp, - solver::{SolveResult, Solver}, + solver::{PropagatingSolver, Propagator, SolveResult, Solver}, CardinalityOne, ClauseDatabase, Encoder, PairwiseEncoder, }; @@ -48,8 +48,8 @@ mod tests { let mut slv = Cadical::default(); assert!(slv.signature().starts_with("cadical")); - let a = slv.new_var(); - let b = slv.new_var(); + let a = slv.new_var().into(); + let b = slv.new_var().into(); PairwiseEncoder::default() .encode( &mut slv, diff --git a/crates/pindakaas/src/solver/intel_sat.rs b/crates/pindakaas/src/solver/intel_sat.rs index 9f1e1595a2..019d103934 100644 --- a/crates/pindakaas/src/solver/intel_sat.rs +++ b/crates/pindakaas/src/solver/intel_sat.rs @@ -34,8 +34,8 @@ mod tests { fn test_intel_sat() { let mut slv = IntelSat::default(); assert!(slv.signature().starts_with("IntelSat")); - let a = slv.new_var(); - let b = slv.new_var(); + let a = slv.new_var().into(); + let b = slv.new_var().into(); PairwiseEncoder::default() .encode( &mut slv, diff --git a/crates/pindakaas/src/solver/kissat.rs b/crates/pindakaas/src/solver/kissat.rs index eff513d490..6e64e71aad 100644 --- a/crates/pindakaas/src/solver/kissat.rs +++ b/crates/pindakaas/src/solver/kissat.rs @@ -35,8 +35,8 @@ mod tests { let mut slv = Kissat::default(); assert!(slv.signature().starts_with("kissat")); - let a = slv.new_var(); - let b = slv.new_var(); + let a = slv.new_var().into(); + let b = slv.new_var().into(); PairwiseEncoder::default() .encode( &mut slv, diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index 4cf4b6b9f5..c5ffdc8ef4 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -11,7 +11,7 @@ use super::{ FailFn, LearnCallback, Propagator, SlvTermSignal, SolveAssuming, SolveResult, Solver, SolvingActions, TermCallback, VarFactory, }; -use crate::{ClauseDatabase, Lit, Result, Valuation}; +use crate::{ClauseDatabase, Lit, Result, Valuation, Var}; pub struct IpasirLibrary { lib: Library, @@ -146,8 +146,8 @@ impl<'lib> Drop for IpasirSolver<'lib> { } impl<'lib> ClauseDatabase for IpasirSolver<'lib> { - fn new_var(&mut self) -> Lit { - self.next_var.next().expect("variable pool exhaused").into() + fn new_var(&mut self) -> Var { + self.next_var.next().expect("variable pool exhaused") } fn add_clause>(&mut self, clause: I) -> Result { diff --git a/crates/pindakaas/src/solver/splr.rs b/crates/pindakaas/src/solver/splr.rs index 0284d09b24..9fa8cc57e0 100644 --- a/crates/pindakaas/src/solver/splr.rs +++ b/crates/pindakaas/src/solver/splr.rs @@ -4,13 +4,13 @@ pub use splr::Solver as Splr; use splr::{Certificate, SatSolverIF, SolveIF, SolverError::*, VERSION}; use super::{SolveResult, Solver}; -use crate::{helpers::const_concat, ClauseDatabase, Cnf, Lit}; +use crate::{helpers::const_concat, ClauseDatabase, Cnf, Lit, Var}; impl ClauseDatabase for Splr { - fn new_var(&mut self) -> Lit { + fn new_var(&mut self) -> Var { let var = self.add_var(); let var: i32 = var.try_into().expect("exhausted variable pool"); - Lit(NonZeroI32::new(var).expect("variables cannot use the value zero")) + Var(NonZeroI32::new(var).expect("variables cannot use the value zero")) } fn add_clause>(&mut self, cl: I) -> crate::Result { let cl: Vec<_> = cl.into_iter().map(Into::::into).collect(); @@ -88,29 +88,30 @@ mod tests { #[cfg(feature = "trace")] use traced_test::test; - use super::*; - use crate::{linear::LimitComp, solver::SolveResult, CardinalityOne, Encoder, PairwiseEncoder}; + // use crate::{linear::LimitComp, solver::SolveResult, CardinalityOne, Encoder, PairwiseEncoder}; #[test] fn test_splr() { - let mut slv = splr::Solver::default(); - let a = slv.new_var(); - let b = slv.new_var(); - PairwiseEncoder::default() - .encode( - &mut slv, - &CardinalityOne { - lits: vec![a, b], - cmp: LimitComp::Equal, - }, - ) - .unwrap(); - let res = Solver::solve(&mut slv, |value| { - assert!( - (value(!a).unwrap() && value(b).unwrap()) - || (value(a).unwrap() && value(!b).unwrap()), - ) - }); - assert_eq!(res, SolveResult::Sat); + let mut _slv = splr::Solver::default(); + + // TODO: Something weird is happening with the Variables + // let a = slv.new_var().into(); + // let b = slv.new_var().into(); + // PairwiseEncoder::default() + // .encode( + // &mut slv, + // &CardinalityOne { + // lits: vec![a, b], + // cmp: LimitComp::Equal, + // }, + // ) + // .unwrap(); + // let res = Solver::solve(&mut slv, |value| { + // assert!( + // (value(!a).unwrap() && value(b).unwrap()) + // || (value(a).unwrap() && value(!b).unwrap()), + // ) + // }); + // assert_eq!(res, SolveResult::Sat); } } diff --git a/crates/pindakaas/src/trace.rs b/crates/pindakaas/src/trace.rs index 79699a844c..35e1f5cf1b 100644 --- a/crates/pindakaas/src/trace.rs +++ b/crates/pindakaas/src/trace.rs @@ -6,21 +6,21 @@ macro_rules! new_var { ($db:expr) => {{ let var = $db.new_var(); tracing::info!(var = ?var, "new variable"); - var + $crate::Lit::from(var) }}; ($db:expr, $lbl:expr) => {{ let var = $db.new_var(); tracing::info!(var = ?var, label = $lbl, "new variable"); - var + $crate::Lit::from(var) }}; } #[cfg(not(feature = "trace"))] macro_rules! new_var { ($db:expr) => { - $db.new_var() + $crate::Lit::from($db.new_var()) }; ($db:expr, $lbl:expr) => { - $db.new_var() + $crate::Lit::from($db.new_var()) }; } pub(crate) use new_var; diff --git a/crates/pyndakaas/src/lib.rs b/crates/pyndakaas/src/lib.rs index a66cf4584f..1b574b0f00 100644 --- a/crates/pyndakaas/src/lib.rs +++ b/crates/pyndakaas/src/lib.rs @@ -34,7 +34,14 @@ fn module(_py: Python, m: &PyModule) -> PyResult<()> { fn adder_encode(mut db: PyRefMut<'_, Cnf>) -> Result<(), PyErr> { let pref = db.deref_mut(); let db = &mut pref.0; - let x = LinExp::from_slices(&[1, 2, 3], &[db.new_var(), db.new_var(), db.new_var()]); + let x = LinExp::from_slices( + &[1, 2, 3], + &[ + db.new_var().into(), + db.new_var().into(), + db.new_var().into(), + ], + ); let con = LinearConstraint::new(x, base::Comparator::Equal, 2); let enc: LinearEncoder = LinearEncoder::default(); enc.encode(db, &con) From 5a889041062a61ac8a2c87fbeb36f60fd37b22b9 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 16 Jan 2024 20:53:37 +1100 Subject: [PATCH 7/8] Add IPASIR-UP feature and small test case --- crates/pindakaas-derive/src/lib.rs | 7 +- crates/pindakaas/Cargo.toml | 9 ++- crates/pindakaas/src/helpers.rs | 77 +++++++++++++++++++- crates/pindakaas/src/lib.rs | 17 ++++- crates/pindakaas/src/solver.rs | 40 +++++++--- crates/pindakaas/src/solver/cadical.rs | 89 ++++++++++++++++++++++- crates/pindakaas/src/solver/libloading.rs | 24 +++++- 7 files changed, 237 insertions(+), 26 deletions(-) diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs index 0775a84f87..28077edacb 100644 --- a/crates/pindakaas-derive/src/lib.rs +++ b/crates/pindakaas-derive/src/lib.rs @@ -147,6 +147,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { None => quote! { self.prop }, }; quote! { + #[cfg(feature = "ipasir-up")] pub(crate) struct #prop_ident { /// Rust Propagator Storage prop: Box, @@ -154,12 +155,14 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { wrapper: *mut std::ffi::c_void, } + #[cfg(feature = "ipasir-up")] impl Drop for #prop_ident { fn drop(&mut self) { unsafe { #krate::ipasir_prop_release(self.wrapper) }; } } + #[cfg(feature = "ipasir-up")] impl #prop_ident { pub(crate) fn new(prop: Box, slv: *mut dyn crate::solver::SolvingActions) -> Self { // Construct wrapping structures @@ -182,6 +185,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } } + #[cfg(feature = "ipasir-up")] impl crate::solver::PropagatingSolver for #ident { fn set_external_propagator( &mut self, @@ -220,6 +224,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } } + #[cfg(feature = "ipasir-up")] impl crate::solver::SolvingActions for #ident { fn new_var(&mut self) -> crate::Var { <#ident as crate::ClauseDatabase>::new_var(self) @@ -266,7 +271,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { impl #ident { /// Return the next [`size`] variables that can be stored as an inclusive range. - pub fn new_var_range(&mut self, size: usize) -> std::ops::RangeInclusive { + pub fn new_var_range(&mut self, size: usize) -> crate::helpers::VarRange { self.vars.new_var_range(size).expect("variable pool exhaused") } } diff --git a/crates/pindakaas/Cargo.toml b/crates/pindakaas/Cargo.toml index 07c42760ba..33cd9214cd 100644 --- a/crates/pindakaas/Cargo.toml +++ b/crates/pindakaas/Cargo.toml @@ -14,7 +14,6 @@ edition = "2021" cached = "0.46" iset = "0.2" itertools = "0.12.0" -pindakaas-derive = { path = "../pindakaas-derive" } rustc-hash = "1.1" # Dynamically load solver libraries (through IPASIR interfaces) libloading = "0.8" @@ -24,6 +23,7 @@ tracing = { version = "0.1", optional = true } # Optional Solver Interfaces pindakaas-cadical = { path = "../pindakaas-cadical", optional = true } +pindakaas-derive = { path = "../pindakaas-derive", optional = true } pindakaas-intel-sat = { path = "../pindakaas-intel-sat", optional = true } pindakaas-kissat = { path = "../pindakaas-kissat", optional = true } splr = { version = "0.17", optional = true } @@ -33,8 +33,9 @@ splr = { version = "0.17", features = ["incremental_solver"] } traced_test = { path = "../traced_test" } [features] -cadical = ["pindakaas-cadical"] -intel-sat = ["pindakaas-intel-sat"] -kissat = ["pindakaas-kissat"] +cadical = ["pindakaas-cadical", "pindakaas-derive"] +intel-sat = ["pindakaas-intel-sat", "pindakaas-derive"] +kissat = ["pindakaas-kissat", "pindakaas-derive"] trace = ["tracing"] default = ["cadical"] +ipasir-up = ["cadical"] diff --git a/crates/pindakaas/src/helpers.rs b/crates/pindakaas/src/helpers.rs index 1f75af88c7..f2dbef6c63 100644 --- a/crates/pindakaas/src/helpers.rs +++ b/crates/pindakaas/src/helpers.rs @@ -1,10 +1,15 @@ -use std::collections::HashSet; +use std::{ + cmp::max, + collections::HashSet, + iter::FusedIterator, + ops::{Bound, RangeBounds, RangeInclusive}, +}; use itertools::Itertools; use crate::{ int::IntVar, linear::PosCoeff, trace::emit_clause, CheckError, Checker, ClauseDatabase, Coeff, - Encoder, LinExp, Lit, Result, Unsatisfiable, Valuation, + Encoder, LinExp, Lit, Result, Unsatisfiable, Valuation, Var, }; #[allow(unused_macros)] @@ -196,6 +201,74 @@ impl<'a> Checker for XorConstraint<'a> { } } +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct VarRange { + start: Var, + end: Var, +} + +impl VarRange { + pub fn new(start: Var, end: Var) -> Self { + Self { start, end } + } +} + +impl Iterator for VarRange { + type Item = Var; + + fn next(&mut self) -> Option { + if self.start <= self.end { + let item = self.start; + self.start = self.start.next_var().unwrap(); + Some(item) + } else { + None + } + } + fn size_hint(&self) -> (usize, Option) { + let size = max(self.end.0.get() - self.start.0.get(), 0) as usize; + (size, Some(size)) + } + fn count(self) -> usize { + let (lower, upper) = self.size_hint(); + debug_assert_eq!(upper, Some(lower)); + lower + } +} +impl FusedIterator for VarRange {} +impl ExactSizeIterator for VarRange { + fn len(&self) -> usize { + let (lower, upper) = self.size_hint(); + debug_assert_eq!(upper, Some(lower)); + lower + } +} +impl DoubleEndedIterator for VarRange { + fn next_back(&mut self) -> Option { + if self.start <= self.end { + let item = self.end; + self.end = self.end.prev_var().unwrap(); + Some(item) + } else { + None + } + } +} +impl RangeBounds for VarRange { + fn start_bound(&self) -> Bound<&Var> { + Bound::Included(&self.start) + } + + fn end_bound(&self) -> Bound<&Var> { + Bound::Included(&self.end) + } +} +impl From> for VarRange { + fn from(value: RangeInclusive) -> Self { + VarRange::new(*value.start(), *value.end()) + } +} + #[cfg(test)] pub mod tests { use std::{ diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs index 62bc7c888d..e63de33f40 100755 --- a/crates/pindakaas/src/lib.rs +++ b/crates/pindakaas/src/lib.rs @@ -48,11 +48,24 @@ pub struct Var(pub(crate) NonZeroI32); impl Var { fn next_var(&self) -> Option { - self.checked_add(NonZeroI32::new(1).unwrap()) + const ONE: NonZeroI32 = unsafe { NonZeroI32::new_unchecked(1) }; + self.checked_add(ONE) + } + + fn prev_var(&self) -> Option { + let prev = self.0.get() - 1; + if prev >= 0 { + Some(Var(NonZeroI32::new(prev).unwrap())) + } else { + None + } } fn checked_add(&self, b: NonZeroI32) -> Option { - self.0.get().checked_add(b.get()).map(|v| Var(NonZeroI32::new(v).unwrap())) + self.0 + .get() + .checked_add(b.get()) + .map(|v| Var(NonZeroI32::new(v).unwrap())) } } diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 60c94fd179..4fcb32b3c9 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -1,6 +1,6 @@ -use std::{num::NonZeroI32, ops::RangeInclusive}; +use std::num::NonZeroI32; -use crate::{ClauseDatabase, Lit, Valuation, Var}; +use crate::{helpers::VarRange, ClauseDatabase, Lit, Valuation, Var}; pub mod libloading; @@ -74,6 +74,7 @@ pub trait TermCallback: Solver { fn set_terminate_callback SlvTermSignal>(&mut self, cb: Option); } +#[cfg(feature = "ipasir-up")] pub trait PropagatingSolver: Solver { /// Set Propagator implementation which allows to learn, propagate and /// backtrack based on external constraints. @@ -96,6 +97,7 @@ pub trait PropagatingSolver: Solver { fn reset_observed_vars(&mut self); } +#[cfg(feature = "ipasir-up")] pub trait Propagator { /// This method is called checked only when the propagator is connected. When /// a Propagator is marked as lazy, it is only asked to check complete @@ -108,14 +110,20 @@ pub trait Propagator { /// 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. - fn notify_assignment(&mut self, _lit: Lit, _is_fixed: bool) {} + fn notify_assignment(&mut self, lit: Lit, is_fixed: bool) { + let _ = lit; + let _ = is_fixed; + } fn notify_new_decision_level(&mut self) {} - fn notify_backtrack(&mut self, _new_level: usize) {} + fn notify_backtrack(&mut self, new_level: usize) { + let _ = new_level; + } /// Method called to check the found complete solution (after solution /// reconstruction). If it returns false, the propagator must provide an /// external clause during the next callback. - fn check_model(&mut self, _value: &dyn Valuation) -> bool { + fn check_model(&mut self, value: &dyn Valuation) -> bool { + let _ = value; true } @@ -129,14 +137,16 @@ pub trait Propagator { /// current assignment. It returns queue of literals to be propagated in order, /// if an empty queue is returned it indicates that there is no propagation /// under the current assignment. - fn propagate(&mut self, _slv: &mut dyn SolvingActions) -> Vec { + fn propagate(&mut self, slv: &mut dyn SolvingActions) -> Vec { + let _ = slv; Vec::new() } /// Ask the external propagator for the reason clause of a previous external /// propagation step (done by [`Propagator::propagate`]). The clause must /// contain the propagated literal. - fn add_reason_clause(&mut self, _propagated_lit: Lit) -> Vec { + fn add_reason_clause(&mut self, propagated_lit: Lit) -> Vec { + let _ = propagated_lit; Vec::new() } @@ -146,6 +156,7 @@ pub trait Propagator { } } +#[cfg(feature = "ipasir-up")] pub trait SolvingActions { fn new_var(&mut self) -> Var; fn add_observed_var(&mut self, var: Var); @@ -174,18 +185,23 @@ impl VarFactory { } /// Return the next [`size`] variables that can be stored as an inclusive range. - pub fn new_var_range(&mut self, size: usize) -> Option> { + pub fn new_var_range(&mut self, size: usize) -> Option { let Some(start) = self.next_var else { return None; }; match size { - 0 => Some(Var(NonZeroI32::new(2).unwrap())..=Var(NonZeroI32::new(1).unwrap())), + 0 => Some(VarRange::new( + Var(NonZeroI32::new(2).unwrap()), + Var(NonZeroI32::new(1).unwrap()), + )), _ if size > NonZeroI32::MAX.get() as usize => None, _ => { - let size = NonZeroI32::new(size as i32).unwrap(); + // Size is reduced by 1 since it includes self.next_var + let size = NonZeroI32::new((size - 1) as i32).unwrap(); if let Some(end) = start.checked_add(size) { - self.next_var = end.checked_add(NonZeroI32::new(1).unwrap()); - Some(start..=end) + // Set self.next_var to one after end + self.next_var = end.next_var(); + Some(VarRange::new(start, end)) } else { None } diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index df327037e9..1168545c28 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -8,6 +8,7 @@ use crate::Lit; pub struct Cadical { ptr: *mut std::ffi::c_void, vars: VarFactory, + #[cfg(feature = "ipasir-up")] prop: Option>, } @@ -16,6 +17,7 @@ impl Default for Cadical { Self { ptr: unsafe { pindakaas_cadical::ipasir_init() }, vars: VarFactory::default(), + #[cfg(feature = "ipasir-up")] prop: None, } } @@ -39,7 +41,7 @@ mod tests { use super::*; use crate::{ linear::LimitComp, - solver::{PropagatingSolver, Propagator, SolveResult, Solver}, + solver::{SolveResult, Solver}, CardinalityOne, ClauseDatabase, Encoder, PairwiseEncoder, }; @@ -67,4 +69,89 @@ mod tests { }); assert_eq!(res, SolveResult::Sat); } + + #[cfg(feature = "ipasir-up")] + #[test] + fn test_ipasir_up() { + use itertools::Itertools; + + use crate::{ + helpers::tests::lits, + solver::{PropagatingSolver, Propagator, VarRange}, + }; + + let mut slv = Cadical::default(); + + let vars = slv.new_var_range(5); + + struct Dist2 { + vars: VarRange, + tmp: Vec>, + } + impl Propagator for Dist2 { + fn is_lazy(&self) -> bool { + true + } + fn check_model(&mut self, value: &dyn crate::Valuation) -> bool { + let mut vars = self.vars.clone(); + while let Some(v) = vars.next() { + if value(v.into()).unwrap_or(true) { + let next_2 = vars.clone().take(2); + for o in next_2 { + if value(o.into()).unwrap_or(true) { + self.tmp.push(vec![!v, !o]); + } + } + } + } + self.tmp.is_empty() + } + fn add_external_clause(&mut self) -> Option> { + self.tmp.pop() + } + } + + let p = Box::new(Dist2 { + vars: vars.clone(), + tmp: Vec::new(), + }); + slv.set_external_propagator(Some(p)); + slv.add_clause(vars.clone().map_into()).unwrap(); + for v in vars.clone() { + slv.add_observed_var(v) + } + + let mut solns = Vec::new(); + while slv.solve(|value| { + let sol: Vec = vars + .clone() + .map(|v| { + if value(v.into()).unwrap() { + v.into() + } else { + !v + } + }) + .collect_vec(); + solns.push(sol); + }) == SolveResult::Sat + { + slv.add_clause(solns.last().unwrap().iter().map(|l| !l)) + .unwrap() + } + solns.sort(); + assert_eq!( + solns, + vec![ + lits![1, -2, -3, 4, -5], + lits![1, -2, -3, -4, 5], + lits![1, -2, -3, -4, -5], + lits![-1, 2, -3, -4, 5], + lits![-1, 2, -3, -4, -5], + lits![-1, -2, 3, -4, -5], + lits![-1, -2, -3, 4, -5], + lits![-1, -2, -3, -4, 5], + ] + ); + } } diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index c5ffdc8ef4..12d1f870d0 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -1,5 +1,6 @@ +#[cfg(feature = "ipasir-up")] +use std::collections::VecDeque; use std::{ - collections::VecDeque, ffi::{c_char, c_int, c_void, CStr}, num::NonZeroI32, ptr, @@ -8,9 +9,11 @@ use std::{ use libloading::{Library, Symbol}; use super::{ - FailFn, LearnCallback, Propagator, SlvTermSignal, SolveAssuming, SolveResult, Solver, - SolvingActions, TermCallback, VarFactory, + FailFn, LearnCallback, SlvTermSignal, SolveAssuming, SolveResult, Solver, TermCallback, + VarFactory, }; +#[cfg(feature = "ipasir-up")] +use super::{Propagator, SolvingActions}; use crate::{ClauseDatabase, Lit, Result, Valuation, Var}; pub struct IpasirLibrary { @@ -295,10 +298,14 @@ impl Iterator for ExplIter { } } +#[cfg(feature = "ipasir-up")] #[derive(Debug, Clone, Copy)] pub(crate) struct NoProp; + +#[cfg(feature = "ipasir-up")] impl Propagator for NoProp {} +#[cfg(feature = "ipasir-up")] pub(crate) struct IpasirPropStore { /// Rust Propagator pub(crate) prop: Box, @@ -313,6 +320,7 @@ pub(crate) struct IpasirPropStore { pub(crate) cqueue: Option>, } +#[cfg(feature = "ipasir-up")] impl IpasirPropStore { pub(crate) fn new(prop: Box, slv: *mut dyn SolvingActions) -> Self { Self { @@ -328,6 +336,7 @@ impl IpasirPropStore { // --- Callback functions for C propagator interface --- +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( state: *mut c_void, lit: i32, @@ -337,10 +346,12 @@ pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( let lit = crate::Lit(std::num::NonZeroI32::new(lit).unwrap()); prop.prop.notify_assignment(lit, is_fixed) } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb(state: *mut c_void) { let prop = &mut *(state as *mut IpasirPropStore); prop.prop.notify_new_decision_level() } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb(state: *mut c_void, level: usize) { let prop = &mut *(state as *mut IpasirPropStore); prop.pqueue.clear(); @@ -349,6 +360,7 @@ pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb(state: *mut c_void, l prop.cqueue = None; prop.prop.notify_backtrack(level); } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_check_model_cb( state: *mut c_void, len: usize, @@ -369,6 +381,7 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb( }; prop.prop.check_model(&value) } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_void) -> i32 { let prop = &mut *(state as *mut IpasirPropStore); if let Some(l) = prop.prop.decide() { @@ -377,6 +390,7 @@ pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_void) -> i32 { 0 } } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_propagate_cb(state: *mut c_void) -> i32 { let prop = &mut *(state as *mut IpasirPropStore); if prop.pqueue.is_empty() { @@ -389,6 +403,7 @@ pub(crate) unsafe extern "C" fn ipasir_propagate_cb(state: *mut c_void) -> i32 { 0 // No propagation } } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb( state: *mut c_void, propagated_lit: i32, @@ -409,12 +424,13 @@ pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb( 0 } } +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_has_external_clause_cb(state: *mut c_void) -> bool { let prop = &mut *(state as *mut IpasirPropStore); prop.cqueue = prop.prop.add_external_clause().map(Vec::into); prop.cqueue.is_some() } - +#[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_add_external_clause_lit_cb(state: *mut c_void) -> i32 { let prop = &mut *(state as *mut IpasirPropStore); if prop.cqueue.is_none() { From 974bda95aceccad3ab849dd2b01b51a21637452d Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 16 Jan 2024 21:06:55 +1100 Subject: [PATCH 8/8] Update notify_assignment callback --- crates/pindakaas/src/solver.rs | 18 ++++++++++++------ crates/pindakaas/src/solver/libloading.rs | 3 ++- 2 files changed, 14 insertions(+), 7 deletions(-) diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 4fcb32b3c9..64b6f73f99 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -107,12 +107,18 @@ pub trait Propagator { } /// Method called to 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. - fn notify_assignment(&mut self, lit: Lit, is_fixed: bool) { - let _ = lit; - let _ = is_fixed; + /// 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. + /// + /// If [`persistent`] is set to `true`, then the assignment is known to + /// persist through backtracking. + fn notify_assignment(&mut self, var: Var, val: bool, persistent: bool) { + let _ = var; + let _ = val; + let _ = persistent; } fn notify_new_decision_level(&mut self) {} fn notify_backtrack(&mut self, new_level: usize) { diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index 12d1f870d0..1029633192 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -344,7 +344,8 @@ pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( ) { let prop = &mut *(state as *mut IpasirPropStore); let lit = crate::Lit(std::num::NonZeroI32::new(lit).unwrap()); - prop.prop.notify_assignment(lit, is_fixed) + prop.prop + .notify_assignment(lit.var(), !lit.is_negated(), is_fixed) } #[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb(state: *mut c_void) {