LogicalEquivalency/extra_formulas.py at master · OpenReasoning/LogicalEquivalency · 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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
# -*- coding: utf-8 -*-
"""
These should be moved into the main forseti package most likely as they are useful
in a variety of contexts
"""
from copy import deepcopy
from forseti.formula import Formula, LogicalOperator, And, Or


class GeneralizedAnd(LogicalOperator):
    def __init__(self, *kwargs):
        if len(kwargs) < 2:
            raise Exception("Need to have at least 2 arguments")
        super(GeneralizedAnd, self).__init__(*kwargs)
        for kwarg in kwargs:
            if isinstance(kwarg, And) or isinstance(kwarg, GeneralizedAnd):
                for arg in kwarg.args:
                    self.args.append(arg)
            else:
                self.args.append(kwarg)

    def __repr__(self):
        return "and(" + ", ".join([repr(arg) for arg in self.args]) + ")"

    def __str__(self):
        return "(" + " & ".join([str(arg) for arg in self.args]) + ")"

    def __eq__(self, other):
        if not isinstance(other, GeneralizedAnd):
            return False
        test = deepcopy(self.args)
        i = 0
        while i < len(test):
            for j in other.args:
                if j == test[i]:
                    del test[i]
                    i -= 1
                    break
            i += 1
        return len(test) == 0

    def __lt__(self, other):
        if not isinstance(other, GeneralizedAnd):
            raise TypeError("Can only compare GeneralizedAnd together. Got type '%s'." % type(other))

        if len(self.args) < len(other.args):
            return True
        elif len(self.args) > len(other.args):
            return False
        else:
            i = 0
            while i < len(self.args):
                if self.args[i] < other.args[i]:
                    return True
                elif other.args[i] < self.args[i]:
                    return False
                i += 1
        return True

    def __gt__(self, other):
        if not isinstance(other, GeneralizedAnd):
            raise TypeError("Can only compare GeneralizedAnd together. Got type '%s'." % type(other))

        if len(self.args) < len(other.args):
            return True
        elif len(self.args) > len(other.args):
            return False
        else:
            i = 0
            while i < len(self.args):
                if self.args[i] > other.args[i]:
                    return True
                i += 1
        return False


class GeneralizedOr(LogicalOperator):
    def __init__(self, *kwargs):
        if len(kwargs) < 2:
            raise Exception("Need to have at least 2 arguments")
        super(GeneralizedOr, self).__init__(*kwargs)
        for kwarg in kwargs:
            if isinstance(kwarg, Or) or isinstance(kwarg, GeneralizedOr):
                for arg in kwarg.args:
                    self.args.append(arg)
            else:
                self.args.append(kwarg)

    def __repr__(self):
        return "or(" + ", ".join([repr(arg) for arg in self.args]) + ")"

    def __str__(self):
        return "(" + " | ".join([str(arg) for arg in self.args]) + ")"


class Contradiction(Formula):
    def __init__(self):
        super(Contradiction, self).__init__()

    def __repr__(self):
        return "FALSE"

    def __str__(self):
        return "⊥"

    def __eq__(self, other):
        if isinstance(other, Contradiction):
            return True
        else:
            return False

    def __ne__(self, other):
        return not (self == other)

    def __gt__(self, other):
        return False

    def __ge__(self, other):
        pass

    def __lt__(self, other):
        pass

    def __le__(self, other):
        pass


class Tautology(Formula):
    def __init__(self):
        super(Tautology, self).__init__()

    def __repr__(self):
        return "TRUE"

    def __str__(self):
        return "T"

    def __eq__(self, other):
        if isinstance(other, Contradiction):
            return True
        else:
            return False

    def __ne__(self, other):
        return not (self == other)

    def __gt__(self, other):
        return False

    def __ge__(self, other):
        pass

    def __lt__(self, other):
        pass

    def __le__(self, other):
        pass