x | !x -> True (#12090)

This commit is contained in:
Sieds Lykles
2025-09-10 03:26:01 +02:00
committed by GitHub
parent 5b73076e48
commit 499f50483b
2 changed files with 12 additions and 0 deletions

View File

@@ -374,6 +374,16 @@ class TestSymbolic(unittest.TestCase):
def test_and_remove(self):
self.helper_test_variable(uand([uconst(1), Variable("a", 0, 1)]), 0, 1, "a")
def test_bool_or_not_tautology(self):
a = Variable("a", 0, 10)
c = a<10
self.helper_test_variable(c | c.logical_not(), True, True, "True")
def test_bool_and_not_contradiction(self):
a = Variable("a", 0, 10)
c = a<10
self.helper_test_variable(c & c.logical_not(), False, False, "False")
def test_mod_factor_negative(self):
self.helper_test_variable(usum([uconst(-29), Variable("a", 0, 10), Variable("b", 0, 10)*28]) % 28, -27, 27, "(((a+(b*28))+-29)%28)")
self.helper_test_variable(usum([uconst(-29), Variable("a", 0, 100), Variable("b", 0, 10)*28]) % 28, -27, 27, "(((a+(b*28))+-29)%28)")

View File

@@ -289,6 +289,8 @@ commutative = PatternMatcher([
symbolic = symbolic_simple+commutative+PatternMatcher([
# ** boolean algebra **
(UPat.var("x") | (UPat.var("x") & UPat.var()), lambda x: x), # x|(x&y) -> x
# TODO: make a more general or folder like simplify_valid
(UPat.var("x", dtype=dtypes.bool) | UPat.var("x").logical_not(), lambda x: x.const_like(True)), # x|!x -> True
# ** combine terms **
(UPat.var("x") * UPat.cvar("c0") + UPat.var("x") * UPat.cvar("c1"), lambda x,c0,c1: x*(c0+c1)), # (x*c0)+(x*c1) -> x*(c0+c1)
((UPat.var("y") + UPat.var("x") * UPat.cvar("c0")) + UPat.var("x") * UPat.cvar("c1"), lambda x,y,c0,c1: y+x*(c0+c1)),