如何反转 Z3py 序列？

Question

我正在尝试使一个序列与她相反。这是代码：

s = Solver()

# declare sequences of integers
seq1 = Const('seq1', SeqSort(IntSort()))
seq2 = Const('seq2', SeqSort(IntSort()))


# assert the sequences have at least 3 elements
s.add(Length(seq1) >= 3)
s.add(Length(seq2) >= 3)

# here I don't know how to do it
s.add(seq1 == Reversed(seq2))


# get a model and print it:
if s.check() == sat:
   print(s.model())

如何实现Reversed功能？

预期的输出是这样的： seq1 == [1, 2, 3] seq2 == [3, 2, 1]

Answer 1

确实可以在z3py中写一个Reversed函数。然而，这样的定义往往是脆弱的并且对于证明不是很友好。也就是说，虽然您可以定义和使用此类函数，但不要期望 z3 能够使用此类构造证明任意属性。这是因为这样的定义通常是递归的，要证明关于递归函数的任何有趣的事情，您需要进行归纳。而且 SMT 求解器不会开箱即用地进行归纳，至少现在还没有。

话虽如此，以下是如何在 z3py 中编写 Reversed 函数：

from z3 import *

s = Solver()

# declare sequences of integers
seq1 = Const('seq1', SeqSort(IntSort()))
seq2 = Const('seq2', SeqSort(IntSort()))


# assert the sequences have at least 3 elements
s.add(Length(seq1) >= 3)
s.add(Length(seq2) >= 3)

Reversed = RecFunction('Reversed', SeqSort(IntSort()), SeqSort(IntSort()))
l = FreshConst(SeqSort(IntSort()))
RecAddDefinition( Reversed
                , [l]
                , If( Length(l) == 0
                    , l
                    , Concat(Reversed(Extract(l, 1, Length(l)-1)), Unit(l[0]))
                    )
                )

s.add(seq1 == Reversed(seq2))

# get a model and print it:
if s.check() == sat:
    m = s.model()
    print(m[seq1])
    print(m[seq2])

这会打印：

Concat(Unit(14), Concat(Unit(9), Unit(4)))
Concat(Unit(4), Concat(Unit(9), Unit(14)))

即，您得到 [14, 9, 4] 及其反向 [4, 9, 14]。

同样，请记住，这些结构在基本条件下大多会运作良好。任何需要归纳的属性很可能会导致 z3 放弃并打印 unknown，或者永远循环。

如何反转 Z3py 序列？

How to reverse Z3py Sequence?

z3

solver

z3py