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
//! Propagation of long clauses.
use partial_ref::{partial, PartialRef};
use varisat_formula::Lit;
use crate::context::{parts::*, Context};
use super::{assignment::fast_option_eq, enqueue_assignment, Conflict, Reason, Watch};
/// Propagate all literals implied by long clauses watched by the given literal.
///
/// On conflict return the clause propgating the conflicting assignment.
///
/// See [`prop::watch`](crate::prop::watch) for the invariants that this has to uphold.
pub fn propagate_long(
mut ctx: partial!(
Context,
mut AssignmentP,
mut ImplGraphP,
mut TrailP,
mut WatchlistsP,
mut ClauseAllocP,
),
lit: Lit,
) -> Result<(), Conflict> {
// The code below is heavily optimized and replaces a much nicer but sadly slower version.
// Nevertheless it still performs full bound checks. Therefore this function is safe to call
// even when some other code violated invariants of for example the clause db.
unsafe {
let (watchlists, mut ctx) = ctx.split_part_mut(WatchlistsP);
let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP);
let watch_begin;
let watch_end;
{
let watch_list = &mut watchlists.watched_by_mut(lit);
watch_begin = watch_list.as_mut_ptr();
watch_end = watch_begin.add(watch_list.len());
}
let mut watch_ptr = watch_begin;
let false_lit = !lit;
let mut watch_write = watch_ptr;
let assignment_limit = ctx.part(AssignmentP).assignment().len();
let assignment_ptr = ctx.part(AssignmentP).assignment().as_ptr();
let is_true = |lit: Lit| {
assert!(lit.index() < assignment_limit);
fast_option_eq(*assignment_ptr.add(lit.index()), Some(lit.is_positive()))
};
let is_false = |lit: Lit| {
assert!(lit.index() < assignment_limit);
fast_option_eq(*assignment_ptr.add(lit.index()), Some(lit.is_negative()))
};
'watchers: while watch_ptr != watch_end {
let watch = *watch_ptr;
watch_ptr = watch_ptr.add(1);
// If the blocking literal (which is part of the watched clause) is already true, the
// watched clause is satisfied and we don't even have to look at it.
if is_true(watch.blocking) {
*watch_write = watch;
watch_write = watch_write.add(1);
continue;
}
let cref = watch.cref;
// Make sure we can access at least 3 lits
alloc.check_bounds(cref, 3);
let clause_ptr = alloc.lits_ptr_mut_unchecked(cref);
let &mut header = alloc.header_unchecked_mut(cref);
// First we ensure that the literal we're currently propagating is at index 1. This
// prepares the literal order for further propagations, as the propagating literal has
// to be at index 0. Doing this here also avoids a similar check later should the clause
// be satisfied by a non-watched literal, as we can just move it to index 1.
let mut first = *clause_ptr.add(0);
if first == false_lit {
let c1 = *clause_ptr.add(1);
first = c1;
*clause_ptr.add(0) = c1;
*clause_ptr.add(1) = false_lit;
}
// We create a new watch with the other watched literal as blocking literal. This will
// either replace the currently processed watch or be added to another literals watch
// list.
let new_watch = Watch {
cref,
blocking: first,
};
// If the other watched literal (now the first) isn't the blocking literal, check
// whether that one is true. If so nothing else needs to be done.
if first != watch.blocking && is_true(first) {
*watch_write = new_watch;
watch_write = watch_write.add(1);
continue;
}
// At this point we try to find a non-false unwatched literal to replace our current
// literal as the watched literal.
let clause_len = header.len();
let mut lit_ptr = clause_ptr.add(2);
let lit_end = clause_ptr.add(clause_len);
// Make sure we can access all clause literals.
alloc.check_bounds(cref, clause_len);
while lit_ptr != lit_end {
let rest_lit = *lit_ptr;
if !is_false(rest_lit) {
// We found a non-false literal and make it a watched literal by reordering the
// literals and adding the watch to the corresponding watchlist.
*clause_ptr.offset(1) = rest_lit;
*lit_ptr = false_lit;
// We're currently using unsafe to modify the watchlist of lit, so make extra
// sure we're not aliasing.
assert_ne!(!rest_lit, lit);
watchlists.add_watch(!rest_lit, new_watch);
continue 'watchers;
}
lit_ptr = lit_ptr.add(1);
}
// We didn't find a non-false unwatched literal, so either we're propagating or we have
// a conflict.
*watch_write = new_watch;
watch_write = watch_write.add(1);
// If the other watched literal is false we have a conflict.
if is_false(first) {
// We move all unprocessed watches and resize the currentl watchlist.
while watch_ptr != watch_end {
*watch_write = *watch_ptr;
watch_write = watch_write.add(1);
watch_ptr = watch_ptr.add(1);
}
let out_size = ((watch_write as usize) - (watch_begin as usize))
/ std::mem::size_of::<Watch>();
watchlists.watched_by_mut(lit).truncate(out_size as usize);
return Err(Conflict::Long(cref));
}
// Otherwise we enqueue a new propagation.
enqueue_assignment(ctx.borrow(), first, Reason::Long(cref));
}
let out_size =
((watch_write as usize) - (watch_begin as usize)) / std::mem::size_of::<Watch>();
watchlists.watched_by_mut(lit).truncate(out_size as usize);
}
Ok(())
}