Antimonotonicity of division

[Viktor Kunčak]

Dear SMT community,

I teach my MSc students about the many virtues of SMT solvers and advantages of their algebraic reasoning, but recently students come back asking me about the surprising limitations in bitvector reasoning, in particular when it comes to properties that carry over from the fact that bitvectors are integers modulo 2^N and thus many algebraic laws do carry over, even if conditionally.

For example, I am trying the following example

(set-logic QF_UFBV)
(declare-fun a () (_ BitVec 32))
(declare-fun b1 () (_ BitVec 32))
(declare-fun b2 () (_ BitVec 32))
(assert (and (bvslt #b00000000000000000000000000000000 a)
             (bvslt #b00000000000000000000000000000000 b1)
             (bvsle b1 b2)
             (bvsgt (bvsdiv a b2) (bvsdiv a b1))))

(check-sat)

which arises from trying to prove:

  def divAntimonotonic(a: Int, b1: Int, b2: Int) : Unit = {
    require(0 < a && 0 < b1 && b1 <= b2)
    ()
  } ensuring(_ => a / b2 <= a / b1)

I suppose that this is not in the library of standard BV pre-processing rewrites because it is a conditional fact that only works for positive b1,b2 ?

Are you aware of any solver options or nightly versions that would work on this smt2 file? cvc4 1.8 and z3 4.8.10 with default core seem to both time out?

Thanks,

  Viktor

[Yannick Moy]

Hi Viktor,

In our experience with SPARK, it's very common that SMT solvers (we use Alt-Ergo, CVC4 and Z3) don't solve non-linear VCs, both in integers and bitvectors. We have developed lemmas that users can call instead, that we prove either automatically (because the context is simpler) or manually (with Coq), like these: https://github.com/AdaCore/spark2014/blob/master/include/spark-mod_arithmetic_lemmas.ads

Just today, one of our customers sent a code they could not get any prover to prove, involving division and multiplication on integers (translated as integers or bitvectors in the VC depending on the prover), but suitably guarded so that there is no overflow, like in your example. The usual monotonicity rules of arithmetic apply in such a case, but provers have a hard time using that. We could get it to prove automatically by proving the same property in integers, and deduce automatically that the same holds in bitvectors, using the combination of three provers.

Another option for such VCs which contain non-linear arithmetic and/or a combination of arithmetic theories, is to use a constraint solver like COLIBRI, which solves your goal immediately. We're currently adding it to the list of our supported provers.

Hope that helps

--

Yannick

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAOaq1xcuVLRRN%2BwLkcRKTU7bD9B%2BkWM6KzQ923N18Y_qZMeoZQ%40mail.gmail.com.