2
** Author(s): Ernie Johnson
3
** Contact: xsb-contact@cs.sunysb.edu
5
** Copyright (C) The Research Foundation of SUNY, 1986, 1993-1998
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)
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
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.
21
** $Id: tst_unify.c,v 1.18 2006/01/02 16:33:37 dwarren Exp $
26
#include "xsb_config.h"
27
#include "xsb_debug.h"
34
#include "memory_xsb.h"
38
#include "subp.h" /* xsbBool unify(Cell, Cell) */
39
#include "table_stats.h"
40
#include "trie_internals.h"
41
#include "macro_xsb.h"
44
#include "tst_utils.h"
45
#include "error_xsb.h"
48
/* ========================================================================= */
51
/* Binding and Trailing
52
-------------------- */
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.
60
#define Bind_and_Trail_Symbol(Symbol,Subterm) { \
61
if (IsUnboundTrieVar(Symbol)) { \
63
bld_ref((CPtr)Symbol,Subterm); \
66
Bind_and_Trail_Subterm(Symbol,Subterm) \
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.
75
#define Bind_and_Trail_Subterm(Subterm,Symbol) { \
76
bind_ref((CPtr)Subterm,Symbol); \
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.
86
#define Bind_and_Trail_Vars(UnknownVar,PrologVar) { \
87
if (IsUnboundTrieVar(UnknownVar)) { \
88
Trail_Push(UnknownVar) \
89
bld_ref((CPtr)UnknownVar,PrologVar); \
92
unify(CTXTc UnknownVar,PrologVar); \
96
/* ========================================================================= */
102
static BTNptr gAnsLeaf; /* answer to consume */
103
static CPtr gAnsTmplt; /* ... using this template */
104
static int gSizeTmplt; /* ... of this size */
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);
116
static void consumption_error(CTXTdeclc char *string) {
121
fprintf(stderr,"This error has occurred, but the following diagnostics may be wrong due to global variables\n");
123
fprintf(stderr,"\nAnswer Return ERROR: Failed to unify answer\n\t");
125
printTriePath(stderr,gAnsLeaf,YES);
127
printTriePath(stderr,gAnsLeaf,NO);
129
fprintf(stderr,"\nwith ");
130
printAnswerTemplate(stderr,gAnsTmplt,gSizeTmplt);
132
"(* Note: this template may be partially instantiated *)\n");
133
#ifdef DEBUG_ASSERTIONS
135
/* Get Consumer SF from the CPS, using the ptr to AnsTmplt */
140
pCPF = gAnsTmplt - gSizeTmplt - NLCP_SIZE;
141
pSF = (VariantSF)nlcp_subgoal_ptr(pCPF);
142
printAnswerList(stderr,subg_answers(pSF));
146
abort_string = string;
148
Trail_Unwind_All; /* unbind TrieVarBindings[] elements */
149
xsb_abort(abort_string);
153
/* ========================================================================= */
157
* A L G O R I T H M I C M A C R O S
158
* ===================================
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.
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"); \
176
/* ------------------------------------------------------------------------- */
179
* Given that the current subterm of the Answer Template contains a
180
* function application, unify it with the current symbol of the trie.
183
#define Unify_Symbol_With_Functor_Subterm(dSubterm,dSymbol,SymOrigTag) \
185
switch(cell_tag(dSymbol)) { \
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. \
193
if ( SymOrigTag == XSB_STRUCT ) { \
194
if ( get_str_psc(dSubterm) == DecodeTrieFunctor(dSymbol) ) { \
196
* There's a corresponding function application in the trie, so \
197
* we must process the rest of the term ourselves. \
199
TermStack_PushFunctorArgs(dSubterm); \
202
consumption_error(CTXTc "Distinct Functor Symbols"); \
208
* We have a TrieVar bound to a heap STRUCT-term; use a standard \
209
* unification algorithm to check the match and perform additional \
212
if ( ! unify(CTXTc dSubterm, dSymbol) ) { \
213
consumption_error(CTXTc "Distinct Function Applications"); \
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. \
226
Bind_and_Trail_Symbol(dSymbol,dSubterm) \
230
consumption_error(CTXTc \
231
"Trie symbol fails to unify with functor subterm"); \
235
/* ------------------------------------------------------------------------- */
238
* Given that the current subterm of the Answer Template contains a
239
* list, unify it with the current symbol of the trie.
242
#define Unify_Symbol_With_List_Subterm(dSubterm,dSymbol,SymOrigTag) \
244
switch(cell_tag(dSymbol)) { \
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. \
251
if ( SymOrigTag == XSB_LIST ) { \
253
* There's a corresponding list structure in the trie, so we must \
254
* process the rest of the term ourselves. \
256
TermStack_PushListArgs(dSubterm); \
260
* We have a TrieVar bound to a heap STRUCT-term; use a standard \
261
* unification algorithm to check the match and perform additional \
264
if ( ! unify(CTXTc dSubterm, dSymbol) ) { \
265
consumption_error(CTXTc "Distinct Lists"); \
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. \
278
Bind_and_Trail_Symbol(dSymbol,dSubterm) \
282
consumption_error(CTXTc \
283
"Trie symbol fails to unify with list subterm"); \
287
/* ------------------------------------------------------------------------- */
290
* Given that the current subterm of the Answer Template contains a
291
* variable, unify it with the current symbol of the trie.
294
#define Unify_Symbol_With_Variable_Subterm(dSubterm,dSymbol,SymOrigTag) \
296
switch(cell_tag(dSymbol)) { \
300
Bind_and_Trail_Subterm(dSubterm,dSymbol) \
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. \
309
if ( SymOrigTag == XSB_STRUCT ) { \
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. \
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; \
327
heap_var_ptr--, i++) { \
328
bld_free(heap_var_ptr); \
329
TermStack_Push((Cell)heap_var_ptr); \
331
hreg = hreg + arity + 1; \
335
* We have a TrieVar bound to a heap-resident XSB_STRUCT. \
337
Bind_and_Trail_Subterm(dSubterm, dSymbol) \
342
if ( SymOrigTag == XSB_LIST ) { \
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. \
349
Bind_and_Trail_Subterm(dSubterm, (Cell)hreg) \
350
bld_list(hreg, hreg + 1); \
352
bld_free(hreg - 1); \
353
TermStack_Push((Cell)(hreg - 1)); \
354
bld_free(hreg - 2); \
355
TermStack_Push((Cell)(hreg - 2)); \
359
* We have a TrieVar bound to a heap-resident XSB_LIST. \
361
Bind_and_Trail_Subterm(dSubterm, dSymbol) \
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. \
372
Bind_and_Trail_Vars(dSymbol,dSubterm) \
376
consumption_error(CTXTc "Unsupported tag on trie node symbol"); \
381
/* ========================================================================= */
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.
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.
398
void consume_subsumptive_answer(CTXTdeclc BTNptr pAnsLeaf, int sizeTmplt,
401
Cell subterm, symbol, sym_orig_tag;
403
/* Set globals for error reporting
404
------------------------------- */
406
gAnsTmplt = pAnsTmplt;
407
gSizeTmplt = sizeTmplt;
409
if ( ! IsLeafNode(pAnsLeaf) ) {
410
consumption_error(CTXTc "Bad answer handle");
413
NumSubOps_AnswerConsumption++;
415
/* Initialize Data Structs
416
----------------------- */
420
TermStack_PushHighToLowVector(pAnsTmplt,sizeTmplt);
422
SymbolStack_ResetTOS;
423
SymbolStack_PushPath(pAnsLeaf);
425
/* Consume the Answer
426
------------------ */
427
while ( ! TermStack_IsEmpty ) {
428
TermStack_Pop(subterm);
430
SymbolStack_Pop(symbol);
431
sym_orig_tag = cell_tag(symbol);
432
TrieSymbol_Deref(symbol);
433
switch ( cell_tag(subterm) ) {
437
Unify_Symbol_With_Constant_Subterm(subterm,symbol)
442
Unify_Symbol_With_Variable_Subterm(subterm,symbol,sym_orig_tag)
446
Unify_Symbol_With_Functor_Subterm(subterm,symbol,sym_orig_tag)
450
Unify_Symbol_With_List_Subterm(subterm,symbol,sym_orig_tag)
454
consumption_error(CTXTc "Unsupported subterm tag");
458
Trail_Unwind_All; /* unbind TrieVarBindings[] elements */