/*----------------------------------------------------------------------- File : cte_termbanks.c Author: Stephan Schulz Contents Functions for term banks (efficient dag-representations for term sets). Bindings (i.e. values in term->binding) make only sense in dynamical contexts, not in (mostly) static term banks. Thus, bindings are followed whenever a term is treated as an individual term, but not when they form part of a term bank and are manipulated as such. Copyright 1998-2011 by the author. This code is released under the GNU General Public Licence and the GNU Lesser General Public License. See the file COPYING in the main E directory for details.. Run "eprover -h" for contact information. Changes <1> Sat Nov 15 16:26:30 MET 1997 New <2> Fri Oct 2 20:35:41 MET DST 1998 Variables are now longer in the term trees and have lost superterm information -> 20% Speedup! <3> You cannot take references for variables anymore. This requires that no variables are ever replaced (but this is a requirement anyways), but deals with a strange bug (and may speed up the code even more). <4> Sat Apr 6 21:42:35 CEST 2002 Changed for new rewriting. No Superterms anymore! References are fully passive. Deletion does not work any more, I'm working on a mark-and-sweep garbage collector for terms instead. -----------------------------------------------------------------------*/ #include "cte_termbanks.h" /*---------------------------------------------------------------------*/ /* Global Variables */ /*---------------------------------------------------------------------*/ bool TBPrintInternalInfo = false; /* Print internal information about term nodes, e.g. the flag field */ bool TBPrintDetails = false; /* Collect potentially expensive information (number of nodes, number of unshared nodes, size of various sub-data structures) and print them if required */ /*---------------------------------------------------------------------*/ /* Forward Declarations */ /*---------------------------------------------------------------------*/ /*---------------------------------------------------------------------*/ /* Internal Functions */ /*---------------------------------------------------------------------*/ /*----------------------------------------------------------------------- // // Function: tb_print_dag() // // Print the terms as a dag in the order of insertion. // // Global Variables: TBPrintInternalInfo // // Side Effects : Output // /----------------------------------------------------------------------*/ static void tb_print_dag(FILE *out, NumTree_p in_index, Sig_p sig) { Term_p term; if(!in_index) { return; } tb_print_dag(out, in_index->lson, sig); term = in_index->val1.p_val; fprintf(out, "*%ld : ", term->entry_no); if(TermIsVar(term)) { VarPrint(out, term->f_code); } else { fputs(SigFindName(sig, term->f_code), out); if(!TermIsConst(term)) { int i; assert(term->arity>=1); assert(term->args); putc('(', out); fprintf(out, "*%ld", TBCellIdent(term->args[0])); for(i=1; iarity; i++) { putc(',', out); fprintf(out, "*%ld", TBCellIdent(term->args[i])); } putc(')', out); } printf(" = "); TermPrint(out, term, sig, DEREF_NEVER); } if(TBPrintInternalInfo) { fprintf(out, "\t/* Properties: %10d */", term->properties); } fprintf(out, "\n"); tb_print_dag(out, in_index->rson, sig); } /*----------------------------------------------------------------------- // // Function: tb_termtop_insert() // // Insert a term into the term bank for which the subterms are // already in the term bank. Will reuse or destroy the top cell! // // Global Variables: TBSupportReplace // // Side Effects : Changes term bank // /----------------------------------------------------------------------*/ static Term_p tb_termtop_insert(TB_p bank, Term_p t) { Term_p new; assert(t); assert(!TermIsVar(t)); new = TermCellStoreInsert(&(bank->term_store), t); if(new) /* Term node already existed, just add properties */ { new->properties = (new->properties | t->properties)/*& bank->prop_mask*/; TermTopFree(t); return new; } else { int i; t->entry_no = ++(bank->in_count); TermCellAssignProp(t,TPGarbageFlag, bank->garbage_state); TermCellSetProp(t, TPIsShared|TPIsGround); /* Groundness may * change below */ t->weight = DEFAULT_FWEIGHT; for(i=0; iarity; i++) { assert(TermIsShared(t->args[i])||TermIsVar(t->args[i])); t->weight+=t->args[i]->weight; if(!TermCellQueryProp(t->args[i], TPIsGround)) { TermCellDelProp(t,TPIsGround); } } assert(TermStandardWeight(t) == TermWeight(t, DEFAULT_VWEIGHT, DEFAULT_FWEIGHT)); assert((TermIsGround(t)==0) == (TBTermIsGround(t)==0)); } return t; } /*----------------------------------------------------------------------- // // Function: tb_parse_cons_list() // // Parse a LOP list into an (shared) internal $cons list. // // Global Variables: - // // Side Effects : Input, Memory operations // /----------------------------------------------------------------------*/ static Term_p tb_parse_cons_list(Scanner_p in, TB_p bank, bool check_symb_prop) { Term_p handle; Term_p current; PStack_p stack; assert(SigSupportLists); stack = PStackAlloc(); AcceptInpTok(in, OpenSquare); handle = DefaultSharedTermCellAlloc(); current = handle; if(!TestInpTok(in, CloseSquare)) { current->f_code = SIG_CONS_CODE; current->arity = 2; current->args = TermArgArrayAlloc(2); current->args[0] = TBTermParseReal(in, bank, check_symb_prop); current->args[1] = DefaultSharedTermCellAlloc(); current = current->args[1]; PStackPushP(stack, current); while(TestInpTok(in, Comma)) { NextToken(in); current->f_code = SIG_CONS_CODE; current->arity = 2; current->args = TermArgArrayAlloc(2); current->args[0] = TBTermParseReal(in, bank, check_symb_prop); current->args[1] = TermDefaultCellAlloc(); current = current->args[1]; PStackPushP(stack, current); } current = PStackPopP(stack); } AcceptInpTok(in, CloseSquare); current->f_code = SIG_NIL_CODE; /* Now insert the list into the bank */ handle = tb_termtop_insert(bank, current); while(!PStackEmpty(stack)) { current = PStackPopP(stack); current->args[1] = handle; handle = tb_termtop_insert(bank, current); } PStackFree(stack); return handle; } /*----------------------------------------------------------------------- // // Function: tb_subterm_parse() // // Parse a subterm, i.e. a term which cannot start with a predicate // symbol. // // Global Variables: - // // Side Effects : Input, memory operations, changes termbank. // /----------------------------------------------------------------------*/ static Term_p tb_subterm_parse(Scanner_p in, TB_p bank) { Term_p res = TBTermParseReal(in, bank, true); if(!TermIsVar(res)) { if(SigIsPredicate(bank->sig, res->f_code)) { AktTokenError(in, "Predicate used as function symbol in preceeding term", SYNTAX_ERROR); } SigSetFunction(bank->sig, res->f_code, true); } return res; } /*----------------------------------------------------------------------- // // Function: tb_term_parse_arglist() // // Parse a list of terms (comma-separated and enclosed in brackets) // into an array of (shared) term pointers. See TermParseArgList() // in cte_terms.c for more. // // Global Variables: - // // Side Effects : Input, memory operations, changes term bank // /----------------------------------------------------------------------*/ static int tb_term_parse_arglist(Scanner_p in, Term_p** arg_anchor, TB_p bank, bool check_symb_prop) { Term_p *handle, tmp; int arity; int size; int i; AcceptInpTok(in, OpenBracket); if(TestInpTok(in, CloseBracket)) { NextToken(in); *arg_anchor = NULL; return 0; } size = TERMS_INITIAL_ARGS; handle = (Term_p*)SizeMalloc(size*sizeof(Term_p)); arity = 0; tmp = check_symb_prop? tb_subterm_parse(in, bank): TBRawTermParse(in,bank); handle[arity] = tmp; arity++; while(TestInpTok(in, Comma)) { NextToken(in); if(arity==size) { size+=TERMS_INITIAL_ARGS; handle = (Term_p*)SecureRealloc(handle, size*sizeof(Term_p)); } handle[arity] = check_symb_prop? tb_subterm_parse(in, bank): TBRawTermParse(in,bank); arity++; } AcceptInpTok(in, CloseBracket); *arg_anchor = TermArgArrayAlloc(arity); for(i=0;iin_count = 0; handle->rewrite_steps = 0; handle->ext_index = PDIntArrayAlloc(1,100000); handle->garbage_state = TPIgnoreProps; handle->sig = sig; handle->vars = VarBankAlloc(); TermCellStoreInit(&(handle->term_store)); term = TermDefaultCellAlloc(); term->f_code = SIG_TRUE_CODE; TermCellSetProp(term, TPPredPos); handle->true_term = TBInsert(handle, term, DEREF_NEVER); TermFree(term); term = TermDefaultCellAlloc(); term->f_code = SIG_FALSE_CODE; TermCellSetProp(term, TPPredPos); handle->false_term = TBInsert(handle, term, DEREF_NEVER); TermFree(term); handle->min_term = 0; return handle; } /*----------------------------------------------------------------------- // // Function: TBFree() // // Free a term bank (if the signature alread has been // extracted). Voids all pointers to terms in the bank! // // Global Variables: - // // Side Effects : Memory operations. // /----------------------------------------------------------------------*/ void TBFree(TB_p junk) { assert(!junk->sig); /* printf("TBFree(): %ld\n", TermCellStoreNodes(&(junk->term_store))); */ TermCellStoreExit(&(junk->term_store)); PDArrayFree(junk->ext_index); VarBankFree(junk->vars); TBCellFree(junk); } /*----------------------------------------------------------------------- // // Function: TBTermNodes() // // Return the number of term nodes (variables and non-variables) in // the term bank. // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ long TBTermNodes(TB_p bank) { assert(TermCellStoreNodes(&(bank->term_store))== TermCellStoreCountNodes(&(bank->term_store))); return TermCellStoreNodes(&(bank->term_store))+ PDArrayMembers(bank->vars->f_code_index); } /*----------------------------------------------------------------------- // // Function: DefaultSharedTermCellAlloc() // // Return a reasonably initialized term cell for shared terms. // // Global Variables: - // // Side Effects : Memory Operations // /----------------------------------------------------------------------*/ Term_p DefaultSharedTermCellAlloc(void) { Term_p handle; handle = TermDefaultCellAlloc(); TermCellSetProp(handle, TPIsShared); return handle; } /*----------------------------------------------------------------------- // // Function: TBInsert() // // Insert the term into the termbank. The original term will remain // untouched. The routine returns a pointer to a new, shared term of // the same structure. // // TermProperties are masked with bank->prop_mask. // // Global Variables: - // // Side Effects : Changes term bank // /----------------------------------------------------------------------*/ Term_p TBInsert(TB_p bank, Term_p term, DerefType deref) { int i; Term_p t; assert(term); term = TermDeref(term, &deref); t = TermEquivCellAlloc(term, bank->vars); /* This is an unshared term cell at the moment, */ if(!TermIsVar(t)) { assert(SysDateIsCreationDate(t->rw_data.nf_date[0])); assert(SysDateIsCreationDate(t->rw_data.nf_date[1])); for(i=0; iarity; i++) { t->args[i] = TBInsert(bank, t->args[i], deref); } t = tb_termtop_insert(bank, t); } return t; } /*----------------------------------------------------------------------- // // Function: TBInsertNoProps() // // As TBInsert, but will set all properties of the new term to 0 // first. // // Global Variables: TBSupportReplace // // Side Effects : Changes term bank // /----------------------------------------------------------------------*/ Term_p TBInsertNoProps(TB_p bank, Term_p term, DerefType deref) { int i; Term_p t; assert(term); term = TermDeref(term, &deref); t = TermEquivCellAlloc(term, bank->vars); /* This is an unshared term cell at the moment */ if(!TermIsVar(t)) { t->properties = TPIgnoreProps; assert(SysDateIsCreationDate(t->rw_data.nf_date[0])); assert(SysDateIsCreationDate(t->rw_data.nf_date[1])); for(i=0; iarity; i++) { t->args[i] = TBInsertNoProps(bank, t->args[i], deref); } t = tb_termtop_insert(bank, t); } return t; } /*----------------------------------------------------------------------- // // Function: TBInsertRepl() // // As TBInsertNoProps, but when old is encountered as a subterm // (regardless of instantiation), replace it with uninstantiated // repl (which _must_ be in bank). // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ Term_p TBInsertRepl(TB_p bank, Term_p term, DerefType deref, Term_p old, Term_p repl) { int i; Term_p t; assert(term); if(term == old) { assert(TBFind(bank, repl)); return repl; } term = TermDeref(term, &deref); t = TermEquivCellAlloc(term, bank->vars); /* This is an unshared term cell at the moment */ if(!TermIsVar(t)) { t->properties = TPIgnoreProps; assert(SysDateIsCreationDate(t->rw_data.nf_date[0])); assert(SysDateIsCreationDate(t->rw_data.nf_date[1])); for(i=0; iarity; i++) { t->args[i] = TBInsertRepl(bank, t->args[i], deref, old, repl); } t = tb_termtop_insert(bank, t); } return t; } /*----------------------------------------------------------------------- // // Function: TBInsertInstantiated() // // Insert a term into the termbank under the assumption that it is a // right side of a rule (or equation) composed of terms from bank, // and (possibly) instantiated with terms from bank - i.e. don't // insert terms that are bound to variables and ground terms, but // assume that they are in the term bank. Properties in newly // created nodes are deleted. // // Global Variables: TBSupportReplace // // Side Effects : Changes term bank // /----------------------------------------------------------------------*/ Term_p TBInsertInstantiated(TB_p bank, Term_p term) { int i; Term_p t; assert(term); if(TBTermIsGround(term)) { assert(TBFind(bank, term)); return term; } if(term->binding) { assert(TBFind(bank, term->binding)); return term->binding; } t = TermEquivCellAlloc(term, bank->vars); /* This is an unshared term cell at the moment */ if(!TermIsVar(t)) { t->properties = TPIgnoreProps; assert(SysDateIsCreationDate(t->rw_data.nf_date[0])); assert(SysDateIsCreationDate(t->rw_data.nf_date[1])); for(i=0; iarity; i++) { t->args[i] = TBInsertInstantiated(bank, t->args[i]); } t = tb_termtop_insert(bank, t); } return t; } /*----------------------------------------------------------------------- // // Function: TBInsertOpt() // // Insert term into bank under the assumption that it it already is // in the bank (except possibly for variables appearing as // bindings). This allows us to just return term for ground terms. // // Global Variables: - // // Side Effects : Changes term bank. // /----------------------------------------------------------------------*/ Term_p TBInsertOpt(TB_p bank, Term_p term, DerefType deref) { int i; Term_p t; assert(term); term = TermDeref(term, &deref); if(TermIsGround(term)) { return term; } t = TermEquivCellAlloc(term, bank->vars); /* This is an unshared term cell at the moment, */ if(!TermIsVar(t)) { assert(SysDateIsCreationDate(t->rw_data.nf_date[0])); assert(SysDateIsCreationDate(t->rw_data.nf_date[1])); for(i=0; iarity; i++) { t->args[i] = TBInsertOpt(bank, t->args[i], deref); } t = tb_termtop_insert(bank, t); } return t; } /*----------------------------------------------------------------------- // // Function: TBInsertDisjoint() // // Create a copy of (uninstantiated) term with disjoint // variables. This assumes that all variables in term are odd or // even, the returned copy will have variable ids shifted by -1. // // Global Variables: - // // Side Effects : Changes bank. // /----------------------------------------------------------------------*/ Term_p TBInsertDisjoint(TB_p bank, Term_p term) { int i; Term_p t; assert(term); if(TermIsGround(term)) { return term; } if(TermIsVar(term)) { t = VarBankFCodeAssertAlloc(bank->vars, term->f_code+1); } else { t = TermEquivCellAlloc(term, bank->vars); /* This is an unshared term cell at the moment, */ assert(SysDateIsCreationDate(t->rw_data.nf_date[0])); assert(SysDateIsCreationDate(t->rw_data.nf_date[1])); for(i=0; iarity; i++) { t->args[i] = TBInsertDisjoint(bank, t->args[i]); } t = tb_termtop_insert(bank, t); } return t; } /*----------------------------------------------------------------------- // // Function: TBTermTopInsert() // // See tb_termtop_insert, for export without hurting inlining // capabilities. // // Global Variables: - // // Side Effects : Changes bank // /----------------------------------------------------------------------*/ Term_p TBTermTopInsert(TB_p bank, Term_p t) { return tb_termtop_insert(bank,t); } /*----------------------------------------------------------------------- // // Function: TBAllocNewSkolem() // // Create a news Skolem term (or definition atom) with the given // variables in the term bank and return the pointer to it. // // Global Variables: // // Side Effects : // /----------------------------------------------------------------------*/ Term_p TBAllocNewSkolem(TB_p bank, PStack_p variables, bool atom) { Term_p handle, res; handle = TermAllocNewSkolem(bank->sig, variables, atom); res = TBInsert(bank, handle, DEREF_NEVER); TermFree(handle); return res; } /*----------------------------------------------------------------------- // // Function: TBFind() // // Find a term in the term cell bank and return it. // // Global Variables: - // // Side Effects : - // /----------------------------------------------------------------------*/ Term_p TBFind(TB_p bank, Term_p term) { if(TermIsVar(term)) { return VarBankFCodeFind(bank->vars, term->f_code); } return TermCellStoreFind(&(bank->term_store), term); } /*----------------------------------------------------------------------- // // Function: TBPrintBankInOrder() // // Print the DAG in the order of ascending entry_no. // // Global Variables: TBPrintTermsFlat // // Side Effects : Output // /----------------------------------------------------------------------*/ void TBPrintBankInOrder(FILE* out, TB_p bank) { NumTree_p tree = NULL; long i; PStack_p stack; Term_p cell; IntOrP dummy; for(i=0; iterm_store.store[i]); while((cell = TermTreeTraverseNext(stack))) { dummy.p_val = cell; NumTreeStore(&tree, cell->entry_no,dummy, dummy); } TermTreeTraverseExit(stack); } tb_print_dag(out, tree, bank->sig); NumTreeFree(tree); } /*----------------------------------------------------------------------- // // Function: TBPrintTermCompact() // // Print a term bank term. Introduce abbreviations for all subterms // encountered. Subterms with TPOutputFlag are not // printed, but are assumed to be known. Does _not_ follow bindings // (they are temporary and as such make little sense in the term // bank context) // // Global Variables: - // // Side Effects : Output, set TPOutputFlag in subterms printed with // abbreviation. // /----------------------------------------------------------------------*/ void TBPrintTermCompact(FILE* out, TB_p bank, Term_p term) { int i; if(TermCellQueryProp(term, TPOutputFlag)) { fprintf(out, "*%ld", term->entry_no); } else { if(TermIsVar(term)) { VarPrint(out, term->f_code); } else { fprintf(out, "*%ld:", term->entry_no); TermCellSetProp(term, TPOutputFlag); fputs(SigFindName(bank->sig, term->f_code), out); if(!TermIsConst(term)) { fputc('(',out); assert(term->args && (term->arity>0)); TBPrintTermCompact(out, bank, term->args[0]); for(i=1;iarity;i++) { fputc(',', out); TBPrintTermCompact(out, bank, term->args[i]); } fputc(')',out); } } } } /*----------------------------------------------------------------------- // // Function: TBPrintTerm() // // Print a term from a term bank either in compact form (with // abbreviations) or as a conventional term. // // Global Variables: - // // Side Effects : By the called functions // /----------------------------------------------------------------------*/ void TBPrintTerm(FILE* out, TB_p bank, Term_p term, bool fullterms) { if(fullterms) { TBPrintTermFull(out, bank, term); } else { TBPrintTermCompact(out, bank, term); } } /*----------------------------------------------------------------------- // // Function: TBPrintBankTerms() // // Print the terms inserted into the term bank with abbreviations. // // Global Variables: - // // Side Effects : Output, changes by TBPrintTermCompact() // /----------------------------------------------------------------------*/ void TBPrintBankTerms(FILE* out, TB_p bank) { PStack_p stack = PStackAlloc(); Term_p term; int i; for(i=0; iterm_store.store[i]); while(!PStackEmpty(stack)) { term = PStackPopP(stack); if(term) { PStackPushP(stack, term->lson); PStackPushP(stack, term->rson); if(TermCellQueryProp(term, TPTopPos)) { TBPrintTermCompact(out, bank, term); fprintf(out, "\n"); } } } } PStackFree(stack); } /*----------------------------------------------------------------------- // // Function: TBTermParseReal() // // Parse a term from the given scanner object directly into the // termbank. Supports abbreviations. This function will _not_ set // the TPTopPos property on top terms while parsing. It will or will // not check and set symbol properties (function symbol, predicate // symbol), depending on the check_symb_prop parameter. // // Global Variables: - // // Side Effects : Input, memory operations, changes termbank. // /----------------------------------------------------------------------*/ Term_p TBTermParseReal(Scanner_p in, TB_p bank, bool check_symb_prop) { Term_p handle; DStr_p id; FuncSymbType id_type; DStr_p source_name, errpos; long line, column; StreamType type; source_name = DStrGetRef(AktToken(in)->source); type = AktToken(in)->stream_type; line = AktToken(in)->line; column = AktToken(in)->column; /* Test for abbreviation */ if(TestInpTok(in, Mult)) { long abbrev; TermProperties properties = TPIgnoreProps; NextToken(in); abbrev = ParseInt(in); if(TestInpTok(in, Colon|Slash)) { /* This _defines_ the abbrev! */ if(PDArrayElementP(bank->ext_index, abbrev)) { /* Error: Abbreviation defined twice */ errpos = DStrAlloc(); DStrAppendStr(errpos, PosRep(type, source_name, line, column)); DStrAppendStr(errpos, "Abbreviation *"); DStrAppendInt(errpos, abbrev); DStrAppendStr(errpos, " already defined"); Error(DStrView(errpos), SYNTAX_ERROR); DStrFree(errpos); } if(TestInpTok(in, Slash)) { NextToken(in); properties = ParseInt(in); } NextToken(in); handle = TBTermParseReal(in, bank, check_symb_prop); /* Elegant, aint it? */ if(properties) { TBRefSetProp(bank, &handle, properties); } /* printf("# Term %ld = %ld\n", abbrev, handle->entry_no); */ PDArrayAssignP(bank->ext_index, abbrev, handle); } else { /* This references the abbrev */ handle = PDArrayElementP(bank->ext_index, abbrev); if(!handle) { /* Error: Undefined abbrev */ errpos = DStrAlloc(); DStrAppendStr(errpos, PosRep(type, source_name, line, column)); DStrAppendStr(errpos, "Abbreviation *"); DStrAppendInt(errpos, abbrev); DStrAppendStr(errpos, " undefined"); Error(DStrView(errpos), SYNTAX_ERROR); DStrFree(errpos); } } } else { /* Normal term stuff, bloated because of the nonsensical SETHEO syntax */ if(SigSupportLists && TestInpTok(in, OpenSquare)) { handle = tb_parse_cons_list(in, bank, check_symb_prop); } else { id = DStrAlloc(); if((id_type=TermParseOperator(in, id))==FSIdentVar) { handle = VarBankExtNameAssertAlloc(bank->vars, DStrView(id)); } else { handle = DefaultSharedTermCellAlloc(); if(TestInpTok(in, OpenBracket)) { if((id_type == FSIdentInt) &&(bank->sig->distinct_props & FPIsInteger)) { AktTokenError(in, "Number cannot have argument list (consider --free-numbers)", false); } if((id_type == FSIdentObject) &&(bank->sig->distinct_props & FPIsObject)) { AktTokenError(in, "Object cannot have argument list (consider --free-objects)", false); } handle->arity = tb_term_parse_arglist(in, &(handle->args), bank, check_symb_prop); } else { handle->arity = 0; } handle->f_code = TermSigInsert(bank->sig, DStrView(id), handle->arity, false, id_type); if(!handle->f_code) { errpos = DStrAlloc(); DStrAppendStr(errpos, PosRep(type, source_name, line, column)); DStrAppendStr(errpos, DStrView(id)); DStrAppendStr(errpos, " used with arity "); DStrAppendInt(errpos, (long)handle->arity); DStrAppendStr(errpos, ", but registered with arity "); DStrAppendInt(errpos, (long)(bank->sig)-> f_info[SigFindFCode(bank->sig, DStrView(id))].arity); Error(DStrView(errpos), SYNTAX_ERROR); DStrFree(errpos); } handle = tb_termtop_insert(bank, handle); } DStrFree(id); } } DStrReleaseRef(source_name); return handle; } /*----------------------------------------------------------------------- // // Function: TBRefSetProp() // // Make ref point to a term of the same structure as *ref, but with // properties prop set. Properties do not work for variables! // // Global Variables: - // // Side Effects : Changes bank, *ref // /----------------------------------------------------------------------*/ void TBRefSetProp(TB_p bank, TermRef ref, TermProperties prop) { Term_p term, new; assert(!TermIsVar(*ref)); term = *ref; if(TermCellQueryProp(term, prop)||TermIsVar(term)) { return; } new = TermTopCopy(term); TermCellSetProp(new, prop); new = tb_termtop_insert(bank, new); *ref = new; /* Old term will be garbage-collected eventually */ } /*----------------------------------------------------------------------- // // Function: TBRefDelProp() // // Make ref point to a term of the same structure as *ref, but with // properties prop deleted. If the term is a variable, do nothing! // // Global Variables: - // // Side Effects : Changes bank, *ref // /----------------------------------------------------------------------*/ void TBRefDelProp(TB_p bank, TermRef ref, TermProperties prop) { Term_p term, new; term = *ref; if(!TermCellIsAnyPropSet(term, prop)||TermIsVar(term)) { return; } new = TermTopCopy(term); TermCellDelProp(new, prop); new = tb_termtop_insert(bank, new); *ref = new; } /*----------------------------------------------------------------------- // // Function: TBTermDelPropCount() // // Delete properties prop in term, return number of term cells with // this property. Does assume that all subterms of a term without // this property also do not carry it! // // Global Variables: // // Side Effects : // /----------------------------------------------------------------------*/ long TBTermDelPropCount(Term_p term, TermProperties prop) { long count = 0; int i; PStack_p stack = PStackAlloc(); PStackPushP(stack, term); while(!PStackEmpty(stack)) { term = PStackPopP(stack); if(TermCellQueryProp(term, prop)) { TermCellDelProp(term, prop); count++; for(i=0; iarity; i++) { PStackPushP(stack, term->args[i]); } } } PStackFree(stack); return count; } /*----------------------------------------------------------------------- // // Function: TBGCMarkTerm() // // Mark a term as used for the garbage collector. // // Global Variables: - // // Side Effects : Marks the term, memory operations // /----------------------------------------------------------------------*/ void TBGCMarkTerm(TB_p bank, Term_p term) { PStack_p stack = PStackAlloc(); int i; assert(bank); assert(term); PStackPushP(stack, term); while(!PStackEmpty(stack)) { term = PStackPopP(stack); if(!TBTermCellIsMarked(bank,term)) { TermCellFlipProp(term, TPGarbageFlag); for(i=0; iarity; i++) { PStackPushP(stack, term->args[i]); } if(TermIsRewritten(term)) { PStackPushP(stack, TermRWReplaceField(term)); } } } PStackFree(stack); } /*----------------------------------------------------------------------- // // Function: TBGCSweep() // // Sweep the term bank and free all unmarked term // cells. bank->true_term will be marked automatically. Returns the // number of term cells recovered. // // Global Variables: - // // Side Effects : Memory operations, flips bank->garbage_state // /----------------------------------------------------------------------*/ long TBGCSweep(TB_p bank) { long recovered = 0; assert(bank); assert(!TermIsRewritten(bank->true_term)); TBGCMarkTerm(bank, bank->true_term); TBGCMarkTerm(bank, bank->false_term); if(bank->min_term) { TBGCMarkTerm(bank, bank->min_term); } VERBOUT("Garbage collection started.\n"); recovered = TermCellStoreGCSweep(&(bank->term_store), bank->garbage_state); VERBOSE(fprintf(stderr, "Garbage collection reclaimed %ld unused term cells.\n",recovered);); #ifdef PRINT_SOMEERRORS_STDOUT if(OutputLevel) { fprintf(GlobalOut, "# Garbage collection reclaimed %ld unused term cells.\n", recovered); } #endif bank->garbage_state = bank->garbage_state?TPIgnoreProps:TPGarbageFlag; return recovered; } /*----------------------------------------------------------------------- // // Function: TBCreateMinTerm() // // If bank->min_term exists, return it. Otherwise create and return // it. // // Global Variables: - // // Side Effects : Might set bank->min_term // /----------------------------------------------------------------------*/ Term_p TBCreateMinTerm(TB_p bank, FunCode min_const) { if(!bank->min_term) { Term_p t = TermConstCellAlloc(min_const); bank->min_term = TBInsert(bank, t, DEREF_NEVER); TermFree(t); } assert(bank->min_term->f_code == min_const); return bank->min_term; } /*----------------------------------------------------------------------- // // Function: TBTermCollectSubterms() // // Collect all subterms of term onto collector. Assumes that // TPOpFlag is set if and only if the term is already in the // collection. Returns the number of new terms found. // // Global Variables: - // // Side Effects : Sets the OpFlag of newly collected terms. // /----------------------------------------------------------------------*/ long TBTermCollectSubterms(Term_p term, PStack_p collector) { long res = 0; int i; assert(term); assert(TermIsShared(term)); if(!TermCellQueryProp(term, TPOpFlag)) { res = 1; TermCellSetProp(term, TPOpFlag); PStackPushP(collector, term); for(i=0; iarity; i++) { res += TBTermCollectSubterms(term->args[i], collector); } } return res; } /*---------------------------------------------------------------------*/ /* End of File */ /*---------------------------------------------------------------------*/