-
Notifications
You must be signed in to change notification settings - Fork 1
/
hw_ply.py
169 lines (142 loc) · 4.91 KB
/
hw_ply.py
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
158
159
160
161
162
163
164
165
166
167
168
169
tokens = (
'VAR',
'CONJUNCTION', 'DISJUNCTION', 'IMPLICATION', 'NEGATION',
'LPAREN','RPAREN',
)
# Tokens
t_VAR = r'[a-z]'
t_CONJUNCTION = r'/\\'
t_DISJUNCTION = r'\\/'
t_IMPLICATION = r'->'
t_NEGATION = r'~'
t_LPAREN = r'\('
t_RPAREN = r'\)'
# Ignored characters
t_ignore = ' \t'
def t_error(t):
print("Illegal character '%s'" % t.value[0])
t.lexer.skip(1)
# Build the lexer
import ply.lex as lex
lexer = lex.lex()
class Unit:
def __init__(self, value):
self.value = value
self.negation = False
def printable(self):
return "~" + self.value if self.negation else self.value
class Clause:
def __init__(self, unit1, unit2):
self.units = [unit1, unit2]
self.tautology = False
self.satisfiable = True
if unit1.value == unit2.value:
if unit1.negation != unit2.negation:
self.tautology = True
elif unit1.value is None:
self.satisfiable = False
else:
self.units[0] = Unit(None)
def printable(self):
return r'({}\/{})'.format(self.units[0].printable(),
self.units[1].printable())
class Expression:
def __init__(self, clauses):
self.clauses = clauses
self.satisfiable = None
def print(self):
print('Resolution:', self.printable())
print('Satisfiable:', self.satisfiable)
def printable(self):
printable_clauses = []
for clause in self.clauses:
printable_clauses.append(clause.printable())
return '/\\'.join(printable_clauses)
def reduce_tautology(self):
n = len(self.clauses)
for i in range(n):
clause = self.clauses[n-i-1]
if clause.tautology: self.clauses.remove(clause)
def is_dublicate(self, new_clause):
for clause in self.clauses:
indicator = 0
for i in range(2):
for j in range(2):
if (new_clause.units[i].value == clause.units[j].value
and new_clause.units[i].negation == clause.units[j].negation):
indicator += 1
if indicator == 2:
return True
return False
def apply_resolution(self):
self.satisfiable = True
while True:
len_clauses = len(self.clauses)
clauses = list(self.clauses)
for clause_i in clauses:
for clause_j in clauses:
if clause_i == clause_j: continue
for i in range(2):
for j in range(2):
i_value = clause_i.units[i].value
j_value = clause_j.units[j].value
i_neg = clause_i.units[i].negation
j_neg = clause_j.units[j].negation
if (i_value == j_value and i_neg != j_neg):
new_clause = Clause(clause_i.units[i^1],
clause_j.units[j^1])
if not new_clause.satisfiable:
self.clauses.append(new_clause)
self.satisfiable = False
return
if (not new_clause.tautology
and not self.is_dublicate(new_clause)):
self.clauses.append(new_clause)
if len_clauses == len(self.clauses):
return
# Grammar
def p_expression_conjunction(p):
'expression : expression CONJUNCTION expression'
p[0] = Expression(p[1].clauses + p[3].clauses)
def p_expression_paren(p):
'expression : LPAREN expression RPAREN'
p[0] = p[2]
def p_expression_clause(p):
'expression : clause'
p[0] = Expression([p[1]])
def p_clause_implication(p):
'clause : unit IMPLICATION unit'
p[1].negation = not p[1].negation
p[0] = Clause(p[1], p[3])
def p_clause_disjunction(p):
'clause : unit DISJUNCTION unit'
p[0] = Clause(p[1], p[3])
def p_clause_unit(p):
'clause : unit'
p[0] = Clause(p[1], Unit(None))
def p_unit_negation(p):
'unit : NEGATION unit'
p[0] = p[2]
p[0].negation = True
def p_unit_var(p):
'unit : VAR'
p[0] = Unit(p[1])
def p_error(p):
print("Syntax error at '%s'" % p.value)
# Build the parser
import ply.yacc as yacc
parser = yacc.yacc()
# example: (p -> q) /\ (~r \/ s) /\ (~q -> p)
# example: (a\/~b)/\(b\/c)/\(~a\/c)/\(e\/~d)/\(d\/~c)/\(~e\/~c)
# example: (p->q) /\ (q->r) /\ (r->s) /\ p /\ ~s
while True:
try:
input_str = input('input > ')
except EOFError:
break
if not input_str: continue
result = parser.parse(input_str)
if result is not None:
result.reduce_tautology()
result.apply_resolution()
result.print()