XSB: C:/dev/sandbox/xsb_release/XSB/emu/tst

00001 /* File:      tst_unify.c
00002 ** Author(s): Ernie Johnson
00003 ** Contact:   xsb-contact@cs.sunysb.edu
00004 ** 
00005 ** Copyright (C) The Research Foundation of SUNY, 1986, 1993-1998
00006 ** 
00007 ** XSB is free software; you can redistribute it and/or modify it under the
00008 ** terms of the GNU Library General Public License as published by the Free
00009 ** Software Foundation; either version 2 of the License, or (at your option)
00010 ** any later version.
00011 ** 
00012 ** XSB is distributed in the hope that it will be useful, but WITHOUT ANY
00013 ** WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
00014 ** FOR A PARTICULAR PURPOSE.  See the GNU Library General Public License for
00015 ** more details.
00016 ** 
00017 ** You should have received a copy of the GNU Library General Public License
00018 ** along with XSB; if not, write to the Free Software Foundation,
00019 ** Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
00020 **
00021 ** $Id: tst_unify.c,v 1.18 2006/01/02 16:33:37 dwarren Exp $
00022 ** 
00023 */
00024 
00025 
00026 #include "xsb_config.h"
00027 #include "xsb_debug.h"
00028 
00029 #include <stdio.h>
00030 
00031 #include "auxlry.h"
00032 #include "cell_xsb.h"
00033 #include "register.h"
00034 #include "memory_xsb.h"
00035 #include "binding.h"
00036 #include "psc_xsb.h"
00037 #include "deref.h"
00038 #include "subp.h"          /* xsbBool unify(Cell, Cell) */
00039 #include "table_stats.h"
00040 #include "trie_internals.h"
00041 #include "macro_xsb.h"
00042 #include "choice.h"
00043 #include "tst_aux.h"
00044 #include "tst_utils.h"
00045 #include "error_xsb.h"
00046 
00047 
00048 /* ========================================================================= */
00049 
00050 
00051 /* Binding and Trailing
00052    -------------------- */
00053 
00054 /*
00055  *  Bind the variable 'Symbol', obtained from a deref of a trie symbol, to
00056  *  the non-variable term 'Subterm'.  Trail the variable Symbol, which may
00057  *  either be a trie var or a prolog var.  If a trie var, then trail
00058  *  locally; if a prolog var, then trail on the WAM trail.
00059  */
00060 #define Bind_and_Trail_Symbol(Symbol,Subterm) { \
00061    if (IsUnboundTrieVar(Symbol)) {              \
00062      Trail_Push(Symbol);                        \
00063      bld_ref((CPtr)Symbol,Subterm);             \
00064    }                                            \
00065    else                                         \
00066      Bind_and_Trail_Subterm(Symbol,Subterm)     \
00067  }
00068 
00069 
00070 /*
00071  *  Bind the variable 'Subterm', obtained from a deref of a variable
00072  *  in the answer template, to the non-variable term 'Symbol'.
00073  *  Conditionally trail 'Subterm' on the system trail.
00074  */
00075 #define Bind_and_Trail_Subterm(Subterm,Symbol) {        \
00076    bind_ref((CPtr)Subterm,Symbol);                      \
00077  }
00078 
00079 
00080 /*
00081  *  Given two variables, one derived from a trie var and the other from
00082  *  the answer template, determine in which direction to bind one to the
00083  *  other and whether (and what kind) of trailing is required.  TrieVars
00084  *  are always bound to Prolog vars and are locally trailed.
00085  */
00086 #define Bind_and_Trail_Vars(UnknownVar,PrologVar) {     \
00087    if (IsUnboundTrieVar(UnknownVar)) {                  \
00088      Trail_Push(UnknownVar)                             \
00089      bld_ref((CPtr)UnknownVar,PrologVar);               \
00090    }                                                    \
00091    else                                                 \
00092      unify(CTXTc UnknownVar,PrologVar);                 \
00093  }
00094 
00095 
00096 /* ========================================================================= */
00097 
00098 /* Error Reporting
00099    --------------- */
00100 
00101 #ifndef MULTI_THREAD
00102 static BTNptr gAnsLeaf;    /* answer to consume */
00103 static CPtr gAnsTmplt;      /* ... using this template */
00104 static int gSizeTmplt;      /* ... of this size */
00105 #endif
00106 
00107 /* TLS: temporary 12/05
00108 static void debug_answer_consumption(CTXTdecl) {
00109   printf("-----------------------------\n");
00110   printTriePath(stderr,gAnsLeaf,NO);
00111   fprintf(stderr,"\nwith ");
00112   printAnswerTemplate(stderr,gAnsTmplt,gSizeTmplt);
00113  }
00114 *****/
00115 
00116 static void consumption_error(CTXTdeclc char *string) {
00117 
00118   char *abort_string;
00119 
00120 #ifdef MULTI_THREAD
00121   fprintf(stderr,"This error has occurred, but the following diagnostics may be wrong due to global variables\n");
00122 #endif
00123   fprintf(stderr,"\nAnswer Return ERROR:  Failed to unify answer\n\t");
00124 #ifdef DEBUG_VERBOSE
00125   printTriePath(stderr,gAnsLeaf,YES);
00126 #else
00127   printTriePath(stderr,gAnsLeaf,NO);
00128 #endif
00129   fprintf(stderr,"\nwith ");
00130   printAnswerTemplate(stderr,gAnsTmplt,gSizeTmplt);
00131   fprintf(stderr,
00132           "(* Note: this template may be partially instantiated *)\n");
00133 #ifdef DEBUG_ASSERTIONS
00134   xsb_error(string);
00135   /* Get Consumer SF from the CPS, using the ptr to AnsTmplt */
00136   {
00137     VariantSF pSF;
00138     CPtr pCPF;
00139 
00140     pCPF = gAnsTmplt - gSizeTmplt - NLCP_SIZE;
00141     pSF = (VariantSF)nlcp_subgoal_ptr(pCPF);
00142     printAnswerList(stderr,subg_answers(pSF));
00143   }
00144   abort_string = "";
00145 #else
00146   abort_string = string;
00147 #endif
00148   Trail_Unwind_All;  /* unbind TrieVarBindings[] elements */
00149   xsb_abort(abort_string);
00150 }
00151 
00152 
00153 /* ========================================================================= */
00154 
00155 
00156 /*
00157  *                   A L G O R I T H M I C   M A C R O S
00158  *                   ===================================
00159  */
00160 
00161 /*
00162  *  Given that the current subterm of the Answer Template contains a
00163  *  constant (int, float, or string), unify it with the current symbol of
00164  *  the trie.  Both have already been dereferenced.
00165  */
00166 
00167 #define Unify_Symbol_With_Constant_Subterm(dSubterm,dSymbol) {  \
00168    if (isref(dSymbol))                                          \
00169      Bind_and_Trail_Symbol(dSymbol,dSubterm)                    \
00170    else if (dSymbol != dSubterm) {                              \
00171      consumption_error(CTXTc "Unequal Constants");              \
00172      return;                                                    \
00173    }                                                            \
00174 }
00175 
00176 /* ------------------------------------------------------------------------- */
00177 
00178 /*
00179  *  Given that the current subterm of the Answer Template contains a
00180  *  function application, unify it with the current symbol of the trie.
00181  */
00182 
00183 #define Unify_Symbol_With_Functor_Subterm(dSubterm,dSymbol,SymOrigTag)     \
00184                                                                            \
00185    switch(cell_tag(dSymbol)) {                                             \
00186    case XSB_STRUCT:                                                        \
00187      /*                                                                    \
00188       * Need to be careful here, because TrieVars can be bound to heap-    \
00189       * resident structures and a deref of the (trie) symbol doesn't       \
00190       * tell you whether we have something in the trie or in the heap.     \
00191       * Check that the same PSC Record is referred to by both.             \
00192       */                                                                   \
00193      if ( SymOrigTag == XSB_STRUCT ) {                                     \
00194        if ( get_str_psc(dSubterm) == DecodeTrieFunctor(dSymbol) ) {        \
00195          /*                                                                \
00196           *  There's a corresponding function application in the trie, so  \
00197           *  we must process the rest of the term ourselves.               \
00198           */                                                               \
00199          TermStack_PushFunctorArgs(dSubterm);                              \
00200        }                                                                   \
00201        else {                                                              \
00202          consumption_error(CTXTc "Distinct Functor Symbols");              \
00203          return;                                                           \
00204        }                                                                   \
00205      }                                                                     \
00206      else {                                                                \
00207        /*                                                                  \
00208         * We have a TrieVar bound to a heap STRUCT-term; use a standard    \
00209         * unification algorithm to check the match and perform additional  \
00210         * unifications.                                                    \
00211         */                                                                 \
00212        if ( ! unify(CTXTc dSubterm, dSymbol) ) {                           \
00213          consumption_error(CTXTc "Distinct Function Applications");        \
00214          return;                                                           \
00215        }                                                                   \
00216      }                                                                     \
00217      break;                                                                \
00218                                                                            \
00219    case XSB_REF:                                                           \
00220    case XSB_REF1:                                                          \
00221      /*                                                                    \
00222       * Either an unbound TrieVar or some unbound heap var.  We bind the   \
00223       * variable to the entire subterm (functor + args), so we don't need  \
00224       * to process its args.                                               \
00225       */                                                                   \
00226      Bind_and_Trail_Symbol(dSymbol,dSubterm)                               \
00227      break;                                                                \
00228                                                                            \
00229    default:                                                                \
00230      consumption_error(CTXTc                                               \
00231                        "Trie symbol fails to unify with functor subterm"); \
00232      return;                                                               \
00233    }
00234 
00235 /* ------------------------------------------------------------------------- */
00236 
00237 /*
00238  *  Given that the current subterm of the Answer Template contains a
00239  *  list, unify it with the current symbol of the trie.
00240  */
00241 
00242 #define Unify_Symbol_With_List_Subterm(dSubterm,dSymbol,SymOrigTag)       \
00243                                                                           \
00244    switch(cell_tag(dSymbol)) {                                            \
00245    case XSB_LIST:                                                         \
00246      /*                                                                   \
00247       * Need to be careful here, because TrieVars can be bound to heap-   \
00248       * resident structures and a deref of the (trie) symbol doesn't      \
00249       * tell you whether we have something in the trie or in the heap.    \
00250       */                                                                  \
00251      if ( SymOrigTag == XSB_LIST ) {                                      \
00252        /*                                                                 \
00253         *  There's a corresponding list structure in the trie, so we must \
00254         *  process the rest of the term ourselves.                        \
00255         */                                                                \
00256        TermStack_PushListArgs(dSubterm);                                  \
00257      }                                                                    \
00258      else {                                                               \
00259        /*                                                                 \
00260         * We have a TrieVar bound to a heap STRUCT-term; use a standard   \
00261         * unification algorithm to check the match and perform additional \
00262         * unifications.                                                   \
00263         */                                                                \
00264        if ( ! unify(CTXTc dSubterm, dSymbol) ) {                          \
00265          consumption_error(CTXTc "Distinct Lists");                       \
00266          return;                                                          \
00267        }                                                                  \
00268      }                                                                    \
00269      break;                                                               \
00270                                                                           \
00271    case XSB_REF:                                                          \
00272    case XSB_REF1:                                                         \
00273      /*                                                                   \
00274       * Either an unbound TrieVar or some unbound heap var.  We bind the  \
00275       * variable to the entire subterm ([First | Rest]), so we don't need \
00276       * to process its args.                                              \
00277       */                                                                  \
00278      Bind_and_Trail_Symbol(dSymbol,dSubterm)                              \
00279      break;                                                               \
00280                                                                           \
00281    default:                                                               \
00282      consumption_error(CTXTc                                              \
00283                         "Trie symbol fails to unify with list subterm");  \
00284      return;                                                              \
00285    }
00286 
00287 /* ------------------------------------------------------------------------- */
00288 
00289 /*
00290  *  Given that the current subterm of the Answer Template contains a
00291  *  variable, unify it with the current symbol of the trie.
00292  */
00293 
00294 #define Unify_Symbol_With_Variable_Subterm(dSubterm,dSymbol,SymOrigTag)  \
00295                                                                          \
00296    switch(cell_tag(dSymbol)) {                                           \
00297    case XSB_INT:                                                         \
00298    case XSB_FLOAT:                                                       \
00299    case XSB_STRING:                                                      \
00300      Bind_and_Trail_Subterm(dSubterm,dSymbol)                            \
00301      break;                                                              \
00302                                                                          \
00303    case XSB_STRUCT:                                                      \
00304      /*                                                                  \
00305       * Need to be careful here, because TrieVars can be bound to heap-  \
00306       * resident structures and a deref of the (trie) symbol doesn't     \
00307       * tell you whether we have something in the trie or in the heap.   \
00308       */                                                                 \
00309      if ( SymOrigTag == XSB_STRUCT ) {                                   \
00310        /*                                                                \
00311         *  Since the TST contains some f/n, create an f(X1,X2,...,Xn)    \
00312         *  structure on the heap so that we can bind the subterm         \
00313         *  variable to it.  Then use this algorithm to find bindings     \
00314         *  for the unbound variables X1,...,Xn along the trie path.      \
00315         */                                                               \
00316        CPtr heap_var_ptr;                                                \
00317        int arity, i;                                                     \
00318        Psc symbolPsc;                                                    \
00319                                                                          \
00320        symbolPsc = DecodeTrieFunctor(dSymbol);                           \
00321        arity = get_arity(symbolPsc);                                     \
00322        Bind_and_Trail_Subterm(dSubterm, (Cell)hreg)                      \
00323        bld_cs(hreg, hreg + 1);                                           \
00324        bld_functor(++hreg, symbolPsc);                                   \
00325        for (heap_var_ptr = hreg + arity, i = 0;                          \
00326             i < arity;                                                   \
00327             heap_var_ptr--, i++) {                                       \
00328          bld_free(heap_var_ptr);                                         \
00329          TermStack_Push((Cell)heap_var_ptr);                             \
00330        }                                                                 \
00331        hreg = hreg + arity + 1;                                          \
00332      }                                                                   \
00333      else {                                                              \
00334        /*                                                                \
00335         *  We have a TrieVar bound to a heap-resident XSB_STRUCT.        \
00336         */                                                               \
00337        Bind_and_Trail_Subterm(dSubterm, dSymbol)                         \
00338      }                                                                   \
00339      break;                                                              \
00340                                                                          \
00341    case XSB_LIST:                                                        \
00342      if ( SymOrigTag == XSB_LIST ) {                                     \
00343        /*                                                                \
00344         *  Since the TST contains a (sub)list beginning, create a        \
00345         *  [X1|X2] structure on the heap so that we can bind the subterm \
00346         *  variable to it.  Then use this algorithm to find bindings for \
00347         *  the unbound variables X1 & X2 along the trie path.            \
00348         */                                                               \
00349        Bind_and_Trail_Subterm(dSubterm, (Cell)hreg)                      \
00350        bld_list(hreg, hreg + 1);                                         \
00351        hreg = hreg + 3;                                                  \
00352        bld_free(hreg - 1);                                               \
00353        TermStack_Push((Cell)(hreg - 1));                                 \
00354        bld_free(hreg - 2);                                               \
00355        TermStack_Push((Cell)(hreg - 2));                                 \
00356      }                                                                   \
00357      else {                                                              \
00358        /*                                                                \
00359         *  We have a TrieVar bound to a heap-resident XSB_LIST.          \
00360         */                                                               \
00361        Bind_and_Trail_Subterm(dSubterm, dSymbol)                         \
00362      }                                                                   \
00363      break;                                                              \
00364                                                                          \
00365    case XSB_REF:                                                         \
00366    case XSB_REF1:                                                        \
00367      /*                                                                  \
00368       *  The symbol is either an unbound TrieVar or some unbound heap    \
00369       *  variable.  If it's an unbound TrieVar, we bind it to the heap   \
00370       *  var.  Otherwise, the direction of binding is high mem to low.   \
00371       */                                                                 \
00372      Bind_and_Trail_Vars(dSymbol,dSubterm)                               \
00373      break;                                                              \
00374                                                                          \
00375    default:                                                              \
00376      consumption_error(CTXTc "Unsupported tag on trie node symbol");     \
00377      return;                                                             \
00378    }
00379 
00380 
00381 /* ========================================================================= */
00382 
00383 /*
00384  *  Given a pointer to the answer template (a high-to-low memory vector),
00385  *  its size, and an answer leaf, unify the corresponding terms of each
00386  *  using the system stacks.  Variables that become bound are
00387  *  conditionally trailed while these values may be built on the heap.
00388  *  In this way, the bindings are readied for use by the engine, i.e., an
00389  *  answer is returned to a subsumed call.
00390  *
00391  *  Trie variables -- elements of the TrieVarBindings[] array -- may also
00392  *  become bound.  The bindings are needed during this operation but
00393  *  these variables should be unbound before leaving this function to
00394  *  ready TrieVarBindings[] for the next tabling operation.  The tstTrail
00395  *  is used to note these bindings for untrailing.
00396  */
00397 
00398 void consume_subsumptive_answer(CTXTdeclc BTNptr pAnsLeaf, int sizeTmplt,
00399                                 CPtr pAnsTmplt) {
00400 
00401   Cell subterm, symbol, sym_orig_tag;
00402 
00403   /* Set globals for error reporting
00404      ------------------------------- */
00405   gAnsLeaf = pAnsLeaf;
00406   gAnsTmplt = pAnsTmplt;
00407   gSizeTmplt = sizeTmplt;
00408 
00409   if ( ! IsLeafNode(pAnsLeaf) ) {
00410     consumption_error(CTXTc "Bad answer handle");
00411     return;
00412   }
00413   NumSubOps_AnswerConsumption++;
00414 
00415   /* Initialize Data Structs
00416      ----------------------- */
00417   Trail_ResetTOS;
00418 
00419   TermStack_ResetTOS;
00420   TermStack_PushHighToLowVector(pAnsTmplt,sizeTmplt);
00421 
00422   SymbolStack_ResetTOS;
00423   SymbolStack_PushPath(pAnsLeaf);
00424 
00425   /* Consume the Answer
00426      ------------------ */
00427   while ( ! TermStack_IsEmpty ) {
00428     TermStack_Pop(subterm);
00429     XSB_Deref(subterm);
00430     SymbolStack_Pop(symbol);
00431     sym_orig_tag = cell_tag(symbol);
00432     TrieSymbol_Deref(symbol);
00433     switch ( cell_tag(subterm) ) {
00434     case XSB_INT:
00435     case XSB_STRING:
00436     case XSB_FLOAT:
00437       Unify_Symbol_With_Constant_Subterm(subterm,symbol)
00438       break;
00439 
00440     case XSB_REF:
00441     case XSB_REF1:
00442       Unify_Symbol_With_Variable_Subterm(subterm,symbol,sym_orig_tag)
00443       break;
00444 
00445     case XSB_STRUCT:
00446       Unify_Symbol_With_Functor_Subterm(subterm,symbol,sym_orig_tag)
00447       break;
00448 
00449     case XSB_LIST:
00450       Unify_Symbol_With_List_Subterm(subterm,symbol,sym_orig_tag)
00451       break;
00452 
00453     default:
00454       consumption_error(CTXTc "Unsupported subterm tag");
00455       return;
00456     }
00457   }
00458   Trail_Unwind_All;  /* unbind TrieVarBindings[] elements */
00459 }