search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
180 stars 46 forks source link

Add rotation operations to BitvectorFormulaManager #362

Closed leventeBajczi closed 6 months ago

leventeBajczi commented 6 months ago

As discussed in https://github.com/sosy-lab/java-smt/issues/360, this PR ~adds~ enhances the rotateRight and rotateLeft operations in the bitvector formula manager.

I added implementations for solvers that do not directly support rotation-by-bitvector, by using shift operations. Therefore, all bitvector-supporting solvers can also use rotation now.

leventeBajczi commented 6 months ago

All tests seem to pass, but Princess is very slow in the bvRotateByBV test. Maybe it is worth disabling that test for Princess as to not make testing take too long (and bvIsIdenticalAfterFullRotation tests Princess's rotation capabilities to some degree)

leventeBajczi commented 6 months ago

Yes, even in the AppVeyor the test experienced a timeout with princess. I'll disable it.

kfriedberger commented 6 months ago

The idea to use mod/rem for computing the shift is very good. I adapted your solution and applied it in 12ceedfa6a.

Princess is quite slow for BV theory, and BV-rotation seems to be beyond its limits, for now.

I will close this PR without merging.