Skip to content

Commit

Permalink
Proof reading docs/papers/amend
Browse files Browse the repository at this point in the history
  • Loading branch information
SSoelvsten committed Dec 8, 2023
1 parent c4c7a39 commit c3f8875
Showing 1 changed file with 12 additions and 12 deletions.
24 changes: 12 additions & 12 deletions docs/papers/amend.md
Original file line number Diff line number Diff line change
Expand Up @@ -27,17 +27,17 @@ edge being *tainted* by the decision diagram's reduction rule [[ATVA
v2.0
------------------------

For *Nested Sweeping*, we need to mark an arc's *source* to be originating from
the *outer sweep*. Yet, the *flag* was up to this point used to store the
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`|
| | | | | |
|-----|----------------------------|-----------------------------------------|-----|-----|
| `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.
Expand All @@ -54,17 +54,17 @@ 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 it into 64-ℓ-1-1 = 62-ℓ bits. Yet,
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`|
| | | |
|----------------------------|------------------------------------------|-----|
| `. . . . . level. . . . .` | `. . . . . . . . . v. . . . . . . . . .` | `f` |

**Figure 10 (b):**

| | | | |
|--------------------------|---------------------------------------|---|---|
|`. . . . . level. . . . .`|`. . . . . . . identifier. . . . . . .`|`o`|`f`|
| | | | |
|----------------------------|------------------------------------------|-----|-----|
| `. . . . . level. . . . .` | `. . . . . . . identifier . . . . . . .` | `o` | `f` |

0 comments on commit c3f8875

Please sign in to comment.