From e7087d6849feed20a7a297369d17db39c4d5add2 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 8 May 2024 17:24:57 +1000 Subject: [PATCH] Implement Debug for types --- Cargo.toml | 3 +++ crates/pindakaas/Cargo.toml | 3 +++ crates/pindakaas/src/cardinality/sorting_network.rs | 1 + crates/pindakaas/src/cardinality_one/bitwise.rs | 2 +- crates/pindakaas/src/cardinality_one/ladder.rs | 2 +- crates/pindakaas/src/cardinality_one/pairwise.rs | 2 +- crates/pindakaas/src/int/model.rs | 2 +- crates/pindakaas/src/lib.rs | 4 ++++ crates/pindakaas/src/linear.rs | 6 +++--- crates/pindakaas/src/linear/adder.rs | 2 +- crates/pindakaas/src/linear/aggregator.rs | 2 +- crates/pindakaas/src/linear/bdd.rs | 2 +- crates/pindakaas/src/linear/swc.rs | 2 +- crates/pindakaas/src/linear/totalizer.rs | 2 +- crates/pindakaas/src/solver.rs | 1 + crates/pindakaas/src/solver/cadical.rs | 11 +++++++++++ crates/pindakaas/src/solver/intel_sat.rs | 2 +- crates/pindakaas/src/solver/kissat.rs | 2 +- crates/pindakaas/src/solver/libloading.rs | 4 ++++ crates/pindakaas/src/sorted.rs | 5 +++-- 20 files changed, 44 insertions(+), 16 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index f7ef798c80..aae7a3ca0c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,3 +5,6 @@ resolver = "2" [profile.release] lto = "fat" codegen-units = 1 + +[workspace.lints.rust] +missing_debug_implementations = "warn" diff --git a/crates/pindakaas/Cargo.toml b/crates/pindakaas/Cargo.toml index 33cd9214cd..d3398fbfbb 100644 --- a/crates/pindakaas/Cargo.toml +++ b/crates/pindakaas/Cargo.toml @@ -39,3 +39,6 @@ kissat = ["pindakaas-kissat", "pindakaas-derive"] trace = ["tracing"] default = ["cadical"] ipasir-up = ["cadical"] + +[lints] +workspace = true diff --git a/crates/pindakaas/src/cardinality/sorting_network.rs b/crates/pindakaas/src/cardinality/sorting_network.rs index 5b6fac357b..be41090324 100644 --- a/crates/pindakaas/src/cardinality/sorting_network.rs +++ b/crates/pindakaas/src/cardinality/sorting_network.rs @@ -5,6 +5,7 @@ use crate::{ }; /// Encoder for the linear constraints that ∑ litsᵢ ≷ k using a sorting network +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct SortingNetworkEncoder { pub sorted_encoder: SortedEncoder, } diff --git a/crates/pindakaas/src/cardinality_one/bitwise.rs b/crates/pindakaas/src/cardinality_one/bitwise.rs index 8435a447a3..fe7a35c95e 100644 --- a/crates/pindakaas/src/cardinality_one/bitwise.rs +++ b/crates/pindakaas/src/cardinality_one/bitwise.rs @@ -10,7 +10,7 @@ use crate::{ /// An encoder for [`CardinalityOne`] constraints that uses a logarithm /// encoded selector variable to ensure the selection of at most one of /// the given literals -#[derive(Default)] +#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] pub struct BitwiseEncoder {} impl Encoder for BitwiseEncoder { diff --git a/crates/pindakaas/src/cardinality_one/ladder.rs b/crates/pindakaas/src/cardinality_one/ladder.rs index cee13cb715..5d979c7719 100644 --- a/crates/pindakaas/src/cardinality_one/ladder.rs +++ b/crates/pindakaas/src/cardinality_one/ladder.rs @@ -5,7 +5,7 @@ use crate::{ }; /// An encoder for an At Most One constraints that TODO -#[derive(Default)] +#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] pub struct LadderEncoder {} impl Encoder for LadderEncoder { diff --git a/crates/pindakaas/src/cardinality_one/pairwise.rs b/crates/pindakaas/src/cardinality_one/pairwise.rs index 77bd86f49d..ab9c87ef51 100644 --- a/crates/pindakaas/src/cardinality_one/pairwise.rs +++ b/crates/pindakaas/src/cardinality_one/pairwise.rs @@ -7,7 +7,7 @@ use crate::{ /// An encoder for an At Most One constraints that for every pair of literals /// states that one of the literals has to be `false`. -#[derive(Default)] +#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] pub struct PairwiseEncoder {} impl Encoder for PairwiseEncoder { diff --git a/crates/pindakaas/src/int/model.rs b/crates/pindakaas/src/int/model.rs index 2d5164b53a..2a9c981a21 100644 --- a/crates/pindakaas/src/int/model.rs +++ b/crates/pindakaas/src/int/model.rs @@ -23,7 +23,7 @@ pub(crate) struct Model { // TODO Domain will be used once (/if) this is added as encoder feature. #[allow(dead_code)] -#[derive(Default, Clone, PartialEq)] +#[derive(Debug, Default, Clone, Copy, PartialEq, Eq, Hash)] pub enum Consistency { None, #[default] diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs index 9ccc933d17..46e8505b77 100755 --- a/crates/pindakaas/src/lib.rs +++ b/crates/pindakaas/src/lib.rs @@ -272,6 +272,7 @@ pub type Coeff = i64; /// IntEncoding is a enumerated type use to represent Boolean encodings of /// integer variables within this library +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum IntEncoding<'a> { /// The Direct variant represents a integer variable encoded using domain /// or direct encoding of an integer variable. Each given Boolean literal @@ -322,6 +323,7 @@ pub trait ClauseDatabase { } // TODO: Add usage and think about interface +#[derive(Debug, PartialEq, Eq, Hash)] pub struct ConditionalDatabase<'a, DB: ClauseDatabase + ?Sized> { db: &'a mut DB, conditions: Vec, @@ -718,6 +720,8 @@ impl Cnf { } } } + +#[derive(Debug, Clone)] pub struct CnfIterator<'a> { lits: &'a Vec, size: std::slice::Iter<'a, usize>, diff --git a/crates/pindakaas/src/linear.rs b/crates/pindakaas/src/linear.rs index 9d2616d44c..2e9d24f743 100644 --- a/crates/pindakaas/src/linear.rs +++ b/crates/pindakaas/src/linear.rs @@ -152,7 +152,7 @@ pub(crate) enum Part { Dom(Vec<(Lit, PosCoeff)>, PosCoeff, PosCoeff), } -#[derive(Clone, Debug, Eq, PartialEq)] +#[derive(Clone, Debug, Eq, PartialEq, Hash)] pub enum LimitComp { Equal, LessEq, @@ -582,7 +582,7 @@ impl Checker for Linear { } } -#[derive(Default)] +#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] pub struct LinearEncoder { pub enc: Enc, pub agg: Agg, @@ -617,7 +617,7 @@ impl> Encoder Encoder for AdderEncoder { diff --git a/crates/pindakaas/src/linear/aggregator.rs b/crates/pindakaas/src/linear/aggregator.rs index 4294db32bb..ce4f260c41 100644 --- a/crates/pindakaas/src/linear/aggregator.rs +++ b/crates/pindakaas/src/linear/aggregator.rs @@ -13,7 +13,7 @@ use crate::{ Linear, LinearConstraint, Lit, Result, Unsatisfiable, }; -#[derive(Default, Clone)] +#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] pub struct LinearAggregator { sorted_encoder: SortedEncoder, sort_same_coefficients: usize, diff --git a/crates/pindakaas/src/linear/bdd.rs b/crates/pindakaas/src/linear/bdd.rs index f6d6c2710a..c45dad8209 100755 --- a/crates/pindakaas/src/linear/bdd.rs +++ b/crates/pindakaas/src/linear/bdd.rs @@ -11,7 +11,7 @@ use crate::{ }; /// Encode the constraint that ∑ coeffᵢ·litsᵢ ≦ k using a Binary Decision Diagram (BDD) -#[derive(Default, Clone)] +#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] pub struct BddEncoder { add_consistency: bool, cutoff: Option, diff --git a/crates/pindakaas/src/linear/swc.rs b/crates/pindakaas/src/linear/swc.rs index 87e3754bc4..29784444a1 100644 --- a/crates/pindakaas/src/linear/swc.rs +++ b/crates/pindakaas/src/linear/swc.rs @@ -8,7 +8,7 @@ use crate::{ }; /// Encode the constraint that ∑ coeffᵢ·litsᵢ ≦ k using a Sorted Weight Counter (SWC) -#[derive(Clone, Default)] +#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] pub struct SwcEncoder { add_consistency: bool, add_propagation: Consistency, diff --git a/crates/pindakaas/src/linear/totalizer.rs b/crates/pindakaas/src/linear/totalizer.rs index 5846c55c28..384c1f35d5 100755 --- a/crates/pindakaas/src/linear/totalizer.rs +++ b/crates/pindakaas/src/linear/totalizer.rs @@ -12,7 +12,7 @@ use crate::{ const EQUALIZE_INTERMEDIATES: bool = false; /// Encode the constraint that ∑ coeffᵢ·litsᵢ ≦ k using a Generalized Totalizer (GT) -#[derive(Clone, Default)] +#[derive(Debug, Clone, Default, PartialEq, Eq, Hash)] pub struct TotalizerEncoder { add_consistency: bool, add_propagation: Consistency, diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 62994f84eb..32c990c012 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -249,6 +249,7 @@ pub trait SolvingActions { fn is_decision(&mut self, lit: Lit) -> bool; } +#[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)] pub enum SlvTermSignal { Continue, Terminate, diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index 644464606e..7029ffcec4 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -1,3 +1,5 @@ +use std::fmt; + use pindakaas_cadical::{ccadical_copy, ccadical_phase, ccadical_unphase}; use pindakaas_derive::IpasirSolver; @@ -36,6 +38,15 @@ impl Clone for Cadical { } } +impl fmt::Debug for Cadical { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.debug_struct("Cadical") + .field("ptr", &self.ptr) + .field("vars", &self.vars) + .finish() + } +} + impl Cadical { pub fn phase(&mut self, lit: Lit) { unsafe { ccadical_phase(self.ptr, lit.0.get()) } diff --git a/crates/pindakaas/src/solver/intel_sat.rs b/crates/pindakaas/src/solver/intel_sat.rs index 91a436d4e9..c6c3a55ba6 100644 --- a/crates/pindakaas/src/solver/intel_sat.rs +++ b/crates/pindakaas/src/solver/intel_sat.rs @@ -2,7 +2,7 @@ use pindakaas_derive::IpasirSolver; use super::VarFactory; -#[derive(IpasirSolver)] +#[derive(Debug, IpasirSolver)] #[ipasir(krate = pindakaas_intel_sat, assumptions, learn_callback, term_callback)] pub struct IntelSat { ptr: *mut std::ffi::c_void, diff --git a/crates/pindakaas/src/solver/kissat.rs b/crates/pindakaas/src/solver/kissat.rs index ee192d7b22..473ca4ed86 100644 --- a/crates/pindakaas/src/solver/kissat.rs +++ b/crates/pindakaas/src/solver/kissat.rs @@ -2,7 +2,7 @@ use pindakaas_derive::IpasirSolver; use super::VarFactory; -#[derive(IpasirSolver)] +#[derive(Debug, IpasirSolver)] #[ipasir(krate = pindakaas_kissat)] pub struct Kissat { ptr: *mut std::ffi::c_void, diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index e2d087ca9f..cb68cde4e5 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -16,6 +16,7 @@ use super::{ use super::{Propagator, SolvingActions}; use crate::{ClauseDatabase, ConditionalDatabase, Lit, Result, Valuation, Var}; +#[derive(Debug)] pub struct IpasirLibrary { lib: Library, } @@ -117,6 +118,7 @@ impl TryFrom for IpasirLibrary { } } +#[derive(Debug)] pub struct IpasirSolver<'lib> { slv: *mut c_void, next_var: VarFactory, @@ -241,6 +243,7 @@ impl<'lib> IpasirSolver<'lib> { } } +#[derive(Debug)] pub struct IpasirSol<'lib> { slv: *mut c_void, value_fn: Symbol<'lib, extern "C" fn(*mut c_void, i32) -> i32>, @@ -261,6 +264,7 @@ impl Valuation for IpasirSol<'_> { } } +#[derive(Debug)] pub struct IpasirFailed<'lib> { slv: *mut c_void, failed_fn: Symbol<'lib, extern "C" fn(*mut c_void, i32) -> c_int>, diff --git a/crates/pindakaas/src/sorted.rs b/crates/pindakaas/src/sorted.rs index 466b79f9d5..e532e93d94 100644 --- a/crates/pindakaas/src/sorted.rs +++ b/crates/pindakaas/src/sorted.rs @@ -11,7 +11,7 @@ use crate::{ Valuation, }; -#[derive(Clone)] +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct SortedEncoder { pub(crate) add_consistency: bool, pub(crate) strategy: SortedStrategy, @@ -20,7 +20,7 @@ pub struct SortedEncoder { pub(crate) sort_n: SortN, } #[allow(dead_code)] -#[derive(Clone)] +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum SortN { One, #[allow(dead_code)] // TODO @@ -57,6 +57,7 @@ impl SortedEncoder { } } +#[derive(Debug, Clone)] pub struct Sorted<'a> { pub(crate) xs: &'a [Lit], pub(crate) cmp: LimitComp,