+++
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