diff options
Diffstat (limited to 'content/zettel/2e1c6a.md')
| -rw-r--r-- | content/zettel/2e1c6a.md | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/content/zettel/2e1c6a.md b/content/zettel/2e1c6a.md new file mode 100644 index 0000000..740231f --- /dev/null +++ b/content/zettel/2e1c6a.md @@ -0,0 +1,25 @@ ++++ +title = "Using hash-consing with `PTree`" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3c3g1", "2e1c7", "2e1c6"] +forwardlinks = ["3c3b", "3a8g5", "3a8g5e", "2e1c6b"] +zettelid = "2e1c6a" ++++ + +One solution to the hash-consing problem is to use a `PTree` to store +the values and to define an equality check between the SAT expressions. +That way, one can assign a unique ID to each of the predicates, and can +therefore add them into the SAT expression. Then the logical expression +can take into account the expressions. This greatly simplifies the +heuristic algorithm to do the comparison, as instead a single SAT +expression can be used to do the same thing. + +This technique can be used to solve the proof of the scheduling +algorithm with hyperblocks ([\#3c3b]), as well as the proof of the +predicates in CompCertGSA ([\#3a8g5], [\#3a8g5e]). + + [\#3c3b]: /zettel/3c3b + [\#3a8g5]: /zettel/3a8g5 + [\#3a8g5e]: /zettel/3a8g5e |