| ▲ | dgan 3 days ago | |
Do modern compiler (register allocation/ instruction generation) involve some kind of integer programming or constraint solving? I vaguely remember compilers using Z3 solver | ||
| ▲ | ngruhn 3 days ago | parent [-] | |
Many use Z3 for type checking like F*, Liquid Haskell, Dafny. | ||