1 /* Part of SWI-Prolog
2
3 Author: Kuniaki Mukai Wielemaker
4 E-mail: mukai@sfc.keio.ac.jp
5 WWW: http://www.swi-prolog.org
6 Copyright (c) 2011-2016, Kuniaki Mukai
7 All rights reserved.
8
9 Redistribution and use in source and binary forms, with or without
10 modification, are permitted provided that the following conditions
11 are met:
12
13 1. Redistributions of source code must retain the above copyright
14 notice, this list of conditions and the following disclaimer.
15
16 2. Redistributions in binary form must reproduce the above copyright
17 notice, this list of conditions and the following disclaimer in
18 the documentation and/or other materials provided with the
19 distribution.
20
21 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
22 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
23 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
24 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
25 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
26 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
27 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
28 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
29 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
30 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
31 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
32 POSSIBILITY OF SUCH DAMAGE.
33 */
34
35 /*#define O_DEBUG 1*/
36 #include "pl-incl.h"
37
38
39 /********************************
40 * VARIANT *
41 *********************************/
42
43 #define consVar(w) (((intptr_t)(w)<<LMASK_BITS) | TAG_VAR | FIRST_MASK)
44 #define valVar(w) ((intptr_t)(w) >> LMASK_BITS)
45
46 #define TAG_COMPOUND_x (STG_STATIC|TAG_COMPOUND)
47 #define isCompound_x(w) \
48 (( (intptr_t)(w) & (STG_MASK|TAG_MASK) ) == TAG_COMPOUND_x )
49 #define valCompound_x(w) ((intptr_t)(w) >> LMASK_BITS)
50 #define consCompound_x(i) (((i)<<LMASK_BITS) | TAG_COMPOUND_x)
51
52 #define node_bp(p) ((p)->bp)
53 #define node_orig(p) ((p)->orig)
54 #define node_variant(p) ((p)->a)
55 #define node_isom(p) ((p)->b)
56
57 typedef struct aWork
58 { word * left; /* left term arguments */
59 word * right; /* right term arguments */
60 int arg;
61 int arity;
62 } aWork;
63
64
65 typedef struct argPairs
66 { aWork work; /* current work */
67 segstack stack;
68 aWork first_chunk[16];
69 } argPairs;
70
71
72 typedef struct node
73 { Word bp; /* pointer to the original term */
74 word orig; /* saved word */
75 int a; /* variant at left */
76 int b; /* link to isomophic node */
77 } node;
78
79
80 static void
init_agenda(argPairs * a)81 init_agenda(argPairs *a)
82 { initSegStack(&a->stack, sizeof(aWork),
83 sizeof(a->first_chunk), a->first_chunk);
84 }
85
86
87 static inline bool
push_start_args(argPairs * a,Word left,Word right,int arity)88 push_start_args(argPairs *a, Word left, Word right, int arity) /* plural */
89 { a->work.left = left;
90 a->work.right = right;
91 a->work.arg = 0;
92 a->work.arity = arity;
93
94 return TRUE;
95 }
96
97 static inline bool
push_args(argPairs * a,Word left,Word right,int arity)98 push_args(argPairs *a, Word left, Word right, int arity) /* plural */
99 { if ( !pushSegStack(&a->stack, a->work, aWork) )
100 return FALSE;
101
102 return push_start_args(a, left, right, arity);
103 }
104
105 static inline bool
next_arg(argPairs * a,Word * lp,Word * rp)106 next_arg(argPairs *a, Word *lp, Word *rp) /* singular (not plural !) */
107 { while( a->work.arg >= a->work.arity)
108 { if ( !popSegStack(&a->stack, &a->work, aWork) )
109 return FALSE;
110 }
111
112 *lp = a->work.left;
113 *rp = a->work.right;
114
115 a->work.arg++;
116 a->work.left++;
117 a->work.right++;
118
119 return TRUE;
120 }
121
122 static inline node *
Node(int i,Buffer buf)123 Node(int i, Buffer buf)
124 { return &fetchBuffer(buf, i, node);
125 }
126
127 static inline bool
add_node_buffer(Buffer b,node * obj)128 add_node_buffer(Buffer b, node *obj)
129 { if ( ((b->top) + sizeof(node)) > (b->max) )
130 { if ( !growBuffer(b, sizeof(node)) )
131 return FALSE;
132 }
133
134 *((node *)(b)->top) = *obj;
135 b->top += sizeof(node);
136
137 return TRUE;
138 }
139
140 static inline int
var_id(Word p,Buffer buf)141 var_id(Word p, Buffer buf)
142 { word w = *p;
143
144 if ( w )
145 { return (int)valVar(w); /* node id truncated to int: */
146 } else /* < 2^31 nodes */
147 { int n = (int)entriesBuffer(buf, node);
148 node new = {p, w, 0, 0};
149
150 if ( !add_node_buffer((Buffer)buf, &new) )
151 return MEMORY_OVERFLOW;
152
153 *p = (word)consVar(n);
154 return n;
155 }
156 }
157
158 static inline int
term_id(Word p,Buffer buf)159 term_id(Word p, Buffer buf)
160 { word w = *p;
161
162 if ( isCompound_x(w) )
163 { return (int)valCompound_x(w);
164 } else
165 { int n = (int)entriesBuffer(buf, node);
166 node new = {p, w, 0, 0};
167
168 if ( !add_node_buffer((Buffer)buf, &new) )
169 return MEMORY_OVERFLOW;
170
171 *p = (word)consCompound_x(n);
172 return n;
173 }
174 }
175
176 static inline int
Root(int i,node ** r,Buffer buf)177 Root(int i, node **r, Buffer buf)
178 { int k;
179 node * n;
180
181 do
182 { k = i;
183 n = Node(i, buf);
184 DEBUG(CHK_SECURE, assert(n != NULL));
185 i = node_isom(n);
186 } while ( i != 0 );
187
188 *r = n;
189
190 return k;
191 }
192
193 static inline void
univ(word t,Word d,Word * a ARG_LD)194 univ(word t, Word d, Word *a ARG_LD)
195 { Functor f;
196
197 f = valueTerm(t);
198 while ( isRef(f->definition) )
199 f = (Functor)unRef(f->definition);
200 *d = f->definition;
201 *a = f->arguments;
202 }
203
204 static inline void
reset_terms(node * r)205 reset_terms(node * r)
206 { *(r->bp) = r->orig;
207 }
208
209 /* isomorphic (==) */
210
211 static int
isomorphic(argPairs * a,int i,int j,Buffer buf ARG_LD)212 isomorphic(argPairs *a, int i, int j, Buffer buf ARG_LD)
213 { Word l = NULL, r = NULL, lm, ln;
214 word dm, dn;
215 Word dummy = NULL;
216
217 if ( i == j )
218 return TRUE;
219
220 if ( !push_args(a, dummy, dummy, 1) )
221 return MEMORY_OVERFLOW;
222
223 univ(node_orig(Node(i, buf)), &dm, &lm PASS_LD);
224 univ(node_orig(Node(j, buf)), &dn, &ln PASS_LD);
225
226 if ( dm != dn )
227 return FALSE;
228
229 if ( !push_args(a, lm, ln, arityFunctor(dm)) )
230 return MEMORY_OVERFLOW;
231
232 while( next_arg(a, &l, &r) )
233 { word wl, wr;
234 if ( l == NULL )
235 return TRUE;
236
237 attvar:
238 deRef(l);
239 deRef(r);
240
241 wl = *l;
242 wr = *r;
243
244 if ( tag(wl) != tag(wr) )
245 return FALSE;
246
247 if ( tag(wl) == TAG_VAR )
248 { if ( l != r ) /* identity test on variables */
249 return FALSE;
250 continue;
251 }
252
253 if ( tag(wl) == TAG_ATTVAR )
254 { l = valPAttVar(wl);
255 r = valPAttVar(wr);
256 goto attvar;
257 }
258
259 if ( wl == wr && !isTerm(wl) )
260 continue;
261
262 switch(tag(wl))
263 { case TAG_ATOM:
264 return FALSE;
265 case TAG_INTEGER:
266 if ( storage(wl) == STG_INLINE ||
267 storage(wr) == STG_INLINE )
268 return FALSE;
269 case TAG_STRING:
270 case TAG_FLOAT:
271 if ( equalIndirect(wl, wr) )
272 continue;
273 return FALSE;
274 case TAG_COMPOUND:
275 { Word lm, ln;
276 word dm, dn;
277 int i, j;
278 node *m, *n;
279
280 if ( (i = term_id(l, buf)) < 0 )
281 return MEMORY_OVERFLOW;
282 i = Root(i, &m, buf);
283
284 if ( (j = term_id(r, buf)) < 0 )
285 return MEMORY_OVERFLOW;
286 j = Root(j, &n, buf);
287
288 if ( i==j )
289 continue;
290
291 univ(node_orig(m), &dm, &lm PASS_LD);
292 univ(node_orig(n), &dn, &ln PASS_LD);
293
294 if ( dm != dn )
295 return FALSE;
296
297 if ( i <= j )
298 node_isom(m) = j; /* union */
299 else
300 node_isom(n) = i;
301
302 if ( !push_args(a, lm, ln, arityFunctor(dm)) )
303 return MEMORY_OVERFLOW;
304
305 continue;
306 }
307 default:
308 assert(0);
309 }
310 }
311
312 return TRUE;
313 }
314
315 /* t =@= u */
316 static int
variant(argPairs * agenda,Buffer buf ARG_LD)317 variant(argPairs *agenda, Buffer buf ARG_LD)
318 { Word l = NULL, r =NULL;
319
320 while( next_arg(agenda, &l, &r) )
321 { word wl, wr;
322
323 attvar:
324 deRef(l);
325 deRef(r);
326
327 wl = *l;
328 wr = *r;
329
330 if ( tag(wl) != tag(wr) )
331 return FALSE;
332
333 if ( tag(wl) == TAG_VAR )
334 { int i, j, m, n;
335 node *vl, *vr;
336
337 if ((i = var_id(l, buf)) < 0)
338 return MEMORY_OVERFLOW;
339 if ((j = var_id(r, buf)) < 0)
340 return MEMORY_OVERFLOW;
341
342 vl = Node(i, buf);
343 vr = Node(j, buf);
344
345 m = vl->a;
346 n = vr->b;
347
348 if ( (m==0) && (n==0) )
349 { vl->a = j;
350 vr->b = i;
351 continue;
352 }
353 if ( (m != 0) && (n != 0) )
354 { if ( (m == j) && (n == i) )
355 continue;
356 }
357 return FALSE;
358 }
359
360 if ( tag(wl) == TAG_ATTVAR )
361 { l = valPAttVar(wl);
362 r = valPAttVar(wr);
363 goto attvar;
364 }
365
366 if ( wl == wr && !isTerm(wl) )
367 continue;
368
369 switch(tag(wl))
370 { case TAG_ATOM:
371 return FALSE;
372 case TAG_INTEGER:
373 if ( storage(wl) == STG_INLINE ||
374 storage(wr) == STG_INLINE )
375 return FALSE;
376 case TAG_STRING:
377 case TAG_FLOAT:
378 if ( equalIndirect(wl, wr) )
379 continue;
380 return FALSE;
381 case TAG_COMPOUND:
382 { int i, j, k, h;
383 node *m;
384
385 word dm, dn; /* definition (= functor/arity) */
386 Word lm, ln; /* arguments list */
387
388 if ( (i = term_id(l, buf)) < 0 )
389 return MEMORY_OVERFLOW;
390 if ( (j = term_id(r, buf)) < 0 )
391 return MEMORY_OVERFLOW;
392
393 m = Node(i, buf);
394 k = node_variant(m);
395
396 if ( 0 != k )
397 { if ( ( h = isomorphic(agenda, k, j, buf PASS_LD) ) <= 0 )
398 return h;
399 continue;
400 }
401
402 univ(node_orig(m), &dm, &lm PASS_LD);
403 univ(node_orig(Node(j,buf)), &dn, &ln PASS_LD);
404
405 if ( dm != dn )
406 return FALSE;
407
408 node_variant(m) = j;
409
410 if ( !push_args(agenda, lm, ln, arityFunctor(dm)) )
411 return MEMORY_OVERFLOW;
412
413 continue;
414 }
415 }
416 }
417
418 return TRUE;
419 }
420
421
422 int
is_variant_ptr(Word p1,Word p2 ARG_LD)423 is_variant_ptr(Word p1, Word p2 ARG_LD)
424 { argPairs agenda;
425 tmp_buffer buf;
426 Buffer VARIANT_BUFFER = (Buffer)&buf;
427 bool rval;
428 node *r;
429 node new = {NULL, 0, 0, 0}; /* dummy node as 0-th element*/
430
431 deRef(p1);
432 deRef(p2);
433
434 if ( *p1 == *p2 ) /* same term */
435 return TRUE;
436 if ( tag(*p1) != tag(*p2) ) /* different type */
437 return FALSE;
438 again:
439 switch(tag(*p1)) /* quick tests */
440 { case TAG_VAR:
441 return TRUE;
442 case TAG_ATTVAR:
443 p1 = valPAttVar(*p1);
444 p2 = valPAttVar(*p2);
445 goto again;
446 case TAG_ATOM:
447 return FALSE;
448 case TAG_INTEGER:
449 if ( !(isIndirect(*p1) && isIndirect(*p2)) )
450 return FALSE;
451 /*FALLTHROUGH*/
452 case TAG_FLOAT:
453 case TAG_STRING:
454 return equalIndirect(*p1, *p2);
455 case TAG_COMPOUND:
456 { Functor t1 = valueTerm(*p1);
457 Functor t2 = valueTerm(*p2);
458
459 if ( t1->definition != t2->definition )
460 return FALSE;
461 break;
462 }
463 default:
464 assert(0);
465 return FALSE;
466 }
467
468 startCritical;
469 initBuffer(&buf); /* can be faster! */
470 init_agenda(&agenda);
471
472 if ( (add_node_buffer(VARIANT_BUFFER, &new) >= 0) &&
473 (push_start_args(&agenda, p1, p2, 1) >=0) )
474 rval = variant(&agenda, VARIANT_BUFFER PASS_LD);
475 else
476 rval = MEMORY_OVERFLOW;
477
478 for(r = baseBuffer(VARIANT_BUFFER, node) + 1;
479 r < topBuffer(VARIANT_BUFFER, node); r++ )
480 reset_terms(r);
481
482 discardBuffer(VARIANT_BUFFER);
483 clearSegStack(&agenda.stack);
484
485 DEBUG(CHK_SECURE, checkStacks(NULL));
486
487 if ( !endCritical )
488 return FALSE;
489
490 if ( rval >= 0 )
491 return rval;
492
493 return PL_error(NULL, 0, NULL, ERR_NOMEM);
494 }
495
496 static
497 PRED_IMPL("=@=", 2, variant, 0)
498 { PRED_LD
499
500 return is_variant_ptr(valTermRef(A1), valTermRef(A2) PASS_LD);
501 }
502
503 static
504 PRED_IMPL("\\=@=", 2, not_variant, 0)
505 { PRED_LD
506
507 return !is_variant_ptr(valTermRef(A1), valTermRef(A2) PASS_LD);
508 }
509
510 /*******************************
511 * PUBLISH PREDICATES *
512 *******************************/
513
514 BeginPredDefs(variant)
515 PRED_DEF("=@=", 2, variant, 0)
516 PRED_DEF("\\=@=", 2, not_variant, 0)
517 EndPredDefs
518