Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Newer
Older
100644 146 lines (98 sloc) 3.249 kb
4e41d53 Yves Müller split into parser and types module
authored
1 from pyparsing import *
2
035ee9c Michael Wittig fofTypes
Sh4kE authored
3 class Formula(object):
2f22d42 Yves Müller add negate method
authored
4
5 def negate(self):
507889c Yves Müller add python2 support
authored
6 return UnaryOperator("~", self)
2f22d42 Yves Müller add negate method
authored
7
d0d305c Yves Müller rewrite parser for first order
authored
8 def __eq__(self,other):
9 return repr(self) == repr(other)
10
035ee9c Michael Wittig fofTypes
Sh4kE authored
11 class Term(Formula):
7e2d5ba Yves Müller add iter to foftypes
authored
12 pass
035ee9c Michael Wittig fofTypes
Sh4kE authored
13
806e9b4 Michael Wittig renamed *Operand to *Operator
Sh4kE authored
14 class UnaryOperator(Formula):
9477395 Updates and stuff
Marco Ziener authored
15 # Since we only have 1 unary operation we can safely assume it is a negation
d0d305c Yves Müller rewrite parser for first order
authored
16 def __init__(self, op, term):
7e2d5ba Yves Müller add iter to foftypes
authored
17 # if len(terms) > 1 something went wrong
d0d305c Yves Müller rewrite parser for first order
authored
18 self.term = term
7e2d5ba Yves Müller add iter to foftypes
authored
19 self.op = op
4e41d53 Yves Müller split into parser and types module
authored
20
21 def __repr__(self):
2f22d42 Yves Müller add negate method
authored
22 return self.op + repr(self.term)
4e41d53 Yves Müller split into parser and types module
authored
23
85c9314 Michael Wittig added equality to nodes
Sh4kE authored
24 def __eq__(self,other):
5dff17e Yves Müller fix tab error
authored
25 return repr(self) == repr(other)
85c9314 Michael Wittig added equality to nodes
Sh4kE authored
26
87824bd hash
Marco Ziener authored
27 def __hash__(self):
7a48cf6 Yves Müller add hash function for fofTypes
authored
28 return hash(self.op) ^ hash(self.term)
87824bd hash
Marco Ziener authored
29
2f22d42 Yves Müller add negate method
authored
30 def negate(self):
31 return self.term
32
7e2d5ba Yves Müller add iter to foftypes
authored
33 def __iter__(self):
34 return iter([self.term])
35
806e9b4 Michael Wittig renamed *Operand to *Operator
Sh4kE authored
36 class BinaryOperator(Formula):
4e41d53 Yves Müller split into parser and types module
authored
37
848de12 Yves Müller change fof data types constructor
authored
38 def __init__(self, op, left_term, right_term):
39 self.terms = (left_term, right_term)
4e41d53 Yves Müller split into parser and types module
authored
40 self.op = op
41
42 def __repr__(self):
43 return "(" + repr(self.terms[0]) + " " + self.op + " " + repr(self.terms[1]) + ")"
85c9314 Michael Wittig added equality to nodes
Sh4kE authored
44 def __eq__(self,other):
5dff17e Yves Müller fix tab error
authored
45 return repr(self) == repr(other)
85c9314 Michael Wittig added equality to nodes
Sh4kE authored
46
87824bd hash
Marco Ziener authored
47 def __hash__(self):
7a48cf6 Yves Müller add hash function for fofTypes
authored
48 return hash(self.op) ^ hash(self.terms)
87824bd hash
Marco Ziener authored
49
7e2d5ba Yves Müller add iter to foftypes
authored
50 def __iter__(self):
51 return iter(self.terms)
9bbbddc Yves Müller remove long running timer problem, improve api and parse quantors
authored
52
d0d305c Yves Müller rewrite parser for first order
authored
53 class Quantor(Formula):
54
55 def __init__(self, op, list_of_vars, term):
56 self.op = op
57 self.variables = frozenset(list_of_vars)
58 self.term = term
59
60 def __repr__(self):
61 return self.op + repr(list(self.variables)) + ":" + repr(self.term)
62
63 def __iter__(self):
64 return iter([self.term])
65
66 def __hash__(self):
67 return hash(self.op) ^ hash(self.term) ^ hash(self.variables)
68
035ee9c Michael Wittig fofTypes
Sh4kE authored
69 class Relation(Formula):
7a48cf6 Yves Müller add hash function for fofTypes
authored
70
507889c Yves Müller add python2 support
authored
71 def __init__(self,name,terms=[]):
7e2d5ba Yves Müller add iter to foftypes
authored
72 """ terms is a list of terms.
73 Like in lecture, containing constants,
74 variables and other terms """
75 self.name = name
035ee9c Michael Wittig fofTypes
Sh4kE authored
76 self.terms = terms
9bbbddc Yves Müller remove long running timer problem, improve api and parse quantors
authored
77
035ee9c Michael Wittig fofTypes
Sh4kE authored
78 def __repr__(self):
d0d305c Yves Müller rewrite parser for first order
authored
79
80 if len(self.terms) == 0:
81 return self.name
82
83 else:
84 return self.name + "(" + ",".join(map(repr,self.terms)) + ")"
035ee9c Michael Wittig fofTypes
Sh4kE authored
85
86 def __eq__(self,other):
87 return repr(self) == repr(other)
88
7e2d5ba Yves Müller add iter to foftypes
authored
89 def __iter__(self):
90 return iter(self.terms)
91
4694b0b Yves Müller add hash implementation to fof funtions and relations
authored
92 def __hash__(self):
93 h = hash(self.name)
94
95 for t in self.terms:
96 h ^= hash(t)
97
98 return h
99
035ee9c Michael Wittig fofTypes
Sh4kE authored
100 class Function(Term):
101
507889c Yves Müller add python2 support
authored
102 def __init__(self,name,terms=[]):
7e2d5ba Yves Müller add iter to foftypes
authored
103 """ terms is a list of terms.
104 Like in lecture, containing constants,
105 variables and other terms """
106 self.name = name
035ee9c Michael Wittig fofTypes
Sh4kE authored
107 self.terms = terms
9bbbddc Yves Müller remove long running timer problem, improve api and parse quantors
authored
108
507889c Yves Müller add python2 support
authored
109 def __repr__(self):
110
111 if len(self.terms) == 0:
112 return self.name
113
114 else:
115 return self.name + "(" + ",".join(map(repr,self.terms)) + ")"
9bbbddc Yves Müller remove long running timer problem, improve api and parse quantors
authored
116
117 def __eq__(self,other):
118 return repr(self) == repr(other)
119
7e2d5ba Yves Müller add iter to foftypes
authored
120 def __iter__(self):
121 return iter(self.terms)
035ee9c Michael Wittig fofTypes
Sh4kE authored
122
4694b0b Yves Müller add hash implementation to fof funtions and relations
authored
123 def __hash__(self):
124 h = hash(self.name)
125
126 for t in self.terms:
127 h ^= hash(t)
128
129 return h
130
035ee9c Michael Wittig fofTypes
Sh4kE authored
131
132 class Variable(Term):
9bbbddc Yves Müller remove long running timer problem, improve api and parse quantors
authored
133
134 def __init__(self, string):
135 self.name = string
136
137 def __repr__(self):
138 return self.name
139
d0d305c Yves Müller rewrite parser for first order
authored
140 def __hash__(self):
141 return hash(self.name)
142
9bbbddc Yves Müller remove long running timer problem, improve api and parse quantors
authored
143 def __eq__(self,other):
144 return repr(self) == repr(other)
145
Something went wrong with that request. Please try again.