z3py：如何在 z3 中实现计数器？

Question

我想在Z3py中设计类似于计数器的逻辑。

如果写python脚本，我们通常会定义一个变量"counter"，然后在需要的时候不断递增。但是，在 Z3 中，没有变体。因此，我没有定义变体，而是定义了该变体的踪迹。

这是示例代码。假设有一个大小为 5 的数组 "myArray"，数组中的元素为 1 或 2。我想声明一个约束，即 "myArray"

中必须有两个 '2'

from z3 import *

s = Solver()
myArray = IntVector('myArray',5)
for i in range(5):
    s.add(Or(myArray[i]==1,myArray[i]==2))
counterTrace = IntVector('counterTrace',6)
s.add(counterTrace[0]==0)
for i in range(5):
    s.add(If(myArray[i]==2,counterTrace[i+1]==counterTrace[i]+1,counterTrace[i+1]==counterTrace[i]))
s.add(counterTrace[5]==2)
print s.check()
print s.model()

我的问题是，这是在 Z3 中实现计数器概念的有效方式吗？在我的实际问题中，比较复杂，这真的很低效。

Answer 1

您可以这样做，但在 myArray[i] == 2 ? 1 : 0 上求和要容易得多。这样你就不需要断言任何东西，你正在处理正常的表达式。

z3py：如何在 z3 中实现计数器？

z3py: How to implement a counter in z3?

counter

smt

z3

z3py