From f994dc6bb63a6f53096042bca4dedb8f90201c7c Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Sun, 12 May 2019 13:10:55 +0200 Subject: [PATCH 1/3] checker: Use a simple bump allocator for clause literals --- varisat/src/checker.rs | 159 +++++++++++++++++++++++++++++++++-------- 1 file changed, 129 insertions(+), 30 deletions(-) diff --git a/varisat/src/checker.rs b/varisat/src/checker.rs index 7592063c..f0138a9e 100644 --- a/varisat/src/checker.rs +++ b/varisat/src/checker.rs @@ -1,6 +1,8 @@ //! Check unsatisfiability proofs. +use std::convert::TryInto; use std::io; +use std::mem::{replace, transmute}; use std::ops::Range; use failure::{Error, Fail}; @@ -91,11 +93,67 @@ pub trait ProofProcessor { fn process_step(&mut self, step: &CheckedProofStep) -> Result<(), Error>; } -/// Avoid indirection for small clauses. -type LitVec = SmallVec<[Lit; 4]>; +const INLINE_LITS: usize = 3; + +/// Literals of a clause, either inline or an index into a buffer +struct ClauseLits { + length: LitIdx, + inline: [LitIdx; INLINE_LITS], +} + +impl ClauseLits { + /// Create a new ClauseLits, storing them in the given buffer if necessary + fn new(lits: &[Lit], buffer: &mut Vec) -> ClauseLits { + let mut inline = [0; INLINE_LITS]; + let length = lits.len(); + + if length > INLINE_LITS { + inline[0] = buffer + .len() + .try_into() + .expect("exceeded maximal literal buffer size"); + buffer.extend(lits); + } else { + let lits = unsafe { + // Lit is a repr(transparent) wrapper of LitIdx + transmute::<&[Lit], &[LitIdx]>(lits) + }; + inline[..length].copy_from_slice(lits); + } + + ClauseLits { + length: length as LitIdx, + inline, + } + } + + /// Returns the literals as a slice given a storage buffer + fn slice<'a, 'b, 'c>(&'a self, buffer: &'b [Lit]) -> &'c [Lit] + where + 'a: 'c, + 'b: 'c, + { + if self.length > INLINE_LITS as LitIdx { + &buffer[self.inline[0] as usize..][..self.length as usize] + } else { + unsafe { + // Lit is a repr(transparent) wrapper of LitIdx + transmute::<&[LitIdx], &[Lit]>(&self.inline[..self.length as usize]) + } + } + } + + /// Literals stored in the literal buffer + fn buffer_used(&self) -> usize { + if self.length > INLINE_LITS as LitIdx { + self.length as usize + } else { + 0 + } + } +} /// Literals and metadata for non-unit clauses. -#[derive(Debug)] struct Clause { /// LRAT clause id. id: u64, @@ -105,7 +163,7 @@ struct Clause { /// solver might not check for duplicated clauses. ref_count: u32, /// Clause's literals. - lits: LitVec, + lits: ClauseLits, } /// Identifies the origin of a unit clause. @@ -137,6 +195,10 @@ pub struct Checker<'a> { step: u64, /// Next clause id to use. next_clause_id: u64, + /// Literal storage for clauses, + literal_buffer: Vec, + /// Number of literals in the buffer which are from deleted clauses. + garbage_size: usize, /// Stores all known non-unit clauses indexed by their hash. clauses: HashMap>, /// Stores known unit clauses and propagations during a clause check. @@ -183,14 +245,16 @@ impl<'a> Checker<'a> { return Ok(()); } - let mut lits = LitVec::from_slice(clause); - lits.sort_unstable(); - lits.dedup(); + let mut tmp = replace(&mut self.tmp, vec![]); + tmp.clear(); + tmp.extend_from_slice(&clause); + + tmp.sort_unstable(); + tmp.dedup(); - self.tmp.clear(); - self.tmp.extend_from_slice(&lits); + let (id, added) = self.store_clause(&tmp); - let (id, added) = self.store_clause(lits); + self.tmp = tmp; if added { Self::process_step( @@ -248,7 +312,7 @@ impl<'a> Checker<'a> { /// /// Returns the id of the added clause and a boolean that is true if the clause wasn't already /// present. - fn store_clause(&mut self, lits: LitVec) -> (u64, bool) { + fn store_clause(&mut self, lits: &[Lit]) -> (u64, bool) { match lits[..] { [] => { let id = self.next_clause_id; @@ -264,7 +328,7 @@ impl<'a> Checker<'a> { let candidates = self.clauses.entry(hash).or_default(); for candidate in candidates.iter_mut() { - if candidate.lits == lits { + if candidate.lits.slice(&self.literal_buffer) == &lits[..] { candidate.ref_count = candidate .ref_count .checked_add(1) @@ -278,7 +342,7 @@ impl<'a> Checker<'a> { candidates.push(Clause { id, ref_count: 1, - lits, + lits: ClauseLits::new(&lits, &mut self.literal_buffer), }); self.next_clause_id += 1; @@ -354,11 +418,15 @@ impl<'a> Checker<'a> { let mut result = None; + let literal_buffer = &self.literal_buffer; + let garbage_size = &mut self.garbage_size; + candidates.retain(|candidate| { - if deleted || &candidate.lits[..] != lits { + if deleted || candidate.lits.slice(literal_buffer) != lits { true } else { deleted = true; + *garbage_size += candidate.lits.buffer_used(); candidate.ref_count -= 1; if candidate.ref_count == 0 { result = Some(candidate.id); @@ -378,9 +446,33 @@ impl<'a> Checker<'a> { step: self.step, clause: lits.to_owned(), }); - } else { - Ok(result) } + + self.collect_garbage(); + + Ok(result) + } + + /// Perform a garbage collection if required + fn collect_garbage(&mut self) { + if self.garbage_size * 2 <= self.literal_buffer.len() { + return; + } + + let mut new_buffer = vec![]; + + new_buffer.reserve(self.literal_buffer.len()); + + for (_, candidates) in self.clauses.iter_mut() { + for clause in candidates.iter_mut() { + let new_lits = + ClauseLits::new(clause.lits.slice(&self.literal_buffer), &mut new_buffer); + clause.lits = new_lits; + } + } + + self.literal_buffer = new_buffer; + self.garbage_size = 0; } /// Check whether a clause is implied by clauses of the given hashes. @@ -430,7 +522,7 @@ impl<'a> Checker<'a> { let range_begin = self.trace_edges.len(); - for &lit in clause.lits.iter() { + for &lit in clause.lits.slice(&self.literal_buffer).iter() { match self.lit_value(lit) { Some((true, _)) => { continue 'candidates; @@ -535,42 +627,49 @@ impl<'a> Checker<'a> { clause, propagation_hashes, } => { - let mut clause = LitVec::from_vec(clause.into_owned()); - clause.sort_unstable(); - clause.dedup(); + let mut tmp = replace(&mut self.tmp, vec![]); + tmp.clear(); + tmp.extend_from_slice(&clause); - self.check_clause_with_hashes(&clause, &*propagation_hashes)?; + tmp.sort_unstable(); + tmp.dedup(); - self.tmp.clear(); - self.tmp.extend_from_slice(&clause[..]); + self.check_clause_with_hashes(&tmp, &*propagation_hashes)?; - let (id, added) = self.store_clause(clause); + let (id, added) = self.store_clause(&tmp); if added { Self::process_step( &mut self.processors, &CheckedProofStep::AtClause { id: id, - clause: &self.tmp, + clause: &tmp, propagations: &self.trace_ids, }, )?; } + + self.tmp = tmp; } ProofStep::DeleteClause(clause) => { - let mut clause = clause.into_owned(); - clause.sort_unstable(); - clause.dedup(); + let mut tmp = replace(&mut self.tmp, vec![]); + tmp.clear(); + tmp.extend_from_slice(&clause); - if let Some(id) = self.delete_clause(&clause)? { + tmp.sort_unstable(); + tmp.dedup(); + + if let Some(id) = self.delete_clause(&tmp)? { Self::process_step( &mut self.processors, &CheckedProofStep::DeleteClause { id: id, - clause: &clause, + clause: &tmp, }, )?; } + + self.tmp = tmp; } ProofStep::UnitClauses(units) => { for &(lit, hash) in units.iter() { From c888cd6d4546e48f3ebfc28f4d527bcfafe7353a Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 13 May 2019 09:15:46 +0200 Subject: [PATCH 2/3] Use variable length encoding for varisat proofs Part of #40 --- Cargo.lock | 18 +---- varisat/Cargo.toml | 1 - varisat/src/binary.rs | 4 +- varisat/src/cdcl.rs | 2 +- varisat/src/checker.rs | 28 +++++--- varisat/src/clause/reduce.rs | 2 +- varisat/src/lib.rs | 1 + varisat/src/load.rs | 4 +- varisat/src/proof.rs | 85 +++------------------- varisat/src/proof/drat.rs | 58 +++++++++++++++ varisat/src/proof/varisat.rs | 135 +++++++++++++++++++++++++++++++++++ varisat/src/simplify.rs | 16 ++--- varisat/src/vli_enc.rs | 134 ++++++++++++++++++++++++++++++++++ 13 files changed, 373 insertions(+), 115 deletions(-) create mode 100644 varisat/src/proof/drat.rs create mode 100644 varisat/src/proof/varisat.rs create mode 100644 varisat/src/vli_enc.rs diff --git a/Cargo.lock b/Cargo.lock index 9982510a..94e4cee5 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -53,16 +53,6 @@ dependencies = [ "libc 0.2.54 (registry+https://github.com/rust-lang/crates.io-index)", ] -[[package]] -name = "bincode" -version = "1.1.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -dependencies = [ - "autocfg 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)", - "byteorder 1.3.1 (registry+https://github.com/rust-lang/crates.io-index)", - "serde 1.0.91 (registry+https://github.com/rust-lang/crates.io-index)", -] - [[package]] name = "bit-set" version = "0.5.1" @@ -458,12 +448,12 @@ name = "serde" version = "1.0.91" source = "registry+https://github.com/rust-lang/crates.io-index" dependencies = [ - "serde_derive 1.0.90 (registry+https://github.com/rust-lang/crates.io-index)", + "serde_derive 1.0.91 (registry+https://github.com/rust-lang/crates.io-index)", ] [[package]] name = "serde_derive" -version = "1.0.90" +version = "1.0.91" source = "registry+https://github.com/rust-lang/crates.io-index" dependencies = [ "proc-macro2 0.4.30 (registry+https://github.com/rust-lang/crates.io-index)", @@ -593,7 +583,6 @@ source = "registry+https://github.com/rust-lang/crates.io-index" name = "varisat" version = "0.2.0" dependencies = [ - "bincode 1.1.3 (registry+https://github.com/rust-lang/crates.io-index)", "failure 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)", "hashbrown 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)", "itoa 0.4.4 (registry+https://github.com/rust-lang/crates.io-index)", @@ -698,7 +687,6 @@ dependencies = [ "checksum autocfg 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "a6d640bee2da49f60a4068a7fae53acde8982514ab7bae8b8cea9e88cbcfd799" "checksum backtrace 0.3.15 (registry+https://github.com/rust-lang/crates.io-index)" = "f106c02a3604afcdc0df5d36cc47b44b55917dbaf3d808f71c163a0ddba64637" "checksum backtrace-sys 0.1.28 (registry+https://github.com/rust-lang/crates.io-index)" = "797c830ac25ccc92a7f8a7b9862bde440715531514594a6154e3d4a54dd769b6" -"checksum bincode 1.1.3 (registry+https://github.com/rust-lang/crates.io-index)" = "959c8e54c1ad412ffeeb95f05a9cade02d2d40a7b3c2f852d3353148f4beff35" "checksum bit-set 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)" = "e84c238982c4b1e1ee668d136c510c67a13465279c0cb367ea6baf6310620a80" "checksum bit-vec 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)" = "f59bbe95d4e52a6398ec21238d31577f2b28a9d86807f06ca59d191d8440d0bb" "checksum bitflags 1.0.5 (registry+https://github.com/rust-lang/crates.io-index)" = "bd1fa8ad26490b0a5cfec99089952250301b6716cdeaa7c9ab229598fb82ab66" @@ -749,7 +737,7 @@ dependencies = [ "checksum rustc-demangle 0.1.14 (registry+https://github.com/rust-lang/crates.io-index)" = "ccc78bfd5acd7bf3e89cffcf899e5cb1a52d6fafa8dec2739ad70c9577a57288" "checksum rusty-fork 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)" = "3dd93264e10c577503e926bd1430193eeb5d21b059148910082245309b424fae" "checksum serde 1.0.91 (registry+https://github.com/rust-lang/crates.io-index)" = "a72e9b96fa45ce22a4bc23da3858dfccfd60acd28a25bcd328a98fdd6bea43fd" -"checksum serde_derive 1.0.90 (registry+https://github.com/rust-lang/crates.io-index)" = "58fc82bec244f168b23d1963b45c8bf5726e9a15a9d146a067f9081aeed2de79" +"checksum serde_derive 1.0.91 (registry+https://github.com/rust-lang/crates.io-index)" = "101b495b109a3e3ca8c4cbe44cf62391527cdfb6ba15821c5ce80bcd5ea23f9f" "checksum smallvec 0.6.9 (registry+https://github.com/rust-lang/crates.io-index)" = "c4488ae950c49d403731982257768f48fada354a5203fe81f9bb6f43ca9002be" "checksum strsim 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)" = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" "checksum syn 0.15.34 (registry+https://github.com/rust-lang/crates.io-index)" = "a1393e4a97a19c01e900df2aec855a29f71cf02c402e2f443b8d2747c25c5dbe" diff --git a/varisat/Cargo.toml b/varisat/Cargo.toml index 3e9dc1ed..e10ab04f 100644 --- a/varisat/Cargo.toml +++ b/varisat/Cargo.toml @@ -12,7 +12,6 @@ edition = "2018" [dependencies] -bincode = "1.1.3" failure = "0.1.5" itoa = "0.4.4" log = "0.4.6" diff --git a/varisat/src/binary.rs b/varisat/src/binary.rs index 120d7f04..eda7c731 100644 --- a/varisat/src/binary.rs +++ b/varisat/src/binary.rs @@ -57,7 +57,7 @@ pub fn simplify_binary<'a>( // This check avoids deleting binary clauses twice if both literals are assigned. if (!lit) < other_lit { let lits = [!lit, other_lit]; - proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(lits[..].into())); + proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(&lits[..])); } } } @@ -69,7 +69,7 @@ pub fn simplify_binary<'a>( // This check avoids deleting binary clauses twice if both literals are assigned. if ctx.part(ProofP).is_active() && !retain && (!lit) < other_lit { let lits = [!lit, other_lit]; - proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(lits[..].into())); + proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(&lits[..])); } retain diff --git a/varisat/src/cdcl.rs b/varisat/src/cdcl.rs index 19fa29a2..948cd63f 100644 --- a/varisat/src/cdcl.rs +++ b/varisat/src/cdcl.rs @@ -67,7 +67,7 @@ pub fn conflict_step<'a>( ctx.borrow(), &ProofStep::AtClause { clause: clause.into(), - propagation_hashes: analyze.clause_hashes().into(), + propagation_hashes: analyze.clause_hashes(), }, ); diff --git a/varisat/src/checker.rs b/varisat/src/checker.rs index f0138a9e..53ea18d7 100644 --- a/varisat/src/checker.rs +++ b/varisat/src/checker.rs @@ -12,7 +12,7 @@ use smallvec::SmallVec; use crate::cnf::CnfFormula; use crate::dimacs::DimacsParser; use crate::lit::{Lit, LitIdx}; -use crate::proof::{clause_hash, ClauseHash, ProofStep}; +use crate::proof::{clause_hash, varisat::Parser, ClauseHash, ProofStep}; mod write_lrat; @@ -26,6 +26,12 @@ pub enum CheckerError { step )] ProofIncomplete { step: u64 }, + #[fail(display = "step {}: Error reading proof file: {}", step, cause)] + IoError { + step: u64, + #[cause] + cause: io::Error, + }, #[fail(display = "step {}: Could not parse proof step: {}", step, cause)] PraseError { step: u64, @@ -714,6 +720,7 @@ impl<'a> Checker<'a> { /// Using this avoids creating a temporary [`CnfFormula`]. pub fn check_proof(&mut self, input: impl io::Read) -> Result<(), CheckerError> { let mut buffer = io::BufReader::new(input); + let mut parser = Parser::default(); while !self.unsat { self.step += 1; @@ -722,15 +729,20 @@ impl<'a> Checker<'a> { log::info!("checking step {}k", self.step / 1000); } - match bincode::deserialize_from(&mut buffer) { + match parser.parse_step(&mut buffer) { Ok(step) => self.check_step(step)?, - Err(err) => match *err { - bincode::ErrorKind::Io(ref io_err) - if io_err.kind() == io::ErrorKind::UnexpectedEof => - { - return Err(CheckerError::ProofIncomplete { step: self.step }) + Err(err) => match err.downcast::() { + Ok(io_err) => { + if io_err.kind() == io::ErrorKind::UnexpectedEof { + return Err(CheckerError::ProofIncomplete { step: self.step }); + } else { + return Err(CheckerError::IoError { + step: self.step, + cause: io_err, + }); + } } - _ => { + Err(err) => { return Err(CheckerError::PraseError { step: self.step, cause: err.into(), diff --git a/varisat/src/clause/reduce.rs b/varisat/src/clause/reduce.rs index 7cd9c686..9c933978 100644 --- a/varisat/src/clause/reduce.rs +++ b/varisat/src/clause/reduce.rs @@ -73,7 +73,7 @@ pub fn reduce_locals<'a>( if ctx.part(ProofP).is_active() { let (alloc, mut ctx) = ctx.split_part(ClauseAllocP); let lits = alloc.clause(*cref).lits(); - proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(lits.into())); + proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(lits)); } cref.remove(); diff --git a/varisat/src/lib.rs b/varisat/src/lib.rs index 7f2d19e4..c2299fbe 100644 --- a/varisat/src/lib.rs +++ b/varisat/src/lib.rs @@ -31,6 +31,7 @@ mod schedule; mod simplify; mod state; mod tmp; +mod vli_enc; mod vec_mut_scan; diff --git a/varisat/src/load.rs b/varisat/src/load.rs index b5c5014e..39208d0f 100644 --- a/varisat/src/load.rs +++ b/varisat/src/load.rs @@ -69,7 +69,7 @@ pub fn load_clause<'a>( for &lit in lits.iter() { if last == Some(!lit) { - proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(lits[..].into())); + proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(lits)); return; } last = Some(lit); @@ -119,7 +119,7 @@ pub fn load_clause<'a>( if clause_is_true { if lits.len() > 1 { - proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(lits[..].into())); + proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(lits)); } return; } diff --git a/varisat/src/proof.rs b/varisat/src/proof.rs index 32fe5773..d2c12538 100644 --- a/varisat/src/proof.rs +++ b/varisat/src/proof.rs @@ -1,10 +1,7 @@ //! Proof generation. -use std::borrow::Cow; use std::io::{self, sink, BufWriter, Write}; -use serde::{Deserialize, Serialize}; - use partial_ref::{partial, PartialRef}; use crate::checker::{Checker, CheckerError, ProofProcessor}; @@ -12,6 +9,9 @@ use crate::context::{Context, ProofP, SolverStateP}; use crate::lit::Lit; use crate::solver::SolverError; +mod drat; +pub mod varisat; + /// Proof formats that can be generated during solving. #[derive(Copy, Clone, Eq, PartialEq, Debug)] pub enum ProofFormat { @@ -46,7 +46,7 @@ pub fn clause_hash(lits: &[Lit]) -> ClauseHash { /// A single proof step. /// /// Represents a mutation of the current formula and a justification for the mutation's validity. -#[derive(Clone, Serialize, Deserialize, Debug)] +#[derive(Clone, Debug)] pub enum ProofStep<'a> { /// Add a clause that is an asymmetric tautoligy (AT). /// @@ -58,8 +58,8 @@ pub enum ProofStep<'a> { /// /// When generating DRAT proofs the second slice is ignored and may be empty. AtClause { - clause: Cow<'a, [Lit]>, - propagation_hashes: Cow<'a, [ClauseHash]>, + clause: &'a [Lit], + propagation_hashes: &'a [ClauseHash], }, /// Unit clauses found by top-level unit-propagation. /// @@ -69,9 +69,9 @@ pub enum ProofStep<'a> { /// for DRAT proofs. /// /// Ignored when generating DRAT proofs. - UnitClauses(Cow<'a, [(Lit, ClauseHash)]>), + UnitClauses(&'a [(Lit, ClauseHash)]), /// Delete a clause consisting of the given literals. - DeleteClause(Cow<'a, [Lit]>), + DeleteClause(&'a [Lit]), } /// Proof generation. @@ -137,70 +137,6 @@ impl<'a> Proof<'a> { None => false, } } - - /// Writes a proof step in our own format. - fn write_varisat_step<'s>(&'s mut self, step: &'s ProofStep<'s>) -> io::Result<()> { - match bincode::serialize_into(&mut self.target, step) { - Ok(()) => Ok(()), - Err(err) => match *err { - bincode::ErrorKind::Io(err) => Err(err), - err => panic!("proof serialization error: {}", err), - }, - } - } - - /// Writes a proof step in DRAT or binary DRAT format. - fn write_drat_step<'s>(&'s mut self, step: &'s ProofStep<'s>) -> io::Result<()> { - match step { - ProofStep::AtClause { clause, .. } => { - self.drat_add_clause()?; - self.drat_literals(&clause)?; - } - ProofStep::DeleteClause(clause) => { - self.drat_delete_clause()?; - self.drat_literals(&clause[..])?; - } - ProofStep::UnitClauses(..) => (), - } - - Ok(()) - } - - /// Writes an add clause step to the DRAT proof. - fn drat_add_clause(&mut self) -> io::Result<()> { - if self.format == Some(ProofFormat::BinaryDrat) { - self.target.write_all(b"a")?; - } - Ok(()) - } - - /// Writes a delete clause step to the DRAT proof. - fn drat_delete_clause(&mut self) -> io::Result<()> { - if self.format == Some(ProofFormat::BinaryDrat) { - self.target.write_all(b"d")?; - } else { - self.target.write_all(b"d ")?; - } - Ok(()) - } - - /// Writes the literals of a clause for a step in a DRAT proof. - fn drat_literals(&mut self, literals: &[Lit]) -> io::Result<()> { - if self.format == Some(ProofFormat::BinaryDrat) { - for &lit in literals { - let drat_code = lit.code() as u64 + 2; - leb128::write::unsigned(&mut self.target, drat_code)?; - } - self.target.write_all(&[0])?; - } else { - for &lit in literals { - itoa::write(&mut self.target, lit.to_dimacs())?; - self.target.write_all(b" ")?; - } - self.target.write_all(b"0\n")?; - } - Ok(()) - } } /// Call when adding an external clause. @@ -226,8 +162,9 @@ pub fn add_step<'a, 's>( let proof = ctx.part_mut(ProofP); let io_result = match proof.format { None => Ok(()), - Some(ProofFormat::Varisat) => proof.write_varisat_step(step), - Some(ProofFormat::Drat) | Some(ProofFormat::BinaryDrat) => proof.write_drat_step(step), + Some(ProofFormat::Varisat) => varisat::write_step(&mut proof.target, step), + Some(ProofFormat::Drat) => drat::write_step(&mut proof.target, step), + Some(ProofFormat::BinaryDrat) => drat::write_binary_step(&mut proof.target, step), }; handle_io_errors(ctx.borrow(), io_result); diff --git a/varisat/src/proof/drat.rs b/varisat/src/proof/drat.rs new file mode 100644 index 00000000..79bf2f53 --- /dev/null +++ b/varisat/src/proof/drat.rs @@ -0,0 +1,58 @@ +use std::io::{self, Write}; + +use crate::lit::Lit; + +use super::ProofStep; + +/// Writes a proof step in DRAT format +pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::Result<()> { + match step { + ProofStep::AtClause { clause, .. } => { + write_literals(target, &clause)?; + } + ProofStep::DeleteClause(clause) => { + target.write_all(b"d ")?; + write_literals(target, &clause[..])?; + } + ProofStep::UnitClauses(..) => (), + } + + Ok(()) +} + +/// Writes a proof step in binary DRAT format +pub fn write_binary_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::Result<()> { + match step { + ProofStep::AtClause { clause, .. } => { + target.write_all(b"a")?; + write_binary_literals(target, &clause)?; + } + ProofStep::DeleteClause(clause) => { + target.write_all(b"d")?; + write_binary_literals(target, &clause[..])?; + } + ProofStep::UnitClauses(..) => (), + } + + Ok(()) +} + +/// Writes the literals of a clause for a step in a DRAT proof. +fn write_literals(target: &mut impl Write, literals: &[Lit]) -> io::Result<()> { + for &lit in literals { + itoa::write(&mut *target, lit.to_dimacs())?; + target.write_all(b" ")?; + } + target.write_all(b"0\n")?; + Ok(()) +} + +/// Writes the literals of a clause for a step in a binary DRAT proof. +fn write_binary_literals(target: &mut impl Write, literals: &[Lit]) -> io::Result<()> { + for &lit in literals { + let drat_code = lit.code() as u64 + 2; + leb128::write::unsigned(target, drat_code)?; + } + target.write_all(&[0])?; + Ok(()) +} diff --git a/varisat/src/proof/varisat.rs b/varisat/src/proof/varisat.rs new file mode 100644 index 00000000..9bcd7712 --- /dev/null +++ b/varisat/src/proof/varisat.rs @@ -0,0 +1,135 @@ +use std::io::{self, BufRead, Write}; + +use failure::Error; + +use crate::lit::Lit; +use crate::vli_enc::{read_u64, write_u64}; + +use super::{ClauseHash, ProofStep}; + +const CODE_AT_CLAUSE: u64 = 0; +const CODE_UNIT_CLAUSES: u64 = 1; +const CODE_DELETE_CLAUSE: u64 = 2; + +/// Writes a proof step in the varisat format +pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::Result<()> { + match step { + ProofStep::AtClause { + clause, + propagation_hashes, + } => { + write_u64(&mut *target, CODE_AT_CLAUSE)?; + write_literals(&mut *target, clause)?; + write_hashes(&mut *target, propagation_hashes)?; + } + + ProofStep::UnitClauses(units) => { + write_u64(&mut *target, CODE_UNIT_CLAUSES)?; + write_unit_clauses(&mut *target, units)?; + } + + ProofStep::DeleteClause(clause) => { + write_u64(&mut *target, CODE_DELETE_CLAUSE)?; + write_literals(&mut *target, clause)?; + } + } + + Ok(()) +} + +#[derive(Default)] +pub struct Parser { + lit_buf: Vec, + hash_buf: Vec, + unit_buf: Vec<(Lit, ClauseHash)>, +} + +impl Parser { + pub fn parse_step<'a>(&'a mut self, source: &mut impl BufRead) -> Result, Error> { + match read_u64(&mut *source)? { + CODE_AT_CLAUSE => { + read_literals(&mut *source, &mut self.lit_buf)?; + read_hashes(&mut *source, &mut self.hash_buf)?; + Ok(ProofStep::AtClause { + clause: &self.lit_buf, + propagation_hashes: &self.hash_buf, + }) + } + CODE_UNIT_CLAUSES => { + read_unit_clauses(&mut *source, &mut self.unit_buf)?; + Ok(ProofStep::UnitClauses(&self.unit_buf)) + } + CODE_DELETE_CLAUSE => { + read_literals(&mut *source, &mut self.lit_buf)?; + Ok(ProofStep::DeleteClause(&self.lit_buf)) + } + _ => failure::bail!("parse error"), + } + } +} + +/// Writes a slice of literals for a varisat proof +fn write_literals(target: &mut impl Write, literals: &[Lit]) -> io::Result<()> { + write_u64(&mut *target, literals.len() as u64)?; + for &lit in literals { + write_u64(&mut *target, lit.code() as u64)?; + } + Ok(()) +} + +/// Read a slice of literals from a varisat proof +fn read_literals(source: &mut impl BufRead, literals: &mut Vec) -> Result<(), io::Error> { + literals.clear(); + let len = read_u64(&mut *source)? as usize; + literals.reserve(len); + for _ in 0..len { + literals.push(Lit::from_code(read_u64(&mut *source)? as usize)); + } + Ok(()) +} + +/// Writes a slice of clause hashes for a varisat proof +fn write_hashes(target: &mut impl Write, hashes: &[ClauseHash]) -> io::Result<()> { + write_u64(&mut *target, hashes.len() as u64)?; + for &hash in hashes { + write_u64(&mut *target, hash as u64)?; + } + Ok(()) +} + +/// Read a slice of clause hashes from a varisat proof +fn read_hashes(source: &mut impl BufRead, hashes: &mut Vec) -> Result<(), io::Error> { + hashes.clear(); + let len = read_u64(&mut *source)? as usize; + hashes.reserve(len); + for _ in 0..len { + hashes.push(read_u64(&mut *source)? as ClauseHash); + } + Ok(()) +} + +/// Writes a slice of unit clauses for a varisat proof +fn write_unit_clauses(target: &mut impl Write, units: &[(Lit, ClauseHash)]) -> io::Result<()> { + write_u64(&mut *target, units.len() as u64)?; + for &(lit, hash) in units { + write_u64(&mut *target, lit.code() as u64)?; + write_u64(&mut *target, hash as u64)?; + } + Ok(()) +} + +/// Read a slice of unit clauses from a varisat proof +fn read_unit_clauses( + source: &mut impl BufRead, + units: &mut Vec<(Lit, ClauseHash)>, +) -> Result<(), io::Error> { + units.clear(); + let len = read_u64(&mut *source)? as usize; + units.reserve(len); + for _ in 0..len { + let lit = Lit::from_code(read_u64(&mut *source)? as usize); + let hash = read_u64(&mut *source)? as ClauseHash; + units.push((lit, hash)); + } + Ok(()) +} diff --git a/varisat/src/simplify.rs b/varisat/src/simplify.rs index 731172f5..e1c72e6e 100644 --- a/varisat/src/simplify.rs +++ b/varisat/src/simplify.rs @@ -55,7 +55,7 @@ pub fn prove_units<'a>( trail.clear(); if !unit_proofs.is_empty() { - proof::add_step(ctx.borrow(), &ProofStep::UnitClauses(unit_proofs.into())); + proof::add_step(ctx.borrow(), &ProofStep::UnitClauses(&unit_proofs)); } } @@ -107,10 +107,7 @@ pub fn simplify<'a>( match assignment.lit_value(lit) { None => new_lits.push(lit), Some(true) => { - proof::add_step( - proof_ctx.borrow(), - &ProofStep::DeleteClause(clause.lits().into()), - ); + proof::add_step(proof_ctx.borrow(), &ProofStep::DeleteClause(clause.lits())); return false; } Some(false) => (), @@ -122,14 +119,11 @@ pub fn simplify<'a>( proof::add_step( proof_ctx.borrow(), &ProofStep::AtClause { - clause: new_lits[..].into(), - propagation_hashes: hash[..].into(), + clause: &new_lits, + propagation_hashes: &hash[..], }, ); - proof::add_step( - proof_ctx.borrow(), - &ProofStep::DeleteClause(clause.lits().into()), - ); + proof::add_step(proof_ctx.borrow(), &ProofStep::DeleteClause(clause.lits())); } match new_lits[..] { diff --git a/varisat/src/vli_enc.rs b/varisat/src/vli_enc.rs new file mode 100644 index 00000000..f41d8142 --- /dev/null +++ b/varisat/src/vli_enc.rs @@ -0,0 +1,134 @@ +//! Variable length integer encoding. +//! +//! This uses a different encoding from the leb128 encoding used for binary DRAT and CLRAT. It uses +//! the same amount of bytes for each input, but is faster to encode and decode. +//! +//! Numbers are encoded like this: +//! ```text +//! 1xxxxxxx for up to 7 bits +//! 01xxxxxx xxxxxxxx for up to 14 bits +//! 001xxxxx xxxxxxxx xxxxxxxx for up to 21 bits +//! ... +//! ``` +//! +//! The x-bits store the number from LSB to MSB. This scheme allows faster encoding and decoding, as +//! the bits are kept consecutive and the length can be determined from the first or first two +//! bytes. +//! +//! The current implementations are not optimal but fast enough to not be the bottleneck when +//! checking proofs. +use std::convert::{TryFrom, TryInto}; +use std::io::{self, BufRead, Write}; + +/// Write an encoded 64 bit number. +pub fn write_u64(target: &mut impl Write, mut value: u64) -> Result<(), io::Error> { + let bits = (64 - value.leading_zeros()) as u32; + let blocks = (bits * (64 / 7)) / 64; + if value < (1 << (8 * 7)) { + value = ((value << 1) | 1) << blocks; + let bytes = unsafe { std::mem::transmute::(value.to_le()) }; + target.write_all(&bytes[..(blocks + 1) as usize]) + } else { + let lo_data = ((value << 1) | 1) << blocks; + let lo_bytes = unsafe { std::mem::transmute::(lo_data.to_le()) }; + let hi_data = value >> (64 - (blocks + 1)); + let hi_bytes = unsafe { std::mem::transmute::(hi_data.to_le()) }; + + target.write_all(&lo_bytes)?; + target.write_all(&hi_bytes[..(blocks as usize) + 1 - 8]) + } +} + +/// Read an encoded 64 bit number, if at least 16 bytes lookahead are available. +fn read_u64_fast(bytes: &[u8; 16]) -> (u64, usize) { + let lo_data = u64::from_le(unsafe { + std::mem::transmute::<[u8; 8], u64>(*<&[u8; 8]>::try_from(&bytes[..8]).unwrap()) + }); + + let len = (lo_data | (1 << 9)).trailing_zeros() + 1; + + if len <= 8 { + let result = lo_data & (!0u64 >> (64 - 8 * len)); + + let result = result >> len; + + (result, len as usize) + } else { + let hi_data = u64::from_le(unsafe { + std::mem::transmute::<[u8; 8], u64>(*<&[u8; 8]>::try_from(&bytes[8..]).unwrap()) + }); + + let hi_data = hi_data & (!0u64 >> (64 - 8 * (len - 8))); + + let result = (lo_data >> len) | (hi_data << (64 - len)); + + (result as u64, len as usize) + } +} + +/// Read an encoded 64 bit number from a buffered reader. +/// +/// This uses [`read_u64_fast`] if the remaining buffer is larger than 16 bytes and falls back to a +/// slower implementation otherwise. +pub fn read_u64(source: &mut impl BufRead) -> Result { + let buf = source.fill_buf()?; + if buf.len() >= 16 { + let next_bytes: &[u8; 16] = (&buf[..16]).try_into().unwrap(); + let (value, advance) = read_u64_fast(next_bytes); + source.consume(advance); + Ok(value) + } else { + let mut scan = 1 << 9; + let mut byte: [u8; 1] = [0]; + let mut begin = 1; + source.read_exact(&mut byte[..])?; + let mut result = byte[0] as u64; + scan |= byte[0] as u64; + if byte[0] == 0 { + begin += 1; + source.read_exact(&mut byte[..])?; + result |= (byte[0] as u64) << 8; + scan |= (byte[0] as u64) << 8; + } + let len = scan.trailing_zeros() + 1; + + result >>= len; + + for i in begin..len { + source.read_exact(&mut byte[..])?; + result |= (byte[0] as u64) << (8 * i - len); + } + + Ok(result as u64) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + use proptest::prelude::*; + + proptest! { + #[test] + fn roundtrip ( + numbers in prop::collection::vec(prop::num::u64::ANY, 0..10_000) + ) { + let mut buf = vec![]; + + for &num in numbers.iter() { + write_u64(&mut buf, num)?; + } + + let mut read = std::io::BufReader::with_capacity(128, &buf[..]); + + let mut out = vec![]; + + while let Ok(num) = read_u64(&mut read) { + out.push(num) + } + + prop_assert_eq!(numbers, out); + } + } +} From 6e7e13c4169422ea9f5e0c76a6128316d4abf753 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 13 May 2019 15:50:22 +0200 Subject: [PATCH 3/3] Dynamically adjust the hash size for varisat proofs This resolves #40 --- varisat/src/checker.rs | 52 ++++++++++++++- varisat/src/proof.rs | 116 ++++++++++++++++++++++++++++++++-- varisat/src/proof/drat.rs | 4 +- varisat/src/proof/map_step.rs | 60 ++++++++++++++++++ varisat/src/proof/varisat.rs | 10 +++ 5 files changed, 231 insertions(+), 11 deletions(-) create mode 100644 varisat/src/proof/map_step.rs diff --git a/varisat/src/checker.rs b/varisat/src/checker.rs index 53ea18d7..fe36277c 100644 --- a/varisat/src/checker.rs +++ b/varisat/src/checker.rs @@ -195,7 +195,6 @@ struct TraceItem { } /// A checker for unsatisfiability proofs in the native varisat format. -#[derive(Default)] pub struct Checker<'a> { /// Current step number. step: u64, @@ -228,6 +227,30 @@ pub struct Checker<'a> { unit_conflict: Option<[u64; 2]>, /// Temporary storage for literals. tmp: Vec, + /// How many bits are used for storing clause hashes. + hash_bits: u32, +} + +impl<'a> Default for Checker<'a> { + fn default() -> Checker<'a> { + Checker { + step: 0, + next_clause_id: 0, + literal_buffer: vec![], + garbage_size: 0, + clauses: Default::default(), + unit_clauses: vec![], + trail: vec![], + unsat: false, + trace: vec![], + trace_edges: vec![], + trace_ids: vec![], + processors: vec![], + unit_conflict: None, + tmp: vec![], + hash_bits: 64, + } + } } impl<'a> Checker<'a> { @@ -304,6 +327,12 @@ impl<'a> Checker<'a> { Ok(()) } + /// Compute a clause hash of the current bit size + fn clause_hash(&self, lits: &[Lit]) -> ClauseHash { + let shift_bits = ClauseHash::max_value().count_ones() - self.hash_bits; + clause_hash(lits) >> shift_bits + } + /// Value of a literal if known from unit clauses. fn lit_value(&self, lit: Lit) -> Option<(bool, UnitClause)> { self.unit_clauses @@ -329,7 +358,7 @@ impl<'a> Checker<'a> { } [lit] => self.store_unit_clause(lit), _ => { - let hash = clause_hash(&lits); + let hash = self.clause_hash(&lits); let candidates = self.clauses.entry(hash).or_default(); @@ -416,7 +445,7 @@ impl<'a> Checker<'a> { }); } - let hash = clause_hash(lits); + let hash = self.clause_hash(lits); let candidates = self.clauses.entry(hash).or_default(); @@ -481,6 +510,19 @@ impl<'a> Checker<'a> { self.garbage_size = 0; } + /// Recompute all clause hashes + fn rehash(&mut self) { + let mut old_clauses = replace(&mut self.clauses, Default::default()); + + for (_, mut candidates) in old_clauses.drain() { + for clause in candidates.drain() { + let hash = self.clause_hash(clause.lits.slice(&self.literal_buffer)); + let candidates = self.clauses.entry(hash).or_default(); + candidates.push(clause); + } + } + } + /// Check whether a clause is implied by clauses of the given hashes. /// /// `lits` must be sorted and free of duplicates. @@ -697,6 +739,10 @@ impl<'a> Checker<'a> { } } } + ProofStep::ChangeHashBits(bits) => { + self.hash_bits = bits; + self.rehash(); + } } Ok(()) diff --git a/varisat/src/proof.rs b/varisat/src/proof.rs index d2c12538..40075731 100644 --- a/varisat/src/proof.rs +++ b/varisat/src/proof.rs @@ -10,6 +10,7 @@ use crate::lit::Lit; use crate::solver::SolverError; mod drat; +mod map_step; pub mod varisat; /// Proof formats that can be generated during solving. @@ -72,6 +73,33 @@ pub enum ProofStep<'a> { UnitClauses(&'a [(Lit, ClauseHash)]), /// Delete a clause consisting of the given literals. DeleteClause(&'a [Lit]), + /// Change the number of clause hash bits used + ChangeHashBits(u32), +} + +impl<'a> ProofStep<'a> { + /// Number of added or removed clauses. + pub fn clause_count_delta(&self) -> isize { + match self { + ProofStep::AtClause { clause, .. } => { + if clause.len() > 1 { + 1 + } else { + 0 + } + } + ProofStep::DeleteClause(clause) => { + if clause.len() > 1 { + -1 + } else { + 0 + } + } + + ProofStep::UnitClauses(..) => 0, + ProofStep::ChangeHashBits(..) => 0, + } + } } /// Proof generation. @@ -79,6 +107,15 @@ pub struct Proof<'a> { format: Option, target: BufWriter>, checker: Option>, + map_step: map_step::MapStep, + /// How many bits are used for storing clause hashes. + hash_bits: u32, + /// How many clauses are currently in the db. + /// + /// This is used to pick a good number of hash_bits + clause_count: isize, + /// Whether we're finished with the initial loading of clauses. + initial_load_complete: bool, } impl<'a> Default for Proof<'a> { @@ -87,6 +124,10 @@ impl<'a> Default for Proof<'a> { format: None, target: BufWriter::new(Box::new(sink())), checker: None, + map_step: Default::default(), + hash_bits: 64, + clause_count: 0, + initial_load_complete: false, } } } @@ -150,6 +191,9 @@ pub fn add_clause<'a>( let result = checker.add_clause(clause); handle_self_check_result(ctx.borrow(), result); } + if clause.len() > 1 { + ctx.part_mut(ProofP).clause_count += 1; + } } /// Add a step to the proof. @@ -160,20 +204,80 @@ pub fn add_step<'a, 's>( step: &'s ProofStep<'s>, ) { let proof = ctx.part_mut(ProofP); + + // This is a crude hack, as delete steps are the only ones emitted during loading. We need this + // to avoid triggering a hash size adjustment during the initial load. The checker has already + // loaded the complete formula, so our clause count doesn't match the checker's and we could + // cause way too many collisions, causing the checker to have quadratic runtime. + match step { + ProofStep::DeleteClause(..) => {} + _ => proof.initial_load_complete = true, + } + let io_result = match proof.format { + Some(ProofFormat::Varisat) => write_varisat_step(ctx.borrow(), step), + Some(ProofFormat::Drat) => { + let step = proof.map_step.map(step, |lit| lit, |hash| hash); + drat::write_step(&mut proof.target, &step) + } + Some(ProofFormat::BinaryDrat) => { + let step = proof.map_step.map(step, |lit| lit, |hash| hash); + drat::write_binary_step(&mut proof.target, &step) + } None => Ok(()), - Some(ProofFormat::Varisat) => varisat::write_step(&mut proof.target, step), - Some(ProofFormat::Drat) => drat::write_step(&mut proof.target, step), - Some(ProofFormat::BinaryDrat) => drat::write_binary_step(&mut proof.target, step), }; + if io_result.is_ok() { + let proof = ctx.part_mut(ProofP); + if let Some(checker) = &mut proof.checker { + let step = proof.map_step.map(step, |lit| lit, |hash| hash); + let result = checker.check_step(step); + handle_self_check_result(ctx.borrow(), result); + } + } + handle_io_errors(ctx.borrow(), io_result); +} +/// Write a step using our native format +fn write_varisat_step<'a, 's>( + mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP), + step: &'s ProofStep<'s>, +) -> io::Result<()> { let proof = ctx.part_mut(ProofP); - if let Some(checker) = &mut proof.checker { - let result = checker.check_step(step.clone()); - handle_self_check_result(ctx.borrow(), result); + + proof.clause_count += step.clause_count_delta(); + + let mut rehash = false; + // Should we change the hash size? + while proof.clause_count > (1 << (proof.hash_bits / 2)) { + proof.hash_bits += 2; + rehash = true; + } + if proof.initial_load_complete { + while proof.hash_bits > 6 && proof.clause_count * 4 < (1 << (proof.hash_bits / 2)) { + proof.hash_bits -= 2; + rehash = true; + } + } + + if rehash { + varisat::write_step( + &mut proof.target, + &ProofStep::ChangeHashBits(proof.hash_bits), + )?; + } + + let shift_bits = ClauseHash::max_value().count_ones() - proof.hash_bits; + + let map_hash = |hash| hash >> shift_bits; + let step = proof.map_step.map(step, |lit| lit, map_hash); + + if proof.format == Some(ProofFormat::Varisat) { + varisat::write_step(&mut proof.target, &step)?; } + + Ok(()) } /// Flush buffers used for writing proof steps. diff --git a/varisat/src/proof/drat.rs b/varisat/src/proof/drat.rs index 79bf2f53..465b8889 100644 --- a/varisat/src/proof/drat.rs +++ b/varisat/src/proof/drat.rs @@ -14,7 +14,7 @@ pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::R target.write_all(b"d ")?; write_literals(target, &clause[..])?; } - ProofStep::UnitClauses(..) => (), + ProofStep::UnitClauses(..) | ProofStep::ChangeHashBits(..) => (), } Ok(()) @@ -31,7 +31,7 @@ pub fn write_binary_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) - target.write_all(b"d")?; write_binary_literals(target, &clause[..])?; } - ProofStep::UnitClauses(..) => (), + ProofStep::UnitClauses(..) | ProofStep::ChangeHashBits(..) => (), } Ok(()) diff --git a/varisat/src/proof/map_step.rs b/varisat/src/proof/map_step.rs new file mode 100644 index 00000000..fae20c2e --- /dev/null +++ b/varisat/src/proof/map_step.rs @@ -0,0 +1,60 @@ +//! Maps literals and hashes of clause steps between the solver and the checker. + +use crate::lit::Lit; + +use super::{ClauseHash, ProofStep}; + +/// Maps literals and hashes of clause steps between the solver and the checker. +#[derive(Default)] +pub struct MapStep { + lit_buf: Vec, + hash_buf: Vec, + unit_buf: Vec<(Lit, ClauseHash)>, +} + +impl MapStep { + pub fn map<'s, 'a, 'b>( + &'a mut self, + step: &ProofStep<'b>, + map_lit: impl Fn(Lit) -> Lit, + map_hash: impl Fn(ClauseHash) -> ClauseHash, + ) -> ProofStep<'s> + where + 'a: 's, + 'b: 's, + { + match step { + ProofStep::AtClause { + clause, + propagation_hashes, + } => { + self.lit_buf.clear(); + self.lit_buf.extend(clause.iter().cloned().map(map_lit)); + self.hash_buf.clear(); + self.hash_buf + .extend(propagation_hashes.iter().cloned().map(map_hash)); + ProofStep::AtClause { + clause: &self.lit_buf, + propagation_hashes: &self.hash_buf, + } + } + + ProofStep::UnitClauses(units) => { + self.unit_buf.clear(); + self.unit_buf.extend( + units + .iter() + .map(|&(lit, hash)| (map_lit(lit), map_hash(hash))), + ); + ProofStep::UnitClauses(&self.unit_buf) + } + + ProofStep::DeleteClause(clause) => { + self.lit_buf.clear(); + self.lit_buf.extend(clause.iter().cloned().map(map_lit)); + ProofStep::DeleteClause(&self.lit_buf) + } + ProofStep::ChangeHashBits(..) => step.clone(), + } + } +} diff --git a/varisat/src/proof/varisat.rs b/varisat/src/proof/varisat.rs index 9bcd7712..29bab4eb 100644 --- a/varisat/src/proof/varisat.rs +++ b/varisat/src/proof/varisat.rs @@ -10,6 +10,7 @@ use super::{ClauseHash, ProofStep}; const CODE_AT_CLAUSE: u64 = 0; const CODE_UNIT_CLAUSES: u64 = 1; const CODE_DELETE_CLAUSE: u64 = 2; +const CODE_CHANGE_HASH_BITS: u64 = 3; /// Writes a proof step in the varisat format pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::Result<()> { @@ -32,6 +33,11 @@ pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::R write_u64(&mut *target, CODE_DELETE_CLAUSE)?; write_literals(&mut *target, clause)?; } + + ProofStep::ChangeHashBits(bits) => { + write_u64(&mut *target, CODE_CHANGE_HASH_BITS)?; + write_u64(&mut *target, *bits as u64)?; + } } Ok(()) @@ -63,6 +69,10 @@ impl Parser { read_literals(&mut *source, &mut self.lit_buf)?; Ok(ProofStep::DeleteClause(&self.lit_buf)) } + CODE_CHANGE_HASH_BITS => { + let bits = read_u64(&mut *source)? as u32; + Ok(ProofStep::ChangeHashBits(bits)) + } _ => failure::bail!("parse error"), } }