Z3 遍历字符串以累加数字(Python API)

huangapple go评论68阅读模式
英文:

Z3 Iterate over String to add up Only Numbers (Python api)

问题

我希望我的Z3脚本能够生成一个字符串,其中所有数字相乘等于某个值。因此,它需要迭代该字符串并仅获取数字并将它们相乘。它应该跳过其他字符。

例如,"a1b2c3" 的结果是 6。

现在我知道我需要重建我的代码片段,但这就是我想要做的事情:

from z3 import *

s = Solver()

def mul_only_numbers(w):
    res = 1
    for elem in str(w):
        if elem.isdigit():
            res *= int(elem)
    return res

word = String("word")
s.add(mul_only_numbers(word) == 6)

res = s.check()
if res == sat:
    st = str(s.model()[word])
    print(st)
else:
    print("Solver said:", res)

当然,这不起作用,因为 str(w) = "word"

但我如何才能实现我试图做的事情?

英文:

I want my Z3 Script to be able to generate a string where all digits multiplied equal a certain value. Therefore it needs to iterate over said String and take only the digits and multiply them together. It should skip other chars.

For example "a1b2c3" results to 6

Now I know that I need to rebuild my snippet, but this is what I wanted to do:

from z3 import *

s = Solver()

def mul_only_numbers(w):
    res = 1
    for elem in str(w):
        if elem.isdigit():
            res *= int(elem)
    return res

word = String("word")
s.add(mul_only_numbers(word) == 6)

res = s.check()
if res == sat:
    st = str(s.model()[word])
    print(st)
else:
    print("Solver said:", res)

Of course this doesn't work because str(w) = "word".

But how can I still achieve, what I'm trying to do?

答案1

得分: 1

在Python中,你不能使用递归(或迭代)来遍历符号字符串的元素。递归必须在z3级别上完成,你可以使用RecFunction工具来实现:

from z3 import *

s = Solver()

def digitValue(c):
    dv = StrToInt(c)
    return If(dv == -1, 1, dv)

mul_only_numbers = RecFunction('mul_only_numbers', StringSort(), IntSort())
w = FreshConst(StringSort())
RecAddDefinition( mul_only_numbers
                , [w]
                , If ( Length(w) == 0
                     , 1
                     , digitValue(Extract(w, 0, 1)) * mul_only_numbers(Extract(w, 1, Length(w) - 1))
                     )
                )

word = String("word")
s.add(mul_only_numbers(word) == 6)
s.add(Length(word) >= 8)

res = s.check()
if res == sat:
    print(s.model()[word])
else:
    print("Solver said:", res)

请注意,我添加了一个额外的约束条件,要求字符串的Unicode长度大于等于8,以使模型更有趣。这将打印:

"61\u{0}\u{0}\u{0}\u{0}\u{0}\u{0}"

这满足字符串中的数字相乘等于6的约束条件。

请注意,这种递归定义虽然可能,但性能可能不佳,并且可能导致可决定性问题。这意味着求解器可能会响应unknown,或者需要很长时间才能得出结果。如果你事先知道字符串的长度,那么最好是分别对每个字符进行建模。或者你可以逐步增加长度:尝试长度1、长度2,依此类推,直到找到满足约束条件的模型。或者甚至可以对长度进行二进制搜索。通常,你需要尝试不同的编码方式,以找到最适合每个特定问题的方法。

英文:

You cannot use recursion (or iteration) in Python to go over the elements of a symbolic string. The recursion has to be done at the z3-level, for which you can use RecFunction facility:

from z3 import *

s = Solver()

def digitValue(c):
    dv = StrToInt(c)
    return If(dv == -1, 1, dv)

mul_only_numbers = RecFunction('mul_only_numbers', StringSort(), IntSort())
w = FreshConst(StringSort())
RecAddDefinition( mul_only_numbers
                , [w]
                , If ( Length(w) == 0
                     , 1
                     , digitValue(Extract(w, 0, 1)) * mul_only_numbers(Extract(w, 1, Length(w) - 1))
                     )
                )

word = String("word")
s.add(mul_only_numbers(word) == 6)
s.add(Length(word) >= 8)

res = s.check()
if res == sat:
    print(s.model()[word])
else:
    print("Solver said:", res)

Note that I added an extra constraint that the string should have unicode length of >= 8 to make the model interesting. This prints:

"61\u{0}\u{0}\u{0}\u{0}\u{0}\u{0}"

which satisfies the constraint that the digits in the string multiplied gives you 6.

Note that this sort of recursive definition, while possible, will not be performant; and it can cause decidability issues. By that, I mean the solver might end up responding unknown, or take very long to come back. If you know the length of the string in advance, then you'd be better served modeling each character separately instead. Or you can iteratively increase the length: Try length 1, length 2, ... etc., until you find a model that satisfies your constraints. Or even do a binary search on the length. One usually needs to experiment with different encodings to find one that works the best for each individual problem.

huangapple
  • 本文由 发表于 2023年7月10日 22:53:05
  • 转载请务必保留本文链接:https://go.coder-hub.com/76654949.html
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定