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

Allow to mutate state. (#2757)

Browse Source 
This changes the solver such that all information that is passed to the
outside at the end is stored in assignments. This adds the flexibility
to perform transformations to the constraint system that might not be
easily reversible or might make the system more complicated.

Depends on #2756
This commit is contained in:
chriseth
2025-05-23 17:01:11 +02:00
committed by GitHub
parent 9084ac4fc3
commit 12c7dbe6ab
6 changed files with 45 additions and 32 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
autoprecompiles/src/optimizer.rs
View File

@@ -4,6 +4,7 @@ use itertools::Itertools;
use powdr_ast::analyzed::{AlgebraicReference, PolyID, PolynomialType};
use powdr_constraint_solver::{
constraint_system::{BusInteraction, BusInteractionHandler, ConstraintSystem},
indexed_constraint_system::apply_substitutions,
quadratic_symbolic_expression::QuadraticSymbolicExpression,
solver::Solver,
symbolic_expression::SymbolicExpression,
@@ -91,7 +92,7 @@ fn solver_based_optimization<T: FieldElement>(
constraint_system: ConstraintSystem<T, Variable>,
bus_interaction_handler: impl BusInteractionHandler<T> + 'static,
) -> ConstraintSystem<T, Variable> {
let result = Solver::new(constraint_system)
let result = Solver::new(constraint_system.clone())
.with_bus_interaction_handler(Box::new(bus_interaction_handler))
.solve()
.map_err(|e| {
@@ -102,7 +103,7 @@ fn solver_based_optimization<T: FieldElement>(
for (var, value) in result.assignments.iter() {
log::trace!(" {var} = {value}");
}
result.simplified_constraint_system
apply_substitutions(constraint_system, result.assignments)
}
/// Removes any columns that are not connected to *stateful* bus interactions (e.g. memory),

1
constraint-solver/src/constraint_system.rs
View File

@@ -8,6 +8,7 @@ use powdr_number::FieldElement;
use std::hash::Hash;
/// Description of a constraint system.
#[derive(Clone)]
pub struct ConstraintSystem<T: FieldElement, V> {
/// The algebraic expressions which have to evaluate to zero.
pub algebraic_constraints: Vec<QuadraticSymbolicExpression<T, V>>,

12
constraint-solver/src/indexed_constraint_system.rs
View File

@@ -9,6 +9,18 @@ use crate::{
symbolic_expression::SymbolicExpression,
};
/// Applies multiple substitutions to a ConstraintSystem in an efficient manner.
pub fn apply_substitutions<T: FieldElement, V: Hash + Eq + Clone + Ord>(
constraint_system: ConstraintSystem<T, V>,
substitutions: impl IntoIterator<Item = (V, QuadraticSymbolicExpression<T, V>)>,
) -> ConstraintSystem<T, V> {
let mut indexed_constraint_system = IndexedConstraintSystem::from(constraint_system);
for (variable, substitution) in substitutions {
indexed_constraint_system.substitute_by_unknown(&variable, &substitution);
}
indexed_constraint_system.into()
}
/// Structure on top of a [`ConstraintSystem`] that stores indices
/// to more efficiently update the constraints.
pub struct IndexedConstraintSystem<T: FieldElement, V> {

39
constraint-solver/src/solver.rs
View File

@@ -22,10 +22,9 @@ mod quadratic_equivalences;
/// The result of the solving process.
pub struct SolveResult<T: FieldElement, V> {
/// The concrete variable assignments that were derived.
pub assignments: BTreeMap<V, QuadraticSymbolicExpression<T, V>>,
/// The final state of the constraint system, with known variables
/// replaced by their values and constraints simplified accordingly.
pub simplified_constraint_system: ConstraintSystem<T, V>,
/// Values might contain variables that are replaced as well,
/// and because of that, assignments should be applied in order.
pub assignments: Vec<(V, QuadraticSymbolicExpression<T, V>)>,
}
/// An error occurred while solving the constraint system.
@@ -52,7 +51,7 @@ pub struct Solver<T: FieldElement, V> {
range_constraints: RangeConstraints<T, V>,
/// The concrete variable assignments or replacements that were derived for variables
/// that do not occur in the constraints any more.
assignments: BTreeMap<V, QuadraticSymbolicExpression<T, V>>,
assignments: Vec<(V, QuadraticSymbolicExpression<T, V>)>,
}
impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display + Debug> Solver<T, V> {
@@ -66,7 +65,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display + Debug> Solver<T, V>
constraint_system: IndexedConstraintSystem::from(constraint_system),
range_constraints: Default::default(),
bus_interaction_handler: Box::new(DefaultBusInteractionHandler::default()),
assignments: BTreeMap::new(),
assignments: Default::default(),
}
}
@@ -87,7 +86,6 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display + Debug> Solver<T, V>
Ok(SolveResult {
assignments: self.assignments,
simplified_constraint_system: self.constraint_system.into(),
})
}
@@ -157,8 +155,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display + Debug> Solver<T, V>
&self.range_constraints,
);
for (x, y) in &equivalences {
// TODO can we make this work with Effects?
self.constraint_system.substitute_by_unknown(
self.apply_assignment(
y,
&QuadraticSymbolicExpression::from_unknown_variable(x.clone()),
);
@@ -174,7 +171,8 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display + Debug> Solver<T, V>
let mut progress = false;
for (variable, value) in &assignments {
progress |= self.apply_assignment(variable, &(*value).into());
progress |=
self.apply_range_constraint_update(variable, RangeConstraint::from_value(*value));
}
Ok(progress)
@@ -182,7 +180,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display + Debug> Solver<T, V>
fn apply_effect(&mut self, effect: Effect<T, V>) -> bool {
match effect {
Effect::Assignment(v, expr) => self.apply_assignment(&v, &expr),
Effect::Assignment(v, expr) => self.apply_assignment(&v, &expr.into()),
Effect::RangeConstraint(v, range_constraint) => {
self.apply_range_constraint_update(&v, range_constraint)
}
@@ -194,11 +192,6 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display + Debug> Solver<T, V>
}
}
fn apply_assignment(&mut self, variable: &V, expr: &SymbolicExpression<T, V>) -> bool {
assert!(expr.try_to_number().is_some());
self.apply_range_constraint_update(variable, expr.range_constraint())
}
fn apply_range_constraint_update(
&mut self,
variable: &V,
@@ -207,10 +200,7 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display + Debug> Solver<T, V>
if self.range_constraints.update(variable, &range_constraint) {
let new_rc = self.range_constraints.get(variable);
if let Some(value) = new_rc.try_to_single_value() {
log::debug!("({variable} := {value})");
self.constraint_system
.substitute_by_known(variable, &value.into());
self.assignments.insert(variable.clone(), value.into());
self.apply_assignment(variable, &value.into());
} else {
// The range constraint was updated.
log::trace!("({variable}: {range_constraint})");
@@ -221,6 +211,15 @@ impl<T: FieldElement, V: Ord + Clone + Hash + Eq + Display + Debug> Solver<T, V>
}
}
fn apply_assignment(&mut self, variable: &V, expr: &QuadraticSymbolicExpression<T, V>) -> bool {
log::debug!("({variable} := {expr})");
self.constraint_system.substitute_by_unknown(variable, expr);
self.assignments.push((variable.clone(), expr.clone()));
// TODO we could check if the variable already has an assignment,
// but usually it should not be in the system once it has been assigned.
true
}
/// Given a set of variable assignments, checks if they violate any constraint.
/// Note that this might return false negatives, because it does not propagate any values.
fn is_assignment_conflicting(&self, assignments: &BTreeMap<V, T>) -> bool {

9
constraint-solver/tests/solver.rs
View File

@@ -4,6 +4,7 @@ use itertools::Itertools;
use num_traits::identities::{One, Zero};
use powdr_constraint_solver::{
constraint_system::{BusInteraction, BusInteractionHandler, ConstraintSystem},
indexed_constraint_system::apply_substitutions,
quadratic_symbolic_expression::QuadraticSymbolicExpression,
range_constraint::RangeConstraint,
solver::{Error, Solver},
@@ -26,9 +27,10 @@ pub fn assert_solve_result(
}
fn assert_expected_state(
final_state: BTreeMap<Var, QuadraticSymbolicExpression<GoldilocksField, Var>>,
final_state: impl IntoIterator<Item = (Var, QuadraticSymbolicExpression<GoldilocksField, Var>)>,
expected_final_state: BTreeMap<Var, GoldilocksField>,
) {
let final_state = final_state.into_iter().collect::<BTreeMap<_, _>>();
assert_eq!(
final_state.keys().collect::<Vec<_>>(),
expected_final_state.keys().collect::<Vec<_>>(),
@@ -276,11 +278,10 @@ fn add_with_carry() {
],
};
let solver = Solver::new(constraint_system)
let solver = Solver::new(constraint_system.clone())
.with_bus_interaction_handler(Box::new(TestBusInteractionHandler {}));
let final_state = solver.solve().unwrap();
let final_state = final_state
.simplified_constraint_system
let final_state = apply_substitutions(constraint_system, final_state.assignments)
.algebraic_constraints
.iter()
.format("\n")

11
pilopt/src/qse_opt.rs
View File

@@ -8,6 +8,7 @@ use powdr_ast::analyzed::{
Analyzed, Challenge, Identity, PolynomialIdentity,
};
use powdr_constraint_solver::constraint_system::ConstraintSystem;
use powdr_constraint_solver::indexed_constraint_system::apply_substitutions;
use powdr_constraint_solver::{
quadratic_symbolic_expression::QuadraticSymbolicExpression,
solver::{self, SolveResult},
@@ -48,14 +49,12 @@ pub fn run_qse_optimization<T: FieldElement>(pil_file: &mut Analyzed<T>) {
//replace_constrained_witness_columns(&mut constraint_system, 3);
match solver::Solver::new(constraint_system).solve() {
match solver::Solver::new(constraint_system.clone()).solve() {
Err(_) => {
log::error!("Error while QSE-optimizing. This is usually the case when the constraints are inconsistent.");
}
Ok(SolveResult {
simplified_constraint_system,
assignments,
}) => {
Ok(SolveResult { assignments }) => {
let constraint_system = apply_substitutions(constraint_system, assignments.clone());
pil_file
.identities
.iter_mut()
@@ -66,7 +65,7 @@ pub fn run_qse_optimization<T: FieldElement>(pil_file: &mut Analyzed<T>) {
None
}
})
.zip_eq(simplified_constraint_system.algebraic_constraints)
.zip_eq(constraint_system.algebraic_constraints)
.for_each(|(identity, simplified)| {
// We can ignore the negation because it is a polynomial identity
// that is equated to zero.