1 | /*
|
2 | * Souffle - A Datalog Compiler
|
3 | * Copyright (c) 2021, The Souffle Developers. All rights reserved
|
4 | * Licensed under the Universal Permissive License v 1.0 as shown at:
|
5 | * - https://opensource.org/licenses/UPL
|
6 | * - <souffle root>/licenses/SOUFFLE-UPL.txt
|
7 | */
|
8 |
|
9 | /************************************************************************
|
10 | *
|
11 | * @file BinaryConstraintOps.h
|
12 | *
|
13 | * Defines binary constraint operators for AST & RAM
|
14 | *
|
15 | ***********************************************************************/
|
16 |
|
17 | #pragma once
|
18 |
|
19 | #include "souffle/TypeAttribute.h"
|
20 | #include "souffle/utility/MiscUtil.h"
|
21 | #include <iostream>
|
22 | #include <string>
|
23 | #include <vector>
|
24 |
|
25 | namespace souffle {
|
26 |
|
27 | /**
|
28 | * Binary Constraint Operators
|
29 | */
|
30 |
|
31 | // TODO (darth_tytus): Some of the constraints are repeated because of float and unsigned.
|
32 | // This is inelegant solution, but Ram execution demands this distinction.
|
33 | // Investigate a better way.
|
34 |
|
35 | enum class BinaryConstraintOp {
|
36 | EQ, // equivalence of two values
|
37 | FEQ, // float equiv; b/c NaNs are never equiv
|
38 | NE, // whether two values are different
|
39 | FNE, // float diff; b/c NaNs are always different
|
40 | LT, // signed <
|
41 | ULT, // Unsigned <
|
42 | FLT, // Float <
|
43 | SLT, // Symbol <
|
44 | LE, // signed ≤
|
45 | ULE, // Unsigned ≤
|
46 | FLE, // Float ≤
|
47 | SLE, // Symbol ≤
|
48 | GT, // signed >
|
49 | UGT, // unsigned >
|
50 | FGT, // float >
|
51 | SGT, // Symbol >
|
52 | GE, // signed ≥
|
53 | UGE, // Unsigned ≥
|
54 | FGE, // Float ≥
|
55 | SGE, // Symbol ≥
|
56 | MATCH, // matching string
|
57 | CONTAINS, // whether a sub-string is contained in a string
|
58 | NOT_MATCH, // not matching string
|
59 | NOT_CONTAINS // whether a sub-string is not contained in a string
|
60 | };
|
61 |
|
62 | char const* toBinaryConstraintSymbol(const BinaryConstraintOp op);
|
63 |
|
64 | inline std::ostream& operator<<(std::ostream& os, BinaryConstraintOp x) {
|
65 | return os << toBinaryConstraintSymbol(x);
|
66 | }
|
67 |
|
68 | inline BinaryConstraintOp getEqConstraint(const std::string& type) {
|
69 | switch (type[0]) {
|
70 | case 'f': return BinaryConstraintOp::FEQ;
|
71 | case 'u': return BinaryConstraintOp::EQ;
|
72 | case 'i': return BinaryConstraintOp::EQ;
|
73 |
|
74 | default: return BinaryConstraintOp::EQ;
|
75 | }
|
76 | }
|
77 |
|
78 | inline BinaryConstraintOp getLessEqualConstraint(const std::string& type) {
|
79 | switch (type[0]) {
|
80 | case 'f': return BinaryConstraintOp::FLE;
|
81 | case 'u': return BinaryConstraintOp::ULE;
|
82 | case 'i': return BinaryConstraintOp::LE;
|
83 |
|
84 | default: return BinaryConstraintOp::LE;
|
85 | }
|
86 | }
|
87 |
|
88 | inline BinaryConstraintOp getGreaterEqualConstraint(const std::string& type) {
|
89 | switch (type[0]) {
|
90 | case 'f': return BinaryConstraintOp::FGE;
|
91 | case 'u': return BinaryConstraintOp::UGE;
|
92 | case 'i': return BinaryConstraintOp::GE;
|
93 |
|
94 | default: return BinaryConstraintOp::GE;
|
95 | }
|
96 | }
|
97 |
|
98 | inline BinaryConstraintOp getLessThanConstraint(const std::string& type) {
|
99 | switch (type[0]) {
|
100 | case 'f': return BinaryConstraintOp::FLT;
|
101 | case 'u': return BinaryConstraintOp::ULT;
|
102 | case 'i': return BinaryConstraintOp::LT;
|
103 |
|
104 | default: return BinaryConstraintOp::LT;
|
105 | }
|
106 | }
|
107 |
|
108 | inline BinaryConstraintOp getGreaterThanConstraint(const std::string& type) {
|
109 | switch (type[0]) {
|
110 | case 'f': return BinaryConstraintOp::FGT;
|
111 | case 'u': return BinaryConstraintOp::UGT;
|
112 | case 'i': return BinaryConstraintOp::GT;
|
113 |
|
114 | default: return BinaryConstraintOp::GT;
|
115 | }
|
116 | }
|
117 |
|
118 | inline bool isEqConstraint(const BinaryConstraintOp constraintOp) {
|
119 | switch (constraintOp) {
|
120 | case BinaryConstraintOp::EQ:
|
121 | case BinaryConstraintOp::FEQ: return true;
|
122 | default: break;
|
123 | }
|
124 | return false;
|
125 | }
|
126 |
|
127 | inline bool isStrictIneqConstraint(const BinaryConstraintOp constraintOp) {
|
128 | switch (constraintOp) {
|
129 | case BinaryConstraintOp::LT:
|
130 | case BinaryConstraintOp::GT:
|
131 | case BinaryConstraintOp::ULT:
|
132 | case BinaryConstraintOp::UGT:
|
133 | case BinaryConstraintOp::FLT:
|
134 | case BinaryConstraintOp::FGT: return true;
|
135 | default: break;
|
136 | }
|
137 | return false;
|
138 | }
|
139 |
|
140 | inline bool isWeakIneqConstraint(const BinaryConstraintOp constraintOp) {
|
141 | switch (constraintOp) {
|
142 | case BinaryConstraintOp::LE:
|
143 | case BinaryConstraintOp::GE:
|
144 | case BinaryConstraintOp::ULE:
|
145 | case BinaryConstraintOp::UGE:
|
146 | case BinaryConstraintOp::FLE:
|
147 | case BinaryConstraintOp::FGE: return true;
|
148 | default: break;
|
149 | }
|
150 | return false;
|
151 | }
|
152 |
|
153 | inline bool isIneqConstraint(const BinaryConstraintOp constraintOp) {
|
154 | return isStrictIneqConstraint(constraintOp) || isWeakIneqConstraint(constraintOp);
|
155 | }
|
156 |
|
157 | inline bool isIndexableConstraint(const BinaryConstraintOp constraintOp) {
|
158 | return isIneqConstraint(constraintOp) || isEqConstraint(constraintOp);
|
159 | }
|
160 |
|
161 | inline bool isSignedInequalityConstraint(const BinaryConstraintOp constraintOp) {
|
162 | switch (constraintOp) {
|
163 | case BinaryConstraintOp::LE:
|
164 | case BinaryConstraintOp::GE:
|
165 | case BinaryConstraintOp::LT:
|
166 | case BinaryConstraintOp::GT: return true;
|
167 | default: break;
|
168 | }
|
169 | return false;
|
170 | }
|
171 |
|
172 | inline BinaryConstraintOp convertStrictToWeakIneqConstraint(const BinaryConstraintOp constraintOp) {
|
173 | assert(isStrictIneqConstraint(constraintOp));
|
174 | switch (constraintOp) {
|
175 | case BinaryConstraintOp::LT: return BinaryConstraintOp::LE;
|
176 | case BinaryConstraintOp::GT: return BinaryConstraintOp::GE;
|
177 | case BinaryConstraintOp::ULT: return BinaryConstraintOp::ULE;
|
178 | case BinaryConstraintOp::UGT: return BinaryConstraintOp::UGE;
|
179 | case BinaryConstraintOp::FLT: return BinaryConstraintOp::FLE;
|
180 | case BinaryConstraintOp::FGT: return BinaryConstraintOp::FGE;
|
181 | default: break;
|
182 | }
|
183 | return constraintOp;
|
184 | }
|
185 |
|
186 | inline BinaryConstraintOp convertStrictToNotEqualConstraint(const BinaryConstraintOp constraintOp) {
|
187 | assert(isStrictIneqConstraint(constraintOp));
|
188 | switch (constraintOp) {
|
189 | case BinaryConstraintOp::LT: return BinaryConstraintOp::NE;
|
190 | case BinaryConstraintOp::GT: return BinaryConstraintOp::NE;
|
191 | case BinaryConstraintOp::ULT: return BinaryConstraintOp::NE;
|
192 | case BinaryConstraintOp::UGT: return BinaryConstraintOp::NE;
|
193 | case BinaryConstraintOp::FLT: return BinaryConstraintOp::FNE;
|
194 | case BinaryConstraintOp::FGT: return BinaryConstraintOp::FNE;
|
195 | default: break;
|
196 | }
|
197 | return constraintOp;
|
198 | }
|
199 |
|
200 | inline bool isLessThan(const BinaryConstraintOp constraintOp) {
|
201 | switch (constraintOp) {
|
202 | case BinaryConstraintOp::LT:
|
203 | case BinaryConstraintOp::ULT:
|
204 | case BinaryConstraintOp::FLT: return true;
|
205 | default: break;
|
206 | }
|
207 | return false;
|
208 | }
|
209 |
|
210 | inline bool isGreaterThan(const BinaryConstraintOp constraintOp) {
|
211 | switch (constraintOp) {
|
212 | case BinaryConstraintOp::GT:
|
213 | case BinaryConstraintOp::UGT:
|
214 | case BinaryConstraintOp::FGT: return true;
|
215 | default: break;
|
216 | }
|
217 | return false;
|
218 | }
|
219 |
|
220 | inline bool isLessEqual(const BinaryConstraintOp constraintOp) {
|
221 | switch (constraintOp) {
|
222 | case BinaryConstraintOp::LE:
|
223 | case BinaryConstraintOp::ULE:
|
224 | case BinaryConstraintOp::FLE: return true;
|
225 | default: break;
|
226 | }
|
227 | return false;
|
228 | }
|
229 |
|
230 | inline bool isGreaterEqual(const BinaryConstraintOp constraintOp) {
|
231 | switch (constraintOp) {
|
232 | case BinaryConstraintOp::GE:
|
233 | case BinaryConstraintOp::UGE:
|
234 | case BinaryConstraintOp::FGE: return true;
|
235 | default: break;
|
236 | }
|
237 | return false;
|
238 | }
|
239 |
|
240 | /**
|
241 | * Utility function, informing whether constraint is overloaded.
|
242 | * Only the signed version's are treated as overloaded (as they are returned by the parser).
|
243 | */
|
244 | inline bool isOverloaded(const BinaryConstraintOp constraintOp) {
|
245 | switch (constraintOp) {
|
246 | case BinaryConstraintOp::EQ:
|
247 | case BinaryConstraintOp::NE:
|
248 | case BinaryConstraintOp::LT:
|
249 | case BinaryConstraintOp::LE:
|
250 | case BinaryConstraintOp::GT:
|
251 | case BinaryConstraintOp::GE: return true;
|
252 | default: break;
|
253 | }
|
254 | return false;
|
255 | }
|
256 |
|
257 | /**
|
258 | * Convert Constraint to work with requested type.
|
259 | * Example: constraintOp = LT, toType = Float -> FLT (less-than working on floats).
|
260 | */
|
261 | inline BinaryConstraintOp convertOverloadedConstraint(
|
262 | const BinaryConstraintOp constraintOp, const TypeAttribute toType) {
|
263 | auto FAIL = [&]() -> BinaryConstraintOp {
|
264 | fatal("invalid binary constraint overload: op = %s; type = %s", constraintOp, toType);
|
265 | };
|
266 |
|
267 | // clang-format off
|
268 | #define COMPARE_CONSTRAINT_FLOAT_OR_RAW(op) \
|
269 | case BinaryConstraintOp::op: \
|
270 | switch (toType) { \
|
271 | default : return BinaryConstraintOp:: op; \
|
272 | case TypeAttribute::Float : return BinaryConstraintOp::F##op; \
|
273 | }
|
274 | #define COMPARE_CONSTRAINT(op) \
|
275 | case BinaryConstraintOp::op: \
|
276 | switch (toType) { \
|
277 | case TypeAttribute::Signed : return BinaryConstraintOp:: op; \
|
278 | case TypeAttribute::Unsigned: return BinaryConstraintOp::U##op; \
|
279 | case TypeAttribute::Float : return BinaryConstraintOp::F##op; \
|
280 | case TypeAttribute::Symbol : return BinaryConstraintOp::S##op; \
|
281 | case TypeAttribute::ADT : \
|
282 | case TypeAttribute::Record : return FAIL(); \
|
283 | } \
|
284 | break; /* HACK: GCC-9 is incorrectly reporting a case fallthru */
|
285 | // clang-format on
|
286 |
|
287 | switch (constraintOp) {
|
288 | COMPARE_CONSTRAINT_FLOAT_OR_RAW(EQ)
|
289 | COMPARE_CONSTRAINT_FLOAT_OR_RAW(NE)
|
290 |
|
291 | COMPARE_CONSTRAINT(LT)
|
292 | COMPARE_CONSTRAINT(LE)
|
293 | COMPARE_CONSTRAINT(GT)
|
294 | COMPARE_CONSTRAINT(GE)
|
295 |
|
296 | default: fatal("invalid constraint conversion: constraint = %s", constraintOp);
|
297 | }
|
298 |
|
299 | UNREACHABLE_BAD_CASE_ANALYSIS
|
300 |
|
301 | #undef COMPARE_CONSTRAINT_FLOAT_OR_RAW
|
302 | #undef COMPARE_CONSTRAINT
|
303 | }
|
304 |
|
305 | /**
|
306 | * Negated Constraint Operator
|
307 | * Each operator requires a negated operator which is
|
308 | * necessary for the expansion of complex rule bodies with disjunction and negation.
|
309 | */
|
310 | inline BinaryConstraintOp negatedConstraintOp(const BinaryConstraintOp op) {
|
311 | switch (op) {
|
312 | case BinaryConstraintOp::EQ: return BinaryConstraintOp::NE;
|
313 | case BinaryConstraintOp::FEQ: return BinaryConstraintOp::FNE;
|
314 | case BinaryConstraintOp::NE: return BinaryConstraintOp::EQ;
|
315 | case BinaryConstraintOp::FNE: return BinaryConstraintOp::FEQ;
|
316 |
|
317 | case BinaryConstraintOp::LT: return BinaryConstraintOp::GE;
|
318 | case BinaryConstraintOp::ULT: return BinaryConstraintOp::UGE;
|
319 | case BinaryConstraintOp::FLT: return BinaryConstraintOp::FGE;
|
320 | case BinaryConstraintOp::SLT: return BinaryConstraintOp::SGE;
|
321 |
|
322 | case BinaryConstraintOp::LE: return BinaryConstraintOp::GT;
|
323 | case BinaryConstraintOp::ULE: return BinaryConstraintOp::UGT;
|
324 | case BinaryConstraintOp::FLE: return BinaryConstraintOp::FGT;
|
325 | case BinaryConstraintOp::SLE: return BinaryConstraintOp::SGT;
|
326 |
|
327 | case BinaryConstraintOp::GE: return BinaryConstraintOp::LT;
|
328 | case BinaryConstraintOp::UGE: return BinaryConstraintOp::ULT;
|
329 | case BinaryConstraintOp::FGE: return BinaryConstraintOp::FLT;
|
330 | case BinaryConstraintOp::SGE: return BinaryConstraintOp::SLT;
|
331 |
|
332 | case BinaryConstraintOp::GT: return BinaryConstraintOp::LE;
|
333 | case BinaryConstraintOp::UGT: return BinaryConstraintOp::ULE;
|
334 | case BinaryConstraintOp::FGT: return BinaryConstraintOp::FLE;
|
335 | case BinaryConstraintOp::SGT: return BinaryConstraintOp::SLE;
|
336 |
|
337 | case BinaryConstraintOp::MATCH: return BinaryConstraintOp::NOT_MATCH;
|
338 | case BinaryConstraintOp::NOT_MATCH: return BinaryConstraintOp::MATCH;
|
339 | case BinaryConstraintOp::CONTAINS: return BinaryConstraintOp::NOT_CONTAINS;
|
340 | case BinaryConstraintOp::NOT_CONTAINS: return BinaryConstraintOp::CONTAINS;
|
341 | }
|
342 |
|
343 | UNREACHABLE_BAD_CASE_ANALYSIS
|
344 | }
|
345 |
|
346 | /**
|
347 | * Converts operator to its symbolic representation
|
348 | */
|
349 | inline char const* toBinaryConstraintSymbol(const BinaryConstraintOp op) {
|
350 | switch (op) {
|
351 | case BinaryConstraintOp::FEQ:
|
352 | case BinaryConstraintOp::EQ: return "=";
|
353 | case BinaryConstraintOp::FNE:
|
354 | case BinaryConstraintOp::NE: return "!=";
|
355 | case BinaryConstraintOp::SLT:
|
356 | case BinaryConstraintOp::ULT:
|
357 | case BinaryConstraintOp::FLT:
|
358 | case BinaryConstraintOp::LT: return "<";
|
359 | case BinaryConstraintOp::SLE:
|
360 | case BinaryConstraintOp::ULE:
|
361 | case BinaryConstraintOp::FLE:
|
362 | case BinaryConstraintOp::LE: return "<=";
|
363 | case BinaryConstraintOp::SGT:
|
364 | case BinaryConstraintOp::UGT:
|
365 | case BinaryConstraintOp::FGT:
|
366 | case BinaryConstraintOp::GT: return ">";
|
367 | case BinaryConstraintOp::SGE:
|
368 | case BinaryConstraintOp::UGE:
|
369 | case BinaryConstraintOp::FGE:
|
370 | case BinaryConstraintOp::GE: return ">=";
|
371 | case BinaryConstraintOp::MATCH: return "match";
|
372 | case BinaryConstraintOp::CONTAINS: return "contains";
|
373 | case BinaryConstraintOp::NOT_MATCH: return "not_match";
|
374 | case BinaryConstraintOp::NOT_CONTAINS: return "not_contains";
|
375 | }
|
376 |
|
377 | UNREACHABLE_BAD_CASE_ANALYSIS
|
378 | }
|
379 |
|
380 | /**
|
381 | * Converts symbolic representation of an operator to the operator.
|
382 | * Note that this won't tell you which polymorphic overload is actually used.
|
383 | */
|
384 | inline BinaryConstraintOp toBinaryConstraintOp(const std::string& symbol) {
|
385 | if (symbol == "=") return BinaryConstraintOp::EQ;
|
386 | if (symbol == "!=") return BinaryConstraintOp::NE;
|
387 | if (symbol == "<") return BinaryConstraintOp::LT;
|
388 | if (symbol == "<=") return BinaryConstraintOp::LE;
|
389 | if (symbol == ">=") return BinaryConstraintOp::GE;
|
390 | if (symbol == ">") return BinaryConstraintOp::GT;
|
391 | if (symbol == "match") return BinaryConstraintOp::MATCH;
|
392 | if (symbol == "contains") return BinaryConstraintOp::CONTAINS;
|
393 | if (symbol == "not_match") return BinaryConstraintOp::NOT_MATCH;
|
394 | if (symbol == "not_contains") return BinaryConstraintOp::NOT_CONTAINS;
|
395 |
|
396 | fatal("unrecognised binary operator: symbol = `%s`", symbol);
|
397 | }
|
398 |
|
399 | /**
|
400 | * Determines whether arguments of constraint are orderable
|
401 | */
|
402 | inline bool isOrderedBinaryConstraintOp(const BinaryConstraintOp op) {
|
403 | switch (op) {
|
404 | case BinaryConstraintOp::EQ:
|
405 | case BinaryConstraintOp::FEQ:
|
406 | case BinaryConstraintOp::NE:
|
407 | case BinaryConstraintOp::FNE:
|
408 | case BinaryConstraintOp::LT:
|
409 | case BinaryConstraintOp::ULT:
|
410 | case BinaryConstraintOp::FLT:
|
411 | case BinaryConstraintOp::LE:
|
412 | case BinaryConstraintOp::ULE:
|
413 | case BinaryConstraintOp::FLE:
|
414 | case BinaryConstraintOp::GE:
|
415 | case BinaryConstraintOp::UGE:
|
416 | case BinaryConstraintOp::FGE:
|
417 | case BinaryConstraintOp::GT:
|
418 | case BinaryConstraintOp::UGT:
|
419 | case BinaryConstraintOp::FGT:
|
420 | case BinaryConstraintOp::SLT:
|
421 | case BinaryConstraintOp::SLE:
|
422 | case BinaryConstraintOp::SGE:
|
423 | case BinaryConstraintOp::SGT: return true;
|
424 |
|
425 | case BinaryConstraintOp::MATCH:
|
426 | case BinaryConstraintOp::NOT_MATCH:
|
427 | case BinaryConstraintOp::CONTAINS:
|
428 | case BinaryConstraintOp::NOT_CONTAINS: return false;
|
429 | }
|
430 |
|
431 | UNREACHABLE_BAD_CASE_ANALYSIS
|
432 | }
|
433 |
|
434 | /**
|
435 | * Determines whether a functor should be written using infix notation (e.g. `a + b + c`)
|
436 | * or prefix notation (e.g. `+(a,b,c)`)
|
437 | */
|
438 | inline bool isInfixFunctorOp(const BinaryConstraintOp op) {
|
439 | switch (op) {
|
440 | case BinaryConstraintOp::MATCH:
|
441 | case BinaryConstraintOp::NOT_MATCH:
|
442 | case BinaryConstraintOp::CONTAINS:
|
443 | case BinaryConstraintOp::NOT_CONTAINS: return false;
|
444 |
|
445 | default: return true;
|
446 | }
|
447 | }
|
448 |
|
449 | /**
|
450 | * Get type binary constraint operates on.
|
451 | **/
|
452 | inline std::vector<TypeAttribute> getBinaryConstraintTypes(const BinaryConstraintOp op) {
|
453 | // clang-format off
|
454 | #define COMPARE_EQUALS(op) \
|
455 | case BinaryConstraintOp::F##op: return { TypeAttribute::Float }; \
|
456 | case BinaryConstraintOp:: op: \
|
457 | return { TypeAttribute::Signed, TypeAttribute::Unsigned, TypeAttribute::Float, \
|
458 | TypeAttribute::Symbol, TypeAttribute::Record, TypeAttribute::ADT};
|
459 | #define COMPARE_OP(op) \
|
460 | case BinaryConstraintOp:: op: return { TypeAttribute::Signed }; \
|
461 | case BinaryConstraintOp::U##op: return { TypeAttribute::Unsigned }; \
|
462 | case BinaryConstraintOp::F##op: return { TypeAttribute::Float }; \
|
463 | case BinaryConstraintOp::S##op: return { TypeAttribute::Symbol };
|
464 | // clang-format on
|
465 |
|
466 | switch (op) {
|
467 | COMPARE_EQUALS(EQ)
|
468 | COMPARE_EQUALS(NE)
|
469 | COMPARE_OP(LT)
|
470 | COMPARE_OP(LE)
|
471 | COMPARE_OP(GT)
|
472 | COMPARE_OP(GE)
|
473 |
|
474 | case BinaryConstraintOp::MATCH:
|
475 | case BinaryConstraintOp::NOT_MATCH:
|
476 | case BinaryConstraintOp::CONTAINS:
|
477 | case BinaryConstraintOp::NOT_CONTAINS: return {TypeAttribute::Symbol};
|
478 | }
|
479 |
|
480 | UNREACHABLE_BAD_CASE_ANALYSIS
|
481 |
|
482 | #undef COMPARE_EQUALS
|
483 | #undef COMPARE_OP
|
484 | }
|
485 |
|
486 | } // end of namespace souffle
|