bv2int and int2bv slow?

[kren1]

I have two fairly complex string quires bitblast.txt and bv2int.txt.

They should be the same, except that bv2int.txt uses bv2int and int2bv and bitblast.txt uses ite expressions to bitblast for a couple of integers: 0,1,2,3,4,5,6,30 .

For me bitblast.txt terminates in under a second whereas bv2int.txt was running for 17hours, used 3.5GB of memory and then I gave up.

So I'm wondering if bv2int and int2bv are just not supported in this context?

I also tried with smt.string_solver=z3str3 , which returned unknown.

[kren1]

I did another experiment, it seems int2bv is the problematic one.

[OrenGitHub]

Here is a related query that returns unsat immediately:

(declare-const ibv (_ BitVec 32))

(assert (= -1 (bv2int ibv)))

(check-sat)
(get-value (ibv))

Since bv2int is uninterpreted, the "expected" value for ibv (=0x80000000)
can be "legally" missed.
I wonder if this "unsigned" behavior of bv2int is part of the reason why bv2int
is "faster" than int2bv (??)
This also appeared in a previous (now closed) issue

[OrenGitHub]

I'm attaching another example based on @kren1 's query where bv2int is probably unsafe to use
as z3 counts on its non-negativity:

(declare-const s String)
(declare-const i Int)
(declare-const j Int)
(declare-const ibv (_ BitVec 32))
(declare-const jbv (_ BitVec 32))

(assert (> (str.len s) 6))

(assert (= i (str.indexof s "#")))
(assert (= j (str.indexof s "@")))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                                             ;
; WHEN                                        ;
;                                             ;
;    (assert (= i (bv2int ibv)))              ;
;    (assert (= j (bv2int jbv)))              ;
;                                             ;
; ARE COMMENTED OUT, THE QUERY IS SAT:        ;
;                                             ;
;    sat                                      ;
;    ((i (- 1))                               ;
;     (j (- 1))                               ;
;     (s "\x00\x00\x00\x00\x00\x00\x00"))     ;
;                                             ;
; =========================================== ;
;                                             ;
; WHEN                                        ;
;                                             ;
;    (assert (= i (bv2int ibv)))              ;
;    (assert (= j (bv2int jbv)))              ;
;                                             ;
; ARE PART OF THE QUERY, IT IS UNSAT:         ;
;                                             ;
;    unsat                                    ;
;    (error "line 46 column 18:               ;
;      model is not available")               ;
;                                             ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;(assert (= i (bv2int ibv)))
;(assert (= j (bv2int jbv)))

(assert (= i j))

(check-sat)
(get-value (i j s))

[NikolajBjorner]

bv2int is interpreted. It maps bit-vectors to non-negative integers using the formula Sum_i 2^i*x_i, where x_i is the i'th bit. in bit-vector x (least significant bit has index 0). Therefore (assert (= -1 (bv2int ibv))) should be unsat.

Therefore we have int2bv(bv2int x) = x, but on the other hand bv2int((_ int2bv N) x) is not the same as x, since it maps integer x to a bit-vector corresponding to x mod 2^N, where N is the bit-width supplied as argument to int2bv. So the bit-blasted version of the bv2int.txt cannot directly afford itself to make simplifications that get rid of int2bv. Even if you restricted the range of the arguments to int2bv to be within the boundaries 0..2^N-1 Z3 would not recognize this in any of its preprocessing or inprocessing. It therefore expands int2bv defining each bit position as a property of its arguments mod 2^j, j = 0...,N.

The only way a position into a string can be both # and @ at the same time is when the position does not exist. The semantics of str.indexof sets the position to -1 for non-existing characters. Since the range of bv2int is non-negative you get unsat as expected. There is nothing "wrong" with Z3's behavior on the above example.

[OrenGitHub]

Thanks @NikolajBjorner ! we've used the documentation from z3/src/api/z3_api.h that says bv2int
is treated as uninterpreted --

/**
  \brief Create an integer from the bit-vector argument \c t1.
  If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned.
  So the result is non-negative
  and in the range \ccode{[0..2^N-1]}, where N are the number of bits in \c t1.
  If \c is_signed is true, \c t1 is treated as a signed bit-vector.
  This function is essentially treated as uninterpreted.
  So you cannot expect Z3 to precisely reflect the semantics of this function
  when solving constraints with this function.
  The node \c t1 must have a bit-vector sort.
  def_API('Z3_mk_bv2int', AST, (_in(CONTEXT), _in(AST), _in(BOOL)))
  */
  Z3_ast Z3_API Z3_mk_bv2int(Z3_context c,Z3_ast t1, Z3_bool is_signed);

Just to conclude your remark, I've compared the following 2 tests, which are essentially identical except the bit-vector width. If I understand you correctly, then there should be a time difference in the two queries solution time (and there is: 38 sec vs. 1 sec) because proving (= (bv2int ((_ int2bv N) i)) i) is not an O(1) immediate conclusion (with the corresponding constraints [0...2^N-1])

;;;; test 1 with 32 bits
(declare-const i Int)
(declare-const ibv (_ BitVec 32))

(assert (<= 0          i))
(assert (<  i 4294967296))

(assert (not (= (bv2int ((_ int2bv 32) i)) i)))

(check-sat)
(get-value (i ibv))

And:

;;;; test 2 with 5 bits
(declare-const i Int)
(declare-const ibv (_ BitVec 5))

(assert (<= 0          i))
(assert (<  i         32))

(assert (not (= (bv2int ((_ int2bv 5) i)) i)))

(check-sat)
(get-value (i ibv))

[NikolajBjorner]

Thanks, yes that documentation does not correspond to the current state.
I used to disable interpreting these functions a while ago, but that led to confusion going the other way.

[OrenGitHub]

I would like to add to this thread the next two (sat) examples that
demonstrate how both positive and negative integers can be mapped to the same bitvector:

(declare-const i Int)
(declare-const ibv (_ BitVec 5))

(assert (< i 0))
(assert (= ((_ int2bv 5) i) ibv))
(assert (= ibv #b10000))

(check-sat)
(get-value (i ibv))

With the answer:

sat
((i (- 48))
 (ibv #b10000))

And when i is constrained to be positive, the answer is sat too:

(declare-const i Int)
(declare-const ibv (_ BitVec 5))

(assert (> i 0))
(assert (= ((_ int2bv 5) i) ibv))
(assert (= ibv #b10000))

(check-sat)
(get-value (i ibv))

With the answer:

sat
((i 16)
 (ibv #b10000))

Thanks again, this issue can be closed.

[kren1]

Thanks for clearing this up.