Expanding Transitive Closure Involving Constraints on Sets and Relations

[tpops]

Transitive Closure

Currently we have transitive closure inplemented in IEGEnLib, can be found in SparseConstraints::TransitiveClosure. It builds terms as nodes in the graph and edges are relationships between each node- otherwise known as constraints. The algorithm uses floyd marshal algorithm as its core to perform a closure on the graph to discover new relationships. This also introduced a new theorem that will be available in a paper coming up. This theorem infers a new relationship by induction that seemed useful in Synthesis research

Current Limitation

A unique situation in synthesis exposed a limitation on current transitive closure. In summary transitive closure does not currently considers parameters to UFs especially equality constraints involving such parameters. A good example can be seen below

R:= { [n] -> [i, k] : i - row1(n) = 0 && k - P1(row1(n), col1(n)) = 0 && col1(n) - col2(k) = 0
 && n >= 0 && i >= 0 && col1(n) >= 0 && row1(n) >= 0 && k - rowptr(i) >= 0 && 
-n + NNZ - 1 >= 0 && -i + NR - 1 >= 0 && -k + rowptr(i + 1) - 1
     >= 0 && NC - col1(n) - 1 >= 0 && NR - row1(n) - 1 >= 0 }

Applying Closure on R will currently result to

TR:= { [n] -> [i, k] : i - P0(row1(n), col1(n)) = 0 && i - row1(n) = 0 && 
k - P1(row1(n), col1(n)) = 0 && P0(row1(n), col1(n)) - row1(n) = 0 && 
col1(n) - col2(k) = 0 && n >= 0 && i >= 0 && P0(row1(n), col1(n)) >= 0 &&
 col1(n)     >= 0 && col2(k) >= 0 && row1(n) >= 0 && -1 >= 0 && k - rowptr(i) >= 0 &&
 NC - 1 >= 0 && NNZ - 1 >= 0 && NR - 1 >= 0 && P1(row1(n), col1(n)) - rowptr(i) >= 0 &&
 -n + NNZ - 1 >= 0 && -i + NR - 1 >= 0 && -k + rowptr(i + 1) - 1 >= 0 &&
 NC - col1(n) - 1 >= 0 && NC - col2(k) - 1 >= 0 && NR - P0(row1(n), col1(n)) - 1 >= 0 &&
 NR - row1(n) - 1 >= 0 && -P1(row1(n), col1(n)) + rowptr(i + 1) - 1 >= 0 &&
 -rowptr(i) + rowptr(i + 1) - 1 >= 0 }

In the above example a constraint shows the relationship between i and row1(n). This relationship should lead to new nodes in the transitive closure graph that produce new relationships such as -k + rowptr(i + 1) - 1 >= 0 also becoming -k + rowptr(row1(n) + 1) - 1 >= 0 or -rowptr(row1(n)) + rowptr(row1(n) + 1) - 1 >= 0 both pairs of relationships are true and should both be in the closure. This is a step further in Transitive closure in presense of UFs.

This Issue tracks changes to expanding Transitive Closure on these cases

[tpops]

This was solved in a different repository: CodeSynthesis which should be moved here by @tpops