Skip to content

Commit ab3486f

Browse files
authored
add back sym_or_bits simplification (#147)
1 parent 25bc43e commit ab3486f

File tree

2 files changed

+88
-85
lines changed

2 files changed

+88
-85
lines changed

libASL/symbolic.ml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -606,6 +606,9 @@ and sym_or_bits loc w (x: sym) (y: sym) =
606606
| x, Val y when is_one_bits y -> Val y
607607
| Val x, y when is_zero_bits x -> y
608608
| x, Val y when is_zero_bits y -> x
609+
(* (a /\ b) \/ !a ~> b \/ !a *)
610+
| Exp (Expr_TApply (FIdent ("and_bits", 0), _, [a; x])), Exp (Expr_TApply (FIdent ("not_bits", 0), _, [a'])) when a = a' ->
611+
sym_or_bits loc w (sym_of_expr x) y
609612
| _ -> Exp (Expr_TApply (FIdent ("or_bits", 0), [w], [sym_expr x; sym_expr y]) )
610613

611614
and sym_eq_bits loc (x: sym) (y: sym) =

0 commit comments

Comments
 (0)