Using z3.BitVecRef vs Integer

Question

A constant in a z3 solver can be a usual python type (1) or a z3 Ref (2) as in the following artificial example, where x and y undergo same constraint set through these two types:

from z3 import *

s = Solver()
x, y = BitVecs("x y",7)
d = BitVecVal(6, 7)

                   #constraints:
#                   ------------
s.add(x & 6 != 6)  #1'th or 2'th bit unset using Integer    #....(1)
#                                                   vs
s.add(y & d != d)  #1'th or 2'th bit unset using BitVecVal  #....(2)


check = s.check()
if check == sat:
    print(s.model())

So, is there one of (1), (2) to prefer? Seems, I don't understand why there are constant sorts if the same can be done with usual python types.

Answer 1

The resulting SMT code for Z3 can be shown as follows:

#  https://stackoverflow.com/a/14629021/1911064
def toSMT2Benchmark(f, status="unknown", name="benchmark", logic=""):
  v = (Ast * 0)()
  return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())

print(toSMT2Benchmark(x & 6 != 6))
print(toSMT2Benchmark(y & d != d))

Output:

; benchmark
(set-info :status unknown)
(declare-fun x () (_ BitVec 7))
(assert
 (and (distinct (bvand x (_ bv6 7)) (_ bv6 7)) true))
(check-sat)

; benchmark
(set-info :status unknown)
(declare-fun y () (_ BitVec 7))
(assert
 (and (distinct (_ bv6 7) (bvand y (_ bv6 7))) true))
(check-sat)

So, both forms do create pretty much the same input for Z3.