blob: f7b04af1ae959fc11de69d298b408cbfe635ed50 (
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
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
|
