Mathematical-Optimization/test_Literals.py at main · laschoe/Mathematical-Optimization · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
import unittest
from Literal import Literal, Clause, CNF


class tests_Literals(unittest.TestCase):

    def test_literal(self):
        a = Literal("a")
        b = Literal("b")
        not_a = -a
        not_b = -b

        self.assertEqual(a.__hash__(), hash(('a', False)))
        self.assertEqual(a.__repr__(), "a")
        self.assertEqual(a.evaluate({'a': True}), True)
        self.assertEqual(a.evaluate({'a': False}), False)
        self.assertEqual(a.evaluate({}), False)

        self.assertEqual(b.__hash__(), hash(('b', False)))
        self.assertEqual(b.__repr__(), "b")
        self.assertEqual(b.evaluate({'b': True}), True)
        self.assertEqual(b.evaluate({'b': False}), False)
        self.assertEqual(b.evaluate({}), False)

        self.assertEqual(not_a.__hash__(), hash(('a', True)))
        self.assertEqual(not_a.__repr__(), "~a")
        self.assertEqual(not_a.evaluate({'a': True}), False)
        self.assertEqual(not_a.evaluate({'a': False}), True)
        self.assertEqual(not_a.evaluate({}), True)

        self.assertEqual(not_b.__hash__(), hash(('b', True)))
        self.assertEqual(not_b.__repr__(), "~b")
        self.assertEqual(not_b.evaluate({'b': True}), False)
        self.assertEqual(not_b.evaluate({'b': False}), True)
        self.assertEqual(not_b.evaluate({}), True)

    def test_clause(self):
        a = Literal("a")
        b = Literal("b")
        not_a = -a
        not_b = -b

        clause = Clause({a, b})
        self.assertEqual(clause.__hash__(), hash(frozenset({a, b})))
        self.assertIn(clause.__repr__(), {"a | b", "b | a"})
        self.assertEqual(clause.evaluate({'a': True, 'b': True}), True)
        self.assertEqual(clause.evaluate({'a': True, 'b': False}), True)
        self.assertEqual(clause.evaluate({'a': False, 'b': True}), True)
        self.assertEqual(clause.evaluate({'a': False, 'b': False}), False)
        self.assertEqual(clause.evaluate({}), False)

        clause = Clause({not_a, b})
        self.assertEqual(clause.__hash__(), hash(frozenset({not_a, b})))
        self.assertIn(clause.__repr__(), {"b | ~a", "~a | b"})
        self.assertEqual(clause.evaluate({'a': True, 'b': True}), True)
        self.assertEqual(clause.evaluate({'a': True, 'b': False}), False)
        self.assertEqual(clause.evaluate({'a': False, 'b': True}), True)
        self.assertEqual(clause.evaluate({'a': False, 'b': False}), True)
        self.assertEqual(clause.evaluate({}), True)

        clause = Clause({a, not_b})
        self.assertEqual(clause.__hash__(), hash(frozenset({a, not_b})))
        self.assertIn(clause.__repr__(), {"~b | a", "a | ~b"})
        self.assertEqual(clause.evaluate({'a': True, 'b': True}), True)
        self.assertEqual(clause.evaluate({'a': True, 'b': False}), True)
        self.assertEqual(clause.evaluate({'a': False, 'b': True}), False)
        self.assertEqual(clause.evaluate({'a': False, 'b': False}), True)
        self.assertEqual(clause.evaluate({}), True)

    def test_CNF(self):
        a = Literal("a")
        b = Literal("b")
        not_a = -a
        not_b = -b

        clauses = {
            Clause({a, b}),
            Clause({not_a, b}),
            Clause({a, not_b})
        }
        cnf = CNF(clauses)
        self.assertEqual(cnf.__hash__(), hash(frozenset(clauses)))
        # not applicable, because the order of the clauses and literals is not defined
        # self.assertIn(cnf.__repr__(), {"a | b & b | ~a & a | ~b", "b | ~a & a | b & a | ~b", "b | ~a & a | ~b & a | b", ...})
        self.assertEqual(cnf.evaluate({'a': True, 'b': True}), True)
        self.assertEqual(cnf.evaluate({'a': True, 'b': False}), False)
        self.assertEqual(cnf.evaluate({'a': False, 'b': True}), False)
        self.assertEqual(cnf.evaluate({'a': False, 'b': False}), False)
        self.assertEqual(cnf.evaluate({}), False)

        clauses = {
            Clause({a, b}),
            Clause({not_a, b}),
            Clause({a, not_b}),
            Clause({not_a, not_b})
        }
        cnf = CNF(clauses)
        self.assertEqual(cnf.__hash__(), hash(frozenset(clauses)))
        # not applicable, because the order of the clauses and literals is not defined
        # self.assertIn(cnf.__repr__(), {"a | b & b | ~a & a | ~b & ~a | ~b", "b | ~a & a | b & a | ~b & ~a | ~b, ..."})
        self.assertEqual(cnf.evaluate({'a': True, 'b': True}), False)
        self.assertEqual(cnf.evaluate({'a': True, 'b': False}), False)
        self.assertEqual(cnf.evaluate({'a': False, 'b': True}), False)
        self.assertEqual(cnf.evaluate({'a': False, 'b': False}), False)
        self.assertEqual(cnf.evaluate({}), False)


if __name__ == '__main__':
    unittest.main()