Add lowerings from smt tensor to low-level smt

[Hatsunespica]

This PR adds two new files:
rewrite_smt_tensor.py
This file matches the pattern (extract (op args) indices) to (extract tensor' indicts')

For example: (extract (transpose T) x y) -> (extract T y x)

More patterns will be added in some next PRs. The only pattern included in this PR is for transposition served as an example usage.

lower_smt_tensor.py
This file lowers a smt_tensor type into smt_arrry type which is <X, <Y, elementType>>

For example: smt_tensor<2x2xi8> -> <IndexType, <IndexType, bv<8>> while IndexType is a bv<64> type defined in `smt_tensor_dialect

Next, it lowers TensorExtractOp as a chain of indices applications.

---

For the next PR, I want to add refine_tensor_semantics in xdsl-smt and provide test cases over there.
Do you think it's a good idea?

[math-fehr]

Can you split this PR in two different PRs (one for the lowering, and one for the optimizations).
Also, can you add tests for these?

[math-fehr]

Is there a reason this file doesn't use the SMTLowerer and use the OperationSemantics class?

[math-fehr]

I would either pass this dictionary to the RewritePattern, or I would use the CSE pass after the pattern rewriter is done.
Having a global variable will mess things up if you run the pass multiple time

[math-fehr]

Actually, I would just use CSE after the pass, that should be fast enough.

[math-fehr]

I would not use that class, I would instead use @dataclass on all the other subclasses and just have the variable there

[math-fehr]

I would change this logic here to just have a single rewrite pattern that matches a TensorExtractOp of TensorTransposeOp.
I would not try to add abstractions that early, that complexifies the code.

[Hatsunespica]

Can you split this PR in two different PRs (one for the lowering, and one for the optimizations). Also, can you add tests for these?

Hi Mathieu, this PR is only for lowerings without any optimizations.
It provides lowerings from tensor to smt_array.
And the next PR is about tensor_refinemnet in xdsl-smt

[math-fehr]

But xdsl_smt/passes/rewrite_smt_tensor.py is a file only containing optimizations right?

[Hatsunespica]

But xdsl_smt/passes/rewrite_smt_tensor.py is a file only containing optimizations right?

Nope, it's not for optimization, but a part of verification.

Here is an example:
To verify

T(T(x)) == x

let's find indices where 
T(T(x))[i, j] != x[i, j]
    |
  ( Rewrite Tensor)
   |
  V
T(x)[j, i] != x[i, j]
    |
  ( Rewrite Tensor)
   |
  V
x[i, j] != x[i, j]
    |
  ( Lower Tensor)
   |
  V
  apply(smt_array(x), i, j) != apply(smt_array(x), i, j))
unsat

tensosr_refinement (that is not in this PR) instantiates indices [i, j] and adds element accessor on both sides.
rewrite tensor keeps rewriting operation with an element accessor with another accessor until reach the simplest form
lower tensor lowers element accessor and tensor to smt_array and apply operations.