Skip to content

Commit

Permalink
Implement Debug for types
Browse files Browse the repository at this point in the history
  • Loading branch information
Dekker1 committed May 8, 2024
1 parent d5c43e1 commit e7087d6
Show file tree
Hide file tree
Showing 20 changed files with 44 additions and 16 deletions.
3 changes: 3 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,6 @@ resolver = "2"
[profile.release]
lto = "fat"
codegen-units = 1

[workspace.lints.rust]
missing_debug_implementations = "warn"
3 changes: 3 additions & 0 deletions crates/pindakaas/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -39,3 +39,6 @@ kissat = ["pindakaas-kissat", "pindakaas-derive"]
trace = ["tracing"]
default = ["cadical"]
ipasir-up = ["cadical"]

[lints]
workspace = true
1 change: 1 addition & 0 deletions crates/pindakaas/src/cardinality/sorting_network.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
}
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas/src/cardinality_one/bitwise.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas/src/cardinality_one/ladder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas/src/cardinality_one/pairwise.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas/src/int/model.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
4 changes: 4 additions & 0 deletions crates/pindakaas/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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>,
Expand Down Expand Up @@ -718,6 +720,8 @@ impl Cnf {
}
}
}

#[derive(Debug, Clone)]
pub struct CnfIterator<'a> {
lits: &'a Vec<Lit>,
size: std::slice::Iter<'a, usize>,
Expand Down
6 changes: 3 additions & 3 deletions crates/pindakaas/src/linear.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas/src/linear/adder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas/src/linear/aggregator.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas/src/linear/bdd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>,
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas/src/linear/swc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas/src/linear/totalizer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
1 change: 1 addition & 0 deletions crates/pindakaas/src/solver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
11 changes: 11 additions & 0 deletions crates/pindakaas/src/solver/cadical.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
use std::fmt;

use pindakaas_cadical::{ccadical_copy, ccadical_phase, ccadical_unphase};
use pindakaas_derive::IpasirSolver;

Expand Down Expand Up @@ -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()) }
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas/src/solver/intel_sat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion crates/pindakaas/src/solver/kissat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
4 changes: 4 additions & 0 deletions crates/pindakaas/src/solver/libloading.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
}
Expand Down Expand Up @@ -117,6 +118,7 @@ impl TryFrom<Library> for IpasirLibrary {
}
}

#[derive(Debug)]
pub struct IpasirSolver<'lib> {
slv: *mut c_void,
next_var: VarFactory,
Expand Down Expand Up @@ -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>,
Expand All @@ -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>,
Expand Down
5 changes: 3 additions & 2 deletions crates/pindakaas/src/sorted.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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
Expand Down Expand Up @@ -57,6 +57,7 @@ impl SortedEncoder {
}
}

#[derive(Debug, Clone)]
pub struct Sorted<'a> {
pub(crate) xs: &'a [Lit],
pub(crate) cmp: LimitComp,
Expand Down

0 comments on commit e7087d6

Please sign in to comment.