Skip to content

Commit

Permalink
also renamed in Clauses
Browse files Browse the repository at this point in the history
  • Loading branch information
baszalmstra committed Jan 9, 2025
1 parent 2af2e47 commit 89a12db
Showing 1 changed file with 10 additions and 4 deletions.
14 changes: 10 additions & 4 deletions src/solver/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1463,8 +1463,10 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
let clause_id = self.clauses.alloc(state, kind);
self.learnt_clause_ids.push(clause_id);
if has_watches {
self.watches
.start_watching(&mut self.clauses.watched_literals[clause_id.to_usize()], clause_id);
self.watches.start_watching(
&mut self.clauses.watched_literals[clause_id.to_usize()],
clause_id,
);
}

tracing::debug!("│├ Learnt disjunction:",);
Expand Down Expand Up @@ -1730,7 +1732,9 @@ async fn add_clauses_for_solvables<D: DependencyProvider>(
WatchedLiterals::lock(locked_solvable_var, other_candidate_var);
let clause_id = clauses.alloc(state, kind);

debug_assert!(clauses.watched_literals[clause_id.to_usize()].has_watches());
debug_assert!(
clauses.watched_literals[clause_id.to_usize()].has_watches()
);
output.clauses_to_watch.push(clause_id);
}
}
Expand Down Expand Up @@ -1814,7 +1818,9 @@ async fn add_clauses_for_solvables<D: DependencyProvider>(
name_id,
);
let clause_id = clauses.alloc(state, kind);
debug_assert!(clauses.watched_literals[clause_id.to_usize()].has_watches());
debug_assert!(
clauses.watched_literals[clause_id.to_usize()].has_watches()
);
output.clauses_to_watch.push(clause_id);
},
|| variable_map.alloc_forbid_multiple_variable(name_id),
Expand Down

0 comments on commit 89a12db

Please sign in to comment.