mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-01-09 14:48:16 -05:00
Move reachability and use IndexedConstraintSystem (#3248)
This moves the reachability analysis module from the autoprecompiles crate to the constraint solver create. I will need it in that crate in an upcoming PR and it also does not have any autoprecompiles-specific code. I also changed the code to use `IndexedConstraintSystem` instead of `ConstraintSystem`.
This commit is contained in:
@@ -292,9 +292,10 @@ impl<T: RuntimeConstant, V: Clone + Hash + Ord + Eq> IndexedConstraintSystem<T,
|
||||
/// Returns a list of all constraints that contain at least one of the given variables.
|
||||
pub fn constraints_referencing_variables<'a>(
|
||||
&'a self,
|
||||
variables: impl Iterator<Item = V> + 'a,
|
||||
variables: impl IntoIterator<Item = V> + 'a,
|
||||
) -> impl Iterator<Item = ConstraintRef<'a, T, V>> + 'a {
|
||||
variables
|
||||
.into_iter()
|
||||
.filter_map(|v| self.variable_occurrences.get(&v))
|
||||
.flatten()
|
||||
.unique()
|
||||
@@ -709,7 +710,7 @@ mod tests {
|
||||
0
|
||||
);
|
||||
let items_with_x = s
|
||||
.constraints_referencing_variables(["x"].into_iter())
|
||||
.constraints_referencing_variables(["x"])
|
||||
.map(|c| match c {
|
||||
ConstraintRef::AlgebraicConstraint(expr) => expr.to_string(),
|
||||
ConstraintRef::BusInteraction(bus_interaction) => {
|
||||
@@ -726,7 +727,7 @@ mod tests {
|
||||
assert_eq!(items_with_x, "x - z = 0, x: x * [x, x]");
|
||||
|
||||
let items_with_z = s
|
||||
.constraints_referencing_variables(["z"].into_iter())
|
||||
.constraints_referencing_variables(["z"])
|
||||
.map(|c| match c {
|
||||
ConstraintRef::AlgebraicConstraint(expr) => expr.to_string(),
|
||||
ConstraintRef::BusInteraction(bus_interaction) => {
|
||||
|
||||
@@ -7,6 +7,7 @@ pub mod grouped_expression;
|
||||
pub mod indexed_constraint_system;
|
||||
pub mod inliner;
|
||||
pub mod range_constraint;
|
||||
pub mod reachability;
|
||||
pub mod runtime_constant;
|
||||
pub mod solver;
|
||||
pub mod symbolic_expression;
|
||||
|
||||
71
constraint-solver/src/reachability.rs
Normal file
71
constraint-solver/src/reachability.rs
Normal file
@@ -0,0 +1,71 @@
|
||||
use std::collections::HashSet;
|
||||
use std::fmt::Display;
|
||||
use std::hash::Hash;
|
||||
|
||||
use itertools::Itertools;
|
||||
|
||||
use crate::indexed_constraint_system::IndexedConstraintSystem;
|
||||
use crate::runtime_constant::{ReferencedSymbols, RuntimeConstant};
|
||||
|
||||
/// Returns the set of all variables reachable from an initial set via shared constraints
|
||||
/// (algebraic constraints and bus interactions).
|
||||
/// The returned set also contains the initial variables.
|
||||
pub fn reachable_variables<T, V>(
|
||||
initial_variables: impl IntoIterator<Item = V>,
|
||||
constraint_system: &IndexedConstraintSystem<T, V>,
|
||||
) -> HashSet<V>
|
||||
where
|
||||
T: RuntimeConstant + ReferencedSymbols<V>,
|
||||
V: Clone + Ord + Hash + Display,
|
||||
{
|
||||
reachable_variables_except_blocked(initial_variables, std::iter::empty(), constraint_system)
|
||||
}
|
||||
|
||||
/// Returns the set of all variables reachable from an initial set via shared constraints
|
||||
/// (algebraic constraints and bus interactions).
|
||||
/// The set of blocking variables is a barrier that stops the reachability search.
|
||||
/// The returned set does not contain the blocking variables but it does contain
|
||||
/// the initial variables.
|
||||
pub fn reachable_variables_except_blocked<T, V>(
|
||||
initial_variables: impl IntoIterator<Item = V>,
|
||||
blocking_variables: impl IntoIterator<Item = V>,
|
||||
constraint_system: &IndexedConstraintSystem<T, V>,
|
||||
) -> HashSet<V>
|
||||
where
|
||||
T: RuntimeConstant + ReferencedSymbols<V>,
|
||||
V: Clone + Ord + Hash + Display,
|
||||
{
|
||||
let mut reachable_variables = initial_variables.into_iter().collect::<HashSet<_>>();
|
||||
let blocking_variables = blocking_variables.into_iter().collect::<HashSet<_>>();
|
||||
// We just remove variables, order does not matter.
|
||||
#[allow(clippy::iter_over_hash_type)]
|
||||
for v in &blocking_variables {
|
||||
reachable_variables.remove(v);
|
||||
}
|
||||
|
||||
loop {
|
||||
let size_before = reachable_variables.len();
|
||||
let reachable_variables_vec = reachable_variables.iter().cloned().collect_vec();
|
||||
for constraint in
|
||||
constraint_system.constraints_referencing_variables(reachable_variables_vec)
|
||||
{
|
||||
if constraint
|
||||
.referenced_variables()
|
||||
.any(|var| reachable_variables.contains(var))
|
||||
{
|
||||
// This constraint is connected to a reachable variable.
|
||||
// Add all variables of this constraint except the blocking ones.
|
||||
reachable_variables.extend(
|
||||
constraint
|
||||
.referenced_variables()
|
||||
.filter(|&var| !blocking_variables.contains(var))
|
||||
.cloned(),
|
||||
);
|
||||
}
|
||||
}
|
||||
if reachable_variables.len() == size_before {
|
||||
break;
|
||||
}
|
||||
}
|
||||
reachable_variables
|
||||
}
|
||||
Reference in New Issue
Block a user