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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
#[cfg(feature = "mem_dbg")]
use mem_dbg::{MemDbg, MemSize};
use super::{CdclIdx, ENodeIdx, InstIdx, LitIdx, StackIdx, TermIdx, TheoryKind};
/// A boolean term which has been assigned either true or false.
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug, Clone)]
pub struct Literal {
pub term: Assignment,
pub frame: StackIdx,
// Same as for `enode` below. We assume that if the equality was assigned
// during an instantiation then that instantiation is to blame for the
// assignment.
pub iblame: Option<InstIdx>,
// Ideally we would work backwards from the assignment to figure out
// everyone to blame for it. Unfortunately due to z3 issues (see comment of
// `parse_bool_literal`) we cannot do this. Instead we assume that the
// creator of the corresponding enode (if there is one) is to blame.
pub enode: Option<ENodeIdx>,
pub justification: Justification,
}
/// The reason for an assignment.
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[derive(Debug, Clone, Copy, Default)]
pub enum JustificationKind {
/// The assignment was derived from an internal axiom.
Axiom,
/// The assignment was a CDCL decision.
Decision,
/// The assignment was derived from a theory.
Theory(TheoryKind),
/// The assignment was due to a yet unsatisfied or-clause, where all other
/// literals are already assigned. The or-clause is all `blamed` assignments
/// negated + my assignment.
Propagate,
/// Appears only if a parsing error occurred.
#[default]
Error,
}
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug, Clone, Default)]
pub struct Justification {
pub kind: JustificationKind,
// Issue 3: No way to convert LitId -> TermIdx
#[cfg(any())]
/// The assignments this justification depends on.
pub blamed: BoxSlice<LitIdx>,
}
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone)]
pub struct Cdcl {
pub kind: CdclKind,
pub frame: StackIdx,
/// After an assignment some clauses may have only 1 unassigned literal
/// left (with all others not satisfying the clause). Thus a decision
/// propagates other assignments which are required.
pub propagates: Vec<LitIdx>,
pub conflicts: bool,
}
impl Cdcl {
fn new(kind: CdclKind, frame: StackIdx) -> Self {
Self {
kind,
frame,
propagates: Vec::new(),
conflicts: false,
}
}
/// Creates the `Root` node of the CDCL tree. Should only be used once.
pub fn root(frame: StackIdx) -> Self {
Self::new(CdclKind::Root, frame)
}
/// Creates a `BeginCheck` node in the CDCL tree.
pub fn begin_check(parent: Option<CdclIdx>, frame: StackIdx) -> Self {
Self::new(CdclKind::BeginCheck(parent), frame)
}
/// Creates a `Empty` node in the CDCL tree.
pub fn new_empty(parent: CdclIdx, frame: StackIdx) -> Self {
Self::new(CdclKind::Empty(parent), frame)
}
pub fn new_decision(lit: LitIdx, frame: StackIdx) -> Self {
Self::new(CdclKind::Decision(lit), frame)
}
pub fn new_conflict(conflict: Conflict, frame: StackIdx) -> Self {
Self::new(CdclKind::Conflict(conflict), frame)
}
/// Return a pair of the previous node and the backtrack node. If the
/// backtrack node is set then its the parent otherwise the previous node is
pub fn backlink(&self, cidx: CdclIdx) -> CdclBacklink {
if matches!(self.kind, CdclKind::Root) {
return CdclBacklink::default();
}
let previous = usize::from(cidx).checked_sub(1).map(CdclIdx::from);
let previous = previous.unwrap();
match self.kind {
CdclKind::Root => unreachable!(),
CdclKind::BeginCheck(backtrack) => CdclBacklink {
previous: Some(previous).filter(|&p| backtrack.is_some_and(|b| p != b)),
backtrack: Some(backtrack.unwrap_or(CdclIdx::ZERO)),
sidetrack: true,
},
CdclKind::Empty(backtrack) => CdclBacklink {
previous: Some(previous).filter(|&p| p != backtrack),
backtrack: Some(backtrack),
sidetrack: true,
},
CdclKind::Decision(..) => CdclBacklink {
previous: Some(previous),
backtrack: None,
sidetrack: false,
},
CdclKind::Conflict(ref conflict) => CdclBacklink {
previous: Some(previous),
backtrack: Some(conflict.backtrack),
sidetrack: false,
},
}
}
pub fn get_assignments(&self) -> impl Iterator<Item = LitIdx> + '_ {
let first = match &self.kind {
CdclKind::Decision(assign) => Some(*assign),
_ => None,
};
first.into_iter().chain(self.propagates.iter().copied())
}
}
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone)]
pub enum CdclKind {
/// Represents an empty node. Used as the root of the CDCL tree (in which
/// the solver may already propagate some facts).
Root,
/// Represents an empty node. Used to indicate that assignments are reset
/// between begin-checks.
BeginCheck(Option<CdclIdx>),
/// Same as `Root` but used when assignments are propagated at a different
/// stack frame than the current decision. The frame of the current decision
/// may have been popped, thus this points to where it should be slotted in.
Empty(CdclIdx),
/// The branching decision z3 took, it "arbitrarily" decided that this
/// clause has this boolean value.
Decision(LitIdx),
Conflict(Conflict),
}
/// Assignment to a literal.
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct Assignment {
/// The boolean term that was assigned.
pub literal: TermIdx,
/// Was it assigned true or false?
pub value: bool,
}
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone)]
pub struct Conflict {
pub cut: Box<[Assignment]>,
/// Which decision to backtrack to (i.e. which one is this conflict rooted
/// from and all between are reverted). If `None` then we backtrack all.
pub backtrack: CdclIdx,
}
#[derive(Debug, Clone, Copy, Default)]
pub struct CdclBacklink {
/// Always `Some` with a one smaller value, unless at the root or at a
/// side-track `Empty` node where previous and backtrack would be the same.
pub previous: Option<CdclIdx>,
/// The node to back-jump to.
pub backtrack: Option<CdclIdx>,
pub sidetrack: bool,
}
impl CdclBacklink {
pub fn to_root(&self) -> Option<CdclIdx> {
self.backtrack.or(self.previous)
}
}