Efficient support for bv128

[yannickmoy]

Describe the bug

Neither CVC4 nor CVC5 seem to be able to solve efficiently VCs that involve bv128. For example, both CVC4 and CVC5 take 3 minutes to solve that VC:

(set-logic AUFBVFPDTNIRA)
(set-info :smt-lib-version 2.6)
(declare-const x (_ BitVec 128))
(declare-const s (_ BitVec 128))
(declare-const s1 (_ BitVec 128))
(assert (bvule s #x00000000000000000000000000000080))
(assert (bvule s1 #x00000000000000000000000000000080))
(assert (not (= (bvshl (bvshl x s) s1) (bvshl x (bvadd s s1)))))
(check-sat)

and they do not seem to solve at all this other one:

(set-logic AUFBVFPDTNIRA)
(set-info :smt-lib-version 2.6)
(declare-const x (_ BitVec 64))
(assert
  (not
  (= (* 18446744073709551616 (bv2nat ((_ zero_extend 64) x)))
     (bv2nat (bvmul #x00000000000000010000000000000000 ((_ zero_extend 64) x))))
  ))
(check-sat)

Are there options for either one that would improve the situation here?

Command line arguments: none cvc5 version/commit: cvc5 version 0.0.3 Operating system: Ubuntu 20.04.3 LTS

configure.sh options
Binary release from GitHub.

configure.sh output
Binary release from GitHub.

[mpreiner]

@yannickmoy are these constraints you regularly encounter in your problems or just one test case where cvc5 is slow?

As for using bv2nat: I'd suggest to avoid bv2nat as much as possible since the conversion is expensive and not very efficient (at least for now). In the second example you can avoid bv2nat by adding the integer bounds for and Int x instead of using zero_extend.

[yannickmoy]

@mpreiner this comes from a proof of a unit which implements operations over 128 bits integers using 64 bits integers. Many VCs become either unprovable or very slow compared to the same unit with 64/32 bits combination. Here are two VCs which I simplified to the minimum, but in fact dozens are much more complex and I was expecting that getting faster support for the simpler VCs would also benefit the complex ones.

The use of bv2nat and zero_extend really come from our encoding of program semantics, so cannot be easily removed:

• bv2nat is called when going to mathematical integers in specifications, which is necessary here
• zero_extend is called when converting from 64 bits to 128 bits, which is also inherent to the code here

Thanks for answering, even if there is no expected improvement to expect on these in the short/medium term!

[ajreynol]

Moving this to cvc5-projects.

[martin-cs]

@yannickmoy I might be able to help with the bit-vector multiply but as @mpreiner says, it is going to be hard to handle anything with bv2nat in because this requires reasoning across different theories. cvc5 does have conversions from BV to Int and vica versa which might help.

[yannickmoy]

@martin-cs are the conversions between BV and Int automatically activated when using bv2nat, or should we use special functions in the VC?