mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-01-09 14:48:16 -05:00
Also return determined range constraints. (#3068)
Sometimes we want to run an optimization that depends on range constraints. Using the solver is the best way to determine range constraints, so it should also return them.
This commit is contained in:
@@ -29,7 +29,7 @@ pub fn solve_system<T, V>(
|
||||
) -> Result<SolveResult<T, V>, Error>
|
||||
where
|
||||
T: RuntimeConstant + VarTransformable<V, Variable<V>> + Display,
|
||||
T::Transformed: RuntimeConstant
|
||||
T::Transformed: RuntimeConstant<FieldType = T::FieldType>
|
||||
+ VarTransformable<Variable<V>, V, Transformed = T>
|
||||
+ ReferencedSymbols<Variable<V>>
|
||||
+ Substitutable<Variable<V>>
|
||||
@@ -43,7 +43,7 @@ where
|
||||
let result = Solver::new(constraint_system)
|
||||
.with_bus_interaction_handler(bus_interaction_handler)
|
||||
.solve()?;
|
||||
Ok(bus_interaction_variable_wrapper.finalize(result.assignments))
|
||||
Ok(bus_interaction_variable_wrapper.finalize(result))
|
||||
}
|
||||
|
||||
/// The result of the solving process.
|
||||
@@ -52,6 +52,9 @@ pub struct SolveResult<T: RuntimeConstant, V> {
|
||||
/// Values might contain variables that are replaced as well,
|
||||
/// and because of that, assignments should be applied in order.
|
||||
pub assignments: Vec<VariableAssignment<T, V>>,
|
||||
/// The range constraints the solver was able to determine
|
||||
/// for the variables.
|
||||
pub range_constraints: RangeConstraints<T::FieldType, V>,
|
||||
/// Maps a (bus interaction index, field index) to a concrete value.
|
||||
pub bus_field_assignments: BTreeMap<(usize, usize), T::FieldType>,
|
||||
}
|
||||
@@ -73,7 +76,7 @@ pub enum Error {
|
||||
pub type VariableAssignment<T, V> = (V, GroupedExpression<T, V>);
|
||||
|
||||
/// Given a list of constraints, tries to derive as many variable assignments as possible.
|
||||
struct Solver<T: RuntimeConstant, V: Clone + Eq, BusInterHandler> {
|
||||
pub struct Solver<T: RuntimeConstant, V: Clone + Eq, BusInterHandler> {
|
||||
/// The constraint system to solve. During the solving process, any expressions will
|
||||
/// be simplified as much as possible.
|
||||
constraint_system: IndexedConstraintSystem<T, V>,
|
||||
@@ -127,11 +130,12 @@ where
|
||||
}
|
||||
|
||||
/// Solves the constraints as far as possible, returning concrete variable
|
||||
/// assignments and a simplified version of the algebraic constraints.
|
||||
/// assignments and determined range constraints.
|
||||
pub fn solve(mut self) -> Result<SolveResult<T, V>, Error> {
|
||||
self.loop_until_no_progress()?;
|
||||
Ok(SolveResult {
|
||||
assignments: self.assignments,
|
||||
range_constraints: self.range_constraints,
|
||||
bus_field_assignments: Default::default(),
|
||||
})
|
||||
}
|
||||
@@ -280,8 +284,8 @@ impl<T: RuntimeConstant, V: Clone + Hash + Eq, B> RangeConstraintProvider<T::Fie
|
||||
}
|
||||
|
||||
/// The currently known range constraints for the variables.
|
||||
struct RangeConstraints<T: FieldElement, V> {
|
||||
range_constraints: HashMap<V, RangeConstraint<T>>,
|
||||
pub struct RangeConstraints<T: FieldElement, V> {
|
||||
pub range_constraints: HashMap<V, RangeConstraint<T>>,
|
||||
}
|
||||
|
||||
// Manual implementation so that we don't have to require `V: Default`.
|
||||
|
||||
@@ -7,7 +7,7 @@ use crate::{
|
||||
constraint_system::{BusInteraction, ConstraintSystem},
|
||||
grouped_expression::GroupedExpression,
|
||||
runtime_constant::{RuntimeConstant, Substitutable, VarTransformable},
|
||||
solver::{SolveResult, VariableAssignment},
|
||||
solver::{RangeConstraints, SolveResult},
|
||||
};
|
||||
|
||||
/// A wrapped variable: Either a regular variable or a bus interaction field.
|
||||
@@ -35,7 +35,7 @@ pub struct BusInteractionVariableWrapper<T, V> {
|
||||
impl<T, V: Ord + Clone + Hash + Eq + Display> BusInteractionVariableWrapper<T, V>
|
||||
where
|
||||
T: RuntimeConstant + VarTransformable<V, Variable<V>> + Display,
|
||||
T::Transformed: RuntimeConstant
|
||||
T::Transformed: RuntimeConstant<FieldType = T::FieldType>
|
||||
+ VarTransformable<Variable<V>, V, Transformed = T>
|
||||
+ Substitutable<Variable<V>>,
|
||||
{
|
||||
@@ -82,9 +82,9 @@ where
|
||||
|
||||
pub fn finalize(
|
||||
mut self,
|
||||
assignments: Vec<VariableAssignment<T::Transformed, Variable<V>>>,
|
||||
solve_result: SolveResult<T::Transformed, Variable<V>>,
|
||||
) -> SolveResult<T, V> {
|
||||
for (variable, expr) in &assignments {
|
||||
for (variable, expr) in &solve_result.assignments {
|
||||
// Apply any assignments to the bus interaction field definitions.
|
||||
if let Variable::BusInteractionField(..) = variable {
|
||||
// Non-concrete assignments are only generated by the `quadratic_equivalences` module,
|
||||
@@ -105,7 +105,8 @@ where
|
||||
}
|
||||
|
||||
// Unwrap assignments. Note that this uses the updated bus interaction field definitions.
|
||||
let assignments = assignments
|
||||
let assignments = solve_result
|
||||
.assignments
|
||||
.into_iter()
|
||||
.filter_map(|(v, expr)| match v {
|
||||
Variable::Variable(v) => {
|
||||
@@ -127,8 +128,23 @@ where
|
||||
})
|
||||
.collect();
|
||||
|
||||
let range_constraints = solve_result
|
||||
.range_constraints
|
||||
.range_constraints
|
||||
.into_iter()
|
||||
.fold(
|
||||
RangeConstraints::<T::FieldType, V>::default(),
|
||||
|mut range_constraints, (v, rc)| {
|
||||
if let Variable::Variable(v) = v {
|
||||
range_constraints.update(&v, &rc);
|
||||
}
|
||||
range_constraints
|
||||
},
|
||||
);
|
||||
|
||||
SolveResult {
|
||||
assignments,
|
||||
range_constraints,
|
||||
bus_field_assignments,
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user