Skip to content

Normalize and simplify #348

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 14 commits into
base: main
Choose a base branch
from
Draft

Normalize and simplify #348

Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
c39e724
adding atomic simplifications
felixL-K May 14, 2025
a237983
adding convertion simplifications
felixL-K May 16, 2025
39dc3b4
simplification of conversions
felixL-K May 16, 2025
557a54d
Merge branch 'formalsec:main' into normalize
felixL-K May 19, 2025
598d4ca
Merge branch 'formalsec:main' into normalize
felixL-K May 22, 2025
744721f
adding reviews changes
felixL-K May 22, 2025
91d5160
adding unit test for simplification
felixL-K May 23, 2025
9a1197f
adding unit tests for normalization
felixL-K May 26, 2025
f2f4092
adding reviews of zapashcanon and filipe
felixL-K May 27, 2025
8bee159
Merge branch 'formalsec:main' into normalize
felixL-K Jun 18, 2025
1e41a76
resolving conversations
felixL-K Jul 15, 2025
1136904
Update src/smtml/expr.ml
felixL-K Jul 15, 2025
bda7978
removed duplicates, And with cst
felixL-K Jul 15, 2025
13e8356
resolved synk conflicts
felixL-K Jul 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 6 additions & 5 deletions src/smtml/expr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -385,14 +385,15 @@ let rec binop ty op hte1 hte2 =
when Bitvector.eqz bv ->
hte1
| (Add | Or), _, Val (Bitv bv) when Bitvector.eqz bv -> hte1
| Add, _, Val (Real 0.) -> hte1
| Add, Val (Real 0.), _ -> hte2
| Add, _, Val (Num (F32 0l)) -> hte1
| Add, Val (Num (F32 0l)), _ -> hte2
| Add, _, Val (Real -0.) -> hte1
| Add, Val (Real -0.), _ -> hte2
| Add, _, Val (Num (F32 -0l)) -> hte1
| Add, Val (Num (F32 -0l)), _ -> hte2
| (And | Mul), _, Val (Bitv bv) when Bitvector.eqz bv -> hte2
| And, Val True, _ -> hte2
| And, _, Val True -> hte1
| And, Val False, _ | And, _, Val False -> make (Val False)
| And, Val False, _ -> hte1
| And, _, Val False -> hte2
| Or, Val True, _ | Or, _, Val True -> make (Val True)
| Or, Val False, _ -> hte2
| Or, _, Val False -> hte1
Expand Down