Your take seems to contradict the article? You say SMT solvers give "no control over ISA/intrinsic level decisions" but their design.md says "user-defined sched

Your take seems to contradict the article? You say SMT solvers give "no control over ISA/intrinsic level decisions" but their design.md says "user-defined scheduling operations can encapsulate common optimization patterns and hardware-specific transformations". Are they wrong about this? Can you explain why?