Sirui Lu

The compilation result: https://lt128.godbolt.org/z/xEK6v4f6f.

Hi @AkashIwnK, thank you for your interest in Grisette. We currently do not have a tutorial like Rosette Guide, but we do have some examples which you can have a...

Hi @AkashIwnK, there is also a library for synthesis in Grisette under development at https://github.com/lsrcz/grisette-synth-lib if your focus is synthesis or super-optimization. An example is available at https://github.com/lsrcz/grisette-synth-lib/tree/development/arith.

Hi @eldritch-cookie, Yeah, I will be glad to add them. I still have plenty of stuff to do at this time, but I will put this into my todo list.

Hi @jan-wassenberg , I have just rerun the tests with clang-17.0.6 and a recent version of clang ([2ace7bd](https://github.com/llvm/llvm-project/tree/2ace7bdcfe640c69bd4dcf508d39485e0ef7ea06)), and they both failed the `SortTestGroup/SortTest.TestAllPartition/RVV` test. The `MatVecTestGroup/MatVecTest.TestAllMatVec/RVV` is no longer...

I am using the default flags, and I believe that it is `-march=rv64gcv1p0` after checking the generated `build.ninja`. However, I found that the test only fails when VLEN is 128....

Thanks. I tried the fa61572 commit, and it seems to work under VLEN=128/1024 on qemu.

Not working pre-ghc 9.6. Will come back to this later.

Already implemented in #214.

`SymAlgReal` has been added in #228, and `SymFP` has been added in #207.