Builds on #2695
In the in-liner, we black-listed any variables that appear in bus
interactions. I don't think this is necessary, and it prevents some
optimizations. But maybe I'm overlooking something. This has also been
[discussed in a previous
PR](https://github.com/powdr-labs/powdr/pull/2677#discussion_r2075080921).
This is the first step in allowing some optimizations, for example to
store a lookup table for the occurrences of variables and only
substituting in those constraints or keeping a queue of modified
constraints.
Adds bus interactions to the solver. See [this
test](215d04fc8b/constraint-solver/tests/solver.rs (L218-L239))
for an example!
The implementation is as follows:
- There is a new `BusInteraction` type, storing the bus ID, multiplicity
and payload. I also added a wrapper `ConstraintSystem` type, which
contains all algebraic constraints and bus interactions.
- `BusInteractions::solve()` has a similar interface to
`QuadraticSymbolicExpression::solve()`. It does the following steps:
- Converts the bus interaction's fields from expressions to range
constraints.
- Calls a `BusInteractionHandler` to update the range constraints
- Users of `Solver` can pass a bus interaction handler that knows how to
deal with the constraint system's buses. If none is provided, bus
interactions are ignored by the solver
[This](215d04fc8b/constraint-solver/tests/solver.rs (L121-L174))
is an example of an implementation of `BusInteractionHandler`. In the
future we could:
- Implement one for Powdr VMs, by detecting machine types. This would be
similar to [an implementation of
`Machine::can_process_call_fully`](215d04fc8b/executor/src/witgen/machines/fixed_lookup_machine.rs (L311)).
- Pass a custom implementation to the solver. For example, we might be
using the solver with single chips of a third-party VM. Then, the
handler would have to know how to handle all bus interactions available
to this chip.
Replace the mechanism of "variable update" by "substitutions". This has
the benefit that we can substitute a variable also by a more complex
value.
The next step (not this PR) would be to also allow substitution by QSEs,
which we will need if we want to apply equivalences.
I tried to implement the simplest possible solver as a starting point
for a solver that we can eventually use to simplify auto-precompiles (by
(1) trying to find concrete variable assignments already and (2) figure
out if two nodes can be computed using the same symbolic expression, and
hence can be collapsed).
I created #2652 to track follow-up work.
---------
Co-authored-by: Thibaut Schaeffer <schaeffer.thibaut@gmail.com>
Co-authored-by: chriseth <chris@ethereum.org>
Adds a quick-and-dirty way to return bit constraints when running
`QuadraticSymbolicExpression::solve()`, by looking for a specific
expression (`X * (X - 1)`). As far as I can see, this is orthogonal to
#2619, which would return a `Branch` effect instead of a range
constraint.
With this PR, we remove the need for "global range constraints". This
will help progressing on the new solver (#2651), which tries to rely
only on `QuadraticSymbolicExpression`. Then, we can have a bit
decomposition example even before implementing machine calls.
---------
Co-authored-by: chriseth <chris@ethereum.org>
