Skip to content

Commit

Permalink
implies tests
Browse files Browse the repository at this point in the history
  • Loading branch information
Wout4 committed Sep 21, 2023
1 parent f39dde4 commit ab967ac
Showing 1 changed file with 9 additions and 2 deletions.
11 changes: 9 additions & 2 deletions tests/test_trans_simplify.py
Original file line number Diff line number Diff line change
Expand Up @@ -108,5 +108,12 @@ def test_normalize(self):
self.assertEqual(str(normalize_boolexpr([a | (b.implies(c.implies(d))) | e])),'[or([BV0, ~BV1, ~BV2, BV3, BV4])]')
self.assertEqual(str(normalize_boolexpr([a | ((b.implies(f)).implies(c.implies(d))) | e])),'[or([BV0, BV1, ~BV2, BV3, BV4]), or([BV0, ~BV5, ~BV2, BV3, BV4])]')
self.assertEqual(str(normalize_boolexpr([a | ((b.implies(f)).implies(c)) | e])),'[or([BV0, BV1, BV2, BV4]), or([BV0, ~BV5, BV2, BV4])]')
self.assertEqual(str(normalize_boolexpr([a | ((b.implies(f)).implies(c & d)) | e])),'[or([BV0, BV1, BV2, BV4]), or([BV0, BV1, BV3, BV4]), or([BV0, ~BV5, BV2, '
'BV4]), or([BV0, ~BV5, BV3, BV4])]')
self.assertEqual(str(normalize_boolexpr([a | ((b.implies(f)).implies(c & d)) | e])),
('[or([BV0, BV1, BV2, BV4]), or([BV0, BV1, BV3, BV4]), or([BV0, ~BV5, BV2, '
'BV4]), or([BV0, ~BV5, BV3, BV4])]'))
self.assertEqual(str(normalize_boolexpr([b.implies(f & a & c)])),'[(BV1) -> (BV5), (BV1) -> (BV0), (BV1) -> (BV2)]')
self.assertEqual(str(normalize_boolexpr([(b | d).implies(f)])),'[(~BV5) -> (~BV1), (~BV5) -> (~BV3)]')
self.assertEqual(str(normalize_boolexpr([(b | d).implies(f & a & c)])),
('[(~BV5) -> (~BV1), (~BV5) -> (~BV3), (~BV0) -> (~BV1), (~BV0) -> (~BV3), '
'(~BV2) -> (~BV1), (~BV2) -> (~BV3)]'))
self.assertEqual(str(normalize_boolexpr([(b.implies(c)).implies(f & a)])),('[(~BV5) -> (BV1), (~BV5) -> (~BV2), (~BV0) -> (BV1), (~BV0) -> (~BV2)]'))

0 comments on commit ab967ac

Please sign in to comment.