Per commit 89efe79, we currently have a bug in Kirigami when handling remapping of node expressions. examples/kirigami/node-eq.nv gives a MWE of this.
Essentially, the issue is as follows:
When encoding a fold over assertions of the form assert foldNodes (fun u v acc -> acc && assertNode u v) sol true, we start by unrolling sol and flattening tuples to obtain a statement that reasons over each node:
where each assertNode has k arguments where k is the number of arguments used to encode the attribute for that particular node.
This leads to an issue when assertNode reasons over expressions that contain references to these nodes.
For instance, the expression
let assertNode u v = if u = 1n then true else v = 0
will have the value of u populated to now leave us with:
Suppose we have two nodes, 0n and 1n, which are placed in separate partitions: then we remap 1n to 0n in partition 1, and we want to eliminate additional conjuncts, leaving us with:
The problem here is that our current approach doesn't know to handle 0n = 1n differently in partition 1, since we'd need to remap 1n to 0n, but since we have that 0n has been cut, we don't recognize that the LHS of the equality should be kept and so both partitions reduce this expression to false.
The best way to handle this may be if we transformed assertNode from the top, we could end up with
(* Partition 0 *)
let assertNode u v = if false then true else v = 0
(* Partition 1 *)
let assertNode u v = if u = 0n then true else v = 0
which would then work once map unrolling is performed.
Per commit 89efe79, we currently have a bug in Kirigami when handling remapping of node expressions.
examples/kirigami/node-eq.nvgives a MWE of this. Essentially, the issue is as follows: When encoding a fold over assertions of the formassert foldNodes (fun u v acc -> acc && assertNode u v) sol true, we start by unrollingsoland flattening tuples to obtain a statement that reasons over each node:where each
assertNodehaskarguments wherekis the number of arguments used to encode the attribute for that particular node. This leads to an issue whenassertNodereasons over expressions that contain references to these nodes. For instance, the expressionwill have the value of u populated to now leave us with:
Suppose we have two nodes, 0n and 1n, which are placed in separate partitions: then we remap 1n to 0n in partition 1, and we want to eliminate additional conjuncts, leaving us with:
The problem here is that our current approach doesn't know to handle
0n = 1ndifferently in partition 1, since we'd need to remap 1n to 0n, but since we have that 0n has been cut, we don't recognize that the LHS of the equality should be kept and so both partitions reduce this expression tofalse. The best way to handle this may be if we transformedassertNodefrom the top, we could end up withwhich would then work once map unrolling is performed.