1 | % evaluate ProB AST predicates | |
2 | ||
3 | :- use_module(library(lists),[is_list/1]). | |
4 | :- use_module(library(sets)). | |
5 | ||
6 | pint(b(truth,pred,_),true). | |
7 | pint(b(falsity,pred,_),false). | |
8 | ||
9 | % conjunct, disjunct, implication, equivalence | |
10 | pint(b(conjunct(Pred1,Pred2),pred,_),Value) :- | |
11 | pint(Pred1,Value1) , | |
12 | pint(Pred2,Value2) , | |
13 | (Value1 , Value2 | |
14 | -> Value = true | |
15 | ; Value = false). | |
16 | pint(b(disjunct(Pred1,Pred2),pred,_),Value) :- | |
17 | pint(Pred1,Value1) , | |
18 | pint(Pred2,Value2) , | |
19 | ((Value1 ; Value2) | |
20 | -> Value = true | |
21 | ; Value = false). | |
22 | pint(b(implication(Pred1,Pred2),pred,_),Value) :- | |
23 | pint(Pred1,Res1) , | |
24 | pint(Pred2,Res2) , | |
25 | ((\+Res1 ; Res2) | |
26 | -> Value = true | |
27 | ; Value = false). | |
28 | pint(b(equivalence(Pred1,Pred2),pred,_),Value) :- | |
29 | pint(Pred1,Res1) , | |
30 | pint(Pred2,Res2) , | |
31 | (Res1 = Res2 | |
32 | -> Value = true | |
33 | ; Value = false). | |
34 | pint(b(negation(Pred),pred,_),Value) :- | |
35 | pint(Pred,Temp) , | |
36 | (Temp | |
37 | -> Value = false | |
38 | ; Value = true). | |
39 | ||
40 | %%%%%%%%%%%% | |
41 | pint(b(finite(_),pred,_),true). | |
42 | %%%%%%%%%%%% | |
43 | ||
44 | % equal, not_equal | |
45 | pint(b(equal(b(value(Set1),_,_),b(value(Set2),_,_)),pred,_),true) :- | |
46 | Set1 == Set2. | |
47 | pint(b(equal(b(value(Set1),_,_),b(value(Set2),_,_)),pred,_),false) :- | |
48 | Set1 \== Set2. | |
49 | pint(b(equal(b(set_extension(Set1),_,_),b(set_extension(Set2),_,_)),pred,_),true) :- | |
50 | Set1 == Set2. | |
51 | pint(b(equal(b(set_extension(Set1),_,_),b(set_extension(Set2),_,_)),pred,_),false) :- | |
52 | Set1 \== Set2. | |
53 | ||
54 | pint(b(equal(b(Expr1,integer,_),b(Expr2,integer,_)),pred,_),true) :- | |
55 | int(Expr1,Value1) , | |
56 | int(Expr2,Value2) , | |
57 | Value1 == Value2. | |
58 | pint(b(equal(b(Expr1,integer,_),b(Expr2,integer,_)),pred,_),false) :- | |
59 | int(Expr1,Value1) , | |
60 | int(Expr2,Value2) , | |
61 | Value1 \== Value2. | |
62 | ||
63 | pint(b(equal(Set1,Set2),pred,_),true) :- | |
64 | Set1 == Set2. | |
65 | pint(b(equal(Set1,Set2),pred,_),false) :- | |
66 | Set1 \== Set2. | |
67 | ||
68 | pint(b(not_equal(Pred1,Pred2),pred,_),true) :- | |
69 | pint(b(equal(Pred1,Pred2),pred,_),false). | |
70 | pint(b(not_equal(Pred1,Pred2),pred,_),false) :- | |
71 | pint(b(equal(Pred1,Pred2),pred,_),true). | |
72 | ||
73 | % less, less_equal, greater, greater_equal | |
74 | pint(b(less_equal(Expr1,Expr2),pred,_),Value) :- | |
75 | int(Expr1,Value1) , | |
76 | int(Expr2,Value2) , | |
77 | (Value1 =< Value2 | |
78 | -> Value = true | |
79 | ; Value = false). | |
80 | pint(b(less(Expr1,Expr2),pred,_),Value) :- | |
81 | int(Expr1,Value1) , | |
82 | int(Expr2,Value2) , | |
83 | (Value1 < Value2 | |
84 | -> Value = true | |
85 | ; Value = false). | |
86 | pint(b(greater_equal(Expr1,Expr2),pred,_),Value) :- | |
87 | int(Expr1,Value1) , | |
88 | int(Expr2,Value2) , | |
89 | (Value1 >= Value2 | |
90 | -> Value = true | |
91 | ; Value = false). | |
92 | pint(b(greater(Expr1,Expr2),pred,_),Value) :- | |
93 | int(Expr1,Value1) , | |
94 | int(Expr2,Value2) , | |
95 | (Value1 > Value2 | |
96 | -> Value = true | |
97 | ; Value = false). | |
98 | ||
99 | % member, not_member | |
100 | pint(b(member(Set,SetOfSet),pred,_),Value) :- | |
101 | Set = b(_,set(_),_) , | |
102 | SetOfSet = b(_,set(set(_)),_) , | |
103 | sint(Set,ValueList) , | |
104 | sint(SetOfSet,SetValue) , | |
105 | (member(ValueList,SetValue) | |
106 | -> Value = true | |
107 | ; Value = false). | |
108 | pint(b(member(b(Elm,integer,_),b(set_extension(Set),_,_)),pred,_),Value) :- | |
109 | maplist(ast_to_value,Set,List) , | |
110 | int(b(Elm,_,_),ElmValue) , | |
111 | (member(ElmValue,List) | |
112 | -> Value = true | |
113 | ; Value = false). | |
114 | pint(b(member(b(Elm,integer,_),b(set_extension(Set),_,_)),pred,_),Value) :- | |
115 | int(b(Elm,_,_),ElmValue) , | |
116 | (member(ElmValue,Set) | |
117 | -> Value = true | |
118 | ; Value = false). | |
119 | % value list set | |
120 | pint(b(member(b(Elm,integer,_),b(value(Set),_,_)),pred,_),Value) :- | |
121 | is_list(Set) , | |
122 | int(b(Elm,_,_),ElmValue) , | |
123 | (member(ElmValue,Set) | |
124 | -> Value = true | |
125 | ; Value = false). | |
126 | % value avl set | |
127 | pint(b(member(b(Elm,integer,_),b(value(avl_set(Set)),_,_)),pred,_),Value) :- | |
128 | int(b(Elm,_,_),ElmValue) , | |
129 | avl_to_list(Set,TempList) , | |
130 | findall(Key,member(Key-_,TempList),List) , | |
131 | (member(ElmValue,List) | |
132 | -> Value = true | |
133 | ; Value = false). | |
134 | pint(b(member(b(Elm,_,_),b(set_extension(Set),_,_)),pred,_),Value) :- | |
135 | maplist(ast_to_value,Set,List) , | |
136 | sint(b(Elm,_,_),ElmValue) , | |
137 | (member(ElmValue,List) | |
138 | -> Value = true | |
139 | ; Value = false). | |
140 | pint(b(member(b(Elm,_,_),b(set_extension(Set),_,_)),pred,_),Value) :- | |
141 | sint(b(Elm,_,_),ElmValue) , | |
142 | (member(ElmValue,Set) | |
143 | -> Value = true | |
144 | ; Value = false). | |
145 | % value list set | |
146 | pint(b(member(b(Elm,_,_),b(value(Set),_,_)),pred,_),Value) :- | |
147 | is_list(Set) , | |
148 | sint(b(Elm,_,_),ElmValue) , | |
149 | (member(ElmValue,Set) | |
150 | -> Value = true | |
151 | ; Value = false). | |
152 | % value avl set | |
153 | pint(b(member(b(Elm,_,_),b(value(avl_set(Set)),_,_)),pred,_),Value) :- | |
154 | sint(b(Elm,_,_),ElmValue) , | |
155 | avl_to_list(Set,TempList) , | |
156 | findall(Key,member(Key-_,TempList),List) , | |
157 | (member(ElmValue,List) | |
158 | -> Value = true | |
159 | ; Value = false). | |
160 | ||
161 | pint(b(not_member(Elm,Set),pred,_),Value) :- | |
162 | pint(b(member(Elm,Set),pred,_),R) , | |
163 | (R = true | |
164 | -> Value = false | |
165 | ; Value = true). | |
166 | ||
167 | % subset, not_subset, | |
168 | pint(b(subset(Set1,Set2),pred,_),Value) :- | |
169 | sint(Set1,ValueSet1) , | |
170 | sint(Set2,ValueSet2) , | |
171 | (subset(ValueSet1,ValueSet2) | |
172 | -> Value = true | |
173 | ; Value = false). | |
174 | pint(b(not_subset(Set1,Set2),pred,_),Value) :- | |
175 | sint(Set1,ValueSet1) , | |
176 | sint(Set2,ValueSet2) , | |
177 | (\+subset(ValueSet1,ValueSet2) | |
178 | -> Value = true | |
179 | ; Value = false). | |
180 | ||
181 | % subset_strict, not_subset_strict | |
182 | pint(b(subset_strict(Set1,Set2),pred,_),Value) :- | |
183 | sint(Set1,ValueSet1) , | |
184 | sint(Set2,ValueSet2) , | |
185 | (subset_strict(ValueSet1,ValueSet2) | |
186 | -> Value = true | |
187 | ; Value = false). | |
188 | pint(b(not_subset_strict(Set1,Set2),pred,_),Value) :- | |
189 | sint(Set1,ValueSet1) , | |
190 | sint(Set2,ValueSet2) , | |
191 | (subset(ValueSet1,ValueSet2) | |
192 | -> Value = false | |
193 | ; Value = true). | |
194 | ||
195 | %%% placeholder, needs some improvement | |
196 | pint(b(exists(_,_),_,_),true). | |
197 | pint(b(forall(_,_,_),_,_),true). | |
198 | ||
199 | % check if set is strict subset | |
200 | subset_strict([],[]). | |
201 | subset_strict(Subset,Set) :- | |
202 | append(Subset,_,Set). | |
203 | subset_strict(Set,[_|T]) :- | |
204 | subset_strict(Set,T). |