Move constraint analysis (#2642)

Cargo.toml

@@ -10,6 +10,7 @@ members = [
     "cargo-powdr",
     "cli",
     "cli-rs",
+    "constraint-solver",
     "executor",
     "jit-compiler",
     "riscv",
@@ -48,6 +49,7 @@ powdr = { path = "./powdr", version = "0.1.4" }
 powdr-airgen = { path = "./airgen", version = "0.1.4" }
 powdr-ast = { path = "./ast", version = "0.1.4" }
 powdr-asm-to-pil = { path = "./asm-to-pil", version = "0.1.4" }
+powdr-constraint-solver = { path = "./constraint-solver", version = "0.1.4" }
 powdr-isa-utils = { path = "./isa-utils", version = "0.1.4" }
 powdr-analysis = { path = "./analysis", version = "0.1.4" }
 powdr-asmopt = { path = "./asmopt", version = "0.1.4" }

constraint-solver/Cargo.toml

@@ -0,0 +1,26 @@
+[package]
+name = "powdr-constraint-solver"
+description = "powdr tools to analyze and solve algebraic constraints"
+version = { workspace = true }
+edition = { workspace = true }
+license = { workspace = true }
+homepage = { workspace = true }
+repository = { workspace = true }
+
+[dependencies]
+powdr-ast.workspace = true
+powdr-number.workspace = true
+
+itertools = "0.13"
+num-traits = "0.2.15"
+derive_more = "0.99.17"
+auto_enums = "0.8.5"
+
+[dev-dependencies]
+pretty_assertions = "1.4.0"
+
+[lints]
+workspace = true
+
+[lib]
+bench = false # See https://github.com/bheisler/criterion.rs/issues/458

constraint-solver/src/effect.rs

@@ -0,0 +1,122 @@
+use std::fmt::{self, Display, Formatter};
+
+use itertools::Itertools;
+use powdr_number::FieldElement;
+
+use crate::{range_constraint::RangeConstraint, symbolic_expression::SymbolicExpression};
+
+/// The effect of solving a symbolic equation.
+#[derive(Clone, PartialEq, Eq)]
+pub enum Effect<T: FieldElement, V> {
+    /// Variable can be assigned a value.
+    Assignment(V, SymbolicExpression<T, V>),
+    /// Perform a bit decomposition of a known value, and assign multiple variables.
+    BitDecomposition(BitDecomposition<T, V>),
+    /// We learnt a new range constraint on variable.
+    RangeConstraint(V, RangeConstraint<T>),
+    /// A run-time assertion. If this fails, we have conflicting constraints.
+    Assertion(Assertion<T, V>),
+    /// A variable is assigned one of two alterantive expressions, depending on a condition.
+    ConditionalAssignment {
+        variable: V,
+        condition: BranchCondition<T, V>,
+        in_range_value: SymbolicExpression<T, V>,
+        out_of_range_value: SymbolicExpression<T, V>,
+    },
+}
+
+/// A bit decomposition of a value.
+/// Executing this effect solves the following equation:
+/// value = sum_{i=0}^{components.len() - 1} (-1)**components[i].negative * 2**components[i].exponent * components[i].variable
+///
+/// This effect can only be created if the equation has a unique solution.
+/// It might be that it leads to a contradiction, which should result in an assertion failure.
+#[derive(Clone, PartialEq, Eq)]
+pub struct BitDecomposition<T: FieldElement, V> {
+    /// The value that is decomposed.
+    pub value: SymbolicExpression<T, V>,
+    /// The components of the decomposition.
+    pub components: Vec<BitDecompositionComponent<T, V>>,
+}
+
+impl<T: FieldElement, V: Display> Display for BitDecomposition<T, V> {
+    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
+        let BitDecomposition { value, components } = self;
+        write!(f, "{} := {value};", components.iter().format(" + "))
+    }
+}
+
+/// A component in the bit decomposition.
+/// In a simplified form, we can solve for `variable` using
+/// `(value & bit_mask) >> exponent`.
+#[derive(Clone, PartialEq, Eq)]
+pub struct BitDecompositionComponent<T: FieldElement, V> {
+    /// The variables that will be assigned to.
+    pub variable: V,
+    /// If the variable occurs negatively in the equation.
+    /// Note that the range constraint of the variable itself is always non-negative.
+    pub is_negative: bool,
+    /// The exponent of two, which forms the coefficient of the variable.
+    pub exponent: u64,
+    /// The bit mask for this component, relative to the value to be decomposed,
+    /// i.e. already scaled by the coefficient.
+    pub bit_mask: T::Integer,
+}
+
+impl<T: FieldElement, V: Display> Display for BitDecompositionComponent<T, V> {
+    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
+        let BitDecompositionComponent {
+            variable,
+            is_negative,
+            exponent,
+            bit_mask: _,
+        } = self;
+        write!(
+            f,
+            "{}2**{exponent} * {variable}",
+            if *is_negative { "-" } else { "" },
+        )
+    }
+}
+
+/// A run-time assertion. If this fails, we have conflicting constraints.
+#[derive(Clone, PartialEq, Eq)]
+pub struct Assertion<T: FieldElement, V> {
+    pub lhs: SymbolicExpression<T, V>,
+    pub rhs: SymbolicExpression<T, V>,
+    /// If this is true, we assert that both sides are equal.
+    /// Otherwise, we assert that they are different.
+    pub expected_equal: bool,
+}
+
+impl<T: FieldElement, V> Assertion<T, V> {
+    pub fn assert_is_zero(condition: SymbolicExpression<T, V>) -> Effect<T, V> {
+        Self::assert_eq(condition, SymbolicExpression::from(T::from(0)))
+    }
+    pub fn assert_is_nonzero(condition: SymbolicExpression<T, V>) -> Effect<T, V> {
+        Self::assert_neq(condition, SymbolicExpression::from(T::from(0)))
+    }
+    pub fn assert_eq(lhs: SymbolicExpression<T, V>, rhs: SymbolicExpression<T, V>) -> Effect<T, V> {
+        Effect::Assertion(Assertion {
+            lhs,
+            rhs,
+            expected_equal: true,
+        })
+    }
+    pub fn assert_neq(
+        lhs: SymbolicExpression<T, V>,
+        rhs: SymbolicExpression<T, V>,
+    ) -> Effect<T, V> {
+        Effect::Assertion(Assertion {
+            lhs,
+            rhs,
+            expected_equal: false,
+        })
+    }
+}
+
+#[derive(Clone, PartialEq, Eq)]
+pub struct BranchCondition<T: FieldElement, V> {
+    pub value: SymbolicExpression<T, V>,
+    pub condition: RangeConstraint<T>,
+}

constraint-solver/src/lib.rs

@@ -0,0 +1,8 @@
+//! Tooling used for analysis and solving of constraints.
+
+pub mod algebraic_to_quadratic;
+pub mod effect;
+pub mod quadratic_symbolic_expression;
+pub mod range_constraint;
+pub mod symbolic_expression;
+pub mod variable_update;

constraint-solver/src/quadratic_symbolic_expression.rs

@@ -9,11 +9,8 @@ use itertools::Itertools;
 use num_traits::Zero;
 use powdr_number::{log2_exact, FieldElement, LargeInt};
 
-use crate::witgen::{
-    jit::effect::{Assertion, BitDecomposition, BitDecompositionComponent, Effect},
-    range_constraints::RangeConstraint,
-};
-
+use super::effect::{Assertion, BitDecomposition, BitDecompositionComponent, Effect};
+use super::range_constraint::RangeConstraint;
 use super::{symbolic_expression::SymbolicExpression, variable_update::VariableUpdate};
 
 #[derive(Default)]
@@ -582,7 +579,6 @@ mod tests {
     use std::collections::HashMap;
 
     use super::*;
-    use crate::witgen::range_constraints::RangeConstraint;
     use powdr_number::GoldilocksField;
 
     use pretty_assertions::assert_eq;

constraint-solver/src/range_constraint.rs

@@ -341,7 +341,6 @@ mod test {
     use itertools::Itertools;
     use powdr_number::GoldilocksField;
     use pretty_assertions::assert_eq;
-    use test_log::test;
 
     use super::*;
 

constraint-solver/src/symbolic_expression.rs

@@ -1,7 +1,5 @@
 use auto_enums::auto_enum;
 use itertools::Itertools;
-use powdr_ast::parsed::visitor::AllChildren;
-use powdr_number::FieldElement;
 use std::hash::Hash;
 use std::ops::Sub;
 use std::ops::{AddAssign, MulAssign};
@@ -12,8 +10,10 @@ use std::{
     sync::Arc,
 };
 
-use crate::witgen::range_constraints::RangeConstraint;
+use powdr_ast::parsed::visitor::AllChildren;
+use powdr_number::FieldElement;
 
+use super::range_constraint::RangeConstraint;
 use super::variable_update::VariableUpdate;
 
 /// A value that is known at run-time, defined through a complex expression

constraint-solver/src/symbolic_to_quadratic.rs

@@ -0,0 +1,38 @@
+use std::hash::Hash;
+
+use powdr_number::FieldElement;
+
+use crate::{
+    quadratic_symbolic_expression::QuadraticSymbolicExpression,
+    symbolic_expression::{BinaryOperator, SymbolicExpression, UnaryOperator},
+};
+
+pub fn symbolic_expression_to_quadratic_symbolic_expression<
+    T: FieldElement,
+    V: Clone + Ord + Hash,
+>(
+    e: &SymbolicExpression<T, V>,
+) -> Option<QuadraticSymbolicExpression<T, V>> {
+    Some(match e {
+        SymbolicExpression::Concrete(value) => (*value).into(),
+        SymbolicExpression::Symbol(var, _) => {
+            QuadraticSymbolicExpression::from_unknown_variable(var.clone())
+        }
+        SymbolicExpression::BinaryOperation(left, op, right, _) => {
+            let left = symbolic_expression_to_quadratic_symbolic_expression(left)?;
+            let right = symbolic_expression_to_quadratic_symbolic_expression(right)?;
+            match op {
+                BinaryOperator::Add => left + right,
+                BinaryOperator::Sub => left - right,
+                BinaryOperator::Mul => left * right,
+                BinaryOperator::Div => return None, // TODO
+            }
+        }
+        SymbolicExpression::UnaryOperation(op, inner, _) => {
+            let inner = symbolic_expression_to_quadratic_symbolic_expression(inner)?;
+            match op {
+                UnaryOperator::Neg => -inner,
+            }
+        }
+    })
+}

constraint-solver/src/variable_update.rs

@@ -1,6 +1,6 @@
 use powdr_number::FieldElement;
 
-use crate::witgen::range_constraints::RangeConstraint;
+use super::range_constraint::RangeConstraint;
 
 /// An update representing new information about a variable.
 #[derive(Debug, Clone)]

executor/Cargo.toml

@@ -9,6 +9,7 @@ repository = { workspace = true }
 
 [dependencies]
 powdr-ast.workspace = true
+powdr-constraint-solver.workspace = true
 powdr-executor-utils.workspace = true
 powdr-number.workspace = true
 powdr-parser-util.workspace = true

executor/src/witgen/affine_expression.rs

@@ -4,10 +4,10 @@ use itertools::{Either, Itertools};
 
 use num_traits::Zero;
 use powdr_ast::analyzed::{AlgebraicExpression, AlgebraicReference};
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 use powdr_number::{FieldElement, LargeInt};
 
 use super::global_constraints::RangeConstraintSet;
-use super::range_constraints::RangeConstraint;
 use super::Constraint;
 use super::{EvalError::*, EvalResult, EvalValue, IncompleteCause};
 
@@ -634,7 +634,8 @@ mod test {
     use std::collections::BTreeMap;
 
     use super::*;
-    use crate::witgen::{range_constraints::RangeConstraint, EvalError};
+    use crate::witgen::EvalError;
+    use powdr_constraint_solver::range_constraint::RangeConstraint;
     use powdr_number::{FieldElement, GoldilocksField};
     use pretty_assertions::assert_eq;
     use test_log::test;

executor/src/witgen/data_structures/mutable_state.rs

@@ -4,12 +4,12 @@ use std::{
 };
 
 use bit_vec::BitVec;
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 use powdr_number::FieldElement;
 
 use crate::witgen::{
     global_constraints::RangeConstraintSet,
     machines::{KnownMachine, LookupCell, Machine},
-    range_constraints::RangeConstraint,
     AffineExpression, AlgebraicVariable, EvalError, EvalResult, QueryCallback,
 };
 

executor/src/witgen/eval_result.rs

@@ -1,8 +1,9 @@
 use std::fmt::{self, Debug};
 
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 use powdr_number::FieldElement;
 
-use super::{affine_expression::AlgebraicVariable, range_constraints::RangeConstraint};
+use super::affine_expression::AlgebraicVariable;
 
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub enum IncompleteCause<K = usize> {

executor/src/witgen/global_constraints.rs

@@ -9,6 +9,7 @@ use powdr_ast::analyzed::{
     AlgebraicReference, AlgebraicReferenceThin, ContainsNextRef, PolyID, PolynomialType,
 };
 
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 use powdr_number::FieldElement;
 
 use crate::witgen::data_structures::column_map::{FixedColumnMap, WitnessColumnMap};
@@ -17,7 +18,6 @@ use super::affine_expression::AlgebraicVariable;
 use super::data_structures::identity::{BusReceive, Identity};
 use super::evaluators::partial_expression_evaluator::PartialExpressionEvaluator;
 use super::evaluators::symbolic_evaluator::SymbolicEvaluator;
-use super::range_constraints::RangeConstraint;
 use super::util::try_to_simple_poly;
 use super::{Constraint, FixedData};
 use powdr_ast::analyzed::AlgebraicExpression;

executor/src/witgen/jit/block_machine_processor.rs

@@ -3,6 +3,7 @@ use std::collections::{BTreeMap, BTreeSet, HashSet};
 use bit_vec::BitVec;
 use itertools::Itertools;
 use powdr_ast::analyzed::{ContainsNextRef, PolyID, PolynomialType};
+use powdr_constraint_solver::quadratic_symbolic_expression::QuadraticSymbolicExpression;
 use powdr_number::FieldElement;
 
 use crate::witgen::{
@@ -14,7 +15,6 @@ use crate::witgen::{
             Processor,
         },
         prover_function_heuristics::decode_prover_functions,
-        quadratic_symbolic_expression::QuadraticSymbolicExpression,
     },
     machines::MachineParts,
     FixedData,
@@ -394,6 +394,7 @@ impl<T: FieldElement> FixedEvaluator<T> for &BlockMachineProcessor<'_, T> {
 mod test {
     use std::fs::read_to_string;
 
+    use powdr_constraint_solver::range_constraint::RangeConstraint;
     use pretty_assertions::assert_eq;
     use test_log::test;
 
@@ -404,7 +405,6 @@ mod test {
         global_constraints,
         jit::{effect::format_code, test_util::read_pil},
         machines::{machine_extractor::MachineExtractor, KnownMachine, Machine},
-        range_constraints::RangeConstraint,
         FixedData,
     };
 

executor/src/witgen/jit/compiler.rs

@@ -6,6 +6,10 @@ use powdr_ast::{
     analyzed::{PolyID, PolynomialType},
     indent,
 };
+use powdr_constraint_solver::{
+    effect::{Assertion, BitDecomposition, BitDecompositionComponent, BranchCondition},
+    symbolic_expression::{BinaryOperator, SymbolicExpression, UnaryOperator},
+};
 use powdr_jit_compiler::{util_code::util_code, CodeGenerator, DefinitionFetcher};
 use powdr_number::FieldElement;
 
@@ -23,12 +27,8 @@ use crate::witgen::{
 };
 
 use super::{
-    effect::{
-        Assertion, BitDecomposition, BitDecompositionComponent, BranchCondition, Effect,
-        ProverFunctionCall,
-    },
+    effect::{Effect, ProverFunctionCall},
     prover_function_heuristics::ProverFunction,
-    symbolic_expression::{BinaryOperator, SymbolicExpression, UnaryOperator},
     variable::Variable,
 };
 
@@ -669,16 +669,15 @@ mod tests {
 
     use powdr_ast::analyzed::AlgebraicReference;
     use powdr_ast::analyzed::FunctionValueDefinition;
+    use powdr_constraint_solver::range_constraint::RangeConstraint;
     use pretty_assertions::assert_eq;
     use test_log::test;
 
     use powdr_number::GoldilocksField;
 
-    use crate::witgen::jit::effect::BitDecompositionComponent;
     use crate::witgen::jit::prover_function_heuristics::QueryType;
     use crate::witgen::jit::variable::Cell;
     use crate::witgen::jit::variable::MachineCallVariable;
-    use crate::witgen::range_constraints::RangeConstraint;
 
     use super::*;
 

executor/src/witgen/jit/debug_formatter.rs

@@ -3,12 +3,10 @@ use powdr_ast::analyzed::{
     AlgebraicBinaryOperation, AlgebraicBinaryOperator, AlgebraicExpression as Expression,
     AlgebraicUnaryOperation, PolynomialIdentity, SelectedExpressions,
 };
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 use powdr_number::FieldElement;
 
-use crate::witgen::{
-    data_structures::identity::{BusSend, Identity},
-    range_constraints::RangeConstraint,
-};
+use crate::witgen::data_structures::identity::{BusSend, Identity};
 
 use super::{
     variable::Variable,

executor/src/witgen/jit/effect.rs

@@ -1,17 +1,20 @@
-use std::fmt::Formatter;
-use std::{cmp::Ordering, fmt::Display};
-
-use std::{fmt, iter};
+use std::cmp::Ordering;
+use std::hash::Hash;
+use std::iter;
 
 use bit_vec::BitVec;
 use itertools::Itertools;
 use powdr_ast::indent;
+use powdr_constraint_solver::effect::{
+    Assertion, BitDecomposition, BitDecompositionComponent, BranchCondition,
+};
+use powdr_constraint_solver::symbolic_expression::SymbolicExpression;
 use powdr_number::FieldElement;
-use std::hash::Hash;
 
-use crate::witgen::range_constraints::RangeConstraint;
+use powdr_constraint_solver::effect::Effect as ConstraintSolverEffect;
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 
-use super::{symbolic_expression::SymbolicExpression, variable::Variable};
+use super::variable::Variable;
 
 /// The effect of solving a symbolic equation.
 #[derive(Clone, PartialEq, Eq)]
@@ -32,6 +35,29 @@ pub enum Effect<T: FieldElement, V> {
     Branch(BranchCondition<T, V>, Vec<Effect<T, V>>, Vec<Effect<T, V>>),
 }
 
+impl<T: FieldElement, V: Clone> From<ConstraintSolverEffect<T, V>> for Effect<T, V> {
+    fn from(effect: ConstraintSolverEffect<T, V>) -> Self {
+        match effect {
+            ConstraintSolverEffect::Assignment(v, expr) => Effect::Assignment(v, expr),
+            ConstraintSolverEffect::RangeConstraint(v, range) => Effect::RangeConstraint(v, range),
+            ConstraintSolverEffect::BitDecomposition(bit_decomp) => {
+                Effect::BitDecomposition(bit_decomp)
+            }
+            ConstraintSolverEffect::Assertion(assertion) => Effect::Assertion(assertion),
+            ConstraintSolverEffect::ConditionalAssignment {
+                variable,
+                condition,
+                in_range_value,
+                out_of_range_value,
+            } => Effect::Branch(
+                condition,
+                vec![Effect::Assignment(variable.clone(), in_range_value)],
+                vec![Effect::Assignment(variable, out_of_range_value)],
+            ),
+        }
+    }
+}
+
 impl<T: FieldElement> Effect<T, Variable> {
     /// Returns an iterator over all variables written to in the effect.
     /// The flag indicates if the variable is the return value of a machine call and thus needs
@@ -94,79 +120,6 @@ impl<T: FieldElement, V: Hash + Eq> Effect<T, V> {
     }
 }
 
-/// A bit decomposition of a value.
-/// Executing this effect solves the following equation:
-/// value = sum_{i=0}^{components.len() - 1} (-1)**components[i].negative * 2**components[i].exponent * components[i].variable
-///
-/// This effect can only be created if the equation has a unique solution.
-/// It might be that it leads to a contradiction, which should result in an assertion failure.
-#[derive(Clone, PartialEq, Eq)]
-pub struct BitDecomposition<T: FieldElement, V> {
-    /// The value that is decomposed.
-    pub value: SymbolicExpression<T, V>,
-    /// The components of the decomposition.
-    pub components: Vec<BitDecompositionComponent<T, V>>,
-}
-
-/// A component in the bit decomposition.
-/// In a simplified form, we can solve for `variable` using
-/// `(value & bit_mask) >> exponent`.
-#[derive(Clone, PartialEq, Eq)]
-pub struct BitDecompositionComponent<T: FieldElement, V> {
-    /// The variables that will be assigned to.
-    pub variable: V,
-    /// If the variable occurs negatively in the equation.
-    /// Note that the range constraint of the variable itself is always non-negative.
-    pub is_negative: bool,
-    /// The exponent of two, which forms the coefficient of the variable.
-    pub exponent: u64,
-    /// The bit mask for this component, relative to the value to be decomposed,
-    /// i.e. already scaled by the coefficient.
-    pub bit_mask: T::Integer,
-}
-
-/// A run-time assertion. If this fails, we have conflicting constraints.
-#[derive(Clone, PartialEq, Eq)]
-pub struct Assertion<T: FieldElement, V> {
-    pub lhs: SymbolicExpression<T, V>,
-    pub rhs: SymbolicExpression<T, V>,
-    /// If this is true, we assert that both sides are equal.
-    /// Otherwise, we assert that they are different.
-    pub expected_equal: bool,
-}
-
-impl<T: FieldElement, V> Assertion<T, V> {
-    pub fn assert_is_zero(condition: SymbolicExpression<T, V>) -> Effect<T, V> {
-        Self::assert_eq(condition, SymbolicExpression::from(T::from(0)))
-    }
-    pub fn assert_is_nonzero(condition: SymbolicExpression<T, V>) -> Effect<T, V> {
-        Self::assert_neq(condition, SymbolicExpression::from(T::from(0)))
-    }
-    pub fn assert_eq(lhs: SymbolicExpression<T, V>, rhs: SymbolicExpression<T, V>) -> Effect<T, V> {
-        Effect::Assertion(Assertion {
-            lhs,
-            rhs,
-            expected_equal: true,
-        })
-    }
-    pub fn assert_neq(
-        lhs: SymbolicExpression<T, V>,
-        rhs: SymbolicExpression<T, V>,
-    ) -> Effect<T, V> {
-        Effect::Assertion(Assertion {
-            lhs,
-            rhs,
-            expected_equal: false,
-        })
-    }
-}
-
-#[derive(Clone, PartialEq, Eq)]
-pub struct BranchCondition<T: FieldElement, V> {
-    pub value: SymbolicExpression<T, V>,
-    pub condition: RangeConstraint<T>,
-}
-
 #[derive(Clone, PartialEq, Eq)]
 pub struct ProverFunctionCall<V> {
     /// Which variables to assign the result to.
@@ -257,31 +210,9 @@ fn format_condition<T: FieldElement>(
     }
 }
 
-impl<T: FieldElement, V: Display> Display for BitDecomposition<T, V> {
-    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
-        let BitDecomposition { value, components } = self;
-        write!(f, "{} := {value};", components.iter().format(" + "))
-    }
-}
-
-impl<T: FieldElement, V: Display> Display for BitDecompositionComponent<T, V> {
-    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
-        let BitDecompositionComponent {
-            variable,
-            is_negative,
-            exponent,
-            bit_mask: _,
-        } = self;
-        write!(
-            f,
-            "{}2**{exponent} * {variable}",
-            if *is_negative { "-" } else { "" },
-        )
-    }
-}
-
 #[cfg(test)]
 mod test {
+    use powdr_constraint_solver::effect::BranchCondition;
     use powdr_number::GoldilocksField;
 
     use crate::witgen::jit::variable::Cell;

executor/src/witgen/jit/function_cache.rs

@@ -2,6 +2,7 @@ use std::{collections::HashMap, hash::Hash};
 
 use bit_vec::BitVec;
 use itertools::Itertools;
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 use powdr_number::{FieldElement, KnownField};
 
 use crate::witgen::{
@@ -11,7 +12,6 @@ use crate::witgen::{
         profiling::{record_end, record_start},
         LookupCell, MachineParts,
     },
-    range_constraints::RangeConstraint,
     EvalError, FixedData, MutableState, QueryCallback,
 };
 

executor/src/witgen/jit/identity_queue.rs

@@ -10,15 +10,14 @@ use powdr_ast::{
     },
     parsed::visitor::{AllChildren, Children},
 };
+use powdr_constraint_solver::{
+    quadratic_symbolic_expression::QuadraticSymbolicExpression, variable_update::VariableUpdate,
+};
 use powdr_number::FieldElement;
 
 use crate::witgen::{data_structures::identity::Identity, jit::variable::MachineCallVariable};
 
-use super::{
-    prover_function_heuristics::ProverFunction,
-    quadratic_symbolic_expression::QuadraticSymbolicExpression, variable::Variable,
-    variable_update::VariableUpdate,
-};
+use super::{prover_function_heuristics::ProverFunction, variable::Variable};
 
 /// Keeps track of identities that still need to be processed and
 /// updates this list based on the occurrence of updated variables

executor/src/witgen/jit/interpreter.rs

@@ -1,25 +1,28 @@
-use super::effect::{
-    Assertion, BitDecomposition, BitDecompositionComponent, BranchCondition, Effect,
-    ProverFunctionCall,
-};
+use std::cmp::Ordering;
+use std::collections::{BTreeSet, HashMap};
+use std::sync::Arc;
 
+use itertools::Itertools;
+
+use powdr_ast::analyzed::{PolyID, PolynomialType};
+use powdr_constraint_solver::effect::{
+    Assertion, BitDecomposition, BitDecompositionComponent, BranchCondition,
+};
+use powdr_constraint_solver::symbolic_expression::{
+    BinaryOperator, SymbolicExpression, UnaryOperator,
+};
+use powdr_number::{FieldElement, LargeInt};
+use powdr_pil_analyzer::evaluator::{self, Definitions, Value};
+
+use super::effect::{Effect, ProverFunctionCall};
 use super::prover_function_heuristics::{ProverFunction, ProverFunctionComputation};
-use super::symbolic_expression::{BinaryOperator, SymbolicExpression, UnaryOperator};
 use super::variable::{Cell, Variable};
+
 use crate::witgen::data_structures::finalizable_data::CompactDataRef;
 use crate::witgen::data_structures::mutable_state::MutableState;
 use crate::witgen::machines::LookupCell;
 use crate::witgen::{FixedData, QueryCallback};
 
-use itertools::Itertools;
-use powdr_ast::analyzed::{PolyID, PolynomialType};
-use powdr_number::{FieldElement, LargeInt};
-use powdr_pil_analyzer::evaluator::{self, Definitions, Value};
-
-use std::cmp::Ordering;
-use std::collections::{BTreeSet, HashMap};
-use std::sync::Arc;
-
 /// Interpreter for instructions compiled from witgen effects.
 pub struct EffectsInterpreter<'a, T: FieldElement> {
     var_count: usize,

executor/src/witgen/jit/mod.rs

@@ -1,4 +1,3 @@
-mod algebraic_to_quadratic;
 mod block_machine_processor;
 pub(crate) mod code_cleaner;
 mod compiler;
@@ -9,11 +8,8 @@ mod identity_queue;
 mod interpreter;
 mod processor;
 mod prover_function_heuristics;
-mod quadratic_symbolic_expression;
 mod single_step_processor;
-mod symbolic_expression;
 mod variable;
-mod variable_update;
 pub(crate) mod witgen_inference;
 
 #[cfg(test)]

executor/src/witgen/jit/processor.rs

@@ -2,21 +2,23 @@ use std::fmt::{self, Display, Formatter, Write};
 
 use itertools::Itertools;
 use powdr_ast::analyzed::{AlgebraicExpression, PolynomialIdentity};
+use powdr_constraint_solver::range_constraint::RangeConstraint;
+use powdr_constraint_solver::{
+    quadratic_symbolic_expression::{self, QuadraticSymbolicExpression},
+    variable_update::VariableUpdate,
+};
 use powdr_number::FieldElement;
 
 use crate::witgen::{
     data_structures::identity::{BusSend, Identity},
     jit::debug_formatter::format_polynomial_identities,
-    range_constraints::RangeConstraint,
 };
 
 use super::{
     debug_formatter::format_incomplete_bus_sends,
     effect::{format_code, Effect},
     identity_queue::{IdentityQueue, QueueItem},
-    quadratic_symbolic_expression::{self, QuadraticSymbolicExpression},
     variable::{MachineCallVariable, Variable},
-    variable_update::VariableUpdate,
     witgen_inference::{
         variable_to_quadratic_symbolic_expression, BranchResult, CanProcessCall, FixedEvaluator,
         WitgenInference,

executor/src/witgen/jit/single_step_processor.rs

@@ -4,6 +4,7 @@ use itertools::Itertools;
 use powdr_ast::analyzed::{
     AlgebraicExpression as Expression, AlgebraicReference, ContainsNextRef, PolyID, PolynomialType,
 };
+use powdr_constraint_solver::quadratic_symbolic_expression::QuadraticSymbolicExpression;
 use powdr_number::FieldElement;
 
 use crate::witgen::{machines::MachineParts, FixedData};
@@ -13,7 +14,6 @@ use super::{
     identity_queue::QueueItem,
     processor::{algebraic_expression_to_queue_items, Processor},
     prover_function_heuristics::decode_prover_functions,
-    quadratic_symbolic_expression::QuadraticSymbolicExpression,
     variable::{Cell, Variable},
     witgen_inference::{CanProcessCall, FixedEvaluator, WitgenInference},
 };

executor/src/witgen/jit/witgen_inference.rs

@@ -6,6 +6,15 @@ use std::{
 use bit_vec::BitVec;
 use itertools::Itertools;
 use powdr_ast::analyzed::{AlgebraicExpression as Expression, AlgebraicReference};
+use powdr_constraint_solver::{
+    algebraic_to_quadratic::algebraic_expression_to_quadratic_symbolic_expression,
+    effect::BranchCondition,
+    quadratic_symbolic_expression::{
+        Error, ProcessResult, QuadraticSymbolicExpression, RangeConstraintProvider,
+    },
+    range_constraint::RangeConstraint,
+    symbolic_expression::SymbolicExpression,
+};
 use powdr_number::FieldElement;
 
 use crate::witgen::{
@@ -14,17 +23,12 @@ use crate::witgen::{
         mutable_state::MutableState,
     },
     global_constraints::RangeConstraintSet,
-    jit::symbolic_expression::SymbolicExpression,
-    range_constraints::RangeConstraint,
     FixedData, QueryCallback,
 };
 
 use super::{
-    algebraic_to_quadratic::algebraic_expression_to_quadratic_symbolic_expression,
-    effect::{BranchCondition, Effect, ProverFunctionCall},
+    effect::{Effect, ProverFunctionCall},
     prover_function_heuristics::ProverFunction,
-    quadratic_symbolic_expression::{Error, ProcessResult},
-    quadratic_symbolic_expression::{QuadraticSymbolicExpression, RangeConstraintProvider},
     variable::{Cell, MachineCallVariable, Variable},
 };
 
@@ -173,8 +177,8 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
         bus_send: &BusSend<T>,
         row_offset: i32,
     ) -> Result<Vec<Variable>, Error> {
-        let result = self.process_call_inner(can_process_call, bus_send, row_offset);
-        self.ingest_effects(result, Some((bus_send.identity_id, row_offset)))
+        let (effects, complete) = self.process_call_inner(can_process_call, bus_send, row_offset);
+        self.ingest_effects(effects, complete, Some((bus_send.identity_id, row_offset)))
     }
 
     /// Process a prover function on a row, i.e. determine if we can execute it and if it will
@@ -217,13 +221,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
             row_offset,
             inputs,
         });
-        self.ingest_effects(
-            ProcessResult {
-                effects: vec![effect],
-                complete: true,
-            },
-            None,
-        )
+        self.ingest_effects(vec![effect], true, None)
     }
 
     /// Set a variable to a fixed value.
@@ -237,8 +235,9 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
         &mut self,
         equation: &QuadraticSymbolicExpression<T, Variable>,
     ) -> Result<Vec<Variable>, Error> {
-        let result = equation.solve(self)?;
-        self.ingest_effects(result, None)
+        let ProcessResult { effects, complete } = equation.solve(self)?;
+        let effects = effects.into_iter().map(Into::into).collect();
+        self.ingest_effects(effects, complete, None)
     }
 
     fn process_call_inner(
@@ -246,19 +245,16 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
         can_process_call: impl CanProcessCall<T>,
         bus_send: &BusSend<T>,
         row_offset: i32,
-    ) -> ProcessResult<T, Variable> {
+    ) -> (Vec<Effect<T, Variable>>, bool) {
         // We need to know the selector and bus ID.
         let (Some(selector), Some(bus_id)) = (
             self.try_evaluate_to_known_number(&bus_send.selected_payload.selector, row_offset),
             self.try_evaluate_to_known_number(&bus_send.bus_id, row_offset),
         ) else {
-            return ProcessResult::empty();
+            return (vec![], false);
         };
         if selector == 0.into() {
-            return ProcessResult {
-                effects: vec![],
-                complete: true,
-            };
+            return (vec![], true);
         } else {
             assert_eq!(selector, 1.into(), "Selector is non-binary");
         }
@@ -289,10 +285,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
         if can_process {
             effects.push(Effect::MachineCall(bus_id, known, arguments.to_vec()));
         }
-        ProcessResult {
-            effects,
-            complete: can_process,
-        }
+        (effects, can_process)
     }
 
     /// Analyze the effects and update the internal state.
@@ -301,11 +294,12 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
     /// Returns the variables that have been updated.
     fn ingest_effects(
         &mut self,
-        process_result: ProcessResult<T, Variable>,
+        effects: Vec<Effect<T, Variable>>,
+        complete: bool,
         identity_id: Option<(u64, i32)>,
     ) -> Result<Vec<Variable>, Error> {
         let mut updated_variables = vec![];
-        for e in process_result.effects {
+        for e in effects {
             match &e {
                 Effect::Assignment(variable, assignment) => {
                     // If the variable was determined to be a constant, we add this
@@ -367,7 +361,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
                     // multiple times to get better range constraints.
                     if self.complete_calls.insert(identity_id.unwrap()) {
                         log::trace!("Machine call: {:?}", identity_id.unwrap());
-                        assert!(process_result.complete);
+                        assert!(complete);
                         for v in vars {
                             // Inputs are already known, but it does not hurt to add all of them.
                             if self.record_known(v.clone()) {
@@ -381,7 +375,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
                 Effect::Branch(..) => unreachable!(),
             }
         }
-        if process_result.complete {
+        if complete {
             // If a machine call is complete because its selector is zero,
             // we will not get an `Effect::MachineCall` above and need to
             // insert here.
@@ -550,10 +544,7 @@ mod test {
 
     use crate::witgen::{
         global_constraints,
-        jit::{
-            algebraic_to_quadratic::algebraic_expression_to_quadratic_symbolic_expression,
-            effect::format_code, test_util::read_pil, variable::Cell,
-        },
+        jit::{effect::format_code, test_util::read_pil, variable::Cell},
         machines::{FixedLookup, KnownMachine},
         FixedData,
     };

executor/src/witgen/machines/block_machine.rs

@@ -16,7 +16,6 @@ use crate::witgen::global_constraints::RangeConstraintSet;
 use crate::witgen::jit::function_cache::FunctionCache;
 use crate::witgen::jit::witgen_inference::CanProcessCall;
 use crate::witgen::processor::{OuterQuery, Processor, SolverState};
-use crate::witgen::range_constraints::RangeConstraint;
 use crate::witgen::rows::{Row, RowIndex};
 use crate::witgen::sequence_iterator::{
     DefaultSequenceIterator, ProcessingSequenceCache, ProcessingSequenceIterator,
@@ -25,7 +24,9 @@ use crate::witgen::util::try_to_simple_poly;
 use crate::witgen::AffineExpression;
 use crate::witgen::{machines::Machine, EvalError, EvalValue, IncompleteCause, QueryCallback};
 use bit_vec::BitVec;
+
 use powdr_ast::analyzed::{DegreeRange, PolyID, PolynomialType};
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 use powdr_number::{DegreeType, FieldElement};
 
 enum ProcessResult<'a, T: FieldElement> {

executor/src/witgen/machines/double_sorted_witness_machine_16.rs

@@ -3,6 +3,7 @@ use std::iter::once;
 
 use bit_vec::BitVec;
 use itertools::Itertools;
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 
 use super::{LookupCell, Machine, MachineParts};
 use crate::witgen::data_structures::caller_data::CallerData;
@@ -11,7 +12,6 @@ use crate::witgen::global_constraints::RangeConstraintSet;
 use crate::witgen::jit::witgen_inference::CanProcessCall;
 use crate::witgen::machines::compute_size_and_log;
 use crate::witgen::processor::OuterQuery;
-use crate::witgen::range_constraints::RangeConstraint;
 use crate::witgen::util::try_to_simple_poly;
 use crate::witgen::{
     AffineExpression, AlgebraicVariable, EvalError, EvalResult, FixedData, QueryCallback,

executor/src/witgen/machines/double_sorted_witness_machine_32.rs

@@ -11,16 +11,15 @@ use crate::witgen::global_constraints::RangeConstraintSet;
 use crate::witgen::jit::witgen_inference::CanProcessCall;
 use crate::witgen::machines::compute_size_and_log;
 use crate::witgen::processor::OuterQuery;
-use crate::witgen::range_constraints::RangeConstraint;
 use crate::witgen::util::try_to_simple_poly;
 use crate::witgen::{
     AffineExpression, AlgebraicVariable, EvalError, EvalResult, EvalValue, FixedData,
     IncompleteCause, QueryCallback,
 };
 
-use powdr_number::{DegreeType, FieldElement, LargeInt};
-
 use powdr_ast::analyzed::{DegreeRange, PolyID};
+use powdr_constraint_solver::range_constraint::RangeConstraint;
+use powdr_number::{DegreeType, FieldElement, LargeInt};
 
 /// If all witnesses of a machine have a name in this list (disregarding the namespace),
 /// we'll consider it to be a double-sorted machine.

executor/src/witgen/machines/fixed_lookup_machine.rs

@@ -5,6 +5,7 @@ use std::mem;
 
 use itertools::{Either, Itertools};
 use powdr_ast::analyzed::{AlgebraicExpression, PolyID, PolynomialType};
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 use powdr_number::FieldElement;
 
 use crate::witgen::affine_expression::{AffineExpression, AlgebraicVariable};
@@ -14,7 +15,6 @@ use crate::witgen::data_structures::mutable_state::MutableState;
 use crate::witgen::global_constraints::{GlobalConstraints, RangeConstraintSet};
 use crate::witgen::jit::witgen_inference::CanProcessCall;
 use crate::witgen::processor::OuterQuery;
-use crate::witgen::range_constraints::RangeConstraint;
 use crate::witgen::util::try_to_simple_poly;
 use crate::witgen::{EvalError, EvalValue, IncompleteCause, QueryCallback};
 use crate::witgen::{EvalResult, FixedData};

executor/src/witgen/machines/mod.rs

@@ -5,6 +5,7 @@ use bit_vec::BitVec;
 use dynamic_machine::DynamicMachine;
 use powdr_ast::analyzed::{self, ContainsNextRef, DegreeRange, PolyID};
 
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 use powdr_number::DegreeType;
 use powdr_number::FieldElement;
 
@@ -22,7 +23,6 @@ use self::write_once_memory::WriteOnceMemory;
 use super::data_structures::identity::{BusReceive, Identity};
 use super::global_constraints::RangeConstraintSet;
 use super::jit::witgen_inference::CanProcessCall;
-use super::range_constraints::RangeConstraint;
 use super::{AffineExpression, AlgebraicVariable, EvalError, EvalResult, FixedData, QueryCallback};
 
 mod block_machine;

executor/src/witgen/mod.rs

@@ -41,7 +41,6 @@ mod machines;
 mod multiplicity_column_generator;
 mod processor;
 mod query_processor;
-mod range_constraints;
 mod rows;
 mod sequence_iterator;
 mod util;

executor/src/witgen/rows.rs

@@ -6,6 +6,7 @@ use std::{
 
 use itertools::Itertools;
 use powdr_ast::analyzed::{AlgebraicExpression as Expression, AlgebraicReference, PolyID};
+use powdr_constraint_solver::range_constraint::RangeConstraint;
 use powdr_number::{DegreeType, FieldElement};
 
 use crate::witgen::Constraint;
@@ -16,7 +17,6 @@ use super::{
     evaluators::symbolic_witness_evaluator::{SymbolicWitnessEvaluator, WitnessColumnEvaluator},
     global_constraints::RangeConstraintSet,
     machines::MachineParts,
-    range_constraints::RangeConstraint,
     FixedData, PartialExpressionEvaluator,
 };