FSeq question

[andrzejolszak]

Hello,

While trying to find a way to specify sequences like "the value of the element is the index+1" or "the value of the element is the sum of the 2 previous elements", I've encountered the below behavior, where a solution will be found for sequence len=5, but not for len=6:

int len = 5; // 5 will succeed with solution {1, 2, 0, 0, 0}, but 6 will not find solutions?
var l = Zen.Symbolic<FSeq<byte>>();
var idx = Zen.Symbolic<BigInteger>();
var sol = And(
  l.Length() == (BigInteger)len,
  l.At(idx) == Option.Some<byte>(1),
  l.At(idx + new BigInteger(1)) == Option.Some<byte>(2)).Solve(Solver.SolverType.Z3);

I assume I must be doing something wrong, or that there must be some parameter like search depth/iterations, that needs adjusting to make this work?

Also, if you have hints for implementing the above mentioned sequences, it will be greatly appreciated ;-)

Best regards,
Andrzej

[rabeckett]

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]

[andrzejolszak]

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