1 files changed, 40 insertions, 0 deletions
diff --git a/content/zettel/2e1c7.md b/content/zettel/2e1c7.md
new file mode 100644
index 0000000..eea31fb
--- /dev/null
+++ b/content/zettel/2e1c7.md
@@ -0,0 +1,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