diff options
Diffstat (limited to 'content/zettel/3a8g5g1.md')
| -rw-r--r-- | content/zettel/3a8g5g1.md | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/content/zettel/3a8g5g1.md b/content/zettel/3a8g5g1.md new file mode 100644 index 0000000..2b8f5db --- /dev/null +++ b/content/zettel/3a8g5g1.md @@ -0,0 +1,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 |