smt_scope/items/
cdcl.rs

1#[cfg(feature = "mem_dbg")]
2use mem_dbg::{MemDbg, MemSize};
3
4use super::{CdclIdx, ENodeIdx, InstIdx, LitIdx, StackIdx, TermIdx, TheoryKind};
5
6/// A boolean term which has been assigned either true or false.
7#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
8#[derive(Debug, Clone)]
9pub struct Literal {
10    pub term: Assignment,
11    pub frame: StackIdx,
12    // Same as for `enode` below. We assume that if the equality was assigned
13    // during an instantiation then that instantiation is to blame for the
14    // assignment.
15    pub iblame: Option<InstIdx>,
16    // Ideally we would work backwards from the assignment to figure out
17    // everyone to blame for it. Unfortunately due to z3 issues (see comment of
18    // `parse_bool_literal`) we cannot do this. Instead we assume that the
19    // creator of the corresponding enode (if there is one) is to blame.
20    pub enode: Option<ENodeIdx>,
21    pub justification: Justification,
22}
23
24/// The reason for an assignment.
25#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
26#[cfg_attr(feature = "mem_dbg", copy_type)]
27#[derive(Debug, Clone, Copy, Default)]
28pub enum JustificationKind {
29    /// The assignment was derived from an internal axiom.
30    Axiom,
31    /// The assignment was a CDCL decision.
32    Decision,
33    /// The assignment was derived from a theory.
34    Theory(TheoryKind),
35    /// The assignment was due to a yet unsatisfied or-clause, where all other
36    /// literals are already assigned. The or-clause is all `blamed` assignments
37    /// negated + my assignment.
38    Propagate,
39    /// Appears only if a parsing error occurred.
40    #[default]
41    Error,
42}
43
44#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
45#[derive(Debug, Clone, Default)]
46pub struct Justification {
47    pub kind: JustificationKind,
48    // Issue 3: No way to convert LitId -> TermIdx
49    #[cfg(any())]
50    /// The assignments this justification depends on.
51    pub blamed: BoxSlice<LitIdx>,
52}
53
54#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
55#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
56#[derive(Debug, Clone)]
57pub struct Cdcl {
58    pub kind: CdclKind,
59    pub frame: StackIdx,
60    /// After an assignment some clauses may have only 1 unassigned literal
61    /// left (with all others not satisfying the clause). Thus a decision
62    /// propagates other assignments which are required.
63    pub propagates: Vec<LitIdx>,
64    pub conflicts: bool,
65}
66
67impl Cdcl {
68    fn new(kind: CdclKind, frame: StackIdx) -> Self {
69        Self {
70            kind,
71            frame,
72            propagates: Vec::new(),
73            conflicts: false,
74        }
75    }
76
77    /// Creates the `Root` node of the CDCL tree. Should only be used once.
78    pub fn root(frame: StackIdx) -> Self {
79        Self::new(CdclKind::Root, frame)
80    }
81
82    /// Creates a `BeginCheck` node in the CDCL tree.
83    pub fn begin_check(parent: Option<CdclIdx>, frame: StackIdx) -> Self {
84        Self::new(CdclKind::BeginCheck(parent), frame)
85    }
86
87    /// Creates a `Empty` node in the CDCL tree.
88    pub fn new_empty(parent: CdclIdx, frame: StackIdx) -> Self {
89        Self::new(CdclKind::Empty(parent), frame)
90    }
91
92    pub fn new_decision(lit: LitIdx, frame: StackIdx) -> Self {
93        Self::new(CdclKind::Decision(lit), frame)
94    }
95
96    pub fn new_conflict(conflict: Conflict, frame: StackIdx) -> Self {
97        Self::new(CdclKind::Conflict(conflict), frame)
98    }
99
100    /// Return a pair of the previous node and the backtrack node. If the
101    /// backtrack node is set then its the parent otherwise the previous node is
102    pub fn backlink(&self, cidx: CdclIdx) -> CdclBacklink {
103        if matches!(self.kind, CdclKind::Root) {
104            return CdclBacklink::default();
105        }
106        let previous = usize::from(cidx).checked_sub(1).map(CdclIdx::from);
107        let previous = previous.unwrap();
108        match self.kind {
109            CdclKind::Root => unreachable!(),
110            CdclKind::BeginCheck(backtrack) => CdclBacklink {
111                previous: Some(previous).filter(|&p| backtrack.is_some_and(|b| p != b)),
112                backtrack: Some(backtrack.unwrap_or(CdclIdx::ZERO)),
113                sidetrack: true,
114            },
115            CdclKind::Empty(backtrack) => CdclBacklink {
116                previous: Some(previous).filter(|&p| p != backtrack),
117                backtrack: Some(backtrack),
118                sidetrack: true,
119            },
120            CdclKind::Decision(..) => CdclBacklink {
121                previous: Some(previous),
122                backtrack: None,
123                sidetrack: false,
124            },
125            CdclKind::Conflict(ref conflict) => CdclBacklink {
126                previous: Some(previous),
127                backtrack: Some(conflict.backtrack),
128                sidetrack: false,
129            },
130        }
131    }
132
133    pub fn get_assignments(&self) -> impl Iterator<Item = LitIdx> + '_ {
134        let first = match &self.kind {
135            CdclKind::Decision(assign) => Some(*assign),
136            _ => None,
137        };
138        first.into_iter().chain(self.propagates.iter().copied())
139    }
140}
141
142#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
143#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
144#[derive(Debug, Clone)]
145pub enum CdclKind {
146    /// Represents an empty node. Used as the root of the CDCL tree (in which
147    /// the solver may already propagate some facts).
148    Root,
149    /// Represents an empty node. Used to indicate that assignments are reset
150    /// between begin-checks.
151    BeginCheck(Option<CdclIdx>),
152    /// Same as `Root` but used when assignments are propagated at a different
153    /// stack frame than the current decision. The frame of the current decision
154    /// may have been popped, thus this points to where it should be slotted in.
155    Empty(CdclIdx),
156    /// The branching decision z3 took, it "arbitrarily" decided that this
157    /// clause has this boolean value.
158    Decision(LitIdx),
159    Conflict(Conflict),
160}
161
162/// Assignment to a literal.
163#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
164#[cfg_attr(feature = "mem_dbg", copy_type)]
165#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
166#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
167pub struct Assignment {
168    /// The boolean term that was assigned.
169    pub literal: TermIdx,
170    /// Was it assigned true or false?
171    pub value: bool,
172}
173
174#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
175#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
176#[derive(Debug, Clone)]
177pub struct Conflict {
178    pub cut: Box<[Assignment]>,
179    /// Which decision to backtrack to (i.e. which one is this conflict rooted
180    /// from and all between are reverted). If `None` then we backtrack all.
181    pub backtrack: CdclIdx,
182}
183
184#[derive(Debug, Clone, Copy, Default)]
185pub struct CdclBacklink {
186    /// Always `Some` with a one smaller value, unless at the root or at a
187    /// side-track `Empty` node where previous and backtrack would be the same.
188    pub previous: Option<CdclIdx>,
189    /// The node to back-jump to.
190    pub backtrack: Option<CdclIdx>,
191    pub sidetrack: bool,
192}
193
194impl CdclBacklink {
195    pub fn to_root(&self) -> Option<CdclIdx> {
196        self.backtrack.or(self.previous)
197    }
198}
smt_scope/items/cdcl.rs

smt_scope/items/
cdcl.rs
