Errors

Apply Pseudocode

Figure 5 of the TACAS 22 paper has the following error in its pseudocode:

The conditional on line 38 should have been as follows:
Q_app:2 != Ø && Q_app:2 matches (_ -> (t_f, t_g), _, __)

That is, it should only refer to the Q_app:2.

This has been fixed in the extended arXiv paper.

Reduce Pseudocode

Figure 6 of the TACAS 22 paper has the following errors

The conditional on line 3 should have been as follows:
Q_red != Ø or F_leaf.has_next()
The conditional on line 7 should have been
PeekMax(Q_red, F_leaf).source.label = j

where PeekMax is similar to PopMax but has no side effects on the contents of Q_red and F_leaf.
The conditional on line 19 should have been t_seek = t_f. Otherwise, the children of v_f are used incorrectly when v_f and v_g have the same uid but t_f != v_f.uid.
The output on line 22 should have been ‘v’notv`.

All of this has been fixed in the extended arXiv paper.

Nested Sweeping Cases

As Springer were preparing the VMCAI 26 publication, the references for the particular cases in Section 3 got turned into "*Case 3*" references to nowhere. We did not notice all botched references. So, some still linger which impedes understanding; see the extended arXiv paper for the correct case references.

Nested Sweeping Example

The example of executing the Exists sweep in VMCAI 26 has a minor error. In Figure 5(d-f) and Figure 9(f-h) since the bottom-left node has its children swapped. See the extended arXiv paper for the correct example.

Changes

64-bit Encoding of Pointers

In the extended arXiv paper for [TACAS 22], we show in Section 3.5 how to encode the unique identifier into a single 64-bit integer. This is (1) to decrease the BDD size and especially (2) to make the pointer sorting operations as fast as possible.

v1.2

It was always the intention that the flag bit on children should be used for the addition of complement edges in BDDs. Yet, up to this point it was left unused. Hence, we reassigned the meaning of this bit to instead propagate an edge being tainted by the decision diagram's reduction rule [ATVA 23].

v2.0

For Nested Sweeping, we need to taint an arc's source to be originating from the outer sweep. Yet, the flag was up to this point used to store the out-index of the source. Hence, for internal nodes we introduce the out-index (p) on the second least-significant bit - essentially adding a second (possibly non-Boolean) flag.

Figure 10 (b):


`0`	`. . . . . label. . . . .`	`. . . . . . . identifier. . . . . . .`	`o`	`f`

At this point, o only uses 1 bit, but in the case of Quantum Multi-valued Decision Diagrams this would use 2 bits to handle the 4-ary outdegree.

Yet, the above introduction of the out-index, o, removes a bit from the number of level identifiers. This decreases the maximum width without an overflow downto only 3 TiB. Hence, the maximum size of a BDD without possible overflow is only 6 TiB.

To get the maximum width safe from overflows back up to 6 TiB, we have removed the most significant terminal bit flag. Instead, now all pointers dedicate the ℓ most significant bits to its level. The largest level is dedicated to null and the second-largest to terminals. This decreases the number of BDD labels by 2 and also restricts terminal values to fit into 64-ℓ-1-1 = 62-ℓ bits. Yet, this is fine for bool, char, int, and float.

Figure 10 (a):


`. . . . . level. . . . .`	`. . . . . . . . . v. . . . . . . . . .`	`f`