blob: 740231f5711232c32c2e888e2a76874356a47543 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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
|
