~burner/xsb/debianized-xsb

« back to all changes in this revision

Viewing changes to emu/tst_unify.c

  • Committer: Michael R. Head
  • Date: 2006-09-06 22:11:55 UTC
  • Revision ID: burner@n23-20060906221155-7e398d23438a7ee4
Add the files from the 3.0.1 release package

Show diffs side-by-side

added added

removed removed

Lines of Context:
 
1
/* File:      tst_unify.c
 
2
** Author(s): Ernie Johnson
 
3
** Contact:   xsb-contact@cs.sunysb.edu
 
4
** 
 
5
** Copyright (C) The Research Foundation of SUNY, 1986, 1993-1998
 
6
** 
 
7
** XSB is free software; you can redistribute it and/or modify it under the
 
8
** terms of the GNU Library General Public License as published by the Free
 
9
** Software Foundation; either version 2 of the License, or (at your option)
 
10
** any later version.
 
11
** 
 
12
** XSB is distributed in the hope that it will be useful, but WITHOUT ANY
 
13
** WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
 
14
** FOR A PARTICULAR PURPOSE.  See the GNU Library General Public License for
 
15
** more details.
 
16
** 
 
17
** You should have received a copy of the GNU Library General Public License
 
18
** along with XSB; if not, write to the Free Software Foundation,
 
19
** Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
 
20
**
 
21
** $Id: tst_unify.c,v 1.18 2006/01/02 16:33:37 dwarren Exp $
 
22
** 
 
23
*/
 
24
 
 
25
 
 
26
#include "xsb_config.h"
 
27
#include "xsb_debug.h"
 
28
 
 
29
#include <stdio.h>
 
30
 
 
31
#include "auxlry.h"
 
32
#include "cell_xsb.h"
 
33
#include "register.h"
 
34
#include "memory_xsb.h"
 
35
#include "binding.h"
 
36
#include "psc_xsb.h"
 
37
#include "deref.h"
 
38
#include "subp.h"          /* xsbBool unify(Cell, Cell) */
 
39
#include "table_stats.h"
 
40
#include "trie_internals.h"
 
41
#include "macro_xsb.h"
 
42
#include "choice.h"
 
43
#include "tst_aux.h"
 
44
#include "tst_utils.h"
 
45
#include "error_xsb.h"
 
46
 
 
47
 
 
48
/* ========================================================================= */
 
49
 
 
50
 
 
51
/* Binding and Trailing
 
52
   -------------------- */
 
53
 
 
54
/*
 
55
 *  Bind the variable 'Symbol', obtained from a deref of a trie symbol, to
 
56
 *  the non-variable term 'Subterm'.  Trail the variable Symbol, which may
 
57
 *  either be a trie var or a prolog var.  If a trie var, then trail
 
58
 *  locally; if a prolog var, then trail on the WAM trail.
 
59
 */
 
60
#define Bind_and_Trail_Symbol(Symbol,Subterm) { \
 
61
   if (IsUnboundTrieVar(Symbol)) {              \
 
62
     Trail_Push(Symbol);                        \
 
63
     bld_ref((CPtr)Symbol,Subterm);             \
 
64
   }                                            \
 
65
   else                                         \
 
66
     Bind_and_Trail_Subterm(Symbol,Subterm)     \
 
67
 }
 
68
 
 
69
 
 
70
/*
 
71
 *  Bind the variable 'Subterm', obtained from a deref of a variable
 
72
 *  in the answer template, to the non-variable term 'Symbol'.
 
73
 *  Conditionally trail 'Subterm' on the system trail.
 
74
 */
 
75
#define Bind_and_Trail_Subterm(Subterm,Symbol) {        \
 
76
   bind_ref((CPtr)Subterm,Symbol);                      \
 
77
 }
 
78
 
 
79
 
 
80
/*
 
81
 *  Given two variables, one derived from a trie var and the other from
 
82
 *  the answer template, determine in which direction to bind one to the
 
83
 *  other and whether (and what kind) of trailing is required.  TrieVars
 
84
 *  are always bound to Prolog vars and are locally trailed.
 
85
 */
 
86
#define Bind_and_Trail_Vars(UnknownVar,PrologVar) {     \
 
87
   if (IsUnboundTrieVar(UnknownVar)) {                  \
 
88
     Trail_Push(UnknownVar)                             \
 
89
     bld_ref((CPtr)UnknownVar,PrologVar);               \
 
90
   }                                                    \
 
91
   else                                                 \
 
92
     unify(CTXTc UnknownVar,PrologVar);                 \
 
93
 }
 
94
 
 
95
 
 
96
/* ========================================================================= */
 
97
 
 
98
/* Error Reporting
 
99
   --------------- */
 
100
 
 
101
#ifndef MULTI_THREAD
 
102
static BTNptr gAnsLeaf;    /* answer to consume */
 
103
static CPtr gAnsTmplt;      /* ... using this template */
 
104
static int gSizeTmplt;      /* ... of this size */
 
105
#endif
 
106
 
 
107
/* TLS: temporary 12/05
 
108
static void debug_answer_consumption(CTXTdecl) {
 
109
  printf("-----------------------------\n");
 
110
  printTriePath(stderr,gAnsLeaf,NO);
 
111
  fprintf(stderr,"\nwith ");
 
112
  printAnswerTemplate(stderr,gAnsTmplt,gSizeTmplt);
 
113
 }
 
114
*****/
 
115
 
 
116
static void consumption_error(CTXTdeclc char *string) {
 
117
 
 
118
  char *abort_string;
 
119
 
 
120
#ifdef MULTI_THREAD
 
121
  fprintf(stderr,"This error has occurred, but the following diagnostics may be wrong due to global variables\n");
 
122
#endif
 
123
  fprintf(stderr,"\nAnswer Return ERROR:  Failed to unify answer\n\t");
 
124
#ifdef DEBUG_VERBOSE
 
125
  printTriePath(stderr,gAnsLeaf,YES);
 
126
#else
 
127
  printTriePath(stderr,gAnsLeaf,NO);
 
128
#endif
 
129
  fprintf(stderr,"\nwith ");
 
130
  printAnswerTemplate(stderr,gAnsTmplt,gSizeTmplt);
 
131
  fprintf(stderr,
 
132
          "(* Note: this template may be partially instantiated *)\n");
 
133
#ifdef DEBUG_ASSERTIONS
 
134
  xsb_error(string);
 
135
  /* Get Consumer SF from the CPS, using the ptr to AnsTmplt */
 
136
  {
 
137
    VariantSF pSF;
 
138
    CPtr pCPF;
 
139
 
 
140
    pCPF = gAnsTmplt - gSizeTmplt - NLCP_SIZE;
 
141
    pSF = (VariantSF)nlcp_subgoal_ptr(pCPF);
 
142
    printAnswerList(stderr,subg_answers(pSF));
 
143
  }
 
144
  abort_string = "";
 
145
#else
 
146
  abort_string = string;
 
147
#endif
 
148
  Trail_Unwind_All;  /* unbind TrieVarBindings[] elements */
 
149
  xsb_abort(abort_string);
 
150
}
 
151
 
 
152
 
 
153
/* ========================================================================= */
 
154
 
 
155
 
 
156
/*
 
157
 *                   A L G O R I T H M I C   M A C R O S
 
158
 *                   ===================================
 
159
 */
 
160
 
 
161
/*
 
162
 *  Given that the current subterm of the Answer Template contains a
 
163
 *  constant (int, float, or string), unify it with the current symbol of
 
164
 *  the trie.  Both have already been dereferenced.
 
165
 */
 
166
 
 
167
#define Unify_Symbol_With_Constant_Subterm(dSubterm,dSymbol) {  \
 
168
   if (isref(dSymbol))                                          \
 
169
     Bind_and_Trail_Symbol(dSymbol,dSubterm)                    \
 
170
   else if (dSymbol != dSubterm) {                              \
 
171
     consumption_error(CTXTc "Unequal Constants");              \
 
172
     return;                                                    \
 
173
   }                                                            \
 
174
}
 
175
 
 
176
/* ------------------------------------------------------------------------- */
 
177
 
 
178
/*
 
179
 *  Given that the current subterm of the Answer Template contains a
 
180
 *  function application, unify it with the current symbol of the trie.
 
181
 */
 
182
 
 
183
#define Unify_Symbol_With_Functor_Subterm(dSubterm,dSymbol,SymOrigTag)     \
 
184
                                                                           \
 
185
   switch(cell_tag(dSymbol)) {                                             \
 
186
   case XSB_STRUCT:                                                        \
 
187
     /*                                                                    \
 
188
      * Need to be careful here, because TrieVars can be bound to heap-    \
 
189
      * resident structures and a deref of the (trie) symbol doesn't       \
 
190
      * tell you whether we have something in the trie or in the heap.     \
 
191
      * Check that the same PSC Record is referred to by both.             \
 
192
      */                                                                   \
 
193
     if ( SymOrigTag == XSB_STRUCT ) {                                     \
 
194
       if ( get_str_psc(dSubterm) == DecodeTrieFunctor(dSymbol) ) {        \
 
195
         /*                                                                \
 
196
          *  There's a corresponding function application in the trie, so  \
 
197
          *  we must process the rest of the term ourselves.               \
 
198
          */                                                               \
 
199
         TermStack_PushFunctorArgs(dSubterm);                              \
 
200
       }                                                                   \
 
201
       else {                                                              \
 
202
         consumption_error(CTXTc "Distinct Functor Symbols");              \
 
203
         return;                                                           \
 
204
       }                                                                   \
 
205
     }                                                                     \
 
206
     else {                                                                \
 
207
       /*                                                                  \
 
208
        * We have a TrieVar bound to a heap STRUCT-term; use a standard    \
 
209
        * unification algorithm to check the match and perform additional  \
 
210
        * unifications.                                                    \
 
211
        */                                                                 \
 
212
       if ( ! unify(CTXTc dSubterm, dSymbol) ) {                           \
 
213
         consumption_error(CTXTc "Distinct Function Applications");        \
 
214
         return;                                                           \
 
215
       }                                                                   \
 
216
     }                                                                     \
 
217
     break;                                                                \
 
218
                                                                           \
 
219
   case XSB_REF:                                                           \
 
220
   case XSB_REF1:                                                          \
 
221
     /*                                                                    \
 
222
      * Either an unbound TrieVar or some unbound heap var.  We bind the   \
 
223
      * variable to the entire subterm (functor + args), so we don't need  \
 
224
      * to process its args.                                               \
 
225
      */                                                                   \
 
226
     Bind_and_Trail_Symbol(dSymbol,dSubterm)                               \
 
227
     break;                                                                \
 
228
                                                                           \
 
229
   default:                                                                \
 
230
     consumption_error(CTXTc                                               \
 
231
                       "Trie symbol fails to unify with functor subterm"); \
 
232
     return;                                                               \
 
233
   }
 
234
 
 
235
/* ------------------------------------------------------------------------- */
 
236
 
 
237
/*
 
238
 *  Given that the current subterm of the Answer Template contains a
 
239
 *  list, unify it with the current symbol of the trie.
 
240
 */
 
241
 
 
242
#define Unify_Symbol_With_List_Subterm(dSubterm,dSymbol,SymOrigTag)       \
 
243
                                                                          \
 
244
   switch(cell_tag(dSymbol)) {                                            \
 
245
   case XSB_LIST:                                                         \
 
246
     /*                                                                   \
 
247
      * Need to be careful here, because TrieVars can be bound to heap-   \
 
248
      * resident structures and a deref of the (trie) symbol doesn't      \
 
249
      * tell you whether we have something in the trie or in the heap.    \
 
250
      */                                                                  \
 
251
     if ( SymOrigTag == XSB_LIST ) {                                      \
 
252
       /*                                                                 \
 
253
        *  There's a corresponding list structure in the trie, so we must \
 
254
        *  process the rest of the term ourselves.                        \
 
255
        */                                                                \
 
256
       TermStack_PushListArgs(dSubterm);                                  \
 
257
     }                                                                    \
 
258
     else {                                                               \
 
259
       /*                                                                 \
 
260
        * We have a TrieVar bound to a heap STRUCT-term; use a standard   \
 
261
        * unification algorithm to check the match and perform additional \
 
262
        * unifications.                                                   \
 
263
        */                                                                \
 
264
       if ( ! unify(CTXTc dSubterm, dSymbol) ) {                          \
 
265
         consumption_error(CTXTc "Distinct Lists");                       \
 
266
         return;                                                          \
 
267
       }                                                                  \
 
268
     }                                                                    \
 
269
     break;                                                               \
 
270
                                                                          \
 
271
   case XSB_REF:                                                          \
 
272
   case XSB_REF1:                                                         \
 
273
     /*                                                                   \
 
274
      * Either an unbound TrieVar or some unbound heap var.  We bind the  \
 
275
      * variable to the entire subterm ([First | Rest]), so we don't need \
 
276
      * to process its args.                                              \
 
277
      */                                                                  \
 
278
     Bind_and_Trail_Symbol(dSymbol,dSubterm)                              \
 
279
     break;                                                               \
 
280
                                                                          \
 
281
   default:                                                               \
 
282
     consumption_error(CTXTc                                              \
 
283
                        "Trie symbol fails to unify with list subterm");  \
 
284
     return;                                                              \
 
285
   }
 
286
 
 
287
/* ------------------------------------------------------------------------- */
 
288
 
 
289
/*
 
290
 *  Given that the current subterm of the Answer Template contains a
 
291
 *  variable, unify it with the current symbol of the trie.
 
292
 */
 
293
 
 
294
#define Unify_Symbol_With_Variable_Subterm(dSubterm,dSymbol,SymOrigTag)  \
 
295
                                                                         \
 
296
   switch(cell_tag(dSymbol)) {                                           \
 
297
   case XSB_INT:                                                         \
 
298
   case XSB_FLOAT:                                                       \
 
299
   case XSB_STRING:                                                      \
 
300
     Bind_and_Trail_Subterm(dSubterm,dSymbol)                            \
 
301
     break;                                                              \
 
302
                                                                         \
 
303
   case XSB_STRUCT:                                                      \
 
304
     /*                                                                  \
 
305
      * Need to be careful here, because TrieVars can be bound to heap-  \
 
306
      * resident structures and a deref of the (trie) symbol doesn't     \
 
307
      * tell you whether we have something in the trie or in the heap.   \
 
308
      */                                                                 \
 
309
     if ( SymOrigTag == XSB_STRUCT ) {                                   \
 
310
       /*                                                                \
 
311
        *  Since the TST contains some f/n, create an f(X1,X2,...,Xn)    \
 
312
        *  structure on the heap so that we can bind the subterm         \
 
313
        *  variable to it.  Then use this algorithm to find bindings     \
 
314
        *  for the unbound variables X1,...,Xn along the trie path.      \
 
315
        */                                                               \
 
316
       CPtr heap_var_ptr;                                                \
 
317
       int arity, i;                                                     \
 
318
       Psc symbolPsc;                                                    \
 
319
                                                                         \
 
320
       symbolPsc = DecodeTrieFunctor(dSymbol);                           \
 
321
       arity = get_arity(symbolPsc);                                     \
 
322
       Bind_and_Trail_Subterm(dSubterm, (Cell)hreg)                      \
 
323
       bld_cs(hreg, hreg + 1);                                           \
 
324
       bld_functor(++hreg, symbolPsc);                                   \
 
325
       for (heap_var_ptr = hreg + arity, i = 0;                          \
 
326
            i < arity;                                                   \
 
327
            heap_var_ptr--, i++) {                                       \
 
328
         bld_free(heap_var_ptr);                                         \
 
329
         TermStack_Push((Cell)heap_var_ptr);                             \
 
330
       }                                                                 \
 
331
       hreg = hreg + arity + 1;                                          \
 
332
     }                                                                   \
 
333
     else {                                                              \
 
334
       /*                                                                \
 
335
        *  We have a TrieVar bound to a heap-resident XSB_STRUCT.        \
 
336
        */                                                               \
 
337
       Bind_and_Trail_Subterm(dSubterm, dSymbol)                         \
 
338
     }                                                                   \
 
339
     break;                                                              \
 
340
                                                                         \
 
341
   case XSB_LIST:                                                        \
 
342
     if ( SymOrigTag == XSB_LIST ) {                                     \
 
343
       /*                                                                \
 
344
        *  Since the TST contains a (sub)list beginning, create a        \
 
345
        *  [X1|X2] structure on the heap so that we can bind the subterm \
 
346
        *  variable to it.  Then use this algorithm to find bindings for \
 
347
        *  the unbound variables X1 & X2 along the trie path.            \
 
348
        */                                                               \
 
349
       Bind_and_Trail_Subterm(dSubterm, (Cell)hreg)                      \
 
350
       bld_list(hreg, hreg + 1);                                         \
 
351
       hreg = hreg + 3;                                                  \
 
352
       bld_free(hreg - 1);                                               \
 
353
       TermStack_Push((Cell)(hreg - 1));                                 \
 
354
       bld_free(hreg - 2);                                               \
 
355
       TermStack_Push((Cell)(hreg - 2));                                 \
 
356
     }                                                                   \
 
357
     else {                                                              \
 
358
       /*                                                                \
 
359
        *  We have a TrieVar bound to a heap-resident XSB_LIST.          \
 
360
        */                                                               \
 
361
       Bind_and_Trail_Subterm(dSubterm, dSymbol)                         \
 
362
     }                                                                   \
 
363
     break;                                                              \
 
364
                                                                         \
 
365
   case XSB_REF:                                                         \
 
366
   case XSB_REF1:                                                        \
 
367
     /*                                                                  \
 
368
      *  The symbol is either an unbound TrieVar or some unbound heap    \
 
369
      *  variable.  If it's an unbound TrieVar, we bind it to the heap   \
 
370
      *  var.  Otherwise, the direction of binding is high mem to low.   \
 
371
      */                                                                 \
 
372
     Bind_and_Trail_Vars(dSymbol,dSubterm)                               \
 
373
     break;                                                              \
 
374
                                                                         \
 
375
   default:                                                              \
 
376
     consumption_error(CTXTc "Unsupported tag on trie node symbol");     \
 
377
     return;                                                             \
 
378
   }
 
379
 
 
380
 
 
381
/* ========================================================================= */
 
382
 
 
383
/*
 
384
 *  Given a pointer to the answer template (a high-to-low memory vector),
 
385
 *  its size, and an answer leaf, unify the corresponding terms of each
 
386
 *  using the system stacks.  Variables that become bound are
 
387
 *  conditionally trailed while these values may be built on the heap.
 
388
 *  In this way, the bindings are readied for use by the engine, i.e., an
 
389
 *  answer is returned to a subsumed call.
 
390
 *
 
391
 *  Trie variables -- elements of the TrieVarBindings[] array -- may also
 
392
 *  become bound.  The bindings are needed during this operation but
 
393
 *  these variables should be unbound before leaving this function to
 
394
 *  ready TrieVarBindings[] for the next tabling operation.  The tstTrail
 
395
 *  is used to note these bindings for untrailing.
 
396
 */
 
397
 
 
398
void consume_subsumptive_answer(CTXTdeclc BTNptr pAnsLeaf, int sizeTmplt,
 
399
                                CPtr pAnsTmplt) {
 
400
 
 
401
  Cell subterm, symbol, sym_orig_tag;
 
402
 
 
403
  /* Set globals for error reporting
 
404
     ------------------------------- */
 
405
  gAnsLeaf = pAnsLeaf;
 
406
  gAnsTmplt = pAnsTmplt;
 
407
  gSizeTmplt = sizeTmplt;
 
408
 
 
409
  if ( ! IsLeafNode(pAnsLeaf) ) {
 
410
    consumption_error(CTXTc "Bad answer handle");
 
411
    return;
 
412
  }
 
413
  NumSubOps_AnswerConsumption++;
 
414
 
 
415
  /* Initialize Data Structs
 
416
     ----------------------- */
 
417
  Trail_ResetTOS;
 
418
 
 
419
  TermStack_ResetTOS;
 
420
  TermStack_PushHighToLowVector(pAnsTmplt,sizeTmplt);
 
421
 
 
422
  SymbolStack_ResetTOS;
 
423
  SymbolStack_PushPath(pAnsLeaf);
 
424
 
 
425
  /* Consume the Answer
 
426
     ------------------ */
 
427
  while ( ! TermStack_IsEmpty ) {
 
428
    TermStack_Pop(subterm);
 
429
    XSB_Deref(subterm);
 
430
    SymbolStack_Pop(symbol);
 
431
    sym_orig_tag = cell_tag(symbol);
 
432
    TrieSymbol_Deref(symbol);
 
433
    switch ( cell_tag(subterm) ) {
 
434
    case XSB_INT:
 
435
    case XSB_STRING:
 
436
    case XSB_FLOAT:
 
437
      Unify_Symbol_With_Constant_Subterm(subterm,symbol)
 
438
      break;
 
439
 
 
440
    case XSB_REF:
 
441
    case XSB_REF1:
 
442
      Unify_Symbol_With_Variable_Subterm(subterm,symbol,sym_orig_tag)
 
443
      break;
 
444
 
 
445
    case XSB_STRUCT:
 
446
      Unify_Symbol_With_Functor_Subterm(subterm,symbol,sym_orig_tag)
 
447
      break;
 
448
 
 
449
    case XSB_LIST:
 
450
      Unify_Symbol_With_List_Subterm(subterm,symbol,sym_orig_tag)
 
451
      break;
 
452
 
 
453
    default:
 
454
      consumption_error(CTXTc "Unsupported subterm tag");
 
455
      return;
 
456
    }
 
457
  }
 
458
  Trail_Unwind_All;  /* unbind TrieVarBindings[] elements */
 
459
}