frozenleaves/pytorch
1
0
Fork 0
mirror of https://github.com/pytorch/pytorch.git synced 2025-10-20 21:14:14 +08:00
Code Issues Packages Projects Releases Wiki Activity

[dynamo] add SymNode bitwise and/or (#138777)

Browse Source 
Fixes [T203472723](https://www.internalfb.com/intern/tasks/?t=203472723)

Pull Request resolved: https://github.com/pytorch/pytorch/pull/138777
Approved by: https://github.com/ezyang
This commit is contained in:
William Wen
2024-11-22 11:00:51 -08:00
committed by PyTorch MergeBot
parent a8c90e5140
commit ee7eaad5c3
13 changed files with 324 additions and 17 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
test/test_fx_experimental.py
View File

@ -1747,7 +1747,7 @@ if TEST_Z3:
import torch._dynamo.config
from torch.fx.experimental.validator import SympyToZ3, TranslationValidator, ValidationException, z3str
from torch.utils._sympy.functions import FloorDiv, Mod
from torch.utils._sympy.functions import FloorDiv, Mod, BitwiseFn_bitwise_and
class TestTranslationValidation(TestCase):
def _prepare_for_translation_validation(self):
@ -1801,6 +1801,8 @@ if TEST_Z3:
(sympy.Ge, operator.ge),
)
],
# Bitwise operations.
(BitwiseFn_bitwise_and(s0, s1), z3.BV2Int(z3.Int2BV(z0, 64) & z3.Int2BV(z1, 64))),
# Other operations.
(
s0 - s1,
@ -1847,6 +1849,18 @@ if TEST_Z3:
validator.validate()
def test_sat_bitwise(self):
(
(s0, s1, s2),
(z0, z1, z2),
validator,
) = self._prepare_for_translation_validation()
validator.add_source_expr(z3.BV2Int(z3.Int2BV(z0, 64) & z3.Int2BV(z1, 64)) == 5)
validator.add_source_expr(z0 == 0b110101)
validator.validate()
def test_unsat(self):
(
(s0, s1, s2),