Skip to content

Commit

Permalink
chore: clippy
Browse files Browse the repository at this point in the history
  • Loading branch information
chrjabs committed Aug 19, 2024
1 parent 971b258 commit cd52b94
Show file tree
Hide file tree
Showing 11 changed files with 69 additions and 56 deletions.
50 changes: 25 additions & 25 deletions src/instances/fio/opb.rs
Original file line number Diff line number Diff line change
Expand Up @@ -358,7 +358,7 @@ fn opb_data(input: &str, opts: Options) -> IResult<&str, OpbData> {

/// Possible lines that can be written to OPB
#[cfg(not(feature = "optimization"))]
pub enum OpbLine {
pub enum FileLine {
/// A comment line
Comment(String),
/// A clausal constraint line
Expand All @@ -371,7 +371,7 @@ pub enum OpbLine {

/// Possible lines that can be written to OPB
#[cfg(feature = "optimization")]
pub enum OpbLine<LI: crate::types::WLitIter> {
pub enum FileLine<LI: crate::types::WLitIter> {
/// A comment line
Comment(String),
/// A clausal constraint line
Expand All @@ -384,47 +384,47 @@ pub enum OpbLine<LI: crate::types::WLitIter> {
Objective(LI),
}

/// Writes an OPB file from an interator over [`OpbLine`]s
/// Writes an OPB file from an interator over [`FileLine`]s
///
/// # Errors
///
/// If writing fails, returns [`io::Error`]
#[cfg(not(feature = "optimization"))]
pub fn write_opb_lines<W, LI, Iter>(
writer: &mut W,
data: Iter,
opts: Options,
) -> Result<(), io::Error>
pub fn write_opb_lines<W, Iter>(writer: &mut W, data: Iter, opts: Options) -> io::Result<()>
where
W: Write,
Iter: Iterator<Item = OpbLine>,
Iter: Iterator<Item = FileLine>,
{
for dat in data {
match dat {
OpbLine::Comment(c) => writeln!(writer, "* {c}")?,
OpbLine::Clause(cl) => write_clause(writer, &cl, opts)?,
OpbLine::Card(card) => write_card(writer, &card, opts)?,
OpbLine::Pb(pb) => write_pb(writer, &pb, opts)?,
FileLine::Comment(c) => writeln!(writer, "* {c}")?,
FileLine::Clause(cl) => write_clause(writer, &cl, opts)?,
FileLine::Card(card) => write_card(writer, &card, opts)?,
FileLine::Pb(pb) => write_pb(writer, &pb, opts)?,
}
}
Ok(())
}

/// Writes an OPB file from an interator over [`OpbLine`]s
/// Writes an OPB file from an interator over [`FileLine`]s
///
/// # Errors
///
/// If writing fails, returns [`io::Error`]
#[cfg(feature = "optimization")]
pub fn write_opb_lines<W, LI, Iter>(
writer: &mut W,
data: Iter,
opts: Options,
) -> Result<(), io::Error>
pub fn write_opb_lines<W, LI, Iter>(writer: &mut W, data: Iter, opts: Options) -> io::Result<()>
where
W: Write,
LI: crate::types::WLitIter,
Iter: Iterator<Item = OpbLine<LI>>,
Iter: Iterator<Item = FileLine<LI>>,
{
for dat in data {
match dat {
OpbLine::Comment(c) => writeln!(writer, "* {c}")?,
OpbLine::Clause(cl) => write_clause(writer, &cl, opts)?,
OpbLine::Card(card) => write_card(writer, &card, opts)?,
OpbLine::Pb(pb) => write_pb(writer, &pb, opts)?,
OpbLine::Objective(obj) => write_objective(writer, (obj, 0), opts)?,
FileLine::Comment(c) => writeln!(writer, "* {c}")?,
FileLine::Clause(cl) => write_clause(writer, &cl, opts)?,
FileLine::Card(card) => write_card(writer, &card, opts)?,
FileLine::Pb(pb) => write_pb(writer, &pb, opts)?,
FileLine::Objective(obj) => write_objective(writer, (obj, 0), opts)?,
}
}
Ok(())
Expand Down
2 changes: 1 addition & 1 deletion src/instances/sat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1080,7 +1080,7 @@ impl<VM: ManageVars> Instance<VM> {

/// Returns an unsatisfied constraint, if one exists
pub fn unsat_constraint(&self, assign: &Assignment) -> Option<ConstraintRef> {
for clause in self.cnf.iter() {
for clause in &self.cnf {
if clause.evaluate(assign) != TernaryVal::True {
return Some(ConstraintRef::Clause(clause));
}
Expand Down
10 changes: 7 additions & 3 deletions src/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -859,6 +859,10 @@ impl Assignment {
/// - [SAT Competition](https://satcompetition.github.io/2024/output.html): `v 1 -2 -3 4 0`
/// - [MaxSAT Evaluation](https://maxsat-evaluations.github.io/2024/rules.html): `v 1001`
/// - [PB Competition](https://www.cril.univ-artois.fr/PB24/competitionRequirements.pdf): `v x1 -x2 -x3 x4`
///
/// # Errors
///
/// Can return various parsing errors
pub fn extend_from_vline(&mut self, lines: &str) -> anyhow::Result<()> {
anyhow::ensure!(!lines.is_empty(), InvalidVLine::EmptyLine);
// determine line format
Expand Down Expand Up @@ -894,7 +898,7 @@ impl Assignment {
VLineFormat::SatComp => self.extend_sat_comp_vline(line),
VLineFormat::MaxSatEval => self.extend_maxsat_eval_vline(line),
VLineFormat::PbComp => self.extend_pb_comp_vline(line),
}?
}?;
}
Ok(())
}
Expand Down Expand Up @@ -942,8 +946,8 @@ impl Assignment {
let line = &line[1..];
for number in line.split_whitespace() {
let (_, lit) = fio::opb::literal(number, fio::opb::Options::default())
.map_err(|e| e.to_owned())
.with_context(|| format!("failed to parse pb literal '{}'", number))?;
.map_err(nom::Err::<nom::error::Error<&str>>::to_owned)
.with_context(|| format!("failed to parse pb literal '{number}'"))?;
let val = self.lit_value(lit);
if val == TernaryVal::True && lit.is_neg() || val == TernaryVal::False && lit.is_pos() {
// Catch conflicting assignments
Expand Down
6 changes: 6 additions & 0 deletions src/types/constraints.rs
Original file line number Diff line number Diff line change
Expand Up @@ -599,6 +599,7 @@ impl CardConstraint {
}

/// Gets the number of literals in the constraint
#[must_use]
pub fn len(&self) -> usize {
match self {
CardConstraint::Ub(constr) => constr.lits.len(),
Expand All @@ -608,11 +609,13 @@ impl CardConstraint {
}

/// Checks whether the constraint is empty
#[must_use]
pub fn is_empty(&self) -> bool {
self.len() == 0
}

/// Gets the number of literals in the constraint
#[must_use]
pub fn n_lits(&self) -> usize {
self.len()
}
Expand Down Expand Up @@ -1109,6 +1112,7 @@ impl PbConstraint {
}

/// Gets the number of literals in the constraint
#[must_use]
pub fn len(&self) -> usize {
match self {
PbConstraint::Ub(constr) => constr.lits.len(),
Expand All @@ -1118,11 +1122,13 @@ impl PbConstraint {
}

/// Checks whether the constraint is empty
#[must_use]
pub fn is_empty(&self) -> bool {
self.len() == 0
}

/// Gets the number of literals in the constraint
#[must_use]
pub fn n_lits(&self) -> usize {
self.len()
}
Expand Down
1 change: 1 addition & 0 deletions tools/src/bin/check-solution.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ pub enum FileFormat {
/// - `.mcnf`: Multi-objective MaxSAT file
/// - `.opb`: OPB file (without an objective)
/// - `.mopb` / `.pbmo`: Multi-objective OPB file
///
/// All file extensions can also be appended with `.bz2`, `.xz`, or `.gz` if compression is used.
Infer,
/// A DIMACS CNF file
Expand Down
10 changes: 5 additions & 5 deletions tools/src/bin/encodings.rs
Original file line number Diff line number Diff line change
Expand Up @@ -259,7 +259,7 @@ fn cnf_knapsack(inst: knapsack::Knapsack) -> impl Iterator<Item = dimacs::McnfLi

fn pb_knapsack(
inst: knapsack::Knapsack,
) -> impl Iterator<Item = opb::OpbLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>> {
) -> impl Iterator<Item = opb::FileLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>> {
pb::knapsack::Encoding::new(inst)
}

Expand All @@ -274,7 +274,7 @@ fn input_assignment(args: &AssignmentArgs) -> anyhow::Result<assignment::Assignm

fn pb_assignment(
inst: assignment::Assignment,
) -> impl Iterator<Item = opb::OpbLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>> {
) -> impl Iterator<Item = opb::FileLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>> {
pb::assignment::Encoding::new(inst)
}

Expand All @@ -291,7 +291,7 @@ fn input_facility_location(

fn pb_facility_location(
inst: facilitylocation::FacilityLocation,
) -> impl Iterator<Item = opb::OpbLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>> {
) -> impl Iterator<Item = opb::FileLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>> {
pb::facilitylocation::Encoding::new(inst)
}

Expand Down Expand Up @@ -322,7 +322,7 @@ fn write_cnf(
}

fn write_pb<LI: WLitIter>(
encoding: impl Iterator<Item = opb::OpbLine<LI>>,
encoding: impl Iterator<Item = opb::FileLine<LI>>,
path: Option<PathBuf>,
opts: opb::Options,
) -> anyhow::Result<()> {
Expand All @@ -337,7 +337,7 @@ fn write_pb<LI: WLitIter>(

type BoxedDimacsIter = Box<dyn Iterator<Item = dimacs::McnfLine>>;
type BoxedOpbIter =
Box<dyn Iterator<Item = opb::OpbLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>>>;
Box<dyn Iterator<Item = opb::FileLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>>>;

fn main() -> anyhow::Result<()> {
let args = CliArgs::parse();
Expand Down
1 change: 1 addition & 0 deletions tools/src/bin/gbmosplit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -218,6 +218,7 @@ enum InputFormat {
/// Infer the input file format from the file extension according to the following rules:
/// - `.wcnf`: Weighted DIMACS CNF (MaxSAT) file
/// - `.opb`: OPB file (without an objective)
///
/// All file extensions can also be appended with `.bz2`, `.xz`, or `.gz` if compression is used.
#[default]
Infer,
Expand Down
1 change: 1 addition & 0 deletions tools/src/bin/mo2ilp.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ enum InputFormat {
/// Infer the file format from the file extension according to the following rules:
/// - `.mcnf`: Multi-objective MaxSAT file
/// - `.opb`, `.pbmo`, `.mopb`: OPB file
///
/// All file extensions can also be appended with `.bz2`, `.xz`, or `.gz` if compression is used.
Infer,
/// A DIMACS MCNF file
Expand Down
14 changes: 8 additions & 6 deletions tools/src/encodings/pb/assignment.rs
Original file line number Diff line number Diff line change
Expand Up @@ -38,23 +38,25 @@ impl Encoding {
}

impl Iterator for Encoding {
type Item = opb::OpbLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>;
type Item = opb::FileLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>;

fn next(&mut self) -> Option<Self::Item> {
let selector = |task: usize, agent: usize| lit![(self.data.n_tasks * task + agent) as u32];
match self.next_line.take() {
Some(line) => Some(match line {
Line::Hint => {
self.next_line = Some(Line::Description);
opb::OpbLine::Comment(format!(
opb::FileLine::Comment(format!(
"#variable= {} #constraint= {}",
self.data.n_tasks * self.data.n_tasks,
2 * self.data.n_tasks
))
}
Line::Description => {
self.next_line = Some(Line::Objective(0));
opb::OpbLine::Comment("MO Assignment instance generated by RustSAT".to_string())
opb::FileLine::Comment(
"MO Assignment instance generated by RustSAT".to_string(),
)
}
Line::Objective(objidx) => {
let data = &self.data;
Expand All @@ -70,7 +72,7 @@ impl Iterator for Encoding {
} else {
Line::OneTask(0)
});
opb::OpbLine::Objective(obj.into_iter())
opb::FileLine::Objective(obj.into_iter())
}
Line::OneTask(agent) => {
let constr = CardConstraint::new_eq(
Expand All @@ -82,7 +84,7 @@ impl Iterator for Encoding {
} else {
Line::OneAgent(0)
});
opb::OpbLine::Card(constr)
opb::FileLine::Card(constr)
}
Line::OneAgent(task) => {
let constr = CardConstraint::new_eq(
Expand All @@ -94,7 +96,7 @@ impl Iterator for Encoding {
} else {
None
};
opb::OpbLine::Card(constr)
opb::FileLine::Card(constr)
}
}),
None => None,
Expand Down
20 changes: 9 additions & 11 deletions tools/src/encodings/pb/facilitylocation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ impl Encoding {
}

impl Iterator for Encoding {
type Item = opb::OpbLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>;
type Item = opb::FileLine<<Vec<(Lit, usize)> as IntoIterator>::IntoIter>;

fn next(&mut self) -> Option<Self::Item> {
let selected = |customer: usize, facility: usize| {
Expand All @@ -53,15 +53,15 @@ impl Iterator for Encoding {
Some(line) => Some(match line {
Line::Hint => {
self.next_line = Some(Line::Description);
opb::OpbLine::Comment(format!(
opb::FileLine::Comment(format!(
"#variable= {} #constraint= {}",
(self.data.n_customers() + 1) * self.data.n_facilities(),
self.data.n_customers() * (self.data.n_facilities() + 1)
))
}
Line::Description => {
self.next_line = Some(Line::Objective(0));
opb::OpbLine::Comment(
opb::FileLine::Comment(
"MO uncapacitated facility location instance generated by RustSAT"
.to_string(),
)
Expand All @@ -86,7 +86,7 @@ impl Iterator for Encoding {
} else {
Line::OneFacility(0)
});
opb::OpbLine::Objective(obj.into_iter())
opb::FileLine::Objective(obj.into_iter())
}
Line::OneFacility(customer) => {
let constr = CardConstraint::new_eq(
Expand All @@ -98,20 +98,18 @@ impl Iterator for Encoding {
} else {
Line::MustOpen(0, 0)
});
opb::OpbLine::Card(constr)
opb::FileLine::Card(constr)
}
Line::MustOpen(fac, customer) => {
let constr = atomics::lit_impl_lit(selected(customer, fac), opening(fac));
self.next_line = if customer + 1 < self.data.n_customers() {
Some(Line::MustOpen(fac, customer + 1))
} else if fac + 1 < self.data.n_facilities() {
Some(Line::MustOpen(fac + 1, 0))
} else {
if fac + 1 < self.data.n_facilities() {
Some(Line::MustOpen(fac + 1, 0))
} else {
None
}
None
};
opb::OpbLine::Clause(constr)
opb::FileLine::Clause(constr)
}
}),
None => None,
Expand Down
Loading

0 comments on commit cd52b94

Please sign in to comment.