Skip to content

Commit

Permalink
Keep completed assignments. (#2331)
Browse files Browse the repository at this point in the history
If we want to propagate range constraints across completed assignments,
we cannot delete them.
  • Loading branch information
chriseth authored Jan 13, 2025
1 parent fe4e2b2 commit 5a47b6e
Showing 1 changed file with 15 additions and 19 deletions.
34 changes: 15 additions & 19 deletions executor/src/witgen/jit/witgen_inference.rs
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ pub struct WitgenInference<'a, T: FieldElement, FixedEval> {
fixed_evaluator: FixedEval,
derived_range_constraints: HashMap<Variable, RangeConstraint<T>>,
known_variables: HashSet<Variable>,
/// Internal equalities we were not able to solve yet.
/// Internal equality constraints that are not identities from the constraint set.
assignments: Vec<Assignment<'a, T>>,
code: Vec<Effect<T, Variable>>,
}
Expand Down Expand Up @@ -283,24 +283,20 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
fn process_assignments(&mut self) {
loop {
let mut progress = false;
let new_assignments = std::mem::take(&mut self.assignments)
.into_iter()
.flat_map(|assignment| {
let rhs = match &assignment.rhs {
VariableOrValue::Variable(v) => {
Evaluator::new(self).evaluate_variable(v.clone())
}
VariableOrValue::Value(v) => (*v).into(),
};
let r =
self.process_equality_on_row(assignment.lhs, assignment.row_offset, rhs);
let summary = self.ingest_effects(r);
progress |= summary.progress;
// If it is not complete, queue it again.
(!summary.complete).then_some(assignment)
})
.collect_vec();
self.assignments.extend(new_assignments);
// We need to take them out because ingest_effects needs a &mut self.
let assignments = std::mem::take(&mut self.assignments);
for assignment in &assignments {
let rhs = match &assignment.rhs {
VariableOrValue::Variable(v) => {
Evaluator::new(self).evaluate_variable(v.clone())
}
VariableOrValue::Value(v) => (*v).into(),
};
let r = self.process_equality_on_row(assignment.lhs, assignment.row_offset, rhs);
progress |= self.ingest_effects(r).progress;
}
assert!(self.assignments.is_empty());
self.assignments = assignments;
if !progress {
break;
}
Expand Down

0 comments on commit 5a47b6e

Please sign in to comment.