How to reverse Z3py Sequence?

I'm trying to make one Sequence equal antoher reversed. Here's the code:

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())

How can I implement Reversed function?

The expected output is something like this: seq1 == [1, 2, 3] seq2 == [3, 2, 1]

Solution

It is indeed possible to write a Reversed function in z3py. However, such definitions tend to be fragile and not very friendly for proofs. That is, while you can define and use such functions, do not expect z3 to be able to prove arbitrary properties using such constructs. This is because such definitions are in general recursive, and to prove anything interesting about a recursive function you need to do induction. And SMT-solvers don't do induction out-of-the-box, at least not yet.

Having said that, here's how you'd code your Reversed function in z3py:

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])

This prints:

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

i.e, you get [14, 9, 4] and its reverse [4, 9, 14].

Again, keep in mind that these constructs will mostly work well on ground-terms. Any property that needs induction will most likely lead z3 to give up and print unknown, or loop forever.