From 8a5b5ab90f08f921ac8c6346d4666ba645007ec8 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 14 May 2019 08:55:31 +0200 Subject: [PATCH 1/5] Check clause deletions in proofs This is needed to check proofs for satisfiable instances. Part of #30 --- varisat/src/binary.rs | 18 ++- varisat/src/cdcl.rs | 1 + varisat/src/checker.rs | 238 +++++++++++++++++++++++++++++----- varisat/src/clause/header.rs | 5 + varisat/src/clause/reduce.rs | 10 +- varisat/src/load.rs | 18 ++- varisat/src/proof.rs | 25 +++- varisat/src/proof/drat.rs | 4 +- varisat/src/proof/map_step.rs | 11 +- varisat/src/proof/varisat.rs | 60 +++++++-- varisat/src/simplify.rs | 28 +++- 11 files changed, 355 insertions(+), 63 deletions(-) diff --git a/varisat/src/binary.rs b/varisat/src/binary.rs index eda7c731..8e469c25 100644 --- a/varisat/src/binary.rs +++ b/varisat/src/binary.rs @@ -3,7 +3,7 @@ use partial_ref::{partial, PartialRef}; use crate::context::{AssignmentP, BinaryClausesP, Context, ProofP, SolverStateP}; -use crate::proof::{self, ProofStep}; +use crate::proof::{self, DeleteClauseProof, ProofStep}; use crate::lit::Lit; @@ -57,7 +57,13 @@ 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[..])); + proof::add_step( + ctx.borrow(), + &ProofStep::DeleteClause { + clause: &lits[..], + proof: DeleteClauseProof::Satisfied, + }, + ); } } } @@ -69,7 +75,13 @@ 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[..])); + proof::add_step( + ctx.borrow(), + &ProofStep::DeleteClause { + clause: &lits[..], + proof: DeleteClauseProof::Satisfied, + }, + ); } retain diff --git a/varisat/src/cdcl.rs b/varisat/src/cdcl.rs index 948cd63f..1be1c8bb 100644 --- a/varisat/src/cdcl.rs +++ b/varisat/src/cdcl.rs @@ -66,6 +66,7 @@ pub fn conflict_step<'a>( proof::add_step( ctx.borrow(), &ProofStep::AtClause { + redundant: clause.len() > 2, clause: clause.into(), propagation_hashes: analyze.clause_hashes(), }, diff --git a/varisat/src/checker.rs b/varisat/src/checker.rs index fe36277c..21685dc0 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, varisat::Parser, ClauseHash, ProofStep}; +use crate::proof::{clause_hash, varisat::Parser, ClauseHash, DeleteClauseProof, ProofStep}; mod write_lrat; @@ -33,7 +33,7 @@ pub enum CheckerError { cause: io::Error, }, #[fail(display = "step {}: Could not parse proof step: {}", step, cause)] - PraseError { + ParseError { step: u64, #[cause] cause: Error, @@ -44,6 +44,8 @@ pub enum CheckerError { ClauseNotFound { step: u64, hash: ClauseHash }, #[fail(display = "step {}: Checking proof for {:?} failed", step, clause)] ClauseCheckFailed { step: u64, clause: Vec }, + #[fail(display = "step {}: Checking proof failed", step)] + CheckFailed { step: u64 }, #[fail(display = "Error in proof processor: {}", cause)] ProofProcessorError { #[cause] @@ -163,11 +165,11 @@ impl ClauseLits { struct Clause { /// LRAT clause id. id: u64, - /// How often the clause is present. + /// How often the clause is present as irred., red. clause. /// /// For checking the formula is a multiset of clauses. This is necessary as the generating /// solver might not check for duplicated clauses. - ref_count: u32, + ref_count: [u32; 2], /// Clause's literals. lits: ClauseLits, } @@ -229,6 +231,13 @@ pub struct Checker<'a> { tmp: Vec, /// How many bits are used for storing clause hashes. hash_bits: u32, + /// Last added irredundant clause. + /// + /// Empty if no such clause was added since the last clause deletion. So if this is non-empty + /// the clause is present and irredundant. + /// + /// Sorted and free of duplicates. + previous_irred_clause: Vec, } impl<'a> Default for Checker<'a> { @@ -249,6 +258,7 @@ impl<'a> Default for Checker<'a> { unit_conflict: None, tmp: vec![], hash_bits: 64, + previous_irred_clause: vec![], } } } @@ -281,7 +291,7 @@ impl<'a> Checker<'a> { tmp.sort_unstable(); tmp.dedup(); - let (id, added) = self.store_clause(&tmp); + let (id, added) = self.store_clause(&tmp, false); self.tmp = tmp; @@ -347,7 +357,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: &[Lit]) -> (u64, bool) { + fn store_clause(&mut self, lits: &[Lit], redundant: bool) -> (u64, bool) { match lits[..] { [] => { let id = self.next_clause_id; @@ -364,19 +374,20 @@ impl<'a> Checker<'a> { for candidate in candidates.iter_mut() { if candidate.lits.slice(&self.literal_buffer) == &lits[..] { - candidate.ref_count = candidate - .ref_count - .checked_add(1) - .expect("ref_count overflow"); + let ref_count = &mut candidate.ref_count[redundant as usize]; + *ref_count = ref_count.checked_add(1).expect("ref_count overflow"); return (candidate.id, false); } } let id = self.next_clause_id; + let mut ref_count = [0, 0]; + ref_count[redundant as usize] += 1; + candidates.push(Clause { id, - ref_count: 1, + ref_count, lits: ClauseLits::new(&lits, &mut self.literal_buffer), }); @@ -437,7 +448,11 @@ impl<'a> Checker<'a> { /// `lits` must be sorted and free of duplicates. /// /// Returns the id of the clause if the clause's ref_count became zero. - fn delete_clause(&mut self, lits: &[Lit]) -> Result, CheckerError> { + fn delete_clause( + &mut self, + lits: &[Lit], + redundant: bool, + ) -> Result, CheckerError> { if lits.len() < 2 { return Err(CheckerError::InvalidDelete { step: self.step, @@ -450,6 +465,7 @@ impl<'a> Checker<'a> { let candidates = self.clauses.entry(hash).or_default(); let mut deleted = false; + let mut found = false; let mut result = None; @@ -457,17 +473,26 @@ impl<'a> Checker<'a> { let garbage_size = &mut self.garbage_size; candidates.retain(|candidate| { - if deleted || candidate.lits.slice(literal_buffer) != lits { + if found || 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); - false - } else { + found = true; + let ref_count = &mut candidate.ref_count[redundant as usize]; + + if *ref_count == 0 { true + } else { + deleted = true; + + *ref_count -= 1; + + if candidate.ref_count == [0, 0] { + *garbage_size += candidate.lits.buffer_used(); + result = Some(candidate.id); + false + } else { + true + } } } }); @@ -477,6 +502,7 @@ impl<'a> Checker<'a> { } if !deleted { + // TODO differentiate between not found and red/irred mismatch return Err(CheckerError::InvalidDelete { step: self.step, clause: lits.to_owned(), @@ -668,10 +694,47 @@ impl<'a> Checker<'a> { } } + /// Check whether a given clause is subsumed by the last added irredundant clause. + /// + /// `lits` must be sorted and free of duplicates. + fn subsumed_by_previous_irred_clause(&self, lits: &[Lit]) -> bool { + if self.previous_irred_clause.is_empty() { + // Here empty doesn't mean empty clause but no clause + return false; + } + let mut subset = &self.previous_irred_clause[..]; + let mut superset = lits; + + let mut strict = false; + + while let Some((&sub_min, sub_rest)) = subset.split_first() { + if let Some((&super_min, super_rest)) = superset.split_first() { + if sub_min < super_min { + // sub_min is not in superset + return false; + } else if sub_min > super_min { + // super_min is not in subset, skip it + superset = super_rest; + strict = true; + } else { + // sub_min == super_min, go to next element + superset = super_rest; + subset = sub_rest; + } + } else { + // sub_min is not in superset + return false; + } + } + strict |= !superset.is_empty(); + strict + } + /// Check a single proof step pub(crate) fn check_step(&mut self, step: ProofStep) -> Result<(), CheckerError> { match step { ProofStep::AtClause { + redundant, clause, propagation_hashes, } => { @@ -684,7 +747,12 @@ impl<'a> Checker<'a> { self.check_clause_with_hashes(&tmp, &*propagation_hashes)?; - let (id, added) = self.store_clause(&tmp); + let (id, added) = self.store_clause(&tmp, redundant); + + if !redundant { + self.previous_irred_clause.clear(); + self.previous_irred_clause.extend_from_slice(&tmp); + } if added { Self::process_step( @@ -699,7 +767,7 @@ impl<'a> Checker<'a> { self.tmp = tmp; } - ProofStep::DeleteClause(clause) => { + ProofStep::DeleteClause { clause, proof } => { let mut tmp = replace(&mut self.tmp, vec![]); tmp.clear(); tmp.extend_from_slice(&clause); @@ -707,7 +775,31 @@ impl<'a> Checker<'a> { tmp.sort_unstable(); tmp.dedup(); - if let Some(id) = self.delete_clause(&tmp)? { + let redundant = proof == DeleteClauseProof::Redundant; + + match proof { + DeleteClauseProof::Redundant => (), + DeleteClauseProof::Satisfied => { + if !tmp.iter().any(|&lit| { + if let Some((true, _)) = self.lit_value(lit) { + true + } else { + false + } + }) { + return Err(CheckerError::CheckFailed { step: self.step }); + } + } + DeleteClauseProof::Simplified => { + if !self.subsumed_by_previous_irred_clause(&tmp) { + return Err(CheckerError::CheckFailed { step: self.step }); + } + } + } + + self.previous_irred_clause.clear(); + + if let Some(id) = self.delete_clause(&tmp, redundant)? { Self::process_step( &mut self.processors, &CheckedProofStep::DeleteClause { @@ -789,7 +881,7 @@ impl<'a> Checker<'a> { } } Err(err) => { - return Err(CheckerError::PraseError { + return Err(CheckerError::ParseError { step: self.step, cause: err.into(), }) @@ -863,7 +955,10 @@ mod tests { ]) .unwrap(); - match checker.check_step(ProofStep::DeleteClause(lits![-5, 4][..].into())) { + match checker.check_step(ProofStep::DeleteClause { + clause: &lits![-5, 4], + proof: DeleteClauseProof::Redundant, + }) { Err(CheckerError::InvalidDelete { .. }) => (), _ => panic!("expected InvalidDelete error"), } @@ -877,26 +972,39 @@ mod tests { .add_formula(&cnf_formula![ 1, 2, 3; 1, 2, 3; + 1; ]) .unwrap(); let lits = &lits![1, 2, 3][..]; checker - .check_step(ProofStep::DeleteClause(lits.into())) + .check_step(ProofStep::DeleteClause { + clause: lits, + proof: DeleteClauseProof::Satisfied, + }) .unwrap(); checker.add_clause(lits).unwrap(); checker - .check_step(ProofStep::DeleteClause(lits.into())) + .check_step(ProofStep::DeleteClause { + clause: lits, + proof: DeleteClauseProof::Satisfied, + }) .unwrap(); checker - .check_step(ProofStep::DeleteClause(lits.into())) + .check_step(ProofStep::DeleteClause { + clause: lits, + proof: DeleteClauseProof::Satisfied, + }) .unwrap(); - match checker.check_step(ProofStep::DeleteClause(lits.into())) { + match checker.check_step(ProofStep::DeleteClause { + clause: lits, + proof: DeleteClauseProof::Satisfied, + }) { Err(CheckerError::InvalidDelete { .. }) => (), _ => panic!("expected InvalidDelete error"), } @@ -912,6 +1020,7 @@ mod tests { .unwrap(); match checker.check_step(ProofStep::AtClause { + redundant: false, clause: [][..].into(), propagation_hashes: [0][..].into(), }) { @@ -930,6 +1039,7 @@ mod tests { .unwrap(); match checker.check_step(ProofStep::AtClause { + redundant: false, clause: [][..].into(), propagation_hashes: [][..].into(), }) { @@ -938,6 +1048,76 @@ mod tests { } } + #[test] + fn delete_clause_not_redundant() { + let mut checker = Checker::new(); + checker + .add_formula(&cnf_formula![ + 1, 2, 3; + ]) + .unwrap(); + + match checker.check_step(ProofStep::DeleteClause { + clause: &lits![1, 2, 3], + proof: DeleteClauseProof::Redundant, + }) { + Err(CheckerError::CheckFailed { .. }) => (), + _ => panic!("expected CheckFailed error"), + } + } + + #[test] + fn delete_clause_not_satisfied() { + let mut checker = Checker::new(); + checker + .add_formula(&cnf_formula![ + 1, 2, 3; + -2; + 4; + ]) + .unwrap(); + + match checker.check_step(ProofStep::DeleteClause { + clause: &lits![1, 2, 3], + proof: DeleteClauseProof::Satisfied, + }) { + Err(CheckerError::CheckFailed { .. }) => (), + _ => panic!("expected CheckFailed error"), + } + } + + #[test] + fn delete_clause_not_simplified() { + let mut checker = Checker::new(); + checker + .add_formula(&cnf_formula![ + 1, 2, 3; + -3, 4; + ]) + .unwrap(); + + let hashes = [ + checker.clause_hash(&lits![1, 2, 3]), + checker.clause_hash(&lits![-3, 4]), + ]; + + checker + .check_step(ProofStep::AtClause { + redundant: false, + clause: &lits![1, 2, 4], + propagation_hashes: &hashes[..], + }) + .unwrap(); + + match checker.check_step(ProofStep::DeleteClause { + clause: &lits![1, 2, 3], + proof: DeleteClauseProof::Simplified, + }) { + Err(CheckerError::CheckFailed { .. }) => (), + _ => panic!("expected CheckFailed error"), + } + } + proptest! { #[test] fn checked_unsat_via_dimacs(formula in sgen_unsat_formula(1..7usize)) { diff --git a/varisat/src/clause/header.rs b/varisat/src/clause/header.rs index a817d40e..56994fe3 100644 --- a/varisat/src/clause/header.rs +++ b/varisat/src/clause/header.rs @@ -79,6 +79,11 @@ impl ClauseHeader { *word = (*word & !(TIER_MASK << TIER_OFFSET)) | ((tier as LitIdx) << TIER_OFFSET); } + /// Whether the clause is redundant. + pub fn redundant(&self) -> bool { + self.tier() != Tier::Irred + } + /// Whether the clause is marked. /// /// The mark is a temporary bit that can be set by various routines, but should always be reset diff --git a/varisat/src/clause/reduce.rs b/varisat/src/clause/reduce.rs index 9c933978..e576ccd2 100644 --- a/varisat/src/clause/reduce.rs +++ b/varisat/src/clause/reduce.rs @@ -8,7 +8,7 @@ use partial_ref::{partial, PartialRef}; use crate::context::{ AssignmentP, ClauseAllocP, ClauseDbP, Context, ImplGraphP, ProofP, SolverStateP, WatchlistsP, }; -use crate::proof::{self, ProofStep}; +use crate::proof::{self, DeleteClauseProof, ProofStep}; use crate::vec_mut_scan::VecMutScan; @@ -73,7 +73,13 @@ 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)); + proof::add_step( + ctx.borrow(), + &ProofStep::DeleteClause { + clause: lits, + proof: DeleteClauseProof::Redundant, + }, + ); } cref.remove(); diff --git a/varisat/src/load.rs b/varisat/src/load.rs index 39208d0f..5a2b22a8 100644 --- a/varisat/src/load.rs +++ b/varisat/src/load.rs @@ -7,7 +7,7 @@ use crate::context::{ ProofP, SolverStateP, TmpDataP, TrailP, VsidsP, WatchlistsP, }; use crate::lit::Lit; -use crate::proof::{self, ProofStep}; +use crate::proof::{self, DeleteClauseProof, ProofStep}; use crate::prop::{assignment, full_restart, Reason}; use crate::simplify::resurrect_unit; use crate::state::SatState; @@ -69,7 +69,13 @@ pub fn load_clause<'a>( for &lit in lits.iter() { if last == Some(!lit) { - proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(lits)); + proof::add_step( + ctx.borrow(), + &ProofStep::DeleteClause { + clause: lits, + proof: DeleteClauseProof::Satisfied, + }, + ); return; } last = Some(lit); @@ -119,7 +125,13 @@ pub fn load_clause<'a>( if clause_is_true { if lits.len() > 1 { - proof::add_step(ctx.borrow(), &ProofStep::DeleteClause(lits)); + proof::add_step( + ctx.borrow(), + &ProofStep::DeleteClause { + clause: lits, + proof: DeleteClauseProof::Satisfied, + }, + ); } return; } diff --git a/varisat/src/proof.rs b/varisat/src/proof.rs index 40075731..25da715d 100644 --- a/varisat/src/proof.rs +++ b/varisat/src/proof.rs @@ -44,10 +44,23 @@ pub fn clause_hash(lits: &[Lit]) -> ClauseHash { hash } +/// Justifications for a simple clause deletion. +#[derive(Copy, Clone, PartialEq, Eq, Debug)] +pub enum DeleteClauseProof { + /// The clause is known to be redundant. + Redundant, + /// The clause is irred and subsumed by the clause added in the previous step. + Simplified, + /// The clause contains a true literal. + /// + /// Also used to justify deletion of tautological clauses. + Satisfied, +} + /// A single proof step. /// /// Represents a mutation of the current formula and a justification for the mutation's validity. -#[derive(Clone, Debug)] +#[derive(Copy, Clone, Debug)] pub enum ProofStep<'a> { /// Add a clause that is an asymmetric tautoligy (AT). /// @@ -59,6 +72,7 @@ pub enum ProofStep<'a> { /// /// When generating DRAT proofs the second slice is ignored and may be empty. AtClause { + redundant: bool, clause: &'a [Lit], propagation_hashes: &'a [ClauseHash], }, @@ -72,7 +86,10 @@ pub enum ProofStep<'a> { /// Ignored when generating DRAT proofs. UnitClauses(&'a [(Lit, ClauseHash)]), /// Delete a clause consisting of the given literals. - DeleteClause(&'a [Lit]), + DeleteClause { + clause: &'a [Lit], + proof: DeleteClauseProof, + }, /// Change the number of clause hash bits used ChangeHashBits(u32), } @@ -88,7 +105,7 @@ impl<'a> ProofStep<'a> { 0 } } - ProofStep::DeleteClause(clause) => { + ProofStep::DeleteClause { clause, .. } => { if clause.len() > 1 { -1 } else { @@ -210,7 +227,7 @@ pub fn add_step<'a, 's>( // 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(..) => {} + ProofStep::DeleteClause { .. } => {} _ => proof.initial_load_complete = true, } diff --git a/varisat/src/proof/drat.rs b/varisat/src/proof/drat.rs index 465b8889..29cd9edc 100644 --- a/varisat/src/proof/drat.rs +++ b/varisat/src/proof/drat.rs @@ -10,7 +10,7 @@ pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::R ProofStep::AtClause { clause, .. } => { write_literals(target, &clause)?; } - ProofStep::DeleteClause(clause) => { + ProofStep::DeleteClause { clause, .. } => { target.write_all(b"d ")?; write_literals(target, &clause[..])?; } @@ -27,7 +27,7 @@ pub fn write_binary_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) - target.write_all(b"a")?; write_binary_literals(target, &clause)?; } - ProofStep::DeleteClause(clause) => { + ProofStep::DeleteClause { clause, .. } => { target.write_all(b"d")?; write_binary_literals(target, &clause[..])?; } diff --git a/varisat/src/proof/map_step.rs b/varisat/src/proof/map_step.rs index fae20c2e..10aed4f1 100644 --- a/varisat/src/proof/map_step.rs +++ b/varisat/src/proof/map_step.rs @@ -23,8 +23,9 @@ impl MapStep { 'a: 's, 'b: 's, { - match step { + match *step { ProofStep::AtClause { + redundant, clause, propagation_hashes, } => { @@ -34,6 +35,7 @@ impl MapStep { self.hash_buf .extend(propagation_hashes.iter().cloned().map(map_hash)); ProofStep::AtClause { + redundant, clause: &self.lit_buf, propagation_hashes: &self.hash_buf, } @@ -49,10 +51,13 @@ impl MapStep { ProofStep::UnitClauses(&self.unit_buf) } - ProofStep::DeleteClause(clause) => { + ProofStep::DeleteClause { clause, proof } => { self.lit_buf.clear(); self.lit_buf.extend(clause.iter().cloned().map(map_lit)); - ProofStep::DeleteClause(&self.lit_buf) + ProofStep::DeleteClause { + clause: &self.lit_buf, + proof, + } } ProofStep::ChangeHashBits(..) => step.clone(), } diff --git a/varisat/src/proof/varisat.rs b/varisat/src/proof/varisat.rs index 29bab4eb..d5e99323 100644 --- a/varisat/src/proof/varisat.rs +++ b/varisat/src/proof/varisat.rs @@ -5,21 +5,29 @@ use failure::Error; use crate::lit::Lit; use crate::vli_enc::{read_u64, write_u64}; -use super::{ClauseHash, ProofStep}; +use super::{ClauseHash, DeleteClauseProof, 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; +const CODE_AT_CLAUSE_RED: u64 = 0; +const CODE_AT_CLAUSE_IRRED: u64 = 1; +const CODE_UNIT_CLAUSES: u64 = 2; +const CODE_DELETE_CLAUSE_REDUNDANT: u64 = 3; +const CODE_DELETE_CLAUSE_SIMPLIFIED: u64 = 4; +const CODE_DELETE_CLAUSE_SATISFIED: u64 = 5; +const CODE_CHANGE_HASH_BITS: u64 = 6; /// 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 { + match *step { ProofStep::AtClause { + redundant, clause, propagation_hashes, } => { - write_u64(&mut *target, CODE_AT_CLAUSE)?; + if redundant { + write_u64(&mut *target, CODE_AT_CLAUSE_RED)?; + } else { + write_u64(&mut *target, CODE_AT_CLAUSE_IRRED)?; + } write_literals(&mut *target, clause)?; write_hashes(&mut *target, propagation_hashes)?; } @@ -29,14 +37,25 @@ pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::R write_unit_clauses(&mut *target, units)?; } - ProofStep::DeleteClause(clause) => { - write_u64(&mut *target, CODE_DELETE_CLAUSE)?; + ProofStep::DeleteClause { clause, proof } => { + match proof { + DeleteClauseProof::Redundant => { + write_u64(&mut *target, CODE_DELETE_CLAUSE_REDUNDANT)?; + } + DeleteClauseProof::Simplified => { + write_u64(&mut *target, CODE_DELETE_CLAUSE_SIMPLIFIED)?; + } + DeleteClauseProof::Satisfied => { + write_u64(&mut *target, CODE_DELETE_CLAUSE_SATISFIED)?; + } + } + write_literals(&mut *target, clause)?; } ProofStep::ChangeHashBits(bits) => { write_u64(&mut *target, CODE_CHANGE_HASH_BITS)?; - write_u64(&mut *target, *bits as u64)?; + write_u64(&mut *target, bits as u64)?; } } @@ -52,11 +71,13 @@ pub struct Parser { impl Parser { pub fn parse_step<'a>(&'a mut self, source: &mut impl BufRead) -> Result, Error> { - match read_u64(&mut *source)? { - CODE_AT_CLAUSE => { + let code = read_u64(&mut *source)?; + match code { + CODE_AT_CLAUSE_IRRED | CODE_AT_CLAUSE_RED => { read_literals(&mut *source, &mut self.lit_buf)?; read_hashes(&mut *source, &mut self.hash_buf)?; Ok(ProofStep::AtClause { + redundant: code == CODE_AT_CLAUSE_RED, clause: &self.lit_buf, propagation_hashes: &self.hash_buf, }) @@ -65,9 +86,20 @@ impl Parser { read_unit_clauses(&mut *source, &mut self.unit_buf)?; Ok(ProofStep::UnitClauses(&self.unit_buf)) } - CODE_DELETE_CLAUSE => { + CODE_DELETE_CLAUSE_REDUNDANT + | CODE_DELETE_CLAUSE_SIMPLIFIED + | CODE_DELETE_CLAUSE_SATISFIED => { + let proof = match code { + CODE_DELETE_CLAUSE_REDUNDANT => DeleteClauseProof::Redundant, + CODE_DELETE_CLAUSE_SIMPLIFIED => DeleteClauseProof::Simplified, + CODE_DELETE_CLAUSE_SATISFIED => DeleteClauseProof::Satisfied, + _ => unreachable!(), + }; read_literals(&mut *source, &mut self.lit_buf)?; - Ok(ProofStep::DeleteClause(&self.lit_buf)) + Ok(ProofStep::DeleteClause { + clause: &self.lit_buf, + proof, + }) } CODE_CHANGE_HASH_BITS => { let bits = read_u64(&mut *source)? as u32; diff --git a/varisat/src/simplify.rs b/varisat/src/simplify.rs index e1c72e6e..58ebc611 100644 --- a/varisat/src/simplify.rs +++ b/varisat/src/simplify.rs @@ -9,7 +9,7 @@ use crate::context::{ SolverStateP, TrailP, WatchlistsP, }; use crate::lit::Lit; -use crate::proof::{self, clause_hash, lit_hash, ProofStep}; +use crate::proof::{self, clause_hash, lit_hash, DeleteClauseProof, ProofStep}; use crate::prop::{enqueue_assignment, Reason}; /// Remove satisfied clauses and false literals. @@ -102,12 +102,23 @@ pub fn simplify<'a>( filter_clauses(ctx_2, |alloc, cref| { let clause = alloc.clause_mut(cref); + let redundant = clause.header().redundant(); new_lits.clear(); for &lit in clause.lits() { match assignment.lit_value(lit) { None => new_lits.push(lit), Some(true) => { - proof::add_step(proof_ctx.borrow(), &ProofStep::DeleteClause(clause.lits())); + proof::add_step( + proof_ctx.borrow(), + &ProofStep::DeleteClause { + clause: clause.lits(), + proof: if redundant { + DeleteClauseProof::Redundant + } else { + DeleteClauseProof::Satisfied + }, + }, + ); return false; } Some(false) => (), @@ -119,11 +130,22 @@ pub fn simplify<'a>( proof::add_step( proof_ctx.borrow(), &ProofStep::AtClause { + redundant: redundant && new_lits.len() > 2, clause: &new_lits, propagation_hashes: &hash[..], }, ); - proof::add_step(proof_ctx.borrow(), &ProofStep::DeleteClause(clause.lits())); + proof::add_step( + proof_ctx.borrow(), + &ProofStep::DeleteClause { + clause: clause.lits(), + proof: if redundant { + DeleteClauseProof::Redundant + } else { + DeleteClauseProof::Simplified + }, + }, + ); } match new_lits[..] { From 3e91c3b01f3934f740cdcf4b08f5f26e6a0c906c Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 14 May 2019 11:01:36 +0200 Subject: [PATCH 2/5] Improve checker error reporting Include more details and make public API less coupled to internals --- varisat-cli/src/check.rs | 7 +- varisat/src/checker.rs | 379 ++++++++++++++++++++++----------------- varisat/src/proof.rs | 11 +- 3 files changed, 233 insertions(+), 164 deletions(-) diff --git a/varisat-cli/src/check.rs b/varisat-cli/src/check.rs index d53ede78..f0a24052 100644 --- a/varisat-cli/src/check.rs +++ b/varisat-cli/src/check.rs @@ -4,7 +4,7 @@ use std::io; use clap::{App, ArgMatches, SubCommand}; use failure::Error; -use varisat::checker::{Checker, WriteLrat}; +use varisat::checker::{Checker, CheckerError, WriteLrat}; use super::{banner, init_logging}; @@ -66,6 +66,11 @@ pub fn check_main(matches: &ArgMatches) -> Result { Ok(()) => println!("s VERIFIED"), Err(err) => { log::error!("{}", err); + if let CheckerError::CheckFailed { debug_step, .. } = err { + if !debug_step.is_empty() { + log::error!("failed step was {}", debug_step) + } + } println!("s NOT VERIFIED"); return Ok(1); } diff --git a/varisat/src/checker.rs b/varisat/src/checker.rs index 21685dc0..4cdb29e2 100644 --- a/varisat/src/checker.rs +++ b/varisat/src/checker.rs @@ -38,14 +38,12 @@ pub enum CheckerError { #[cause] cause: Error, }, - #[fail(display = "step {}: Delete of unknown clause {:?}", step, clause)] - InvalidDelete { step: u64, clause: Vec }, - #[fail(display = "step {}: No clause with hash {:x} found", step, hash)] - ClauseNotFound { step: u64, hash: ClauseHash }, - #[fail(display = "step {}: Checking proof for {:?} failed", step, clause)] - ClauseCheckFailed { step: u64, clause: Vec }, - #[fail(display = "step {}: Checking proof failed", step)] - CheckFailed { step: u64 }, + #[fail(display = "step {}: Checking proof failed: {}", step, msg)] + CheckFailed { + step: u64, + msg: String, + debug_step: String, + }, #[fail(display = "Error in proof processor: {}", cause)] ProofProcessorError { #[cause] @@ -56,6 +54,17 @@ pub enum CheckerError { __Nonexhaustive, } +impl CheckerError { + /// Generate a CheckFailed error with an empty debug_step + fn check_failed(step: u64, msg: String) -> CheckerError { + CheckerError::CheckFailed { + step, + msg, + debug_step: String::new(), + } + } +} + /// A single step of a proof. /// /// Clauses are identified by a unique increasing id assigned by the checker. Whenever the literals @@ -454,10 +463,10 @@ impl<'a> Checker<'a> { redundant: bool, ) -> Result, CheckerError> { if lits.len() < 2 { - return Err(CheckerError::InvalidDelete { - step: self.step, - clause: lits.to_owned(), - }); + return Err(CheckerError::check_failed( + self.step, + format!("delete of unit or empty clause {:?}", lits), + )); } let hash = self.clause_hash(lits); @@ -502,11 +511,12 @@ impl<'a> Checker<'a> { } if !deleted { - // TODO differentiate between not found and red/irred mismatch - return Err(CheckerError::InvalidDelete { - step: self.step, - clause: lits.to_owned(), - }); + let msg = match (found, redundant) { + (false, _) => format!("delete of unknown clause {:?}", lits), + (_, true) => format!("delete of redundant clause {:?} which is irredundant", lits), + (_, false) => format!("delete of irredundant clause {:?} which is redundant", lits), + }; + return Err(CheckerError::check_failed(self.step, msg)); } self.collect_garbage(); @@ -582,10 +592,10 @@ impl<'a> Checker<'a> { let candidates = match self.clauses.get(&hash) { Some(candidates) if !candidates.is_empty() => candidates, _ => { - return Err(CheckerError::ClauseNotFound { - step: self.step, - hash, - }) + return Err(CheckerError::check_failed( + self.step, + format!("no clause found for hash {:x}", hash), + )) } }; @@ -687,10 +697,10 @@ impl<'a> Checker<'a> { if rup_is_unsat { Ok(()) } else { - Err(CheckerError::ClauseCheckFailed { - step: self.step, - clause: lits.to_owned(), - }) + Err(CheckerError::check_failed( + self.step, + format!("AT check failed for {:?}", lits), + )) } } @@ -732,111 +742,149 @@ impl<'a> Checker<'a> { /// Check a single proof step pub(crate) fn check_step(&mut self, step: ProofStep) -> Result<(), CheckerError> { - match step { + let mut result = match step { ProofStep::AtClause { redundant, clause, propagation_hashes, - } => { - let mut tmp = replace(&mut self.tmp, vec![]); - tmp.clear(); - tmp.extend_from_slice(&clause); + } => self.check_at_clause_step(redundant, clause, propagation_hashes), + ProofStep::DeleteClause { clause, proof } => { + self.check_delete_clause_step(clause, proof) + } + ProofStep::UnitClauses(units) => self.check_unit_clauses_step(units), + ProofStep::ChangeHashBits(bits) => { + self.hash_bits = bits; + self.rehash(); + Ok(()) + } + }; - tmp.sort_unstable(); - tmp.dedup(); + if let Err(CheckerError::CheckFailed { + ref mut debug_step, .. + }) = result + { + *debug_step = format!("{:?}", step) + } + result + } - self.check_clause_with_hashes(&tmp, &*propagation_hashes)?; + /// Check an AtClause step + fn check_at_clause_step( + &mut self, + redundant: bool, + clause: &[Lit], + propagation_hashes: &[ClauseHash], + ) -> Result<(), CheckerError> { + let mut tmp = replace(&mut self.tmp, vec![]); + tmp.clear(); + tmp.extend_from_slice(&clause); - let (id, added) = self.store_clause(&tmp, redundant); + tmp.sort_unstable(); + tmp.dedup(); - if !redundant { - self.previous_irred_clause.clear(); - self.previous_irred_clause.extend_from_slice(&tmp); - } + self.check_clause_with_hashes(&tmp, &*propagation_hashes)?; - if added { - Self::process_step( - &mut self.processors, - &CheckedProofStep::AtClause { - id: id, - clause: &tmp, - propagations: &self.trace_ids, - }, - )?; - } + let (id, added) = self.store_clause(&tmp, redundant); - self.tmp = tmp; - } - ProofStep::DeleteClause { clause, proof } => { - let mut tmp = replace(&mut self.tmp, vec![]); - tmp.clear(); - tmp.extend_from_slice(&clause); - - tmp.sort_unstable(); - tmp.dedup(); - - let redundant = proof == DeleteClauseProof::Redundant; - - match proof { - DeleteClauseProof::Redundant => (), - DeleteClauseProof::Satisfied => { - if !tmp.iter().any(|&lit| { - if let Some((true, _)) = self.lit_value(lit) { - true - } else { - false - } - }) { - return Err(CheckerError::CheckFailed { step: self.step }); - } - } - DeleteClauseProof::Simplified => { - if !self.subsumed_by_previous_irred_clause(&tmp) { - return Err(CheckerError::CheckFailed { step: self.step }); - } - } - } + if !redundant { + self.previous_irred_clause.clear(); + self.previous_irred_clause.extend_from_slice(&tmp); + } - self.previous_irred_clause.clear(); + if added { + Self::process_step( + &mut self.processors, + &CheckedProofStep::AtClause { + id: id, + clause: &tmp, + propagations: &self.trace_ids, + }, + )?; + } - if let Some(id) = self.delete_clause(&tmp, redundant)? { - Self::process_step( - &mut self.processors, - &CheckedProofStep::DeleteClause { - id: id, - clause: &tmp, - }, - )?; - } + self.tmp = tmp; - self.tmp = tmp; - } - ProofStep::UnitClauses(units) => { - for &(lit, hash) in units.iter() { - let clause = [lit]; - let propagation_hashes = [hash]; - self.check_clause_with_hashes(&clause[..], &propagation_hashes[..])?; - - let (id, added) = self.store_unit_clause(lit); - - if added { - Self::process_step( - &mut self.processors, - &CheckedProofStep::AtClause { - id: id, - clause: &clause, - propagations: &self.trace_ids, - }, - )?; + Ok(()) + } + + fn check_delete_clause_step( + &mut self, + clause: &[Lit], + proof: DeleteClauseProof, + ) -> Result<(), CheckerError> { + let mut tmp = replace(&mut self.tmp, vec![]); + tmp.clear(); + tmp.extend_from_slice(&clause); + + tmp.sort_unstable(); + tmp.dedup(); + + let redundant = proof == DeleteClauseProof::Redundant; + + match proof { + DeleteClauseProof::Redundant => (), + DeleteClauseProof::Satisfied => { + if !tmp.iter().any(|&lit| { + if let Some((true, _)) = self.lit_value(lit) { + true + } else { + false } + }) { + return Err(CheckerError::check_failed( + self.step, + format!("deleted clause {:?} is not satisfied", clause), + )); } } - ProofStep::ChangeHashBits(bits) => { - self.hash_bits = bits; - self.rehash(); + DeleteClauseProof::Simplified => { + if !self.subsumed_by_previous_irred_clause(&tmp) { + return Err(CheckerError::check_failed( + self.step, + format!( + "deleted clause {:?} is not subsumed by previous clause {:?}", + clause, self.previous_irred_clause + ), + )); + } } } + self.previous_irred_clause.clear(); + + if let Some(id) = self.delete_clause(&tmp, redundant)? { + Self::process_step( + &mut self.processors, + &CheckedProofStep::DeleteClause { + id: id, + clause: &tmp, + }, + )?; + } + + self.tmp = tmp; + Ok(()) + } + + fn check_unit_clauses_step(&mut self, units: &[(Lit, ClauseHash)]) -> Result<(), CheckerError> { + for &(lit, hash) in units.iter() { + let clause = [lit]; + let propagation_hashes = [hash]; + self.check_clause_with_hashes(&clause[..], &propagation_hashes[..])?; + + let (id, added) = self.store_unit_clause(lit); + + if added { + Self::process_step( + &mut self.processors, + &CheckedProofStep::AtClause { + id: id, + clause: &clause, + propagations: &self.trace_ids, + }, + )?; + } + } Ok(()) } @@ -930,6 +978,13 @@ mod tests { use crate::solver::{ProofFormat, Solver}; + fn expect_check_failed(result: Result<(), CheckerError>, contains: &str) { + match result { + Err(CheckerError::CheckFailed { ref msg, .. }) if msg.contains(contains) => (), + err => panic!("expected {:?} error but got {:?}", contains, err), + } + } + #[test] fn conflicting_units() { let mut checker = Checker::new(); @@ -955,13 +1010,13 @@ mod tests { ]) .unwrap(); - match checker.check_step(ProofStep::DeleteClause { - clause: &lits![-5, 4], - proof: DeleteClauseProof::Redundant, - }) { - Err(CheckerError::InvalidDelete { .. }) => (), - _ => panic!("expected InvalidDelete error"), - } + expect_check_failed( + checker.check_step(ProofStep::DeleteClause { + clause: &lits![-5, 4], + proof: DeleteClauseProof::Redundant, + }), + "unknown clause", + ); } #[test] @@ -1001,13 +1056,13 @@ mod tests { }) .unwrap(); - match checker.check_step(ProofStep::DeleteClause { - clause: lits, - proof: DeleteClauseProof::Satisfied, - }) { - Err(CheckerError::InvalidDelete { .. }) => (), - _ => panic!("expected InvalidDelete error"), - } + expect_check_failed( + checker.check_step(ProofStep::DeleteClause { + clause: lits, + proof: DeleteClauseProof::Satisfied, + }), + "unknown clause", + ); } #[test] @@ -1019,14 +1074,14 @@ mod tests { ]) .unwrap(); - match checker.check_step(ProofStep::AtClause { - redundant: false, - clause: [][..].into(), - propagation_hashes: [0][..].into(), - }) { - Err(CheckerError::ClauseNotFound { .. }) => (), - _ => panic!("expected ClauseNotFound error"), - } + expect_check_failed( + checker.check_step(ProofStep::AtClause { + redundant: false, + clause: [][..].into(), + propagation_hashes: [0][..].into(), + }), + "no clause found", + ) } #[test] @@ -1038,14 +1093,14 @@ mod tests { ]) .unwrap(); - match checker.check_step(ProofStep::AtClause { - redundant: false, - clause: [][..].into(), - propagation_hashes: [][..].into(), - }) { - Err(CheckerError::ClauseCheckFailed { .. }) => (), - _ => panic!("expected ClauseCheckFailed error"), - } + expect_check_failed( + checker.check_step(ProofStep::AtClause { + redundant: false, + clause: [][..].into(), + propagation_hashes: [][..].into(), + }), + "AT check failed", + ) } #[test] @@ -1057,13 +1112,13 @@ mod tests { ]) .unwrap(); - match checker.check_step(ProofStep::DeleteClause { - clause: &lits![1, 2, 3], - proof: DeleteClauseProof::Redundant, - }) { - Err(CheckerError::CheckFailed { .. }) => (), - _ => panic!("expected CheckFailed error"), - } + expect_check_failed( + checker.check_step(ProofStep::DeleteClause { + clause: &lits![1, 2, 3], + proof: DeleteClauseProof::Redundant, + }), + "is irredundant", + ) } #[test] @@ -1077,13 +1132,13 @@ mod tests { ]) .unwrap(); - match checker.check_step(ProofStep::DeleteClause { - clause: &lits![1, 2, 3], - proof: DeleteClauseProof::Satisfied, - }) { - Err(CheckerError::CheckFailed { .. }) => (), - _ => panic!("expected CheckFailed error"), - } + expect_check_failed( + checker.check_step(ProofStep::DeleteClause { + clause: &lits![1, 2, 3], + proof: DeleteClauseProof::Satisfied, + }), + "not satisfied", + ) } #[test] @@ -1109,13 +1164,13 @@ mod tests { }) .unwrap(); - match checker.check_step(ProofStep::DeleteClause { - clause: &lits![1, 2, 3], - proof: DeleteClauseProof::Simplified, - }) { - Err(CheckerError::CheckFailed { .. }) => (), - _ => panic!("expected CheckFailed error"), - } + expect_check_failed( + checker.check_step(ProofStep::DeleteClause { + clause: &lits![1, 2, 3], + proof: DeleteClauseProof::Simplified, + }), + "not subsumed", + ) } proptest! { diff --git a/varisat/src/proof.rs b/varisat/src/proof.rs index 25da715d..a709ced9 100644 --- a/varisat/src/proof.rs +++ b/varisat/src/proof.rs @@ -335,7 +335,16 @@ fn handle_self_check_result<'a>( Some(SolverError::ProofProcessorError { cause }); *ctx.part_mut(ProofP) = Proof::default(); } - result => result.expect("self check failure"), + Err(err) => { + log::error!("{}", err); + if let CheckerError::CheckFailed { debug_step, .. } = err { + if !debug_step.is_empty() { + log::error!("failed step was {}", debug_step) + } + } + panic!("self check failure"); + } + Ok(()) => (), } } From 60a2256f2cba2a6f355c5703e46febc201ebda8b Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 14 May 2019 15:06:24 +0200 Subject: [PATCH 3/5] Add clause deletion proofs to CheckedProofStep Part of #30 --- varisat/src/checker.rs | 283 ++++++++++++++++++++---------- varisat/src/checker/write_lrat.rs | 16 +- 2 files changed, 203 insertions(+), 96 deletions(-) diff --git a/varisat/src/checker.rs b/varisat/src/checker.rs index 4cdb29e2..c2130d12 100644 --- a/varisat/src/checker.rs +++ b/varisat/src/checker.rs @@ -92,17 +92,22 @@ pub enum CheckedProofStep<'a> { /// clauses in the order they became unit and as last element the clause that caused a conflict. AtClause { id: u64, + redundant: bool, clause: &'a [Lit], propagations: &'a [u64], }, /// Deletion of a redundant clause. - /// - /// Currently the redundancy of the deleted clause is not checked. Such a check is not required - /// to validate unsatisfiability proofs. This might change in the future to cover more use - /// cases. DeleteClause { id: u64, clause: &'a [Lit] }, - #[doc(hidden)] - __Nonexhaustive, + /// Deletion of a clause that is an asymmetric tautology w.r.t the remaining irredundant + /// clauses. + DeleteAtClause { + id: u64, + keep_as_redundant: bool, + clause: &'a [Lit], + propagations: &'a [u64], + }, + /// Make a redundant clause irredundant. + MakeIrredundant { id: u64, clause: &'a [Lit] }, } /// Implement to process proof steps. @@ -205,6 +210,22 @@ struct TraceItem { unused: bool, } +/// Return type of [`Checker::store_clause`] +#[derive(Copy, Clone, PartialEq, Eq)] +enum StoreClauseResult { + New, + Duplicate, + NewlyIrredundant, +} + +/// Return type of [`Checker::delete_clause`] +#[derive(Copy, Clone, PartialEq, Eq)] +enum DeleteClauseResult { + Unchanged, + NewlyRedundant, + Removed, +} + /// A checker for unsatisfiability proofs in the native varisat format. pub struct Checker<'a> { /// Current step number. @@ -240,13 +261,12 @@ pub struct Checker<'a> { tmp: Vec, /// How many bits are used for storing clause hashes. hash_bits: u32, - /// Last added irredundant clause. - /// - /// Empty if no such clause was added since the last clause deletion. So if this is non-empty - /// the clause is present and irredundant. + /// Last added irredundant clause id. /// /// Sorted and free of duplicates. - previous_irred_clause: Vec, + previous_irred_clause_id: Option, + /// Last added irredundant clause literals. + previous_irred_clause_lits: Vec, } impl<'a> Default for Checker<'a> { @@ -267,7 +287,8 @@ impl<'a> Default for Checker<'a> { unit_conflict: None, tmp: vec![], hash_bits: 64, - previous_irred_clause: vec![], + previous_irred_clause_id: None, + previous_irred_clause_lits: vec![], } } } @@ -304,26 +325,39 @@ impl<'a> Checker<'a> { self.tmp = tmp; - if added { - Self::process_step( - &mut self.processors, - &CheckedProofStep::AddClause { - id: id, - clause: &self.tmp, - }, - )?; - } else { - Self::process_step( - &mut self.processors, - &CheckedProofStep::DuplicatedClause { - id: self.next_clause_id, - same_as_id: id, - clause: &self.tmp, - }, - )?; - // This is a duplicated clause. We want to ensure that the clause ids match the input - // order so we skip a clause id. - self.next_clause_id += 1; + match added { + StoreClauseResult::New => { + Self::process_step( + &mut self.processors, + &CheckedProofStep::AddClause { + id: id, + clause: &self.tmp, + }, + )?; + } + StoreClauseResult::NewlyIrredundant | StoreClauseResult::Duplicate => { + if let StoreClauseResult::NewlyIrredundant = added { + Self::process_step( + &mut self.processors, + &CheckedProofStep::MakeIrredundant { + id, + clause: &self.tmp, + }, + )?; + } + + Self::process_step( + &mut self.processors, + &CheckedProofStep::DuplicatedClause { + id: self.next_clause_id, + same_as_id: id, + clause: &self.tmp, + }, + )?; + // This is a duplicated clause. We want to ensure that the clause ids match the input + // order so we skip a clause id. + self.next_clause_id += 1; + } } Ok(()) @@ -364,16 +398,16 @@ impl<'a> Checker<'a> { /// /// `lits` must be sorted and free of duplicates. /// - /// 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: &[Lit], redundant: bool) -> (u64, bool) { + /// Returns the id of the added clause and indicates whether the clause is new or changed from + /// redundant to irredundant. + fn store_clause(&mut self, lits: &[Lit], redundant: bool) -> (u64, StoreClauseResult) { match lits[..] { [] => { let id = self.next_clause_id; self.next_clause_id += 1; self.unsat = true; - (id, true) + (id, StoreClauseResult::New) } [lit] => self.store_unit_clause(lit), _ => { @@ -383,9 +417,16 @@ impl<'a> Checker<'a> { for candidate in candidates.iter_mut() { if candidate.lits.slice(&self.literal_buffer) == &lits[..] { + let result = if !redundant && candidate.ref_count[0] == 0 { + // first irredundant copy + StoreClauseResult::NewlyIrredundant + } else { + StoreClauseResult::Duplicate + }; + let ref_count = &mut candidate.ref_count[redundant as usize]; *ref_count = ref_count.checked_add(1).expect("ref_count overflow"); - return (candidate.id, false); + return (candidate.id, result); } } @@ -401,7 +442,7 @@ impl<'a> Checker<'a> { }); self.next_clause_id += 1; - (id, true) + (id, StoreClauseResult::New) } } } @@ -410,7 +451,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_unit_clause(&mut self, lit: Lit) -> (u64, bool) { + fn store_unit_clause(&mut self, lit: Lit) -> (u64, StoreClauseResult) { match self.lit_value(lit) { Some(( true, @@ -418,7 +459,7 @@ impl<'a> Checker<'a> { id: UnitId::Global(id), .. }, - )) => (id, false), + )) => (id, StoreClauseResult::Duplicate), Some(( false, UnitClause { @@ -430,7 +471,7 @@ impl<'a> Checker<'a> { let id = self.next_clause_id; self.unit_conflict = Some([conflicting_id, id]); self.next_clause_id += 1; - (id, true) + (id, StoreClauseResult::New) } Some(_) => unreachable!(), None => { @@ -447,7 +488,7 @@ impl<'a> Checker<'a> { self.next_clause_id += 1; - (id, true) + (id, StoreClauseResult::New) } } } @@ -456,12 +497,13 @@ impl<'a> Checker<'a> { /// /// `lits` must be sorted and free of duplicates. /// - /// Returns the id of the clause if the clause's ref_count became zero. + /// Returns the id of the deleted clause and whether the ref_count (or irredundant ref_count) + /// became zero. fn delete_clause( &mut self, lits: &[Lit], redundant: bool, - ) -> Result, CheckerError> { + ) -> Result<(u64, DeleteClauseResult), CheckerError> { if lits.len() < 2 { return Err(CheckerError::check_failed( self.step, @@ -473,7 +515,6 @@ impl<'a> Checker<'a> { let candidates = self.clauses.entry(hash).or_default(); - let mut deleted = false; let mut found = false; let mut result = None; @@ -491,15 +532,18 @@ impl<'a> Checker<'a> { if *ref_count == 0 { true } else { - deleted = true; - *ref_count -= 1; if candidate.ref_count == [0, 0] { *garbage_size += candidate.lits.buffer_used(); - result = Some(candidate.id); + result = Some((candidate.id, DeleteClauseResult::Removed)); false } else { + if !redundant && candidate.ref_count[0] == 0 { + result = Some((candidate.id, DeleteClauseResult::NewlyRedundant)); + } else { + result = Some((candidate.id, DeleteClauseResult::Unchanged)); + } true } } @@ -510,18 +554,17 @@ impl<'a> Checker<'a> { self.clauses.remove(&hash); } - if !deleted { - let msg = match (found, redundant) { - (false, _) => format!("delete of unknown clause {:?}", lits), - (_, true) => format!("delete of redundant clause {:?} which is irredundant", lits), - (_, false) => format!("delete of irredundant clause {:?} which is redundant", lits), - }; - return Err(CheckerError::check_failed(self.step, msg)); + if let Some(result) = result { + self.collect_garbage(); + return Ok(result); } - self.collect_garbage(); - - Ok(result) + let msg = match (found, redundant) { + (false, _) => format!("delete of unknown clause {:?}", lits), + (_, true) => format!("delete of redundant clause {:?} which is irredundant", lits), + (_, false) => format!("delete of irredundant clause {:?} which is redundant", lits), + }; + return Err(CheckerError::check_failed(self.step, msg)); } /// Perform a garbage collection if required @@ -708,11 +751,10 @@ impl<'a> Checker<'a> { /// /// `lits` must be sorted and free of duplicates. fn subsumed_by_previous_irred_clause(&self, lits: &[Lit]) -> bool { - if self.previous_irred_clause.is_empty() { - // Here empty doesn't mean empty clause but no clause + if self.previous_irred_clause_id.is_none() { return false; } - let mut subset = &self.previous_irred_clause[..]; + let mut subset = &self.previous_irred_clause_lits[..]; let mut superset = lits; let mut strict = false; @@ -787,19 +829,30 @@ impl<'a> Checker<'a> { let (id, added) = self.store_clause(&tmp, redundant); if !redundant { - self.previous_irred_clause.clear(); - self.previous_irred_clause.extend_from_slice(&tmp); + self.previous_irred_clause_id = Some(id); + self.previous_irred_clause_lits.clear(); + self.previous_irred_clause_lits.extend_from_slice(&tmp); } - if added { - Self::process_step( - &mut self.processors, - &CheckedProofStep::AtClause { - id: id, - clause: &tmp, - propagations: &self.trace_ids, - }, - )?; + match added { + StoreClauseResult::New => { + Self::process_step( + &mut self.processors, + &CheckedProofStep::AtClause { + id, + redundant: redundant, + clause: &tmp, + propagations: &self.trace_ids, + }, + )?; + } + StoreClauseResult::NewlyIrredundant => { + Self::process_step( + &mut self.processors, + &CheckedProofStep::MakeIrredundant { id, clause: &tmp }, + )?; + } + StoreClauseResult::Duplicate => (), } self.tmp = tmp; @@ -807,6 +860,7 @@ impl<'a> Checker<'a> { Ok(()) } + /// Check a DeleteClause step fn check_delete_clause_step( &mut self, clause: &[Lit], @@ -821,11 +875,21 @@ impl<'a> Checker<'a> { let redundant = proof == DeleteClauseProof::Redundant; + let mut subsumed_by = None; + match proof { DeleteClauseProof::Redundant => (), DeleteClauseProof::Satisfied => { if !tmp.iter().any(|&lit| { - if let Some((true, _)) = self.lit_value(lit) { + if let Some(( + true, + UnitClause { + id: UnitId::Global(id), + .. + }, + )) = self.lit_value(lit) + { + subsumed_by = Some(id); true } else { false @@ -838,34 +902,60 @@ impl<'a> Checker<'a> { } } DeleteClauseProof::Simplified => { + subsumed_by = self.previous_irred_clause_id; if !self.subsumed_by_previous_irred_clause(&tmp) { return Err(CheckerError::check_failed( self.step, format!( "deleted clause {:?} is not subsumed by previous clause {:?}", - clause, self.previous_irred_clause + clause, self.previous_irred_clause_lits ), )); } } } - self.previous_irred_clause.clear(); + self.previous_irred_clause_id = None; + self.previous_irred_clause_lits.clear(); - if let Some(id) = self.delete_clause(&tmp, redundant)? { - Self::process_step( - &mut self.processors, - &CheckedProofStep::DeleteClause { - id: id, - clause: &tmp, - }, - )?; + let (id, deleted) = self.delete_clause(&tmp, redundant)?; + + if redundant { + match deleted { + DeleteClauseResult::Removed => { + Self::process_step( + &mut self.processors, + &CheckedProofStep::DeleteClause { + id: id, + clause: &tmp, + }, + )?; + } + DeleteClauseResult::Unchanged => (), + DeleteClauseResult::NewlyRedundant => unreachable!(), + } + } else { + match deleted { + DeleteClauseResult::Removed | DeleteClauseResult::NewlyRedundant => { + Self::process_step( + &mut self.processors, + &CheckedProofStep::DeleteAtClause { + id: id, + keep_as_redundant: deleted == DeleteClauseResult::NewlyRedundant, + clause: &tmp, + propagations: &[subsumed_by.unwrap()], + }, + )?; + } + DeleteClauseResult::Unchanged => (), + } } self.tmp = tmp; Ok(()) } + /// Check a UnitClauses step fn check_unit_clauses_step(&mut self, units: &[(Lit, ClauseHash)]) -> Result<(), CheckerError> { for &(lit, hash) in units.iter() { let clause = [lit]; @@ -874,20 +964,26 @@ impl<'a> Checker<'a> { let (id, added) = self.store_unit_clause(lit); - if added { - Self::process_step( - &mut self.processors, - &CheckedProofStep::AtClause { - id: id, - clause: &clause, - propagations: &self.trace_ids, - }, - )?; + match added { + StoreClauseResult::New => { + Self::process_step( + &mut self.processors, + &CheckedProofStep::AtClause { + id, + redundant: false, + clause: &clause, + propagations: &self.trace_ids, + }, + )?; + } + StoreClauseResult::Duplicate => (), + StoreClauseResult::NewlyIrredundant => unreachable!(), } } Ok(()) } + /// Invoke all proof processors for a CheckedProofStep fn process_step<'b>( processors: &'b mut [&'a mut dyn ProofProcessor], step: &CheckedProofStep<'b>, @@ -949,7 +1045,8 @@ impl<'a> Checker<'a> { &mut self.processors, &CheckedProofStep::AtClause { id: self.next_clause_id, - clause: clause, + redundant: false, + clause, propagations: ids, }, )?; diff --git a/varisat/src/checker/write_lrat.rs b/varisat/src/checker/write_lrat.rs index c554b5f6..4c869250 100644 --- a/varisat/src/checker/write_lrat.rs +++ b/varisat/src/checker/write_lrat.rs @@ -2,7 +2,7 @@ use std::io::{BufWriter, Write}; use std::mem::replace; -use failure::{bail, Error}; +use failure::Error; use crate::lit::Lit; @@ -50,6 +50,7 @@ impl<'a> ProofProcessor for WriteLrat<'a> { id, clause, propagations, + .. } => { self.close_delete()?; self.last_added_id = id; @@ -60,12 +61,21 @@ impl<'a> ProofProcessor for WriteLrat<'a> { self.write_ids(propagations)?; self.write_end()?; } + &CheckedProofStep::DeleteAtClause { + id, + keep_as_redundant, + .. + } => { + if !keep_as_redundant { + self.open_delete()?; + self.write_ids(&[id])?; + } + } &CheckedProofStep::DeleteClause { id, .. } => { self.open_delete()?; - self.write_ids(&[id])?; } - _ => bail!("LRAT doesn't support proof step {:?}", step), + &CheckedProofStep::MakeIrredundant { .. } => (), } Ok(()) } From e5d0876f7fa068d718066cf84123468e01323c5f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 15 May 2019 09:13:30 +0200 Subject: [PATCH 4/5] Emit and check found models in varisat proofs --- varisat/src/cdcl.rs | 16 ++++++ varisat/src/checker.rs | 87 ++++++++++++++++++++++++++++++- varisat/src/checker/write_lrat.rs | 2 +- varisat/src/proof.rs | 30 ++++++----- varisat/src/proof/drat.rs | 4 +- varisat/src/proof/map_step.rs | 6 +++ varisat/src/proof/varisat.rs | 10 ++++ 7 files changed, 138 insertions(+), 17 deletions(-) diff --git a/varisat/src/cdcl.rs b/varisat/src/cdcl.rs index 1be1c8bb..cbce5957 100644 --- a/varisat/src/cdcl.rs +++ b/varisat/src/cdcl.rs @@ -10,6 +10,7 @@ use crate::context::{ }; use crate::decision::make_decision; use crate::incremental::{enqueue_assumption, EnqueueAssumption}; +use crate::lit::Lit; use crate::proof::{self, ProofStep}; use crate::prop::{backtrack, enqueue_assignment, propagate, Conflict, Reason}; use crate::simplify::{prove_units, simplify}; @@ -39,6 +40,21 @@ pub fn conflict_step<'a>( let conflict = match conflict { Ok(()) => { + if ctx.part(ProofP).models_in_proof() { + let (tmp, mut ctx) = ctx.split_part_mut(TmpDataP); + let model = &mut tmp.lits; + model.clear(); + model.extend( + ctx.part(AssignmentP) + .assignment() + .iter() + .enumerate() + .flat_map(|(index, assignment)| { + assignment.map(|polarity| Lit::from_index(index, !polarity)) + }), + ); + proof::add_step(ctx.borrow(), &ProofStep::Model(&model)); + } ctx.part_mut(SolverStateP).sat_state = SatState::Sat; return; } diff --git a/varisat/src/checker.rs b/varisat/src/checker.rs index c2130d12..5525aeb9 100644 --- a/varisat/src/checker.rs +++ b/varisat/src/checker.rs @@ -6,7 +6,7 @@ use std::mem::{replace, transmute}; use std::ops::Range; use failure::{Error, Fail}; -use hashbrown::HashMap; +use hashbrown::{HashMap, HashSet}; use smallvec::SmallVec; use crate::cnf::CnfFormula; @@ -108,6 +108,8 @@ pub enum CheckedProofStep<'a> { }, /// Make a redundant clause irredundant. MakeIrredundant { id: u64, clause: &'a [Lit] }, + /// A (partial) assignment that satisfies all clauses. + Model { assignment: &'a [Lit] }, } /// Implement to process proof steps. @@ -799,6 +801,7 @@ impl<'a> Checker<'a> { self.rehash(); Ok(()) } + ProofStep::Model(model) => self.check_model_step(model), }; if let Err(CheckerError::CheckFailed { @@ -983,6 +986,40 @@ impl<'a> Checker<'a> { Ok(()) } + /// Check a Model step + fn check_model_step(&mut self, model: &[Lit]) -> Result<(), CheckerError> { + let mut assignments = HashSet::new(); + + for &lit in model.iter() { + if let Some((false, _)) = self.lit_value(lit) { + return Err(CheckerError::check_failed( + self.step, + format!("model assignment conflicts with unit clause {:?}", !lit), + )); + } + if assignments.contains(&!lit) { + return Err(CheckerError::check_failed( + self.step, + format!("model contains conflicting assignment {:?}", !lit), + )); + } + assignments.insert(lit); + } + + for (_, candidates) in self.clauses.iter() { + for clause in candidates.iter() { + let lits = clause.lits.slice(&self.literal_buffer); + if !lits.iter().any(|lit| assignments.contains(&lit)) { + return Err(CheckerError::check_failed( + self.step, + format!("model does not satisfy clause {:?}", lits), + )); + } + } + } + Ok(()) + } + /// Invoke all proof processors for a CheckedProofStep fn process_step<'b>( processors: &'b mut [&'a mut dyn ProofProcessor], @@ -1270,6 +1307,54 @@ mod tests { ) } + #[test] + fn model_unit_conflict() { + let mut checker = Checker::new(); + checker + .add_formula(&cnf_formula![ + 1; + 2, 3; + ]) + .unwrap(); + + expect_check_failed( + checker.check_step(ProofStep::Model(&lits![-1, 2, -3])), + "conflicts with unit clause", + ) + } + + #[test] + fn model_internal_conflict() { + let mut checker = Checker::new(); + checker + .add_formula(&cnf_formula![ + 2, 3; + ]) + .unwrap(); + + expect_check_failed( + checker.check_step(ProofStep::Model(&lits![-1, 1, 2, -3])), + "conflicting assignment", + ) + } + + #[test] + fn model_clause_unsat() { + let mut checker = Checker::new(); + checker + .add_formula(&cnf_formula![ + 1, 2, 3; + -1, -2, 3; + 1, -2, -3; + ]) + .unwrap(); + + expect_check_failed( + checker.check_step(ProofStep::Model(&lits![-1, 2, 3])), + "does not satisfy clause", + ) + } + proptest! { #[test] fn checked_unsat_via_dimacs(formula in sgen_unsat_formula(1..7usize)) { diff --git a/varisat/src/checker/write_lrat.rs b/varisat/src/checker/write_lrat.rs index 4c869250..bd827c59 100644 --- a/varisat/src/checker/write_lrat.rs +++ b/varisat/src/checker/write_lrat.rs @@ -75,7 +75,7 @@ impl<'a> ProofProcessor for WriteLrat<'a> { self.open_delete()?; self.write_ids(&[id])?; } - &CheckedProofStep::MakeIrredundant { .. } => (), + &CheckedProofStep::MakeIrredundant { .. } | &CheckedProofStep::Model { .. } => (), } Ok(()) } diff --git a/varisat/src/proof.rs b/varisat/src/proof.rs index a709ced9..ba78e426 100644 --- a/varisat/src/proof.rs +++ b/varisat/src/proof.rs @@ -92,6 +92,8 @@ pub enum ProofStep<'a> { }, /// Change the number of clause hash bits used ChangeHashBits(u32), + /// A (partial) assignment that satisfies all clauses. + Model(&'a [Lit]), } impl<'a> ProofStep<'a> { @@ -112,9 +114,7 @@ impl<'a> ProofStep<'a> { 0 } } - - ProofStep::UnitClauses(..) => 0, - ProofStep::ChangeHashBits(..) => 0, + ProofStep::UnitClauses(..) | ProofStep::ChangeHashBits(..) | ProofStep::Model(..) => 0, } } } @@ -176,24 +176,28 @@ impl<'a> Proof<'a> { self.checker.is_some() || self.format.is_some() } - /// Whether clause hashes are required for steps that support them. - pub fn clause_hashes_required(&self) -> bool { + /// Are we emitting or checking our native format. + pub fn native_format(&self) -> bool { self.checker.is_some() || match self.format { Some(ProofFormat::Varisat) => true, - Some(ProofFormat::Drat) | Some(ProofFormat::BinaryDrat) => false, - None => false, + _ => false, } } + /// Whether clause hashes are required for steps that support them. + pub fn clause_hashes_required(&self) -> bool { + self.native_format() + } + /// Whether unit clauses discovered through unit propagation have to be proven. pub fn prove_propagated_unit_clauses(&self) -> bool { - self.checker.is_some() - || match self.format { - Some(ProofFormat::Varisat) => true, - Some(ProofFormat::Drat) | Some(ProofFormat::BinaryDrat) => false, - None => false, - } + self.native_format() + } + + /// Whether found models are included in the proof. + pub fn models_in_proof(&self) -> bool { + self.native_format() } } diff --git a/varisat/src/proof/drat.rs b/varisat/src/proof/drat.rs index 29cd9edc..48db9a7c 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::ChangeHashBits(..) => (), + ProofStep::UnitClauses(..) | ProofStep::ChangeHashBits(..) | ProofStep::Model(..) => (), } 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::ChangeHashBits(..) => (), + ProofStep::UnitClauses(..) | ProofStep::ChangeHashBits(..) | ProofStep::Model(..) => (), } Ok(()) diff --git a/varisat/src/proof/map_step.rs b/varisat/src/proof/map_step.rs index 10aed4f1..8a28898d 100644 --- a/varisat/src/proof/map_step.rs +++ b/varisat/src/proof/map_step.rs @@ -60,6 +60,12 @@ impl MapStep { } } ProofStep::ChangeHashBits(..) => step.clone(), + + ProofStep::Model(model) => { + self.lit_buf.clear(); + self.lit_buf.extend(model.iter().cloned().map(map_lit)); + ProofStep::Model(&self.lit_buf) + } } } } diff --git a/varisat/src/proof/varisat.rs b/varisat/src/proof/varisat.rs index d5e99323..226fe47d 100644 --- a/varisat/src/proof/varisat.rs +++ b/varisat/src/proof/varisat.rs @@ -14,6 +14,7 @@ const CODE_DELETE_CLAUSE_REDUNDANT: u64 = 3; const CODE_DELETE_CLAUSE_SIMPLIFIED: u64 = 4; const CODE_DELETE_CLAUSE_SATISFIED: u64 = 5; const CODE_CHANGE_HASH_BITS: u64 = 6; +const CODE_MODEL: u64 = 7; /// Writes a proof step in the varisat format pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::Result<()> { @@ -57,6 +58,11 @@ pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::R write_u64(&mut *target, CODE_CHANGE_HASH_BITS)?; write_u64(&mut *target, bits as u64)?; } + + ProofStep::Model(model) => { + write_u64(&mut *target, CODE_MODEL)?; + write_literals(&mut *target, model)?; + } } Ok(()) @@ -105,6 +111,10 @@ impl Parser { let bits = read_u64(&mut *source)? as u32; Ok(ProofStep::ChangeHashBits(bits)) } + CODE_MODEL => { + read_literals(&mut *source, &mut self.lit_buf)?; + Ok(ProofStep::Model(&self.lit_buf)) + } _ => failure::bail!("parse error"), } } From 4fa91ce02d6732cb4b007a87e6ab58116bc0e279 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 15 May 2019 09:39:01 +0200 Subject: [PATCH 5/5] Use an explicit end of proof marker instead of UNSAT --- varisat/src/checker.rs | 14 +++++++++----- varisat/src/proof.rs | 11 ++++++++++- varisat/src/proof/drat.rs | 10 ++++++++-- varisat/src/proof/map_step.rs | 3 ++- varisat/src/proof/varisat.rs | 9 +++++++++ varisat/src/solver.rs | 6 ++++++ 6 files changed, 44 insertions(+), 9 deletions(-) diff --git a/varisat/src/checker.rs b/varisat/src/checker.rs index 5525aeb9..7c3d8ba1 100644 --- a/varisat/src/checker.rs +++ b/varisat/src/checker.rs @@ -21,10 +21,7 @@ pub use write_lrat::WriteLrat; /// Possible errors while checking a varisat proof. #[derive(Debug, Fail)] pub enum CheckerError { - #[fail( - display = "step {}: Proof ended without deriving unsatisfiability", - step - )] + #[fail(display = "step {}: Unexpected end of proof file", step)] ProofIncomplete { step: u64 }, #[fail(display = "step {}: Error reading proof file: {}", step, cause)] IoError { @@ -246,6 +243,8 @@ pub struct Checker<'a> { trail: Vec<(Lit, Option)>, /// Whether unsatisfiability was proven. unsat: bool, + /// Whether an end of proof step was checked. + ended: bool, /// Involved clauses during the last check. trace: Vec, /// Edges of the trace implication graph. @@ -282,6 +281,7 @@ impl<'a> Default for Checker<'a> { unit_clauses: vec![], trail: vec![], unsat: false, + ended: false, trace: vec![], trace_edges: vec![], trace_ids: vec![], @@ -802,6 +802,10 @@ impl<'a> Checker<'a> { Ok(()) } ProofStep::Model(model) => self.check_model_step(model), + ProofStep::End => { + self.ended = true; + Ok(()) + } }; if let Err(CheckerError::CheckFailed { @@ -1041,7 +1045,7 @@ impl<'a> Checker<'a> { let mut buffer = io::BufReader::new(input); let mut parser = Parser::default(); - while !self.unsat { + while !self.ended { self.step += 1; if self.step % 100000 == 0 { diff --git a/varisat/src/proof.rs b/varisat/src/proof.rs index ba78e426..7e2c4634 100644 --- a/varisat/src/proof.rs +++ b/varisat/src/proof.rs @@ -94,6 +94,11 @@ pub enum ProofStep<'a> { ChangeHashBits(u32), /// A (partial) assignment that satisfies all clauses. Model(&'a [Lit]), + /// Signals the end of a proof. + /// + /// A varisat proof must end with this command or else the checker will complain about an + /// incomplete proof. + End, } impl<'a> ProofStep<'a> { @@ -114,7 +119,10 @@ impl<'a> ProofStep<'a> { 0 } } - ProofStep::UnitClauses(..) | ProofStep::ChangeHashBits(..) | ProofStep::Model(..) => 0, + ProofStep::UnitClauses(..) + | ProofStep::ChangeHashBits(..) + | ProofStep::Model(..) + | ProofStep::End => 0, } } } @@ -310,6 +318,7 @@ pub fn flush_proof<'a>(mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut Solver /// Stop writing proof steps. pub fn close_proof<'a>(mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP)) { + add_step(ctx.borrow(), &ProofStep::End); flush_proof(ctx.borrow()); ctx.part_mut(ProofP).format = None; ctx.part_mut(ProofP).target = BufWriter::new(Box::new(sink())); diff --git a/varisat/src/proof/drat.rs b/varisat/src/proof/drat.rs index 48db9a7c..de41ceec 100644 --- a/varisat/src/proof/drat.rs +++ b/varisat/src/proof/drat.rs @@ -14,7 +14,10 @@ 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::ChangeHashBits(..) | ProofStep::Model(..) => (), + ProofStep::UnitClauses(..) + | ProofStep::ChangeHashBits(..) + | ProofStep::Model(..) + | ProofStep::End => (), } Ok(()) @@ -31,7 +34,10 @@ 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::ChangeHashBits(..) | ProofStep::Model(..) => (), + ProofStep::UnitClauses(..) + | ProofStep::ChangeHashBits(..) + | ProofStep::Model(..) + | ProofStep::End => (), } Ok(()) diff --git a/varisat/src/proof/map_step.rs b/varisat/src/proof/map_step.rs index 8a28898d..ccb80234 100644 --- a/varisat/src/proof/map_step.rs +++ b/varisat/src/proof/map_step.rs @@ -59,13 +59,14 @@ impl MapStep { proof, } } - ProofStep::ChangeHashBits(..) => step.clone(), ProofStep::Model(model) => { self.lit_buf.clear(); self.lit_buf.extend(model.iter().cloned().map(map_lit)); ProofStep::Model(&self.lit_buf) } + + ProofStep::ChangeHashBits(..) | ProofStep::End => step.clone(), } } } diff --git a/varisat/src/proof/varisat.rs b/varisat/src/proof/varisat.rs index 226fe47d..5a31c33b 100644 --- a/varisat/src/proof/varisat.rs +++ b/varisat/src/proof/varisat.rs @@ -16,6 +16,10 @@ const CODE_DELETE_CLAUSE_SATISFIED: u64 = 5; const CODE_CHANGE_HASH_BITS: u64 = 6; const CODE_MODEL: u64 = 7; +// Using a random value here makes it unlikely that a corrupted proof will be silently truncated and +// accepted +const CODE_END: u64 = 0x9ac3391f4294c211; + /// 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 { @@ -63,6 +67,10 @@ pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::R write_u64(&mut *target, CODE_MODEL)?; write_literals(&mut *target, model)?; } + + ProofStep::End => { + write_u64(&mut *target, CODE_END)?; + } } Ok(()) @@ -115,6 +123,7 @@ impl Parser { read_literals(&mut *source, &mut self.lit_buf)?; Ok(ProofStep::Model(&self.lit_buf)) } + CODE_END => Ok(ProofStep::End), _ => failure::bail!("parse error"), } } diff --git a/varisat/src/solver.rs b/varisat/src/solver.rs index d17fb8d6..cf3134a0 100644 --- a/varisat/src/solver.rs +++ b/varisat/src/solver.rs @@ -233,6 +233,12 @@ impl<'a> Solver<'a> { } } +impl<'a> Drop for Solver<'a> { + fn drop(&mut self) { + let _ = self.close_proof(); + } +} + #[cfg(test)] mod tests { use super::*;