However, I think you can still get a lot of value if you just use Z3 as a constraint solver to verify that your subsystems satisfy robot rules (like not using too many PDP slots). I’ve had a few close calls when integrating things late in the build.
I actually think this is harder to some extent. It’s not clear to me how to best model time to location as a distribution instead of just a static number. My examples explicitly excluded defense (and implicitly excluded robots breaking) for this reason.
If you have any ideas on how to improve in this area, please reach out.
The original goal of this research was actually to combine the robot design and match strategy models, such that your robot design optimizer was maximizing points scored across an alliance.
One of Z3’s limitations is that it does not like working with exponential functions. Unfortunately, if you want to optimize the sprint distance to a particular location with FRC motors, physics gives you an exponential function to solve. I tried a few Taylor series approximations but the approximation error became high very quickly.
It also blows up the search space by a lot.