Problem Statement

The logic module contains a lark file for parsing logic expressions. However, the setup.py does not package the file currently.

Solution

Include the lark file as package_data in the setup.py

Shall we upload the coverage data from this repo to (e.g.) codecov.io? Since we're already computing it as an artefact it could add additional checks and data for PRs: https://about.codecov.io/product/features/#github-checks

I can do this.

Proposal

Currently, we simplify conjunctions or disjunctions of ranges only if they are all signed or all unsigned.
Consequently, we do not simplify expressions such as

• (x@8 u<= 10@8) & (x@8 s<= -3@8) to false
• (x@8 u<= 10@8) & (x@8 s<= 20@8) to x@8 u<= 10@8
• (x@8 u>= 5@8) & (x@8 s>= 2@8), to x@8 s>= 5@8
• (x@8 u>= 128@8) & (x@8 s>= -5@8) to x@8 u>= -5@8

Approach

Implement range simplification when signed and unsigned comparisons are mixed. Not all combinations may be possible.

Proposal

Currently, we only implemented CNF conversion. However, for dewolf, we also need DNF conversion.

Approach

Implement DNF conversion analog to CNF conversion as a visitor pattern