IPASIR-UP interface

.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:

crates/pindakaas-build-macros/src/ipasir_up.h

@@ -0,0 +1,141 @@
+#ifndef _ipasir_up_h_INCLUDED
+#define _ipasir_up_h_INCLUDED
+
+#include <stddef.h>
+#include <stdint.h>
+
+/*------------------------------------------------------------------------*/
+#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_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

crates/pindakaas-build-macros/src/lib.rs

@@ -69,21 +69,121 @@ 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 _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<unsafe extern "C" fn(*mut std::ffi::c_void, i32, bool)>);
+				pub fn [<$prefix _prop_set_notify_new_decision_level>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void)>);
+				pub fn [<$prefix _prop_set_notify_backtrack>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, usize)>);
+				pub fn [<$prefix _prop_set_check_model>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, usize, *const i32) -> bool>);
+				pub fn [<$prefix _prop_set_decide>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> i32>);
+				pub fn [<$prefix _prop_set_propagate>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> i32>);
+				pub fn [<$prefix _prop_set_add_reason_clause_lit>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, i32) -> i32>);
+				pub fn [<$prefix _prop_set_has_external_clause>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> bool>);
+				pub fn [<$prefix _prop_set_add_external_clause_lit>](prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> 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_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<unsafe extern "C" fn(*mut std::ffi::c_void, i32, bool)>) {
+				[<$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<unsafe extern "C" fn(*mut std::ffi::c_void)>) {
+				[<$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<unsafe extern "C" fn(*mut std::ffi::c_void, usize)>) {
+				[<$prefix _prop_set_notify_backtrack>](prop, cb)
+			}
+			pub unsafe fn ipasir_prop_set_check_model(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, usize, *const i32) -> bool>) {
+				[<$prefix _prop_set_check_model>](prop, cb)
+			}
+			pub unsafe fn ipasir_prop_set_decide(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> i32>) {
+				[<$prefix _prop_set_decide>](prop, cb)
+			}
+			pub unsafe fn ipasir_prop_set_propagate(prop: *mut std::ffi::c_void, cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> 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<unsafe extern "C" fn(*mut std::ffi::c_void, i32) -> 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<unsafe extern "C" fn(*mut std::ffi::c_void) -> 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<unsafe extern "C" fn(*mut std::ffi::c_void) -> 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",
+		"_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());
+	}
 }

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();