1 files changed, 26 insertions, 0 deletions
diff --git a/content/zettel/3d2b1.md b/content/zettel/3d2b1.md
new file mode 100644
index 0000000..f7b04af
--- /dev/null
+++ b/content/zettel/3d2b1.md
@@ -0,0 +1,26 @@
++++
+title = "Contents of Different Tables in SMTCoq"
+date = "2022-08-08"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3d2b"]
+forwardlinks = ["2e1c7", "3c3g1", "3d2b1a"]
+zettelid = "3d2b1"
++++
+
+In SMTCoq the formula needs to be represented somehow, which is easy to
+interpret as well as efficient to represent. For this they go with a
+multi-table approach, which is similar to the hashing that we are doing
+as well ([\#2e1c7], [\#3c3g1]). There are multiple different tables
+which are going to be presented in the next sections. At the top-level,
+the main representation of the logical formula is done by a list of
+literals, which refer to formulas inside of the formula table. This is
+called the state. Every formula in the state needs to be true for the
+whole system to be valid. These variables referring to formulas take the
+shape of an int, like `x`, where `x>>1` will refer to the location of
+the formula in the formula table, and `x&1` will be true if the formula
+should be negated and false otherwise.
+
+  [\#2e1c7]: /zettel/2e1c7
+  [\#3c3g1]: /zettel/3c3g1