/
operations.py
137 lines (92 loc) · 3.6 KB
/
operations.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
import fofTypes as f
import unification as u
from copy import deepcopy
from itertools import count
counter = count()
# helpers for unf transform
substitutions = {}
def gen_uniq_varname(variable):
return variable.name + str(next(counter))
def rewrite_binary(binary_formula, left, right, new_op):
""" Reweriting a binary operand formula, from its current op to the new op,
with negating the left and right formula, if requested"""
[ left_formula, right_formula ] = binary_formula.terms
if not left:
left_formula = left_formula.negate()
if not right:
right_formula = right_formula.negate()
return f.BinaryOperator(new_op, transform(left_formula), transform(right_formula))
def rewrite_quantor(quantor_formula, not_negated, new_quantor):
global substitutions
old = deepcopy(substitutions)
for var in quantor_formula.variables:
substitutions[var] = f.Variable(gen_uniq_varname(var))
if not_negated:
new_term = transform(quantor_formula.term)
else:
new_term = transform(quantor_formula.term.negate())
new_vars = [ u.substitute(var,substitutions) for var in quantor_formula.variables ]
substitutions = old
return f.Quantor(new_quantor, new_vars, new_term)
# basic unf transforms
def alpha(left, right):
return lambda formula: rewrite_binary(formula, left, right, "&")
def beta(left, right):
return lambda formula: rewrite_binary(formula, left, right, "|")
def gamma(not_negated):
return lambda formula: rewrite_quantor(formula, not_negated, '!')
def delta(not_negated):
return lambda formula: rewrite_quantor(formula, not_negated, '?')
# non unf transforms
def double_negation(unary_formula):
return transform(unary_formula.term.term)
def equivalance_rewrite(not_negated = True):
def inner_function(eq_formula):
[ left_formula, right_formula] = eq_formula.terms
new_formula = f.BinaryOperator('|',
f.BinaryOperator('&', left_formula, right_formula),
f.BinaryOperator('&', left_formula.negate(), right_formula.negate()))
if not_negated:
return transform(new_formula)
else:
return transform(new_formula.negate())
return inner_function
transformations = {
'&' : alpha(True, True),
'~|' : alpha(False, False),
'|' : beta(True, True),
'~|' : beta(False, False),
'=>' : beta(False, True),
'<=' : beta(True, False),
'!' : gamma(True),
'?' : delta(True),
'~' : {
'|' : alpha(False, False),
'=>' : alpha(True, False),
'<=' : alpha(False, True),
'~&' : alpha(True, True),
'&' : beta(False, False),
'~|' : beta(True, True),
'?' : gamma(False),
'!' : delta(False),
'~' : double_negation,
'<=>' : equivalance_rewrite(False),
'<~>' : equivalance_rewrite(),
},
'<=>' : equivalance_rewrite(),
'<~>' : equivalance_rewrite(False),
}
def transform(formula):
if type(formula) == f.Relation:
return transform_relation(formula)
if type(formula.negate()) == f.Relation:
return (transform_relation(formula.negate())).negate()
if type(formula) == f.UnaryOperator and formula.op == "~":
return transformations['~'][formula.term.op](formula.term)
else:
return transformations[formula.op](formula)
# transformations on terms
def transform_relation(relation):
global substitutions
terms = [ u.substitute(term, substitutions) for term in relation ]
return f.Relation(relation.name, terms)