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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
//! The implication graph.
use partial_ref::{partial, PartialRef};
use varisat_formula::{lit::LitIdx, Lit, Var};
use crate::{
clause::ClauseRef,
context::{parts::*, Context},
};
/// Assignments that caused a propagation.
#[derive(Copy, Clone, Eq, PartialEq, Debug)]
pub enum Reason {
Unit,
Binary([Lit; 1]),
Long(ClauseRef),
}
impl Reason {
/// The literals that caused the propagation.
pub fn lits<'out, 'a, 'b>(&'a self, ctx: &'b partial!('b Context, ClauseAllocP)) -> &'out [Lit]
where
'a: 'out,
'b: 'out,
{
match self {
Reason::Unit => &[],
Reason::Binary(lit) => lit,
// The propagated literal is always kept at position 0
Reason::Long(cref) => &ctx.part(ClauseAllocP).clause(*cref).lits()[1..],
}
}
/// True if a unit clause or assumption and not a propagation.
pub fn is_unit(&self) -> bool {
match self {
Reason::Unit => true,
_ => false,
}
}
}
/// Propagation that resulted in a conflict.
#[derive(Copy, Clone, Eq, PartialEq, Debug)]
pub enum Conflict {
Binary([Lit; 2]),
Long(ClauseRef),
}
impl Conflict {
/// The literals that caused the conflict.
pub fn lits<'out, 'a, 'b>(&'a self, ctx: &'b partial!('b Context, ClauseAllocP)) -> &'out [Lit]
where
'a: 'out,
'b: 'out,
{
match self {
Conflict::Binary(lits) => lits,
Conflict::Long(cref) => ctx.part(ClauseAllocP).clause(*cref).lits(),
}
}
}
/// Node and incoming edges of the implication graph.
#[derive(Copy, Clone)]
pub struct ImplNode {
pub reason: Reason,
pub level: LitIdx,
/// Position in trail when assigned, `LitIdx::max_value()` is used as sentinel for removed
/// units.
pub depth: LitIdx,
}
/// The implication graph.
///
/// This is a DAG having all assigned variables as nodes. It has unit clauses, assumptions and
/// decisions as sources. For each propagated assignment it has incomming edges from the literals
/// whose assignment caused the propagation to happen.
#[derive(Default)]
pub struct ImplGraph {
/// Contains only valid data for indices of assigned variables.
pub nodes: Vec<ImplNode>,
}
impl ImplGraph {
/// Update structures for a new variable count.
pub fn set_var_count(&mut self, count: usize) {
self.nodes.resize(
count,
ImplNode {
reason: Reason::Unit,
level: 0,
depth: 0,
},
);
}
/// Get the reason for an assigned variable.
///
/// Returns stale data if the variable isn't assigned.
pub fn reason(&self, var: Var) -> &Reason {
&self.nodes[var.index()].reason
}
/// Get the decision level of an assigned variable.
///
/// Returns stale data if the variable isn't assigned.
pub fn level(&self, var: Var) -> usize {
self.nodes[var.index()].level as usize
}
/// Get the trail depth of an assigned variable.
///
/// Returns stale data if the variable isn't assigned.
pub fn depth(&self, var: Var) -> usize {
self.nodes[var.index()].depth as usize
}
/// Updates the reason for an assigned variable.
///
/// Make sure the reason vars are in front of the assigned variable in the trail.
pub fn update_reason(&mut self, var: Var, reason: Reason) {
self.nodes[var.index()].reason = reason
}
/// Updates the reason and depth of a unit clause removed from the trail.
pub fn update_removed_unit(&mut self, var: Var) {
let node = &mut self.nodes[var.index()];
node.reason = Reason::Unit;
node.depth = LitIdx::max_value();
}
pub fn is_removed_unit(&self, var: Var) -> bool {
self.nodes[var.index()].depth == LitIdx::max_value()
}
}
|
