diff --git a/cadical/src/lib.rs b/cadical/src/lib.rs index 2dd045bb..2303370f 100644 --- a/cadical/src/lib.rs +++ b/cadical/src/lib.rs @@ -351,6 +351,15 @@ impl Extend for CaDiCaL<'_, '_> { } } +impl<'a> Extend<&'a Clause> for CaDiCaL<'_, '_> { + fn extend>(&mut self, iter: T) { + iter.into_iter().for_each(|cl| { + self.add_clause_ref(cl) + .expect("Error adding clause in extend") + }) + } +} + impl Solve for CaDiCaL<'_, '_> { fn signature(&self) -> &'static str { let c_chars = unsafe { ffi::ccadical_signature() }; @@ -427,7 +436,7 @@ impl Solve for CaDiCaL<'_, '_> { } } - fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> { + fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> { // Update wrapper-internal state self.stats.n_clauses += 1; self.stats.avg_clause_len = @@ -436,7 +445,7 @@ impl Solve for CaDiCaL<'_, '_> { self.state = InternalSolverState::Input; // Call CaDiCaL backend clause - .into_iter() + .iter() .for_each(|l| unsafe { ffi::ccadical_add(self.handle, l.to_ipasir()) }); unsafe { ffi::ccadical_add(self.handle, 0) }; Ok(()) diff --git a/data/tiny-single-opt.opb b/data/tiny-single-opt.opb new file mode 100644 index 00000000..042f3b78 --- /dev/null +++ b/data/tiny-single-opt.opb @@ -0,0 +1,6 @@ +* #variable= 4 #constraint= 3 +* A handwritten OPB sat instance for basic testing +min: 1 x1 2 x2; +5 x1 -3 x2 >= 4; +5 x3 -3 x4 >= 2; +5 ~x4 >= 4; diff --git a/docs/0-5-0-migration-guide.md b/docs/0-5-0-migration-guide.md new file mode 100644 index 00000000..c7203dab --- /dev/null +++ b/docs/0-5-0-migration-guide.md @@ -0,0 +1,47 @@ +# Migration Guide for Breaking Changes in v0.5.0 + +This document gives an overview of the breaking API changes in v0.5.0 and how +to update your code accordingly. Mostly, follow the error messages the compiler +will give you after updating to the new RustSAT version. + +## Error Handling + +Error handling in the `Solve` trait, and file parsers now uses the +[`anyhow`](https://docs.rs/anyhow/latest/anyhow/) crate. This allows for better +error messages, and better tracing. In the process, some of the error types or +variants that are not needed any more have been removed: + +- `rustsat::solvers::SolverError` has been removed and only + `rustsat::solvers::StateError` remains +- `rustsat::instances::fio::opb::Error` has been removed +- `rustsat::instances::fio::dimacs::Error` has been removed +- `rustsat::instances::fio::ParsingError` has been removed +- `rustsat::solvers::SolverState::Error` has also been removed as no error + state is needed with proper error returns + +If you need to handle a specific error, you can use `anyhow`'s +[`downcast`](https://docs.rs/anyhow/latest/anyhow/struct.Error.html#method.downcast) +(e.g., on `solvers::StateError`), but I imagine most often these errors are +anyhow just propagated outwards and displayed. + +## Changes to Improve API Ergonomics + +There have been some API changes to improve usability, even though they are breaking. + +- File writing methods: all file writing methods (on `SatInstance`, + `OptInstance` and `MultiOptInstance`) are now called `write_` instead of `to_`. + Furthermore they take references instead of values and will return an error if + a specific format of the instance is expected but the instance does not satisfy + this requirement. +- File reading methods: all file reading methods (DIMACS and OPB, on + `SatInsatnce`, etc) now require a `BufRead` type as input. Previously, the + reader was internally wrapped in a + [`BufReader`](https://doc.rust-lang.org/stable/std/io/struct.BufReader.html) + object. This now has to be done externally to avoid potentially double + buffering. +- "Heavy" conversion function (e.g., `SatInstance::to_cnf`) are now called + `into_`. Additionally, inplace converter functions named `convert_to_` are also + provided. +- Methods providing references to internal data are now named `_ref` and `_mut` + if mutability is allowed. If only a non-mutable accessor is present, the `_ref` + suffix is omitted (e.g., for `SatInstance::cnf`). diff --git a/glucose/src/core.rs b/glucose/src/core.rs index 1c4a5231..ab9b4769 100644 --- a/glucose/src/core.rs +++ b/glucose/src/core.rs @@ -82,6 +82,15 @@ impl Extend for Glucose { } } +impl<'a> Extend<&'a Clause> for Glucose { + fn extend>(&mut self, iter: T) { + iter.into_iter().for_each(|cl| { + self.add_clause_ref(cl) + .expect("Error adding clause in extend") + }) + } +} + impl Solve for Glucose { fn signature(&self) -> &'static str { let c_chars = unsafe { ffi::cglucose4_signature() }; @@ -150,7 +159,7 @@ impl Solve for Glucose { } } - fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> { + fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> { // Update wrapper-internal state self.stats.n_clauses += 1; self.stats.avg_clause_len = @@ -158,7 +167,7 @@ impl Solve for Glucose { / self.stats.n_clauses as f32; self.state = InternalSolverState::Input; // Call glucose backend - clause.into_iter().for_each(|l| unsafe { + clause.iter().for_each(|l| unsafe { ffi::cglucose4_add(self.handle, l.to_ipasir()); }); unsafe { ffi::cglucose4_add(self.handle, 0) }; diff --git a/glucose/src/simp.rs b/glucose/src/simp.rs index 133dd083..84fcee65 100644 --- a/glucose/src/simp.rs +++ b/glucose/src/simp.rs @@ -90,6 +90,15 @@ impl Extend for Glucose { } } +impl<'a> Extend<&'a Clause> for Glucose { + fn extend>(&mut self, iter: T) { + iter.into_iter().for_each(|cl| { + self.add_clause_ref(cl) + .expect("Error adding clause in extend") + }) + } +} + impl Solve for Glucose { fn signature(&self) -> &'static str { let c_chars = unsafe { ffi::cglucose4_signature() }; @@ -158,7 +167,7 @@ impl Solve for Glucose { } } - fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> { + fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> { // Update wrapper-internal state self.stats.n_clauses += 1; self.stats.avg_clause_len = @@ -166,7 +175,7 @@ impl Solve for Glucose { / self.stats.n_clauses as f32; self.state = InternalSolverState::Input; // Call glucose backend - clause.into_iter().for_each(|l| unsafe { + clause.iter().for_each(|l| unsafe { ffi::cglucosesimp4_add(self.handle, l.to_ipasir()); }); unsafe { ffi::cglucosesimp4_add(self.handle, 0) }; diff --git a/ipasir/src/lib.rs b/ipasir/src/lib.rs index e4806b45..a1938893 100644 --- a/ipasir/src/lib.rs +++ b/ipasir/src/lib.rs @@ -186,7 +186,7 @@ impl Solve for IpasirSolver<'_, '_> { } } - fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> { + fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> { // Update wrapper-internal state self.stats.n_clauses += 1; clause.iter().for_each(|l| match self.stats.max_var { @@ -202,7 +202,7 @@ impl Solve for IpasirSolver<'_, '_> { / self.stats.n_clauses as f32; self.state = InternalSolverState::Input; // Call IPASIR backend - for lit in &clause { + for lit in clause { unsafe { ffi::ipasir_add(self.handle, lit.to_ipasir()) } } unsafe { ffi::ipasir_add(self.handle, 0) }; @@ -369,6 +369,15 @@ impl Extend for IpasirSolver<'_, '_> { } } +impl<'a> Extend<&'a Clause> for IpasirSolver<'_, '_> { + fn extend>(&mut self, iter: T) { + iter.into_iter().for_each(|cl| { + self.add_clause_ref(cl) + .expect("Error adding clause in extend") + }) + } +} + /// cbindgen:ignore mod ffi { use super::{LearnCallbackPtr, TermCallbackPtr}; diff --git a/kissat/src/lib.rs b/kissat/src/lib.rs index 900a4e1e..e0172c8a 100644 --- a/kissat/src/lib.rs +++ b/kissat/src/lib.rs @@ -188,6 +188,15 @@ impl Extend for Kissat<'_> { } } +impl<'a> Extend<&'a Clause> for Kissat<'_> { + fn extend>(&mut self, iter: T) { + iter.into_iter().for_each(|cl| { + self.add_clause_ref(cl) + .expect("Error adding clause in extend") + }) + } +} + impl Solve for Kissat<'_> { fn signature(&self) -> &'static str { let c_chars = unsafe { ffi::kissat_signature() }; @@ -260,7 +269,7 @@ impl Solve for Kissat<'_> { } } - fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> { + fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> { // Kissat is non-incremental, so only add if in input or configuring state if !matches!( self.state, @@ -288,7 +297,7 @@ impl Solve for Kissat<'_> { self.state = InternalSolverState::Input; // Call Kissat backend clause - .into_iter() + .iter() .for_each(|l| unsafe { ffi::kissat_add(self.handle, l.to_ipasir()) }); unsafe { ffi::kissat_add(self.handle, 0) }; Ok(()) diff --git a/minisat/src/core.rs b/minisat/src/core.rs index 7fa688ea..5d1200b4 100644 --- a/minisat/src/core.rs +++ b/minisat/src/core.rs @@ -82,6 +82,15 @@ impl Extend for Minisat { } } +impl<'a> Extend<&'a Clause> for Minisat { + fn extend>(&mut self, iter: T) { + iter.into_iter().for_each(|cl| { + self.add_clause_ref(cl) + .expect("Error adding clause in extend") + }) + } +} + impl Solve for Minisat { fn signature(&self) -> &'static str { let c_chars = unsafe { ffi::cminisat_signature() }; @@ -150,7 +159,7 @@ impl Solve for Minisat { } } - fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> { + fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> { // Update wrapper-internal state self.stats.n_clauses += 1; self.stats.avg_clause_len = @@ -158,7 +167,7 @@ impl Solve for Minisat { / self.stats.n_clauses as f32; self.state = InternalSolverState::Input; // Call minisat backend - clause.into_iter().for_each(|l| unsafe { + clause.iter().for_each(|l| unsafe { ffi::cminisat_add(self.handle, l.to_ipasir()); }); unsafe { ffi::cminisat_add(self.handle, 0) }; diff --git a/minisat/src/simp.rs b/minisat/src/simp.rs index e0991260..8c56b86b 100644 --- a/minisat/src/simp.rs +++ b/minisat/src/simp.rs @@ -90,6 +90,15 @@ impl Extend for Minisat { } } +impl<'a> Extend<&'a Clause> for Minisat { + fn extend>(&mut self, iter: T) { + iter.into_iter().for_each(|cl| { + self.add_clause_ref(cl) + .expect("Error adding clause in extend") + }) + } +} + impl Solve for Minisat { fn signature(&self) -> &'static str { let c_chars = unsafe { ffi::cminisat_signature() }; @@ -158,7 +167,7 @@ impl Solve for Minisat { } } - fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> { + fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> { // Update wrapper-internal state self.stats.n_clauses += 1; self.stats.avg_clause_len = @@ -166,7 +175,7 @@ impl Solve for Minisat { / self.stats.n_clauses as f32; self.state = InternalSolverState::Input; // Call minisat backend - clause.into_iter().for_each(|l| unsafe { + clause.iter().for_each(|l| unsafe { ffi::cminisatsimp_add(self.handle, l.to_ipasir()); }); unsafe { ffi::cminisatsimp_add(self.handle, 0) }; diff --git a/rustsat/.gitignore b/rustsat/.gitignore new file mode 100644 index 00000000..79cbaa16 --- /dev/null +++ b/rustsat/.gitignore @@ -0,0 +1,4 @@ +rustsat-test.opb +rustsat-test.cnf +rustsat-test.wcnf +rustsat-test.mcnf diff --git a/rustsat/src/encodings/card.rs b/rustsat/src/encodings/card.rs index 7bb3ab93..9ba9f4d9 100644 --- a/rustsat/src/encodings/card.rs +++ b/rustsat/src/encodings/card.rs @@ -356,7 +356,7 @@ pub fn encode_cardinality_constraint, Col: Col return; } if constr.is_clause() { - collector.extend([constr.as_clause().unwrap()]); + collector.extend([constr.into_clause().unwrap()]); return; } CE::encode_constr(constr, collector, var_manager).unwrap() diff --git a/rustsat/src/encodings/nodedb.rs b/rustsat/src/encodings/nodedb.rs index fba5bf17..6bd575e3 100644 --- a/rustsat/src/encodings/nodedb.rs +++ b/rustsat/src/encodings/nodedb.rs @@ -291,6 +291,7 @@ impl NodeCon { } /// Trait for a database managing [`NodeLike`]s by their [`NodeId`]s +#[allow(dead_code)] pub trait NodeById: IndexMut { /// The type of node in the database type Node: NodeLike; diff --git a/rustsat/src/encodings/pb.rs b/rustsat/src/encodings/pb.rs index f52b17b4..ca7557e5 100644 --- a/rustsat/src/encodings/pb.rs +++ b/rustsat/src/encodings/pb.rs @@ -405,11 +405,11 @@ pub fn encode_pb_constraint, Col: Co return; } if constr.is_clause() { - collector.extend([constr.as_clause().unwrap()]); + collector.extend([constr.into_clause().unwrap()]); return; } if constr.is_card() { - let card = constr.as_card_constr().unwrap(); + let card = constr.into_card_constr().unwrap(); return card::default_encode_cardinality_constraint(card, collector, var_manager); } PBE::encode_constr(constr, collector, var_manager).unwrap() diff --git a/rustsat/src/instances/fio.rs b/rustsat/src/instances/fio.rs index 3ee2cc9f..f258299f 100644 --- a/rustsat/src/instances/fio.rs +++ b/rustsat/src/instances/fio.rs @@ -17,29 +17,35 @@ pub struct ObjNoExist(usize); /// Opens a reader for the file at Path. /// With feature `compression` supports bzip2 and gzip compression. -pub(crate) fn open_compressed_uncompressed_read>( +pub fn open_compressed_uncompressed_read>( path: P, -) -> Result, io::Error> { +) -> Result, io::Error> { let path = path.as_ref(); let raw_reader = File::open(path)?; #[cfg(feature = "compression")] if let Some(ext) = path.extension() { if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("bz2")) { - return Ok(Box::new(bzip2::read::BzDecoder::new(raw_reader))); + return Ok(Box::new(io::BufReader::new(bzip2::read::BzDecoder::new( + raw_reader, + )))); } if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("gz")) { - return Ok(Box::new(flate2::read::GzDecoder::new(raw_reader))); + return Ok(Box::new(io::BufReader::new(flate2::read::GzDecoder::new( + raw_reader, + )))); } if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("xz")) { - return Ok(Box::new(xz2::read::XzDecoder::new(raw_reader))); + return Ok(Box::new(io::BufReader::new(xz2::read::XzDecoder::new( + raw_reader, + )))); } } - Ok(Box::new(raw_reader)) + Ok(Box::new(io::BufReader::new(raw_reader))) } /// Opens a writer for the file at Path. /// With feature `compression` supports bzip2 and gzip compression. -pub(crate) fn open_compressed_uncompressed_write>( +pub fn open_compressed_uncompressed_write>( path: P, ) -> Result, io::Error> { let path = path.as_ref(); diff --git a/rustsat/src/instances/fio/dimacs.rs b/rustsat/src/instances/fio/dimacs.rs index 76e9e92e..d121a7ed 100644 --- a/rustsat/src/instances/fio/dimacs.rs +++ b/rustsat/src/instances/fio/dimacs.rs @@ -12,7 +12,7 @@ use crate::{ instances::{Cnf, ManageVars, SatInstance}, - types::{Clause, Lit, Var}, + types::{Clause, Lit}, }; use anyhow::Context; use nom::{ @@ -27,7 +27,7 @@ use nom::{ }; use std::{ convert::TryFrom, - io::{self, BufRead, BufReader, Read, Write}, + io::{self, BufRead, Write}, }; use thiserror::Error; @@ -53,10 +53,9 @@ pub struct InvalidPLine(String); /// Parses a CNF instance from a reader (typically a (compressed) file) pub fn parse_cnf(reader: R) -> anyhow::Result> where - R: Read, + R: BufRead, VM: ManageVars + Default, { - let reader = BufReader::new(reader); let content = parse_dimacs(reader)?; #[cfg(not(feature = "optimization"))] { @@ -73,12 +72,11 @@ where /// (compressed) file). The objective with the index obj_idx is used. pub fn parse_wcnf_with_idx(reader: R, obj_idx: usize) -> anyhow::Result> where - R: Read, + R: BufRead, VM: ManageVars + Default, { use super::ObjNoExist; - let reader = BufReader::new(reader); let (constrs, mut objs) = parse_dimacs(reader)?; if objs.is_empty() { objs.push(Objective::default()); @@ -95,10 +93,9 @@ where /// Parses a MCNF instance (old or new format) from a reader (typically a (compressed) file) pub fn parse_mcnf(reader: R) -> anyhow::Result> where - R: Read, + R: BufRead, VM: ManageVars + Default, { - let reader = BufReader::new(reader); let (constrs, objs) = parse_dimacs(reader)?; Ok(MultiOptInstance::compose(constrs, objs)) } @@ -472,22 +469,12 @@ fn parse_clause_ending(input: &str) -> IResult<&str, &str> { /// Writes a CNF to a DIMACS CNF file pub fn write_cnf_annotated( writer: &mut W, - cnf: Cnf, - max_var: Option, + cnf: &Cnf, + n_vars: u32, ) -> Result<(), io::Error> { writeln!(writer, "c CNF file written by RustSAT")?; - writeln!( - writer, - "p cnf {} {}", - if let Some(max_var) = max_var { - max_var.pos_lit().to_ipasir() - } else { - 0 - }, - cnf.len() - )?; - cnf.into_iter() - .try_for_each(|cl| write_clause(writer, cl))?; + writeln!(writer, "p cnf {} {}", n_vars, cnf.len())?; + cnf.iter().try_for_each(|cl| write_clause(writer, cl))?; writer.flush() } @@ -506,7 +493,7 @@ pub fn write_cnf>( ) -> Result<(), io::Error> { data.try_for_each(|dat| match dat { CnfLine::Comment(c) => write!(writer, "c {}", c), - CnfLine::Clause(cl) => write_clause(writer, cl), + CnfLine::Clause(cl) => write_clause(writer, &cl), }) } @@ -514,26 +501,26 @@ pub fn write_cnf>( /// Writes a CNF and soft clauses to a (post 22, no p line) DIMACS WCNF file pub fn write_wcnf_annotated( writer: &mut W, - cnf: Cnf, + cnf: &Cnf, softs: (CI, isize), - max_var: Option, + n_vars: Option, ) -> Result<(), io::Error> { let (soft_cls, offset) = softs; let soft_cls: Vec<(Clause, usize)> = soft_cls.into_iter().collect(); writeln!(writer, "c WCNF file written by RustSAT")?; - if let Some(mv) = max_var { - writeln!(writer, "c highest var: {}", mv.pos_lit().to_ipasir())?; + if let Some(n_vars) = n_vars { + writeln!(writer, "c {} variables", n_vars)?; } writeln!(writer, "c {} hard clauses", cnf.len())?; writeln!(writer, "c {} soft clauses", soft_cls.len())?; writeln!(writer, "c objective offset: {}", offset)?; - cnf.into_iter().try_for_each(|cl| { + cnf.iter().try_for_each(|cl| { write!(writer, "h ")?; write_clause(writer, cl) })?; soft_cls.into_iter().try_for_each(|(cl, w)| { write!(writer, "{} ", w)?; - write_clause(writer, cl) + write_clause(writer, &cl) })?; writer.flush() } @@ -559,22 +546,22 @@ pub fn write_wcnf>( WcnfLine::Comment(c) => write!(writer, "c {}", c), WcnfLine::Hard(cl) => { write!(writer, "h ")?; - write_clause(writer, cl) + write_clause(writer, &cl) } WcnfLine::Soft(cl, w) => { write!(writer, "{} ", w)?; - write_clause(writer, cl) + write_clause(writer, &cl) } }) } #[cfg(feature = "multiopt")] /// Writes a CNF and multiple objectives as sets of soft clauses to a DIMACS MCNF file -pub fn write_mcnf_annotated( +pub fn write_mcnf_annotated, CI: WClsIter>( writer: &mut W, - cnf: Cnf, - softs: Vec<(CI, isize)>, - max_var: Option, + cnf: &Cnf, + softs: Iter, + n_vars: Option, ) -> Result<(), io::Error> { let (soft_cls, offsets) = softs.into_iter().unzip::<_, _, Vec<_>, Vec<_>>(); let soft_cls: Vec> = soft_cls @@ -582,8 +569,8 @@ pub fn write_mcnf_annotated( .map(|ci| ci.into_iter().collect()) .collect(); writeln!(writer, "c MCNF file written by RustSAT")?; - if let Some(mv) = max_var { - writeln!(writer, "c highest var: {}", mv.pos_lit().to_ipasir())?; + if let Some(n_vars) = n_vars { + writeln!(writer, "c {} variables", n_vars)?; } writeln!(writer, "c {} hard clauses", cnf.len())?; writeln!(writer, "c {} objectives", soft_cls.len())?; @@ -597,7 +584,7 @@ pub fn write_mcnf_annotated( .into_iter() .try_for_each(|o| write!(writer, "{} ", o))?; writeln!(writer, ")")?; - cnf.into_iter().try_for_each(|cl| { + cnf.iter().try_for_each(|cl| { write!(writer, "h ")?; write_clause(writer, cl) })?; @@ -607,7 +594,7 @@ pub fn write_mcnf_annotated( .try_for_each(|(idx, sft_cls)| { sft_cls.into_iter().try_for_each(|(cl, w)| { write!(writer, "o{} {} ", idx + 1, w)?; - write_clause(writer, cl) + write_clause(writer, &cl) }) })?; writer.flush() @@ -634,16 +621,16 @@ pub fn write_mcnf>( McnfLine::Comment(c) => writeln!(writer, "c {}", c), McnfLine::Hard(cl) => { write!(writer, "h ")?; - write_clause(writer, cl) + write_clause(writer, &cl) } McnfLine::Soft(cl, w, oidx) => { write!(writer, "o{} {} ", oidx + 1, w)?; - write_clause(writer, cl) + write_clause(writer, &cl) } }) } -fn write_clause(writer: &mut W, clause: Clause) -> Result<(), io::Error> { +fn write_clause(writer: &mut W, clause: &Clause) -> Result<(), io::Error> { clause .into_iter() .try_for_each(|l| write!(writer, "{} ", l.to_ipasir()))?; @@ -659,7 +646,7 @@ mod tests { use crate::{ clause, instances::{Cnf, SatInstance}, - ipasir_lit, var, + ipasir_lit, }; use nom::error::Error as NomError; use std::io::{Cursor, Seek}; @@ -1093,12 +1080,12 @@ mod tests { let mut cursor = Cursor::new(vec![]); - write_cnf_annotated(&mut cursor, true_cnf.clone(), Some(var![1])).unwrap(); + write_cnf_annotated(&mut cursor, &true_cnf, 2).unwrap(); cursor.rewind().unwrap(); let parsed_inst: SatInstance = super::parse_cnf(cursor).unwrap(); - let (parsed_cnf, _) = parsed_inst.as_cnf(); + let (parsed_cnf, _) = parsed_inst.into_cnf(); assert_eq!(parsed_cnf, true_cnf); } @@ -1110,14 +1097,15 @@ mod tests { let mut true_obj = Objective::new(); true_constrs.add_clause(clause![ipasir_lit![1], ipasir_lit![2]]); true_obj.add_soft_clause(10, clause![ipasir_lit![-3], ipasir_lit![4], ipasir_lit![5]]); + let offset = true_obj.offset(); let mut cursor = Cursor::new(vec![]); write_wcnf_annotated( &mut cursor, - true_constrs.clone().as_cnf().0, - true_obj.clone().as_soft_cls(), - Some(var![1]), + &true_constrs.cnf(), + (true_obj.iter_soft_cls(), offset), + Some(5), ) .unwrap(); @@ -1136,18 +1124,21 @@ mod tests { let mut true_obj1 = Objective::new(); true_constrs.add_clause(clause![ipasir_lit![1], ipasir_lit![2]]); true_obj0.add_soft_clause(3, clause![ipasir_lit![-1]]); + let offset0 = true_obj0.offset(); true_obj1.add_soft_clause(10, clause![ipasir_lit![-3], ipasir_lit![4], ipasir_lit![5]]); + let offset1 = true_obj1.offset(); let mut cursor = Cursor::new(vec![]); write_mcnf_annotated( &mut cursor, - true_constrs.clone().as_cnf().0, + &true_constrs.cnf(), vec![ - true_obj0.clone().as_soft_cls(), - true_obj1.clone().as_soft_cls(), - ], - Some(var![4]), + (true_obj0.iter_soft_cls(), offset0), + (true_obj1.iter_soft_cls(), offset1), + ] + .into_iter(), + Some(5), ) .unwrap(); diff --git a/rustsat/src/instances/fio/opb.rs b/rustsat/src/instances/fio/opb.rs index 8c1d941e..a2f78782 100644 --- a/rustsat/src/instances/fio/opb.rs +++ b/rustsat/src/instances/fio/opb.rs @@ -27,7 +27,7 @@ use nom::{ IResult, }; use std::{ - io::{self, BufRead, BufReader, Read, Write}, + io::{self, BufRead, Write}, num::TryFromIntError, }; @@ -92,7 +92,7 @@ enum OpbData { /// Parses the constraints from an OPB file as a [`SatInstance`] pub fn parse_sat(reader: R, opts: Options) -> anyhow::Result> where - R: Read, + R: BufRead, VM: ManageVars + Default, { let data = parse_opb_data(reader, opts)?; @@ -114,7 +114,7 @@ pub fn parse_opt_with_idx( opts: Options, ) -> anyhow::Result> where - R: Read, + R: BufRead, VM: ManageVars + Default, { use super::ObjNoExist; @@ -149,7 +149,7 @@ where /// index (starting from 0). pub fn parse_multi_opt(reader: R, opts: Options) -> anyhow::Result> where - R: Read, + R: BufRead, VM: ManageVars + Default, { let data = parse_opb_data(reader, opts)?; @@ -164,8 +164,7 @@ where } /// Parses all OPB data of a reader -fn parse_opb_data(reader: R, opts: Options) -> anyhow::Result> { - let mut reader = BufReader::new(reader); +fn parse_opb_data(mut reader: R, opts: Options) -> anyhow::Result> { let mut buf = String::new(); let mut data = vec![]; // TODO: consider not necessarily reading a full line @@ -350,7 +349,7 @@ fn opb_data(input: &str, opts: Options) -> IResult<&str, OpbData> { /// Writes a [`SatInstance`] to an OPB file pub fn write_sat( writer: &mut W, - inst: SatInstance, + inst: &SatInstance, opts: Options, ) -> Result<(), io::Error> where @@ -371,125 +370,103 @@ where writeln!(writer, "* {} cardinality constraints", inst.cards.len())?; writeln!(writer, "* {} pseudo-boolean constraints", inst.pbs.len())?; inst.cnf - .into_iter() + .iter() .try_for_each(|cl| write_clause(writer, cl, opts))?; inst.cards - .into_iter() + .iter() .try_for_each(|card| write_card(writer, card, opts))?; inst.pbs - .into_iter() + .iter() .try_for_each(|pb| write_pb(writer, pb, opts))?; writer.flush() } #[cfg(feature = "optimization")] -/// Writes an [`OptInstance`] to an OPB file -pub fn write_opt( +/// Writes an optimization instance to an OPB file +pub fn write_opt( writer: &mut W, - inst: OptInstance, + constrs: &SatInstance, + obj: (LI, isize), opts: Options, ) -> Result<(), io::Error> where W: Write, + LI: WLitIter, VM: ManageVars, { - let (constrs, obj) = inst.decompose(); - let cnf = constrs.cnf; - let cards = constrs.cards; - let pbs = constrs.pbs; - let mut vm = constrs.var_manager; - let (hardened, softs) = obj.as_soft_lits(&mut vm); + let cnf = &constrs.cnf; + let cards = &constrs.cards; + let pbs = &constrs.pbs; writeln!( writer, "* #variable = {} #constraint= {}", - vm.n_used(), + constrs.n_vars(), cnf.len() + cards.len() + pbs.len() )?; writeln!(writer, "* OPB file written by RustSAT")?; - if let Some(max_var) = vm.max_var() { + if let Some(max_var) = constrs.max_var() { writeln!(writer, "* maximum variable: {}", max_var)?; } writeln!(writer, "* {} original hard clauses", cnf.len())?; writeln!(writer, "* {} cardinality constraints", cards.len())?; writeln!(writer, "* {} pseudo-boolean constraints", pbs.len())?; - writeln!( - writer, - "* {} relaxed and hardened soft clauses", - hardened.len() - )?; - write_objective(writer, softs, opts)?; - hardened - .into_iter() - .try_for_each(|cl| write_clause(writer, cl, opts))?; - cnf.into_iter() + write_objective(writer, obj, opts)?; + cnf.iter() .try_for_each(|cl| write_clause(writer, cl, opts))?; cards - .into_iter() + .iter() .try_for_each(|card| write_card(writer, card, opts))?; - pbs.into_iter() - .try_for_each(|pb| write_pb(writer, pb, opts))?; + pbs.iter().try_for_each(|pb| write_pb(writer, pb, opts))?; writer.flush() } #[cfg(feature = "multiopt")] /// Writes a [`MultiOptInstance`] to an OPB file -pub fn write_multi_opt( +pub fn write_multi_opt( writer: &mut W, - inst: MultiOptInstance, + constrs: &SatInstance, + mut objs: Iter, opts: Options, ) -> Result<(), io::Error> where W: Write, VM: ManageVars, + Iter: Iterator, + LI: WLitIter, { - let (constrs, objs) = inst.decompose(); - let cnf = constrs.cnf; - let cards = constrs.cards; - let pbs = constrs.pbs; - let mut vm = constrs.var_manager; - let (hardened, objs) = objs - .into_iter() - .map(|o| o.as_soft_lits(&mut vm)) - .unzip::<_, _, Vec<_>, Vec<_>>(); + let cnf = &constrs.cnf; + let cards = &constrs.cards; + let pbs = &constrs.pbs; writeln!( writer, "* #variable = {} #constraint= {}", - vm.n_used(), + constrs.n_vars(), cnf.len() + cards.len() + pbs.len() )?; writeln!(writer, "* OPB file written by RustSAT")?; - if let Some(max_var) = vm.max_var() { + if let Some(max_var) = constrs.max_var() { writeln!(writer, "* maximum variable: {}", max_var)?; } writeln!(writer, "* {} original hard clauses", cnf.len())?; writeln!(writer, "* {} cardinality constraints", cards.len())?; writeln!(writer, "* {} pseudo-boolean constraints", pbs.len())?; write!(writer, "* ( ")?; - hardened - .iter() - .try_for_each(|h| write!(writer, "{} ", h.len()))?; writeln!(writer, ") relaxed and hardened soft clauses",)?; - objs.into_iter() - .try_for_each(|softs| write_objective(writer, softs, opts))?; - hardened.into_iter().try_for_each(|h| { - h.into_iter() - .try_for_each(|cl| write_clause(writer, cl, opts)) - })?; - cnf.into_iter() + objs.try_for_each(|softs| write_objective(writer, softs, opts))?; + cnf.iter() .try_for_each(|cl| write_clause(writer, cl, opts))?; cards - .into_iter() + .iter() .try_for_each(|card| write_card(writer, card, opts))?; - pbs.into_iter() - .try_for_each(|pb| write_pb(writer, pb, opts))?; + pbs.iter().try_for_each(|pb| write_pb(writer, pb, opts))?; writer.flush() } /// Writes a clause to an OPB file -fn write_clause(writer: &mut W, clause: Clause, opts: Options) -> Result<(), io::Error> { +fn write_clause(writer: &mut W, clause: &Clause, opts: Options) -> Result<(), io::Error> { if opts.no_negated_lits { let mut rhs: isize = 1; - clause.into_iter().try_for_each(|l| { + clause.iter().try_for_each(|l| { if l.is_pos() { write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx) } else { @@ -499,7 +476,7 @@ fn write_clause(writer: &mut W, clause: Clause, opts: Options) -> Resu })?; writeln!(writer, ">= {};", rhs) } else { - clause.into_iter().try_for_each(|l| { + clause.iter().try_for_each(|l| { if l.is_pos() { write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx) } else { @@ -513,123 +490,137 @@ fn write_clause(writer: &mut W, clause: Clause, opts: Options) -> Resu /// Writes a cardinality constraint to an OPB file fn write_card( writer: &mut W, - card: CardConstraint, + card: &CardConstraint, opts: Options, ) -> Result<(), io::Error> { + let mut iter_a; + let mut iter_b; + let neg_lit = |l: &Lit| !*l; if opts.no_negated_lits { - let (lits, bound, op) = match card { + let (lits, bound, op): (&mut dyn Iterator, _, _) = match card { CardConstraint::UB(constr) => { - let (lits, bound) = constr.decompose(); - let bound = lits.len() as isize - bound as isize; + let (lits, bound) = constr.decompose_ref(); + let bound = lits.len() as isize - *bound as isize; // Flip operator by negating literals - let lits: Vec = lits.into_iter().map(|l| !l).collect(); - (lits, bound, ">=") + iter_a = lits.iter().map(neg_lit); + (&mut iter_a, bound, ">=") } CardConstraint::LB(constr) => { - let (lits, bound) = constr.decompose(); - (lits, bound as isize, ">=") + let (lits, bound) = constr.decompose_ref(); + iter_b = lits.iter().copied(); + (&mut iter_b, *bound as isize, ">=") } CardConstraint::EQ(constr) => { - let (lits, bound) = constr.decompose(); - (lits, bound as isize, "=") + let (lits, bound) = constr.decompose_ref(); + iter_b = lits.iter().copied(); + (&mut iter_b, *bound as isize, "=") } }; let mut offset = 0; - lits.into_iter().try_for_each(|l| { + for l in lits { if l.is_pos() { - write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx) + write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx)?; } else { offset += 1; - write!(writer, "-1 x{} ", l.vidx32() + opts.first_var_idx) + write!(writer, "-1 x{} ", l.vidx32() + opts.first_var_idx)?; } - })?; + } writeln!(writer, "{} {};", op, bound - offset) } else { - let (lits, bound, op) = match card { + let (lits, bound, op): (&mut dyn Iterator, _, _) = match card { CardConstraint::UB(constr) => { - let (lits, bound) = constr.decompose(); - let bound = lits.len() as isize - bound as isize; + let (lits, bound) = constr.decompose_ref(); + let bound = lits.len() as isize - *bound as isize; // Flip operator by negating literals - let lits: Vec = lits.into_iter().map(|l| !l).collect(); - (lits, bound, ">=") + iter_a = lits.iter().map(neg_lit); + (&mut iter_a, bound, ">=") } CardConstraint::LB(constr) => { - let (lits, bound) = constr.decompose(); - (lits, bound as isize, ">=") + let (lits, bound) = constr.decompose_ref(); + iter_b = lits.iter().copied(); + (&mut iter_b, *bound as isize, ">=") } CardConstraint::EQ(constr) => { - let (lits, bound) = constr.decompose(); - (lits, bound as isize, "=") + let (lits, bound) = constr.decompose_ref(); + iter_b = lits.iter().copied(); + (&mut iter_b, *bound as isize, "=") } }; - lits.into_iter().try_for_each(|l| { + for l in lits { if l.is_pos() { - write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx) + write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx)?; } else { - write!(writer, "1 ~x{} ", l.vidx32() + opts.first_var_idx) + write!(writer, "1 ~x{} ", l.vidx32() + opts.first_var_idx)?; } - })?; + } writeln!(writer, "{} {};", op, bound) } } /// Writes a pseudo-boolean constraint to an OPB file -fn write_pb(writer: &mut W, pb: PBConstraint, opts: Options) -> Result<(), io::Error> { +fn write_pb(writer: &mut W, pb: &PBConstraint, opts: Options) -> Result<(), io::Error> { + let mut iter_a; + let mut iter_b; + let neg_lit = |(l, w): &(Lit, usize)| (!*l, *w); if opts.no_negated_lits { - let (lits, bound, op) = match pb { + let (lits, bound, op): (&mut dyn Iterator, _, _) = match pb { PBConstraint::UB(constr) => { - let (lits, bound) = constr.decompose(); + let (lits, bound) = constr.decompose_ref(); let weight_sum = lits.iter().fold(0, |sum, (_, w)| sum + w); // Flip operator by negating literals - let lits = lits.into_iter().map(|(l, w)| (!l, w)).collect(); - (lits, weight_sum as isize - bound, ">=") + iter_a = lits.iter().map(neg_lit); + (&mut iter_a, weight_sum as isize - bound, ">=") } PBConstraint::LB(constr) => { - let (lits, bound) = constr.decompose(); - (lits, bound, ">=") + let (lits, bound) = constr.decompose_ref(); + iter_b = lits.iter().copied(); + (&mut iter_b, *bound, ">=") } PBConstraint::EQ(constr) => { - let (lits, bound) = constr.decompose(); - (lits, bound, "=") + let (lits, bound) = constr.decompose_ref(); + iter_b = lits.iter().copied(); + (&mut iter_b, *bound, "=") } }; let mut offset: isize = 0; - lits.into_iter().try_for_each(|(l, w)| { + for (l, w) in lits { if l.is_pos() { - write!(writer, "{} x{} ", w, l.vidx32() + opts.first_var_idx) + write!(writer, "{} x{} ", w, l.vidx32() + opts.first_var_idx)?; } else { // TODO: consider returning error for usize -> isize cast let w = w as isize; offset += w; - write!(writer, "{} x{} ", -w, l.vidx32() + opts.first_var_idx) + write!(writer, "{} x{} ", -w, l.vidx32() + opts.first_var_idx)?; } - })?; + } writeln!(writer, "{} {};", op, bound - offset) } else { - let (lits, bound, op) = match pb { + let (lits, bound, op): (&mut dyn Iterator, _, _) = match pb { PBConstraint::UB(constr) => { - let (lits, bound) = constr.decompose(); + let (lits, bound) = constr.decompose_ref(); let weight_sum = lits.iter().fold(0, |sum, (_, w)| sum + w); // Flip operator by negating literals - let lits = lits.into_iter().map(|(l, w)| (!l, w)).collect(); - (lits, weight_sum as isize - bound, ">=") + iter_a = lits.iter().map(neg_lit); + (&mut iter_a, weight_sum as isize - bound, ">=") } PBConstraint::LB(constr) => { - let (lits, bound) = constr.decompose(); - (lits, bound, ">=") + let (lits, bound) = constr.decompose_ref(); + iter_b = lits.iter().copied(); + (&mut iter_b, *bound, ">=") } PBConstraint::EQ(constr) => { - let (lits, bound) = constr.decompose(); - (lits, bound, "=") + let (lits, bound) = constr.decompose_ref(); + iter_b = lits.iter().copied(); + (&mut iter_b, *bound, "=") } }; - lits.into_iter().try_for_each(|(l, w)| { + for (l, w) in lits { if l.is_pos() { - write!(writer, "{} x{} ", w, l.vidx32() + opts.first_var_idx) + write!(writer, "{} x{} ", w, l.vidx32() + opts.first_var_idx)?; } else { - write!(writer, "{} ~x{} ", w, l.vidx32() + opts.first_var_idx) + write!(writer, "{} ~x{} ", w, l.vidx32() + opts.first_var_idx)?; } - })?; + } writeln!(writer, "{} {};", op, bound) } } @@ -925,19 +916,19 @@ mod test { let mut cursor = Cursor::new(vec![]); - write_clause(&mut cursor, cl.clone(), Options::default()).unwrap(); + write_clause(&mut cursor, &cl, Options::default()).unwrap(); cursor.rewind().unwrap(); let (cnf, _) = super::parse_sat::<_, BasicVarManager>(cursor, Options::default()) .unwrap() - .as_cnf(); + .into_cnf(); assert_eq!(cnf.len(), 1); assert_eq!(cnf.into_iter().next().unwrap().normalize(), cl.normalize()); } - fn write_parse_inst_test(in_inst: SatInstance, true_inst: SatInstance, opts: Options) { + fn write_parse_inst_test(in_inst: &SatInstance, true_inst: SatInstance, opts: Options) { let mut cursor = Cursor::new(vec![]); write_sat(&mut cursor, in_inst, opts).unwrap(); @@ -946,8 +937,8 @@ mod test { let parsed_inst: SatInstance = super::parse_sat(cursor, opts).unwrap(); - let (parsed_cnf, parsed_vm) = parsed_inst.as_cnf(); - let (true_cnf, true_vm) = true_inst.as_cnf(); + let (parsed_cnf, parsed_vm) = parsed_inst.into_cnf(); + let (true_cnf, true_vm) = true_inst.into_cnf(); assert_eq!(parsed_vm, true_vm); assert_eq!(parsed_cnf.normalize(), true_cnf.normalize()); @@ -967,19 +958,19 @@ mod test { in_inst.add_card_constr(CardConstraint::new_ub(vec![!lit![3], lit![4], !lit![5]], 2)); let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_ub(lits.clone(), 2)); - write_parse_inst_test(in_inst, true_inst, Options::default()); + write_parse_inst_test(&in_inst, true_inst, Options::default()); let mut in_inst: SatInstance = SatInstance::new(); in_inst.add_card_constr(CardConstraint::new_eq(vec![!lit![3], lit![4], !lit![5]], 2)); let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_eq(lits.clone(), 2)); - write_parse_inst_test(in_inst, true_inst, Options::default()); + write_parse_inst_test(&in_inst, true_inst, Options::default()); let mut in_inst: SatInstance = SatInstance::new(); in_inst.add_card_constr(CardConstraint::new_lb(vec![!lit![3], lit![4], !lit![5]], 2)); let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_lb(lits.clone(), 2)); - write_parse_inst_test(in_inst, true_inst, Options::default()); + write_parse_inst_test(&in_inst, true_inst, Options::default()); } #[test] @@ -992,26 +983,28 @@ mod test { // constraint as well. let lits = vec![(!lit![3], 1), (lit![4], 1), (!lit![5], 1)]; - let mut alt_opb_opts = Options::default(); - alt_opb_opts.no_negated_lits = false; + let alt_opb_opts = Options { + no_negated_lits: false, + ..Default::default() + }; let mut in_inst: SatInstance = SatInstance::new(); in_inst.add_card_constr(CardConstraint::new_ub(vec![!lit![3], lit![4], !lit![5]], 2)); let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_ub(lits.clone(), 2)); - write_parse_inst_test(in_inst, true_inst, alt_opb_opts); + write_parse_inst_test(&in_inst, true_inst, alt_opb_opts); let mut in_inst: SatInstance = SatInstance::new(); in_inst.add_card_constr(CardConstraint::new_eq(vec![!lit![3], lit![4], !lit![5]], 2)); let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_eq(lits.clone(), 2)); - write_parse_inst_test(in_inst, true_inst, alt_opb_opts); + write_parse_inst_test(&in_inst, true_inst, alt_opb_opts); let mut in_inst: SatInstance = SatInstance::new(); in_inst.add_card_constr(CardConstraint::new_lb(vec![!lit![3], lit![4], !lit![5]], 2)); let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_lb(lits.clone(), 2)); - write_parse_inst_test(in_inst, true_inst, alt_opb_opts); + write_parse_inst_test(&in_inst, true_inst, alt_opb_opts); } #[test] @@ -1020,34 +1013,36 @@ mod test { let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_ub(lits.clone(), 2)); - write_parse_inst_test(true_inst.clone(), true_inst, Options::default()); + write_parse_inst_test(&true_inst, true_inst.clone(), Options::default()); let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_eq(lits.clone(), 2)); - write_parse_inst_test(true_inst.clone(), true_inst, Options::default()); + write_parse_inst_test(&true_inst, true_inst.clone(), Options::default()); let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_lb(lits.clone(), 2)); - write_parse_inst_test(true_inst.clone(), true_inst, Options::default()); + write_parse_inst_test(&true_inst, true_inst.clone(), Options::default()); } #[test] fn write_parse_pb_neg_lits() { let lits = vec![(!lit![6], 3), (!lit![7], -5), (lit![8], 2), (lit![9], -4)]; - let mut alt_opb_opts = Options::default(); - alt_opb_opts.no_negated_lits = false; + let alt_opb_opts = Options { + no_negated_lits: false, + ..Default::default() + }; let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_ub(lits.clone(), 2)); - write_parse_inst_test(true_inst.clone(), true_inst, alt_opb_opts); + write_parse_inst_test(&true_inst, true_inst.clone(), alt_opb_opts); let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_eq(lits.clone(), 2)); - write_parse_inst_test(true_inst.clone(), true_inst, alt_opb_opts); + write_parse_inst_test(&true_inst, true_inst.clone(), alt_opb_opts); let mut true_inst: SatInstance = SatInstance::new(); true_inst.add_pb_constr(PBConstraint::new_lb(lits.clone(), 2)); - write_parse_inst_test(true_inst.clone(), true_inst, alt_opb_opts); + write_parse_inst_test(&true_inst, true_inst.clone(), alt_opb_opts); } } diff --git a/rustsat/src/instances/multiopt.rs b/rustsat/src/instances/multiopt.rs index 53ed0aa3..4ebeb142 100644 --- a/rustsat/src/instances/multiopt.rs +++ b/rustsat/src/instances/multiopt.rs @@ -8,6 +8,7 @@ use crate::{ constraints::{CardConstraint, PBConstraint}, Assignment, Lit, Var, WClsIter, WLitIter, }, + RequiresClausal, RequiresSoftLits, }; use super::{ @@ -40,7 +41,7 @@ impl MultiOptInstance { pub fn compose(mut constraints: SatInstance, objectives: Vec) -> Self { objectives.iter().for_each(|o| { if let Some(mv) = o.max_var() { - constraints.var_manager().increase_next_free(mv + 1); + constraints.var_manager_mut().increase_next_free(mv + 1); } }); MultiOptInstance { @@ -67,35 +68,67 @@ impl MultiOptInstance { } /// Gets a mutable reference to the hard constraints for modifying them + #[deprecated( + since = "0.5.0", + note = "get_constraints has been renamed to constraints_mut and will be removed in a future release" + )] pub fn get_constraints(&mut self) -> &mut SatInstance { &mut self.constrs } + /// Gets a mutable reference to the hard constraints for modifying them + pub fn constraints_mut(&mut self) -> &mut SatInstance { + &mut self.constrs + } + + /// Gets a reference to the hard constraints + pub fn constraints_ref(&self) -> &SatInstance { + &self.constrs + } + /// Reserves a new variable in the internal variable manager. This is a /// shortcut for `inst.get_constraints().var_manager().new_var()`. pub fn new_var(&mut self) -> Var { - self.get_constraints().var_manager().new_var() + self.constraints_mut().var_manager_mut().new_var() } /// Reserves a new variable in the internal variable manager. This is a /// shortcut for `inst.get_constraints().var_manager().new_lit()`. pub fn new_lit(&mut self) -> Lit { - self.get_constraints().var_manager().new_lit() + self.constraints_mut().var_manager_mut().new_lit() } /// Gets the used variable with the highest index. This is a shortcut /// for `inst.get_constraints().var_manager().max_var()`. - pub fn max_var(&mut self) -> Option { - self.get_constraints().var_manager().max_var() + pub fn max_var(&self) -> Option { + self.constraints_ref().var_manager_ref().max_var() } /// Gets a mutable reference to the first objective for modifying it. /// Make sure `obj_idx` does not exceed the number of objectives in the instance. + #[deprecated( + since = "0.5.0", + note = "get_objective has been renamed to objective_mut and will be removed in a future release" + )] pub fn get_objective(&mut self, obj_idx: usize) -> &mut Objective { assert!(obj_idx < self.objs.len()); &mut self.objs[obj_idx] } + /// Gets a mutable reference to the objective with index `obj_idx` for modifying it. + /// Make sure `obj_idx` does not exceed the number of objectives in the instance. + pub fn objective_mut(&mut self, obj_idx: usize) -> &mut Objective { + assert!(obj_idx < self.objs.len()); + &mut self.objs[obj_idx] + } + + /// Gets a reference to the objective with index `obj_idx`. + /// Make sure `obj_idx` does not exceed the number of objectives in the instance. + pub fn objective_ref(&self, obj_idx: usize) -> &Objective { + assert!(obj_idx < self.objs.len()); + &self.objs[obj_idx] + } + /// Returns an iterator over references to the objectives pub fn iter_obj(&self) -> impl Iterator { self.objs.iter() @@ -107,8 +140,17 @@ impl MultiOptInstance { } /// Converts the instance to a set of hard and soft clauses + #[deprecated( + since = "0.5.0", + note = "as_hard_cls_soft_cls has been renamed to into_hard_cls_soft_cls and will be removed in a future release" + )] pub fn as_hard_cls_soft_cls(self) -> (Cnf, Vec<(impl WClsIter, isize)>, VM) { - let (cnf, mut vm) = self.constrs.as_cnf(); + self.into_hard_cls_soft_cls() + } + + /// Converts the instance to a set of hard and soft clauses + pub fn into_hard_cls_soft_cls(self) -> (Cnf, Vec<(impl WClsIter, isize)>, VM) { + let (cnf, mut vm) = self.constrs.into_cnf(); let omv = self.objs.iter().fold(Var::new(0), |v, o| { if let Some(mv) = o.max_var() { return std::cmp::max(v, mv); @@ -116,13 +158,22 @@ impl MultiOptInstance { v }); vm.increase_next_free(omv + 1); - let soft_cls = self.objs.into_iter().map(|o| o.as_soft_cls()).collect(); + let soft_cls = self.objs.into_iter().map(|o| o.into_soft_cls()).collect(); (cnf, soft_cls, vm) } /// Converts the instance to a set of hard clauses and soft literals + #[deprecated( + since = "0.5.0", + note = "as_hard_cls_soft_lits has been renamed to into_hard_cls_soft_lits and will be removed in a future release" + )] pub fn as_hard_cls_soft_lits(self) -> (Cnf, Vec<(impl WLitIter, isize)>, VM) { - let (mut cnf, mut vm) = self.constrs.as_cnf(); + self.into_hard_cls_soft_lits() + } + + /// Converts the instance to a set of hard clauses and soft literals + pub fn into_hard_cls_soft_lits(self) -> (Cnf, Vec<(impl WLitIter, isize)>, VM) { + let (mut cnf, mut vm) = self.constrs.into_cnf(); let omv = self.objs.iter().fold(Var::new(0), |v, o| { if let Some(mv) = o.max_var() { return std::cmp::max(v, mv); @@ -134,7 +185,7 @@ impl MultiOptInstance { .objs .into_iter() .map(|o| { - let (hards, softs) = o.as_soft_lits(&mut vm); + let (hards, softs) = o.into_soft_lits(&mut vm); cnf.extend(hards); softs }) @@ -182,13 +233,17 @@ impl MultiOptInstance { /// # Performance /// /// For performance, consider using a [`std::io::BufWriter`] instance. + #[deprecated(since = "0.5.0", note = "use write_dimacs_path instead")] pub fn to_dimacs_path>(self, path: P) -> Result<(), io::Error> { let mut writer = fio::open_compressed_uncompressed_write(path)?; + #[allow(deprecated)] self.to_dimacs(&mut writer) } /// Write to DIMACS MCNF + #[deprecated(since = "0.5.0", note = "use write_dimacs instead")] pub fn to_dimacs(self, writer: &mut W) -> Result<(), io::Error> { + #[allow(deprecated)] self.to_dimacs_with_encoders( card::default_encode_cardinality_constraint, pb::default_encode_pb_constraint, @@ -198,6 +253,10 @@ impl MultiOptInstance { /// Writes the instance to DIMACS MCNF converting non-clausal constraints /// with specific encoders. + #[deprecated( + since = "0.5.0", + note = "use convert_to_cnf_with_encoders and write_dimacs instead" + )] pub fn to_dimacs_with_encoders( self, card_encoder: CardEnc, @@ -209,9 +268,57 @@ impl MultiOptInstance { CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars), PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars), { - let (cnf, vm) = self.constrs.as_cnf_with_encoders(card_encoder, pb_encoder); - let soft_cls = self.objs.into_iter().map(|o| o.as_soft_cls()).collect(); - fio::dimacs::write_mcnf_annotated(writer, cnf, soft_cls, vm.max_var()) + let (cnf, vm) = self + .constrs + .into_cnf_with_encoders(card_encoder, pb_encoder); + let soft_cls = self.objs.into_iter().map(|o| o.into_soft_cls()); + fio::dimacs::write_mcnf_annotated(writer, &cnf, soft_cls, Some(vm.n_used())) + } + + /// Writes the instance to a DIMACS MCNF file at a path + /// + /// This requires that the instance is clausal, i.e., does not contain any non-converted + /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by + /// [`SatInstance::convert_to_cnf`] or [`SatInstance::convert_to_cnf_with_encoders`] first. + /// + /// # Errors + /// + /// - If the instance is not clausal, returns [`NonClausal`] + /// - Returns [`io::Error`] on errors during writing + pub fn write_dimacs_path>(&self, path: P) -> anyhow::Result<()> { + let mut writer = fio::open_compressed_uncompressed_write(path)?; + self.write_dimacs(&mut writer) + } + + /// Write to DIMACS MCNF + /// + /// This requires that the instance is clausal, i.e., does not contain any non-converted + /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by + /// [`SatInstance::convert_to_cnf`] or [`SatInstance::convert_to_cnf_with_encoders`] first. + /// + /// # Performance + /// + /// For performance, consider using a [`std::io::BufWriter`] instance. + /// + /// # Errors + /// + /// - If the instance is not clausal, returns [`NonClausal`] + /// - Returns [`io::Error`] on errors during writing + pub fn write_dimacs(&self, writer: &mut W) -> anyhow::Result<()> { + if self.constrs.n_cards() > 0 || self.constrs.n_pbs() > 0 { + return Err(RequiresClausal.into()); + } + let n_vars = self.constrs.n_vars(); + let iter = self.objs.iter().map(|o| { + let offset = o.offset(); + (o.iter_soft_cls(), offset) + }); + Ok(fio::dimacs::write_mcnf_annotated( + writer, + &self.constrs.cnf, + iter, + Some(n_vars), + )?) } /// Writes the instance to an OPB file at a path @@ -219,22 +326,87 @@ impl MultiOptInstance { /// # Performance /// /// For performance, consider using a [`std::io::BufWriter`] instance. + #[deprecated(since = "0.5.0", note = "use write_opb_path instead")] pub fn to_opb_path>( self, path: P, opts: fio::opb::Options, ) -> Result<(), io::Error> { let mut writer = fio::open_compressed_uncompressed_write(path)?; + #[allow(deprecated)] self.to_opb(&mut writer, opts) } /// Writes the instance to an OPB file + #[deprecated(since = "0.5.0", note = "use write_opb instead")] pub fn to_opb( - self, + mut self, writer: &mut W, opts: fio::opb::Options, ) -> Result<(), io::Error> { - fio::opb::write_multi_opt::(writer, self, opts) + for obj in &mut self.objs { + let vm = self.constrs.var_manager_mut(); + let hardened = obj.convert_to_soft_lits(vm); + self.constrs.cnf.extend(hardened); + } + let objs = self.objs.iter().map(|o| { + let offset = o.offset(); + (o.iter_soft_lits().unwrap(), offset) + }); + fio::opb::write_multi_opt::(writer, &self.constrs, objs, opts) + } + + /// Writes the instance to an OPB file at a path + /// + /// This requires that the objective does not contain soft clauses. If it does, use + /// [`Objective::convert_to_soft_lits`] first. + /// + /// # Errors + /// + /// - If the objective containes soft literals, returns [`RequiresSoftLits`] + /// - Returns [`io::Error`] on errors during writing + pub fn write_opb_path>( + &self, + path: P, + opts: fio::opb::Options, + ) -> anyhow::Result<()> { + let mut writer = fio::open_compressed_uncompressed_write(path)?; + self.write_opb(&mut writer, opts) + } + + /// Writes the instance to an OPB file + /// + /// This requires that the objective does not contain soft clauses. If it does, use + /// [`Objective::convert_to_soft_lits`] first. + /// + /// # Performance + /// + /// For performance, consider using a [`std::io::BufWriter`] instance(crate). + /// + /// # Errors + /// + /// - If the objective containes soft literals, returns [`RequiresSoftLits`] + /// - Returns [`io::Error`] on errors during writing + pub fn write_opb( + &self, + writer: &mut W, + opts: fio::opb::Options, + ) -> anyhow::Result<()> { + let objs: Result, RequiresSoftLits> = self + .objs + .iter() + .map(|o| { + let offset = o.offset(); + Ok((o.iter_soft_lits()?, offset)) + }) + .collect(); + let objs = objs?; + Ok(fio::opb::write_multi_opt::( + writer, + &self.constrs, + objs.into_iter(), + opts, + )?) } /// Calculates the objective values of an assignment. Returns [`None`] if the @@ -283,7 +455,7 @@ impl MultiOptInstance { /// positive number preceded by an 'o', indicating what objective this soft /// clause belongs to. After that, the format is identical to a soft clause /// in a WCNF file. - pub fn from_dimacs(reader: R) -> anyhow::Result { + pub fn from_dimacs(reader: R) -> anyhow::Result { fio::dimacs::parse_mcnf(reader) } @@ -302,7 +474,7 @@ impl MultiOptInstance { /// pseudo-boolean optimization instances with multiple objectives defined. /// For details on the file format see /// [here](https://www.cril.univ-artois.fr/PB12/format.pdf). - pub fn from_opb(reader: R, opts: fio::opb::Options) -> anyhow::Result { + pub fn from_opb(reader: R, opts: fio::opb::Options) -> anyhow::Result { fio::opb::parse_multi_opt(reader, opts) } @@ -321,12 +493,12 @@ impl FromIterator for MultiOptInstance { for line in iter { match line { McnfLine::Comment(_) => (), - McnfLine::Hard(cl) => inst.get_constraints().add_clause(cl), + McnfLine::Hard(cl) => inst.constraints_mut().add_clause(cl), McnfLine::Soft(cl, w, oidx) => { if oidx >= inst.objs.len() { inst.objs.resize(oidx + 1, Default::default()) } - inst.get_objective(oidx).add_soft_clause(w, cl); + inst.objective_mut(oidx).add_soft_clause(w, cl); } } } diff --git a/rustsat/src/instances/opt.rs b/rustsat/src/instances/opt.rs index 84bbd64c..9c6e6193 100644 --- a/rustsat/src/instances/opt.rs +++ b/rustsat/src/instances/opt.rs @@ -1,6 +1,6 @@ //! # Optimization Instance Representations -use std::{cmp, io, path::Path}; +use std::{cmp, collections::hash_map, io, path::Path, slice}; use crate::{ clause, @@ -9,6 +9,7 @@ use crate::{ constraints::{CardConstraint, PBConstraint}, Assignment, Clause, ClsIter, Lit, LitIter, RsHashMap, TernaryVal, Var, WClsIter, WLitIter, }, + RequiresClausal, RequiresSoftLits, }; /// Internal objective type for not exposing variants @@ -305,10 +306,10 @@ impl Objective { if let Some(unit_weight) = unit_weight { *self = IntObj::Weighted { offset: *offset, - soft_lits: soft_lits.iter_mut().map(|l| (*l, *unit_weight)).collect(), + soft_lits: soft_lits.drain(..).map(|l| (l, *unit_weight)).collect(), soft_clauses: soft_clauses - .iter_mut() - .map(|cl| (cl.clone(), *unit_weight)) + .drain(..) + .map(|cl| (cl, *unit_weight)) .collect(), } .into() @@ -335,12 +336,12 @@ impl Objective { } => { let mut soft_unit_lits = vec![]; soft_lits - .iter_mut() - .for_each(|(l, w)| soft_unit_lits.resize(soft_unit_lits.len() + *w, *l)); + .drain() + .for_each(|(l, w)| soft_unit_lits.resize(soft_unit_lits.len() + w, l)); let mut soft_unit_clauses = vec![]; - soft_clauses.iter_mut().for_each(|(cl, w)| { - soft_unit_clauses.resize(soft_unit_clauses.len() + *w, cl.clone()) - }); + soft_clauses + .drain() + .for_each(|(cl, w)| soft_unit_clauses.resize(soft_unit_clauses.len() + w, cl)); *self = IntObj::Unweighted { offset: *offset, unit_weight: Some(1), @@ -547,7 +548,16 @@ impl Objective { } /// Converts the objective to a set of soft clauses and an offset + #[deprecated( + since = "0.5.0", + note = "as_soft_cls has been renamed to into_soft_cls and will be removed in a future release" + )] pub fn as_soft_cls(self) -> (impl WClsIter, isize) { + self.into_soft_cls() + } + + /// Converts the objective to a set of soft clauses and an offset + pub fn into_soft_cls(self) -> (impl WClsIter, isize) { match self.0 { IntObj::Unweighted { mut soft_clauses, @@ -583,7 +593,18 @@ impl Objective { /// Converts the objective to unweighted soft clauses, a unit weight and an offset. If the /// objective is weighted, the soft clause will appear as often as its /// weight in the output vector. - pub fn as_unweighted_soft_cls(mut self) -> (impl ClsIter, usize, isize) { + #[deprecated( + since = "0.5.0", + note = "as_unweighted_soft_cls has been renamed to into_unweighted_soft_cls and will be removed in a future release" + )] + pub fn as_unweighted_soft_cls(self) -> (impl ClsIter, usize, isize) { + self.into_unweighted_soft_cls() + } + + /// Converts the objective to unweighted soft clauses, a unit weight and an offset. If the + /// objective is weighted, the soft clause will appear as often as its + /// weight in the output vector. + pub fn into_unweighted_soft_cls(mut self) -> (impl ClsIter, usize, isize) { self.weighted_2_unweighted(); match self.0 { IntObj::Weighted { .. } => panic!(), @@ -606,33 +627,79 @@ impl Objective { } } + /// Converts the objective to soft literals in place, returning hardened clauses produced in + /// the conversion. + /// + /// See [`Self::into_soft_lits`] if you do not need to convert in place. + pub fn convert_to_soft_lits(&mut self, var_manager: &mut VM) -> Cnf + where + VM: ManageVars, + { + let mut cnf = Cnf::new(); + match &mut self.0 { + IntObj::Weighted { + soft_lits, + soft_clauses, + .. + } => { + cnf.clauses.reserve(soft_clauses.len()); + soft_lits.reserve(soft_clauses.len()); + for (mut cl, w) in soft_clauses.drain() { + debug_assert!(cl.len() > 1); + let relax_lit = var_manager.new_var().pos_lit(); + cl.add(relax_lit); + cnf.add_clause(cl); + soft_lits.insert(relax_lit, w); + } + } + IntObj::Unweighted { + soft_lits, + soft_clauses, + .. + } => { + cnf.clauses.reserve(soft_clauses.len()); + soft_lits.reserve(soft_clauses.len()); + for mut cl in soft_clauses.drain(..) { + debug_assert!(cl.len() > 1); + let relax_lit = var_manager.new_var().pos_lit(); + cl.add(relax_lit); + cnf.add_clause(cl); + soft_lits.push(relax_lit); + } + } + } + cnf + } + /// Converts the objective to a set of hard clauses, soft literals and an offset - pub fn as_soft_lits(mut self, var_manager: &mut VM) -> (Cnf, (impl WLitIter, isize)) + #[deprecated( + since = "0.5.0", + note = "as_soft_lits has been renamed to into_soft_lits and will be removed in a future release" + )] + pub fn as_soft_lits(self, var_manager: &mut VM) -> (Cnf, (impl WLitIter, isize)) where VM: ManageVars, { + self.into_soft_lits(var_manager) + } + + /// Converts the objective to a set of hard clauses, soft literals and an offset + /// + /// See [`Self::convert_to_soft_lits`] for converting in place + pub fn into_soft_lits(mut self, var_manager: &mut VM) -> (Cnf, (impl WLitIter, isize)) + where + VM: ManageVars, + { + let cnf = self.convert_to_soft_lits(var_manager); self.unweighted_2_weighted(); match self.0 { - IntObj::Unweighted { .. } => panic!(), + IntObj::Unweighted { .. } => unreachable!(), IntObj::Weighted { - mut soft_lits, + soft_lits, soft_clauses, offset, } => { - let mut cnf = Cnf::new(); - cnf.clauses.reserve(soft_clauses.len()); - soft_lits.reserve(soft_clauses.len()); - for (mut cl, w) in soft_clauses { - if cl.len() > 1 { - let relax_lit = var_manager.new_var().pos_lit(); - cl.add(relax_lit); - cnf.add_clause(cl); - soft_lits.insert(relax_lit, w); - } else { - assert!(cl.len() == 1); - soft_lits.insert(!cl[0], w); - } - } + debug_assert!(soft_clauses.is_empty()); (cnf, (soft_lits, offset)) } } @@ -641,6 +708,10 @@ impl Objective { /// Converts the objective to hard clauses, unweighted soft literals, a unit /// weight and an offset. If the objective is weighted, the soft literals /// will appear as often as its weight in the output vector. + #[deprecated( + since = "0.5.0", + note = "as_unweighted_soft_lits has been renamed to into_unweighted_soft_lits and will be removed in a future release" + )] pub fn as_unweighted_soft_lits( self, var_manager: &mut VM, @@ -648,37 +719,41 @@ impl Objective { where VM: ManageVars, { + self.into_unweighted_soft_lits(var_manager) + } + + /// Converts the objective to hard clauses, unweighted soft literals, a unit + /// weight and an offset. If the objective is weighted, the soft literals + /// will appear as often as its weight in the output vector. + pub fn into_unweighted_soft_lits( + mut self, + var_manager: &mut VM, + ) -> (Cnf, impl LitIter, usize, isize) + where + VM: ManageVars, + { + let cnf = self.convert_to_soft_lits(var_manager); match self.0 { - IntObj::Weighted { .. } => { - let (cnf, softs) = self.as_soft_lits(var_manager); + IntObj::Weighted { + soft_lits, + soft_clauses, + offset, + } => { + debug_assert!(soft_clauses.is_empty()); let mut soft_unit_lits = vec![]; - softs - .0 + soft_lits .into_iter() .for_each(|(l, w)| soft_unit_lits.resize(soft_unit_lits.len() + w, l)); - (cnf, soft_unit_lits, 1, softs.1) + (cnf, soft_unit_lits, 1, offset) } IntObj::Unweighted { offset, unit_weight, - mut soft_lits, + soft_lits, soft_clauses, } => { + debug_assert!(soft_clauses.is_empty()); if let Some(unit_weight) = unit_weight { - let mut cnf = Cnf::new(); - cnf.clauses.reserve(soft_clauses.len()); - soft_lits.reserve(soft_clauses.len()); - for mut cl in soft_clauses { - if cl.len() > 1 { - let relax_lit = var_manager.new_var().pos_lit(); - cl.add(relax_lit); - cnf.add_clause(cl); - soft_lits.push(relax_lit); - } else { - assert!(cl.len() == 1); - soft_lits.push(!cl[0]); - } - } (cnf, soft_lits, unit_weight, offset) } else { (Cnf::new(), vec![], 1, offset) @@ -813,6 +888,94 @@ impl Objective { }; self } + + /// Gets a weighted literal iterator over only the soft literals + /// + /// # Errors + /// + /// If the objective contains soft clauses that this iterator would miss, returns + /// [`RequiresSoftLits`] + pub fn iter_soft_lits(&self) -> Result { + if self.n_clauses() > 0 { + return Err(RequiresSoftLits); + } + Ok(match &self.0 { + IntObj::Weighted { soft_lits, .. } => ObjSoftLitIter::Weighted(soft_lits.iter()), + IntObj::Unweighted { + soft_lits, + unit_weight, + .. + } => ObjSoftLitIter::Unweighted(soft_lits.iter(), unit_weight.unwrap_or(0)), + }) + } + + /// Gets an iterator over the entire objective as soft clauses + pub fn iter_soft_cls(&self) -> impl WClsIter + '_ { + match &self.0 { + IntObj::Weighted { + soft_lits, + soft_clauses, + .. + } => ObjSoftClauseIter::Weighted(soft_lits.iter(), soft_clauses.iter()), + IntObj::Unweighted { + unit_weight, + soft_lits, + soft_clauses, + .. + } => ObjSoftClauseIter::Unweighted( + soft_lits.iter(), + soft_clauses.iter(), + unit_weight.unwrap_or(0), + ), + } + } +} + +/// A wrapper type for iterators over soft literals in an objective +enum ObjSoftLitIter<'a> { + Weighted(hash_map::Iter<'a, Lit, usize>), + Unweighted(slice::Iter<'a, Lit>, usize), +} + +impl Iterator for ObjSoftLitIter<'_> { + type Item = (Lit, usize); + + fn next(&mut self) -> Option { + match self { + ObjSoftLitIter::Weighted(iter) => iter.next().map(|(&l, &w)| (l, w)), + ObjSoftLitIter::Unweighted(iter, w) => iter.next().map(|&l| (l, *w)), + } + } +} + +/// A wrapper type for iterators over soft clauses in an objective +enum ObjSoftClauseIter<'a> { + Weighted( + hash_map::Iter<'a, Lit, usize>, + hash_map::Iter<'a, Clause, usize>, + ), + Unweighted(slice::Iter<'a, Lit>, slice::Iter<'a, Clause>, usize), +} + +impl Iterator for ObjSoftClauseIter<'_> { + type Item = (Clause, usize); + + fn next(&mut self) -> Option { + match self { + ObjSoftClauseIter::Weighted(lit_iter, cl_iter) => { + if let Some((&l, &w)) = lit_iter.next() { + return Some((clause![!l], w)); + } + cl_iter.next().map(|(cl, &w)| (cl.clone(), w)) + } + ObjSoftClauseIter::Unweighted(lit_iter, cl_iter, w) => { + if let Some(&l) = lit_iter.next() { + return Some((clause![!l], *w)); + } + cl_iter.next().map(|cl| (cl.clone(), *w)) + } + } + } } impl FromIterator<(Lit, usize)> for Objective { @@ -865,7 +1028,7 @@ impl OptInstance { /// Creates a new optimization instance from constraints and an objective pub fn compose(mut constraints: SatInstance, objective: Objective) -> Self { if let Some(mv) = objective.max_var() { - constraints.var_manager().increase_next_free(mv); + constraints.var_manager_mut().increase_next_free(mv); } OptInstance { constrs: constraints, @@ -876,57 +1039,85 @@ impl OptInstance { /// Decomposes the optimization instance to a [`SatInstance`] and an [`Objective`] pub fn decompose(mut self) -> (SatInstance, Objective) { if let Some(mv) = self.obj.max_var() { - self.constrs.var_manager.increase_next_free(mv + 1); + self.constrs.var_manager_mut().increase_next_free(mv + 1); } (self.constrs, self.obj) } /// Gets a mutable reference to the hard constraints for modifying them + #[deprecated( + since = "0.5.0", + note = "get_constraints has been renamed to constraints_mut and will be removed in a future release" + )] pub fn get_constraints(&mut self) -> &mut SatInstance { &mut self.constrs } + /// Gets a mutable reference to the hard constraints for modifying them + pub fn constraints_mut(&mut self) -> &mut SatInstance { + &mut self.constrs + } + + /// Gets a reference to the hard constraints + pub fn constraints_ref(&self) -> &SatInstance { + &self.constrs + } + /// Gets a mutable reference to the objective for modifying it + #[deprecated( + since = "0.5.0", + note = "get_objective has been renamed to objective_mut and will be removed in a future release" + )] pub fn get_objective(&mut self) -> &mut Objective { &mut self.obj } + /// Gets a mutable reference to the objective for modifying it + pub fn objective_mut(&mut self) -> &mut Objective { + &mut self.obj + } + + /// Gets a reference to the objective + pub fn objective_ref(&self) -> &Objective { + &self.obj + } + /// Reserves a new variable in the internal variable manager. This is a /// shortcut for `inst.get_constraints().var_manager().new_var()`. pub fn new_var(&mut self) -> Var { - self.get_constraints().var_manager().new_var() + self.constraints_mut().var_manager_mut().new_var() } /// Reserves a new variable in the internal variable manager. This is a /// shortcut for `inst.get_constraints().var_manager().new_lit()`. pub fn new_lit(&mut self) -> Lit { - self.get_constraints().var_manager().new_lit() + self.constraints_mut().var_manager_mut().new_lit() } /// Gets the used variable with the highest index. This is a shortcut /// for `inst.get_constraints().var_manager().max_var()`. - pub fn max_var(&mut self) -> Option { - self.get_constraints().var_manager().max_var() + pub fn max_var(&self) -> Option { + self.constraints_ref().var_manager_ref().max_var() } /// Converts the instance to a set of hard and soft clauses, an objective /// offset and a variable manager - pub fn as_hard_cls_soft_cls(self) -> (Cnf, (impl WClsIter, isize), VM) { - let (cnf, mut vm) = self.constrs.as_cnf(); + pub fn into_hard_cls_soft_cls(self) -> (Cnf, (impl WClsIter, isize), VM) { + let (cnf, mut vm) = self.constrs.into_cnf(); if let Some(mv) = self.obj.max_var() { vm.increase_next_free(mv + 1); } - (cnf, self.obj.as_soft_cls(), vm) + (cnf, self.obj.into_soft_cls(), vm) } /// Converts the instance to a set of hard clauses and soft literals, an /// objective offset and a variable manager - pub fn as_hard_cls_soft_lits(self) -> (Cnf, (impl WLitIter, isize), VM) { - let (mut cnf, mut vm) = self.constrs.as_cnf(); + pub fn into_hard_cls_soft_lits(self) -> (Cnf, (impl WLitIter, isize), VM) { + let (mut cnf, mut vm) = self.constrs.into_cnf(); if let Some(mv) = self.obj.max_var() { vm.increase_next_free(mv + 1); } - let (hard_softs, softs) = self.obj.as_soft_lits(&mut vm); + let (hard_softs, softs) = self.obj.into_soft_lits(&mut vm); cnf.extend(hard_softs); (cnf, softs, vm) } @@ -967,13 +1158,17 @@ impl OptInstance { /// # Performance /// /// For performance, consider using a [`std::io::BufWriter`] instance. + #[deprecated(since = "0.5.0", note = "use write_dimacs_path instead")] pub fn to_dimacs_path>(self, path: P) -> Result<(), io::Error> { let mut writer = fio::open_compressed_uncompressed_write(path)?; + #[allow(deprecated)] self.to_dimacs(&mut writer) } /// Write to DIMACS WCNF (post 22) + #[deprecated(since = "0.5.0", note = "use write_dimacs instead")] pub fn to_dimacs(self, writer: &mut W) -> Result<(), io::Error> { + #[allow(deprecated)] self.to_dimacs_with_encoders( card::default_encode_cardinality_constraint, pb::default_encode_pb_constraint, @@ -983,6 +1178,10 @@ impl OptInstance { /// Writes the instance to DIMACS WCNF (post 22) converting non-clausal /// constraints with specific encoders. + #[deprecated( + since = "0.5.0", + note = "use convert_to_cnf_with_encoders and write_dimacs instead" + )] pub fn to_dimacs_with_encoders( self, card_encoder: CardEnc, @@ -994,9 +1193,55 @@ impl OptInstance { CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars), PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars), { - let (cnf, vm) = self.constrs.as_cnf_with_encoders(card_encoder, pb_encoder); - let soft_cls = self.obj.as_soft_cls(); - fio::dimacs::write_wcnf_annotated(writer, cnf, soft_cls, vm.max_var()) + let (cnf, vm) = self + .constrs + .into_cnf_with_encoders(card_encoder, pb_encoder); + let soft_cls = self.obj.into_soft_cls(); + fio::dimacs::write_wcnf_annotated(writer, &cnf, soft_cls, Some(vm.n_used())) + } + + /// Writes the instance to a DIMACS WCNF file at a path + /// + /// This requires that the instance is clausal, i.e., does not contain any non-converted + /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by + /// [`SatInstance::convert_to_cnf`] or [`SatInstance::convert_to_cnf_with_encoders`] first. + /// + /// # Errors + /// + /// - If the instance is not clausal, returns [`NonClausal`] + /// - Returns [`io::Error`] on errors during writing + pub fn write_dimacs_path>(&self, path: P) -> anyhow::Result<()> { + let mut writer = fio::open_compressed_uncompressed_write(path)?; + self.write_dimacs(&mut writer) + } + + /// Write to DIMACS WCNF (post 22) + /// + /// This requires that the instance is clausal, i.e., does not contain any non-converted + /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by + /// [`SatInstance::convert_to_cnf`] or [`SatInstance::convert_to_cnf_with_encoders`] first. + /// + /// # Performance + /// + /// For performance, consider using a [`std::io::BufWriter`] instance. + /// + /// # Errors + /// + /// - If the instance is not clausal, returns [`NonClausal`] + /// - Returns [`io::Error`] on errors during writing + pub fn write_dimacs(&self, writer: &mut W) -> anyhow::Result<()> { + if self.constrs.n_cards() > 0 || self.constrs.n_pbs() > 0 { + return Err(RequiresClausal.into()); + } + let n_vars = self.constrs.n_vars(); + let offset = self.obj.offset(); + let soft_cls = self.obj.iter_soft_cls(); + Ok(fio::dimacs::write_wcnf_annotated( + writer, + &self.constrs.cnf, + (soft_cls, offset), + Some(n_vars), + )?) } /// Writes the instance to an OPB file at a path @@ -1004,22 +1249,75 @@ impl OptInstance { /// # Performance /// /// For performance, consider using a [`std::io::BufWriter`] instance. + #[deprecated(since = "0.5.0", note = "use write_opb_path instead")] pub fn to_opb_path>( self, path: P, opts: fio::opb::Options, ) -> Result<(), io::Error> { let mut writer = fio::open_compressed_uncompressed_write(path)?; + #[allow(deprecated)] self.to_opb(&mut writer, opts) } /// Writes the instance to an OPB file + #[deprecated(since = "0.5.0", note = "use write_opb instead")] pub fn to_opb( - self, + mut self, writer: &mut W, opts: fio::opb::Options, ) -> Result<(), io::Error> { - fio::opb::write_opt::(writer, self, opts) + let var_manager = self.constrs.var_manager_mut(); + self.obj.convert_to_soft_lits(var_manager); + let offset = self.obj.offset(); + let iter = self.obj.iter_soft_lits().unwrap(); + fio::opb::write_opt::(writer, &self.constrs, (iter, offset), opts) + } + + /// Writes the instance to an OPB file at a path + /// + /// This requires that the objective does not contain soft clauses. If it does, use + /// [`Objective::convert_to_soft_lits`] first. + /// + /// # Errors + /// + /// - If the objective containes soft literals, returns [`RequiresSoftLits`] + /// - Returns [`io::Error`] on errors during writing + pub fn write_opb_path>( + &self, + path: P, + opts: fio::opb::Options, + ) -> anyhow::Result<()> { + let mut writer = fio::open_compressed_uncompressed_write(path)?; + self.write_opb(&mut writer, opts) + } + + /// Writes the instance to an OPB file + /// + /// This requires that the objective does not contain soft clauses. If it does, use + /// [`Objective::convert_to_soft_lits`] first. + /// + /// # Performance + /// + /// For performance, consider using a [`std::io::BufWriter`] instance(crate). + /// + /// # Errors + /// + /// - If the objective containes soft literals, returns [`RequiresSoftLits`] + /// - Returns [`io::Error`] on errors during writing + pub fn write_opb( + &self, + writer: &mut W, + opts: fio::opb::Options, + ) -> anyhow::Result<()> { + let offset = self.obj.offset(); + let iter = self.obj.iter_soft_lits()?; + Ok(fio::opb::write_opt::( + writer, + &self.constrs, + (iter, offset), + opts, + )?) } /// Calculates the objective value of an assignment. Returns [`None`] if the @@ -1053,14 +1351,14 @@ impl OptInstance { /// /// If a DIMACS MCNF file is passed to this function, all objectives but the /// first are ignored. - pub fn from_dimacs(reader: R) -> anyhow::Result { + pub fn from_dimacs(reader: R) -> anyhow::Result { Self::from_dimacs_with_idx(reader, 0) } /// Parses a DIMACS instance from a reader object, selecting the objective /// with index `obj_idx` if multiple are available. The index starts at 0. /// For more details see [`OptInstance::from_dimacs`]. - pub fn from_dimacs_with_idx(reader: R, obj_idx: usize) -> anyhow::Result { + pub fn from_dimacs_with_idx(reader: R, obj_idx: usize) -> anyhow::Result { fio::dimacs::parse_wcnf_with_idx(reader, obj_idx) } @@ -1090,14 +1388,14 @@ impl OptInstance { /// The file format expected by this parser is the OPB format for /// pseudo-boolean optimization instances. For details on the file format /// see [here](https://www.cril.univ-artois.fr/PB12/format.pdf). - pub fn from_opb(reader: R, opts: fio::opb::Options) -> anyhow::Result { + pub fn from_opb(reader: R, opts: fio::opb::Options) -> anyhow::Result { Self::from_opb_with_idx(reader, 0, opts) } /// Parses an OPB instance from a reader object, selecting the objective /// with index `obj_idx` if multiple are available. The index starts at 0. /// For more details see [`OptInstance::from_opb`]. - pub fn from_opb_with_idx( + pub fn from_opb_with_idx( reader: R, obj_idx: usize, opts: fio::opb::Options, @@ -1134,9 +1432,9 @@ impl FromIterator for OptInstance { for line in iter { match line { WcnfLine::Comment(_) => (), - WcnfLine::Hard(cl) => inst.get_constraints().add_clause(cl), + WcnfLine::Hard(cl) => inst.constraints_mut().add_clause(cl), WcnfLine::Soft(cl, w) => { - inst.get_objective().add_soft_clause(w, cl); + inst.objective_mut().add_soft_clause(w, cl); } } } diff --git a/rustsat/src/instances/sat.rs b/rustsat/src/instances/sat.rs index 69e77524..287cc81d 100644 --- a/rustsat/src/instances/sat.rs +++ b/rustsat/src/instances/sat.rs @@ -10,6 +10,7 @@ use crate::{ constraints::{CardConstraint, PBConstraint}, Assignment, Clause, Lit, Var, }, + RequiresClausal, }; use anyhow::Context; @@ -77,6 +78,11 @@ impl Cnf { self.clauses.len() } + /// Adds a clause from a slice of literals + pub fn add_nary(&mut self, lits: &[Lit]) { + self.add_clause(lits.into()) + } + /// See [`atomics::lit_impl_lit`] pub fn add_lit_impl_lit(&mut self, a: Lit, b: Lit) { self.add_clause(atomics::lit_impl_lit(a, b)) @@ -190,6 +196,21 @@ impl Cnf { pub fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) { self.add_clause(clause![lit1, lit2, lit3]) } + + /// Writes the CNF to a DIMACS CNF file at a path + pub fn write_dimacs_path>(&self, path: P, n_vars: u32) -> Result<(), io::Error> { + let mut writer = fio::open_compressed_uncompressed_write(path)?; + self.write_dimacs(&mut writer, n_vars) + } + + /// Writes the CNF to DIMACS CNF + /// + /// # Performance + /// + /// For performance, consider using a [`std::io::BufWriter`] instance. + pub fn write_dimacs(&self, writer: &mut W, n_vars: u32) -> Result<(), io::Error> { + fio::dimacs::write_cnf_annotated(writer, self, n_vars) + } } impl CollectClauses for Cnf { @@ -283,6 +304,11 @@ impl SatInstance { self.cnf.add_clause(cl); } + /// Adds a clause from a slice of literals + pub fn add_nary(&mut self, lits: &[Lit]) { + self.add_clause(lits.into()) + } + /// Adds a unit clause to the instance pub fn add_unit(&mut self, unit: Lit) { self.add_clause(clause![unit]) @@ -401,27 +427,51 @@ impl SatInstance { self.pbs.push(pb) } + /// Gets a reference to the internal CNF + pub fn cnf(&self) -> &Cnf { + &self.cnf + } + /// Gets a reference to the variable manager + #[deprecated( + since = "0.5.0", + note = "var_manager has been renamed to var_manager_mut and will be removed in a future release" + )] pub fn var_manager(&mut self) -> &mut VM { &mut self.var_manager } + /// Gets a mutable reference to the variable manager + pub fn var_manager_mut(&mut self) -> &mut VM { + &mut self.var_manager + } + + /// Gets a reference to the variable manager + pub fn var_manager_ref(&self) -> &VM { + &self.var_manager + } + /// Reserves a new variable in the internal variable manager. This is a /// shortcut for `inst.var_manager().new_var()`. pub fn new_var(&mut self) -> Var { - self.var_manager().new_var() + self.var_manager_mut().new_var() } /// Reserves a new variable in the internal variable manager. This is a /// shortcut for `inst.var_manager().new_lit()`. pub fn new_lit(&mut self) -> Lit { - self.var_manager().new_lit() + self.var_manager_mut().new_lit() } /// Gets the used variable with the highest index. This is a shortcut /// for `inst.var_manager().max_var()`. - pub fn max_var(&mut self) -> Option { - self.var_manager().max_var() + pub fn max_var(&self) -> Option { + self.var_manager_ref().max_var() + } + + /// Returns the number of variables in the variable manager of the instance + pub fn n_vars(&self) -> u32 { + self.var_manager_ref().n_used() } /// Converts the included variable manager to a different type @@ -443,8 +493,31 @@ impl SatInstance { /// Converts the instance to a set of clauses. /// Uses the default encoders from the `encodings` module. + #[deprecated( + since = "0.5.0", + note = "as_cnf has been renamed to into_cnf and will be removed in a future release" + )] pub fn as_cnf(self) -> (Cnf, VM) { - self.as_cnf_with_encoders( + self.into_cnf() + } + + /// Converts the instance to a set of clauses. + /// Uses the default encoders from the `encodings` module. + /// + /// See [`Self::convert_to_cnf`] for converting in place + pub fn into_cnf(self) -> (Cnf, VM) { + self.into_cnf_with_encoders( + card::default_encode_cardinality_constraint, + pb::default_encode_pb_constraint, + ) + } + + /// Converts the instance to a set of clauses inplace. + /// Uses the default encoders from the `encodings` module. + /// + /// See [`Self::into_cnf`] if you don't need to convert in place + pub fn convert_to_cnf(&mut self) { + self.convert_to_cnf_with_encoders( card::default_encode_cardinality_constraint, pb::default_encode_pb_constraint, ) @@ -452,22 +525,57 @@ impl SatInstance { /// Converts the instance to a set of clauses with explicitly specified /// converters for non-clausal constraints. + #[deprecated( + since = "0.5.0", + note = "as_cnf_with_encoders has been renamed to into_cnf_with_encoders and will be removed in a future release" + )] pub fn as_cnf_with_encoders( + self, + card_encoder: CardEnc, + pb_encoder: PBEnc, + ) -> (Cnf, VM) + where + CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars), + PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars), + { + self.into_cnf_with_encoders(card_encoder, pb_encoder) + } + + /// Converts the instance to a set of clauses with explicitly specified + /// converters for non-clausal constraints. + /// + /// See [`Self::into_cnf_with_encoders`] to convert in place + pub fn into_cnf_with_encoders( mut self, - mut card_encoder: CardEnc, - mut pb_encoder: PBEnc, + card_encoder: CardEnc, + pb_encoder: PBEnc, ) -> (Cnf, VM) where CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars), PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars), + { + self.convert_to_cnf_with_encoders(card_encoder, pb_encoder); + (self.cnf, self.var_manager) + } + + /// Converts the instance inplace to a set of clauses with explicitly specified + /// converters for non-clausal constraints. + /// + /// See [`Self::into_cnf_with_encoders`] if you don't need to convert in place + pub fn convert_to_cnf_with_encoders( + &mut self, + mut card_encoder: CardEnc, + mut pb_encoder: PBEnc, + ) where + CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars), + PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars), { self.cards - .into_iter() + .drain(..) .for_each(|constr| card_encoder(constr, &mut self.cnf, &mut self.var_manager)); self.pbs - .into_iter() + .drain(..) .for_each(|constr| pb_encoder(constr, &mut self.cnf, &mut self.var_manager)); - (self.cnf, self.var_manager) } /// Extends the instance by another instance @@ -512,13 +620,17 @@ impl SatInstance { /// # Performance /// /// For performance, consider using a [`std::io::BufWriter`] instance. + #[deprecated(since = "0.5.0", note = "use write_dimacs_path instead")] pub fn to_dimacs_path>(self, path: P) -> Result<(), io::Error> { let mut writer = fio::open_compressed_uncompressed_write(path)?; + #[allow(deprecated)] self.to_dimacs(&mut writer) } /// Writes the instance to DIMACS CNF + #[deprecated(since = "0.5.0", note = "use write_dimacs instead")] pub fn to_dimacs(self, writer: &mut W) -> Result<(), io::Error> { + #[allow(deprecated)] self.to_dimacs_with_encoders( card::default_encode_cardinality_constraint, pb::default_encode_pb_constraint, @@ -528,6 +640,10 @@ impl SatInstance { /// Writes the instance to DIMACS CNF converting non-clausal constraints /// with specific encoders. + #[deprecated( + since = "0.5.0", + note = "use convert_to_cnf_with_encoders and write_dimacs instead" + )] pub fn to_dimacs_with_encoders( self, card_encoder: CardEnc, @@ -539,8 +655,45 @@ impl SatInstance { CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars), PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars), { - let (cnf, vm) = self.as_cnf_with_encoders(card_encoder, pb_encoder); - fio::dimacs::write_cnf_annotated(writer, cnf, vm.max_var()) + let (cnf, vm) = self.into_cnf_with_encoders(card_encoder, pb_encoder); + fio::dimacs::write_cnf_annotated(writer, &cnf, vm.n_used()) + } + + /// Writes the instance to a DIMACS CNF file at a path + /// + /// This requires that the instance is clausal, i.e., does not contain any non-converted + /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by + /// [`Self::convert_to_cnf`] or [`Self::convert_to_cnf_with_encoders`] first. + /// + /// # Errors + /// + /// - If the instance is not clausal, returns [`NonClausal`] + /// - Returns [`io::Error`] on errors during writing + pub fn write_dimacs_path>(&self, path: P) -> anyhow::Result<()> { + let mut writer = fio::open_compressed_uncompressed_write(path)?; + self.write_dimacs(&mut writer) + } + + /// Writes the instance to DIMACS CNF + /// + /// This requires that the instance is clausal, i.e., does not contain any non-converted + /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by + /// [`Self::convert_to_cnf`] or [`Self::convert_to_cnf_with_encoders`] first. + /// + /// # Performance + /// + /// For performance, consider using a [`std::io::BufWriter`] instance. + /// + /// # Errors + /// + /// - If the instance is not clausal, returns [`NonClausal`] + /// - Returns [`io::Error`] on errors during writing + pub fn write_dimacs(&self, writer: &mut W) -> anyhow::Result<()> { + if self.n_cards() > 0 || self.n_pbs() > 0 { + return Err(RequiresClausal.into()); + } + let n_vars = self.n_vars(); + Ok(fio::dimacs::write_cnf_annotated(writer, &self.cnf, n_vars)?) } /// Writes the instance to an OPB file at a path @@ -548,20 +701,46 @@ impl SatInstance { /// # Performance /// /// For performance, consider using a [`std::io::BufWriter`] instance. + #[deprecated(since = "0.5.0", note = "use write_opb_path instead")] pub fn to_opb_path>( self, path: P, opts: fio::opb::Options, ) -> Result<(), io::Error> { let mut writer = fio::open_compressed_uncompressed_write(path)?; + #[allow(deprecated)] self.to_opb(&mut writer, opts) } /// Writes the instance to an OPB file + #[deprecated(since = "0.5.0", note = "use write_opb instead")] pub fn to_opb( self, writer: &mut W, opts: fio::opb::Options, + ) -> Result<(), io::Error> { + fio::opb::write_sat(writer, &self, opts) + } + + /// Writes the instance to an OPB file at a path + pub fn write_opb_path>( + &self, + path: P, + opts: fio::opb::Options, + ) -> Result<(), io::Error> { + let mut writer = fio::open_compressed_uncompressed_write(path)?; + self.write_opb(&mut writer, opts) + } + + /// Writes the instance to an OPB file + /// + /// # Performance + /// + /// For performance, consider using a [`std::io::BufWriter`] instance. + pub fn write_opb( + &self, + writer: &mut W, + opts: fio::opb::Options, ) -> Result<(), io::Error> { fio::opb::write_sat(writer, self, opts) } @@ -599,11 +778,11 @@ impl SatInstance { return None; } if pb.is_clause() { - cnf.add_clause(pb.as_clause().unwrap()); + cnf.add_clause(pb.into_clause().unwrap()); return None; } if pb.is_card() { - cards.push(pb.as_card_constr().unwrap()); + cards.push(pb.into_card_constr().unwrap()); return None; } Some(pb) @@ -630,7 +809,7 @@ impl SatInstance { return None; } if card.is_clause() { - cnf.add_clause(card.as_clause().unwrap()); + cnf.add_clause(card.into_clause().unwrap()); return None; } Some(card) @@ -688,7 +867,7 @@ impl SatInstance { /// /// If a DIMACS WCNF or MCNF file is parsed with this method, the objectives /// are ignored and only the constraints returned. - pub fn from_dimacs(reader: R) -> anyhow::Result { + pub fn from_dimacs(reader: R) -> anyhow::Result { fio::dimacs::parse_cnf(reader) } @@ -708,7 +887,7 @@ impl SatInstance { /// The file format expected by this parser is the OPB format for /// pseudo-boolean satisfaction instances. For details on the file format /// see [here](https://www.cril.univ-artois.fr/PB12/format.pdf). - pub fn from_opb(reader: R, opts: fio::opb::Options) -> anyhow::Result { + pub fn from_opb(reader: R, opts: fio::opb::Options) -> anyhow::Result { fio::opb::parse_sat(reader, opts) } diff --git a/rustsat/src/lib.rs b/rustsat/src/lib.rs index d05d0f33..3095fcfc 100644 --- a/rustsat/src/lib.rs +++ b/rustsat/src/lib.rs @@ -88,3 +88,11 @@ impl fmt::Display for NotAllowed { #[cfg(feature = "bench")] #[cfg(test)] mod bench; + +#[derive(Error, Debug)] +#[error("operation requires a clausal constraint(s) but it is not")] +pub struct RequiresClausal; + +#[derive(Error, Debug)] +#[error("operation requires an objective only consisting of soft literals")] +pub struct RequiresSoftLits; diff --git a/rustsat/src/solvers.rs b/rustsat/src/solvers.rs index cc979a8a..08917610 100644 --- a/rustsat/src/solvers.rs +++ b/rustsat/src/solvers.rs @@ -96,7 +96,7 @@ use thiserror::Error; /// Trait for all SAT solvers in this library. /// Solvers outside of this library can also implement this trait to be able to /// use them with this library. -pub trait Solve: Extend { +pub trait Solve: Extend + for<'a> Extend<&'a Clause> { /// Gets a signature of the solver implementation fn signature(&self) -> &'static str; /// Reserves memory in the solver until a maximum variables, if the solver @@ -175,10 +175,19 @@ pub trait Solve: Extend { /// - If the solver is not in the satisfied state /// - A specific implementation might return other errors fn lit_val(&self, lit: Lit) -> anyhow::Result; - /// Adds a clause to the solver + /// Adds a clause to the solver. /// If the solver is in the satisfied or unsatisfied state before, it is in /// the input state afterwards. - fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()>; + /// + /// This method can be implemented by solvers that can truly take ownership of the clause. + /// Otherwise, it will fall back to the mandatory [`Solve::add_clause_ref`] method. + fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> { + self.add_clause_ref(&clause) + } + /// Adds a clause to the solver by reference. + /// If the solver is in the satisfied or unsatisfied state before, it is in + /// the input state afterwards. + fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()>; /// Like [`Solve::add_clause`] but for unit clauses (clauses with one literal). fn add_unit(&mut self, lit: Lit) -> anyhow::Result<()> { self.add_clause(clause![lit]) @@ -195,6 +204,10 @@ pub trait Solve: Extend { fn add_cnf(&mut self, cnf: Cnf) -> anyhow::Result<()> { cnf.into_iter().try_for_each(|cl| self.add_clause(cl)) } + /// Adds all clauses from a [`Cnf`] instance by reference. + fn add_cnf_ref(&mut self, cnf: &Cnf) -> anyhow::Result<()> { + cnf.iter().try_for_each(|cl| self.add_clause_ref(cl)) + } } /// Trait for all SAT solvers in this library. diff --git a/rustsat/src/types/constraints.rs b/rustsat/src/types/constraints.rs index 2856b9b8..664298d9 100644 --- a/rustsat/src/types/constraints.rs +++ b/rustsat/src/types/constraints.rs @@ -13,6 +13,8 @@ use thiserror::Error; use super::{Assignment, IWLitIter, Lit, LitIter, RsHashSet, TernaryVal, WLitIter}; +use crate::RequiresClausal; + /// Type representing a clause. /// Wrapper around a std collection to allow for changing the data structure. /// Optional clauses as sets will be included in the future. @@ -433,16 +435,25 @@ impl CardConstraint { } /// Converts the constraint into a clause, if possible + #[deprecated( + since = "0.5.0", + note = "as_clause has been slightly changed and renamed to into_clause and will be removed in a future release" + )] pub fn as_clause(self) -> Option { + self.into_clause().ok() + } + + /// Converts the constraint into a clause, if possible + pub fn into_clause(self) -> Result { if !self.is_clause() { - return None; + return Err(RequiresClausal); } match self { CardConstraint::UB(constr) => { - Some(Clause::from_iter(constr.lits.into_iter().map(Lit::not))) + Ok(Clause::from_iter(constr.lits.into_iter().map(Lit::not))) } - CardConstraint::LB(constr) => Some(Clause::from_iter(constr.lits)), - CardConstraint::EQ(_) => panic!(), + CardConstraint::LB(constr) => Ok(Clause::from_iter(constr.lits)), + CardConstraint::EQ(_) => unreachable!(), } } @@ -494,6 +505,11 @@ impl CardUBConstr { (self.lits, self.b) } + /// Get references to the constraints internals + pub(crate) fn decompose_ref(&self) -> (&Vec, &usize) { + (&self.lits, &self.b) + } + /// Checks if the constraint is always satisfied pub fn is_tautology(&self) -> bool { self.b >= self.lits.len() @@ -523,6 +539,11 @@ impl CardLBConstr { (self.lits, self.b) } + /// Get references to the constraints internals + pub(crate) fn decompose_ref(&self) -> (&Vec, &usize) { + (&self.lits, &self.b) + } + /// Checks if the constraint is always satisfied pub fn is_tautology(&self) -> bool { self.b == 0 @@ -557,6 +578,11 @@ impl CardEQConstr { (self.lits, self.b) } + /// Get references to the constraints internals + pub(crate) fn decompose_ref(&self) -> (&Vec, &usize) { + (&self.lits, &self.b) + } + /// Checks if the constraint is unsatisfiable pub fn is_unsat(&self) -> bool { self.b > self.lits.len() @@ -763,7 +789,16 @@ impl PBConstraint { } /// Converts the pseudo-boolean constraint into a cardinality constraint, if possible + #[deprecated( + since = "0.5.0", + note = "as_card_constr has been renamed to into_card_constr" + )] pub fn as_card_constr(self) -> Result { + self.into_card_constr() + } + + /// Converts the pseudo-boolean constraint into a cardinality constraint, if possible + pub fn into_card_constr(self) -> Result { if self.is_tautology() { return Err(PBToCardError::Tautology); } @@ -816,18 +851,27 @@ impl PBConstraint { } /// Converts the constraint into a clause, if possible + #[deprecated( + since = "0.5.0", + note = "as_clause has been slightly changed and renamed to into_clause and will be removed in a future release" + )] pub fn as_clause(self) -> Option { + self.into_clause().ok() + } + + /// Converts the constraint into a clause, if possible + pub fn into_clause(self) -> Result { if !self.is_clause() { - return None; + return Err(RequiresClausal); } match self { - PBConstraint::UB(constr) => Some(Clause::from_iter( + PBConstraint::UB(constr) => Ok(Clause::from_iter( constr.lits.into_iter().map(|(lit, _)| !lit), )), - PBConstraint::LB(constr) => Some(Clause::from_iter( + PBConstraint::LB(constr) => Ok(Clause::from_iter( constr.lits.into_iter().map(|(lit, _)| lit), )), - PBConstraint::EQ(_) => panic!(), + PBConstraint::EQ(_) => unreachable!(), } } @@ -907,6 +951,11 @@ impl PBUBConstr { (self.lits, self.b) } + /// Gets references to the constraints internals + pub(crate) fn decompose_ref(&self) -> (&Vec<(Lit, usize)>, &isize) { + (&self.lits, &self.b) + } + /// Checks if the constraint is always satisfied pub fn is_tautology(&self) -> bool { if self.b < 0 { @@ -977,6 +1026,11 @@ impl PBLBConstr { (self.lits, self.b) } + /// Gets references to the constraints internals + pub(crate) fn decompose_ref(&self) -> (&Vec<(Lit, usize)>, &isize) { + (&self.lits, &self.b) + } + /// Checks if the constraint is always satisfied pub fn is_tautology(&self) -> bool { self.b <= 0 @@ -1048,6 +1102,11 @@ impl PBEQConstr { (self.lits, self.b) } + /// Gets references to the constraints internals + pub(crate) fn decompose_ref(&self) -> (&Vec<(Lit, usize)>, &isize) { + (&self.lits, &self.b) + } + /// Checks if the constraint is unsatisfiable pub fn is_unsat(&self) -> bool { if self.b < 0 { diff --git a/rustsat/tests/compression.rs b/rustsat/tests/compression.rs index 36f88f7e..cb131106 100644 --- a/rustsat/tests/compression.rs +++ b/rustsat/tests/compression.rs @@ -9,7 +9,7 @@ fn small_sat_instance_gzip() { let inst: SatInstance = SatInstance::from_dimacs_path("./data/AProVE11-12.cnf.gz").unwrap(); let mut solver = rustsat_minisat::core::Minisat::default(); - solver.add_cnf(inst.as_cnf().0).unwrap(); + solver.add_cnf(inst.into_cnf().0).unwrap(); let res = solver.solve().unwrap(); assert_eq!(res, SolverResult::Sat); } @@ -22,7 +22,7 @@ fn small_unsat_instance_gzip() { ) .unwrap(); let mut solver = rustsat_minisat::core::Minisat::default(); - solver.add_cnf(inst.as_cnf().0).unwrap(); + solver.add_cnf(inst.into_cnf().0).unwrap(); let res = solver.solve().unwrap(); assert_eq!(res, SolverResult::Unsat); } @@ -32,7 +32,7 @@ fn small_sat_instance_bz2() { let inst: SatInstance = SatInstance::from_dimacs_path("./data/AProVE11-12.cnf.bz2").unwrap(); let mut solver = rustsat_minisat::core::Minisat::default(); - solver.add_cnf(inst.as_cnf().0).unwrap(); + solver.add_cnf(inst.into_cnf().0).unwrap(); let res = solver.solve().unwrap(); assert_eq!(res, SolverResult::Sat); } @@ -45,7 +45,7 @@ fn small_unsat_instance_bz2() { ) .unwrap(); let mut solver = rustsat_minisat::core::Minisat::default(); - solver.add_cnf(inst.as_cnf().0).unwrap(); + solver.add_cnf(inst.into_cnf().0).unwrap(); let res = solver.solve().unwrap(); assert_eq!(res, SolverResult::Unsat); } diff --git a/rustsat/tests/constraints.rs b/rustsat/tests/constraints.rs index 37aa58e7..1fc3c206 100644 --- a/rustsat/tests/constraints.rs +++ b/rustsat/tests/constraints.rs @@ -12,7 +12,7 @@ macro_rules! test_card { ( $constr:expr, $sat_assump:expr, $unsat_assump:expr ) => {{ let mut inst: SatInstance = SatInstance::new(); inst.add_card_constr($constr); - let (cnf, _) = inst.as_cnf(); + let (cnf, _) = inst.into_cnf(); println!("{:?}", cnf); let mut solver = rustsat_tools::Solver::default(); solver.add_cnf(cnf).unwrap(); @@ -31,7 +31,7 @@ macro_rules! test_pb { ( $constr:expr, $sat_assump:expr, $unsat_assump:expr ) => {{ let mut inst: SatInstance = SatInstance::new(); inst.add_pb_constr($constr); - let (cnf, _) = inst.as_cnf(); + let (cnf, _) = inst.into_cnf(); println!("{:?}", cnf); let mut solver = rustsat_tools::Solver::default(); solver.add_cnf(cnf).unwrap(); diff --git a/rustsat/tests/opb.rs b/rustsat/tests/opb.rs index f0ccdc5a..8f18f8bc 100644 --- a/rustsat/tests/opb.rs +++ b/rustsat/tests/opb.rs @@ -14,7 +14,7 @@ use rustsat::{ macro_rules! opb_test { ($path:expr, $expect:expr) => {{ let inst: SatInstance = SatInstance::from_opb_path($path, Options::default()).unwrap(); - let (cnf, _) = inst.as_cnf(); + let (cnf, _) = inst.into_cnf(); println!("{:?}", cnf); let mut solver = rustsat_minisat::core::Minisat::default(); solver.add_cnf(cnf).unwrap(); diff --git a/solvertests/src/integration.rs b/solvertests/src/integration.rs index 67aefabd..f3dee2ee 100644 --- a/solvertests/src/integration.rs +++ b/solvertests/src/integration.rs @@ -21,7 +21,7 @@ pub fn base(input: MacroInput) -> TokenStream { let mut solver = <$slv>::default(); let inst = rustsat::instances::SatInstance::::from_dimacs_path($inst) .expect("failed to parse instance"); - rustsat::solvers::Solve::add_cnf(&mut solver, inst.as_cnf().0) + rustsat::solvers::Solve::add_cnf(&mut solver, inst.into_cnf().0) .expect("failed to add cnf to solver"); let res = rustsat::solvers::Solve::solve(&mut solver).expect("failed solving"); assert_eq!(res, $res); @@ -30,7 +30,7 @@ pub fn base(input: MacroInput) -> TokenStream { let mut solver = $init; let inst = rustsat::instances::SatInstance::::from_dimacs_path($inst) .expect("failed to parse instance"); - rustsat::solvers::Solve::add_cnf(&mut solver, inst.as_cnf().0) + rustsat::solvers::Solve::add_cnf(&mut solver, inst.into_cnf().0) .expect("failed to add cnf to solver"); let res = rustsat::solvers::Solve::solve(&mut solver).expect("failed solving"); assert_eq!(res, $res); @@ -97,7 +97,7 @@ pub fn incremental(input: MacroInput) -> TokenStream { let mut solver = init_slv!(#slv); let inst: SatInstance = SatInstance::from_dimacs_path("./data/small.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); + solver.add_cnf(inst.into_cnf().0).unwrap(); let res = solver.solve().unwrap(); assert_eq!(res, Sat); let res = solver.solve_assumps(&[!lit![0], !lit![1]]).unwrap(); @@ -205,7 +205,7 @@ pub fn phasing(input: MacroInput) -> TokenStream { let mut solver = init_slv!(#slv); let inst: SatInstance = SatInstance::from_dimacs_path("./data/small.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); + solver.add_cnf(inst.into_cnf().0).unwrap(); solver.phase_lit(lit![0]).unwrap(); solver.phase_lit(!lit![1]).unwrap(); solver.phase_lit(lit![2]).unwrap(); diff --git a/tools/Cargo.toml b/tools/Cargo.toml index 22c9cc1a..8dfda761 100644 --- a/tools/Cargo.toml +++ b/tools/Cargo.toml @@ -27,6 +27,7 @@ atty = { version = "0.2.14" } nom = "7.1.3" rand = "0.8.5" rand_chacha = "0.3.1" +anyhow = { version = "1.0.80" } [features] default = ["minisat"] diff --git a/tools/src/bin/cnf2opb.rs b/tools/src/bin/cnf2opb.rs index c0153dcc..6242c3f9 100644 --- a/tools/src/bin/cnf2opb.rs +++ b/tools/src/bin/cnf2opb.rs @@ -2,6 +2,7 @@ //! //! A small tool for converting DIMACS CNF files to OPB. +use anyhow::Context; use clap::Parser; use rustsat::instances::{fio::opb::Options as OpbOptions, SatInstance}; use std::{io, path::PathBuf}; @@ -21,7 +22,7 @@ struct Args { avoid_negated_lits: bool, } -fn main() { +fn main() -> anyhow::Result<()> { let args = Args::parse(); let opb_opts = OpbOptions { first_var_idx: args.first_var_idx, @@ -29,16 +30,17 @@ fn main() { }; let inst: SatInstance = if let Some(in_path) = args.in_path { - SatInstance::from_dimacs_path(in_path).expect("error parsing the input file") + SatInstance::from_dimacs_path(in_path).context("error parsing the input file")? } else { - SatInstance::from_dimacs(io::stdin()).expect("error parsing input") + SatInstance::from_dimacs(io::BufReader::new(io::stdin())).context("error parsing input")? }; if let Some(out_path) = args.out_path { - inst.to_opb_path(out_path, opb_opts) - .expect("io error writing the output file"); + inst.write_opb_path(out_path, opb_opts) + .context("error writing the output file")?; } else { - inst.to_opb(&mut io::stdout(), opb_opts) - .expect("io error writing the output file"); + inst.write_opb(&mut io::stdout(), opb_opts) + .context("error writing the output file")?; } + Ok(()) } diff --git a/tools/src/bin/encodings.rs b/tools/src/bin/encodings.rs index fc28c61f..95768524 100644 --- a/tools/src/bin/encodings.rs +++ b/tools/src/bin/encodings.rs @@ -14,7 +14,7 @@ use clap::{Args, Parser, Subcommand}; use rustsat::{encodings::pb, instances::fio::dimacs}; use rustsat_tools::encodings::{ - clustering::{self, saturating_map, scaling_map, Encoding, Error, Variant}, + clustering::{self, saturating_map, scaling_map, Encoding, Variant}, knapsack, }; use std::{fs::File, io, path::PathBuf}; @@ -93,7 +93,7 @@ struct KnapsackArgs { seed: u64, } -fn clustering(args: ClusteringArgs) -> Result<(), Error> { +fn clustering(args: ClusteringArgs) -> anyhow::Result<()> { let mcnf_to_wcnf = |line: dimacs::McnfLine| match line { dimacs::McnfLine::Comment(c) => dimacs::WcnfLine::Comment(c), dimacs::McnfLine::Hard(cl) => dimacs::WcnfLine::Hard(cl), @@ -149,7 +149,7 @@ fn clustering(args: ClusteringArgs) -> Result<(), Error> { Ok(()) } -fn knapsack(args: KnapsackArgs) -> Result<(), Error> { +fn knapsack(args: KnapsackArgs) -> anyhow::Result<()> { let encoding = knapsack::Encoding::new::(knapsack::Knapsack::random( args.n_items, args.n_objectives, @@ -167,7 +167,7 @@ fn knapsack(args: KnapsackArgs) -> Result<(), Error> { Ok(()) } -fn main() -> Result<(), Error> { +fn main() -> anyhow::Result<()> { let args = CliArgs::parse(); match args.cmd { diff --git a/tools/src/bin/enumerator.rs b/tools/src/bin/enumerator.rs index b885503f..2c2efcf8 100644 --- a/tools/src/bin/enumerator.rs +++ b/tools/src/bin/enumerator.rs @@ -4,6 +4,7 @@ //! //! Usage: enumerator [dimacs cnf file] +use anyhow::Context; use rustsat::{ instances::{ManageVars, SatInstance}, solvers::{self, Solve, SolveIncremental}, @@ -45,17 +46,17 @@ impl Iterator for Enumerator { } } -fn main() { +fn main() -> anyhow::Result<()> { let in_path = std::env::args().nth(1).unwrap_or_else(|| print_usage!()); let inst: SatInstance = - SatInstance::from_dimacs_path(in_path).expect("error parsing the input file"); - let (cnf, vm) = inst.as_cnf(); + SatInstance::from_dimacs_path(in_path).context("error parsing the input file")?; + let (cnf, vm) = inst.into_cnf(); let mut solver = rustsat_tools::Solver::default(); solver .reserve(vm.max_var().expect("no variables in instance")) - .expect("error reserving memory in solver"); + .context("error reserving memory in solver")?; solver.add_cnf(cnf).expect("error adding cnf to solver"); let enumerator = Enumerator { @@ -63,5 +64,6 @@ fn main() { max_var: vm.max_var().unwrap(), }; - enumerator.for_each(|sol| println!("s {}", sol)) + enumerator.for_each(|sol| println!("s {}", sol)); + Ok(()) } diff --git a/tools/src/bin/gbmosplit.rs b/tools/src/bin/gbmosplit.rs index 7c48f45b..e7d2de7c 100644 --- a/tools/src/bin/gbmosplit.rs +++ b/tools/src/bin/gbmosplit.rs @@ -252,7 +252,7 @@ fn split( ); } - let (softs, offset) = obj.as_soft_cls(); + let (softs, offset) = obj.into_soft_cls(); if offset != 0 { cli.warning(&format!( @@ -475,7 +475,7 @@ fn main() { if let Some(out_path) = &cli.out_path { if found_split || cli.always_dump { - mo_inst.to_dimacs_path(out_path).unwrap_or_else(|e| { + mo_inst.write_dimacs_path(out_path).unwrap_or_else(|e| { cli.error(&format!("io error writing the output file: {}", e)); panic!() }); diff --git a/tools/src/bin/mcnf2opb.rs b/tools/src/bin/mcnf2opb.rs index 9830083d..345d06b4 100644 --- a/tools/src/bin/mcnf2opb.rs +++ b/tools/src/bin/mcnf2opb.rs @@ -2,6 +2,7 @@ //! //! A small tool for converting DIMACS MCNF files to OPB. +use anyhow::Context; use clap::Parser; use rustsat::instances::{fio::opb::Options as OpbOptions, MultiOptInstance}; use std::{io, path::PathBuf}; @@ -21,7 +22,7 @@ struct Args { avoid_negated_lits: bool, } -fn main() { +fn main() -> anyhow::Result<()> { let args = Args::parse(); let opb_opts = OpbOptions { first_var_idx: args.first_var_idx, @@ -29,16 +30,25 @@ fn main() { }; let inst: MultiOptInstance = if let Some(in_path) = args.in_path { - MultiOptInstance::from_dimacs_path(in_path).expect("error parsing the input file") + MultiOptInstance::from_dimacs_path(in_path).context("error parsing the input file")? } else { - MultiOptInstance::from_dimacs(io::stdin()).expect("error parsing input") + MultiOptInstance::from_dimacs(io::BufReader::new(io::stdin())) + .context("error parsing input")? }; + let (mut constr, mut objs) = inst.decompose(); + for obj in &mut objs { + let hardened = obj.convert_to_soft_lits(constr.var_manager_mut()); + constr.extend(hardened.into()); + } + let inst = MultiOptInstance::compose(constr, objs); + if let Some(out_path) = args.out_path { - inst.to_opb_path(out_path, opb_opts) - .expect("io error writing the output file"); + inst.write_opb_path(out_path, opb_opts) + .context("error writing the output file")?; } else { - inst.to_opb(&mut io::stdout(), opb_opts) - .expect("io error writing the output file"); + inst.write_opb(&mut io::stdout(), opb_opts) + .context("error writing the output file")?; } + Ok(()) } diff --git a/tools/src/bin/opb2cnf.rs b/tools/src/bin/opb2cnf.rs index 9bc13768..0d8244f3 100644 --- a/tools/src/bin/opb2cnf.rs +++ b/tools/src/bin/opb2cnf.rs @@ -2,6 +2,7 @@ //! //! A small tool for converting OPB files to DIMACS CNF. +use anyhow::Context; use clap::Parser; use rustsat::instances::{fio::opb::Options as OpbOptions, SatInstance}; use std::{io, path::PathBuf}; @@ -18,28 +19,32 @@ struct Args { first_var_idx: usize, } -fn main() { +fn main() -> anyhow::Result<()> { let args = Args::parse(); let opb_opts = OpbOptions { first_var_idx: 0, ..Default::default() }; - let inst: SatInstance = if let Some(in_path) = args.in_path { - SatInstance::from_opb_path(in_path, opb_opts).expect("error parsing the input file") + let mut inst: SatInstance = if let Some(in_path) = args.in_path { + SatInstance::from_opb_path(in_path, opb_opts).context("error parsing the input file")? } else { - SatInstance::from_opb(io::stdin(), opb_opts).expect("error parsing input") + SatInstance::from_opb(io::BufReader::new(io::stdin()), opb_opts) + .context("error parsing input")? }; println!("{} clauses", inst.n_clauses()); println!("{} cards", inst.n_cards()); println!("{} pbs", inst.n_pbs()); + inst.convert_to_cnf(); + if let Some(out_path) = args.out_path { - inst.to_dimacs_path(out_path) - .expect("io error writing the output file"); + inst.write_dimacs_path(out_path) + .context("error writing the output file")?; } else { - inst.to_dimacs(&mut io::stdout()) - .expect("io error writing to stdout"); + inst.write_dimacs(&mut io::stdout()) + .context("error writing to stdout")?; } + Ok(()) } diff --git a/tools/src/bin/opb2mcnf.rs b/tools/src/bin/opb2mcnf.rs index a7127f8b..0bb9c873 100644 --- a/tools/src/bin/opb2mcnf.rs +++ b/tools/src/bin/opb2mcnf.rs @@ -2,6 +2,7 @@ //! //! A small tool for converting OPB files to DIMACS MCNF. +use anyhow::Context; use clap::Parser; use rustsat::instances::{fio::opb::Options as OpbOptions, MultiOptInstance}; use std::{io, path::PathBuf}; @@ -18,7 +19,7 @@ struct Args { first_var_idx: usize, } -fn main() { +fn main() -> anyhow::Result<()> { let args = Args::parse(); let opb_opts = OpbOptions { first_var_idx: 0, @@ -26,9 +27,11 @@ fn main() { }; let inst: MultiOptInstance = if let Some(in_path) = args.in_path { - MultiOptInstance::from_opb_path(in_path, opb_opts).expect("error parsing the input file") + MultiOptInstance::from_opb_path(in_path, opb_opts) + .context("error parsing the input file")? } else { - MultiOptInstance::from_opb(io::stdin(), opb_opts).expect("error parsing input") + MultiOptInstance::from_opb(io::BufReader::new(io::stdin()), opb_opts) + .context("error parsing input")? }; let (constrs, objs) = inst.decompose(); @@ -39,13 +42,15 @@ fn main() { println!("c {} pbs", constrs.n_pbs()); println!("c {} objectives", objs.len()); - let inst = MultiOptInstance::compose(constrs, objs); + let mut inst = MultiOptInstance::compose(constrs, objs); + inst.constraints_mut().convert_to_cnf(); if let Some(out_path) = args.out_path { - inst.to_dimacs_path(out_path) - .expect("io error writing the output file"); + inst.write_dimacs_path(out_path) + .context("error writing the output file")?; } else { - inst.to_dimacs(&mut io::stdout()) - .expect("io error writing to stdout"); + inst.write_dimacs(&mut io::stdout()) + .context("error writing to stdout")?; } + Ok(()) } diff --git a/tools/src/bin/opb2wcnf.rs b/tools/src/bin/opb2wcnf.rs index 3e075a84..f2fdf3a0 100644 --- a/tools/src/bin/opb2wcnf.rs +++ b/tools/src/bin/opb2wcnf.rs @@ -2,6 +2,7 @@ //! //! A small tool for converting OPB files to DIMACS WCNF. +use anyhow::Context; use clap::Parser; use rustsat::instances::{fio::opb::Options as OpbOptions, OptInstance}; use std::{io, path::PathBuf}; @@ -18,7 +19,7 @@ struct Args { first_var_idx: usize, } -fn main() { +fn main() -> anyhow::Result<()> { let args = Args::parse(); let opb_opts = OpbOptions { first_var_idx: 0, @@ -26,25 +27,28 @@ fn main() { }; let inst: OptInstance = if let Some(in_path) = args.in_path { - OptInstance::from_opb_path(in_path, opb_opts).expect("error parsing the input file") + OptInstance::from_opb_path(in_path, opb_opts).context("error parsing the input file")? } else { - OptInstance::from_opb(io::stdin(), opb_opts).expect("error parsing input") + OptInstance::from_opb(io::BufReader::new(io::stdin()), opb_opts) + .context("error parsing input")? }; let (constrs, obj) = inst.decompose(); - let constrs = constrs.sanitize(); + let mut constrs = constrs.sanitize(); println!("c {} clauses", constrs.n_clauses()); println!("c {} cards", constrs.n_cards()); println!("c {} pbs", constrs.n_pbs()); + constrs.convert_to_cnf(); let inst = OptInstance::compose(constrs, obj); if let Some(out_path) = args.out_path { - inst.to_dimacs_path(out_path) - .expect("io error writing the output file"); + inst.write_dimacs_path(out_path) + .context("io error writing the output file")?; } else { - inst.to_dimacs(&mut io::stdout()) - .expect("io error writing to stdout"); + inst.write_dimacs(&mut io::stdout()) + .context("io error writing to stdout")?; } + Ok(()) } diff --git a/tools/src/bin/shuffledimacs.rs b/tools/src/bin/shuffledimacs.rs index 645d1568..e10c61e9 100644 --- a/tools/src/bin/shuffledimacs.rs +++ b/tools/src/bin/shuffledimacs.rs @@ -7,7 +7,8 @@ use std::path::{Path, PathBuf}; -use rustsat::instances::{self, BasicVarManager, ManageVars, RandReindVarManager}; +use anyhow::Context; +use rustsat::instances::{self, BasicVarManager, RandReindVarManager}; macro_rules! print_usage { () => {{ @@ -22,43 +23,43 @@ enum FileType { Mcnf, } -fn main() { +fn main() -> anyhow::Result<()> { let in_path = PathBuf::from(&std::env::args().nth(1).unwrap_or_else(|| print_usage!())); let out_path = PathBuf::from(&std::env::args().nth(2).unwrap_or_else(|| print_usage!())); match determine_file_type(&in_path) { FileType::Cnf => { - let mut inst = instances::SatInstance::::from_dimacs_path(in_path) - .expect("Could not parse CNF"); - let n_vars = inst.var_manager().n_used(); + let inst = instances::SatInstance::::from_dimacs_path(in_path) + .context("Could not parse CNF")?; + let n_vars = inst.n_vars(); let rand_reindexer = RandReindVarManager::init(n_vars); inst.reindex(rand_reindexer) .shuffle() - .to_dimacs_path(out_path) - .expect("Could not write CNF"); + .write_dimacs_path(out_path) + .context("Could not write CNF")?; } FileType::Wcnf => { - let mut inst = instances::OptInstance::::from_dimacs_path(in_path) - .expect("Could not parse WCNF"); - let n_vars = inst.get_constraints().var_manager().n_used(); + let inst = instances::OptInstance::::from_dimacs_path(in_path) + .context("Could not parse WCNF")?; + let n_vars = inst.constraints_ref().n_vars(); let rand_reindexer = RandReindVarManager::init(n_vars); inst.reindex(rand_reindexer) .shuffle() - .to_dimacs_path(out_path) - .expect("Could not write WCNF"); + .write_dimacs_path(out_path) + .context("Could not write WCNF")?; } FileType::Mcnf => { - let mut inst = - instances::MultiOptInstance::::from_dimacs_path(in_path) - .expect("Could not parse MCNF"); - let n_vars = inst.get_constraints().var_manager().n_used(); + let inst = instances::MultiOptInstance::::from_dimacs_path(in_path) + .context("Could not parse MCNF")?; + let n_vars = inst.constraints_ref().n_vars(); let rand_reindexer = RandReindVarManager::init(n_vars); inst.reindex(rand_reindexer) .shuffle() - .to_dimacs_path(out_path) - .expect("Could not write MCNF"); + .write_dimacs_path(out_path) + .context("Could not write MCNF")?; } } + Ok(()) } macro_rules! is_one_of { diff --git a/tools/src/bin/wcnf2opb.rs b/tools/src/bin/wcnf2opb.rs index 115ee609..6be8aea7 100644 --- a/tools/src/bin/wcnf2opb.rs +++ b/tools/src/bin/wcnf2opb.rs @@ -2,6 +2,7 @@ //! //! A small tool for converting DIMACS WCNF files to OPB. +use anyhow::Context; use clap::Parser; use rustsat::instances::{fio::opb::Options as OpbOptions, OptInstance}; use std::{io, path::PathBuf}; @@ -21,7 +22,7 @@ struct Args { avoid_negated_lits: bool, } -fn main() { +fn main() -> anyhow::Result<()> { let args = Args::parse(); let opb_opts = OpbOptions { first_var_idx: args.first_var_idx, @@ -29,16 +30,22 @@ fn main() { }; let inst: OptInstance = if let Some(in_path) = args.in_path { - OptInstance::from_dimacs_path(in_path).expect("error parsing the input file") + OptInstance::from_dimacs_path(in_path).context("error parsing the input file")? } else { - OptInstance::from_dimacs(io::stdin()).expect("error parsing input") + OptInstance::from_dimacs(io::BufReader::new(io::stdin())).context("error parsing input")? }; + let (mut constr, mut obj) = inst.decompose(); + let hardened = obj.convert_to_soft_lits(constr.var_manager_mut()); + constr.extend(hardened.into()); + let inst = OptInstance::compose(constr, obj); + if let Some(out_path) = args.out_path { - inst.to_opb_path(out_path, opb_opts) - .expect("io error writing the output file"); + inst.write_opb_path(out_path, opb_opts) + .context("error writing the output file")?; } else { - inst.to_opb(&mut io::stdout(), opb_opts) - .expect("io error writing to stdout"); + inst.write_opb(&mut io::stdout(), opb_opts) + .context("io error writing to stdout")?; }; + Ok(()) } diff --git a/tools/src/encodings/clustering.rs b/tools/src/encodings/clustering.rs index 00b1387b..d8b078f8 100644 --- a/tools/src/encodings/clustering.rs +++ b/tools/src/encodings/clustering.rs @@ -123,24 +123,6 @@ impl Default for VarManager { } } -#[derive(Debug)] -pub enum Error { - Io(io::Error), - Parsing(String), -} - -impl From for Error { - fn from(value: io::Error) -> Self { - Error::Io(value) - } -} - -impl From>> for Error { - fn from(value: nom::Err>) -> Self { - Error::Parsing(value.to_string()) - } -} - #[derive(Clone, Copy, PartialEq, Eq, Debug)] pub enum Similarity { Similar(usize), @@ -179,7 +161,7 @@ impl Encoding { in_reader: R, variant: Variant, sim_map: Map, - ) -> Result { + ) -> anyhow::Result { if variant != Variant::Binary { panic!("only the binary encoding is implemented so far"); } @@ -187,7 +169,7 @@ impl Encoding { let mut ident_map = RsHashMap::default(); let mut next_idx: u32 = 0; let process_line = - |line: Result| -> Option> { + |line: Result| -> Option> { let line = line.ok()?; let line = line.trim_start(); if line.starts_with('%') {