blob: 2b8f5dbfb69099762e356307542321651c713649 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
+++
title = "Implementing a three-valued solver"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3m2", "3a8g5g"]
forwardlinks = ["3a8g5h3", "3a8g5h5"]
zettelid = "3a8g5g1"
+++
In the end, the current conversion to GSA uses a three-valued logic
solver, as described in the third solution ([\#3a8g5h3]). The main
problem with this check is that it is quite slow, and needs to be
performed a lot of times. Even using a solver like Z3, it takes quite a
bit of time to get a solution, and especially with large constructs like
case statements, it becomes even harder of a translation problem.
One way to approach this is to properly reason about the predicates
instead of validating them, which is similar to the solution proposed in
([\#3a8g5h5]).
[\#3a8g5h3]: /zettel/3a8g5h3
[\#3a8g5h5]: /zettel/3a8g5h5
|
