diff --git a/.config/abbreviations.dic b/.config/abbreviations.dic index b279e471..4c76289c 100644 --- a/.config/abbreviations.dic +++ b/.config/abbreviations.dic @@ -1,4 +1,4 @@ -26 +27 AIJ API APIs @@ -17,6 +17,7 @@ GCD IJCAI IPASIR IPASIR's +JSAT MCNF MOPB OPB diff --git a/.config/lingo.dic b/.config/lingo.dic index 9dddfa07..9d93a0f6 100644 --- a/.config/lingo.dic +++ b/.config/lingo.dic @@ -1,4 +1,4 @@ -37 +38 accessor al AllDifferent @@ -11,6 +11,7 @@ boolean cardinality changelog children's +comparator decrementing encoding/S et diff --git a/.config/names.dic b/.config/names.dic index 7bd6a87d..2eb4b2cf 100644 --- a/.config/names.dic +++ b/.config/names.dic @@ -1,4 +1,4 @@ -55 +58 Argelich Armin Audemard @@ -12,7 +12,7 @@ Boufkhad bzip2 CaDiCaL CaDiCaL's -Een +Eén Fazekas Fleury Gihwon @@ -24,11 +24,13 @@ Jeremias Joao Josep Joshi +Joose Katalin Kissat Kissat's Klieber Kwon +Lett Lynce Manquinho Matti @@ -52,5 +54,6 @@ Tobias Treengeling Vasco vOptLib +Warners WebAssembly Yacine diff --git a/.github/workflows/capi.yml b/.github/workflows/capi.yml index c776d203..e447ce28 100644 --- a/.github/workflows/capi.yml +++ b/.github/workflows/capi.yml @@ -14,7 +14,7 @@ jobs: name: Build and test strategy: matrix: - os: [ubuntu-latest, macos-latest, windows-latest] + os: [ubuntu-latest, macos-latest] runs-on: ${{ matrix.os }} steps: - name: Checkout sources diff --git a/.github/workflows/pyapi.yml b/.github/workflows/pyapi.yml index 9045a2e8..eb231262 100644 --- a/.github/workflows/pyapi.yml +++ b/.github/workflows/pyapi.yml @@ -19,7 +19,7 @@ permissions: jobs: build-test: - name: Build and test + name: Build strategy: matrix: os: [ubuntu-latest, macos-latest, windows-latest] @@ -32,16 +32,16 @@ jobs: - uses: Swatinem/rust-cache@v2 with: shared-key: "build-test" - - name: Install latest nextest release - uses: taiki-e/install-action@nextest + # - name: Install latest nextest release + # uses: taiki-e/install-action@nextest - name: Cargo build run: cargo build -p rustsat-pyapi --verbose env: CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }} - - name: Run tests - run: cargo nextest run --profile ci -p rustsat-pyapi --verbose - env: - CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }} + # - name: Run tests + # run: cargo nextest run --profile ci -p rustsat-pyapi --verbose + # env: + # CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }} - name: Build Python package uses: PyO3/maturin-action@v1 with: diff --git a/capi/cbindgen.toml b/capi/cbindgen.toml index 055ffd41..4dedf806 100644 --- a/capi/cbindgen.toml +++ b/capi/cbindgen.toml @@ -50,7 +50,7 @@ cpp_compat = true [export] -include = ["DbTotalizer", "DynamicPolyWatchdog", "DbGte"] +include = ["DbTotalizer", "DynamicPolyWatchdog", "DbGte", "BinaryAdder"] exclude = [] # prefix = "CAPI_" item_types = [] diff --git a/capi/rustsat.h b/capi/rustsat.h index 52086cdf..f572c3a2 100644 --- a/capi/rustsat.h +++ b/capi/rustsat.h @@ -43,6 +43,19 @@ typedef enum MaybeError { PrecisionDecreased, } MaybeError; +/** + * Implementation of the binary adder encoding first described in \[1\]. + * The implementation follows the description in \[2\]. + * + * ## References + * + * - \[1\] Joose P. Warners: _A linear-time transformation of linear inequalities into conjunctive + * normal form_, Inf. Process. Lett. 1998. + * - \[2\] Niklas Eén and Niklas Sörensson: _Translating Pseudo-Boolean Constraints into SAT_, + * JSAT 2006. + */ +typedef struct BinaryAdder BinaryAdder; + /** * Implementation of the binary adder tree generalized totalizer encoding * \[1\]. The implementation is incremental. The implementation is recursive. @@ -97,6 +110,132 @@ typedef void (*CAssumpCollector)(int lit, void *data); extern "C" { #endif // __cplusplus +/** + * Adds a new input literal to a [`BinaryAdder`]. + * + * # Errors + * + * - If `lit` is not a valid IPASIR-style literal (e.g., `lit = 0`), + * [`MaybeError::InvalidLiteral`] is returned + * + * # Safety + * + * `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been + * called on. + */ +enum MaybeError bin_adder_add(struct BinaryAdder *adder, int lit, size_t weight); + +/** + * Frees the memory associated with a [`BinaryAdder`] + * + * # Safety + * + * `adder` must be a return value of [`bin_adder_new`] and cannot be used + * afterwards again. + */ +void bin_adder_drop(struct BinaryAdder *adder); + +/** + * Lazily builds the _change in_ pseudo-boolean encoding to enable lower bounds from within the + * range. + * + * The min and max bounds are inclusive. After a call to [`bin_adder_encode_lb`] with + * `min_bound=2` and `max_bound=4`, bounds satisfying `2 <= bound <= 4` can be enforced. + * + * Clauses are returned via the `collector`. The `collector` function should expect clauses to be + * passed similarly to `ipasir_add`, as a 0-terminated sequence of literals where the literals are + * passed as the first argument and the `collector_data` as a second. + * + * `n_vars_used` must be the number of variables already used and will be incremented by the + * number of variables used up in the encoding. + * + * # Safety + * + * `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been + * called on. + * + * # Panics + * + * If `min_bound > max_bound`. + */ +void bin_adder_encode_lb(struct BinaryAdder *adder, + size_t min_bound, + size_t max_bound, + uint32_t *n_vars_used, + CClauseCollector collector, + void *collector_data); + +/** + * Lazily builds the _change in_ pseudo-boolean encoding to enable upper bounds from within the + * range. + * + * The min and max bounds are inclusive. After a call to [`bin_adder_encode_ub`] with + * `min_bound=2` and `max_bound=4`, bounds satisfying `2 <= bound <= 4` can be enforced. + * + * Clauses are returned via the `collector`. The `collector` function should expect clauses to be + * passed similarly to `ipasir_add`, as a 0-terminated sequence of literals where the literals are + * passed as the first argument and the `collector_data` as a second. + * + * `n_vars_used` must be the number of variables already used and will be incremented by the + * number of variables used up in the encoding. + * + * # Safety + * + * `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been + * called on. + * + * # Panics + * + * If `min_bound > max_bound`. + */ +void bin_adder_encode_ub(struct BinaryAdder *adder, + size_t min_bound, + size_t max_bound, + uint32_t *n_vars_used, + CClauseCollector collector, + void *collector_data); + +/** + * Returns assumptions/units for enforcing an upper bound (`sum of lits >= lb`). Make sure that + * [`bin_adder_encode_lb`] has been called adequately and nothing has been called afterwards, + * otherwise [`MaybeError::NotEncoded`] will be returned. + * + * Assumptions are returned via the collector callback. There is _no_ terminating zero, all + * assumptions are passed when [`bin_adder_enforce_lb`] returns. + * + * # Safety + * + * `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been + * called on. + */ +enum MaybeError bin_adder_enforce_lb(struct BinaryAdder *adder, + size_t ub, + CAssumpCollector collector, + void *collector_data); + +/** + * Returns assumptions/units for enforcing an upper bound (`sum of lits <= ub`). Make sure that + * [`bin_adder_encode_ub`] has been called adequately and nothing has been called afterwards, + * otherwise [`MaybeError::NotEncoded`] will be returned. + * + * Assumptions are returned via the collector callback. There is _no_ terminating zero, all + * assumptions are passed when [`bin_adder_enforce_ub`] returns. + * + * # Safety + * + * `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been + * called on. + */ +enum MaybeError bin_adder_enforce_ub(struct BinaryAdder *adder, + size_t ub, + CAssumpCollector collector, + void *collector_data); + +/** + * Creates a new [`BinaryAdder`] cardinality encoding + */ +struct BinaryAdder *bin_adder_new(void); + /** * Adds a new input literal to a [`DynamicPolyWatchdog`]. * @@ -291,6 +430,10 @@ void gte_drop(struct DbGte *gte); * # Safety * * `gte` must be a return value of [`gte_new`] that [`gte_drop`] has not yet been called on. + * + * # Panics + * + * If `min_bound > max_bound`. */ void gte_encode_ub(struct DbGte *gte, size_t min_bound, @@ -364,7 +507,7 @@ void tot_drop(struct DbTotalizer *tot); * * # Panics * - * If `min_bound <= max_bound`. + * If `min_bound > max_bound`. */ void tot_encode_ub(struct DbTotalizer *tot, size_t min_bound, diff --git a/capi/src/encodings.rs b/capi/src/encodings.rs index c33a842a..b4522ae3 100644 --- a/capi/src/encodings.rs +++ b/capi/src/encodings.rs @@ -153,6 +153,7 @@ impl<'a> ManageVars for VarManager<'a> { } } +pub mod adder; pub mod dpw; pub mod gte; pub mod totalizer; diff --git a/capi/src/encodings/adder.rs b/capi/src/encodings/adder.rs new file mode 100644 index 00000000..1a181af6 --- /dev/null +++ b/capi/src/encodings/adder.rs @@ -0,0 +1,273 @@ +//! # Binary Adder C-API + +use std::ffi::{c_int, c_void}; + +use rustsat::{ + encodings::pb::{ + BinaryAdder, BoundLower, BoundLowerIncremental, BoundUpper, BoundUpperIncremental, + }, + types::Lit, +}; + +use super::{CAssumpCollector, CClauseCollector, ClauseCollector, MaybeError, VarManager}; + +/// Creates a new [`BinaryAdder`] cardinality encoding +#[no_mangle] +pub extern "C" fn bin_adder_new() -> *mut BinaryAdder { + Box::into_raw(Box::default()) +} + +/// Adds a new input literal to a [`BinaryAdder`]. +/// +/// # Errors +/// +/// - If `lit` is not a valid IPASIR-style literal (e.g., `lit = 0`), +/// [`MaybeError::InvalidLiteral`] is returned +/// +/// # Safety +/// +/// `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been +/// called on. +#[no_mangle] +pub unsafe extern "C" fn bin_adder_add( + adder: *mut BinaryAdder, + lit: c_int, + weight: usize, +) -> MaybeError { + let Ok(lit) = Lit::from_ipasir(lit) else { + return MaybeError::InvalidLiteral; + }; + unsafe { (*adder).extend([(lit, weight)]) }; + MaybeError::Ok +} + +/// Lazily builds the _change in_ pseudo-boolean encoding to enable upper bounds from within the +/// range. +/// +/// The min and max bounds are inclusive. After a call to [`bin_adder_encode_ub`] with +/// `min_bound=2` and `max_bound=4`, bounds satisfying `2 <= bound <= 4` can be enforced. +/// +/// Clauses are returned via the `collector`. The `collector` function should expect clauses to be +/// passed similarly to `ipasir_add`, as a 0-terminated sequence of literals where the literals are +/// passed as the first argument and the `collector_data` as a second. +/// +/// `n_vars_used` must be the number of variables already used and will be incremented by the +/// number of variables used up in the encoding. +/// +/// # Safety +/// +/// `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been +/// called on. +/// +/// # Panics +/// +/// If `min_bound > max_bound`. +#[no_mangle] +pub unsafe extern "C" fn bin_adder_encode_ub( + adder: *mut BinaryAdder, + min_bound: usize, + max_bound: usize, + n_vars_used: &mut u32, + collector: CClauseCollector, + collector_data: *mut c_void, +) { + assert!(min_bound <= max_bound); + let mut collector = ClauseCollector::new(collector, collector_data); + let mut var_manager = VarManager::new(n_vars_used); + unsafe { (*adder).encode_ub_change(min_bound..=max_bound, &mut collector, &mut var_manager) } + .expect("clause collector returned out of memory"); +} + +/// Returns assumptions/units for enforcing an upper bound (`sum of lits <= ub`). Make sure that +/// [`bin_adder_encode_ub`] has been called adequately and nothing has been called afterwards, +/// otherwise [`MaybeError::NotEncoded`] will be returned. +/// +/// Assumptions are returned via the collector callback. There is _no_ terminating zero, all +/// assumptions are passed when [`bin_adder_enforce_ub`] returns. +/// +/// # Safety +/// +/// `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been +/// called on. +#[no_mangle] +pub unsafe extern "C" fn bin_adder_enforce_ub( + adder: *mut BinaryAdder, + ub: usize, + collector: CAssumpCollector, + collector_data: *mut c_void, +) -> MaybeError { + match unsafe { (*adder).enforce_ub(ub) } { + Ok(assumps) => { + for l in assumps { + collector(l.to_ipasir(), collector_data); + } + MaybeError::Ok + } + Err(err) => err.into(), + } +} + +/// Lazily builds the _change in_ pseudo-boolean encoding to enable lower bounds from within the +/// range. +/// +/// The min and max bounds are inclusive. After a call to [`bin_adder_encode_lb`] with +/// `min_bound=2` and `max_bound=4`, bounds satisfying `2 <= bound <= 4` can be enforced. +/// +/// Clauses are returned via the `collector`. The `collector` function should expect clauses to be +/// passed similarly to `ipasir_add`, as a 0-terminated sequence of literals where the literals are +/// passed as the first argument and the `collector_data` as a second. +/// +/// `n_vars_used` must be the number of variables already used and will be incremented by the +/// number of variables used up in the encoding. +/// +/// # Safety +/// +/// `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been +/// called on. +/// +/// # Panics +/// +/// If `min_bound > max_bound`. +#[no_mangle] +pub unsafe extern "C" fn bin_adder_encode_lb( + adder: *mut BinaryAdder, + min_bound: usize, + max_bound: usize, + n_vars_used: &mut u32, + collector: CClauseCollector, + collector_data: *mut c_void, +) { + assert!(min_bound <= max_bound); + let mut collector = ClauseCollector::new(collector, collector_data); + let mut var_manager = VarManager::new(n_vars_used); + unsafe { (*adder).encode_lb_change(min_bound..=max_bound, &mut collector, &mut var_manager) } + .expect("clause collector returned out of memory"); +} + +/// Returns assumptions/units for enforcing an upper bound (`sum of lits >= lb`). Make sure that +/// [`bin_adder_encode_lb`] has been called adequately and nothing has been called afterwards, +/// otherwise [`MaybeError::NotEncoded`] will be returned. +/// +/// Assumptions are returned via the collector callback. There is _no_ terminating zero, all +/// assumptions are passed when [`bin_adder_enforce_lb`] returns. +/// +/// # Safety +/// +/// `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been +/// called on. +#[no_mangle] +pub unsafe extern "C" fn bin_adder_enforce_lb( + adder: *mut BinaryAdder, + ub: usize, + collector: CAssumpCollector, + collector_data: *mut c_void, +) -> MaybeError { + match unsafe { (*adder).enforce_lb(ub) } { + Ok(assumps) => { + for l in assumps { + collector(l.to_ipasir(), collector_data); + } + MaybeError::Ok + } + Err(err) => err.into(), + } +} + +/// Frees the memory associated with a [`BinaryAdder`] +/// +/// # Safety +/// +/// `adder` must be a return value of [`bin_adder_new`] and cannot be used +/// afterwards again. +#[no_mangle] +pub unsafe extern "C" fn bin_adder_drop(adder: *mut BinaryAdder) { + drop(unsafe { Box::from_raw(adder) }); +} + +// TODO: figure out how to get these to work on windows +#[cfg(all(test, not(target_os = "windows")))] +mod tests { + use inline_c::assert_c; + + #[test] + fn new_drop() { + (assert_c! { + #include + #include "rustsat.h" + + int main() { + BinaryAdder *adder = bin_adder_new(); + assert(adder != NULL); + bin_adder_drop(adder); + return 0; + } + }) + .success(); + } + + #[test] + fn basic_ub() { + (assert_c! { + #include + #include + #include "rustsat.h" + + void clause_counter(int lit, void *data) { + if (!lit) { + int *cnt = (int *)data; + (*cnt)++; + } + } + + int main() { + BinaryAdder *adder = bin_adder_new(); + assert(bin_adder_add(adder, 1, 1) == Ok); + assert(bin_adder_add(adder, 2, 2) == Ok); + assert(bin_adder_add(adder, 3, 3) == Ok); + assert(bin_adder_add(adder, 4, 4) == Ok); + uint32_t n_used = 4; + uint32_t n_clauses = 0; + bin_adder_encode_ub(adder, 0, 6, &n_used, &clause_counter, &n_clauses); + bin_adder_drop(adder); + printf("%d", n_used); + assert(n_used == 17); + assert(n_clauses == 32); + return 0; + } + }) + .success(); + } + + #[test] + fn basic_lb() { + (assert_c! { + #include + #include + #include "rustsat.h" + + void clause_counter(int lit, void *data) { + if (!lit) { + int *cnt = (int *)data; + (*cnt)++; + } + } + + int main() { + BinaryAdder *adder = bin_adder_new(); + assert(bin_adder_add(adder, 1, 1) == Ok); + assert(bin_adder_add(adder, 2, 2) == Ok); + assert(bin_adder_add(adder, 3, 3) == Ok); + assert(bin_adder_add(adder, 4, 4) == Ok); + uint32_t n_used = 4; + uint32_t n_clauses = 0; + bin_adder_encode_lb(adder, 0, 6, &n_used, &clause_counter, &n_clauses); + bin_adder_drop(adder); + printf("%d", n_used); + assert(n_used == 16); + assert(n_clauses == 27); + return 0; + } + }) + .success(); + } +} diff --git a/capi/src/encodings/gte.rs b/capi/src/encodings/gte.rs index e5713eb2..5951b5a6 100644 --- a/capi/src/encodings/gte.rs +++ b/capi/src/encodings/gte.rs @@ -50,6 +50,10 @@ pub unsafe extern "C" fn gte_add(gte: *mut DbGte, lit: c_int, weight: usize) -> /// # Safety /// /// `gte` must be a return value of [`gte_new`] that [`gte_drop`] has not yet been called on. +/// +/// # Panics +/// +/// If `min_bound > max_bound`. #[no_mangle] pub unsafe extern "C" fn gte_encode_ub( gte: *mut DbGte, diff --git a/capi/src/encodings/totalizer.rs b/capi/src/encodings/totalizer.rs index ffa63c2b..21588d0d 100644 --- a/capi/src/encodings/totalizer.rs +++ b/capi/src/encodings/totalizer.rs @@ -53,7 +53,7 @@ pub unsafe extern "C" fn tot_add(tot: *mut DbTotalizer, lit: c_int) -> MaybeErro /// /// # Panics /// -/// If `min_bound <= max_bound`. +/// If `min_bound > max_bound`. #[no_mangle] pub unsafe extern "C" fn tot_encode_ub( tot: *mut DbTotalizer, diff --git a/src/encodings/am1/bimander.rs b/src/encodings/am1/bimander.rs index 615adf5f..3a0c61dd 100644 --- a/src/encodings/am1/bimander.rs +++ b/src/encodings/am1/bimander.rs @@ -66,8 +66,8 @@ where for split in 0..n_splits { let lits = &self.in_lits[split * N..std::cmp::min(self.in_lits.len(), (split + 1) * N)]; - for k in 0..p as usize { - let aux = aux_vars[k].lit(split & (1 << k) == 0); + for (k, aux) in aux_vars.iter().enumerate().take(p as usize) { + let aux = aux.lit(split & (1 << k) == 0); collector.extend_clauses(atomics::clause_impl_lit(lits, aux))?; } let mut sub = lits.iter().copied().collect::(); diff --git a/src/encodings/pb.rs b/src/encodings/pb.rs index eec4d438..4458e62a 100644 --- a/src/encodings/pb.rs +++ b/src/encodings/pb.rs @@ -64,6 +64,9 @@ pub use dpw::DynamicPolyWatchdog; pub mod dbgte; pub use dbgte::DbGte; +pub mod adder; +pub use adder::BinaryAdder; + /// Trait for all pseudo-boolean encodings of form `weighted sum of lits <> rhs` pub trait Encode { /// Get the sum of weights in the encoding diff --git a/src/encodings/pb/adder.rs b/src/encodings/pb/adder.rs new file mode 100644 index 00000000..f113bc76 --- /dev/null +++ b/src/encodings/pb/adder.rs @@ -0,0 +1,1469 @@ +//! # Binary Adder Encoding +//! +//! Implementation of the binary adder encoding first described in \[1\]. +//! The implementation follows the description in \[2\]. +//! +//! **Note**: the CNF definition of the full adder in \[2\] is incorrect, but it is implemented +//! correctly here. +//! +//! ## References +//! +//! - \[1\] Joose P. Warners: _A linear-time transformation of linear inequalities into conjunctive +//! normal form_, Inf. Process. Lett. 1998. +//! - \[2\] Niklas Eén and Niklas Sörensson: _Translating Pseudo-Boolean Constraints into SAT_, +//! JSAT 2006. + +#![allow(clippy::module_name_repetitions)] + +use std::collections::VecDeque; + +use crate::{ + clause, + encodings::{CollectClauses, EncodeStats, Error}, + instances::ManageVars, + types::{Clause, Lit, RsHashMap}, + OutOfMemory, +}; + +use super::{ + BoundLower, BoundLowerIncremental, BoundUpper, BoundUpperIncremental, Encode, EncodeIncremental, +}; + +/// Implementation of the binary adder encoding first described in \[1\]. +/// The implementation follows the description in \[2\]. +/// +/// ## References +/// +/// - \[1\] Joose P. Warners: _A linear-time transformation of linear inequalities into conjunctive +/// normal form_, Inf. Process. Lett. 1998. +/// - \[2\] Niklas Eén and Niklas Sörensson: _Translating Pseudo-Boolean Constraints into SAT_, +/// JSAT 2006. +#[derive(Default, Debug)] +pub struct BinaryAdder { + /// Input literals and weights for the encoding + lit_buffer: RsHashMap, + /// The encoding structure + structure: Option, + /// Sum of all input weight + weight_sum: usize, + /// The number of variables + n_vars: u32, + /// The number of clauses + n_clauses: usize, + /// The node database of this encoding + nodes: Vec, +} + +/// The structure of a binary adder encoding +#[cfg_attr(feature = "internals", visibility::make(pub))] +#[cfg_attr(docsrs, doc(cfg(feature = "internals")))] +#[derive(Debug, Clone)] +struct Structure { + /// The output bits of the structure + outputs: Vec>, + /// Comparator structure for providing assumptions + comparator: Vec>, +} + +impl BinaryAdder { + fn extend_structure(&mut self) { + if self.lit_buffer.is_empty() { + return; + } + + let mut buckets = Vec::new(); + + // Add new input literals into buckets + for (lit, weight) in self.lit_buffer.drain() { + debug_assert_ne!(weight, 0); + self.weight_sum += weight; + let max_bucket = weight.next_power_of_two(); + if max_bucket >= buckets.len() { + buckets.resize_with(max_bucket + 1, || VecDeque::with_capacity(1)); + } + for (idx, bucket) in buckets.iter_mut().take(max_bucket + 1).enumerate() { + if weight & (1usize << idx) != 0 { + // NOTE: we push to the front here in order to get input literals into the + // structure first + bucket.push_back(Connection::Input(lit)); + } + } + } + + // Add existing structure into buckets + if let Some(structure) = &self.structure { + if buckets.len() < structure.outputs.len() { + buckets.resize_with(structure.outputs.len(), || VecDeque::with_capacity(1)); + } + for (bucket, &output) in buckets.iter_mut().zip(&structure.outputs) { + let Some(output) = output else { + continue; + }; + bucket.push_back(output); + } + } + + // Build the encoding + for idx in 0..buckets.len() { + if idx == buckets.len() - 1 && buckets[idx].len() >= 2 { + buckets.resize_with(buckets.len() + 1, || VecDeque::with_capacity(1)); + } + while buckets[idx].len() >= 3 { + let a = buckets[idx].pop_front().unwrap(); + let b = buckets[idx].pop_front().unwrap(); + let c = buckets[idx].pop_front().unwrap(); + + self.nodes.push(Node::full(a, b, c)); + + buckets[idx].push_back(Connection::Sum(self.nodes.len() - 1)); + buckets[idx + 1].push_back(Connection::Carry(self.nodes.len() - 1)); + } + if buckets[idx].len() == 2 { + let a = buckets[idx].pop_front().unwrap(); + let b = buckets[idx].pop_front().unwrap(); + + self.nodes.push(Node::half(a, b)); + + buckets[idx].push_back(Connection::Sum(self.nodes.len() - 1)); + buckets[idx + 1].push_back(Connection::Carry(self.nodes.len() - 1)); + } + } + + // Store the structure + self.structure = Some(Structure { + outputs: buckets + .into_iter() + .map(|mut q| { + debug_assert!(q.len() <= 1); + q.pop_front() + }) + .collect(), + comparator: Vec::new(), + }); + } +} + +impl Encode for BinaryAdder { + fn weight_sum(&self) -> usize { + self.lit_buffer + .iter() + .fold(self.weight_sum, |sum, (_, w)| sum + w) + } +} + +impl BoundUpper for BinaryAdder { + fn encode_ub( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + ) -> Result<(), OutOfMemory> + where + Col: CollectClauses, + R: std::ops::RangeBounds, + { + // reset previous encoding status + for node in &mut self.nodes { + if let Node::Full { sum: Some(out), .. } | Node::Half { sum: Some(out), .. } = node { + out.enc_if = false; + out.enc_only_if = false; + } + if let Node::Full { + carry: Some(out), .. + } + | Node::Half { + carry: Some(out), .. + } = node + { + out.enc_if = false; + out.enc_only_if = false; + } + } + self.encode_ub_change(range, collector, var_manager) + } + + fn enforce_ub(&self, ub: usize) -> Result, Error> { + if ub >= self.weight_sum() { + return Ok(vec![]); + } + let Some(structure) = &self.structure else { + return Err(Error::NotEncoded); + }; + let Some(Some(Output { + bit, enc_if: true, .. + })) = structure.comparator.get(ub) + else { + return Err(Error::NotEncoded); + }; + Ok(vec![!*bit]) + } +} + +impl BoundUpperIncremental for BinaryAdder { + fn encode_ub_change( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + ) -> Result<(), OutOfMemory> + where + Col: CollectClauses, + R: std::ops::RangeBounds, + { + let range = super::prepare_ub_range(self, range); + if range.is_empty() { + return Ok(()); + } + + let n_vars_before = var_manager.n_used(); + let n_clauses_before = collector.n_clauses(); + + self.extend_structure(); + if let Some(structure) = &mut self.structure { + // TODO: could maybe optimize some edge cases here where we are guaranteed to never use + // certain outputs of the adder + let mut outputs = Vec::with_capacity(structure.outputs.len()); + for con in &structure.outputs { + if let Some(con) = con { + outputs.push(Some(get_bit_if( + *con, + &mut self.nodes, + collector, + var_manager, + )?)); + } else { + outputs.push(None); + } + } + if structure.comparator.len() < range.end { + structure.comparator.resize(range.end, None); + } + for val in range { + let output = if let Some(output) = &mut structure.comparator[val] { + if output.enc_if { + continue; + } + output.enc_if = true; + output.bit + } else { + let bit = var_manager.new_lit(); + structure.comparator[val] = Some(Output { + bit, + enc_if: true, + enc_only_if: false, + }); + bit + }; + comparator_if(val, output, &outputs, collector)?; + } + } + + self.n_clauses += collector.n_clauses() - n_clauses_before; + self.n_vars += var_manager.n_used() - n_vars_before; + Ok(()) + } +} + +impl BoundLower for BinaryAdder { + fn encode_lb( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + ) -> Result<(), OutOfMemory> + where + Col: CollectClauses, + R: std::ops::RangeBounds, + { + // reset previous encoding status + for node in &mut self.nodes { + if let Node::Full { sum: Some(out), .. } | Node::Half { sum: Some(out), .. } = node { + out.enc_if = false; + out.enc_only_if = false; + } + if let Node::Full { + carry: Some(out), .. + } + | Node::Half { + carry: Some(out), .. + } = node + { + out.enc_if = false; + out.enc_only_if = false; + } + } + self.encode_lb_change(range, collector, var_manager) + } + + fn enforce_lb(&self, lb: usize) -> Result, Error> { + if lb > self.weight_sum() { + return Err(Error::Unsat); + } + if lb == 0 { + return Ok(vec![]); + } + let Some(structure) = &self.structure else { + return Err(Error::NotEncoded); + }; + let Some(Some(Output { + bit, + enc_only_if: true, + .. + })) = structure.comparator.get(lb - 1) + else { + return Err(Error::NotEncoded); + }; + Ok(vec![*bit]) + } +} + +impl BoundLowerIncremental for BinaryAdder { + fn encode_lb_change( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + ) -> Result<(), OutOfMemory> + where + Col: CollectClauses, + R: std::ops::RangeBounds, + { + let range = super::prepare_lb_range(self, range); + if range.is_empty() { + return Ok(()); + } + + let n_vars_before = var_manager.n_used(); + let n_clauses_before = collector.n_clauses(); + + self.extend_structure(); + if let Some(structure) = &mut self.structure { + // TODO: could maybe optimize some edge cases here where we are guaranteed to never use + // certain outputs of the adder + let mut outputs = Vec::with_capacity(structure.outputs.len()); + for con in &structure.outputs { + if let Some(con) = con { + outputs.push(Some(get_bit_only_if( + *con, + &mut self.nodes, + collector, + var_manager, + )?)); + } else { + outputs.push(None); + } + } + if structure.comparator.len() < range.end { + structure.comparator.resize(range.end, None); + } + for val in range { + let output = if let Some(output) = &mut structure.comparator[val - 1] { + if output.enc_if { + continue; + } + output.enc_only_if = true; + output.bit + } else { + let bit = var_manager.new_lit(); + structure.comparator[val - 1] = Some(Output { + bit, + enc_if: false, + enc_only_if: true, + }); + bit + }; + comparator_only_if(val - 1, output, &outputs, collector)?; + } + } + + self.n_clauses += collector.n_clauses() - n_clauses_before; + self.n_vars += var_manager.n_used() - n_vars_before; + Ok(()) + } +} + +impl EncodeIncremental for BinaryAdder { + fn reserve(&mut self, var_manager: &mut dyn ManageVars) { + self.extend_structure(); + + if let Some(structure) = &self.structure { + for &o in &structure.outputs { + if let Some(Connection::Sum(node) | Connection::Carry(node)) = o { + reserve(&mut self.nodes[..=node], var_manager); + } + } + } + } +} + +impl EncodeStats for BinaryAdder { + fn n_clauses(&self) -> usize { + self.n_clauses + } + + fn n_vars(&self) -> u32 { + self.n_vars + } +} + +impl From> for BinaryAdder { + fn from(lits: RsHashMap) -> Self { + Self { + lit_buffer: lits, + ..Default::default() + } + } +} + +impl FromIterator<(Lit, usize)> for BinaryAdder { + fn from_iter>(iter: T) -> Self { + let lits: RsHashMap = RsHashMap::from_iter(iter); + Self::from(lits) + } +} + +impl Extend<(Lit, usize)> for BinaryAdder { + fn extend>(&mut self, iter: T) { + iter.into_iter().for_each(|(l, w)| { + // Insert into buffer to be added to tree + match self.lit_buffer.get_mut(&l) { + Some(old_w) => *old_w += w, + None => { + self.lit_buffer.insert(l, w); + } + }; + }); + } +} + +#[derive(Debug, Clone, Copy)] +enum Node { + Full { + a: Connection, + b: Connection, + c: Connection, + sum: Option, + carry: Option, + }, + Half { + a: Connection, + b: Connection, + sum: Option, + carry: Option, + }, +} + +impl Node { + fn full(a: Connection, b: Connection, c: Connection) -> Self { + Node::Full { + a, + b, + c, + sum: None, + carry: None, + } + } + + fn half(a: Connection, b: Connection) -> Self { + Node::Half { + a, + b, + sum: None, + carry: None, + } + } + + fn reserve(&mut self, var_manager: &mut dyn ManageVars) { + match self { + Node::Full { sum, carry, .. } | Node::Half { sum, carry, .. } => { + if sum.is_none() { + *sum = Some(Output { + bit: var_manager.new_lit(), + enc_if: false, + enc_only_if: false, + }); + } + if carry.is_none() { + *carry = Some(Output { + bit: var_manager.new_lit(), + enc_if: false, + enc_only_if: false, + }); + } + } + } + } +} + +#[derive(Debug, Clone, Copy)] +enum Connection { + Input(Lit), + Sum(usize), + Carry(usize), +} + +#[derive(Debug, Clone, Copy)] +struct Output { + bit: Lit, + enc_if: bool, + enc_only_if: bool, +} + +#[inline] +fn get_bit_if( + con: Connection, + nodes: &mut [Node], + collector: &mut Col, + var_manager: &mut dyn ManageVars, +) -> Result +where + Col: CollectClauses, +{ + match con { + Connection::Input(bit) => Ok(bit), + Connection::Sum(node) => { + let nodes = &mut nodes[..=node]; + sum_if(nodes, collector, var_manager) + } + Connection::Carry(node) => { + let nodes = &mut nodes[..=node]; + carry_if(nodes, collector, var_manager) + } + } +} + +#[inline] +fn get_bit_only_if( + con: Connection, + nodes: &mut [Node], + collector: &mut Col, + var_manager: &mut dyn ManageVars, +) -> Result +where + Col: CollectClauses, +{ + match con { + Connection::Input(bit) => Ok(bit), + Connection::Sum(node) => { + let nodes = &mut nodes[..=node]; + sum_only_if(nodes, collector, var_manager) + } + Connection::Carry(node) => { + let nodes = &mut nodes[..=node]; + carry_only_if(nodes, collector, var_manager) + } + } +} + +/// Encodes the if direction of the sum bit for the last node in `nodes` recursively +fn sum_if( + nodes: &mut [Node], + collector: &mut Col, + var_manager: &mut dyn ManageVars, +) -> Result +where + Col: CollectClauses, +{ + let (nodes, node) = nodes.split_at_mut(nodes.len() - 1); + let node = &mut node[0]; + + match node { + Node::Full { a, b, c, sum, .. } => { + let sum = if let Some(sum) = sum { + if sum.enc_if { + return Ok(sum.bit); + } + sum.enc_if = true; + sum.bit + } else { + let bit = var_manager.new_lit(); + *sum = Some(Output { + bit, + enc_if: true, + enc_only_if: false, + }); + bit + }; + + let a = get_bit_if(*a, nodes, collector, var_manager)?; + let b = get_bit_if(*b, nodes, collector, var_manager)?; + let c = get_bit_if(*c, nodes, collector, var_manager)?; + + collector.add_clause(clause![!a, !b, !c, sum])?; + collector.add_clause(clause![!a, b, c, sum])?; + collector.add_clause(clause![a, !b, c, sum])?; + collector.add_clause(clause![a, b, !c, sum])?; + + Ok(sum) + } + Node::Half { a, b, sum, .. } => { + let sum = if let Some(sum) = sum { + if sum.enc_if { + return Ok(sum.bit); + } + sum.enc_if = true; + sum.bit + } else { + let bit = var_manager.new_lit(); + *sum = Some(Output { + bit, + enc_if: true, + enc_only_if: false, + }); + bit + }; + + let a = get_bit_if(*a, nodes, collector, var_manager)?; + let b = get_bit_if(*b, nodes, collector, var_manager)?; + + collector.add_clause(clause![!a, b, sum])?; + collector.add_clause(clause![a, !b, sum])?; + + Ok(sum) + } + } +} + +/// Encodes the only-if direction of the sum bit for the last node in `nodes` recursively +fn sum_only_if( + nodes: &mut [Node], + collector: &mut Col, + var_manager: &mut dyn ManageVars, +) -> Result +where + Col: CollectClauses, +{ + let (nodes, node) = nodes.split_at_mut(nodes.len() - 1); + let node = &mut node[0]; + + match node { + Node::Full { a, b, c, sum, .. } => { + let sum = if let Some(sum) = sum { + if sum.enc_only_if { + return Ok(sum.bit); + } + sum.enc_only_if = true; + sum.bit + } else { + let bit = var_manager.new_lit(); + *sum = Some(Output { + bit, + enc_if: false, + enc_only_if: true, + }); + bit + }; + + let a = get_bit_only_if(*a, nodes, collector, var_manager)?; + let b = get_bit_only_if(*b, nodes, collector, var_manager)?; + let c = get_bit_only_if(*c, nodes, collector, var_manager)?; + + collector.add_clause(clause![a, b, c, !sum])?; + collector.add_clause(clause![a, !b, !c, !sum])?; + collector.add_clause(clause![!a, b, !c, !sum])?; + collector.add_clause(clause![!a, !b, c, !sum])?; + + Ok(sum) + } + Node::Half { a, b, sum, .. } => { + let sum = if let Some(sum) = sum { + if sum.enc_only_if { + return Ok(sum.bit); + } + sum.enc_only_if = true; + sum.bit + } else { + let bit = var_manager.new_lit(); + *sum = Some(Output { + bit, + enc_if: false, + enc_only_if: true, + }); + bit + }; + + let a = get_bit_only_if(*a, nodes, collector, var_manager)?; + let b = get_bit_only_if(*b, nodes, collector, var_manager)?; + + collector.add_clause(clause![a, b, !sum])?; + collector.add_clause(clause![!a, !b, !sum])?; + + Ok(sum) + } + } +} + +/// Encodes the if direction of the carry bit for the last node in `nodes` recursively +fn carry_if( + nodes: &mut [Node], + collector: &mut Col, + var_manager: &mut dyn ManageVars, +) -> Result +where + Col: CollectClauses, +{ + let (nodes, node) = nodes.split_at_mut(nodes.len() - 1); + let node = &mut node[0]; + + match node { + Node::Full { a, b, c, carry, .. } => { + let carry = if let Some(carry) = carry { + if carry.enc_if { + return Ok(carry.bit); + } + carry.enc_if = true; + carry.bit + } else { + let bit = var_manager.new_lit(); + *carry = Some(Output { + bit, + enc_if: true, + enc_only_if: false, + }); + bit + }; + + let a = get_bit_if(*a, nodes, collector, var_manager)?; + let b = get_bit_if(*b, nodes, collector, var_manager)?; + let c = get_bit_if(*c, nodes, collector, var_manager)?; + + collector.add_clause(clause![!b, !c, carry])?; + collector.add_clause(clause![!a, !c, carry])?; + collector.add_clause(clause![!a, !b, carry])?; + + Ok(carry) + } + Node::Half { a, b, carry, .. } => { + let carry = if let Some(carry) = carry { + if carry.enc_if { + return Ok(carry.bit); + } + carry.enc_if = true; + carry.bit + } else { + let bit = var_manager.new_lit(); + *carry = Some(Output { + bit, + enc_if: true, + enc_only_if: false, + }); + bit + }; + + let a = get_bit_if(*a, nodes, collector, var_manager)?; + let b = get_bit_if(*b, nodes, collector, var_manager)?; + + collector.add_clause(clause![!a, !b, carry])?; + + Ok(carry) + } + } +} + +/// Encodes the only-if direction of the carry bit for the last node in `nodes` recursively +fn carry_only_if( + nodes: &mut [Node], + collector: &mut Col, + var_manager: &mut dyn ManageVars, +) -> Result +where + Col: CollectClauses, +{ + let (nodes, node) = nodes.split_at_mut(nodes.len() - 1); + let node = &mut node[0]; + + match node { + Node::Full { a, b, c, carry, .. } => { + let carry = if let Some(carry) = carry { + if carry.enc_only_if { + return Ok(carry.bit); + } + carry.enc_only_if = true; + carry.bit + } else { + let bit = var_manager.new_lit(); + *carry = Some(Output { + bit, + enc_if: false, + enc_only_if: true, + }); + bit + }; + + let a = get_bit_if(*a, nodes, collector, var_manager)?; + let b = get_bit_if(*b, nodes, collector, var_manager)?; + let c = get_bit_if(*c, nodes, collector, var_manager)?; + + collector.add_clause(clause![b, c, !carry])?; + collector.add_clause(clause![a, c, !carry])?; + collector.add_clause(clause![a, b, !carry])?; + + Ok(carry) + } + Node::Half { a, b, carry, .. } => { + let carry = if let Some(carry) = carry { + if carry.enc_only_if { + return Ok(carry.bit); + } + carry.enc_if = true; + carry.bit + } else { + let bit = var_manager.new_lit(); + *carry = Some(Output { + bit, + enc_if: true, + enc_only_if: false, + }); + bit + }; + + let a = get_bit_if(*a, nodes, collector, var_manager)?; + let b = get_bit_if(*b, nodes, collector, var_manager)?; + + collector.add_clause(clause![a, !carry])?; + collector.add_clause(clause![b, !carry])?; + + Ok(carry) + } + } +} + +/// Reserves the variables for the last node in `nodes` recursively +fn reserve(nodes: &mut [Node], var_manager: &mut dyn ManageVars) { + let (nodes, node) = nodes.split_at_mut(nodes.len()); + + let node = &mut node[0]; + node.reserve(var_manager); + + let mut recurse = |con: Connection| match con { + Connection::Input(_) => {} + Connection::Sum(node) | Connection::Carry(node) => { + reserve(&mut nodes[..=node], var_manager); + } + }; + + match node { + Node::Full { a, b, c, .. } => { + recurse(*a); + recurse(*b); + recurse(*c); + } + Node::Half { a, b, .. } => { + recurse(*a); + recurse(*b); + } + } +} + +fn comparator_if( + rhs: usize, + output: Lit, + lhs: &[Option], + collector: &mut Col, +) -> Result<(), OutOfMemory> +where + Col: CollectClauses, +{ + debug_assert!(rhs < (1usize << lhs.len())); + + let y = |idx: usize| -> bool { rhs & (1usize << idx) != 0 }; + + let comp_clause = |i: usize| -> Option { + if y(i) { + return None; + } + + let mut cl = clause![]; + + let lhs_i = lhs[i]?; + cl.add(!lhs_i); + + #[allow(clippy::needless_range_loop)] + for j in i + 1..lhs.len() { + if y(j) { + let lhs_j = lhs[j]?; + cl.add(!lhs_j); + } else if let Some(lhs_j) = lhs[j] { + cl.add(lhs_j); + } + } + + cl.add(output); + + Some(cl) + }; + + collector.extend_clauses((0..lhs.len()).filter_map(comp_clause)) +} + +fn comparator_only_if( + rhs: usize, + output: Lit, + lhs: &[Option], + collector: &mut Col, +) -> Result<(), OutOfMemory> +where + Col: CollectClauses, +{ + debug_assert!(rhs < (1usize << lhs.len())); + + if rhs == (1usize << lhs.len()) - 1 { + return collector.add_clause(clause![!output]); + } + + let rhs = rhs + 1; + + let y = |idx: usize| -> bool { rhs & (1usize << idx) != 0 }; + + let comp_clause = |i: usize| -> Option { + if !y(i) { + return None; + } + + let mut cl = clause![]; + + if let Some(lhs_i) = lhs[i] { + cl.add(lhs_i); + } + + #[allow(clippy::needless_range_loop)] + for j in i + 1..lhs.len() { + if y(j) { + let lhs_j = lhs[j]?; + cl.add(!lhs_j); + } else if let Some(lhs_j) = lhs[j] { + cl.add(lhs_j); + } + } + + cl.add(!output); + + Some(cl) + }; + + collector.extend_clauses((0..lhs.len()).filter_map(comp_clause)) +} + +#[cfg(test)] +mod tests { + use crate::{ + encodings::pb::{BoundLower, BoundUpper}, + instances::{BasicVarManager, Cnf, ManageVars}, + lit, + types::{Assignment, Lit, TernaryVal}, + var, + }; + + const N: u32 = 4; + + const ALL_LITS: [Option; N as usize] = + [Some(lit![0]), Some(lit![1]), Some(lit![2]), Some(lit![3])]; + const SOME_LITS: [Option; N as usize] = + [Some(lit![0]), None, Some(lit![2]), Some(lit![3])]; + const LESS_LITS: [Option; N as usize] = [Some(lit![0]), None, None, Some(lit![3])]; + + fn make_assignment(val: usize) -> Assignment { + let mut assign = Assignment::default(); + for idx in 0..=N { + assign.assign_var(var![idx], TernaryVal::from(val & (1usize << idx) != 0)); + } + assign + } + + fn value(lits: &[Option], assign: &Assignment) -> usize { + let mut val = 0; + for (idx, lit) in lits.iter().enumerate() { + if lit.is_some_and(|lit| assign.lit_value(lit) == TernaryVal::True) { + val += 1usize << idx; + } + } + val + } + + fn comparator_if(output: Lit, lits: &[Option]) { + for rhs in 0..(1usize << N) { + let mut cnf = Cnf::new(); + super::comparator_if(rhs, output, lits, &mut cnf).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << (N + 1)) { + let assign = make_assignment(assign); + let lhs = value(lits, &assign); + dbg!(lhs, rhs, assign.lit_value(output)); + if assign.lit_value(output) == TernaryVal::True || lhs <= rhs { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } + } + } + } + + #[test] + fn comparator_if_all() { + let output = lit![N]; + comparator_if(output, &ALL_LITS); + } + + #[test] + fn comparator_if_some() { + let output = lit![N]; + comparator_if(output, &SOME_LITS); + } + + #[test] + fn comparator_if_less() { + let output = lit![N]; + comparator_if(output, &LESS_LITS); + } + + fn comparator_only_if(output: Lit, lits: &[Option]) { + for rhs in 0..(1usize << N) { + let mut cnf = Cnf::new(); + super::comparator_only_if(rhs, output, lits, &mut cnf).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << (N + 1)) { + let assign = make_assignment(assign); + let lhs = value(lits, &assign); + dbg!(lhs, rhs, assign.lit_value(output)); + if assign.lit_value(output) == TernaryVal::False || lhs > rhs { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } + } + } + } + + #[test] + fn comparator_only_if_all() { + let output = lit![N]; + comparator_only_if(output, &ALL_LITS); + } + + #[test] + fn comparator_only_if_some() { + let output = lit![N]; + comparator_only_if(output, &SOME_LITS); + } + + #[test] + fn comparator_only_if_less() { + let output = lit![N]; + comparator_only_if(output, &LESS_LITS); + } + + fn comparator_if_and_only_if(output: Lit, lits: &[Option]) { + for rhs in 0..(1usize << N) { + let mut cnf = Cnf::new(); + super::comparator_if(rhs, output, lits, &mut cnf).unwrap(); + super::comparator_only_if(rhs, output, lits, &mut cnf).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << (N + 1)) { + let assign = make_assignment(assign); + let lhs = value(lits, &assign); + dbg!(lhs, rhs, assign.lit_value(output)); + if lhs <= rhs { + assert_eq!(cnf.evaluate(&assign), !assign.lit_value(output)); + } else { + assert_eq!(cnf.evaluate(&assign), assign.lit_value(output)); + } + } + } + } + + #[test] + fn comparator_if_and_only_if_all() { + let output = lit![N]; + comparator_if_and_only_if(output, &ALL_LITS); + } + + #[test] + fn comparator_if_and_only_if_some() { + let output = lit![N]; + comparator_if_and_only_if(output, &SOME_LITS); + } + + #[test] + fn comparator_if_and_only_if_less() { + let output = lit![N]; + comparator_if_and_only_if(output, &LESS_LITS); + } + + #[test] + fn full_adder_sum_if() { + let mut nodes = vec![super::Node::Full { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + c: super::Connection::Input(lit![2]), + sum: Some(super::Output { + bit: lit![3], + enc_if: false, + enc_only_if: false, + }), + carry: None, + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![4]); + super::sum_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 4) { + let val = (assign & 0b111).count_ones(); + dbg!(val); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![3]) == TernaryVal::False) && ((val & 0b1) != 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } + } + } + + #[test] + fn full_adder_sum_only_if() { + let mut nodes = vec![super::Node::Full { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + c: super::Connection::Input(lit![2]), + sum: Some(super::Output { + bit: lit![3], + enc_if: false, + enc_only_if: false, + }), + carry: None, + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![4]); + super::sum_only_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 4) { + let val = (assign & 0b111).count_ones(); + dbg!(val); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![3]) == TernaryVal::True) && ((val & 0b1) == 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } + } + } + + #[test] + fn full_adder_sum_if_and_only_if() { + let mut nodes = vec![super::Node::Full { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + c: super::Connection::Input(lit![2]), + sum: Some(super::Output { + bit: lit![3], + enc_if: false, + enc_only_if: false, + }), + carry: None, + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![4]); + super::sum_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + super::sum_only_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 4) { + let val = (assign & 0b111).count_ones(); + dbg!(val); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![3]) == TernaryVal::True) == ((val & 0b1) != 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } + } + } + + #[test] + fn full_adder_carry_if() { + let mut nodes = vec![super::Node::Full { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + c: super::Connection::Input(lit![2]), + sum: None, + carry: Some(super::Output { + bit: lit![3], + enc_if: false, + enc_only_if: false, + }), + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![4]); + super::carry_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 4) { + let val = (assign & 0b111).count_ones(); + dbg!(val); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![3]) == TernaryVal::False) && ((val & 0b10) != 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } + } + } + + #[test] + fn full_adder_carry_only_if() { + let mut nodes = vec![super::Node::Full { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + c: super::Connection::Input(lit![2]), + sum: None, + carry: Some(super::Output { + bit: lit![3], + enc_if: false, + enc_only_if: false, + }), + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![4]); + super::carry_only_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 4) { + let val = (assign & 0b111).count_ones(); + dbg!(val); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![3]) == TernaryVal::True) && ((val & 0b10) == 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } + } + } + + #[test] + fn full_adder_carry_if_and_only_if() { + let mut nodes = vec![super::Node::Full { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + c: super::Connection::Input(lit![2]), + sum: None, + carry: Some(super::Output { + bit: lit![3], + enc_if: false, + enc_only_if: false, + }), + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![4]); + super::carry_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + super::carry_only_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 4) { + let val = (assign & 0b111).count_ones(); + dbg!(val); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![3]) == TernaryVal::True) == ((val & 0b10) != 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } + } + } + + #[test] + fn half_adder_sum_if() { + let mut nodes = vec![super::Node::Half { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + sum: Some(super::Output { + bit: lit![2], + enc_if: false, + enc_only_if: false, + }), + carry: None, + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![3]); + super::sum_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 3) { + let val = (assign & 0b11).count_ones(); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![2]) == TernaryVal::False) && ((val & 0b1) != 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } + } + } + + #[test] + fn half_adder_sum_only_if() { + let mut nodes = vec![super::Node::Half { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + sum: Some(super::Output { + bit: lit![2], + enc_if: false, + enc_only_if: false, + }), + carry: None, + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![3]); + super::sum_only_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 3) { + let val = (assign & 0b11).count_ones(); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![2]) == TernaryVal::True) && ((val & 0b1) == 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } + } + } + + #[test] + fn half_adder_sum_if_and_only_if() { + let mut nodes = vec![super::Node::Half { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + sum: Some(super::Output { + bit: lit![2], + enc_if: false, + enc_only_if: false, + }), + carry: None, + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![3]); + super::sum_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + super::sum_only_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 3) { + let val = (assign & 0b11).count_ones(); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![2]) == TernaryVal::True) == ((val & 0b1) != 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } + } + } + + #[test] + fn half_adder_carry_if() { + let mut nodes = vec![super::Node::Half { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + sum: None, + carry: Some(super::Output { + bit: lit![2], + enc_if: false, + enc_only_if: false, + }), + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![3]); + super::carry_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 3) { + let val = (assign & 0b11).count_ones(); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![2]) == TernaryVal::False) && ((val & 0b10) != 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } + } + } + + #[test] + fn half_adder_carry_only_if() { + let mut nodes = vec![super::Node::Half { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + sum: None, + carry: Some(super::Output { + bit: lit![2], + enc_if: false, + enc_only_if: false, + }), + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![3]); + super::carry_only_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 3) { + let val = (assign & 0b11).count_ones(); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![2]) == TernaryVal::True) && ((val & 0b10) == 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } + } + } + + #[test] + fn half_adder_carry_if_and_only_if() { + let mut nodes = vec![super::Node::Half { + a: super::Connection::Input(lit![0]), + b: super::Connection::Input(lit![1]), + sum: None, + carry: Some(super::Output { + bit: lit![2], + enc_if: false, + enc_only_if: false, + }), + }]; + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![3]); + super::carry_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + super::carry_only_if(&mut nodes, &mut cnf, &mut vm).unwrap(); + dbg!(&cnf); + for assign in 0..(1usize << 3) { + let val = (assign & 0b11).count_ones(); + let assign = make_assignment(assign); + dbg!(&assign); + if (assign.lit_value(lit![2]) == TernaryVal::True) == ((val & 0b10) != 0) { + assert_eq!(cnf.evaluate(&assign), TernaryVal::True); + } else { + assert_eq!(cnf.evaluate(&assign), TernaryVal::False); + } + } + } + + #[test] + fn basic_ub() { + let mut adder: super::BinaryAdder = + [(lit![0], 1), (lit![1], 2), (lit![2], 3), (lit![3], 4)] + .into_iter() + .collect(); + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![4]); + adder.encode_ub(0..=6, &mut cnf, &mut vm).unwrap(); + assert_eq!(vm.n_used(), 17); + assert_eq!(cnf.len(), 32); + } + + #[test] + fn basic_lb() { + let mut adder: super::BinaryAdder = + [(lit![0], 1), (lit![1], 2), (lit![2], 3), (lit![3], 4)] + .into_iter() + .collect(); + let mut cnf = Cnf::new(); + let mut vm = BasicVarManager::from_next_free(var![4]); + adder.encode_lb(0..=6, &mut cnf, &mut vm).unwrap(); + assert_eq!(vm.n_used(), 16); + assert_eq!(cnf.len(), 27); + } +} diff --git a/src/solvers.rs b/src/solvers.rs index ae91b094..bcaef193 100644 --- a/src/solvers.rs +++ b/src/solvers.rs @@ -44,12 +44,12 @@ //! ### Minisat //! //! [Minisat](https://github.com/niklasso/minisat) is an incremental SAT solver -//! by Niklas Een and Niklas Sörensson. It is available through the +//! by Niklas Eén and Niklas Sörensson. It is available through the //! [`rustsat-minisat`](https://crates.io/crates/rustsat-minisat) crate. //! //! #### References //! -//! - Niklas Een and Niklas Sörensson (2003): _An Extensible SAT-solver_, SAT +//! - Niklas Eén and Niklas Sörensson (2003): _An Extensible SAT-solver_, SAT //! 2003. //! - Repository: //! [`https://github.com/niklasso/minisat`](https://github.com/niklasso/minisat) diff --git a/src/types.rs b/src/types.rs index 478eb7b9..810ab766 100644 --- a/src/types.rs +++ b/src/types.rs @@ -59,7 +59,7 @@ impl Var { /// /// If `idx > Var::MAX_IDX`. #[must_use] - pub fn new(idx: u32) -> Var { + pub const fn new(idx: u32) -> Var { assert!(idx <= Var::MAX_IDX, "variable index too high"); Var { idx } } @@ -87,7 +87,7 @@ impl Var { /// `idx` must be guaranteed to be not higher than `Var::MAX_IDX` #[inline] #[must_use] - pub unsafe fn new_unchecked(idx: u32) -> Var { + pub const unsafe fn new_unchecked(idx: u32) -> Var { debug_assert!(idx <= Var::MAX_IDX); Var { idx } } @@ -104,7 +104,7 @@ impl Var { /// ``` #[inline] #[must_use] - pub fn lit(self, negated: bool) -> Lit { + pub const fn lit(self, negated: bool) -> Lit { unsafe { Lit::new_unchecked(self.idx, negated) } } @@ -120,7 +120,7 @@ impl Var { /// ``` #[inline] #[must_use] - pub fn pos_lit(self) -> Lit { + pub const fn pos_lit(self) -> Lit { unsafe { Lit::positive_unchecked(self.idx) } } @@ -136,7 +136,7 @@ impl Var { /// ``` #[inline] #[must_use] - pub fn neg_lit(self) -> Lit { + pub const fn neg_lit(self) -> Lit { unsafe { Lit::negative_unchecked(self.idx) } } @@ -301,8 +301,8 @@ pub struct Lit { impl Lit { /// Represents a literal in memory #[inline] - fn represent(idx: u32, negated: bool) -> u32 { - (idx << 1) + u32::from(negated) + const fn represent(idx: u32, negated: bool) -> u32 { + (idx << 1) + if negated { 1 } else { 0 } } /// Creates a new (negated or not) literal with a given index. @@ -311,7 +311,7 @@ impl Lit { /// /// If `idx > Var::MAX_IDX`. #[must_use] - pub fn new(idx: u32, negated: bool) -> Lit { + pub const fn new(idx: u32, negated: bool) -> Lit { assert!(idx < Var::MAX_IDX, "variable index too high"); Lit { lidx: Lit::represent(idx, negated), @@ -340,7 +340,7 @@ impl Lit { /// /// `idx` must be guaranteed to be not higher than `Var::MAX_IDX` #[must_use] - pub unsafe fn new_unchecked(idx: u32, negated: bool) -> Lit { + pub const unsafe fn new_unchecked(idx: u32, negated: bool) -> Lit { debug_assert!(idx <= Var::MAX_IDX); Lit { lidx: Lit::represent(idx, negated), @@ -351,7 +351,7 @@ impl Lit { /// Panics if `idx > Var::MAX_IDX`. #[inline] #[must_use] - pub fn positive(idx: u32) -> Lit { + pub const fn positive(idx: u32) -> Lit { Lit::new(idx, false) } @@ -359,7 +359,7 @@ impl Lit { /// Panics if `idx > Var::MAX_IDX`. #[inline] #[must_use] - pub fn negative(idx: u32) -> Lit { + pub const fn negative(idx: u32) -> Lit { Lit::new(idx, true) } @@ -392,7 +392,7 @@ impl Lit { /// `idx` must be guaranteed to be not higher than `Var::MAX_IDX` #[inline] #[must_use] - pub unsafe fn positive_unchecked(idx: u32) -> Lit { + pub const unsafe fn positive_unchecked(idx: u32) -> Lit { Lit::new_unchecked(idx, false) } @@ -405,7 +405,7 @@ impl Lit { /// `idx` must be guaranteed to be not higher than `Var::MAX_IDX` #[inline] #[must_use] - pub unsafe fn negative_unchecked(idx: u32) -> Lit { + pub const unsafe fn negative_unchecked(idx: u32) -> Lit { Lit::new_unchecked(idx, true) } @@ -706,6 +706,20 @@ impl ops::Neg for TernaryVal { } } +#[cfg(kani)] +impl kani::Arbitrary for TernaryVal { + fn any() -> Self { + let val: u8 = kani::any(); + kani::assume(val < 3); + match val { + 0 => TernaryVal::False, + 1 => TernaryVal::True, + 2 => TernaryVal::DontCare, + _ => panic!(), + } + } +} + /// Possible errors in parsing a SAT solver value (`v`) line #[derive(Error, Debug)] pub enum InvalidVLine { diff --git a/src/types/constraints.rs b/src/types/constraints.rs index 2cf9983f..fe1a9aa6 100644 --- a/src/types/constraints.rs +++ b/src/types/constraints.rs @@ -311,6 +311,9 @@ impl fmt::Debug for Clause { /// Creates a clause from a list of literals #[macro_export] macro_rules! clause { + () => { + $crate::types::Clause::new() + }; ( $($l:expr),* ) => { { let mut tmp_clause = $crate::types::Clause::new(); diff --git a/tests/pb_encodings.rs b/tests/pb_encodings.rs index 58eb10e9..63284531 100644 --- a/tests/pb_encodings.rs +++ b/tests/pb_encodings.rs @@ -3,7 +3,7 @@ use rustsat::{ encodings::{ card::Totalizer, pb::{ - simulators::Card, BoundBoth, BoundBothIncremental, BoundLower, BoundUpper, + simulators::Card, BinaryAdder, BoundBoth, BoundBothIncremental, BoundLower, BoundUpper, BoundUpperIncremental, DbGte, DoubleGeneralizedTotalizer, DynamicPolyWatchdog, GeneralizedTotalizer, InvertedGeneralizedTotalizer, }, @@ -49,37 +49,37 @@ fn test_inc_pb_ub + Default>() let mut enc = PBE::default(); enc.extend(lits); - enc.encode_ub(0..3, &mut solver, &mut var_manager).unwrap(); + enc.encode_ub(0..=2, &mut solver, &mut var_manager).unwrap(); let assumps = enc.enforce_ub(2).unwrap(); - let res = solver.solve_assumps(&assumps).unwrap(); + let res = solver.solve_assumps(dbg!(&assumps)).unwrap(); assert_eq!(res, SolverResult::Unsat); - enc.encode_ub_change(0..5, &mut solver, &mut var_manager) + enc.encode_ub_change(0..=4, &mut solver, &mut var_manager) .unwrap(); let assumps = enc.enforce_ub(4).unwrap(); - let res = solver.solve_assumps(&assumps).unwrap(); + let res = solver.solve_assumps(dbg!(&assumps)).unwrap(); assert_eq!(res, SolverResult::Unsat); - enc.encode_ub_change(0..6, &mut solver, &mut var_manager) + enc.encode_ub_change(0..=5, &mut solver, &mut var_manager) .unwrap(); let assumps = enc.enforce_ub(5).unwrap(); - let res = solver.solve_assumps(&assumps).unwrap(); + let res = solver.solve_assumps(dbg!(&assumps)).unwrap(); assert_eq!(res, SolverResult::Sat); let mut lits = RsHashMap::default(); lits.insert(lit![5], 4); enc.extend(lits); - enc.encode_ub_change(0..6, &mut solver, &mut var_manager) + enc.encode_ub_change(0..=5, &mut solver, &mut var_manager) .unwrap(); let assumps = enc.enforce_ub(5).unwrap(); - let res = solver.solve_assumps(&assumps).unwrap(); + let res = solver.solve_assumps(dbg!(&assumps)).unwrap(); assert_eq!(res, SolverResult::Unsat); - enc.encode_ub_change(0..10, &mut solver, &mut var_manager) + enc.encode_ub_change(0..=9, &mut solver, &mut var_manager) .unwrap(); let assumps = enc.enforce_ub(9).unwrap(); - let res = solver.solve_assumps(&assumps).unwrap(); + let res = solver.solve_assumps(dbg!(&assumps)).unwrap(); assert_eq!(res, SolverResult::Sat); let mut lits = RsHashMap::default(); @@ -90,16 +90,16 @@ fn test_inc_pb_ub + Default>() lits.insert(lit![10], 2); enc.extend(lits); - enc.encode_ub_change(0..10, &mut solver, &mut var_manager) + enc.encode_ub_change(0..=9, &mut solver, &mut var_manager) .unwrap(); let assumps = enc.enforce_ub(9).unwrap(); - let res = solver.solve_assumps(&assumps).unwrap(); + let res = solver.solve_assumps(dbg!(&assumps)).unwrap(); assert_eq!(res, SolverResult::Unsat); - enc.encode_ub_change(0..15, &mut solver, &mut var_manager) + enc.encode_ub_change(0..=14, &mut solver, &mut var_manager) .unwrap(); let assumps = enc.enforce_ub(14).unwrap(); - let res = solver.solve_assumps(&assumps).unwrap(); + let res = solver.solve_assumps(dbg!(&assumps)).unwrap(); assert_eq!(res, SolverResult::Sat); } @@ -115,7 +115,7 @@ fn test_pb_eq>>() { lits.insert(lit![2], 2); let mut enc = PBE::from(lits); - enc.encode_both(4..5, &mut solver, &mut var_manager) + enc.encode_both(4..=4, &mut solver, &mut var_manager) .unwrap(); let mut assumps = enc.enforce_eq(4).unwrap(); @@ -177,14 +177,15 @@ fn test_pb_lb>>() { lits.insert(lit![2], 3); let mut enc = PBE::from(lits); - enc.encode_lb(0..11, &mut solver, &mut var_manager).unwrap(); + enc.encode_lb(0..=10, &mut solver, &mut var_manager) + .unwrap(); let assumps = enc.enforce_lb(10).unwrap(); - let res = solver.solve_assumps(&assumps).unwrap(); + let res = solver.solve_assumps(dbg!(&assumps)).unwrap(); assert_eq!(res, SolverResult::Unsat); let assumps = enc.enforce_lb(9).unwrap(); println!("{:?}", assumps); - let res = solver.solve_assumps(&assumps).unwrap(); + let res = solver.solve_assumps(dbg!(&assumps)).unwrap(); assert_eq!(res, SolverResult::Sat); } @@ -200,7 +201,7 @@ fn test_pb_ub_min_enc>>() { lits.insert(lit![2], 1); let mut enc = PBE::from(lits); - enc.encode_ub(2..3, &mut solver, &mut var_manager).unwrap(); + enc.encode_ub(2..=2, &mut solver, &mut var_manager).unwrap(); let mut assumps = enc.enforce_ub(2).unwrap(); assumps.extend(vec![lit![0], lit![1], lit![2]]); let res = solver.solve_assumps(&assumps).unwrap(); @@ -282,6 +283,26 @@ fn dbgte_min_enc() { test_pb_ub_min_enc::() } +#[test] +fn adder_ub() { + test_inc_pb_ub::() +} + +#[test] +fn adder_lb() { + test_pb_lb::() +} + +#[test] +fn adder_eq() { + test_pb_eq::() +} + +#[test] +fn adder_min_enc() { + test_pb_ub_min_enc::() +} + use rustsat_tools::{test_all, test_assignment}; fn test_ub_exhaustive>>( @@ -425,6 +446,8 @@ generate_exhaustive!( simulators::Card ); +generate_exhaustive!(adder, BinaryAdder); + mod dpw_inc_prec { use rustsat::{ encodings::pb::{dpw::DynamicPolyWatchdog, BoundUpper, BoundUpperIncremental},