如何将IntVector转换为z3py中的Int

Question

我正在使用z3py，并且我的IntVector的大小为3。我需要将IntVector中的每个数字解析为一个整数。意思是，如果我有一个IntVector，它具有这样的约束：

myIntVector = IntVector('iv', 3)
s = Solver()
s.add(iv[0] == 5)
s.add(iv[1] == 2)
s.add(iv[2] == 6)
….

我需要能够在z3中作为Int排序对数字526进行操作，因为我需要同时添加适用于IntVector（数字）的每个单独成员的约束和适用于整数的约束，在这种情况下是526。我无法执行以下操作：

s.add(iv[0] / iv == 55)

因为它们是2个单独的类型。 iv[0]是Int，而iv是IntVector

Answer 1

这里是一个示例，它使用IntVector的概念作为单独的数字以及由这些数字形成的数字。它解决了传统的谜语，即将“ SEND + MORE = MONEY”中的每个字母替换为一个不同的数字。

from z3 import *

# trying to find different digits for each letter for SEND+MORE=MONEY
letters = 'SENDMOREMONEY'
iv = IntVector('iv', len(letters))
send = Int('send')
more = Int('more')
money = Int('money')

s = Solver()

# all letters to be replaced by digits 0..9
s.add([And(i >= 0, i <= 9) for i in iv])

# the first digit of a number can not be 0
s.add(And(iv[0] > 0, iv[4] > 0, iv[8] > 0))

# distinct letters need distinct digits
s.add(Distinct([i for k, i in enumerate(iv) if letters[k] not in letters[:k]]))

# "send" is the number formed by the first 4 digits, "more" the 4 next, "money" the last
s.add(send == Sum([10**(3-k)*i for k,i in enumerate(iv[:4])]))
s.add(more == Sum([10**(3-k)*i for k,i in enumerate(iv[4:8])]))
s.add(money == Sum([10**(4-k)*i for k,i in enumerate(iv[8:])]))

# the numbers for "send" and "more" sum together to "money"
s.add(send + more == money)

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

    # list each digit of iv
    print([m[i].as_long() for i in iv])

    # show the sum as "send" + "more" = "money"
    print("{} + {} = {}".format(m[send].as_long(), m[more].as_long(), m[money].as_long()))