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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
+++
title = "Hashing symbolic expressions"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3d2b1", "2e1c6"]
forwardlinks = ["2e1c6a", "3c3c3"]
zettelid = "2e1c7"
+++
We want to be able to transform symbolic expressions into a
representation that can be passed to the SAT solver. For this, we need
to turn two different symbolic expressions, that are structurally equal,
into the same value. Using IDs from hash-consing is maybe not the best
solution for this, because one would need to add axioms to Coq to be
able to access the actual IDs of the hashes. These are needed to do the
fundamental comparison.
In addition to that, it might be necessary to be able to reify the IDs
back into expressions, although this is maybe not the most important,
just might be a function that is needed to show the uniqueness of the
outputs, and the injectivity of the function.
The first idea would be uniquely identify the constructors with an ID,
and then recursively translate the IDs of the other expressions as well.
However, these lists should then be translated to a unique value to be
used in the SAT solver. The easiest way to do that would be to add them
all up as power of twos, but that might result in IDs that are much too
large.
Using hash-consing with the use of a map and pointers to the value, that
would make things easier, but as stated earlier, actually accessing the
value of the map requires some axioms, so it would be nice to not use
them directly, but to maybe only use them as an optimisations, and a
back-up way to generate the ids.
A solution to this might be ([\#2e1c6a] or [\#3c3c3]).
[\#2e1c6a]: /zettel/2e1c6a
[\#3c3c3]: /zettel/3c3c3
|
