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

Introduce AlgebraicConstraint type in solver (#3215)

Browse Source 
I got confused before about what is an expression and what is a
constraint.
For example, in boolean extraction, we return an expression which I
thought was the boolean. But it turns out the expression is the new
constraint.

Similarly, there are some things that we can do for constraints which
wouldn't work for expression: for example, `2 * x == 0` can be replaced
by `x == 0`. But `2 * x` as an expression cannot be replaced by `x`.

This PR introduces a wrapper and uses it where possible.

Some caveats:
- This PR implements `Deref` and `DerefMut` for the constraint, which
means that we can call any function which takes a reference to an
expression by passing a constraint. This partially defeats the purpose
of the change, as we can by mistake call a function which would only be
meant for expressions. This is fixed in #3220
- This PR keeps the `solve` functions as before, where they run on
expressions, not constraints. This does not make sense in my opinion, as
solving should be for constraints only, however here's an example which
would break if we made this change: if we are solving the constraint `a
* b = 0` we want to solve the constraint `a = 0`. This would require
creating a constraint out of `a` on the fly, which is not implemented in
this PR. This is fixed in #3220
This commit is contained in:
Thibaut Schaeffer
2025-08-25 21:08:44 +02:00
committed by GitHub
parent 8700b12716
commit 3cc2de7e0d
18 changed files with 491 additions and 354 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
autoprecompiles/src/constraint_optimizer.rs
View File

@@ -8,7 +8,9 @@ use std::{
use itertools::Itertools;
use num_traits::Zero;
use powdr_constraint_solver::{
constraint_system::{BusInteractionHandler, ConstraintRef, ConstraintSystem},
constraint_system::{
AlgebraicConstraint, BusInteractionHandler, ConstraintRef, ConstraintSystem,
},
grouped_expression::GroupedExpression,
journaling_constraint_system::JournalingConstraintSystem,
solver::Solver,
@@ -114,7 +116,8 @@ fn solver_based_optimization<T: FieldElement, V: Clone + Ord + Hash + Display>(
.map(|field| {
if let Some(n) = try_replace_by_number(field, solver) {
modified = true;
new_algebraic_constraints.push(&n - field);
new_algebraic_constraints
.push(AlgebraicConstraint::assert_eq(n.clone(), field.clone()));
n
} else {
field.clone()
@@ -296,10 +299,9 @@ fn variables_in_stateful_bus_interactions<'a, P: FieldElement, V: Ord + Clone +
fn remove_trivial_constraints<P: FieldElement, V: PartialEq + Clone + Hash + Ord>(
mut constraint_system: JournalingConstraintSystem<P, V>,
) -> JournalingConstraintSystem<P, V> {
let zero = GroupedExpression::zero();
constraint_system.retain_algebraic_constraints(|constraint| constraint != &zero);
constraint_system.retain_algebraic_constraints(|constraint| !constraint.is_redundant());
constraint_system
.retain_bus_interactions(|bus_interaction| bus_interaction.multiplicity != zero);
.retain_bus_interactions(|bus_interaction| !bus_interaction.multiplicity.is_zero());
constraint_system
}
@@ -395,12 +397,12 @@ fn remove_duplicate_factors<P: FieldElement, V: Clone + Ord + Hash + Display>(
let factor_count = factors.len();
let unique_factors = factors.into_iter().unique().collect_vec();
if unique_factors.len() < factor_count {
constraint_to_add.push(
constraint_to_add.push(AlgebraicConstraint::assert_zero(
unique_factors
.into_iter()
.reduce(|acc, factor| acc * factor)
.unwrap(),
);
));
false
} else {
true

38
autoprecompiles/src/low_degree_bus_interaction_optimizer.rs
View File

@@ -1,7 +1,7 @@
use itertools::Itertools;
use num_traits::Zero;
use powdr_constraint_solver::constraint_system::{
BusInteraction, BusInteractionHandler, ConstraintSystem,
AlgebraicConstraint, BusInteraction, BusInteractionHandler, ConstraintSystem,
};
use powdr_constraint_solver::grouped_expression::GroupedExpression;
use powdr_constraint_solver::inliner::DegreeBound;
@@ -26,6 +26,11 @@ pub struct LowDegreeBusInteractionOptimizer<'a, T, V, S, B> {
_phantom: PhantomData<(T, V)>,
}
struct LowDegreeReplacement<T: FieldElement, V> {
constraint: AlgebraicConstraint<GroupedExpression<T, V>>,
range_constraints: RangeConstraints<T, V>,
}
impl<
'a,
T: FieldElement,
@@ -44,13 +49,15 @@ impl<
}
pub fn optimize(self, mut system: ConstraintSystem<T, V>) -> ConstraintSystem<T, V> {
let mut new_constraints: Vec<GroupedExpression<T, V>> = vec![];
let mut new_constraints = vec![];
system.bus_interactions = system
.bus_interactions
.into_iter()
.flat_map(|bus_int| {
if let Some((replacement, range_constraints)) =
self.try_replace_bus_interaction(&bus_int)
if let Some(LowDegreeReplacement {
constraint: replacement,
range_constraints,
}) = self.try_replace_bus_interaction(&bus_int)
{
// If we found a replacement, add the polynomial constraints (unless it is
// trivially zero) and replace the bus interaction with interactions implementing
@@ -92,7 +99,7 @@ impl<
fn try_replace_bus_interaction(
&self,
bus_interaction: &BusInteraction<GroupedExpression<T, V>>,
) -> Option<(GroupedExpression<T, V>, RangeConstraints<T, V>)> {
) -> Option<LowDegreeReplacement<T, V>> {
let bus_id = bus_interaction.bus_id.try_to_number()?;
if self.bus_interaction_handler.is_stateful(bus_id) {
return None;
@@ -112,8 +119,10 @@ impl<
.map(|input| input.expression)
.collect();
let low_degree_function = low_degree_function(symbolic_inputs);
let polynomial_constraint =
symbolic_function.output.expression.clone() - low_degree_function;
let polynomial_constraint = AlgebraicConstraint::assert_eq(
symbolic_function.output.expression,
low_degree_function,
);
// Check degree
let within_degree_bound =
@@ -124,7 +133,10 @@ impl<
.into_iter()
.map(|field| (field.expression, field.range_constraint))
.collect();
Some((polynomial_constraint, range_constraints))
Some(LowDegreeReplacement {
constraint: polynomial_constraint,
range_constraints,
})
} else {
None
}
@@ -439,7 +451,7 @@ mod tests {
fn compute_replacement(
mut solver: impl Solver<BabyBearField, Var>,
bus_interaction: &BusInteraction<GroupedExpression<BabyBearField, Var>>,
) -> Option<GroupedExpression<BabyBearField, Var>> {
) -> Option<AlgebraicConstraint<GroupedExpression<BabyBearField, Var>>> {
let optimizer = LowDegreeBusInteractionOptimizer {
solver: &mut solver,
bus_interaction_handler: XorBusHandler,
@@ -451,7 +463,7 @@ mod tests {
};
optimizer
.try_replace_bus_interaction(bus_interaction)
.map(|(replacement, _)| replacement)
.map(|v| v.constraint)
}
#[test]
@@ -482,7 +494,7 @@ mod tests {
let Some(replacement) = compute_replacement(solver, &bus_interaction) else {
panic!("Expected a replacement")
};
assert_eq!(replacement.to_string(), "x + z - 255");
assert_eq!(replacement.to_string(), "x + z - 255 = 0");
}
#[test]
@@ -499,7 +511,7 @@ mod tests {
let Some(replacement) = compute_replacement(solver, &bus_interaction) else {
panic!("Expected a replacement")
};
assert_eq!(replacement.to_string(), "(2 * x) * (y) - x - y + z");
assert_eq!(replacement.to_string(), "(2 * x) * (y) - x - y + z = 0");
}
#[test]
@@ -516,6 +528,6 @@ mod tests {
let Some(replacement) = compute_replacement(solver, &bus_interaction) else {
panic!("Expected a replacement")
};
assert_eq!(replacement.to_string(), "-(x + y - z)");
assert_eq!(replacement.to_string(), "-(x + y - z) = 0");
}
}

15
autoprecompiles/src/memory_optimizer.rs
View File

@@ -3,7 +3,9 @@ use std::fmt::Display;
use std::hash::Hash;
use itertools::Itertools;
use powdr_constraint_solver::constraint_system::{BusInteraction, ConstraintSystem};
use powdr_constraint_solver::constraint_system::{
AlgebraicConstraint, BusInteraction, ConstraintSystem,
};
use powdr_constraint_solver::grouped_expression::GroupedExpression;
use powdr_constraint_solver::solver::Solver;
use powdr_number::FieldElement;
@@ -135,8 +137,11 @@ fn redundant_memory_interactions_indices<
system: &ConstraintSystem<T, V>,
solver: &mut impl Solver<T, V>,
memory_bus_id: u64,
) -> (Vec<usize>, Vec<GroupedExpression<T, V>>) {
let mut new_constraints: Vec<GroupedExpression<T, V>> = Vec::new();
) -> (
Vec<usize>,
Vec<AlgebraicConstraint<GroupedExpression<T, V>>>,
) {
let mut new_constraints = Vec::new();
// Track memory contents by memory type while we go through bus interactions.
// This maps an address to the index of the previous send on that address and the
@@ -169,7 +174,9 @@ fn redundant_memory_interactions_indices<
// between the data that would have been sent and received.
if let Some((previous_send, existing_values)) = memory_contents.remove(&addr) {
for (existing, new) in existing_values.iter().zip_eq(mem_int.data().iter()) {
new_constraints.push(existing.clone() - new.clone());
new_constraints.push(AlgebraicConstraint::assert_zero(
existing.clone() - new.clone(),
));
}
to_remove.extend([index, previous_send]);
}

6
autoprecompiles/src/optimizer.rs
View File

@@ -3,7 +3,7 @@ use std::hash::Hash;
use std::{collections::BTreeMap, fmt::Display};
use itertools::Itertools;
use powdr_constraint_solver::constraint_system::BusInteractionHandler;
use powdr_constraint_solver::constraint_system::{AlgebraicConstraint, BusInteractionHandler};
use powdr_constraint_solver::inliner::{self, inline_everything_below_degree_bound};
use powdr_constraint_solver::solver::{new_solver, Solver};
use powdr_constraint_solver::{
@@ -242,7 +242,9 @@ fn symbolic_machine_to_constraint_system<P: FieldElement>(
algebraic_constraints: symbolic_machine
.constraints
.iter()
.map(|constraint| algebraic_to_grouped_expression(&constraint.expr))
.map(|constraint| {
AlgebraicConstraint::assert_zero(algebraic_to_grouped_expression(&constraint.expr))
})
.collect(),
bus_interactions: symbolic_machine
.bus_interactions

5
autoprecompiles/src/range_constraint_optimizer.rs
View File

@@ -3,9 +3,8 @@ use std::fmt::Display;
use std::hash::Hash;
use itertools::Itertools;
use num_traits::One;
use powdr_constraint_solver::constraint_system::{
BusInteraction, BusInteractionHandler, ConstraintSystem,
AlgebraicConstraint, BusInteraction, BusInteractionHandler, ConstraintSystem,
};
use powdr_constraint_solver::grouped_expression::GroupedExpression;
use powdr_constraint_solver::inliner::DegreeBound;
@@ -110,7 +109,7 @@ pub fn optimize_range_constraints<T: FieldElement, V: Ord + Clone + Hash + Eq +
let to_constrain = to_constrain
.into_iter()
.filter(|(expr, rc)| {
let bit_range_constraint = expr.clone() * (expr.clone() - GroupedExpression::one());
let bit_range_constraint = AlgebraicConstraint::assert_bool(expr.clone());
if rc == &RangeConstraint::from_mask(1)
&& bit_range_constraint.degree() <= degree_bound.identities
{

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

@@ -5,6 +5,7 @@ use crate::{
runtime_constant::{ReferencedSymbols, RuntimeConstant},
};
use itertools::Itertools;
use num_traits::{One, Zero};
use powdr_number::{ExpressionConvertible, FieldElement};
use std::{fmt::Display, hash::Hash};
@@ -12,7 +13,7 @@ use std::{fmt::Display, hash::Hash};
#[derive(Clone)]
pub struct ConstraintSystem<T, V> {
/// The algebraic expressions which have to evaluate to zero.
pub algebraic_constraints: Vec<GroupedExpression<T, V>>,
pub algebraic_constraints: Vec<AlgebraicConstraint<GroupedExpression<T, V>>>,
/// Bus interactions, which can further restrict variables.
/// Exact semantics are up to the implementation of BusInteractionHandler
pub bus_interactions: Vec<BusInteraction<GroupedExpression<T, V>>>,
@@ -34,7 +35,7 @@ impl<T: RuntimeConstant + Display, V: Clone + Ord + Display> Display for Constra
"{}",
self.algebraic_constraints
.iter()
.map(|expr| format!("{expr} = 0"))
.map(|constraint| format!("{constraint}"))
.chain(
self.bus_interactions
.iter()
@@ -46,7 +47,7 @@ impl<T: RuntimeConstant + Display, V: Clone + Ord + Display> Display for Constra
}
impl<T: RuntimeConstant, V> ConstraintSystem<T, V> {
pub fn iter(&self) -> impl Iterator<Item = ConstraintRef<T, V>> {
pub fn iter(&self) -> impl Iterator<Item = ConstraintRef<'_, T, V>> {
Box::new(
self.algebraic_constraints
.iter()
@@ -63,17 +64,21 @@ impl<T: RuntimeConstant, V> ConstraintSystem<T, V> {
Box::new(
self.algebraic_constraints
.iter()
.map(|c| &c.expression)
.chain(self.bus_interactions.iter().flat_map(|b| b.fields())),
)
}
pub fn expressions_mut(&mut self) -> impl Iterator<Item = &mut GroupedExpression<T, V>> {
Box::new(
self.algebraic_constraints.iter_mut().chain(
self.bus_interactions
.iter_mut()
.flat_map(|b| b.fields_mut()),
),
self.algebraic_constraints
.iter_mut()
.map(|c| &mut c.expression)
.chain(
self.bus_interactions
.iter_mut()
.flat_map(|b| b.fields_mut()),
),
)
}
@@ -86,6 +91,77 @@ impl<T: RuntimeConstant, V> ConstraintSystem<T, V> {
}
}
/// An algebraic constraint
#[derive(Clone, Debug, Hash, Eq, PartialEq)]
pub struct AlgebraicConstraint<V> {
/// The expression representing the constraint, which must evaluate to 0 for the constraint to be satisfied.
pub expression: V,
}
// We implement `From` to make writing tests easier. However, we recommend using `AlgebraicConstraint::assert_zero` for clarity
impl<V> From<V> for AlgebraicConstraint<V> {
fn from(expression: V) -> Self {
AlgebraicConstraint::assert_zero(expression)
}
}
impl<V> AlgebraicConstraint<V> {
/// Create a constraint which asserts that the expression evaluates to 0.
pub fn assert_zero(expression: V) -> Self {
AlgebraicConstraint { expression }
}
}
impl<V> std::ops::Deref for AlgebraicConstraint<V> {
type Target = V;
fn deref(&self) -> &V {
&self.expression
}
}
impl<V> std::ops::DerefMut for AlgebraicConstraint<V> {
fn deref_mut(&mut self) -> &mut V {
&mut self.expression
}
}
impl<T: FieldElement, V: Clone + Ord> AlgebraicConstraint<GroupedExpression<T, V>> {
/// Returns the referenced unknown variables. Might contain repetitions.
pub fn referenced_unknown_variables(&self) -> Box<dyn Iterator<Item = &V> + '_> {
self.expression.referenced_unknown_variables()
}
/// Returns a constraint which asserts that the two expressions are equal.
pub fn assert_eq(expression: GroupedExpression<T, V>, other: GroupedExpression<T, V>) -> Self {
Self::assert_zero(expression - other)
}
/// Returns a constraint which asserts that the expression is a boolean.
pub fn assert_bool(expression: GroupedExpression<T, V>) -> Self {
Self::assert_zero(expression.clone() * (expression - GroupedExpression::one()))
}
}
impl<V: Zero> AlgebraicConstraint<V> {
pub fn is_redundant(&self) -> bool {
self.expression.is_zero()
}
}
impl<V: Display> Display for AlgebraicConstraint<V> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(f, "{} = 0", self.expression)
}
}
impl<T: ReferencedSymbols<V>, V> AlgebraicConstraint<GroupedExpression<T, V>> {
/// Returns the set of referenced variables, both know and unknown.
pub fn referenced_variables(&self) -> Box<dyn Iterator<Item = &V> + '_> {
self.expression.referenced_variables()
}
}
/// A bus interaction.
#[derive(Clone, Debug, Hash, Eq, PartialEq)]
pub struct BusInteraction<V> {
@@ -261,7 +337,7 @@ impl<T: FieldElement> BusInteractionHandler<T> for DefaultBusInteractionHandler<
}
pub enum ConstraintRef<'a, T, V> {
AlgebraicConstraint(&'a GroupedExpression<T, V>),
AlgebraicConstraint(&'a AlgebraicConstraint<GroupedExpression<T, V>>),
BusInteraction(&'a BusInteraction<GroupedExpression<T, V>>),
}

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

@@ -9,7 +9,7 @@ use bitvec::vec::BitVec;
use itertools::Itertools;
use crate::{
constraint_system::{BusInteraction, ConstraintRef, ConstraintSystem},
constraint_system::{AlgebraicConstraint, BusInteraction, ConstraintRef, ConstraintSystem},
grouped_expression::GroupedExpression,
runtime_constant::{RuntimeConstant, Substitutable},
};
@@ -36,12 +36,18 @@ pub fn apply_substitutions_to_expressions<
) -> Vec<GroupedExpression<T, V>> {
apply_substitutions(
ConstraintSystem {
algebraic_constraints: expressions.into_iter().collect(),
algebraic_constraints: expressions
.into_iter()
.map(AlgebraicConstraint::assert_zero)
.collect(),
bus_interactions: Vec::new(),
},
substitutions,
)
.algebraic_constraints
.into_iter()
.map(|constraint| constraint.expression)
.collect()
}
/// Structure on top of a [`ConstraintSystem`] that stores indices
@@ -143,7 +149,7 @@ impl<T: RuntimeConstant, V: Clone + Eq> IndexedConstraintSystem<T, V> {
&self.constraint_system
}
pub fn algebraic_constraints(&self) -> &[GroupedExpression<T, V>] {
pub fn algebraic_constraints(&self) -> &[AlgebraicConstraint<GroupedExpression<T, V>>] {
&self.constraint_system.algebraic_constraints
}
@@ -164,7 +170,7 @@ impl<T: RuntimeConstant, V: Clone + Eq> IndexedConstraintSystem<T, V> {
/// Removes all constraints that do not fulfill the predicate.
pub fn retain_algebraic_constraints(
&mut self,
mut f: impl FnMut(&GroupedExpression<T, V>) -> bool,
mut f: impl FnMut(&AlgebraicConstraint<GroupedExpression<T, V>>) -> bool,
) {
retain(
&mut self.constraint_system.algebraic_constraints,
@@ -239,7 +245,7 @@ impl<T: RuntimeConstant, V: Clone + Eq + Hash> IndexedConstraintSystem<T, V> {
/// Adds new algebraic constraints to the system.
pub fn add_algebraic_constraints(
&mut self,
constraints: impl IntoIterator<Item = GroupedExpression<T, V>>,
constraints: impl IntoIterator<Item = AlgebraicConstraint<GroupedExpression<T, V>>>,
) {
self.extend(ConstraintSystem {
algebraic_constraints: constraints.into_iter().collect(),
@@ -386,7 +392,9 @@ fn substitute_by_known_in_item<T: RuntimeConstant + Substitutable<V>, V: Ord + C
) {
match item {
ConstraintSystemItem::AlgebraicConstraint(i) => {
constraint_system.algebraic_constraints[i].substitute_by_known(variable, substitution);
constraint_system.algebraic_constraints[i]
.expression
.substitute_by_known(variable, substitution);
}
ConstraintSystemItem::BusInteraction(i) => {
constraint_system.bus_interactions[i]
@@ -405,6 +413,7 @@ fn substitute_by_unknown_in_item<T: RuntimeConstant + Substitutable<V>, V: Ord +
match item {
ConstraintSystemItem::AlgebraicConstraint(i) => {
constraint_system.algebraic_constraints[i]
.expression
.substitute_by_unknown(variable, substitution);
}
ConstraintSystemItem::BusInteraction(i) => {
@@ -478,7 +487,7 @@ where
pub fn add_algebraic_constraints(
&mut self,
constraints: impl IntoIterator<Item = GroupedExpression<T, V>>,
constraints: impl IntoIterator<Item = AlgebraicConstraint<GroupedExpression<T, V>>>,
) {
let initial_len = self
.constraint_system
@@ -512,7 +521,7 @@ where
pub fn retain_algebraic_constraints(
&mut self,
mut f: impl FnMut(&GroupedExpression<T, V>) -> bool,
mut f: impl FnMut(&AlgebraicConstraint<GroupedExpression<T, V>>) -> bool,
) {
self.constraint_system.retain_algebraic_constraints(&mut f);
if !self.queue.queue.is_empty() {
@@ -622,23 +631,25 @@ mod tests {
let x = Ge::from_unknown_variable("x");
let y = Ge::from_unknown_variable("y");
let z = Ge::from_unknown_variable("z");
let mut s: IndexedConstraintSystem<_, _> = ConstraintSystem {
algebraic_constraints: vec![
let mut s: IndexedConstraintSystem<_, _> = ConstraintSystem::default()
.with_constraints(vec![
x.clone() + y.clone(),
x.clone() - z.clone(),
y.clone() - z.clone(),
],
bus_interactions: vec![BusInteraction {
])
.with_bus_interactions(vec![BusInteraction {
bus_id: x,
payload: vec![y.clone(), z],
multiplicity: y,
}],
}
.into();
}])
.into();
s.substitute_by_unknown(&"x", &Ge::from_unknown_variable("z"));
assert_eq!(format_system(&s), "y + z | 0 | y - z | z: y * [y, z]");
assert_eq!(
format_system(&s),
"y + z = 0 | 0 = 0 | y - z = 0 | z: y * [y, z]"
);
s.substitute_by_unknown(
&"z",
@@ -647,7 +658,7 @@ mod tests {
assert_eq!(
format_system(&s),
"x + y + 7 | 0 | -(x - y + 7) | x + 7: y * [y, x + 7]"
"x + y + 7 = 0 | 0 = 0 | -(x - y + 7) = 0 | x + 7: y * [y, x + 7]"
);
}
@@ -657,13 +668,13 @@ mod tests {
let x = Ge::from_unknown_variable("x");
let y = Ge::from_unknown_variable("y");
let z = Ge::from_unknown_variable("z");
let mut s: IndexedConstraintSystem<_, _> = ConstraintSystem {
algebraic_constraints: vec![
let mut s: IndexedConstraintSystem<_, _> = ConstraintSystem::default()
.with_constraints(vec![
x.clone() + y.clone(),
x.clone() - z.clone(),
y.clone() - z.clone(),
],
bus_interactions: vec![
])
.with_bus_interactions(vec![
BusInteraction {
bus_id: x.clone(),
payload: vec![y.clone(), z],
@@ -674,9 +685,8 @@ mod tests {
payload: vec![x.clone(), x.clone()],
multiplicity: x,
},
],
}
.into();
])
.into();
s.retain_algebraic_constraints(|c| !c.referenced_unknown_variables().any(|v| *v == "y"));
s.retain_bus_interactions(|b| {
@@ -704,7 +714,7 @@ mod tests {
})
.format(", ")
.to_string();
assert_eq!(items_with_x, "x - z, x: x * [x, x]");
assert_eq!(items_with_x, "x - z = 0, x: x * [x, x]");
let items_with_z = s
.constraints_referencing_variables(["z"].into_iter())
@@ -721,6 +731,6 @@ mod tests {
})
.format(", ")
.to_string();
assert_eq!(items_with_z, "x - z");
assert_eq!(items_with_z, "x - z = 0");
}
}

121
constraint-solver/src/inliner.rs
View File

@@ -1,4 +1,4 @@
use crate::constraint_system::ConstraintRef;
use crate::constraint_system::{AlgebraicConstraint, ConstraintRef};
use crate::grouped_expression::GroupedExpression;
use crate::indexed_constraint_system::IndexedConstraintSystem;
use crate::journaling_constraint_system::JournalingConstraintSystem;
@@ -100,8 +100,11 @@ pub fn substitution_would_not_violate_degree_bound<
.constraints_referencing_variables(std::iter::once(var.clone()))
.all(|cref| match cref {
ConstraintRef::AlgebraicConstraint(identity) => {
let degree =
expression_degree_with_virtual_substitution(identity, var, replacement_deg);
let degree = expression_degree_with_virtual_substitution(
&identity.expression,
var,
replacement_deg,
);
degree <= degree_bound.identities
}
ConstraintRef::BusInteraction(interaction) => interaction.fields().all(|expr| {
@@ -117,13 +120,13 @@ fn find_inlinable_variables<
T: RuntimeConstant + ExpressionConvertible<T::FieldType, V> + Display,
V: Ord + Clone + Hash + Eq + Display,
>(
constraint: &GroupedExpression<T, V>,
constraint: &AlgebraicConstraint<GroupedExpression<T, V>>,
) -> Vec<(V, GroupedExpression<T, V>)> {
let (_, linear, _) = constraint.components();
let (_, linear, _) = constraint.expression.components();
linear
.rev()
.filter_map(|(target_var, _)| {
let rhs_expr = constraint.try_solve_for(target_var)?;
let rhs_expr = constraint.expression.try_solve_for(target_var)?;
assert!(!rhs_expr.referenced_unknown_variables().contains(target_var));
Some((target_var.clone(), rhs_expr))
})
@@ -173,14 +176,12 @@ mod test {
#[test]
fn test_no_substitution() {
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
let constraint_system = ConstraintSystem::default()
.with_constraints(vec![
var("a") * var("b") + var("c") * var("d"),
var("e") * var("e") - constant(2),
],
bus_interactions: vec![],
}
.into();
])
.into();
let constraint_system =
replace_constrained_witness_columns(constraint_system, bounds(3, 3));
@@ -196,15 +197,14 @@ mod test {
multiplicity: constant(1),
}];
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
let constraint_system = ConstraintSystem::default()
.with_constraints(vec![
var("a") + var("b") + var("c"),
var("b") + var("d") - constant(1),
var("c") + var("b") + var("a") + var("d") - var("0result"),
],
bus_interactions,
}
.into();
])
.with_bus_interactions(bus_interactions)
.into();
let constraint_system =
replace_constrained_witness_columns(constraint_system, bounds(3, 3));
@@ -253,11 +253,10 @@ mod test {
multiplicity: constant(1),
}];
let constraint_system = ConstraintSystem {
algebraic_constraints: identities,
bus_interactions,
}
.into();
let constraint_system = ConstraintSystem::default()
.with_constraints(identities)
.with_bus_interactions(bus_interactions)
.into();
let constraint_system =
replace_constrained_witness_columns(constraint_system, bounds(3, 3));
@@ -288,11 +287,9 @@ mod test {
identities.push(expr_constraint);
// no columns to keep
let constraint_system = ConstraintSystem {
algebraic_constraints: identities,
bus_interactions: vec![],
}
.into();
let constraint_system = ConstraintSystem::default()
.with_constraints(identities)
.into();
let constraint_system =
replace_constrained_witness_columns(constraint_system, bounds(3, 3));
@@ -310,15 +307,14 @@ mod test {
multiplicity: constant(1),
}];
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
let constraint_system = ConstraintSystem::default()
.with_constraints(vec![
var("y") - (var("x") + constant(3)),
var("z") - (var("y") + constant(2)),
var("result") - (var("z") + constant(1)),
],
bus_interactions,
}
.into();
])
.with_bus_interactions(bus_interactions)
.into();
let constraint_system =
replace_constrained_witness_columns(constraint_system, bounds(3, 3));
@@ -338,31 +334,32 @@ mod test {
#[test]
fn test_replace_constrained_witness_columns_max_degree_limit() {
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
let constraint_system = ConstraintSystem::default()
.with_constraints(vec![
var("a") - (var("b") + constant(1)),
var("c") - (var("a") * var("a")),
var("d") - (var("c") * var("a")),
var("e") - (var("d") * var("a")),
var("f") - (var("e") + constant(5)),
var("result") - (var("f") * constant(2)),
],
// Get all variables
bus_interactions: vec![BusInteraction {
bus_id: constant(1),
payload: vec![
var("a"),
var("b"),
var("c"),
var("d"),
var("e"),
var("f"),
var("result"),
],
multiplicity: constant(1),
}],
}
.into();
])
.with_bus_interactions(
// Get all variables
vec![BusInteraction {
bus_id: constant(1),
payload: vec![
var("a"),
var("b"),
var("c"),
var("d"),
var("e"),
var("f"),
var("result"),
],
multiplicity: constant(1),
}],
)
.into();
let constraint_system =
replace_constrained_witness_columns(constraint_system, bounds(3, 3));
@@ -384,7 +381,7 @@ mod test {
// In-lining c would violate the degree bound, so it is kept as a symbol
// with a constraint to enforce the equality.
assert_eq!(c.to_string(), "c");
assert_eq!(identity.to_string(), "-((a) * (a) - c)");
assert_eq!(identity.to_string(), "-((a) * (a) - c) = 0");
// From third identity: d = c * a
assert_eq!(d.to_string(), "(c) * (a)");
// From fourth identity: e = d * a
@@ -428,17 +425,13 @@ mod test {
suboptimal_order_identities.push(constraint2.clone()); // b = c + d
suboptimal_order_identities.push(constraint4.clone()); // c = d * d
let optimal_system = ConstraintSystem {
algebraic_constraints: optimal_order_identities,
bus_interactions: vec![],
}
.into();
let optimal_system = ConstraintSystem::default()
.with_constraints(optimal_order_identities)
.into();
let suboptimal_system = ConstraintSystem {
algebraic_constraints: suboptimal_order_identities,
bus_interactions: vec![],
}
.into();
let suboptimal_system = ConstraintSystem::default()
.with_constraints(suboptimal_order_identities)
.into();
// Apply the same optimization to both systems
let optimal_system = replace_constrained_witness_columns(optimal_system, bounds(5, 5));

10
constraint-solver/src/journaling_constraint_system.rs
View File

@@ -1,5 +1,5 @@
use crate::{
constraint_system::{BusInteraction, ConstraintSystem},
constraint_system::{AlgebraicConstraint, BusInteraction, ConstraintSystem},
grouped_expression::GroupedExpression,
indexed_constraint_system::IndexedConstraintSystem,
runtime_constant::{RuntimeConstant, Substitutable},
@@ -32,7 +32,9 @@ impl<T: RuntimeConstant, V: Hash + Clone + Eq> JournalingConstraintSystem<T, V>
}
/// Returns an iterator over the algebraic constraints.
pub fn algebraic_constraints(&self) -> impl Iterator<Item = &GroupedExpression<T, V>> {
pub fn algebraic_constraints(
&self,
) -> impl Iterator<Item = &AlgebraicConstraint<GroupedExpression<T, V>>> {
self.system.algebraic_constraints().iter()
}
@@ -72,7 +74,7 @@ impl<T: RuntimeConstant, V: Clone + Eq + Hash> JournalingConstraintSystem<T, V>
/// Adds new algebraic constraints to the system.
pub fn add_algebraic_constraints(
&mut self,
constraints: impl IntoIterator<Item = GroupedExpression<T, V>>,
constraints: impl IntoIterator<Item = AlgebraicConstraint<GroupedExpression<T, V>>>,
) {
self.system.add_algebraic_constraints(constraints);
}
@@ -90,7 +92,7 @@ impl<T: RuntimeConstant, V: Clone + Eq> JournalingConstraintSystem<T, V> {
/// Removes all algebraic constraints that do not fulfill the predicate.
pub fn retain_algebraic_constraints(
&mut self,
f: impl FnMut(&GroupedExpression<T, V>) -> bool,
f: impl FnMut(&AlgebraicConstraint<GroupedExpression<T, V>>) -> bool,
) {
// We do not track removal of constraints yet, but we could.
self.system.retain_algebraic_constraints(f);

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

@@ -1,6 +1,8 @@
use powdr_number::ExpressionConvertible;
use crate::constraint_system::{BusInteraction, BusInteractionHandler, ConstraintSystem};
use crate::constraint_system::{
AlgebraicConstraint, BusInteraction, BusInteractionHandler, ConstraintSystem,
};
use crate::grouped_expression::GroupedExpression;
use crate::range_constraint::RangeConstraint;
use crate::runtime_constant::{
@@ -75,7 +77,7 @@ pub trait Solver<T: RuntimeConstant, V>: RangeConstraintProvider<T::FieldType, V
/// Adds a new algebraic constraint to the system.
fn add_algebraic_constraints(
&mut self,
constraints: impl IntoIterator<Item = GroupedExpression<T, V>>,
constraints: impl IntoIterator<Item = AlgebraicConstraint<GroupedExpression<T, V>>>,
);
/// Adds a new bus interaction to the system.

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

@@ -2,7 +2,9 @@ use itertools::Itertools;
use num_traits::Zero;
use powdr_number::{ExpressionConvertible, FieldElement};
use crate::constraint_system::{BusInteraction, BusInteractionHandler, ConstraintRef};
use crate::constraint_system::{
AlgebraicConstraint, BusInteraction, BusInteractionHandler, ConstraintRef,
};
use crate::effect::Effect;
use crate::grouped_expression::{GroupedExpression, RangeConstraintProvider};
use crate::indexed_constraint_system::IndexedConstraintSystemWithQueue;
@@ -149,7 +151,7 @@ where
fn add_algebraic_constraints(
&mut self,
constraints: impl IntoIterator<Item = GroupedExpression<T, V>>,
constraints: impl IntoIterator<Item = AlgebraicConstraint<GroupedExpression<T, V>>>,
) {
self.equivalent_expressions_cache.clear();
@@ -164,7 +166,7 @@ where
// needed because of unique access to the var dispenser / self.
.collect_vec()
.into_iter()
.flat_map(|constr| self.linearize_expression(constr))
.flat_map(|constr| self.linearize_constraint(constr))
.collect_vec();
self.constraint_system
@@ -270,34 +272,34 @@ where
/// by introducing new boolean variables.
fn try_extract_boolean(
&mut self,
constr: &GroupedExpression<T, V>,
) -> Option<GroupedExpression<T, V>> {
let (constr, var) = self
constr: &AlgebraicConstraint<GroupedExpression<T, V>>,
) -> Option<AlgebraicConstraint<GroupedExpression<T, V>>> {
let result = self
.boolean_extractor
.try_extract_boolean(constr, || self.var_dispenser.next_boolean())?;
if let Some(var) = var {
if let Some(var) = result.new_unconstrained_boolean_variable {
// If we created a boolean variable, we constrain it to be boolean.
self.add_range_constraint(&var, RangeConstraint::from_mask(1));
}
Some(constr)
Some(result.constraint)
}
/// Performs linearization of `constr`, i.e. replaces all non-affine sub-components of the constraint
/// by new variables.
/// This function will always return the original constraint as well as the linearized constraints
/// and equivalences needed after linearization.
fn linearize_expression(
fn linearize_constraint(
&mut self,
constr: GroupedExpression<T, V>,
) -> impl Iterator<Item = GroupedExpression<T, V>> {
constr: AlgebraicConstraint<GroupedExpression<T, V>>,
) -> impl Iterator<Item = AlgebraicConstraint<GroupedExpression<T, V>>> {
let mut constrs = vec![constr.clone()];
if !constr.is_affine() {
let linearized = self.linearizer.linearize(
constr,
let linearized = self.linearizer.linearize_expression(
constr.expression,
&mut || self.var_dispenser.next_linear(),
&mut constrs,
);
constrs.push(linearized);
constrs.push(AlgebraicConstraint::assert_zero(linearized));
}
constrs.into_iter()
}
@@ -310,7 +312,7 @@ where
fn linearize_bus_interaction(
&mut self,
bus_interaction: BusInteraction<GroupedExpression<T, V>>,
constraint_collection: &mut Vec<GroupedExpression<T, V>>,
constraint_collection: &mut Vec<AlgebraicConstraint<GroupedExpression<T, V>>>,
) -> BusInteraction<GroupedExpression<T, V>> {
bus_interaction
.fields()
@@ -541,11 +543,11 @@ where
ConstraintRef::BusInteraction(_) => None,
})
.flat_map(|constr| {
let (constr, new_var) = self
let result = self
.boolean_extractor
.try_extract_boolean(constr, &mut || self.var_dispenser.next_boolean())?;
vars_to_boolean_constrain.extend(new_var);
Some(constr)
vars_to_boolean_constrain.extend(result.new_unconstrained_boolean_variable);
Some(result.constraint)
})
.collect_vec();
for v in vars_to_boolean_constrain {

98
constraint-solver/src/solver/boolean_extractor.rs
View File

@@ -4,6 +4,7 @@ use itertools::Itertools;
use powdr_number::{FieldElement, LargeInt};
use crate::{
constraint_system::AlgebraicConstraint,
grouped_expression::GroupedExpression,
indexed_constraint_system::apply_substitutions_to_expressions,
runtime_constant::{RuntimeConstant, Substitutable},
@@ -31,6 +32,11 @@ impl<T, V> Default for BooleanExtractor<T, V> {
}
}
pub struct BooleanExtractionValue<T, V> {
pub constraint: AlgebraicConstraint<GroupedExpression<T, V>>,
pub new_unconstrained_boolean_variable: Option<V>,
}
impl<T: RuntimeConstant + Hash, V: Ord + Clone + Hash + Eq> BooleanExtractor<T, V> {
/// Tries to simplify a quadratic constraint by transforming it into an affine
/// constraint that makes use of a new boolean variable.
@@ -49,9 +55,9 @@ impl<T: RuntimeConstant + Hash, V: Ord + Clone + Hash + Eq> BooleanExtractor<T,
/// It will only be called if the transformation is performed.
pub fn try_extract_boolean(
&mut self,
constraint: &GroupedExpression<T, V>,
constraint: &AlgebraicConstraint<GroupedExpression<T, V>>,
mut var_dispenser: impl FnMut() -> V,
) -> Option<(GroupedExpression<T, V>, Option<V>)> {
) -> Option<BooleanExtractionValue<T, V>> {
let (left, right) = constraint.try_as_single_product()?;
// We want to check if `left` and `right` differ by a constant offset.
// Since multiplying the whole constraint by a non-zero constant does
@@ -95,7 +101,10 @@ impl<T: RuntimeConstant + Hash, V: Ord + Clone + Hash + Eq> BooleanExtractor<T,
None
} else {
self.substitutions.insert(right.clone(), None);
Some((right.clone(), None))
Some(BooleanExtractionValue {
constraint: AlgebraicConstraint::assert_zero(right.clone()),
new_unconstrained_boolean_variable: None,
})
}
} else {
// We can substitute the initial constraint using a new boolean variable `z`
@@ -133,10 +142,12 @@ impl<T: RuntimeConstant + Hash, V: Ord + Clone + Hash + Eq> BooleanExtractor<T,
self.substitutions.insert(key, Some(z.clone()));
// We return `expr + z * offset == 0`, which is equivalent to the original constraint.
Some((
expr + (GroupedExpression::from_unknown_variable(z.clone()) * offset),
Some(z),
))
Some(BooleanExtractionValue {
constraint: AlgebraicConstraint::assert_zero(
expr + (GroupedExpression::from_unknown_variable(z.clone()) * offset),
),
new_unconstrained_boolean_variable: Some(z),
})
}
}
}
@@ -174,11 +185,11 @@ mod tests {
let mut var_dispenser = || "z";
let expr = (var("a") + var("b")) * (var("a") + var("b") + constant(10));
let mut extractor: BooleanExtractor<_, _> = Default::default();
let result = extractor.try_extract_boolean(&expr, &mut var_dispenser);
assert!(result.is_some());
let (result, z) = result.unwrap();
assert_eq!(result.to_string(), "-(a + b + 10 * z)");
assert_eq!(z, Some("z"));
let result = extractor
.try_extract_boolean(&expr.into(), &mut var_dispenser)
.unwrap();
assert_eq!(result.constraint.to_string(), "-(a + b + 10 * z) = 0");
assert_eq!(result.new_unconstrained_boolean_variable, Some("z"));
}
#[test]
@@ -186,11 +197,11 @@ mod tests {
let mut var_dispenser = || "z";
let expr = (var("a") + var("b")) * (var("a") + var("b"));
let mut extractor: BooleanExtractor<_, _> = Default::default();
let result = extractor.try_extract_boolean(&expr, &mut var_dispenser);
assert!(result.is_some());
let (result, z) = result.unwrap();
assert_eq!(result.to_string(), "a + b");
assert_eq!(z, None);
let result = extractor
.try_extract_boolean(&expr.into(), &mut var_dispenser)
.unwrap();
assert_eq!(result.constraint.to_string(), "a + b = 0");
assert_eq!(result.new_unconstrained_boolean_variable, None);
}
#[test]
@@ -198,11 +209,11 @@ mod tests {
let mut var_dispenser = || "z";
let expr = (var("a") - constant(1)) * (var("a"));
let mut extractor: BooleanExtractor<_, _> = Default::default();
let result = extractor.try_extract_boolean(&expr, &mut var_dispenser);
let result = extractor.try_extract_boolean(&expr.into(), &mut var_dispenser);
assert!(result.is_none());
let expr = (constant(2) * var("a") - constant(2)) * (constant(2) * var("a"));
let result = extractor.try_extract_boolean(&expr, &mut var_dispenser);
let result = extractor.try_extract_boolean(&expr.into(), &mut var_dispenser);
assert!(result.is_none());
}
@@ -211,43 +222,43 @@ mod tests {
let mut var_dispenser = || "z";
let expr = (var("a") + var("b")) * (var("a") + var("b") + constant(10));
let mut extractor: BooleanExtractor<_, _> = Default::default();
let result = extractor.try_extract_boolean(&expr, &mut var_dispenser);
assert!(result.is_some());
let (result, z) = result.unwrap();
assert_eq!(result.to_string(), "-(a + b + 10 * z)");
assert_eq!(z, Some("z"));
let result = extractor
.try_extract_boolean(&expr.clone().into(), &mut var_dispenser)
.unwrap();
assert_eq!(result.constraint.to_string(), "-(a + b + 10 * z) = 0");
assert_eq!(result.new_unconstrained_boolean_variable, Some("z"));
assert!(extractor
.try_extract_boolean(&expr, &mut var_dispenser)
.try_extract_boolean(&expr.into(), &mut var_dispenser)
.is_none());
// left and right swapped
assert!(extractor
.try_extract_boolean(
&(var("a") + var("b") + constant(10) * (var("a") + var("b"))),
&(var("a") + var("b") + constant(10) * (var("a") + var("b"))).into(),
&mut var_dispenser
)
.is_none());
let expr2 = (constant(2) * (var("a") + var("b"))) * (var("a") + var("b") + constant(10));
assert!(extractor
.try_extract_boolean(&expr2, &mut var_dispenser)
.try_extract_boolean(&expr2.into(), &mut var_dispenser)
.is_none());
let expr3 = (var("a") + var("b")) * (constant(2) * (var("a") + var("b") + constant(10)));
assert!(extractor
.try_extract_boolean(&expr3, &mut var_dispenser)
.try_extract_boolean(&expr3.into(), &mut var_dispenser)
.is_none());
// This is different because the effective constant is different.
let expr4 = (var("a") + var("b")) * (constant(2) * (var("a") + var("b") + constant(20)));
assert_eq!(
extractor
.try_extract_boolean(&expr4, &mut var_dispenser)
.try_extract_boolean(&expr4.into(), &mut var_dispenser)
.unwrap()
.0
.constraint
.to_string(),
"-(2 * a + 2 * b + 40 * z)"
"-(2 * a + 2 * b + 40 * z) = 0"
);
}
@@ -256,13 +267,14 @@ mod tests {
let mut var_dispenser = || "z";
let expr = (var("a") + var("b")) * (var("a") + var("b"));
let mut extractor: BooleanExtractor<_, _> = Default::default();
let result = extractor.try_extract_boolean(&expr, &mut var_dispenser);
assert!(result.is_some());
let (result, z) = result.unwrap();
assert_eq!(result.to_string(), "a + b");
assert_eq!(z, None);
let result = extractor
.try_extract_boolean(&expr.clone().into(), &mut var_dispenser)
.unwrap();
let result = extractor.try_extract_boolean(&expr, &mut var_dispenser);
assert_eq!(result.constraint.to_string(), "a + b = 0");
assert_eq!(result.new_unconstrained_boolean_variable, None);
let result = extractor.try_extract_boolean(&expr.into(), &mut var_dispenser);
assert!(result.is_none());
}
@@ -277,17 +289,17 @@ mod tests {
let expr =
(var("a") + var("b") + var("k")) * (var("a") + var("b") + var("k") - constant(2));
let mut extractor: BooleanExtractor<_, _> = Default::default();
let result = extractor.try_extract_boolean(&expr, &mut var_dispenser);
assert!(result.is_some());
let (result, z) = result.unwrap();
assert_eq!(result.to_string(), "-(a + b + k - 2 * z_0)");
assert_eq!(z, Some("z_0"));
let result = extractor
.try_extract_boolean(&expr.into(), &mut var_dispenser)
.unwrap();
assert_eq!(result.constraint.to_string(), "-(a + b + k - 2 * z_0) = 0");
assert_eq!(result.new_unconstrained_boolean_variable, Some("z_0"));
extractor.apply_assignments(&[("k", -constant(9))]);
let expr2 =
(var("a") + var("b") - constant(9)) * (var("a") + var("b") - constant(9) - constant(2));
let result = extractor.try_extract_boolean(&expr2, &mut var_dispenser);
let result = extractor.try_extract_boolean(&expr2.into(), &mut var_dispenser);
assert!(result.is_none());
}
}

31
constraint-solver/src/solver/linearizer.rs
View File

@@ -3,6 +3,7 @@ use std::hash::Hash;
use itertools::Itertools;
use crate::constraint_system::AlgebraicConstraint;
use crate::indexed_constraint_system::apply_substitutions_to_expressions;
use crate::runtime_constant::Substitutable;
use crate::solver::VariableAssignment;
@@ -23,15 +24,15 @@ impl<T, V> Default for Linearizer<T, V> {
}
impl<T: RuntimeConstant + Hash, V: Clone + Eq + Ord + Hash> Linearizer<T, V> {
/// Linearizes the constraint by introducing new variables for
/// Linearizes the expression by introducing new variables for
/// non-affine parts. The new constraints are appended to
/// `constraint_collection` and must be added to the system.
/// The linearized expression is returned.
pub fn linearize(
pub fn linearize_expression(
&mut self,
expr: GroupedExpression<T, V>,
var_dispenser: &mut impl FnMut() -> V,
constraint_collection: &mut impl Extend<GroupedExpression<T, V>>,
constraint_collection: &mut impl Extend<AlgebraicConstraint<GroupedExpression<T, V>>>,
) -> GroupedExpression<T, V> {
if expr.is_affine() {
return expr;
@@ -89,9 +90,9 @@ impl<T: RuntimeConstant + Hash, V: Clone + Eq + Ord + Hash> Linearizer<T, V> {
&mut self,
expr: GroupedExpression<T, V>,
var_dispenser: &mut impl FnMut() -> V,
constraint_collection: &mut impl Extend<GroupedExpression<T, V>>,
constraint_collection: &mut impl Extend<AlgebraicConstraint<GroupedExpression<T, V>>>,
) -> GroupedExpression<T, V> {
let linearized = self.linearize(expr, var_dispenser, constraint_collection);
let linearized = self.linearize_expression(expr, var_dispenser, constraint_collection);
self.substitute_by_var(linearized, var_dispenser, constraint_collection)
}
@@ -104,7 +105,7 @@ impl<T: RuntimeConstant + Hash, V: Clone + Eq + Ord + Hash> Linearizer<T, V> {
&mut self,
expr: GroupedExpression<T, V>,
var_dispenser: &mut impl FnMut() -> V,
constraint_collection: &mut impl Extend<GroupedExpression<T, V>>,
constraint_collection: &mut impl Extend<AlgebraicConstraint<GroupedExpression<T, V>>>,
) -> GroupedExpression<T, V> {
if let Some(var) = self.try_substitute_by_existing_var(&expr) {
var
@@ -112,7 +113,7 @@ impl<T: RuntimeConstant + Hash, V: Clone + Eq + Ord + Hash> Linearizer<T, V> {
let var = var_dispenser();
self.substitutions.insert(expr.clone(), var.clone());
let var = GroupedExpression::from_unknown_variable(var);
constraint_collection.extend([expr - var.clone()]);
constraint_collection.extend([AlgebraicConstraint::assert_zero(expr - var.clone())]);
var
}
}
@@ -197,7 +198,7 @@ mod tests {
let mut linearizer = Linearizer::default();
let expr = var("x") + var("y") * (var("z") + constant(1)) * (var("x") - constant(1));
let mut constraints_to_add = vec![];
let linearized = linearizer.linearize(
let linearized = linearizer.linearize_expression(
expr,
&mut || {
let var = Variable::Linearized(var_counter);
@@ -209,7 +210,7 @@ mod tests {
assert_eq!(linearized.to_string(), "x + lin_3");
assert_eq!(
constraints_to_add.into_iter().format("\n").to_string(),
"z - lin_0 + 1\n(y) * (lin_0) - lin_1\nx - lin_2 - 1\n(lin_1) * (lin_2) - lin_3"
"z - lin_0 + 1 = 0\n(y) * (lin_0) - lin_1 = 0\nx - lin_2 - 1 = 0\n(lin_1) * (lin_2) - lin_3 = 0"
);
}
@@ -217,10 +218,14 @@ mod tests {
fn solver_transforms() {
let mut solver =
BaseSolver::<_, _, _, VarDispenserImpl>::new(DefaultBusInteractionHandler::default());
solver.add_algebraic_constraints(vec![
(var("x") + var("y")) * (var("z") + constant(1)) * (var("x") - constant(1)),
(var("a") + var("b")) * (var("c") - constant(2)),
]);
solver.add_algebraic_constraints(
[
(var("x") + var("y")) * (var("z") + constant(1)) * (var("x") - constant(1)),
(var("a") + var("b")) * (var("c") - constant(2)),
]
.into_iter()
.map(AlgebraicConstraint::assert_zero),
);
solver.add_bus_interactions(vec![BusInteraction {
bus_id: constant(1),
payload: vec![var("x") + var("y"), -var("a"), var("a")],

10
constraint-solver/src/solver/quadratic_equivalences.rs
View File

@@ -5,20 +5,20 @@ use std::{collections::HashSet, fmt::Display, hash::Hash};
use itertools::Itertools;
use crate::{
constraint_system::AlgebraicConstraint,
grouped_expression::{GroupedExpression, RangeConstraintProvider},
range_constraint::RangeConstraint,
runtime_constant::RuntimeConstant,
};
/// Given a list of constraints in the form of grouped expressions, tries to determine
/// pairs of equivalent variables.
/// Given a list of constraints, tries to determine pairs of equivalent variables.
pub fn find_quadratic_equalities<T: RuntimeConstant, V: Ord + Clone + Hash + Eq + Display>(
constraints: &[GroupedExpression<T, V>],
constraints: &[AlgebraicConstraint<GroupedExpression<T, V>>],
range_constraints: impl RangeConstraintProvider<T::FieldType, V>,
) -> Vec<(V, V)> {
let candidates = constraints
.iter()
.filter_map(QuadraticEqualityCandidate::try_from_grouped_expression)
.filter_map(QuadraticEqualityCandidate::try_from_constraint)
.filter(|c| c.variables.len() >= 2)
.collect::<Vec<_>>();
candidates
@@ -105,7 +105,7 @@ struct QuadraticEqualityCandidate<T: RuntimeConstant, V: Ord + Clone + Hash + Eq
}
impl<T: RuntimeConstant, V: Ord + Clone + Hash + Eq> QuadraticEqualityCandidate<T, V> {
fn try_from_grouped_expression(constr: &GroupedExpression<T, V>) -> Option<Self> {
fn try_from_constraint(constr: &AlgebraicConstraint<GroupedExpression<T, V>>) -> Option<Self> {
let (left, right) = constr.try_as_single_product()?;
if !left.is_affine() || !right.is_affine() {
return None;

25
constraint-solver/src/solver/var_transformation.rs
View File

@@ -1,4 +1,4 @@
use crate::constraint_system::BusInteraction;
use crate::constraint_system::{AlgebraicConstraint, BusInteraction};
use crate::grouped_expression::{GroupedExpression, RangeConstraintProvider};
use crate::range_constraint::RangeConstraint;
use crate::runtime_constant::{RuntimeConstant, VarTransformable};
@@ -117,10 +117,10 @@ where
fn add_algebraic_constraints(
&mut self,
constraints: impl IntoIterator<Item = GroupedExpression<T, V>>,
constraints: impl IntoIterator<Item = AlgebraicConstraint<GroupedExpression<T, V>>>,
) {
self.solver
.add_algebraic_constraints(constraints.into_iter().map(|c| transform(&c)));
.add_algebraic_constraints(constraints.into_iter().map(|c| transform_constraint(&c)));
}
fn add_bus_interactions(
@@ -130,7 +130,7 @@ where
self.solver.add_bus_interactions(
bus_interactions
.into_iter()
.map(|bus_interaction| bus_interaction.fields().map(transform).collect()),
.map(|bus_interaction| bus_interaction.fields().map(transform_expr).collect()),
)
}
@@ -154,7 +154,7 @@ where
expr: &GroupedExpression<T, V>,
) -> RangeConstraint<T::FieldType> {
self.solver
.range_constraint_for_expression(&transform(expr))
.range_constraint_for_expression(&transform_expr(expr))
}
fn are_expressions_known_to_be_different(
@@ -162,13 +162,13 @@ where
a: &GroupedExpression<T, V>,
b: &GroupedExpression<T, V>,
) -> bool {
let a = transform(a);
let b = transform(b);
let a = transform_expr(a);
let b = transform_expr(b);
self.solver.are_expressions_known_to_be_different(&a, &b)
}
}
fn transform<T, V: Ord + Clone>(
fn transform_expr<T, V: Ord + Clone>(
expr: &GroupedExpression<T, V>,
) -> GroupedExpression<T::Transformed, Variable<V>>
where
@@ -176,3 +176,12 @@ where
{
expr.transform_var_type(&mut |v| v.into())
}
fn transform_constraint<T, V: Ord + Clone>(
constraint: &AlgebraicConstraint<GroupedExpression<T, V>>,
) -> AlgebraicConstraint<GroupedExpression<T::Transformed, Variable<V>>>
where
T: RuntimeConstant + VarTransformable<V, Variable<V>>,
{
AlgebraicConstraint::assert_zero(transform_expr(&constraint.expression))
}

27
constraint-solver/src/test_utils.rs
View File

@@ -1,6 +1,11 @@
use powdr_number::GoldilocksField;
use crate::{grouped_expression::GroupedExpression, symbolic_expression::SymbolicExpression};
use crate::{
constraint_system::{AlgebraicConstraint, BusInteraction, ConstraintSystem},
grouped_expression::GroupedExpression,
runtime_constant::RuntimeConstant,
symbolic_expression::SymbolicExpression,
};
pub type Var = &'static str;
pub type Qse = GroupedExpression<SymbolicExpression<GoldilocksField, Var>, Var>;
@@ -12,3 +17,23 @@ pub fn var(name: Var) -> Qse {
pub fn constant(value: u64) -> Qse {
Qse::from_number(GoldilocksField::from(value))
}
impl<T: RuntimeConstant, V> ConstraintSystem<T, V> {
pub fn with_constraints(
mut self,
constraints: Vec<impl Into<AlgebraicConstraint<GroupedExpression<T, V>>>>,
) -> Self {
self.algebraic_constraints
.extend(constraints.into_iter().map(Into::into));
self
}
pub fn with_bus_interactions(
mut self,
bus_interactions: Vec<impl Into<BusInteraction<GroupedExpression<T, V>>>>,
) -> Self {
self.bus_interactions
.extend(bus_interactions.into_iter().map(Into::into));
self
}
}

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

@@ -59,10 +59,7 @@ fn assert_expected_state(
#[test]
fn single_variable() {
assert_solve_result(
ConstraintSystem {
algebraic_constraints: vec![var("x") - constant(5)],
bus_interactions: vec![],
},
ConstraintSystem::default().with_constraints(vec![var("x") - constant(5)]),
DefaultBusInteractionHandler::default(),
vec![("x", 5.into())],
);
@@ -70,17 +67,14 @@ fn single_variable() {
#[test]
fn concretely_solvable() {
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
var("a") - constant(2),
var("b") - constant(3),
// c = a * b = 6
var("c") - var("a") * var("b"),
// d = c * 4 - a = 22
var("d") - (var("c") * constant(4) - var("a")),
],
bus_interactions: vec![],
};
let constraint_system = ConstraintSystem::default().with_constraints(vec![
var("a") - constant(2),
var("b") - constant(3),
// c = a * b = 6
var("c") - var("a") * var("b"),
// d = c * 4 - a = 22
var("d") - (var("c") * constant(4) - var("a")),
]);
assert_solve_result(
constraint_system,
DefaultBusInteractionHandler::default(),
@@ -95,19 +89,16 @@ fn concretely_solvable() {
#[test]
fn bit_decomposition() {
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
// 4 bit-constrained variables:
var("b0") * (var("b0") - constant(1)),
var("b1") * (var("b1") - constant(1)),
var("b2") * (var("b2") - constant(1)),
var("b3") * (var("b3") - constant(1)),
// Bit-decomposition of a concrete value:
var("b0") + var("b1") * constant(2) + var("b2") * constant(4) + var("b3") * constant(8)
- constant(0b1110),
],
bus_interactions: vec![],
};
let constraint_system = ConstraintSystem::default().with_constraints(vec![
// 4 bit-constrained variables:
var("b0") * (var("b0") - constant(1)),
var("b1") * (var("b1") - constant(1)),
var("b2") * (var("b2") - constant(1)),
var("b3") * (var("b3") - constant(1)),
// Bit-decomposition of a concrete value:
var("b0") + var("b1") * constant(2) + var("b2") * constant(4) + var("b3") * constant(8)
- constant(0b1110),
]);
assert_solve_result(
constraint_system,
@@ -192,20 +183,21 @@ fn send(
#[test]
fn byte_decomposition() {
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
let constraint_system = ConstraintSystem::default()
.with_constraints(vec![
// Byte-decomposition of a concrete value:
var("b0")
+ var("b1") * constant(1 << 8)
+ var("b2") * constant(1 << 16)
+ var("b3") * constant(1 << 24)
- constant(0xabcdef12),
],
// Byte range constraints on b0..3
bus_interactions: (0..4)
.map(|i| send(BYTE_BUS_ID, vec![var(format!("b{i}").leak())]))
.collect(),
};
])
.with_bus_interactions(
// Byte range constraints on b0..3
(0..4)
.map(|i| send(BYTE_BUS_ID, vec![var(format!("b{i}").leak())]))
.collect(),
);
assert_solve_result(
constraint_system,
@@ -221,17 +213,16 @@ fn byte_decomposition() {
#[test]
fn xor() {
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
let constraint_system = ConstraintSystem::default()
.with_constraints(vec![
// a and b are the byte decomposition of 0xa00b
// Note that solving this requires range constraints on a and b
constant(1 << 8) * var("a") + var("b") - constant(0xa00b),
],
])
// Send (a, b, c) to the XOR table.
// Initially, this should return the required range constraints for a and b.
// Once a and b are known concretely, c can be computed concretely as well.
bus_interactions: vec![send(XOR_BUS_ID, vec![var("a"), var("b"), var("c")])],
};
.with_bus_interactions(vec![send(XOR_BUS_ID, vec![var("a"), var("b"), var("c")])]);
assert_solve_result(
constraint_system,
@@ -242,16 +233,13 @@ fn xor() {
#[test]
fn xor_invalid() {
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
let constraint_system = ConstraintSystem::default()
.with_constraints(vec![
var("a") - constant(0xa0),
var("b") - constant(0x0b),
var("c") - constant(0xff),
],
// Send (a, b, c) to the XOR table.
// Note that this violates the bus rules, because 0xa0 ^ 0x0b != 0xff.
bus_interactions: vec![send(XOR_BUS_ID, vec![var("a"), var("b"), var("c")])],
};
])
.with_bus_interactions(vec![send(XOR_BUS_ID, vec![var("a"), var("b"), var("c")])]);
match solve_system(constraint_system, TestBusInteractionHandler) {
Err(e) => assert_eq!(e, Error::BusInteractionError),
@@ -267,18 +255,17 @@ fn add_with_carry() {
// A or A - 256, depending on whether the value of A is between
// 0 and 255 or not.
// A is the result of an addition with carry.
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
let constraint_system = ConstraintSystem::default()
.with_constraints(vec![
(var("X") * constant(7) - var("A") * constant(7) + constant(256) * constant(7))
* (var("X") * constant(7) - var("A") * constant(7)),
(var("Y") - var("A") + constant(256)) * (var("Y") - var("A")),
],
// Byte range constraints on X and Y
bus_interactions: vec![
])
.with_bus_interactions(vec![
// Byte range constraints on X and Y
send(BYTE_BUS_ID, vec![var("X")]),
send(BYTE_BUS_ID, vec![var("Y")]),
],
};
]);
let final_state = solve_system(constraint_system.clone(), TestBusInteractionHandler).unwrap();
let final_state = apply_substitutions(constraint_system, final_state)
@@ -288,31 +275,28 @@ fn add_with_carry() {
.to_string();
assert_eq!(
final_state,
"(7 * A - 7 * X - 1792) * (7 * A - 7 * X)
(A - X - 256) * (A - X)"
"(7 * A - 7 * X - 1792) * (7 * A - 7 * X) = 0
(A - X - 256) * (A - X) = 0"
);
}
#[test]
fn one_hot_flags() {
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
// Boolean flags
var("flag0") * (var("flag0") - constant(1)),
var("flag1") * (var("flag1") - constant(1)),
var("flag2") * (var("flag2") - constant(1)),
var("flag3") * (var("flag3") - constant(1)),
// Exactly one flag is active
var("flag0") + var("flag1") + var("flag2") + var("flag3") - constant(1),
// Flag 2 is active
var("flag0") * constant(0)
+ var("flag1") * constant(1)
+ var("flag2") * constant(2)
+ var("flag3") * constant(3)
- constant(2),
],
bus_interactions: vec![],
};
let constraint_system = ConstraintSystem::default().with_constraints(vec![
// Boolean flags
var("flag0") * (var("flag0") - constant(1)),
var("flag1") * (var("flag1") - constant(1)),
var("flag2") * (var("flag2") - constant(1)),
var("flag3") * (var("flag3") - constant(1)),
// Exactly one flag is active
var("flag0") + var("flag1") + var("flag2") + var("flag3") - constant(1),
// Flag 2 is active
var("flag0") * constant(0)
+ var("flag1") * constant(1)
+ var("flag2") * constant(2)
+ var("flag3") * constant(3)
- constant(2),
]);
// This can be solved via backtracking: There are 16 possible assignments
// for the 4 flags, but only 1 of them satisfies all the constraints.
@@ -339,24 +323,21 @@ fn binary_flags() {
.map(move |j| bit_to_expression(i & (1 << j) != 0, var(format!("flag{j}").leak())))
.fold(constant(1), |acc, x| acc * x)
};
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
// Boolean flags
var("flag0") * (var("flag0") - constant(1)),
var("flag1") * (var("flag1") - constant(1)),
var("flag2") * (var("flag2") - constant(1)),
index_to_expression(0b000) * constant(101)
+ index_to_expression(0b001) * constant(102)
+ index_to_expression(0b010) * constant(103)
+ index_to_expression(0b011) * constant(104)
+ index_to_expression(0b100) * constant(105)
+ index_to_expression(0b101) * constant(106)
+ index_to_expression(0b110) * constant(107)
+ index_to_expression(0b111) * constant(108)
- constant(104),
],
bus_interactions: vec![],
};
let constraint_system = ConstraintSystem::default().with_constraints(vec![
// Boolean flags
var("flag0") * (var("flag0") - constant(1)),
var("flag1") * (var("flag1") - constant(1)),
var("flag2") * (var("flag2") - constant(1)),
index_to_expression(0b000) * constant(101)
+ index_to_expression(0b001) * constant(102)
+ index_to_expression(0b010) * constant(103)
+ index_to_expression(0b011) * constant(104)
+ index_to_expression(0b100) * constant(105)
+ index_to_expression(0b101) * constant(106)
+ index_to_expression(0b110) * constant(107)
+ index_to_expression(0b111) * constant(108)
- constant(104),
]);
assert_solve_result(
constraint_system,
@@ -398,39 +379,36 @@ fn ternary_flags() {
var("flag1") * var("flag3"),
var("flag2") * var("flag3"),
];
let constraint_system = ConstraintSystem {
algebraic_constraints: vec![
// All flags are either 0, 1, or 2.
var("flag0") * (var("flag0") - constant(1)) * (var("flag0") - constant(2)),
var("flag1") * (var("flag1") - constant(1)) * (var("flag1") - constant(2)),
var("flag2") * (var("flag2") - constant(1)) * (var("flag2") - constant(2)),
var("flag3") * (var("flag3") - constant(1)) * (var("flag3") - constant(2)),
// The sum of flags is either 1 or 2.
(sum.clone() - constant(1)) * (sum.clone() - constant(2)),
// Of the expressions in `cases`, exactly one must evaluate to 1.
// From this constraint, it can be derived that it must be one of case 3, 4, 5, or 6.
cases[0].clone() * constant(1)
+ (cases[1].clone() + cases[2].clone()) * constant(2)
+ (cases[3].clone() + cases[4].clone() + cases[5].clone() + cases[6].clone())
* constant(3)
+ cases[7].clone() * constant(4)
+ (cases[8].clone() + cases[9].clone()) * constant(5)
+ (cases[10].clone() + cases[11].clone() + cases[12].clone() + cases[13].clone())
* constant(6)
- constant(3),
// We don't know which case is active, but for any of the cases that it could be,
// is_load would be 1, so we should be able to solve for it.
var("is_load")
- (cases[0].clone()
+ cases[1].clone()
+ cases[2].clone()
+ cases[3].clone()
+ cases[4].clone()
+ cases[5].clone()
+ cases[6].clone()),
],
bus_interactions: vec![],
};
let constraint_system = ConstraintSystem::default().with_constraints(vec![
// All flags are either 0, 1, or 2.
var("flag0") * (var("flag0") - constant(1)) * (var("flag0") - constant(2)),
var("flag1") * (var("flag1") - constant(1)) * (var("flag1") - constant(2)),
var("flag2") * (var("flag2") - constant(1)) * (var("flag2") - constant(2)),
var("flag3") * (var("flag3") - constant(1)) * (var("flag3") - constant(2)),
// The sum of flags is either 1 or 2.
(sum.clone() - constant(1)) * (sum.clone() - constant(2)),
// Of the expressions in `cases`, exactly one must evaluate to 1.
// From this constraint, it can be derived that it must be one of case 3, 4, 5, or 6.
cases[0].clone() * constant(1)
+ (cases[1].clone() + cases[2].clone()) * constant(2)
+ (cases[3].clone() + cases[4].clone() + cases[5].clone() + cases[6].clone())
* constant(3)
+ cases[7].clone() * constant(4)
+ (cases[8].clone() + cases[9].clone()) * constant(5)
+ (cases[10].clone() + cases[11].clone() + cases[12].clone() + cases[13].clone())
* constant(6)
- constant(3),
// We don't know which case is active, but for any of the cases that it could be,
// is_load would be 1, so we should be able to solve for it.
var("is_load")
- (cases[0].clone()
+ cases[1].clone()
+ cases[2].clone()
+ cases[3].clone()
+ cases[4].clone()
+ cases[5].clone()
+ cases[6].clone()),
]);
assert_solve_result(
constraint_system,
@@ -451,10 +429,7 @@ fn bit_decomposition_bug() {
(var("BusInteractionField(10, 2)") - constant(4))
* (var("BusInteractionField(10, 2)") - constant(8)),
];
let constraint_system = ConstraintSystem {
algebraic_constraints,
bus_interactions: vec![],
};
let constraint_system = ConstraintSystem::default().with_constraints(algebraic_constraints);
// The solver used to infer more assignments due to a bug
// in the bit decomposition logic.
assert_solve_result(

8
pilopt/src/qse_opt.rs
View File

@@ -7,7 +7,9 @@ use powdr_ast::analyzed::{
AlgebraicExpression, AlgebraicReference, AlgebraicUnaryOperation, AlgebraicUnaryOperator,
Analyzed, Challenge, Identity, PolynomialIdentity,
};
use powdr_constraint_solver::constraint_system::{ConstraintSystem, DefaultBusInteractionHandler};
use powdr_constraint_solver::constraint_system::{
AlgebraicConstraint, ConstraintSystem, DefaultBusInteractionHandler,
};
use powdr_constraint_solver::grouped_expression::GroupedExpression;
use powdr_constraint_solver::indexed_constraint_system::apply_substitutions;
use powdr_constraint_solver::runtime_constant::RuntimeConstant;
@@ -33,7 +35,9 @@ pub fn run_qse_optimization<T: FieldElement>(pil_file: &mut Analyzed<T>) {
.iter()
.filter_map(|identity| match identity {
Identity::Polynomial(PolynomialIdentity { expression, .. }) => {
Some(algebraic_to_quadratic_symbolic_expression(expression))
Some(AlgebraicConstraint::assert_zero(
algebraic_to_quadratic_symbolic_expression(expression),
))
}
_ => None,
})