From 6c196ec8a41d6ed506c133c8b33dba9684f9a7a6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 12:34:43 +0000 Subject: Updated raytracer test. Added SPASS test. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- test/spass/subsumption.c | 2041 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 2041 insertions(+) create mode 100644 test/spass/subsumption.c (limited to 'test/spass/subsumption.c') diff --git a/test/spass/subsumption.c b/test/spass/subsumption.c new file mode 100644 index 00000000..d312cbf8 --- /dev/null +++ b/test/spass/subsumption.c @@ -0,0 +1,2041 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * SUBSUMPTION * */ +/* * * */ +/* * $Module: SUBSUMPTION * */ +/* * * */ +/* * Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001 * */ +/* * MPI fuer Informatik * */ +/* * * */ +/* * This program is free software; you can redistribute * */ +/* * it and/or modify it under the terms of the GNU * */ +/* * General Public License as published by the Free * */ +/* * Software Foundation; either version 2 of the License, * */ +/* * or (at your option) any later version. * */ +/* * * */ +/* * This program is distributed in the hope that it will * */ +/* * be useful, but WITHOUT ANY WARRANTY; without even * */ +/* * the implied warranty of MERCHANTABILITY or FITNESS * */ +/* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */ +/* * License for more details. * */ +/* * * */ +/* * You should have received a copy of the GNU General * */ +/* * Public License along with this program; if not, write * */ +/* * to the Free Software Foundation, Inc., 59 Temple * */ +/* * Place, Suite 330, Boston, MA 02111-1307 USA * */ +/* * * */ +/* * * */ +/* $Revision: 21527 $ * */ +/* $State$ * */ +/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */ +/* $Author: duraid $ * */ +/* * * */ +/* * Contact: * */ +/* * Christoph Weidenbach * */ +/* * MPI fuer Informatik * */ +/* * Stuhlsatzenhausweg 85 * */ +/* * 66123 Saarbruecken * */ +/* * Email: weidenb@mpi-sb.mpg.de * */ +/* * Germany * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +/* $RCSfile$ */ + + +#include "subsumption.h" + +static NAT multvec_i[subs__MAXLITS]; +static NAT multvec_j[subs__MAXLITS]; +static NAT stamp; + +static BOOL subs_InternIdc(CLAUSE, int, CLAUSE); +static BOOL subs_InternIdcEq(CLAUSE, int, CLAUSE); +static BOOL subs_InternIdcEqExcept(CLAUSE, int, CLAUSE, int); +static BOOL subs_InternIdcRes(CLAUSE, int, int, int); + +/* The following functions are currently unused */ +BOOL subs_IdcTestlits(CLAUSE, CLAUSE, LITPTR*); +BOOL subs_Testlits(CLAUSE, CLAUSE); + + +void subs_Init(void) +{ + int i; + + stamp = 0; + for (i = 0; i < subs__MAXLITS; i++) + multvec_i[i] = multvec_j[i] = 0; +} + + +static BOOL subs_TestlitsEq(CLAUSE c1, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1 and c2. + RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise. + CAUTION: None. +***********************************************************/ +{ + TERM t1,t2; + int i,j,n,k; + BOOL found; + + n = clause_Length(c1); + k = clause_Length(c2); + + for (i = 0; i < n; i++){ + j = 0; + found = FALSE; + t1 = clause_GetLiteralTerm(c1,i); + + do { + t2 = clause_GetLiteralTerm(c2,j); + cont_StartBinding(); + if (unify_Match(cont_LeftContext(), t1, t2)) + found = TRUE; + else{ + if (symbol_Equal(term_TopSymbol(t1),term_TopSymbol(t2)) && + fol_IsEquality(fol_Atom(t1)) && + fol_IsEquality(fol_Atom(t2)) && + (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,i)) || + clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,j)))) { + cont_BackTrackAndStart(); + if (unify_Match(cont_LeftContext(), + term_FirstArgument(fol_Atom(t1)), + term_SecondArgument(fol_Atom(t2))) && + unify_Match(cont_LeftContext(), + term_SecondArgument(fol_Atom(t1)), + term_FirstArgument(fol_Atom(t2)))) + found = TRUE; + else + j++; + } + else + j++; + } + cont_BackTrack(); + + } while (!found && j < k); + + if (!found) + return FALSE; + } + + return TRUE; +} + + +static BOOL subs_STMultiIntern(int i, CLAUSE c1, CLAUSE c2) +/********************************************************** + INPUT: Integers i,j and two clauses c1 and c2 + i and j stand for the i-th and the j-th literal + in the clause c1 respectively c2. + RETURNS: FALSE if c1 does not multisubsume c2 and TRUE otherwise. + CAUTION: None. +***********************************************************/ +{ + int n,j; + TERM lit1,lit2; + + j = 0; + n = clause_Length(c2); + lit1 = clause_GetLiteralTerm(c1,i); + + while (j < n) { + if (multvec_j[j] != stamp) { + lit2 = clause_GetLiteralTerm(c2,j); + cont_StartBinding(); + if (unify_Match(cont_LeftContext(),lit1,lit2)) { + if (i == (clause_Length(c1)-1)) { + cont_BackTrack(); + return TRUE; + } + multvec_j[j] = stamp; + if (subs_STMultiIntern(i+1, c1, c2)) { + cont_BackTrack(); + return TRUE; + } + multvec_j[j] = 0; + } + cont_BackTrack(); + if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) && + fol_IsEquality(fol_Atom(lit1)) && + fol_IsEquality(fol_Atom(lit2)) && + (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,i)) || + clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,j)))) { + cont_StartBinding(); + if (unify_Match(cont_LeftContext(), + term_FirstArgument(fol_Atom(lit1)), + term_SecondArgument(fol_Atom(lit2))) && + unify_Match(cont_LeftContext(), + term_SecondArgument(fol_Atom(lit1)), + term_FirstArgument(fol_Atom(lit2)))) { + if (i == (clause_Length(c1)-1)) { + cont_BackTrack(); + return TRUE; + } + multvec_j[j] = stamp; + if (subs_STMultiIntern(i+1, c1, c2)) { + cont_BackTrack(); + return TRUE; + } + multvec_j[j] = 0; + } + cont_BackTrack(); + } + } + j++; + } + return FALSE; +} + + +BOOL subs_STMulti(CLAUSE c1, CLAUSE c2) +{ + BOOL Result; + int n; + + n = clause_Length(c1); + + /*printf("\n St-Multi: %d -> %d",clause_Number(c1),clause_Number(c2));*/ + + if (n > clause_Length(c2) || + (n > 1 && !subs_TestlitsEq(c1,c2))) { + /*fputs(" Testlits failure ", stdout);*/ + return(FALSE); + } + + if (++stamp == NAT_MAX) { + int i; + stamp = 1; + for (i = 0; i < subs__MAXLITS; i++) + multvec_i[i] = multvec_j[i] = 0; + } + /*unify_SaveState();*/ + Result = subs_STMultiIntern(0,c1,c2); + /*unify_CheckState();*/ + return Result; +} + + +static BOOL subs_TestlitsEqExcept(CLAUSE C1, CLAUSE C2) +{ + TERM t1,t2; + int i,j,n,k; + BOOL found; + + n = clause_Length(C1); + k = clause_Length(C2); + + i = 0; + while (multvec_i[i] == stamp && i < n) + i++; + + while (i < n) { + j = 0; + found = FALSE; + t1 = clause_GetLiteralTerm(C1,i); + + do { + if (multvec_j[j] == stamp) + j++; + else { + t2 = clause_GetLiteralTerm(C2,j); + cont_StartBinding(); + if (unify_MatchBindings(cont_LeftContext(), t1, t2)) + found = TRUE; + else { + if (symbol_Equal(term_TopSymbol(t1),term_TopSymbol(t2)) && + fol_IsEquality(fol_Atom(t1)) && + fol_IsEquality(fol_Atom(t2)) && + (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) || + clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) { + cont_BackTrackAndStart(); + if (unify_MatchBindings(cont_LeftContext(), + term_FirstArgument(fol_Atom(t1)), + term_SecondArgument(fol_Atom(t2))) && + unify_MatchBindings(cont_LeftContext(), + term_SecondArgument(fol_Atom(t1)), + term_FirstArgument(fol_Atom(t2)))) + found = TRUE; + else + j++; + } + else + j++; + } + cont_BackTrack(); + } /* else */ + } while (!found && (j < k)); + + if (!found) + return FALSE; + do + i++; + while (multvec_i[i] == stamp && i < n); + } /* while i < n */ + + + return TRUE; +} + + +static BOOL subs_STMultiExceptIntern(CLAUSE C1, CLAUSE C2) +{ + int n, i, j, k; + NAT occs, occsaux; + TERM lit1,lit2; + + i = -1; + k = 0; + occs = 0; + j = 0; + n = clause_Length(C2); + + while (k < clause_Length(C1)) { + /* Select Literal with maximal number of variable occurrences. */ + if (multvec_i[k] != stamp) { + if (i < 0) { + i = k; + occs = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,i)); + } else + if ((occsaux = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,k))) + > occs) { + i = k; + occs = occsaux; + } + } + k++; + } + + if (i < 0) + return TRUE; + + lit1 = clause_GetLiteralTerm(C1, i); + multvec_i[i] = stamp; + + while (j < n) { + if (multvec_j[j] != stamp) { + lit2 = clause_GetLiteralTerm(C2, j); + cont_StartBinding(); + if (unify_MatchBindings(cont_LeftContext(), lit1, lit2)) { + multvec_j[j] = stamp; + if (subs_STMultiExceptIntern(C1, C2)) { + cont_BackTrack(); + return TRUE; + } + multvec_j[j] = 0; + } + cont_BackTrack(); + if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) && + fol_IsEquality(fol_Atom(lit1)) && + fol_IsEquality(fol_Atom(lit2)) && + (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) || + clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) { + cont_StartBinding(); + if (unify_MatchBindings(cont_LeftContext(), + term_FirstArgument(fol_Atom(lit1)), + term_SecondArgument(fol_Atom(lit2))) && + unify_MatchBindings(cont_LeftContext(), + term_SecondArgument(fol_Atom(lit1)), + term_FirstArgument(fol_Atom(lit2)))) { + multvec_j[j] = stamp; + if (subs_STMultiExceptIntern(C1, C2)) { + cont_BackTrack(); + return TRUE; + } + multvec_j[j] = 0; + } + cont_BackTrack(); + } + } + j++; + } + multvec_i[i] = 0; + return FALSE; +} + + +BOOL subs_STMultiExcept(CLAUSE C1, CLAUSE C2, int ExceptI, int ExceptJ) +/********************************************************** + INPUT: Two clauses and for each clause a literal that is + already bound to each other. If the literal value is negative, + a general subsumption test is performed. + RETURNS: TRUE if the first clause subsumes the second one. + CAUTION: The weight of the clauses must be up to date! +***********************************************************/ +{ + BOOL Result; + int n; + + n = clause_Length(C1); + + if (n > clause_Length(C2) || + (clause_Weight(C1)-clause_LiteralWeight(clause_GetLiteral(C1,ExceptI))) > + (clause_Weight(C2)-clause_LiteralWeight(clause_GetLiteral(C2,ExceptJ)))) + return FALSE; + + if (++stamp == NAT_MAX) { + int i; + stamp = 1; + for (i = 0; i < subs__MAXLITS; i++) + multvec_i[i] = multvec_j[i] = 0; + } + multvec_i[ExceptI] = stamp; + multvec_j[ExceptJ] = stamp; + + if (n > 1 && !subs_TestlitsEqExcept(C1, C2)) + return FALSE; + + /*unify_SaveState();*/ + Result = subs_STMultiExceptIntern(C1, C2); + /*unify_CheckState();*/ + return Result; +} + + +static BOOL subs_PartnerTest(CLAUSE C1, int c1l, int c1r, CLAUSE C2, int c2l, int c2r) +/********************************************************** + INPUT: Two clauses and for each clause a starting left index + and an exclusive right index. + RETURNS: TRUE if every literal inside the bounds of the first clause + can be matched against a literal inside the bounds of the + second clause. + CAUTION: None. +***********************************************************/ +{ + TERM t1,t2; + int j; + BOOL found; + + if (c1l == c1r) + return TRUE; + + while (multvec_i[c1l] == stamp && c1l < c1r) + c1l++; + + if (c1l < c1r) { + if (c2l == c2r) + return FALSE; + else + do { + j = c2l; + found = FALSE; + t1 = clause_GetLiteralTerm(C1,c1l); + + do { + if (multvec_j[j] == stamp) + j++; + else { + t2 = clause_GetLiteralTerm(C2,j); + cont_StartBinding(); + if (unify_MatchBindings(cont_LeftContext(), t1, t2)) + found = TRUE; + else { + if (symbol_Equal(term_TopSymbol(t1),term_TopSymbol(t2)) && + fol_IsEquality(fol_Atom(t1)) && + fol_IsEquality(fol_Atom(t2)) && + (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,c1l)) || + clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) { + cont_BackTrackAndStart(); + if (unify_MatchBindings(cont_LeftContext(), + term_FirstArgument(fol_Atom(t1)), + term_SecondArgument(fol_Atom(t2))) && + unify_MatchBindings(cont_LeftContext(), + term_SecondArgument(fol_Atom(t1)), + term_FirstArgument(fol_Atom(t2)))) + found = TRUE; + else + j++; + } + else + j++; + } + cont_BackTrack(); + } /* else */ + } while (!found && (j < c2r)); + + if (!found) + return FALSE; + do + c1l++; + while (multvec_i[c1l] == stamp && c1l < c1r); + } while (c1l < c1r); + } + return TRUE; +} + + +static BOOL subs_SubsumesInternBasic(CLAUSE C1, int c1fa, int c1fs, int c1l, + CLAUSE C2, int c2fa, int c2fs, int c2l) +{ + int i, j, n, k; + NAT occs, occsaux; + TERM lit1,lit2; + + i = -1; + k = clause_FirstLitIndex(); + occs = 0; + + while (k < c1l) { /* Select literal with maximal variable occurrences. */ + if (multvec_i[k] != stamp) { + if (i < 0) { + i = k; + occs = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,i)); + } else + if ((occsaux = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,k))) + > occs) { + i = k; + occs = occsaux; + } + } + k++; + } + + if (i < 0) + return TRUE; + + lit1 = clause_GetLiteralTerm(C1, i); + multvec_i[i] = stamp; + + if (i < c1fa) { /* Only consider relevant partner literals */ + j = clause_FirstLitIndex(); + n = c2fa; + } + else if (i < c1fs) { + j = c2fa; + n = c2fs; + } + else { + j = c2fs; + n = c2l; + } + + while (j < n) { + if (multvec_j[j] != stamp) { + lit2 = clause_GetLiteralTerm(C2, j); + cont_StartBinding(); + if (unify_MatchBindings(cont_LeftContext(), lit1, lit2)) { + multvec_j[j] = stamp; + if (subs_SubsumesInternBasic(C1,c1fa,c1fs,c1l,C2,c2fa,c2fs,c2l)) { + cont_BackTrack(); + return TRUE; + } + multvec_j[j] = 0; + } + cont_BackTrack(); + if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) && + fol_IsEquality(fol_Atom(lit1)) && + fol_IsEquality(fol_Atom(lit2)) && + (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) || + clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) { + cont_StartBinding(); + if (unify_MatchBindings(cont_LeftContext(), + term_FirstArgument(fol_Atom(lit1)), + term_SecondArgument(fol_Atom(lit2))) && + unify_MatchBindings(cont_LeftContext(), + term_SecondArgument(fol_Atom(lit1)), + term_FirstArgument(fol_Atom(lit2)))) { + multvec_j[j] = stamp; + if (subs_SubsumesInternBasic(C1,c1fa,c1fs,c1l,C2,c2fa,c2fs,c2l)) { + cont_BackTrack(); + return TRUE; + } + multvec_j[j] = 0; + } + cont_BackTrack(); + } + } + j++; + } + multvec_i[i] = 0; + return FALSE; +} + + +BOOL subs_SubsumesBasic(CLAUSE C1, CLAUSE C2, int ExceptI, int ExceptJ) +/********************************************************** + INPUT: Two clauses and for each clause a literal that are + already bound to each other. If the literal value is negative, + a general subsumption test is performed. + RETURNS: TRUE if the first clause subsumes the second one with respect + to basic restrictions on the sort literals. + CAUTION: The weight of the clauses must be up to date! +***********************************************************/ +{ + BOOL Result; + int c1fa,c1fs,c1l,c2fa,c2fs,c2l,lw1,lw2; + + c1fa = clause_FirstAntecedentLitIndex(C1); + c1fs = clause_FirstSuccedentLitIndex(C1); + c1l = clause_Length(C1); + c2fa = clause_FirstAntecedentLitIndex(C2); + c2fs = clause_FirstSuccedentLitIndex(C2); + c2l = clause_Length(C2); + + lw1 = (ExceptI >= clause_FirstLitIndex() ? + clause_LiteralWeight(clause_GetLiteral(C1,ExceptI)) : 0); + lw2 = (ExceptJ >= clause_FirstLitIndex() ? + clause_LiteralWeight(clause_GetLiteral(C2,ExceptJ)) : 0); + + if (c1l > c2l || /* Multiset restriction */ + (clause_Weight(C1)-lw1) > (clause_Weight(C2)-lw2)) { + return FALSE; + } + + if (++stamp == NAT_MAX) { + int i; + stamp = 1; + for (i = 0; i < subs__MAXLITS; i++) + multvec_i[i] = multvec_j[i] = 0; + } + + if (ExceptI >= clause_FirstLitIndex()) + multvec_i[ExceptI] = stamp; + if (ExceptJ >= clause_FirstLitIndex()) + multvec_j[ExceptJ] = stamp; + + if (c1l > 1 && + (!subs_PartnerTest(C1,clause_FirstConstraintLitIndex(C1),c1fa, + C2,clause_FirstConstraintLitIndex(C2),c2fa) || + !subs_PartnerTest(C1,c1fa,c1fs,C2,c2fa,c2fs) || + !subs_PartnerTest(C1,c1fs,c1l,C2,c2fs,c2l))) + return FALSE; + +#ifdef CHECK + cont_SaveState(); +#endif + + Result = subs_SubsumesInternBasic(C1,c1fa,c1fs,c1l,C2,c2fa,c2fs,c2l); + +#ifdef CHECK + cont_CheckState(); +#endif + + return Result; +} + + +static BOOL subs_SubsumesInternWithSignature(int i, CLAUSE c1, CLAUSE c2, BOOL Variants, LIST* Bindings) +/********************************************************** + INPUT: + RETURNS: + CAUTION: +***********************************************************/ +{ + int n,j; + TERM lit1,lit2; + LIST NewBindings,Scan; + + j = 0; + n = clause_Length(c2); + lit1 = clause_GetLiteralTerm(c1,i); + NewBindings = list_Nil(); + + while (j < n) { + if (multvec_j[j] != stamp) { + lit2 = clause_GetLiteralTerm(c2,j); + cont_StartBinding(); + if (fol_SignatureMatch(lit1,lit2,&NewBindings,Variants)) { + if (i == (clause_Length(c1)-1)) { + *Bindings = list_Nconc(NewBindings,*Bindings); + return TRUE; + } + multvec_j[j] = stamp; + if (subs_SubsumesInternWithSignature(i+1, c1, c2,Variants,&NewBindings)) { + *Bindings = list_Nconc(NewBindings,*Bindings); + return TRUE; + } + multvec_j[j] = 0; + } + for (Scan=NewBindings;!list_Empty(Scan);Scan=list_Cdr(Scan)) { /* Backtrack bindings */ + if (symbol_IsVariable((SYMBOL)list_Car(Scan))) + term_ClearBinding((SYMBOL)list_Car(Scan)); + else + symbol_ContextClearValue((SYMBOL)list_Car(Scan)); + } + list_Delete(NewBindings); + NewBindings = list_Nil(); + if (symbol_Equal(term_TopSymbol(fol_Atom(lit1)),term_TopSymbol(fol_Atom(lit2))) && + fol_IsEquality(fol_Atom(lit1))) { + if (fol_SignatureMatch(term_FirstArgument(fol_Atom(lit1)), + term_SecondArgument(fol_Atom(lit2)), &NewBindings, Variants) && + fol_SignatureMatch(term_SecondArgument(fol_Atom(lit1)), + term_FirstArgument(fol_Atom(lit2)), &NewBindings, Variants)) { + if (i == (clause_Length(c1)-1)) { + *Bindings = list_Nconc(NewBindings,*Bindings); + return TRUE; + } + multvec_j[j] = stamp; + if (subs_SubsumesInternWithSignature(i+1, c1, c2,Variants,&NewBindings)) { + *Bindings = list_Nconc(NewBindings,*Bindings); + return TRUE; + } + multvec_j[j] = 0; + } + for (Scan=NewBindings;!list_Empty(Scan);Scan=list_Cdr(Scan)) { /* Backtrack bindings */ + if (symbol_IsVariable((SYMBOL)list_Car(Scan))) + term_ClearBinding((SYMBOL)list_Car(Scan)); + else + symbol_ContextClearValue((SYMBOL)list_Car(Scan)); + } + list_Delete(NewBindings); + NewBindings = list_Nil(); + } + } + j++; + } + return FALSE; +} + +BOOL subs_SubsumesWithSignature(CLAUSE C1, CLAUSE C2, BOOL Variants, LIST *Bindings) +/********************************************************** + INPUT: Two clauses . + RETURNS: TRUE if the first clause subsumes the second one where + we allow signature symbols to be matched as well. + If is TRUE variables must be mapped to variables. + Returns the signature symbols that were bound. + EFFECT: Symbol context bindings are established. +***********************************************************/ +{ + BOOL Result; + + if (clause_Length(C1) > clause_Length(C2) || + clause_NumOfSuccLits(C1) > clause_NumOfSuccLits(C2) || + (clause_NumOfAnteLits(C1) + clause_NumOfConsLits(C1)) > + (clause_NumOfAnteLits(C2) + clause_NumOfConsLits(C2))) { /* Multiset restriction */ + return FALSE; + } + + if (++stamp == NAT_MAX) { + int i; + stamp = 1; + for (i = 0; i < subs__MAXLITS; i++) + multvec_i[i] = multvec_j[i] = 0; + } + + term_NewMark(); + Result = subs_SubsumesInternWithSignature(clause_FirstLitIndex(),C1,C2,Variants, Bindings); + *Bindings = list_DeleteElementIf(*Bindings, (BOOL (*)(POINTER)) symbol_IsVariable); + return Result; +} + +static BOOL subs_SubsumesIntern(CLAUSE C1, int c1fs, int c1l, CLAUSE C2, int c2fs, int c2l) +{ + int i, j, n, k; + NAT occs, occsaux; + TERM lit1,lit2; + + i = -1; + k = clause_FirstLitIndex(); + occs = 0; + + while (k < c1l) { /* Select literal with maximal variable occurrences. */ + if (multvec_i[k] != stamp) { + if (i < 0) { + i = k; + occs = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,i)); + } else + if ((occsaux = term_NumberOfVarOccs(clause_GetLiteralAtom(C1,k))) + > occs) { + i = k; + occs = occsaux; + } + } + k++; + } + + if (i < 0) + return TRUE; + + lit1 = clause_GetLiteralTerm(C1, i); + multvec_i[i] = stamp; + + if (i < c1fs) { /* Only consider relevant partner literals */ + j = clause_FirstLitIndex(); + n = c2fs; + } + else { + j = c2fs; + n = c2l; + } + + while (j < n) { + if (multvec_j[j] != stamp) { + lit2 = clause_GetLiteralTerm(C2, j); + cont_StartBinding(); + if (unify_MatchBindings(cont_LeftContext(), lit1, lit2)) { + multvec_j[j] = stamp; + if (subs_SubsumesIntern(C1,c1fs,c1l,C2,c2fs,c2l)) { + cont_BackTrack(); + return TRUE; + } + multvec_j[j] = 0; + } + cont_BackTrack(); + if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) && + fol_IsEquality(fol_Atom(lit1)) && + fol_IsEquality(fol_Atom(lit2)) && + (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C1,i)) || + clause_LiteralIsNotOrientedEquality(clause_GetLiteral(C2,j)))) { + cont_StartBinding(); + if (unify_MatchBindings(cont_LeftContext(), + term_FirstArgument(fol_Atom(lit1)), + term_SecondArgument(fol_Atom(lit2))) && + unify_MatchBindings(cont_LeftContext(), + term_SecondArgument(fol_Atom(lit1)), + term_FirstArgument(fol_Atom(lit2)))) { + multvec_j[j] = stamp; + if (subs_SubsumesIntern(C1,c1fs,c1l,C2,c2fs,c2l)) { + cont_BackTrack(); + return TRUE; + } + multvec_j[j] = 0; + } + cont_BackTrack(); + } + } + j++; + } + multvec_i[i] = 0; + return FALSE; +} + + +BOOL subs_Subsumes(CLAUSE C1, CLAUSE C2, int ExceptI, int ExceptJ) +/********************************************************** + INPUT: Two clauses and for each clause a literal that is + already bound to each other. If the literal value is negative, + a general subsumption test is performed. + RETURNS: TRUE if the first clause subsumes the second one. + CAUTION: The weight of the clauses must be up to date! +***********************************************************/ +{ + BOOL Result; + int c1fs, c1l, c2fs, c2l, lw1, lw2; + + c1fs = clause_FirstSuccedentLitIndex(C1); + c1l = clause_Length(C1); + c2fs = clause_FirstSuccedentLitIndex(C2); + c2l = clause_Length(C2); + + lw1 = (ExceptI >= clause_FirstLitIndex() ? + clause_LiteralWeight(clause_GetLiteral(C1,ExceptI)) : 0); + lw2 = (ExceptJ >= clause_FirstLitIndex() ? + clause_LiteralWeight(clause_GetLiteral(C2,ExceptJ)) : 0); + + if (c1l > c2l || /* Multiset restriction */ + (clause_Weight(C1) - lw1) > (clause_Weight(C2) - lw2)) + return FALSE; + + if (++stamp == NAT_MAX) { + int i; + stamp = 1; + for (i = 0; i < subs__MAXLITS; i++) + multvec_i[i] = multvec_j[i] = 0; + } + + if (ExceptI >= clause_FirstLitIndex()) + multvec_i[ExceptI] = stamp; + if (ExceptJ >= clause_FirstLitIndex()) + multvec_j[ExceptJ] = stamp; + + if (c1l > 1 && + (!subs_PartnerTest(C1,clause_FirstConstraintLitIndex(C1),c1fs, + C2,clause_FirstConstraintLitIndex(C2),c2fs) || + !subs_PartnerTest(C1,c1fs,c1l,C2,c2fs,c2l))) + return FALSE; + +#ifdef CHECK + cont_SaveState(); +#endif + + Result = subs_SubsumesIntern(C1,c1fs,c1l,C2,c2fs,c2l); + +#ifdef CHECK + cont_CheckState(); +#endif + + return Result; +} + + + + +BOOL subs_ST(int i, int j, CLAUSE c1, CLAUSE c2) +/********************************************************** + INPUT: Integers i,j and two clauses c1 and c2. + i and j stand for the i-th and the j-th literal + in the clause c1 respectively c2. + RETURNS: FALSE if c1 does not subsume c2 and TRUE otherwise. + CAUTION: None. +***********************************************************/ +{ + cont_StartBinding(); + + while ((j < clause_Length(c2)) && + !(unify_Match(cont_LeftContext(), + clause_GetLiteralTerm(c1,i), + clause_GetLiteralTerm(c2,j)))){ + j++; + cont_BackTrackAndStart(); + } + + if (j >= clause_Length(c2)) { + cont_BackTrack(); + return FALSE; + } + + if ((i == (clause_Length(c1)-1)) || subs_ST(i+1, 0, c1, c2)) + return TRUE; + else + cont_BackTrack(); + + if (++j == clause_Length(c2)) + return FALSE; + + return subs_ST(i, j, c1, c2); +} + + +BOOL subs_Testlits(CLAUSE c1, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1 and c2. + RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise. + CAUTION: None. +***********************************************************/ +{ + TERM t1; + int i,j; + BOOL found; + + for (i = 0; i < clause_Length(c1); i++){ + j = 0; + found = FALSE; + t1 = clause_GetLiteralTerm(c1,i); + + do { + cont_StartBinding(); + if (!(found = unify_Match(cont_LeftContext(), t1, clause_GetLiteralTerm(c2,j)))) + j++; + cont_BackTrack(); + + } while (!found && (j < clause_Length(c2))); + + if (!found) + return FALSE; + } + + return TRUE; +} + + +static LIST subs_GetVariables(TERM t) +/********************************************************** + INPUT: A term. + RETURNS: The list of non bound variables of the term. + CAUTION: None. +***********************************************************/ +{ + LIST scan,insert,symbols,end; + + symbols = term_VariableSymbols(t); + insert = symbols; + end = list_Nil(); + + for (scan = symbols; !list_Empty(scan); scan = list_Cdr(scan)) { + if (!cont_VarIsBound(cont_LeftContext(), (SYMBOL)list_Car(scan))) { + end = insert; + list_Rplaca(insert, list_Car(scan)); + insert = list_Cdr(insert); + } + } + + if (!list_Empty(insert)) { + list_Delete(insert); + if (list_Empty(end)) + symbols = list_Nil(); + else + list_Rplacd(end,list_Nil()); + } + + return(symbols); +} + + +static BOOL subs_SubsumptionPossible(CLAUSE c1, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1 and c2. + RETURNS: TRUE if every literal in c1 can independently be + matched to a literal in c2. + CAUTION: None. +***********************************************************/ +{ + int i,j; + + for (i = 0; i < clause_Length(c1); i++) { + for (j = 0; j < clause_Length(c2); j++) { + cont_StartBinding(); + if (unify_Match(cont_LeftContext(), + clause_GetLiteralTerm(c1,i), + clause_GetLiteralTerm(c2,j))) + j = clause_Length(c2) + 1; + cont_BackTrack(); + } + if (j == clause_Length(c2)) + return FALSE; + } + + return TRUE; +} + + +BOOL subs_IdcTestlits(CLAUSE c1, CLAUSE c2, LITPTR* litptr) +/********************************************************** + INPUT: Two clauses c1, c2 and a pointer to a litptr structure. + RETURNS: FALSE if c1 can not independently be matched + to c2 and TRUE otherwise. + CAUTION: A structure is build and litptr points to that structure. +***********************************************************/ +{ + LIST TermIndexlist,VarSymbList,TermSymbList; + int i; + + if (subs_SubsumptionPossible(c1,c2)) { + + TermIndexlist = list_Nil(); + VarSymbList = list_Nil(); + TermSymbList = list_Nil(); + + for (i = 0; i < clause_Length(c1); i++) { + VarSymbList = subs_GetVariables(clause_GetLiteralTerm(c1,i)); + + if (VarSymbList != list_Nil()){ + TermIndexlist = list_Cons((POINTER)i, TermIndexlist); + TermSymbList = list_Cons(VarSymbList,TermSymbList); + } + } + + *litptr = litptr_Create(TermIndexlist,TermSymbList); + + list_Delete(TermSymbList); + list_Delete(TermIndexlist); + + return TRUE; + } + return FALSE; +} + + +static BOOL subs_SubsumptionVecPossible(CLAUSE c1, int vec, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1 and c2 and a vector pointer. + RETURNS: TRUE if all literals in c1 which indexes stand + in the vector with bottom pointer vec can + independently be matched to a literal in c2. + CAUTION: None. +***********************************************************/ +{ + int i,j; + + for (i = vec; i < vec_ActMax(); i++) { + for (j = 0; j < clause_Length(c2); j++) { + cont_StartBinding(); + if (unify_Match(cont_LeftContext(), + clause_GetLiteralTerm(c1, (int) vec_GetNth(i)), + clause_GetLiteralTerm(c2,j))) + j = clause_Length(c2) + 1; + cont_BackTrack(); + } + if (j == clause_Length(c2)) + return FALSE; + } + + return TRUE; +} + + +static BOOL subs_SubsumptionVecPossibleEq(CLAUSE c1, int vec, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1 and c2 and a vector pointer. + RETURNS: TRUE if all literals in c1 which indexes stand + in the vector with bottom pointer vec can + independently be matched to a literal in c2. + CAUTION: None. +***********************************************************/ +{ + int i,j,n; + TERM lit1,lit2; + + n = clause_Length(c2); + for (i = vec; i < vec_ActMax(); i++) { + lit1 = clause_GetLiteralTerm(c1, (int) vec_GetNth(i)); + for (j=0;j 0){ + for (j = 0; j < n; j++) { + if (!literal_GetUsed(litptr_Literal(litptr,j))) { + complist = list_Cons((POINTER)j,complist); + vec_Push((POINTER)literal_GetLitIndex(litptr_Literal(litptr,j))); + literal_PutUsed(litptr_Literal(litptr,j), TRUE); + j = n + 1; + } + } + + if (j != n) { + end = complist; + for (scan = complist; !list_Empty(scan); scan = list_Cdr(scan)) { + lit = (int)list_Car(scan); + for (i = 0; i < n; i++) { + if (!literal_GetUsed(litptr_Literal(litptr,i)) && + list_HasIntersection(literal_GetLitVarList(litptr_Literal(litptr,lit)), + literal_GetLitVarList(litptr_Literal(litptr,i)))) { + list_Rplacd(end,list_List((POINTER)i)); + end = list_Cdr(end); + vec_Push((POINTER)literal_GetLitIndex(litptr_Literal(litptr,i))); + literal_PutUsed(litptr_Literal(litptr,i), TRUE); + } + } + } + list_Delete(complist); + } + } +} + + +static BOOL subs_StVec(int i, int j, CLAUSE c1, CLAUSE c2) +/********************************************************** + INPUT: Integers i,j and two clauses c1 and c2. + i is a pointer to vector and represents a + literal in clause c1 and j stand for the j-th + literal in the clause c2. + RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise. + CAUTION: None. +***********************************************************/ +{ + int a; + + if (j >= clause_Length(c2)) + return FALSE; + + a = j; + + cont_StartBinding(); + + while ((a < clause_Length(c2)) && + !(unify_Match(cont_LeftContext(), + clause_GetLiteralTerm(c1, (int) vec_GetNth(i)), + clause_GetLiteralTerm(c2,a)))){ + a++; + cont_BackTrackAndStart(); + } + + if (a >= clause_Length(c2)) { + cont_BackTrack(); + return FALSE; + } + + if ((i == (vec_ActMax()-1)) || subs_StVec(i+1, 0, c1, c2)) + return TRUE; + else + cont_BackTrack(); + + return subs_StVec(i, a+1, c1, c2); +} + + +static int subs_SearchTop(CLAUSE c1, int vec, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1, c2, a vector pointer vec. + RETURNS: The index of that literal in c1 which has the least positive + matching tests with the literals in c2. + CAUTION: None. +***********************************************************/ +{ + int index, i, j, zaehler; + + index = (int)vec_GetNth(vec); + + for (i = vec; i < vec_ActMax(); i++) { + zaehler = 0; + j = 0; + while (j < clause_Length(c2) && zaehler < 2) { + cont_StartBinding(); + if (unify_Match(cont_LeftContext(), + clause_GetLiteralTerm(c1, (int) vec_GetNth(i)), + clause_GetLiteralTerm(c2,j))) { + zaehler++; + } + cont_BackTrack(); + j++; + } + + if (zaehler == 0 || zaehler == 1) { + index = (int)vec_GetNth(i); + return index; + } + } + return index; +} + + +static BOOL subs_TcVec(CLAUSE c1, int vec, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1, c2, a vector pointer vec. + RETURNS: FALSE if the literals of c1 which are designated by + the elements of vec do not subsume c2 and TRUE otherwise. + CAUTION: None. +***********************************************************/ +{ + int a,top_index; + a = 0; + + top_index = subs_SearchTop(c1,vec,c2); + + do { + cont_StartBinding(); + while ((a < clause_Length(c2)) && + !(unify_Match(cont_LeftContext(), + clause_GetLiteralTerm(c1,top_index), + clause_GetLiteralTerm(c2,a)))) { + a++; + cont_BackTrackAndStart(); + } + + if (a >= clause_Length(c2)){ + cont_BackTrack(); + return FALSE; + } + + if ((vec - vec_ActMax()) == 1) + return TRUE; + + if (subs_InternIdc(c1, vec, c2)) + return TRUE; + else { + cont_BackTrack(); /* Dies ist der 'Hurra' Fall.*/ + a++; + } + + } while (a < clause_Length(c2)); + + return FALSE; +} + +static BOOL subs_TcVecEq(CLAUSE c1, int vec, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1, c2, a vector pointer vec. + RETURNS: FALSE if the literals of c1 which are designated by + the elements of vec do not subsume c2 and TRUE otherwise. + CAUTION: None. +***********************************************************/ +{ + int a,top_index; + BOOL search; + TERM lit1,lit2; + + a = 0; + top_index = subs_SearchTop(c1,vec,c2); + lit1 = clause_GetLiteralTerm(c1,top_index); + + do { + search = TRUE; + + while (a < clause_Length(c2) && search) { + lit2 = clause_GetLiteralTerm(c2,a); + cont_StartBinding(); + if (unify_Match(cont_LeftContext(),lit1,lit2)) + search = FALSE; + else { + if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) && + fol_IsEquality(fol_Atom(lit1)) && + fol_IsEquality(fol_Atom(lit2)) && + (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,top_index)) || + clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,a)))) { + cont_BackTrackAndStart(); + if (unify_Match(cont_LeftContext(), + term_FirstArgument(fol_Atom(lit1)), + term_SecondArgument(fol_Atom(lit2))) && + unify_Match(cont_LeftContext(), + term_SecondArgument(fol_Atom(lit1)), + term_FirstArgument(fol_Atom(lit2)))) + search = FALSE; + } + if (search) { + a++; + cont_BackTrack(); + } + } + } + + if (a >= clause_Length(c2)) { + cont_BackTrack(); + return FALSE; + } + + if ((vec_ActMax() - vec) == 1) + return TRUE; + + if (subs_InternIdcEq(c1, vec, c2)) + return TRUE; + else { + cont_BackTrack(); + a++; + } + + } while (a < clause_Length(c2)); + + return FALSE; +} + + +static BOOL subs_InternIdc(CLAUSE c1, int vec, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1, c2, a vector pointer vec. + RETURNS: FALSE if the literals of c1 which are designed by + the elements of vec do not subsume c2 and TRUE otherwise. + CAUTION: +***********************************************************/ +{ + int locvec; + LITPTR litptr; + + + if (!subs_IdcVecTestlits(c1,vec,c2,&litptr)) + return FALSE; + + locvec = vec_ActMax(); + + do { + subs_CompVec(litptr); + if (!vec_IsMax(locvec)) { + if (!subs_TcVec(c1,locvec,c2)) { + vec_SetMax(locvec); + litptr_Delete(litptr); + return FALSE; + } + else + vec_SetMax(locvec); + } + } while (!litptr_AllUsed(litptr)); + + litptr_Delete(litptr); + + return TRUE; +} + + +static BOOL subs_InternIdcEq(CLAUSE c1, int vec, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1, c2, a vector pointer vec. + RETURNS: FALSE if the literals of c1 which are designed by + the elements of vec do not subsume c2 and TRUE otherwise. + CAUTION: +***********************************************************/ +{ + int locvec; + LITPTR litptr; + + + if (!subs_IdcVecTestlitsEq(c1,vec,c2,&litptr)) + return FALSE; + + locvec = vec_ActMax(); + + do { + subs_CompVec(litptr); + if (!vec_IsMax(locvec)) { + if (!subs_TcVecEq(c1,locvec,c2)) { + vec_SetMax(locvec); + litptr_Delete(litptr); + return FALSE; + } + else + vec_SetMax(locvec); + } + + } while (!litptr_AllUsed(litptr)); + + litptr_Delete(litptr); + + return TRUE; +} + + +BOOL subs_Idc(CLAUSE c1, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1, c2. + RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise. + CAUTION: +***********************************************************/ +{ + int i,vec; + BOOL Result; + + vec = vec_ActMax(); + + for (i = 0; i < clause_Length(c1); i++) + vec_Push((POINTER) i); + + Result = subs_InternIdc(c1,vec,c2); + + vec_SetMax(vec); + + cont_Reset(); + + return Result; +} + + +BOOL subs_IdcEq(CLAUSE c1, CLAUSE c2) +/********************************************************** + INPUT: Two clauses c1, c2. + RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise. + CAUTION: +***********************************************************/ +{ + int i,vec; + BOOL Result; + + /*fputs("\n Idc on: ", stdout); clause_Print(c1); + putchar('\t'); clause_Print(c2); */ + vec = vec_ActMax(); + + for (i = 0; i < clause_Length(c1); i++) + vec_Push((POINTER) i); + + Result = subs_InternIdcEq(c1,vec,c2); + + vec_SetMax(vec); + + cont_Reset(); + + /*printf(" Result: %s ",(Result ? "TRUE" : "FALSE"));*/ + + return Result; +} + + +BOOL subs_IdcEqMatch(CLAUSE c1, CLAUSE c2, SUBST subst) +/********************************************************** + INPUT: Two clauses c1, c2. + RETURNS: FALSE if c1 do not subsume c2 and TRUE otherwise. + CAUTION: +***********************************************************/ +{ + int i,vec; + BOOL Result; + + /* fputs("\n Idc on: ", stdout); clause_Print(c1); + putchar('\t'); clause_Print(c2); DBG */ + vec = vec_ActMax(); + + for (i = 0; i < clause_Length(c1); i++) + vec_Push((POINTER) i); + + i = 0; /* Doesn't matter, there is a general cont_Reset below */ + unify_EstablishMatcher(cont_LeftContext(), subst); + + Result = subs_InternIdcEq(c1,vec,c2); + + vec_SetMax(vec); + + cont_Reset(); + + /*fputs("\nsubs_Idc end: ",stdout); clause_Print(c1); clause_Print(c2); DBG */ + + return Result; +} + + +static BOOL subs_SubsumptionVecPossibleRes(CLAUSE c1, int vec, + int beg, int end) +/********************************************************** + INPUT: Two clauses c1 and c2 and three vector pointer + vec,beg and end. + RETURNS: TRUE if all literals in c1 which indexes stand + in the vector with bottom pointer vec can + independently be matched to a literal in c2 + which indexes stand in the vector between the + pointers beg and end (exclusive). + CAUTION: None. +***********************************************************/ +{ + int j,i; + + for (i = vec; i < vec_ActMax(); i++) { + for (j = beg; j < end; j++){ + cont_StartBinding(); + if (unify_Match(cont_LeftContext(), + clause_GetLiteralTerm(c1, (int) vec_GetNth(i)), + clause_GetLiteralTerm(c1, (int) vec_GetNth(j)))) + j = end+1; + cont_BackTrack(); + } + if (j == end) + return FALSE; + } + return TRUE; +} + + +static BOOL subs_IdcVecTestlitsRes(CLAUSE c1, int vec, + int beg, int end, LITPTR* litptr) +/********************************************************** + INPUT: A clause c1, a pointer to a literal structure and + three vector pointer vec, beg and end. + RETURNS: FALSE if the literals of c1 which are designated by + the elements of vec can not be matched independently + to literal in c2 which are designated by the elements + of the vector between the pointers beg and end (exclusive). + CAUTION: A structure is build and litptr points to that structure. +***********************************************************/ +{ + LIST TermIndexlist,VarSymbList,TermSymbList; + int i; + + if (subs_SubsumptionVecPossibleRes(c1,vec,beg,end)) { + + TermIndexlist = list_Nil(); + VarSymbList = list_Nil(); + TermSymbList = list_Nil(); + + for (i = vec; i < vec_ActMax(); i++) { + VarSymbList = + subs_GetVariables(clause_GetLiteralTerm(c1, (int) vec_GetNth(i))); + + if (VarSymbList != list_Nil()) { + TermIndexlist = list_Cons(vec_GetNth(i), TermIndexlist); + TermSymbList = list_Cons(VarSymbList,TermSymbList); + } + } + + *litptr = litptr_Create(TermIndexlist,TermSymbList); + + list_Delete(TermSymbList); + list_Delete(TermIndexlist); + + return TRUE; + } + return FALSE; +} + + +static int subs_SearchTopRes(CLAUSE c1, int vec, int beg, int end) +/********************************************************** + INPUT: A clause c1, three vector pointers vec, beg and end. + RETURNS: The index of that literal in c1 which has the least positive + matching tests with the literals in c2 with respect to + vector and the vector pointers beg and end. + CAUTION: None. +***********************************************************/ +{ + int index,i,j,zaehler; + + index = (int) vec_GetNth(vec); + + for (i = vec; i < vec_ActMax(); i++) { + zaehler = 0; + j = beg; + while ((j < end) && (zaehler < 2)) { + cont_StartBinding(); + if (unify_Match(cont_LeftContext(), + clause_GetLiteralTerm(c1, (int) vec_GetNth(i)), + clause_GetLiteralTerm(c1, (int) vec_GetNth(j)))) { + zaehler++; + } + cont_BackTrack(); + j++; + } + + if (zaehler == 0 || zaehler == 1) { + index = (int)vec_GetNth(i); + return index; + } + } + return index; +} + + +static BOOL subs_TcVecRes(CLAUSE c1, int vec, int beg, int end) +/********************************************************** + INPUT: A clause c1, three vector pointers vec,beg and end. + RETURNS: FALSE if the literals of c1 which are designated by + the elements of vec do not subsume c2 with + respect to the vector and the vector pointers + beg and end and TRUE otherwise. + CAUTION: None. +***********************************************************/ +{ + int a,top_index; + + a = beg; + + top_index = subs_SearchTopRes(c1,vec,beg,end); + + do { + cont_StartBinding(); + while ((a < end) && + !unify_Match(cont_LeftContext(), + clause_GetLiteralTerm(c1,top_index), + clause_GetLiteralTerm(c1,(int)vec_GetNth(a)))) { + a++; + cont_BackTrackAndStart(); + } + + if (a >= end){ + cont_BackTrack(); + return FALSE; + } + + if ((vec - vec_ActMax()) == 1) + return TRUE; + + if (subs_InternIdcRes(c1, vec, beg, end)) + return TRUE; + else { + cont_BackTrack(); + a++; + } + + } while (a < end); + + return FALSE; +} + + +static BOOL subs_InternIdcRes(CLAUSE c1, int vec, int beg, int end) +/********************************************************** + INPUT: A clause c1 and three vector pointers vec,beg and end. + RETURNS: FALSE if the literals of c1 which are designated by + the elements of vec do not subsume c2 with respect + to vector and the vector pointers beg and end + and TRUE otherwise. + CAUTION: None. +***********************************************************/ +{ + int locvec; + LITPTR litptr; + + + if (!subs_IdcVecTestlitsRes(c1,vec,beg,end,&litptr)) + return FALSE; + + locvec = vec_ActMax(); + + do { + subs_CompVec(litptr); + if (!vec_IsMax(locvec)) { + if (!subs_TcVecRes(c1,locvec,beg,end)) { + vec_SetMax(locvec); + litptr_Delete(litptr); + return FALSE; + } + else + vec_SetMax(locvec); + } + } while (!litptr_AllUsed(litptr)); + + litptr_Delete(litptr); + + return TRUE; +} + + +BOOL subs_IdcRes(CLAUSE c1, int beg, int end) +/********************************************************** + INPUT: A clause c1 and two vector pointers beg and end. + RETURNS: FALSE if c1 do not subsume c2 with respect to + vector and the vector pointers beg and end + and TRUE otherwise. + CAUTION: +***********************************************************/ +{ + int i,vec; + BOOL Result; + + vec = vec_ActMax(); + + for (i = 0; i < clause_Length(c1); i++) + vec_Push((POINTER) i); + + Result = subs_InternIdcRes(c1, vec, beg, end); + + vec_SetMax(vec); + + cont_Reset(); + + return Result; +} + + +static BOOL subs_TcVecEqExcept(CLAUSE c1, int vec, CLAUSE c2, int i2) +/********************************************************** + INPUT: Two clauses c1, c2, a vector pointer vec. + RETURNS: FALSE if the literals of c1 which are designated by + the elements of vec do not subsume c2 and TRUE otherwise. + CAUTION: None. +***********************************************************/ +{ + int a,top_index; + BOOL search; + TERM lit1,lit2; + + a = 0; + top_index = subs_SearchTop(c1,vec,c2); + lit1 = clause_GetLiteralTerm(c1,top_index); + + do { + search = TRUE; + + while (a < clause_Length(c2) && search) { + if (a != i2) { + lit2 = clause_GetLiteralTerm(c2,a); + cont_StartBinding(); + if (unify_Match(cont_LeftContext(),lit1,lit2)) + search = FALSE; + else { + if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) && + fol_IsEquality(fol_Atom(lit1)) && + fol_IsEquality(fol_Atom(lit2)) && + (clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c1,top_index)) || + clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,a)))) { + cont_BackTrackAndStart(); + if (unify_Match(cont_LeftContext(), + term_FirstArgument(fol_Atom(lit1)), + term_SecondArgument(fol_Atom(lit2))) && + unify_Match(cont_LeftContext(), + term_SecondArgument(fol_Atom(lit1)), + term_FirstArgument(fol_Atom(lit2)))) + search = FALSE; + } + if (search) { + a++; + cont_BackTrack(); + } + } + } + else + a++; + } + + if (a>=clause_Length(c2)) { + cont_BackTrack(); + return FALSE; + } + + if ((vec_ActMax() - vec) == 1) + return TRUE; + + if (subs_InternIdcEqExcept(c1, vec, c2, i2)) + return TRUE; + else { + cont_BackTrack(); + a++; + } + + } while (a < clause_Length(c2)); + + return FALSE; +} + + +static BOOL subs_SubsumptionVecPossibleEqExcept(CLAUSE c1, int vec, + CLAUSE c2, int i2) +/********************************************************** + INPUT: Two clauses c1 and c2 and a vector pointer + and an accept literal index for c2. + RETURNS: TRUE if all literals in c1 which indexes stand + in the vector with bottom pointer vec can + independently be matched to a literal in c2. + CAUTION: None. +***********************************************************/ +{ + int i,j,n; + TERM lit1,lit2; + + n = clause_Length(c2); + for (i = vec; i < vec_ActMax(); i++) { + lit1 = clause_GetLiteralTerm(c1, (int) vec_GetNth(i)); + for (j = 0; j < n; j++) { + if (j != i2) { + lit2 = clause_GetLiteralTerm(c2,j); + cont_StartBinding(); + if (unify_Match(cont_LeftContext(),lit1,lit2)) + j = n + 1; + else { + if (symbol_Equal(term_TopSymbol(lit1),term_TopSymbol(lit2)) && + fol_IsEquality(fol_Atom(lit1)) && + fol_IsEquality(fol_Atom(lit2)) && + (clause_LiteralIsNotOrientedEquality( + clause_GetLiteral(c1,(int)vec_GetNth(i))) || + clause_LiteralIsNotOrientedEquality(clause_GetLiteral(c2,j)))) { + cont_BackTrackAndStart(); + if (unify_Match(cont_LeftContext(), + term_FirstArgument(fol_Atom(lit1)), + term_SecondArgument(fol_Atom(lit2))) && + unify_Match(cont_LeftContext(), + term_SecondArgument(fol_Atom(lit1)), + term_FirstArgument(fol_Atom(lit2)))) + j = n+1; + } + } + cont_BackTrack(); + } + } + if (j==n) + return FALSE; + } + + return TRUE; +} + + +static BOOL subs_IdcVecTestlitsEqExcept(CLAUSE c1, int vec, + CLAUSE c2, int i2, LITPTR* litptr) +/********************************************************** + INPUT: Two clauses c1, c2, a pointer to a literal structure and + a vector pointer and a literal index i2 in c2 + RETURNS: FALSE if the literals of c1 which are designated by + the elements of vec do not subsume c2 and TRUE otherwise. + CAUTION: A structure is build and litptr points to that structure. + ***********************************************************/ +{ + LIST TermIndexlist,VarSymbList,TermSymbList; + int i; + + if (subs_SubsumptionVecPossibleEqExcept(c1,vec,c2,i2)) { + + TermIndexlist = list_Nil(); + VarSymbList = list_Nil(); + TermSymbList = list_Nil(); + + for (i = vec; i < vec_ActMax(); i++) { + VarSymbList = + subs_GetVariables(clause_GetLiteralTerm(c1, (int) vec_GetNth(i))); + + if (VarSymbList != list_Nil()){ + TermIndexlist = list_Cons(vec_GetNth(i), TermIndexlist); + TermSymbList = list_Cons(VarSymbList,TermSymbList); + } + } + + *litptr = litptr_Create(TermIndexlist,TermSymbList); + + list_Delete(TermSymbList); + list_Delete(TermIndexlist); + + return TRUE; + } + return FALSE; +} + + +static BOOL subs_InternIdcEqExcept(CLAUSE c1, int vec, CLAUSE c2, int i2) +/********************************************************** + INPUT: Two clauses c1, c2, a vector pointer vec and a literal + i2 in c2 which must not be considered + RETURNS: FALSE if the literals of c1 which are designed by + the elements of vec do not subsume c2/i2 and TRUE otherwise. + CAUTION: +***********************************************************/ +{ + int locvec; + LITPTR litptr; + + + if (!subs_IdcVecTestlitsEqExcept(c1,vec,c2,i2,&litptr)) + return FALSE; + + locvec = vec_ActMax(); + + do { + subs_CompVec(litptr); + if (!vec_IsMax(locvec)) { + if (!subs_TcVecEqExcept(c1,locvec,c2,i2)) { + vec_SetMax(locvec); + litptr_Delete(litptr); + return FALSE; + } + else + vec_SetMax(locvec); + } + } while (!litptr_AllUsed(litptr)); + + litptr_Delete(litptr); + + return TRUE; +} + + +BOOL subs_IdcEqMatchExcept(CLAUSE c1, int i1, CLAUSE c2, int i2, + SUBST subst) +/********************************************************** + INPUT: Two clauses c1, c2 with the indices of two literals + which need not to be considered and a matcher + RETURNS: TRUE if (/) subsumes (/) + CAUTION: +***********************************************************/ +{ + int i,vec; + BOOL Result; + + /*fputs("\n IdcEQExcept on: \n\t", stdout); + subst_Print(subst); fputs("\n\t", stdout); + clause_Print(c1); printf(" \t\t%d \n\t",i1); + clause_Print(c2); printf(" \t\t%d \n\t",i2);*/ + + if (clause_Length(c1) == 1) + Result = TRUE; + else { + vec = vec_ActMax(); + + for (i = 0; i < clause_Length(c1); i++) + if (i != i1) + vec_Push((POINTER) i); + + i = 0; /* Doesn't matter, there is a general cont_Reset below */ + unify_EstablishMatcher(cont_LeftContext(), subst); + + Result = subs_InternIdcEqExcept(c1,vec,c2,i2); + + /* printf("Result : %d",Result); */ + + vec_SetMax(vec); + + cont_Reset(); + } + + return Result; +} -- cgit