1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
use std::io::{self, Write};
use varisat_formula::Lit;
use varisat_internal_proof::ProofStep;
fn drat_step(
step: &ProofStep,
mut emit_drat_step: impl FnMut(bool, &[Lit]) -> io::Result<()>,
) -> io::Result<()> {
match step {
ProofStep::AtClause { clause, .. } => {
emit_drat_step(true, &clause)?;
}
ProofStep::UnitClauses { units } => {
for &(unit, _hash) in units.iter() {
emit_drat_step(true, &[unit])?;
}
}
ProofStep::DeleteClause { clause, .. } => {
emit_drat_step(false, &clause[..])?;
}
ProofStep::SolverVarName { .. }
| ProofStep::UserVarName { .. }
| ProofStep::DeleteVar { .. }
| ProofStep::ChangeSamplingMode { .. }
| ProofStep::ChangeHashBits { .. }
| ProofStep::Model { .. }
| ProofStep::End => (),
ProofStep::AddClause { .. } => {
panic!("incremental clause additions not supported by DRAT proofs");
}
ProofStep::Assumptions { .. } | ProofStep::FailedAssumptions { .. } => {
panic!("assumptions not supported by DRAT proofs");
}
}
Ok(())
}
pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::Result<()> {
drat_step(step, |add, clause| {
if !add {
target.write_all(b"d ")?;
}
write_literals(target, &clause[..])?;
Ok(())
})
}
pub fn write_binary_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::Result<()> {
drat_step(step, |add, clause| {
if add {
target.write_all(b"a")?;
} else {
target.write_all(b"d")?;
}
write_binary_literals(target, &clause[..])?;
Ok(())
})
}
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(())
}
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(())
}