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

Some refactoring of AlgebraicConstraint. (#3242)

Browse Source 
Co-authored-by: Thibaut Schaeffer <schaeffer.thibaut@gmail.com>
This commit is contained in:
chriseth
2025-09-03 11:37:12 +02:00
committed by GitHub
parent 6dbb2710e3
commit 38b8406c78
1 changed files with 14 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

29
constraint-solver/src/algebraic_constraint/solve.rs
View File

@@ -41,10 +41,10 @@ pub enum Error {
ConstraintUnsatisfiable(String),
}
impl<
T: RuntimeConstant + Display + ExpressionConvertible<<T as RuntimeConstant>::FieldType, V>,
V: Ord + Clone + Eq + Hash + Display,
> AlgebraicConstraint<&GroupedExpression<T, V>>
impl<T, V> AlgebraicConstraint<&GroupedExpression<T, V>>
where
T: RuntimeConstant + Display + ExpressionConvertible<<T as RuntimeConstant>::FieldType, V>,
V: Ord + Clone + Eq + Hash + Display,
{
/// Solves the equation `self = 0` and returns how to compute the solution.
/// The solution can contain assignments to multiple variables.
@@ -65,19 +65,18 @@ impl<
return Err(Error::ConstraintUnsatisfiable(self.to_string()));
}
Ok(if expression.is_quadratic() {
self.solve_quadratic(range_constraints)?
if expression.is_quadratic() {
self.solve_quadratic(range_constraints)
} else if let Some(k) = expression.try_to_known() {
if k.is_known_nonzero() {
return Err(Error::ConstraintUnsatisfiable(self.to_string()));
} else {
// TODO we could still process more information
// and reach "unsatisfiable" here.
ProcessResult::complete(vec![])
}
// If we know `expression` to be nonzero, we should have returned
// Err already in the range constraint check above.
assert!(!k.is_known_nonzero());
// TODO we could still process more information
// and reach "unsatisfiable" here.
Ok(ProcessResult::complete(vec![]))
} else {
self.solve_affine(range_constraints)?
})
self.solve_affine(range_constraints)
}
}
/// Solves the constraint for `variable`. This is only possible if