github/powdr
1
1
Fork 0
mirror of https://github.com/powdr-labs/powdr.git synced 2026-01-09 14:48:16 -05:00
Code Issues Packages Projects Releases Wiki Activity

Document is_simple_equivalence. (#3224)

Browse Source
This commit is contained in:
chriseth
2025-08-26 16:14:44 +02:00
committed by GitHub
parent 349c742fcc
commit e65df60cfe
1 changed files with 15 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

21
constraint-solver/src/solver/base.rs
View File

@@ -365,7 +365,7 @@ where
while let Some(item) = self.constraint_system.pop_front() {
let effects = match item {
ConstraintRef::AlgebraicConstraint(c) => {
if let Some((v1, expr)) = is_simple_equivalence(c) {
if let Some((v1, expr)) = try_to_simple_equivalence(c) {
self.apply_assignment(&v1, &expr);
continue;
}
@@ -562,15 +562,24 @@ where
}
}
fn is_simple_equivalence<T: RuntimeConstant, V: Clone + Ord + Eq>(
expr: &GroupedExpression<T, V>,
/// If the constraint is equivalent to `X = Y` for some variables `X` and `Y`,
/// returns the "larger" variable and the result of solving the constraint
/// for the variable.
///
/// Note: Does not find all cases of equivalence.
fn try_to_simple_equivalence<T: RuntimeConstant, V: Clone + Ord + Eq>(
constr: &AlgebraicConstraint<GroupedExpression<T, V>>,
) -> Option<(V, GroupedExpression<T, V>)> {
if !expr.is_affine() {
if !constr.expression.is_affine() {
return None;
}
let (_, linear, offset) = constr.expression.components();
if !offset.is_zero() {
return None;
}
let (_, linear, offset) = expr.components();
let [(v1, c1), (v2, c2)] = linear.collect_vec().try_into().ok()?;
if offset.is_zero() && (c1.is_one() || c2.is_one()) && (c1.clone() + c2.clone()).is_zero() {
// c1 = 1, c2 = -1 or vice-versa
if (c1.is_one() || c2.is_one()) && (c1.clone() + c2.clone()).is_zero() {
Some((
v2.clone(),
GroupedExpression::from_unknown_variable(v1.clone()),