search

sosy-lab / java-smt

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

Bitvector rotations not included in FunctionDeclarationKind #397

Open daniel-raffler opened 4 hours ago

daniel-raffler commented 4 hours ago

Hello, we added bitvector rotation in commit 7c0e9f4a4536be8622ed51cdd25e4fd6c2779353 but support in FunctionDeclarationKind is still missing. This does cause problems when visitors are used over formulas that contain bitvector rotations. Most solver backends seem to treat rotation as a unknown symbol and return FunctionDeclarationKind.Other, but Bitwuzla actually crashes with the error message java.lang.UnsupportedOperationException: Can not discern formula kind BV_ROLI.

This issue is complicated by the fact that there are 4 different rotation operations and not all solvers support them natively. We currently use a workaround that tries to emulate missing operations, but that also means that the actual symbol will be missing in the formula. We need to figure out how to best handle such cases without making it too confusing for the user.

daniel-raffler commented 4 hours ago

I've opened a new branch (397-bitvector-rotations-not-included-in-functiondeclarationkind) and added some test for the issue