FSeq question about zen HOT 2 CLOSED

Hi Andrzej,

Your intuition is correct. The problem here is that the FSeq type will only model sequences up to a certain bounded length. The default was 5 (and recently increased to 8). So when you ask for a sequence of length 6 it can't find such a sequence because no sequence of length 5 or less can have length 6. There are two ways to solve this.

1. You can increase the size of the FSeq. Just use the depth parameter when creating the sequence:

int len = 6;
var l = Zen.Symbolic<FSeq<byte>>(depth: 10); // give the max size here
var idx = Zen.Symbolic<BigInteger>();
var sol = Zen.And(
    l.Length() == (BigInteger)len,
    l.At(idx) == Option.Some<byte>(1),
    l.At(idx + BigInteger.One) == Option.Some<byte>(2)).Solve();

2. You could use the Seq type, which does not bound the size of the sequence. However, Z3 may not always give you an answer for Seq. For example, the following works for me:

int len = 30;
var l = Zen.Symbolic<Seq<byte>>();
var idx = Zen.Symbolic<BigInteger>();
var sol = Zen.And(
    idx >= BigInteger.Zero,               // have to add constraints on the index since Nth can return any value if out of bounds
    idx < (BigInteger)(len - 1),
    l.Length() == (BigInteger)len,
    l.Nth(idx) == 1,
    l.Nth(idx + BigInteger.One) == 2).Solve();

In terms of having every element of the sequence depend on other values, there is not a super clean way to do that since the sequence length is variable. If you really want to you can write recursive functions (like this), but I wouldn't recommend it. If you are okay with modeling a sequence that has a fixed length, you could look at the Array type, which just gives you direct access to all of the elements. For example:

var a = Zen.Symbolic<Array<byte, _10>>();
Zen<byte>[] array = a.ToArray();
var constraints = new List<Zen<bool>>();
for (int i = 0; i < array.Length; i++)
{
    constraints.Add(array[i] == (byte)(i + 1));
}

var sol = Zen.And(constraints).Solve();
Console.WriteLine(sol.Get(a));

Result is:
[1,2,3,4,5,6,7,8,9,10]

from zen.

Thank you for the detailed answer, this helps :-)

from zen.