title: Z3: Performing Matrix Operations
body: <h2>My Situation</h2>
  <p>I'm working on a project which needs to:</p>
  <ul>
  <li>Prove the correctness of <a href="http://rodrigo-silveira.com/3d-programming-transformation-matrix-tutorial/#.UU65YicWsYZ" rel="noreferrer">3D matrix transformation</a> formulas involving matrix operations</li>
  <li>Find a model with the values of the unknown matrix entries.</li>
  </ul>
  <h2>My Question</h2>
  <ul>
  <li>What's the best way to express formulas using matrix operations so
  that they can be solved by <code>z3</code>? (The way used in <a href="http://rise4fun.com/z3py/tutorialcontent/guide#h210" rel="noreferrer">Z3Py's Sudoku
  Example</a> isn't
  very elegant and doesn't seem suitable for more complex matrix
  operations.)</li>
  </ul>
  <p>Thanks. - If anything's unclear, please leave a question comment.</p>