如何在 z3py 中将 IntVector 转换为 Int

Question

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

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

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

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

因为它们是两种不同的类型。 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()))