Unbounded shifts for (SInteger,SInteger)

[MrChico]

Hello again @LeventErkok, Some integer experiments led me to this error:

SBV.shiftRight: Not yet implemented unbounded/non-constants shifts for (SInteger,SInteger), please file a request!

So I will abide and kindly ask for shifts for SIntegers :)

[LeventErkok]

Unfortunately, there's no viable translation for unbounded-integer-shifts in SMTLib.

SMTLib only supports shifts for fixed-size bit-vectors. (http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml) The integer theory has no notion of shifts. (http://smtlib.cs.uiowa.edu/theories-Ints.shtml)

SBV tries to do its best when some of the arguments are constants and if it can get away with a translation to existing constructs. Unfortunately, when the second argument is symbolic, there's no corresponding SMTLib function to translate to. So, that's where it gives up and you get the message you got.

One way to handle this might be to write it as:

a `shift` b = ite (b >= 0) (a * (pow 2 b)) (a `sDiv` (pow 2 (- b)))

But the problem is that there's also no exponentiation operator in SMTLib. (http://smtlib.cs.uiowa.edu/theories-Ints.shtml).

So, that's where things stand; without a proper way to translate there isn't much we can do.

Note that if we just restrict ourselves to z3, then z3 does indeed have an exponentiation operator. (Currently not supported by SBV, but we can easily add support.) But doing that is unlikely to buy us anything, as it creates highly non-linear problems, and z3 is likely to say unknown and thus not really make any progress. Here's an example using the Python interface to z3.

>>> from z3 import *
>>> a, b = Ints("a b")
>>> s = Solver()
>>> s.add(a**b == 8)
>>> print (s.sexpr())
(declare-fun b () Int)
(declare-fun a () Int)
(assert (= (^ a b) 8))

>>> s.check()
unknown

So, even if we added similar support, it'd only "work" with z3, and you'll get unknown for even the simplest problems. My hunch is that whenever z3 can handle exponentiation is exactly the cases the SBV already supports (i.e., concrete exponent values), so I don't see this adding much value for the code-complexity it introduces.

If you've any other idea on how to translate unbounded shifts that works well with SMT-solvers, I'd like to hear. Without a good translation, it's rather moot to add a conversion that simply gives you unknown as answer.

But, perhaps more importantly, why do you need unbounded shifts? For any effective use of shifts, I'd suggest using bit-vectors; and you can also use sFromIntegral to convert unbounded integers to bit-vectors if necessary. (Though that can also create complicated problems for the backend solver.) If we know exactly what the use case for unbounded shifts are, you can come up with some other encoding. (Maybe you know the bounds on the second parameter? Then you can even convert it to a look-up table, assuming the bounds give you a small enough range.)

[MrChico]

Thanks for the extensive answer. I do see the problem, and it seems quite tricky to solve in the general case.

Luckily, I am in a setting where I have some upper bounds on the integer, so I should be able to make do with sFromIntegral to the appropriate bitvector. It is unfortunate that smt solvers are quite bad at this conversion, but that's the reality we live in I guess. Feel free to close this issue.

[LeventErkok]

If your variables have known bounds, it's always better to just stick to the corresponding bit-vector size from the very start. (BV-logic is always decidable, regardless of the presence of multiplication.) Best of luck!