wip: support non-indexed bit rotate where possible

[xeniarose]

This implements non-indexed bit rotation operations (i.e., where the amount to rotate by can be symbolic) for all solvers that support it (Z3, Bitwuzla), and falls back to the current behavior which reduces the bit rotates to bit shifts for all other solvers. See issue: #302

While Boolector nominally supports ext_rotate_{left,right}, I found that it segfaults when given SMT-LIB input containing these operations. It's unlikely that's going to ever be fixed, so the Boolector solver still uses the reduction to bit shifts.

Description of the changes:

• Lifts bvror and bvrol to their own operation types
• Add an new solver feature ext_rotate to solvers that support a bit rotation extension
• Add a new solver-custom-encode method to gen:solver which is threaded through enc and called when enc doesn't know how to encode something. base-solver lowers @bvrol and @bvror to bit shifts by default. Solvers with a bit rotation extension override the method to output their appropriate extension syntax. If neither enc nor the solver know how to encode something, it still raises the same error as before.
• Add both Z3's and Bitwuzla's form of the bit rotation extension to the decoder (ext_rotate_{left,right} and bvro{l,r}). These are hardcoded (instead of using a new gen:solver method as above), since the same decoding behavior works for all solvers.
• Add a simple test to ensure that SMT-LIB output is as expected for bit rotate operations on supported solvers

I ran the test suite with all the available solvers on my computer. The generic tests are passing, and the following solvers are working: Z3 (bundled version, 4.8.8), CVC4 (1.8), CVC5 (1.3.4), Bitwuzla (0.9.0), Boolector (3.2.4), Yices (2.7.0)

STP (2.3.4) tests are failing even on the current main branch (29808a0), so I'm unable to test with it. If there's a specific known working version of STP I can run the tests with that version.

I'm happy to make any required changes if a different implementation is desired or other fixes are needed