Merge pull request #464 from ethereum/por-pand-rules

Adding POr and PAnd rules
ethereum · Mar 6, 2024 · 67a06eb · 67a06eb
2 parents 5d1ce43 + 330cc38
commit 67a06eb
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -8,6 +8,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## Changed
 
 ## Added
+- More POr and PAnd rules
 
 ## Fixed
 - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing

diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs
@@ -1202,9 +1202,13 @@ simplifyProp prop =
     go (PAnd (PBool l) (PBool r)) = PBool (l && r)
     go (PAnd (PBool False) _) = PBool False
     go (PAnd _ (PBool False)) = PBool False
+    go (PAnd (PBool True) x) = x
+    go (PAnd x (PBool True)) = x
     go (POr (PBool True) _) = PBool True
     go (POr _ (PBool True)) = PBool True
     go (POr (PBool l) (PBool r)) = PBool (l || r)
+    go (POr x (PBool False)) = x
+    go (POr (PBool False) x) = x
 
     -- Imply
     go (PImpl _ (PBool True)) = PBool True