Skip to content

Commit

Permalink
Make Lit its own type
Browse files Browse the repository at this point in the history
  • Loading branch information
@Dekker1
Dekker1 committed Oct 6, 2023
1 parent dee1297 commit f18578e
Show file tree
Hide file tree
Showing 25 changed files with 2,875 additions and 2,990 deletions.
61 changes: 49 additions & 12 deletions .github/workflows/rust.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,33 +8,70 @@ on:

env:
CARGO_TERM_COLOR: always
RUST_CHANNEL: stable
# Lets us format with unstable rustfmt options
RUST_FMT_CHANNEL: nightly

jobs:
build:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: Build
run: cargo build --verbose
# build:
# runs-on: ubuntu-latest
# strategy:
# matrix:
# crate: []
# steps:
# - uses: actions/checkout@v3
# - name: Install Rust toolchain
# run: |
# rustup toolchain install --profile minimal --no-self-update ${{ env.RUST_CHANNEL }}
# rustup default ${{ env.RUST_CHANNEL }}
# - name: Cache dependencies
# uses: Swatinem/rust-cache@v2
# - name: Build ${{ matrix.crate }}
# run: cargo install --root dist/ --path crates/${{ matrix.crate }}
# - name: Upload build artifact
# uses: actions/upload-artifact@v3
# with:
# name: ${{ matrix.crate }}-${{ matrix.os }}
# path: dist/
test:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: Run tests
run: cargo test --workspace --verbose
check:
- name: Install Rust toolchain
run: |
rustup toolchain install --profile minimal --no-self-update ${{ env.RUST_CHANNEL }}
rustup default ${{ env.RUST_CHANNEL }}
- name: Cache dependencies
uses: Swatinem/rust-cache@v2
- name: Run cargo test
run: cargo test
clippy:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: Check Formatting
run: cargo fmt --all -- --check
- name: Install Rust toolchain
run: |
rustup toolchain install --profile minimal --component clippy --no-self-update ${{ env.RUST_CHANNEL }}
rustup default ${{ env.RUST_CHANNEL }}
- name: Cache dependencies
uses: Swatinem/rust-cache@v2
- name: Run clippy
run: cargo clippy -- -D warnings
format:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: Install Rust toolchain
run: |
rustup toolchain install --profile minimal --component rustfmt --no-self-update ${{ env.RUST_FMT_CHANNEL }}
rustup default ${{ env.RUST_CHANNEL }}
- name: Run cargo format
run: cargo +nightly fmt --all --check
semver:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: Check semver
uses: obi1kenobi/cargo-semver-checks-action@v1
uses: obi1kenobi/cargo-semver-checks-action@v2
with:
crate-name: pindakaas
2 changes: 0 additions & 2 deletions crates/pindakaas/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,14 +15,12 @@ cached = "0.46"
ipasir = { version = "0.3", features = ["ffi"] }
iset = "0.2"
itertools = "0.11"
num = "0.4"
rustc-hash = "1.1"

# Optional encoding tracing capabilities
tracing = { version = "0.1", optional = true }

# Optional Solver Interfaces
minisat = { git = "https://github.com/luteberget/minisat-rs.git", optional = true } # waiting on release for minisat::Lit::var()
splr = { version = "0.17", optional = true }

[dev-dependencies]
Expand Down
115 changes: 55 additions & 60 deletions crates/pindakaas/src/cardinality.rs
View file
Original file line number Diff line number Diff line change
@@ -1,29 +1,29 @@
use crate::{
linear::{LimitComp, LinMarker, Linear, PosCoeff},
CardinalityOne, Checker, ClauseDatabase, Coefficient, Encoder, Literal,
CardinalityOne, CheckError, Checker, ClauseDatabase, Encoder, Lit, Valuation,
};

mod sorting_network;
pub use sorting_network::SortingNetworkEncoder;

#[derive(Clone, Debug)]
pub struct Cardinality<Lit: Literal, C: Coefficient> {
pub lits: Vec<Lit>,
pub cmp: LimitComp,
pub k: PosCoeff<C>,
pub struct Cardinality {
pub(crate) lits: Vec<Lit>,
pub(crate) cmp: LimitComp,
pub(crate) k: PosCoeff,
}

impl<Lit: Literal, C: Coefficient> From<CardinalityOne<Lit>> for Cardinality<Lit, C> {
fn from(card1: CardinalityOne<Lit>) -> Self {
impl From<CardinalityOne> for Cardinality {
fn from(card1: CardinalityOne) -> Self {
Self {
lits: card1.lits,
cmp: card1.cmp,
k: C::one().into(),
k: PosCoeff::new(1),
}
}
}

impl<Lit: Literal, C: Coefficient> Cardinality<Lit, C> {
impl Cardinality {
#[cfg(feature = "trace")]
#[allow(dead_code)] // FIXME: Remove when used
pub(crate) fn trace_print(&self) -> String {
Expand All @@ -39,20 +39,18 @@ impl<Lit: Literal, C: Coefficient> Cardinality<Lit, C> {
}
}

impl<Lit: Literal, C: Coefficient> Checker for Cardinality<Lit, C> {
type Lit = Lit;

fn check(&self, solution: &[Self::Lit]) -> Result<(), crate::CheckError<Self::Lit>> {
Linear::from(self.clone()).check(solution)
impl Checker for Cardinality {
fn check<F: Valuation>(&self, value: F) -> Result<(), CheckError> {
Linear::from(self.clone()).check(value)
}
}

// Automatically implement AtMostOne encoding when you can encode Cardinality constraints
impl<DB: ClauseDatabase, Enc: Encoder<DB, Cardinality<DB::Lit, i8>> + CardMarker>
Encoder<DB, CardinalityOne<DB::Lit>> for Enc
impl<DB: ClauseDatabase, Enc: Encoder<DB, Cardinality> + CardMarker> Encoder<DB, CardinalityOne>
for Enc
{
fn encode(&mut self, db: &mut DB, con: &CardinalityOne<DB::Lit>) -> crate::Result {
self.encode(db, &Cardinality::<DB::Lit, i8>::from(con.clone()))
fn encode(&mut self, db: &mut DB, con: &CardinalityOne) -> crate::Result {
self.encode(db, &Cardinality::from(con.clone()))
}
}
// local marker trait, to ensure the previous definition only applies within this crate
Expand All @@ -71,18 +69,18 @@ pub(crate) mod tests {
$encoder,
3,
&Cardinality {
lits: vec![-1, -2, 3],
lits: lits![-1, -2, 3],
cmp: LimitComp::LessEq,
k: 2.into()
k: PosCoeff::new(2)
} =>
vec![
vec![-1, -2, -3],
vec![-1, 2, -3],
vec![-1, 2, 3],
vec![1, -2, -3],
vec![1, -2, 3],
vec![1, 2, -3],
vec![1, 2, 3],
lits![-1, -2, -3],
lits![-1, 2, -3],
lits![-1, 2, 3],
lits![1, -2, -3],
lits![1, -2, 3],
lits![1, 2, -3],
lits![1, 2, 3],
]
);
}
Expand All @@ -93,15 +91,15 @@ pub(crate) mod tests {
$encoder,
3,
&Cardinality {
lits: vec![1, 2, 3],
lits: lits![1, 2, 3],
cmp: LimitComp::Equal,
k: 1.into()
k: PosCoeff::new(1)
}
=>
vec![
vec![ 1,-2,-3],
vec![-1, 2,-3],
vec![-1,-2, 3],
lits![ 1,-2,-3],
lits![-1, 2,-3],
lits![-1,-2, 3],
]
);
}
Expand All @@ -113,15 +111,15 @@ pub(crate) mod tests {
$encoder,
3,
&Cardinality {
lits: vec![1, 2, 3],
lits: lits![1, 2, 3],
cmp: LimitComp::Equal,
k: 2.into()
k: PosCoeff::new(2)
}
=>
vec![
vec![1, 2, -3],
vec![1, -2, 3],
vec![-1, 2, 3],
lits![1, 2, -3],
lits![1, -2, 3],
lits![-1, 2, 3],
]
);
}
Expand All @@ -132,17 +130,17 @@ pub(crate) mod tests {
$encoder,
4,
&Cardinality {
lits: vec![1, 2, 3, 4],
lits: lits![1, 2, 3, 4],
cmp: LimitComp::Equal,
k: 2.into()
k: PosCoeff::new(2)
} =>
vec![
vec![1, 2, -3, -4],
vec![1, -2, 3, -4],
vec![-1, 2, 3, -4],
vec![1, -2, -3, 4],
vec![-1, 2, -3, 4],
vec![-1, -2, 3, 4],
lits![1, 2, -3, -4],
lits![1, -2, 3, -4],
lits![-1, 2, 3, -4],
lits![1, -2, -3, 4],
lits![-1, 2, -3, 4],
lits![-1, -2, 3, 4],
]
);
}
Expand All @@ -155,28 +153,25 @@ pub(crate) mod tests {
$encoder,
5,
&Cardinality {
lits: vec![ 1, 2, 3, 4 ,5 ],
lits: lits![1, 2, 3, 4 ,5],
cmp: LimitComp::Equal,
k: 3.into()
k: PosCoeff::new(3)
}
=>
vec![
vec![1, 2, 3, -4, -5],
vec![1, 2, -3, 4, -5],
vec![1, -2, 3, 4, -5],
vec![-1, 2, 3, 4, -5],
vec![1, 2, -3, -4, 5],
vec![1, -2, 3, -4, 5],
vec![-1, 2, 3, -4, 5],
vec![1, -2, -3, 4, 5],
vec![-1, 2, -3, 4, 5],
vec![-1, -2, 3, 4, 5],
lits![1, 2, 3, -4, -5],
lits![1, 2, -3, 4, -5],
lits![1, -2, 3, 4, -5],
lits![-1, 2, 3, 4, -5],
lits![1, 2, -3, -4, 5],
lits![1, -2, 3, -4, 5],
lits![-1, 2, 3, -4, 5],
lits![1, -2, -3, 4, 5],
lits![-1, 2, -3, 4, 5],
lits![-1, -2, 3, 4, 5],
]
);
}



};
}

Expand Down
16 changes: 7 additions & 9 deletions crates/pindakaas/src/cardinality/sorting_network.rs
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use crate::{
int::IntVarEnc,
sorted::{Sorted, SortedEncoder},
Cardinality, ClauseDatabase, Coefficient, Encoder, Result,
Cardinality, ClauseDatabase, Encoder, Result,
};

/// Encoder for the linear constraints that ∑ litsᵢ ≷ k using a sorting network
Expand All @@ -28,16 +28,14 @@ impl SortingNetworkEncoder {
}
}

impl<DB: ClauseDatabase, C: Coefficient> Encoder<DB, Cardinality<DB::Lit, C>>
for SortingNetworkEncoder
{
fn encode(&mut self, db: &mut DB, card: &Cardinality<DB::Lit, C>) -> Result {
impl<DB: ClauseDatabase> Encoder<DB, Cardinality> for SortingNetworkEncoder {
fn encode(&mut self, db: &mut DB, card: &Cardinality) -> Result {
self.sorted_encoder.encode(
db,
&Sorted::new(
card.lits.as_slice(),
card.cmp.clone(),
&IntVarEnc::Const(*card.k),
&IntVarEnc::Const(card.k.into()),
),
)
}
Expand All @@ -48,7 +46,7 @@ mod tests {
use super::*;
use crate::{
helpers::tests::assert_sol,
linear::LimitComp,
linear::{LimitComp, PosCoeff},
sorted::{SortedEncoder, SortedStrategy},
Cardinality, Encoder,
};
Expand All @@ -59,9 +57,9 @@ mod tests {
$encoder,
$n,
&Cardinality {
lits: (1..=$n).collect(),
lits: (1..=$n).map(|l| l.into()).collect(),
cmp: $cmp,
k: $k.into()
k: PosCoeff::new($k)
}
);
};
Expand Down
Loading

0 comments on commit f18578e

Please sign in to comment.