Z3 SMT 和 Python 的结果不正确

Question

我正在尝试从此处的 Whosebug 答案中复制另一个用户给出的脚本

我认为大部分内容都可以使它与 python 绑定一起使用，但是我没有得到正确的答案。这是 python 脚本：

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()

我的结果如下：

(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)))

[掩码 = 0，被乘数 = 0，y = 0，x = 0]

这显然是不正确的。我看到的主要区别是我生成的 SMT 代码似乎对 'y' 进行了赋值，而在另一个 StackExchange 答案中他有一个 let 表达式。有人可以在这里为我指出正确的方向吗？

Answer 1

通过 Python API 和 parse_smt2_string ( http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#-parse_smt2_string ):

解析 SMT2 字符串，您可能会喜欢这个技巧

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())

输出为：

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

你对 let 表达式的编码有问题。对于主要断言，您需要在所有 x 上使用通用量词，而您正试图使用它来定义 let 表达式。以下基本上适用于您的原始编码，只需创建一个指向适当表达式 y 的指针并复制它：

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())

输出为：

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

Answer 2

问题实际上是关于 Z3 Python 绑定的。但这是一个有趣的。在不引发任何语言战争的情况下，我只是想将 Haskell 解决方案放在这里以供参考，再次使用 Z3 作为底层求解器：

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]]

我们得到：

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

Z3 SMT 和 Python 的结果不正确

Incorrect result with Z3 SMT and Python

smt

z3

z3py