Forall quantifier

[tjausm]

Notation A notation of formula such as forall params : expr is required which allows us to access in expr: at least 2 array indexes and 2 values of said array indexes. We could do forall arr, index, value : expr, and use nested expressions to get an arbitrary number of indexes and corresponding values.

z3-implementation There are 2 ideas:

• z3-array: transform the array to a z3-array and use it in combination with the forall quantifier
• Frontend arraybuilder: transform the array to a Expression in the frontend as suggested here.

Both methods seem to have their up and downside in runtime and difficulty of implementation. I will research how to actually implement both, and start with implementing the easiest variant.

Notes Wishnu proposed several notations:

1. forall x in a : x >= 0 which, mapped to z3 infinite array, becomes: forall i : 0 <= i < #a ==> a[i] >= 0
2. forall i in Int : 0 <= i < #a ==> a[i] >= i
3. (he als proposed Stefan's notation, while noting it wasn't very convenient)

[tjausm]

Frontend array builder was implemented in commit 9e29f199e021849b04e9c391915ec088cf530ffd. Next is the Exist quantifier