Implement Debug for types

Cargo.toml

@@ -5,3 +5,6 @@ resolver = "2"
 [profile.release]
 lto = "fat"
 codegen-units = 1
+
+[workspace.lints.rust]
+missing_debug_implementations = "warn"

crates/pindakaas/Cargo.toml

@@ -39,3 +39,6 @@ kissat = ["pindakaas-kissat", "pindakaas-derive"]
 trace = ["tracing"]
 default = ["cadical"]
 ipasir-up = ["cadical"]
+
+[lints]
+workspace = true

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,
 }

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<DB: ClauseDatabase> Encoder<DB, CardinalityOne> for BitwiseEncoder {

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<DB: ClauseDatabase> Encoder<DB, CardinalityOne> for LadderEncoder {

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<DB: ClauseDatabase> Encoder<DB, CardinalityOne> for PairwiseEncoder {

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]

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<Lit>,
@@ -718,6 +720,8 @@ impl Cnf {
 		}
 	}
 }
+
+#[derive(Debug, Clone)]
 pub struct CnfIterator<'a> {
 	lits: &'a Vec<Lit>,
 	size: std::slice::Iter<'a, usize>,

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<Enc = StaticLinEncoder, Agg = LinearAggregator> {
 	pub enc: Enc,
 	pub agg: Agg,
@@ -617,7 +617,7 @@ impl<DB: ClauseDatabase, Enc: Encoder<DB, LinVariant>> Encoder<DB, LinearConstra
 
 // This is just a linear encoder that currently makes an arbitrary choice.
 // This is probably not how we would like to do it in the future.
-#[derive(Default)]
+#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)]
 pub struct StaticLinEncoder<
 	LinEnc = AdderEncoder,
 	CardEnc = AdderEncoder, // TODO: Actual Cardinality encoding

crates/pindakaas/src/linear/adder.rs

@@ -10,7 +10,7 @@ use crate::{
 };
 
 /// Encoder for the linear constraints that ∑ coeffᵢ·litsᵢ ≷ k using a binary adders circuits
-#[derive(Default)]
+#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)]
 pub struct AdderEncoder {}
 
 impl<DB: ClauseDatabase> Encoder<DB, Linear> for AdderEncoder {

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,

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<Coeff>,

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,

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,

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,

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

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,

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,

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<Library> 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>,

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,