| Sapan Bhatia | 3e3c1cd | 2017-07-15 01:35:44 -0400 | [diff] [blame] | 1 | import unittest |
| 2 | from xosgenx.jinja2_extensions.fol2 import FOL2Python |
| 3 | import pdb |
| 4 | |
| 5 | class XProtoOptimizeTest(unittest.TestCase): |
| 6 | def setUp(self): |
| 7 | self.f2p = FOL2Python() |
| 8 | |
| 9 | def test_constant(self): |
| 10 | input = 'True' |
| 11 | output = self.f2p.hoist_constants(input) |
| 12 | self.assertEqual(output, input) |
| 13 | |
| 14 | def test_exists(self): |
| 15 | input = {'exists': ['x',{'|':['x','y']}]} |
| 16 | |
| 17 | output = self.f2p.hoist_constants(input) |
| 18 | expected = {'|': ['y', {'exists': ['x', 'x']}]} |
| 19 | self.assertEqual(output, expected) |
| 20 | |
| 21 | def test_forall(self): |
| 22 | input = {'forall': ['x',{'|':['x','y']}]} |
| 23 | |
| 24 | output = self.f2p.hoist_constants(input) |
| 25 | expected = {'|': ['y', {'forall': ['x', 'x']}]} |
| 26 | self.assertEqual(output, expected) |
| 27 | |
| 28 | def test_exists_embedded(self): |
| 29 | input = {'|':['True',{'exists': ['x',{'|':['x','y']}]}]} |
| 30 | |
| 31 | output = self.f2p.hoist_constants(input) |
| 32 | expected = {'|': ['True', {'|': ['y', {'exists': ['x', 'x']}]}]} |
| 33 | self.assertEqual(output, expected) |
| 34 | |
| 35 | def test_exists_equals(self): |
| 36 | input = {'|':['True',{'exists': ['x',{'|':['x',{'=':['y','z']}]}]}]} |
| 37 | |
| 38 | output = self.f2p.hoist_constants(input) |
| 39 | expected = {'|': ['True', {'|': [{'=': ['y', 'z']}, {'exists': ['x', 'x']}]}]} |
| 40 | self.assertEqual(output, expected) |
| 41 | |
| 42 | def test_exists_nested_constant(self): |
| 43 | input = {'|':['True',{'exists': ['x',{'|':['y',{'=':['y','x']}]}]}]} |
| 44 | |
| 45 | output = self.f2p.hoist_constants(input) |
| 46 | expected = {'|': ['True', {'|': ['y', {'exists': ['x', {'=': ['y', 'x']}]}]}]} |
| 47 | self.assertEqual(output, expected) |
| 48 | |
| 49 | def test_exists_nested(self): |
| 50 | input = {'exists': ['x',{'exists':['y',{'=':['y','x']}]}]} |
| 51 | |
| 52 | output = self.f2p.hoist_constants(input) |
| 53 | expected = {'exists': ['x', {'exists': ['y', {'=': ['y', 'x']}]}]} |
| 54 | self.assertEqual(output, expected) |
| 55 | |
| 56 | def test_exists_nested2(self): |
| 57 | input = {'exists': ['x',{'exists':['y',{'=':['z','y']}]}]} |
| 58 | |
| 59 | output = self.f2p.hoist_constants(input) |
| 60 | expected = {'exists': ['y', {'=': ['z', 'y']}]} |
| 61 | self.assertEqual(output, expected) |
| 62 | |
| 63 | def test_exists_nested3(self): |
| 64 | input = {'exists': ['x',{'exists':['y',{'=':['z','x']}]}]} |
| 65 | |
| 66 | output = self.f2p.hoist_constants(input) |
| 67 | expected = {'exists': ['x', {'=': ['z', 'x']}]} |
| 68 | self.assertEqual(output, expected) |
| 69 | |
| 70 | |
| 71 | if __name__ == '__main__': |
| 72 | unittest.main() |
| 73 | |
| 74 | |