Incorrect result with Z3 SMT and Python

1
votes

I'm trying to replicate the script given by another user from this StackOverflow answer here https://stackoverflow.com/a/14551792

I have what I believe to be most of the pieces to get this to work with the python bindings, however I don't get the correct answer. Here is the python script:

from z3 import *

mask = BitVec('mask', 64)
multiplicand = BitVec('multiplicand', 64)
x = BitVec('x', 64)
y = BitVec('y', 64)

s = SolverFor("BV")
F = [
ForAll(x, (y == (mask & x) * multiplicand)),
And(Extract(63, 63, x) == Extract(63, 63, y),
    Extract(55, 55, x) == Extract(62, 62, y),
    Extract(47, 47, x) == Extract(61, 61, y),
    Extract(39, 39, x) == Extract(60, 60, y),
    Extract(31, 31, x) == Extract(59, 59, y),
    Extract(23, 23, x) == Extract(58, 58, y),
    Extract(15, 15, x) == Extract(57, 57, y),
    Extract(7, 7, x) == Extract(56, 56, y))
]

print F[0].sexpr()
print F[1].sexpr()

s.add(F)
if s.check() == sat:
    print "ok"
    print s.model()

My results give me the following:

(forall ((x (_ BitVec 64))) (= y (bvmul (bvand mask x) multiplicand)))
(and (= ((_ extract 63 63) x) ((_ extract 63 63) y))
     (= ((_ extract 55 55) x) ((_ extract 62 62) y))
     (= ((_ extract 47 47) x) ((_ extract 61 61) y))
     (= ((_ extract 39 39) x) ((_ extract 60 60) y))
     (= ((_ extract 31 31) x) ((_ extract 59 59) y))
     (= ((_ extract 23 23) x) ((_ extract 58 58) y))
     (= ((_ extract 15 15) x) ((_ extract 57 57) y))
     (= ((_ extract 7 7) x) ((_ extract 56 56) y)))

[mask = 0, multiplicand = 0, y = 0, x = 0]

This is obviously incorrect. The main difference I'm seeing is that my produced SMT code appears to do an assignment to 'y' whereas in the other StackExchange answer he's got a let-expression. Can somebody point me in the right direction here?

2
z3smtz3py

2 Answers

2
votes

Here's a trick you might enjoy by parsing the SMT2 string via the Python API with parse_smt2_string ( http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#-parse_smt2_string ):

from z3 import *

s = SolverFor("BV")

#s.set(':pp.bv_literals', True) # gives error for some reason

mask = BitVec('mask', 64)
multiplicand = BitVec('multiplicand', 64)
x = BitVec('x', 64)
y = BitVec('y', 64)

F = parse_smt2_string(' \
(set-option :pp.bv_literals true) \
(declare-const mask         (BV64)) \
(declare-const multiplicand (BV64)) \
(assert (forall ((x (BV64))) \
    (let ((y (bvmul (bvand mask x) multiplicand))) \
      (and \
        (= ((_ extract 63 63) x) ((_ extract 63 63) y)) \
        (= ((_ extract 55 55) x) ((_ extract 62 62) y)) \
        (= ((_ extract 47 47) x) ((_ extract 61 61) y)) \
        (= ((_ extract 39 39) x) ((_ extract 60 60) y)) \
        (= ((_ extract 31 31) x) ((_ extract 59 59) y)) \
        (= ((_ extract 23 23) x) ((_ extract 58 58) y)) \
        (= ((_ extract 15 15) x) ((_ extract 57 57) y)) \
        (= ((_ extract  7  7) x) ((_ extract 56 56) y)) \
      ) \
    ) \
  ))', sorts={ 'BV64' : BitVecSort(64) })

print F

s.add(F)

print s.to_smt2()

if s.check() == sat:
    print "ok"
    print s.model()
    m = s.model()
    print hex(m[mask].as_long())
    print hex(m[multiplicand].as_long())

Output is:

[mask = 9259542123273814144, multiplicand = 567382630219905]
0x8080808080808080L
0x2040810204081L

There was a problem of your encoding of the let expression. You need the universal quantifier over all x for the main assertion, whereas you were trying to use it to define the let expression. The following works for basically your original encoding, just creating a pointer to the appropriate expression y and copying it:

from z3 import *

mask = BitVec('mask', 64)
multiplicand = BitVec('multiplicand', 64)
x = BitVec('x', 64)
y = BitVec('y', 64)

y = ((mask & x) * multiplicand)

s = SolverFor("BV")
F = [
ForAll(x,
And(Extract(63, 63, x) == Extract(63, 63, y),
    Extract(55, 55, x) == Extract(62, 62, y),
    Extract(47, 47, x) == Extract(61, 61, y),
    Extract(39, 39, x) == Extract(60, 60, y),
    Extract(31, 31, x) == Extract(59, 59, y),
    Extract(23, 23, x) == Extract(58, 58, y),
    Extract(15, 15, x) == Extract(57, 57, y),
    Extract(7, 7, x) == Extract(56, 56, y)))
]

print F[0].sexpr()

s.add(F)
if s.check() == sat:
    print "ok"
    print s.model()
    m = s.model()
    print hex(m[mask].as_long())
    print hex(m[multiplicand].as_long())

Output is:

[mask = 9259542123273814144, multiplicand = 567382630219905]
0x8080808080808080L
0x2040810204081L
2
votes

The question is really about the Z3 Python bindings. But it's an interesting one. Without starting any language wars, I just wanted to put here the Haskell solution to the same for reference purposes, again using Z3 as the underlying solver:

import Data.SBV

main :: IO ()
main = print =<< satWith z3{printBase=16} find
  where find = do mask <- exists "mask"
                  mult <- exists "mult"
                  inp  <- forall "inp"
                  let res         = (mask .&. inp) * (mult :: SWord64)
                      x `grab` is = map (sbvTestBit x) is
                  solve [inp `grab` [7, 15 .. 63] .== res `grab` [56 .. 63]]

We get:

*Main> main
Satisfiable. Model:
  mask = 0x8080808080808080 :: Word64
  mult = 0x0002040810204081 :: Word64