如何反转 Z3py 序列？答案

【问题标题】：How to reverse Z3py Sequence?如何反转 Z3py 序列？
【发布时间】：2021-11-17 13:36:51
【问题描述】：

我正在尝试使一个序列等于另一个相反的序列。代码如下：

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]

【问题讨论】：

标签： z3 solver z3py

【解决方案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，或者永远循环。

【讨论】：