a mildly optimized sat solver
sat-solver
Fix regressions
+241
-83
-1
Cargo.lock
-1
Cargo.lock
-1
Cargo.toml
-1
Cargo.toml
+40
-7
src/alg/cdcl.rs
+40
-7
src/alg/cdcl.rs
···
111
111
.as_ref()
112
112
.expect("Should not happen");
113
113
clause_to_resolve = var_state.reason;
114
+
#[cfg(debug_assertions)]
115
+
if let Some(reason_idx) = clause_to_resolve {
116
+
let reason_cl = clauses.clause(reason_idx);
117
+
for reason_lit in reason_cl.literals() {
118
+
assert!(
119
+
trail.variable_states[reason_lit.variable.0 as usize].is_some(),
120
+
"Reason clause {:?} for var {:?} contains unassigned variable {:?}",
121
+
reason_idx, lit.variable, reason_lit.variable
122
+
);
123
+
}
124
+
}
114
125
break;
115
126
}
116
127
}
···
181
192
if trail.current_level() == 0 {
182
193
return Err(Unsat);
183
194
}
195
+
#[cfg(debug_assertions)]
196
+
{
197
+
let conflict_cl = clauses.clause(conflict);
198
+
for lit in conflict_cl.literals() {
199
+
assert!(
200
+
trail.variable_states[lit.variable.0 as usize].is_some(),
201
+
"Conflict clause {:?} contains unassigned variable {:?}",
202
+
conflict, lit.variable
203
+
);
204
+
}
205
+
let all_false = conflict_cl.literals()
206
+
.all(|lit| trail.literal_is_false(lit));
207
+
assert!(all_false, "Conflict clause {:?} is not actually all-false", conflict);
208
+
}
184
209
// b ← ConflictAnalysis(φ, α) // Diagnose stage
185
210
let analysis = conflict_analysis(&clauses, &trail, &mut scratch, conflict);
186
211
// if b < 0 then
···
191
216
// Backtrack(φ, α, b)
192
217
// d ← b // Decrement decision level due to backtracking
193
218
trail.backtrack_to(analysis.backtrack_level, &mut dec_heur);
194
-
clauses.add_learned_clause(&mut trail, &analysis.learned_clause);
195
-
stats.number_of_learned_clauses += 1;
196
-
for l in &analysis.learned_clause {
197
-
dec_heur.bump_variable(l.variable);
198
-
}
199
-
dec_heur.decay();
200
219
// Maybe restart
201
220
if let Some(restart_level) = restart.restart() &&
202
221
restart_level < trail.current_level() {
222
+
stats.number_of_restarts += 1;
203
223
trail.backtrack_to(restart_level, &mut dec_heur);
224
+
let mut locked_clauses = trail.variable_states.iter().filter_map(|vs|{
225
+
let vs = vs.as_ref()?;
226
+
let r = vs.reason?;
227
+
Some(r)
228
+
}).collect::<Vec<_>>();
229
+
locked_clauses.sort();
204
230
// delete learned clauses
205
-
for ci in deletion.clauses_to_delete(&trail, &mut clauses) {
231
+
let to_delete = deletion.clauses_to_delete(&locked_clauses, &clauses);
232
+
for ci in to_delete {
206
233
clauses.delete_clause(ci);
207
234
stats.number_of_deleted_clauses += 1;
208
235
}
209
236
break;
210
237
}
238
+
clauses.add_learned_clause(&mut trail, &analysis.learned_clause);
239
+
stats.number_of_learned_clauses += 1;
240
+
for l in &analysis.learned_clause {
241
+
dec_heur.bump_variable(l.variable);
242
+
}
243
+
dec_heur.decay();
211
244
}
212
245
}
213
246
}
+4
-4
src/alg/clause_del/lbd.rs
+4
-4
src/alg/clause_del/lbd.rs
···
1
-
use crate::alg::{Clause, ClauseCDCL, clause_del::ClauseDeletion};
1
+
use crate::alg::{Clause, ClauseCDCL, ClauseIndex, clause_del::ClauseDeletion};
2
2
3
3
#[derive(Clone)]
4
4
pub struct ShortLowLBD<S: ClauseDeletion> {
···
18
18
}
19
19
20
20
impl<S: ClauseDeletion> ClauseDeletion for ShortLowLBD<S> {
21
-
fn clauses_to_delete<C: crate::alg::prop::InterimClauses<Clause = ClauseCDCL>>(&mut self, trail: &crate::alg::Trail, clauses: &C) -> Vec<crate::alg::ClauseIndex> {
22
-
let mut to_delete = self.inner.clauses_to_delete(trail, clauses);
21
+
fn clauses_to_delete<C: crate::alg::prop::InterimClauses<Clause = ClauseCDCL>>(&mut self, locked_clauses: &[ClauseIndex], clauses: &C) -> Vec<crate::alg::ClauseIndex> {
22
+
let mut to_delete = self.inner.clauses_to_delete(locked_clauses, clauses);
23
23
for (i, clause) in clauses.iter_enumerate_clauses() {
24
-
if clause.is_learned {
24
+
if clause.is_learned && locked_clauses.binary_search(&i).is_err() {
25
25
if clause.len() <= self.max_len || clause.lbd <= self.max_lbd {
26
26
continue;
27
27
}
+10
-3
src/alg/clause_del/mod.rs
+10
-3
src/alg/clause_del/mod.rs
···
1
-
use crate::alg::{ClauseCDCL, ClauseIndex, Trail, prop::InterimClauses};
1
+
use crate::alg::{ClauseCDCL, ClauseIndex, prop::InterimClauses};
2
2
3
3
pub mod lbd;
4
4
pub mod most_active;
5
5
pub mod no_duplicates;
6
6
7
7
pub trait ClauseDeletion: Clone {
8
-
fn clauses_to_delete<C: InterimClauses<Clause = ClauseCDCL>>(&mut self, trail: &Trail, clauses: &C) -> Vec<ClauseIndex>;
8
+
fn clauses_to_delete<C: InterimClauses<Clause = ClauseCDCL>>(&mut self, locked_clauses: &[ClauseIndex], clauses: &C) -> Vec<ClauseIndex>;
9
9
}
10
10
11
11
#[derive(Clone)]
12
12
pub struct Never;
13
13
14
14
impl ClauseDeletion for Never {
15
-
fn clauses_to_delete<C: InterimClauses<Clause = ClauseCDCL>>(&mut self, _trail: &Trail, _clauses: &C) -> Vec<ClauseIndex> {
15
+
fn clauses_to_delete<C: InterimClauses<Clause = ClauseCDCL>>(&mut self, _locked_clauses: &[ClauseIndex], _clauses: &C) -> Vec<ClauseIndex> {
16
16
vec![]
17
17
}
18
18
}
19
+
20
+
#[inline]
21
+
fn insert_sorted<T: Ord>(vec: &mut Vec<T>, elem: T) {
22
+
if let Err(pos) = vec.binary_search(&elem) {
23
+
vec.insert(pos, elem);
24
+
}
25
+
}
+4
-4
src/alg/clause_del/most_active.rs
+4
-4
src/alg/clause_del/most_active.rs
···
1
-
use crate::alg::clause_del::ClauseDeletion;
1
+
use crate::alg::{ClauseIndex, clause_del::ClauseDeletion};
2
2
3
3
#[derive(Clone)]
4
4
pub struct MostActive<S> {
···
16
16
}
17
17
18
18
impl<S: ClauseDeletion> ClauseDeletion for MostActive<S> {
19
-
fn clauses_to_delete<C: crate::alg::prop::InterimClauses<Clause = crate::alg::ClauseCDCL>>(&mut self, trail: &crate::alg::Trail, clauses: &C) -> Vec<crate::alg::ClauseIndex> {
20
-
let mut to_delete = self.inner.clauses_to_delete(trail, clauses);
19
+
fn clauses_to_delete<C: crate::alg::prop::InterimClauses<Clause = crate::alg::ClauseCDCL>>(&mut self, locked_clauses: &[ClauseIndex], clauses: &C) -> Vec<crate::alg::ClauseIndex> {
20
+
let mut to_delete = self.inner.clauses_to_delete(locked_clauses, clauses);
21
21
let mut learned = Vec::new();
22
22
for (i, clause) in clauses.iter_enumerate_clauses() {
23
23
if clause.is_learned {
···
25
25
}
26
26
}
27
27
learned.sort_by_key(|&(_idx, activity)| std::cmp::Reverse(activity));
28
-
to_delete.extend(learned.iter().skip(self.keep_n).map(|&(idx, _)| idx));
28
+
to_delete.extend(learned.iter().skip(self.keep_n).map(|&(idx, _)| idx).filter(|ci| locked_clauses.binary_search(ci).is_err()));
29
29
to_delete
30
30
}
31
31
}
+10
-16
src/alg/clause_del/no_duplicates.rs
+10
-16
src/alg/clause_del/no_duplicates.rs
···
1
1
2
-
use crate::{alg::{Clause, clause_del::ClauseDeletion}, repr::cnf};
2
+
use crate::{alg::{Clause, ClauseIndex, clause_del::{ClauseDeletion, insert_sorted}}, repr::cnf};
3
3
4
4
#[derive(Clone)]
5
5
pub struct NoDuplicates<S>(S);
···
11
11
}
12
12
13
13
impl<S: ClauseDeletion> ClauseDeletion for NoDuplicates<S> {
14
-
fn clauses_to_delete<C: crate::alg::prop::InterimClauses<Clause = crate::alg::ClauseCDCL>>(&mut self, trail: &crate::alg::Trail, clauses: &C) -> Vec<crate::alg::ClauseIndex> {
15
-
let mut to_delete = self.0.clauses_to_delete(trail, clauses);
14
+
fn clauses_to_delete<C: crate::alg::prop::InterimClauses<Clause = crate::alg::ClauseCDCL>>(&mut self, locked_clauses: &[ClauseIndex], clauses: &C) -> Vec<crate::alg::ClauseIndex> {
15
+
let mut to_delete = self.0.clauses_to_delete(locked_clauses, clauses);
16
16
to_delete.sort_unstable();
17
17
to_delete.dedup();
18
18
···
22
22
if !clause.is_learned || contains(&to_delete, i) {
23
23
continue;
24
24
}
25
-
let first_var = clause.index(0).variable;
26
-
let candidate_start = seen.binary_search_by_key(&first_var, |&(_, v)| v).unwrap_or(seen.len());
25
+
let first_var = clause.sorted_index(0).variable;
26
+
let candidate_start = seen.binary_search_by_key(&first_var, |&(_, v)| v).unwrap_or_else(|x| x);
27
27
let candidates =
28
28
seen[candidate_start..]
29
29
.iter()
···
39
39
break;
40
40
}
41
41
}
42
-
if subsumed {
42
+
if subsumed && locked_clauses.binary_search(&i).is_err() {
43
43
insert_sorted(&mut to_delete, i);
44
44
continue;
45
45
}
···
49
49
if contains(&to_delete, **seen_idx) {
50
50
continue;
51
51
}
52
-
if is_subset(clause.inner(), clauses.clause(**seen_idx).inner()) {
52
+
if is_subset(clause.inner(), clauses.clause(**seen_idx).inner()) &&
53
+
locked_clauses.binary_search(seen_idx).is_err() {
53
54
insert_sorted(&mut to_delete, **seen_idx);
54
55
}
55
56
}
···
61
62
}
62
63
63
64
#[inline]
64
-
fn insert_sorted<T: Ord>(vec: &mut Vec<T>, elem: T) {
65
-
if let Err(pos) = vec.binary_search(&elem) {
66
-
vec.insert(pos, elem);
67
-
}
68
-
}
69
-
70
-
#[inline]
71
65
fn contains<T: Eq + Ord>(arr: &[T], elem: T) -> bool {
72
66
if arr.len() < 20 {
73
-
arr.iter().any(|x| *x == elem)
67
+
arr.contains(&elem)
74
68
} else{
75
69
arr.binary_search(&elem).is_ok()
76
70
}
···
83
77
}
84
78
let (mut i, mut j) = (0, 0);
85
79
while i < a.len() && j < b.len() {
86
-
match a.index(i).cmp(&b.index(j)) {
80
+
match a.sorted_index(i).cmp(&b.sorted_index(j)) {
87
81
std::cmp::Ordering::Equal => {i += 1; j +=1;},
88
82
std::cmp::Ordering::Less => return false,
89
83
std::cmp::Ordering::Greater => j += 1,
+31
-2
src/alg/mod.rs
+31
-2
src/alg/mod.rs
···
42
42
fn from_cnf(literals: impl IntoIterator<Item = cnf::Literal>) -> Self;
43
43
fn new_learned(literals: impl IntoIterator<Item = cnf::Literal>) -> Self;
44
44
fn literals(&self) -> impl Iterator<Item = cnf::Literal>;
45
+
fn sorted_literals(&self) -> impl Iterator<Item = cnf::Literal>;
45
46
fn len(&self) -> usize;
46
47
fn swap(&mut self, a: usize, b: usize);
47
48
fn index(&self, idx: usize) -> cnf::Literal;
49
+
fn sorted_index(&self, idx: usize) -> cnf::Literal;
48
50
}
49
51
50
52
impl Clause for cnf::Clause {
···
65
67
cnf::Clause::literals(self)
66
68
}
67
69
70
+
fn sorted_literals(&self) -> impl Iterator<Item = cnf::Literal> {
71
+
self.literals()
72
+
}
73
+
68
74
fn len(&self) -> usize {
69
75
cnf::Clause::len(self)
70
76
}
···
72
78
fn index(&self, idx: usize) -> cnf::Literal {
73
79
cnf::Clause::index(self, idx)
74
80
}
81
+
82
+
fn sorted_index(&self, idx: usize) -> cnf::Literal {
83
+
self.index(idx)
84
+
}
75
85
}
76
86
77
87
#[derive(Clone)]
78
88
pub struct ClauseCDCL {
89
+
// positions 0,1 = watched (may not be sorted)
79
90
clause: cnf::Clause,
91
+
// always sorted for subsumption checks
92
+
sorted: cnf::Clause,
80
93
lbd: usize,
81
94
activity: usize,
82
95
is_learned: bool,
···
90
103
91
104
impl Clause for ClauseCDCL {
92
105
fn from_cnf(literals: impl IntoIterator<Item = cnf::Literal>) -> Self {
106
+
let clause = cnf::Clause::from_cnf(literals);
93
107
Self {
94
-
clause: cnf::Clause::from_cnf(literals),
108
+
clause: clause.clone(),
109
+
sorted: clause,
95
110
lbd: 0,
96
111
activity: 0,
97
112
is_learned: false,
···
99
114
}
100
115
101
116
fn new_learned(literals: impl IntoIterator<Item = cnf::Literal>) -> Self {
117
+
let literals = literals.into_iter().collect::<Vec<_>>();
102
118
Self {
103
-
clause: cnf::Clause::from_cnf(literals),
119
+
clause: cnf::Clause::from_iter_unsorted(literals.iter().copied()),
120
+
sorted: cnf::Clause::from_iter(literals),
104
121
lbd: 0,
105
122
activity: 0,
106
123
is_learned: true,
···
109
126
110
127
fn literals(&self) -> impl Iterator<Item = cnf::Literal> {
111
128
self.clause.literals()
129
+
}
130
+
131
+
fn sorted_literals(&self) -> impl Iterator<Item = cnf::Literal> {
132
+
self.sorted.literals()
112
133
}
113
134
114
135
fn len(&self) -> usize {
···
123
144
self.clause.index(idx)
124
145
}
125
146
147
+
fn sorted_index(&self, idx: usize) -> cnf::Literal {
148
+
self.sorted.index(idx)
149
+
}
126
150
}
127
151
128
152
#[derive(Clone, Copy, Debug)]
···
153
177
}
154
178
155
179
pub fn enqueue(&mut self, literal: cnf::Literal, level: usize, reason: Option<ClauseIndex>) {
180
+
#[cfg(debug_assertions)]
181
+
// reason clause must not exist yet or be correct
182
+
if self.variable_states[literal.variable.0 as usize].is_some() {
183
+
panic!("Variable {:?} is already assigned when enqueuing {:?}", literal.variable, literal);
184
+
}
156
185
self.variable_states[literal.variable.0 as usize] = Some(VariableState {
157
186
value: literal.sign,
158
187
level,
+113
-38
src/alg/prop/watched.rs
+113
-38
src/alg/prop/watched.rs
···
1
+
use super::InterimClauses;
2
+
use crate::alg::{BaseStats, ClauseIndex, Trail};
1
3
use crate::{alg, repr::cnf};
2
-
use super::{InterimClauses};
3
-
use crate::alg::{ClauseIndex, Trail, BaseStats};
4
4
5
5
#[derive(Clone, Copy)]
6
6
struct Watch {
···
49
49
50
50
impl<C: alg::Clause> InterimClauses for WatchedLiterals<C> {
51
51
type Clause = C;
52
-
52
+
53
53
fn new(formula: &cnf::Formula) -> Self {
54
54
let mut this = Self {
55
-
clauses: formula.clauses.iter().map(|c| Some(C::from_cnf(c.literals()))).collect(),
55
+
clauses: formula
56
+
.clauses
57
+
.iter()
58
+
.map(|c| Some(C::from_cnf(c.literals())))
59
+
.collect(),
56
60
watch_list: WatchList::new(formula.num_of_vars),
57
61
};
58
62
// NOTE: cannot use iter_enumerate_clauses bcs borrows of this
59
-
for (i, clause) in this.clauses.iter().enumerate().filter_map(|(i, c)| Some((i, c.as_ref()?))) {
63
+
for (i, clause) in this
64
+
.clauses
65
+
.iter()
66
+
.enumerate()
67
+
.filter_map(|(i, c)| Some((i, c.as_ref()?)))
68
+
{
60
69
if clause.len() >= 2 {
61
70
let a = clause.index(0);
62
71
let b = clause.index(1);
63
72
let idx = ClauseIndex(i);
64
-
this.watch_list.add_watch(a, Watch { blocker: b, clause: idx });
65
-
this.watch_list.add_watch(b, Watch { blocker: a, clause: idx });
73
+
this.watch_list.add_watch(
74
+
a,
75
+
Watch {
76
+
blocker: b,
77
+
clause: idx,
78
+
},
79
+
);
80
+
this.watch_list.add_watch(
81
+
b,
82
+
Watch {
83
+
blocker: a,
84
+
clause: idx,
85
+
},
86
+
);
66
87
}
67
88
}
68
89
this
···
79
100
}
80
101
}
81
102
82
-
fn iter_clauses<'a>(&'a self) -> impl Iterator<Item = &'a C> where C: 'a {
103
+
fn iter_clauses<'a>(&'a self) -> impl Iterator<Item = &'a C>
104
+
where
105
+
C: 'a,
106
+
{
83
107
self.clauses.iter().filter_map(|c| c.as_ref())
84
108
}
85
109
86
-
fn iter_enumerate_clauses<'a>(&'a self) -> impl Iterator<Item = (ClauseIndex, &'a C)> where C: 'a {
87
-
self.clauses.iter().enumerate().filter_map(|(i, c)| Some((ClauseIndex(i), c.as_ref()?)))
110
+
fn iter_enumerate_clauses<'a>(&'a self) -> impl Iterator<Item = (ClauseIndex, &'a C)>
111
+
where
112
+
C: 'a,
113
+
{
114
+
self.clauses
115
+
.iter()
116
+
.enumerate()
117
+
.filter_map(|(i, c)| Some((ClauseIndex(i), c.as_ref()?)))
88
118
}
89
-
119
+
90
120
fn clause(&self, idx: ClauseIndex) -> &C {
91
-
self.clauses[idx.0].as_ref().expect("Should never reference a deleted clause")
121
+
self.clauses[idx.0]
122
+
.as_ref()
123
+
.expect("Should never reference a deleted clause")
92
124
}
93
125
94
126
fn clause_mut(&mut self, idx: ClauseIndex) -> &mut C {
95
-
self.clauses[idx.0].as_mut().expect("Should never reference a deleted clause")
127
+
self.clauses[idx.0]
128
+
.as_mut()
129
+
.expect("Should never reference a deleted clause")
96
130
}
97
-
98
131
99
132
fn unit_propagate(
100
133
&mut self,
···
119
152
i += 1;
120
153
continue;
121
154
}
122
-
let lits = self.clauses[watch.clause.0].as_mut().expect("Should not happen");
155
+
let lits = self.clauses[watch.clause.0]
156
+
.as_mut()
157
+
.expect("Should not happen");
123
158
if lits.index(0) == falsified_lit {
124
159
lits.swap(0, 1);
125
160
}
126
161
let other_watched = lits.index(0);
127
162
if trail.literal_is_true(other_watched) {
128
-
watches[j] = Watch { blocker: other_watched, clause: watch.clause };
163
+
watches[j] = Watch {
164
+
blocker: other_watched,
165
+
clause: watch.clause,
166
+
};
129
167
j += 1;
130
168
i += 1;
131
169
continue;
132
170
}
133
171
let mut replacement = false;
134
-
{
172
+
{
135
173
for k in 2..lits.len() {
136
174
if !trail.literal_is_false(lits.index(k)) {
137
175
lits.swap(1, k);
138
176
let new_watched = lits.index(1);
139
-
self.watch_list.add_watch(new_watched, Watch {
140
-
blocker: other_watched,
141
-
clause: watch.clause,
142
-
});
177
+
self.watch_list.add_watch(
178
+
new_watched,
179
+
Watch {
180
+
blocker: other_watched,
181
+
clause: watch.clause,
182
+
},
183
+
);
143
184
replacement = true;
185
+
break;
144
186
}
145
187
}
146
188
}
···
148
190
i += 1;
149
191
continue;
150
192
}
151
-
watches[j] = Watch { blocker: other_watched, clause: watch.clause };
193
+
watches[j] = Watch {
194
+
blocker: other_watched,
195
+
clause: watch.clause,
196
+
};
152
197
i += 1;
153
198
j += 1;
154
199
if trail.literal_is_false(other_watched) {
···
156
201
conflict = Some(watch.clause);
157
202
break;
158
203
} else {
204
+
#[cfg(debug_assertions)]
205
+
{
206
+
let reason_cl = &self.clauses[watch.clause.0].as_ref().unwrap();
207
+
for reason_lit in reason_cl.literals() {
208
+
if reason_lit.variable != other_watched.variable {
209
+
assert!(
210
+
trail.literal_is_false(reason_lit),
211
+
"About to enqueue {:?} with reason {:?} but literal {:?} in reason is not false",
212
+
other_watched,
213
+
watch.clause,
214
+
reason_lit
215
+
);
216
+
}
217
+
}
218
+
}
159
219
trail.enqueue(other_watched, trail.current_level(), Some(watch.clause));
160
220
}
161
221
}
···
170
230
Ok(())
171
231
}
172
232
173
-
fn add_learned_clause(
174
-
&mut self,
175
-
trail: &mut Trail,
176
-
learned: &[cnf::Literal],
177
-
) -> ClauseIndex {
233
+
fn add_learned_clause(&mut self, trail: &mut Trail, learned: &[cnf::Literal]) -> ClauseIndex {
178
234
let idx = ClauseIndex(self.clauses.len());
179
235
self.clauses.push(Some(C::new_learned(learned.to_vec())));
180
236
if learned.len() == 1 {
181
237
trail.enqueue(learned[0], 0, Some(idx));
182
-
} else {
183
-
self.watch_list.add_watch(learned[0], Watch { blocker: learned[1], clause: idx });
184
-
self.watch_list.add_watch(learned[1], Watch { blocker: learned[0], clause: idx });
185
-
trail.enqueue(learned[0], trail.current_level(), Some(idx));
238
+
return idx;
186
239
}
240
+
241
+
self.watch_list.add_watch(
242
+
learned[0],
243
+
Watch {
244
+
blocker: learned[1],
245
+
clause: idx,
246
+
},
247
+
);
248
+
self.watch_list.add_watch(
249
+
learned[1],
250
+
Watch {
251
+
blocker: learned[0],
252
+
clause: idx,
253
+
},
254
+
);
255
+
trail.enqueue(learned[0], trail.current_level(), Some(idx));
256
+
187
257
idx
188
258
}
189
259
190
-
fn delete_clause(
191
-
&mut self,
192
-
clause: ClauseIndex,
193
-
) {
194
-
for var_watch in &mut self.watch_list.0 {
195
-
var_watch.positive.retain(|w| w.clause != clause);
196
-
var_watch.negative.retain(|w| w.clause != clause);
260
+
fn delete_clause(&mut self, clause: ClauseIndex) {
261
+
if let Some(cl) = &self.clauses[clause.0]
262
+
&& cl.len() >= 2
263
+
{
264
+
let a = cl.index(0);
265
+
let b = cl.index(1);
266
+
self.watch_list
267
+
.watches_for_mut(a)
268
+
.retain(|w| w.clause != clause);
269
+
self.watch_list
270
+
.watches_for_mut(b)
271
+
.retain(|w| w.clause != clause);
197
272
}
198
273
self.clauses[clause.0] = None;
199
274
}
+1
-1
src/alg/restart/luby.rs
+1
-1
src/alg/restart/luby.rs
···
13
13
fn next_luby(&mut self) {
14
14
// there is no siple cast of usize to isize that is safe
15
15
// without a lot of casts, this works due to two's complement
16
-
if self.u & (!self.u + 1) == self.v {
16
+
if self.u & self.u.wrapping_neg() == self.v {
17
17
self.u += 1;
18
18
self.v = 1;
19
19
} else {
+12
-6
src/lib.rs
+12
-6
src/lib.rs
···
1
1
use clap::ValueEnum;
2
2
use miette::IntoDiagnostic;
3
-
use owo_colors::OwoColorize;
4
3
5
4
use crate::{arg::{AlgorithmKind, Args}, repr::WithMeta};
6
5
···
25
24
stats: Box<dyn alg::Stats>,
26
25
mut w: W,
27
26
) -> miette::Result<()> {
27
+
use tabled::settings::{*, style::*};
28
+
28
29
let mut table_b = tabled::builder::Builder::new();
29
30
let mut horizontals = vec![];
31
+
let mut colorize_result = Color::BOLD;
30
32
match result {
31
33
Ok(alg::Sat { mut model }) => {
32
-
table_b.push_record(["result", &format!("{}", "SAT".green().bold())]);
33
-
horizontals.push((table_b.count_records(), tabled::settings::style::HorizontalLine::inherit(tabled::settings::Style::modern()).horizontal('=')));
34
+
table_b.push_record(["result", "SAT"]);
35
+
colorize_result = colorize_result | Color::FG_BRIGHT_GREEN;
36
+
37
+
horizontals.push((table_b.count_records(), HorizontalLine::inherit(Style::modern_rounded())));
34
38
table_b.push_record(["variable", "original variable"]);
35
39
model.sort_by_key(|a| a.1);
36
40
for s in &model {
···
38
42
}
39
43
}
40
44
Err(alg::Unsat) => {
41
-
table_b.push_record(["result", &format!("{}", "UNSAT".red().bold())]);
45
+
table_b.push_record(["result", "UNSAT"]);
46
+
colorize_result = colorize_result | Color::FG_BRIGHT_RED;
42
47
}
43
48
}
44
-
horizontals.push((table_b.count_records(), tabled::settings::style::HorizontalLine::inherit(tabled::settings::Style::modern()).horizontal('=')));
49
+
horizontals.push((table_b.count_records(), HorizontalLine::inherit(Style::modern_rounded())));
45
50
table_b.push_record(["input", (args.input.as_ref().map(|i| i as &str)).unwrap_or("<stdin>")]);
46
51
table_b.push_record(["algorithm", &format!("{}", args.algorithm)]);
47
52
table_b.push_record(["decision heuristic", &format!("{}", args.decision_heuristic)]);
···
50
55
table_b.push_record(["restarts", &format!("{}", args.restarts)]);
51
56
table_b.push_record(["clause deletion", &format!("{}", args.clause_deletion)]);
52
57
}
53
-
horizontals.push((table_b.count_records(), tabled::settings::style::HorizontalLine::inherit(tabled::settings::Style::modern()).horizontal('=')));
58
+
horizontals.push((table_b.count_records(), HorizontalLine::inherit(Style::modern_rounded())));
54
59
stats.table(&mut table_b, args.deterministic);
55
60
let mut table = table_b.build();
56
61
let style = {
···
62
67
style
63
68
};
64
69
table.with(style);
70
+
table.with(tabled::settings::themes::Colorization::exact([colorize_result], tabled::settings::object::Cell::new(0, 1)));
65
71
write!(w, "{}", table).into_diagnostic()?;
66
72
Ok(())
67
73
}
+16
src/repr/cnf.rs
+16
src/repr/cnf.rs
···
115
115
}
116
116
}
117
117
118
+
/// Create a deliberately unsorted clause
119
+
/// you likely don't want this!
120
+
pub(crate) fn from_iter_unsorted(literals: impl IntoIterator<Item = Literal>) -> Self {
121
+
let mut vars = SmallVec::new();
122
+
let mut signs = SmallVec::new();
123
+
124
+
for lit in literals.into_iter() {
125
+
signs.push(lit.sign);
126
+
vars.push(lit.variable);
127
+
}
128
+
Self {
129
+
signs,
130
+
vars,
131
+
}
132
+
}
133
+
118
134
pub fn literals(&self) -> impl Iterator<Item = Literal> {
119
135
self.signs.iter().zip(self.vars.iter()).map(|(s, v)| Literal { sign: *s, variable: *v })
120
136
}