diff options
Diffstat (limited to 'vendor/varisat/src/unit_simplify.rs')
| -rw-r--r-- | vendor/varisat/src/unit_simplify.rs | 198 |
1 files changed, 198 insertions, 0 deletions
diff --git a/vendor/varisat/src/unit_simplify.rs b/vendor/varisat/src/unit_simplify.rs new file mode 100644 index 000000000..d70130b58 --- /dev/null +++ b/vendor/varisat/src/unit_simplify.rs @@ -0,0 +1,198 @@ +//! Simplification using unit clauses. + +use partial_ref::{partial, split_borrow, PartialRef}; + +use varisat_formula::{Lit, Var}; +use varisat_internal_proof::{clause_hash, lit_hash, DeleteClauseProof, ProofStep}; + +use crate::{ + binary::simplify_binary, + clause::db::filter_clauses, + context::{parts::*, Context}, + proof, + prop::{enqueue_assignment, Reason}, + variables, +}; + +/// Remove satisfied clauses and false literals. +pub fn prove_units<'a>( + mut ctx: partial!( + Context<'a>, + mut ImplGraphP, + mut ProofP<'a>, + mut SolverStateP, + mut TrailP, + AssignmentP, + ClauseAllocP, + VariablesP, + ), +) -> bool { + let mut new_unit = false; + + if ctx.part(TrailP).current_level() == 0 { + let (impl_graph, mut ctx) = ctx.split_part_mut(ImplGraphP); + + let mut unit_proofs = vec![]; + + let (trail, mut ctx) = ctx.split_part_mut(TrailP); + + for &lit in trail.trail() { + new_unit = true; + let ctx_lits = ctx.borrow(); + let reason = impl_graph.reason(lit.var()); + if !reason.is_unit() { + let lits = impl_graph.reason(lit.var()).lits(&ctx_lits); + let hash = clause_hash(lits) ^ lit_hash(lit); + + unit_proofs.push((lit, hash)); + } + + impl_graph.update_removed_unit(lit.var()); + } + + trail.clear(); + + if !unit_proofs.is_empty() { + proof::add_step( + ctx.borrow(), + true, + &ProofStep::UnitClauses { + units: &unit_proofs, + }, + ); + } + } + + new_unit +} + +/// Put a removed unit back onto the trail. +pub fn resurrect_unit<'a>( + mut ctx: partial!(Context<'a>, mut AssignmentP, mut ImplGraphP, mut TrailP), + lit: Lit, +) { + if ctx.part(ImplGraphP).is_removed_unit(lit.var()) { + debug_assert!(ctx.part(AssignmentP).lit_is_true(lit)); + ctx.part_mut(AssignmentP).unassign_var(lit.var()); + + // Because we always enqueue with Reason::Unit this will not cause a unit clause to be + // proven in `prove_units`. + enqueue_assignment(ctx.borrow(), lit, Reason::Unit); + } +} + +/// Remove satisfied clauses and false literals. +pub fn unit_simplify<'a>( + mut ctx: partial!( + Context<'a>, + mut AssignmentP, + mut BinaryClausesP, + mut ClauseAllocP, + mut ClauseDbP, + mut ProofP<'a>, + mut SolverStateP, + mut VariablesP, + mut WatchlistsP, + mut VsidsP, + AssumptionsP, + ), +) { + simplify_binary(ctx.borrow()); + + let (assignment, mut ctx) = ctx.split_part(AssignmentP); + + let mut new_lits = vec![]; + { + split_borrow!(proof_ctx = &(mut ProofP, mut SolverStateP, VariablesP) ctx); + let (ctx_2, mut ctx) = ctx.split_borrow(); + + 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(), + true, + &ProofStep::DeleteClause { + clause: clause.lits(), + proof: if redundant { + DeleteClauseProof::Redundant + } else { + DeleteClauseProof::Satisfied + }, + }, + ); + return false; + } + Some(false) => (), + } + } + if new_lits.len() < clause.lits().len() { + if proof_ctx.part(ProofP).is_active() { + let hash = [clause_hash(clause.lits())]; + proof::add_step( + proof_ctx.borrow(), + true, + &ProofStep::AtClause { + redundant: redundant && new_lits.len() > 2, + clause: &new_lits, + propagation_hashes: &hash[..], + }, + ); + proof::add_step( + proof_ctx.borrow(), + true, + &ProofStep::DeleteClause { + clause: clause.lits(), + proof: if redundant { + DeleteClauseProof::Redundant + } else { + DeleteClauseProof::Simplified + }, + }, + ); + } + + match new_lits[..] { + // Cannot have empty or unit clauses after full propagation. An empty clause would + // have been a conflict and a unit clause must be satisfied and thus would have been + // dropped above. + [] | [_] => unreachable!(), + [lit_0, lit_1] => { + ctx.part_mut(BinaryClausesP) + .add_binary_clause([lit_0, lit_1]); + false + } + ref lits => { + clause.lits_mut()[..lits.len()].copy_from_slice(lits); + clause.header_mut().set_len(lits.len()); + true + } + } + } else { + true + } + }); + } + + // TODO detect vars that became isolated without being having a unit clause + + for (var_index, &value) in assignment.assignment().iter().enumerate() { + let var = Var::from_index(var_index); + if !ctx.part(VariablesP).solver_var_present(var) { + continue; + } + let var_data = ctx.part_mut(VariablesP).var_data_solver_mut(var); + if let Some(value) = value { + var_data.unit = Some(value); + var_data.isolated = true; + } + if var_data.isolated && !var_data.assumed { + variables::remove_solver_var(ctx.borrow(), var); + } + } +} |