use varisat_formula::{Lit, Var};
pub mod binary_format;
mod vli_enc;
pub type ClauseHash = u64;
pub fn lit_hash(lit: Lit) -> ClauseHash {
lit_code_hash(lit.code())
}
pub fn lit_code_hash(lit_code: usize) -> ClauseHash {
(!(lit_code as u64)).wrapping_mul(0x61c8864680b583ebu64)
}
pub fn clause_hash(lits: &[Lit]) -> ClauseHash {
let mut hash = 0;
for &lit in lits {
hash ^= lit_hash(lit);
}
hash
}
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
pub enum DeleteClauseProof {
Redundant,
Simplified,
Satisfied,
}
#[derive(Copy, Clone, Debug)]
pub enum ProofStep<'a> {
SolverVarName { global: Var, solver: Option<Var> },
UserVarName { global: Var, user: Option<Var> },
DeleteVar { var: Var },
ChangeSamplingMode { var: Var, sample: bool },
AddClause { clause: &'a [Lit] },
AtClause {
redundant: bool,
clause: &'a [Lit],
propagation_hashes: &'a [ClauseHash],
},
UnitClauses { units: &'a [(Lit, ClauseHash)] },
DeleteClause {
clause: &'a [Lit],
proof: DeleteClauseProof,
},
ChangeHashBits { bits: u32 },
Model { assignment: &'a [Lit] },
Assumptions { assumptions: &'a [Lit] },
FailedAssumptions {
failed_core: &'a [Lit],
propagation_hashes: &'a [ClauseHash],
},
End,
}
impl<'a> ProofStep<'a> {
pub fn contains_hashes(&self) -> bool {
match self {
ProofStep::AtClause { .. }
| ProofStep::UnitClauses { .. }
| ProofStep::FailedAssumptions { .. } => true,
ProofStep::SolverVarName { .. }
| ProofStep::UserVarName { .. }
| ProofStep::DeleteVar { .. }
| ProofStep::ChangeSamplingMode { .. }
| ProofStep::AddClause { .. }
| ProofStep::DeleteClause { .. }
| ProofStep::ChangeHashBits { .. }
| ProofStep::Model { .. }
| ProofStep::Assumptions { .. }
| ProofStep::End => false,
}
}
}