diff options
Diffstat (limited to 'test/spass/sort.c')
| -rw-r--r-- | test/spass/sort.c | 1974 |
1 files changed, 1974 insertions, 0 deletions
diff --git a/test/spass/sort.c b/test/spass/sort.c new file mode 100644 index 0000000..e109ef1 --- /dev/null +++ b/test/spass/sort.c @@ -0,0 +1,1974 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * SORTED REASONING * */ +/* * * */ +/* * $Module: SORT * */ +/* * * */ +/* * 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 "sort.h" + +/**************************************************************/ +/* Global Variables */ +/**************************************************************/ + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * HIGH LEVEL FUNCTIONS * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + +void sort_Delete(SORT Sort) +/************************************************************** + INPUT: A sort. + RETURNS: Nothing. + MEMORY: The memory of the sort is freed. +***************************************************************/ +{ + list_Delete(Sort); +} + +BOOL sort_Eq(SORT S1, SORT S2) +/************************************************************** + INPUT: Two sorts. + RETURNS: TRUE iff the sorts <S1> and <S2> are the same base + sort intersection +***************************************************************/ +{ + LIST Scan1,Scan2; + BOOL Found; + +#ifdef CHECK + if (!sort_IsSort(S1) || !sort_IsSort(S2)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sort_Eq :"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + if (list_Length(S1) != list_Length(S2)) + return FALSE; + + for (Scan1=S1; !list_Empty(Scan1); Scan1=list_Cdr(Scan1)) { + Found = FALSE; + for (Scan2=S2; !list_Empty(Scan2) && !Found; Scan2=list_Cdr(Scan2)) + Found = sort_NodeEqual(list_Car(Scan1),list_Car(Scan2)); + if (!Found) + return FALSE; + } + + return TRUE; +} + + +LIST sort_GetSymbolsFromSort(SORT Sort) +/************************************************************** + INPUT: A sort. + RETURNS: The list of sort symbols.. +***************************************************************/ +{ + LIST result = list_Nil(); + + for ( ; !list_Empty(Sort); Sort = list_Cdr(Sort)) + result = list_Cons((POINTER)sort_NodeSymbol(list_Car(Sort)), result); + + return result; +} + +BOOL sort_ContainsSymbol(SORT Sort, SYMBOL Symbol) +/************************************************************** + INPUT: A sort and a symbol. + RETURNS: TRUE, if the sort contains the symbol, FALSE otherwise. +***************************************************************/ +{ + for ( ; !list_Empty(Sort); Sort = list_Cdr(Sort)) + if (symbol_Equal(sort_NodeSymbol(list_Car(Sort)), Symbol)) + return TRUE; + + return FALSE; +} + +BOOL sort_IsSort(SORT Sort) +/************************************************************** + INPUT: A sort. + RETURNS: TRUE, if the sort contains not more than one node. +***************************************************************/ +{ + LIST Scan1,Scan2; + + for (Scan1=Sort ; !list_Empty(Scan1); Scan1 = list_Cdr(Scan1)) + for (Scan2=list_Cdr(Scan1) ; !list_Empty(Scan2); Scan2 = list_Cdr(Scan2)) + if (sort_NodeEqual(list_Car(Scan1),list_Car(Scan2))) + return FALSE; + + return TRUE; +} + +BOOL sort_TheorySortEqual(SORTTHEORY Theory, SORT Sort1, SORT Sort2) +/************************************************************** + INPUT: + RETURNS: +***************************************************************/ +{ + LIST Scan; + + if (list_Length(Sort1) != list_Length(Sort2)) + return FALSE; + + sort_TheoryIncrementMark(Theory); + + for (Scan=Sort1; !list_Empty(Scan); Scan=list_Cdr(Scan)) + sort_PutNodeExtraTrue(Theory,list_Car(Scan)); + for (Scan=Sort2; !list_Empty(Scan); Scan=list_Cdr(Scan)) + if (!sort_NodeExtraValue(Theory,list_Car(Scan))) + return FALSE; + + return TRUE; +} + +static BOOL sort_TheorySortMember(SORTTHEORY Theory, LIST List, SORT Sort) +/************************************************************** + INPUT: + RETURNS: +***************************************************************/ +{ + while (!list_Empty(List)) { + if (sort_TheorySortEqual(Theory,list_Car(List),Sort)) + return TRUE; + List = list_Cdr(List); + } + return FALSE; +} + + +void sort_DeleteSortPair(SOJU Pair) +/************************************************************** + INPUT: + RETURNS: Nothing. +***************************************************************/ +{ + sort_DeleteOne(sort_PairSort(Pair)); + sort_ConditionDelete(sort_PairCondition(Pair)); + list_PairFree(Pair); +} + + + +static void sort_ConditionPrint(CONDITION Cond) +/************************************************************** + INPUT: + RETURNS: Nothing. +***************************************************************/ +{ + LIST Scan; + + symbol_Print(sort_ConditionVar(Cond)); + for (Scan=sort_ConditionConstraint(Cond);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + putchar(','); + term_PrintPrefix(list_Car(Scan)); + } + for (Scan=sort_ConditionAntecedent(Cond);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + putchar(','); + term_PrintPrefix(list_Car(Scan)); + } + for (Scan=sort_ConditionSuccedent(Cond);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + putchar(','); + term_PrintPrefix(list_Car(Scan)); + } + for (Scan=sort_ConditionClauses(Cond);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + printf(",%d",clause_Number(list_Car(Scan))); + } +} + +static void sort_LinkPrint(SLINK Link) +/************************************************************** + INPUT: + RETURNS: Nothing. +***************************************************************/ +{ + LIST Scan; + + fputs("Input: (", stdout); + for (Scan=sort_LinkInput(Link);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + symbol_Print(sort_NodeSymbol(list_Car(Scan))); + if (!list_Empty(list_Cdr(Scan))) + putchar(','); + } + fputs(") Output: ", stdout); + symbol_Print(sort_NodeSymbol(sort_LinkOutput(Link))); + fputs(" C: (", stdout); + for (Scan=sort_LinkConstraint(Link);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + term_PrintPrefix(list_Car(Scan)); + if (!list_Empty(list_Cdr(Scan))) + putchar(','); + } + fputs(") A: (", stdout); + for (Scan=sort_LinkAntecedent(Link);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + term_PrintPrefix(list_Car(Scan)); + if (!list_Empty(list_Cdr(Scan))) + putchar(','); + } + fputs(") S: (", stdout); + for (Scan=sort_LinkSuccedent(Link);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + term_PrintPrefix(list_Car(Scan)); + if (!list_Empty(list_Cdr(Scan))) + putchar(','); + } + printf(") Clause: %d Card: %d Fire: %d Var: ", clause_Number(sort_LinkClause(Link)), sort_LinkCard(Link), + sort_LinkFire(Link)); + symbol_Print(sort_LinkVar(Link)); +} + + + +void sort_PairPrint(SOJU Pair) +/************************************************************** + INPUT: + RETURNS: Nothing. +***************************************************************/ +{ + sort_Print(sort_PairSort(Pair)); + fputs(":[", stdout); + sort_ConditionPrint(sort_PairCondition(Pair)); + putchar(']'); +} + + +static NODE sort_NodeCreate(SYMBOL S) +/************************************************************** + INPUT: A sort symbol. + RETURNS: A new initialized sort node for the symbol <S>. +***************************************************************/ +{ + NODE Result; + + Result = (NODE)memory_Malloc(sizeof(NODE_NODE)); + + sort_PutNodeLinks(Result, list_Nil()); + sort_PutNodeConditions(Result, list_Nil()); + sort_PutNodeMark(Result, 0); + sort_PutNodeStart(Result, 0); + sort_PutNodeExtra(Result, 0); + sort_PutNodeSymbol(Result, S); + + return Result; +} + +BOOL sort_NodeIsTop(SORTTHEORY Theory, NODE Node) +/************************************************************** + INPUT: A sort theory and a node. + RETURNS: TRUE if the Node is declared to be equivalent to the + top sort. +***************************************************************/ +{ + LIST Scan; + SLINK Link; + + for (Scan=sort_TheorySuborigcls(Theory);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Link = (SLINK)list_Third(list_Car(Scan)); + if (list_Empty(sort_LinkInput(Link)) && Node == sort_LinkOutput(Link)) + return TRUE; + } + return FALSE; +} + + +static SLINK sort_TheoryLinkCreate(SORTTHEORY Theory, CLAUSE Origin, + CLAUSE Clause, LITERAL Lit) +/************************************************************** + INPUT: A sort theory, a clause its origin and a subsort declaration + literal in the clause + RETURNS: A new link in <Theory> origin <Clause> and subsort declaration <Lit> +***************************************************************/ +{ + SLINK Result; + SYMBOL Output,Var,Max; + int i; + LIST Input, Antecedent, Succedent, Constraint; + TERM Term; + + Result = (SLINK)memory_Malloc(sizeof(SLINK_NODE)); + + Output = term_TopSymbol(clause_LiteralSignedAtom(Lit)); + Var = term_TopSymbol(term_FirstArgument(clause_LiteralSignedAtom(Lit))); + Input = Antecedent = Succedent = Constraint = list_Nil(); + Max = clause_MaxVar(Clause); + term_StartMaxRenaming(Max); + Max = symbol_CreateStandardVariable(); + + for (i = clause_FirstConstraintLitIndex(Clause); + i <= clause_LastConstraintLitIndex(Clause); i++) + if (symbol_Equal(Var,term_TopSymbol(term_FirstArgument(clause_GetLiteralAtom(Clause,i))))) + Input = list_Cons(sort_TheoryNode(Theory,term_TopSymbol(clause_GetLiteralAtom(Clause,i))), + Input); + else { + Term = term_Copy(clause_GetLiteralTerm(Clause,i)); + term_ExchangeVariable(Term,Var,Max); + Constraint = list_Cons(Term,Constraint); + } + + for (i = clause_FirstAntecedentLitIndex(Clause); + i <= clause_LastAntecedentLitIndex(Clause); i++) { + Term = term_Copy(clause_GetLiteralTerm(Clause,i)); + term_ExchangeVariable(Term,Var,Max); + Antecedent = list_Cons(Term,Antecedent); + } + + for (i = clause_FirstSuccedentLitIndex(Clause); + i <= clause_LastSuccedentLitIndex(Clause); i++) + if (clause_GetLiteral(Clause,i) != Lit) { + Term = term_Copy(clause_GetLiteralTerm(Clause,i)); + term_ExchangeVariable(Term,Var,Max); + Succedent = list_Cons(Term,Succedent); + } + + + sort_PutLinkInput(Result,Input); + sort_PutLinkOutput(Result,sort_TheoryNode(Theory,Output)); + sort_PutLinkVar(Result,Max); + sort_PutLinkConstraint(Result,Constraint); + sort_PutLinkAntecedent(Result,Antecedent); + sort_PutLinkSuccedent(Result,Succedent); + sort_PutLinkCard(Result,list_Length(Input)); + sort_LinkResetFire(Result); + sort_PutLinkClause(Result,Origin); + + while (!list_Empty(Input)) { + sort_PutNodeLinks(list_Car(Input),list_Cons(Result,sort_NodeLinks(list_Car(Input)))); + Input = list_Cdr(Input); + } + + return Result; +} + + +void sort_Init(void) +/************************************************************** + INPUT: None. + RETURNS: None. + SUMMARY: Initializes the sort Module. + EFFECTS: Initializes global variables, i.e. the BASESORT-Array. + CAUTION: MUST BE CALLED BEFORE ANY OTHER sort-FUNCTION. +***************************************************************/ +{ + return; +} + + +void sort_Print(SORT Sort) +/************************************************************** + INPUT: + RETURNS: Nothing. +***************************************************************/ +{ + putchar('('); + + while (!list_Empty(Sort)) { + symbol_Print(sort_NodeSymbol(list_Car(Sort))); + Sort = list_Cdr(Sort); + if (!list_Empty(Sort)) + putchar(','); + } + putchar(')'); +} + + +void sort_Free(void) +/************************************************************** + INPUT: None. + RETURNS: Nothing. + SUMMARY: Frees the sort Module. +***************************************************************/ +{ + return; +} + +SORTTHEORY sort_TheoryCreate(void) +/************************************************************** + INPUT: None. + RETURNS: A new sort theory. + EFFECT: A new sort theory is created and initialized. +***************************************************************/ +{ + SORTTHEORY Result; + int i; + SIGNATURE Entry; + SYMBOL Symbol; + + Result = (SORTTHEORY)memory_Malloc(sizeof(SORTTHEORY_NODE)); + + for (i = 1; i < symbol_ACTINDEX; i++) { + Result->basesorttable[i] = (NODE)NULL; + Entry = symbol_Signature(i); + if (Entry != NULL) { + Symbol = Entry->info; + if (symbol_IsPredicate(Symbol) && Entry->arity == 1) + Result->basesorttable[i] = sort_NodeCreate(Symbol); + } + } + + Result->index = st_IndexCreate(); + Result->suborigcls = list_Nil(); + Result->termorigcls = list_Nil(); + Result->mark = 0; + + return Result; +} + +void sort_TheoryPrint(SORTTHEORY Theory) +/************************************************************** + INPUT: A sort theory + RETURNS: None. + EFFECT: Prints the sort theory to stdout. +***************************************************************/ +{ + LIST Scan; + + if (Theory == (SORTTHEORY)NULL) { + fputs(" Empty Theory", stdout); + return; + } + + fputs("\n Subsort Clauses:", stdout); + for (Scan=sort_TheorySuborigcls(Theory);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + fputs("\n\t\t Clause:", stdout); + clause_Print(list_Second(list_Car(Scan))); + fputs("\n\t\t Link: ", stdout); + sort_LinkPrint(list_Third(list_Car(Scan))); + } + fputs("\n Term Declaration Clauses:", stdout); + for (Scan=sort_TheoryTermorigcls(Theory);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + fputs("\n\t\t Clause:", stdout); + clause_Print(list_Second(list_Car(Scan))); + } + +} + +void sort_TheoryDelete(SORTTHEORY Theory) +/************************************************************** + INPUT: A sort theory + RETURNS: None. + EFFECT: The complete sort theory is deleted. +***************************************************************/ +{ + if (Theory != (SORTTHEORY)NULL) { + int i; + LIST Scan,Tuple; + TERM Term, Atom; + + for (Scan=Theory->suborigcls;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Tuple = (LIST)list_Car(Scan); + sort_LinkDelete(list_Third(Tuple)); + clause_Delete(list_Second(Tuple)); + list_Delete(Tuple); + } + list_Delete(Theory->suborigcls); + for (Scan=Theory->termorigcls;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Tuple = (LIST)list_Car(Scan); + Term = (TERM)list_Third(Tuple); + Atom = (TERM)list_Car(term_SupertermList(Term)); + st_EntryDelete(Theory->index,Term,Term,cont_LeftContext()); + st_EntryDelete(Theory->index,Atom,Atom,cont_LeftContext()); + list_Delete(term_SupertermList(Atom)); + list_Delete(term_SupertermList(Term)); + term_RplacSupertermList(Term, list_Nil()); + term_RplacSupertermList(Atom, list_Nil()); + clause_Delete(list_Second(Tuple)); + list_Delete(Tuple); + } + list_Delete(Theory->termorigcls); + st_IndexDelete(Theory->index); + + for (i=1;i<symbol_ACTINDEX;i++) + if (Theory->basesorttable[i] != (NODE)NULL) + sort_NodeDelete(Theory->basesorttable[i]); + + memory_Free(Theory,sizeof(SORTTHEORY_NODE)); + } +} + +void sort_TheoryInsertClause(SORTTHEORY Theory, CLAUSE Origin, CLAUSE Clause, LITERAL L) +/************************************************************** + INPUT: A sort theory, two clauses and a declaration of the second clause. + <Origin> is the original clause and <Clause> is a possibly approximated + copy of <Origin>. + RETURNS: None. + EFFECT: Inserts <Clause> with declaration <L> into the sort theory. +***************************************************************/ +{ + TERM Term, Atom; + + Term = term_FirstArgument(clause_LiteralSignedAtom(L)); + + if (term_IsVariable(Term)) { + SLINK Link; + Link = sort_TheoryLinkCreate(Theory,Origin,Clause,L); + Theory->suborigcls = list_Cons(list_Cons(Origin,list_Cons(clause_Copy(Clause),list_List(Link))), + Theory->suborigcls); + } + + /* Since currently Sort Resolution and Empty Sort require the subsort declaration clauses */ + /* also subsort clauses are introduced into the sort theory index */ + + Atom = clause_LiteralSignedAtom(L); + term_RplacSupertermList(Atom, list_List(L)); + term_RplacSupertermList(Term, list_List(Atom)); /* Must be empty before this operation */ + st_EntryCreate(Theory->index,Term,Term,cont_LeftContext()); + st_EntryCreate(Theory->index,Atom,Atom,cont_LeftContext()); + Theory->termorigcls = list_Cons(list_Cons(Origin,list_Cons(Clause,list_List(Term))), + Theory->termorigcls); +} + +void sort_TheoryDeleteClause(SORTTHEORY Theory, CLAUSE Origin) +/************************************************************** + INPUT: A sort theory and a clause possibly inserted several times in the theory. + RETURNS: None. + EFFECT: <Origin> is deleted from the sort theory, but not deleted itself. +***************************************************************/ +{ + TERM Term,Atom; + LIST Scan,Tuple; + + for (Scan=Theory->suborigcls;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Tuple = list_Car(Scan); + if ((CLAUSE)list_First(Tuple) == Origin) { + list_Rplaca(Scan,NULL); + sort_LinkDelete(list_Third(Tuple)); + clause_Delete(list_Second(Tuple)); + list_Delete(Tuple); + } + } + Theory->suborigcls = list_PointerDeleteElement(Theory->suborigcls,NULL); + for (Scan=Theory->termorigcls;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Tuple = list_Car(Scan); + if ((CLAUSE)list_First(Tuple) == Origin) { + list_Rplaca(Scan,NULL); + Term = (TERM)list_Third(Tuple); + Atom = (TERM)list_Car(term_SupertermList(Term)); + st_EntryDelete(Theory->index,Term,Term,cont_LeftContext()); + st_EntryDelete(Theory->index,Atom,Atom,cont_LeftContext()); + list_Delete(term_SupertermList(Atom)); + list_Delete(term_SupertermList(Term)); + term_RplacSupertermList(Term, list_Nil()); + term_RplacSupertermList(Atom, list_Nil()); + clause_Delete(list_Second(Tuple)); + list_Delete(Tuple); + } + } + Theory->termorigcls = list_PointerDeleteElement(Theory->termorigcls,NULL); +} + +CONDITION sort_ConditionCreate(SYMBOL Var, LIST Constr, LIST Ante, LIST Succ, LIST Clauses) +/************************************************************** + INPUT: A variable, a list of constraint literals, antecedent literals, succedent literals + and a list of clauses. + RETURNS: The condition created from these arguments. + MEMORY: It is assumed that all literals are unshared whereas the clauses are shared. +***************************************************************/ +{ + CONDITION Result; + + Result = (CONDITION)memory_Malloc(sizeof(CONDITION_NODE)); + + sort_ConditionPutVar(Result, Var); + sort_ConditionPutConstraint(Result, Constr); + sort_ConditionPutAntecedent(Result, Ante); + sort_ConditionPutSuccedent(Result, Succ); + sort_ConditionPutClauses(Result, Clauses); + + return Result; +} + +CONDITION sort_ConditionNormalize(CONDITION Cond) +/************************************************************** + INPUT: A condition. + RETURNS: The normalized condition, i.e., the variables for the various + literals are normalized starting with the minimal variable. + EFFECT: Destructive. +***************************************************************/ +{ + LIST Scan; + SYMBOL Old,New; + + term_StartMinRenaming(); + for (Scan=sort_ConditionConstraint(Cond);!list_Empty(Scan);Scan=list_Cdr(Scan)) + term_Rename(list_Car(Scan)); + for (Scan=sort_ConditionAntecedent(Cond);!list_Empty(Scan);Scan=list_Cdr(Scan)) + term_Rename(list_Car(Scan)); + for (Scan=sort_ConditionSuccedent(Cond);!list_Empty(Scan);Scan=list_Cdr(Scan)) + term_Rename(list_Car(Scan)); + New = symbol_CreateStandardVariable(); + Old = term_GetRenamedVarSymbol(sort_ConditionVar(Cond)); + for (Scan=sort_ConditionConstraint(Cond);!list_Empty(Scan);Scan=list_Cdr(Scan)) + term_ExchangeVariable(list_Car(Scan),Old,New); + for (Scan=sort_ConditionAntecedent(Cond);!list_Empty(Scan);Scan=list_Cdr(Scan)) + term_ExchangeVariable(list_Car(Scan),Old,New); + for (Scan=sort_ConditionSuccedent(Cond);!list_Empty(Scan);Scan=list_Cdr(Scan)) + term_ExchangeVariable(list_Car(Scan),Old,New); + + sort_ConditionPutVar(Cond,New); + + return Cond; +} + +CONDITION sort_ConditionCreateNoResidues(LIST Clauses) +/************************************************************** + INPUT: A list of clauses. + RETURNS: The condition created just from the clauses. +***************************************************************/ +{ + CONDITION Result; + + Result = (CONDITION)memory_Malloc(sizeof(CONDITION_NODE)); + + sort_ConditionPutVar(Result, symbol_FirstVariable()); + sort_ConditionPutConstraint(Result, list_Nil()); + sort_ConditionPutAntecedent(Result, list_Nil()); + sort_ConditionPutSuccedent(Result, list_Nil()); + sort_ConditionPutClauses(Result, Clauses); + + return Result; +} + +CONDITION sort_ExtendConditionByLink(CONDITION Cond, SLINK Link) +/************************************************************** + INPUT: A condition and a link. + RETURNS: <Cond> extended by the clause, antecedent, constraint and succedent + literals of <Link> + EFFECT: <Cond> is destructively extended with <Link>. +***************************************************************/ +{ + LIST Lits,Antecedent,Succedent,Constraint; + SYMBOL Old,New; + + + term_StartMaxRenaming(sort_ConditionVar(Cond)); + Constraint = term_CopyTermList(sort_LinkConstraint(Link)); + Antecedent = term_CopyTermList(sort_LinkAntecedent(Link)); + Succedent = term_CopyTermList(sort_LinkSuccedent(Link)); + for (Lits=Constraint;!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + for (Lits=Antecedent;!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + for (Lits=Succedent;!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + Old = term_GetRenamedVarSymbol(sort_LinkVar(Link)); + New = symbol_CreateStandardVariable(); + for (Lits=Constraint;!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=Antecedent;!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=Succedent;!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + Old = sort_ConditionVar(Cond); + for (Lits=sort_ConditionConstraint(Cond);!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=sort_ConditionAntecedent(Cond);!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=sort_ConditionSuccedent(Cond);!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + sort_ConditionPutConstraint(Cond,list_Nconc(sort_ConditionConstraint(Cond),Constraint)); + sort_ConditionPutAntecedent(Cond,list_Nconc(sort_ConditionAntecedent(Cond),Antecedent)); + sort_ConditionPutSuccedent(Cond,list_Nconc(sort_ConditionSuccedent(Cond),Succedent)); + sort_ConditionPutClauses(Cond,list_Cons(sort_LinkClause(Link),sort_ConditionClauses(Cond))); + sort_ConditionPutVar(Cond,New); + sort_ConditionNormalize(Cond); + + return Cond; + +} + +CONDITION sort_ExtendConditionByCondition(CONDITION Cond, CONDITION Update) +/************************************************************** + INPUT: Two conditions. + RETURNS: <Cond> extended by the clauses, antecedent, constraint and succedent + literals of <Update> + EFFECT: <Cond> is destructively extended by <Update>. +***************************************************************/ +{ + LIST Lits,Antecedent,Succedent,Constraint; + SYMBOL Old,New; + + term_StartMaxRenaming(sort_ConditionVar(Cond)); + Constraint = term_CopyTermList(sort_ConditionConstraint(Update)); + Antecedent = term_CopyTermList(sort_ConditionAntecedent(Update)); + Succedent = term_CopyTermList(sort_ConditionSuccedent(Update)); + for (Lits=Constraint;!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + for (Lits=Antecedent;!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + for (Lits=Succedent;!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + Old = term_GetRenamedVarSymbol(sort_ConditionVar(Update)); + New = symbol_CreateStandardVariable(); + for (Lits=Constraint; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=Antecedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=Succedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + Old = sort_ConditionVar(Cond); + for (Lits=sort_ConditionConstraint(Cond);!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=sort_ConditionAntecedent(Cond);!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=sort_ConditionSuccedent(Cond);!list_Empty(Lits);Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + sort_ConditionPutConstraint(Cond,list_Nconc(sort_ConditionConstraint(Cond),Constraint)); + sort_ConditionPutAntecedent(Cond,list_Nconc(sort_ConditionAntecedent(Cond),Antecedent)); + sort_ConditionPutSuccedent(Cond,list_Nconc(sort_ConditionSuccedent(Cond),Succedent)); + sort_ConditionPutClauses(Cond,list_Nconc(list_Copy(sort_ConditionClauses(Update)), + sort_ConditionClauses(Cond))); + sort_ConditionPutVar(Cond,New); + sort_ConditionNormalize(Cond); + + return Cond; +} + +LIST sort_ExtendConditions(LIST Conditions, SLINK Link) +/************************************************************** + INPUT: A list of conditions and a link. + RETURNS: A new list of conditions augmented by the conditions in <Link>. +***************************************************************/ +{ + LIST Result,Scan,Antecedent,Succedent,Constraint; + CONDITION Cond; + + Result = list_Nil(); + + for (Scan=Conditions;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Cond = (CONDITION)list_Car(Scan); + Constraint = term_CopyTermList(sort_ConditionConstraint(Cond)); + Antecedent = term_CopyTermList(sort_ConditionAntecedent(Cond)); + Succedent = term_CopyTermList(sort_ConditionSuccedent(Cond)); + if (sort_LinkNoResidues(Link)) + Result = list_Cons(sort_ConditionCreate(sort_ConditionVar(Cond),Constraint,Antecedent, + Succedent,list_Cons(sort_LinkClause(Link), + list_Copy(sort_ConditionClauses(Cond)))), + Result); + else { + SYMBOL New,Old; + LIST NewAntecedent,NewSuccedent,NewConstraint,Lits; + term_StartMaxRenaming(sort_ConditionVar(Cond)); + NewConstraint = term_CopyTermList(sort_LinkConstraint(Link)); + NewAntecedent = term_CopyTermList(sort_LinkAntecedent(Link)); + NewSuccedent = term_CopyTermList(sort_LinkSuccedent(Link)); + for (Lits=NewConstraint; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + for (Lits=NewAntecedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + for (Lits=NewSuccedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + Old = term_GetRenamedVarSymbol(sort_LinkVar(Link)); + New = symbol_CreateStandardVariable(); + for (Lits=NewConstraint; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=NewAntecedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=NewSuccedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + Old = sort_ConditionVar(Cond); + for (Lits=Constraint; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=Antecedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=Succedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + Result = list_Cons(sort_ConditionNormalize(sort_ConditionCreate(New,list_Nconc(Constraint,NewConstraint), + list_Nconc(Antecedent,NewAntecedent), + list_Nconc(Succedent,NewSuccedent), + list_Cons(sort_LinkClause(Link), + list_Copy(sort_ConditionClauses(Cond))))), + Result); + } + } + return Result; +} + +CONDITION sort_ConditionsUnion(LIST Conditions) +/************************************************************** + INPUT: A list of conditions. + RETURNS: A new condition that is the union of all input conditions. +***************************************************************/ +{ + LIST Scan,Antecedent,Succedent,Constraint; + CONDITION Cond; + SYMBOL Act,New,Old; + LIST NewAntecedent,NewSuccedent,NewConstraint,NewClauses,Lits; + + if (list_Empty(Conditions)) + return sort_ConditionCreate(symbol_FirstVariable(),list_Nil(),list_Nil(),list_Nil(), + list_Nil()); + else { + Cond = (CONDITION)list_Car(Conditions); + Conditions = list_Cdr(Conditions); + Act = sort_ConditionVar(Cond); + NewConstraint = term_CopyTermList(sort_ConditionConstraint(Cond)); + NewAntecedent = term_CopyTermList(sort_ConditionAntecedent(Cond)); + NewSuccedent = term_CopyTermList(sort_ConditionSuccedent(Cond)); + NewClauses = list_Copy(sort_ConditionClauses(Cond)); + } + + for (Scan=Conditions;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Cond = (CONDITION)list_Car(Scan); + if (!sort_ConditionNoResidues(Cond)) { + Constraint = term_CopyTermList(sort_ConditionConstraint(Cond)); + Antecedent = term_CopyTermList(sort_ConditionAntecedent(Cond)); + Succedent = term_CopyTermList(sort_ConditionSuccedent(Cond)); + + term_StartMaxRenaming(Act); + for (Lits=Constraint; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + for (Lits=Antecedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + for (Lits=Succedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_Rename(list_Car(Lits)); + Old = term_GetRenamedVarSymbol(sort_ConditionVar(Cond)); + New = symbol_CreateStandardVariable(); + for (Lits=Constraint; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=Antecedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=Succedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Old,New); + for (Lits=NewConstraint; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Act,New); + for (Lits=NewAntecedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Act,New); + for (Lits=NewSuccedent; !list_Empty(Lits); Lits=list_Cdr(Lits)) + term_ExchangeVariable(list_Car(Lits),Act,New); + Act = New; + NewConstraint = list_Nconc(Constraint,NewConstraint); + NewAntecedent = list_Nconc(Antecedent,NewAntecedent); + NewSuccedent = list_Nconc(Succedent,NewSuccedent); + } + NewClauses = list_Nconc(list_Copy(sort_ConditionClauses(Cond)),NewClauses); + } + + return sort_ConditionNormalize(sort_ConditionCreate(Act,NewConstraint,NewAntecedent,NewSuccedent,NewClauses)); +} + +void sort_ConditionDelete(CONDITION C) +/************************************************************** + INPUT: A condition. + RETURNS: Nothing. + MEMORY: The condition and all literals and lists are deleted. +***************************************************************/ +{ + if (C!= (CONDITION)NULL) { + term_DeleteTermList(sort_ConditionConstraint(C)); + term_DeleteTermList(sort_ConditionAntecedent(C)); + term_DeleteTermList(sort_ConditionSuccedent(C)); + list_Delete(sort_ConditionClauses(C)); + + sort_ConditionFree(C); + } +} + + +CONDITION sort_ConditionCopy(CONDITION C) +/************************************************************** + INPUT: A condition. + RETURNS: A copy of the condition. +***************************************************************/ +{ + return sort_ConditionCreate(sort_ConditionVar(C), + term_CopyTermList(sort_ConditionConstraint(C)), + term_CopyTermList(sort_ConditionAntecedent(C)), + term_CopyTermList(sort_ConditionSuccedent(C)), + list_Copy(sort_ConditionClauses(C))); +} + + + +BOOL sort_IsBaseSortSymbol(SYMBOL Symbol) +/********************************************************* + INPUT: A Symbol. + RETURNS: The boolean value TRUE, if 'Symbol' is a + basesortsymbol, FALSE else. +*******************************************************/ +{ +#ifdef CHECK + if (!symbol_IsSymbol(Symbol)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sort_IsBaseSymbol :"); + misc_ErrorReport(" Illegal input. Input not a symbol.\n"); + misc_FinishErrorReport(); + } +#endif + + return(symbol_IsPredicate(Symbol) && symbol_Arity(Symbol) == 1); +} + + +SORT sort_TheorySortOfSymbol(SORTTHEORY Theory, SYMBOL Symbol) +/********************************************************* + INPUT: A sort theory and a base sort symbol. + RETURNS: The Basesort of 'Symbol'. +*******************************************************/ +{ +#ifdef CHECK + if (!sort_IsBaseSortSymbol(Symbol)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sort_TheorySortOfSymbol :"); + misc_ErrorReport(" Illegal input. Input not a symbol.\n"); + misc_FinishErrorReport(); + } +#endif + + return (list_List(sort_TheoryNode(Theory, Symbol))); +} + + +static void sort_EvalSubsortNoResidues(SORTTHEORY Theory, LIST Nodes) +/********************************************************* + INPUT: A sort theory and a list of nodes from this theory. + RETURNS: None. + EFFECT: Starting from the nodes in <Nodes> the subsort + graph is exploited as long as links fire and + new nodes become true. Only links without residues + are considered. +*******************************************************/ +{ + NODE Node,Head; + LIST Scan,Help,Clauses; + SLINK Link; + + while (!list_Empty(Nodes)) { + Node = (NODE)list_Car(Nodes); + Scan = Nodes; + Nodes = list_Cdr(Nodes); + list_Free(Scan); + + for (Scan = sort_NodeLinks(Node); + !list_Empty(Scan); + Scan = list_Cdr(Scan)) { + Link = (SLINK)list_Car(Scan); + if (sort_LinkNoResidues(Link) && sort_LinkDecrementFire(Link) == 0) { + Head = sort_LinkOutput(Link); + if (!sort_NodeValue(Theory, Head)) { + Clauses = list_List(sort_LinkClause(Link)); + for (Help=sort_LinkInput(Link);!list_Empty(Help);Help=list_Cdr(Help)) + if (!list_Empty(sort_NodeConditions(list_Car(Help)))) + Clauses = + list_Nconc(list_Copy(sort_ConditionClauses( + list_Car(sort_NodeConditions(list_Car(Help))))),Clauses); + sort_DeleteConditionList(sort_NodeConditions(Head)); + sort_PutNodeConditions(Head,list_List(sort_ConditionCreateNoResidues(Clauses))); + sort_PutNodeTrue(Theory, Head); + Nodes = list_Cons(Head,Nodes); + } + } + } + } +} + + +static BOOL sort_TestSubsortSpecial(SORTTHEORY Theory, LIST Nodes, LIST Goal) +/********************************************************* + INPUT: A sort theory and a list of nodes from this theory and + a list of goal nodes. + RETURNS: TRUE if we can walk from at least one node of <Nodes> over + a previously evaluated sort structure. +*******************************************************/ +{ + NODE Node,Head; + LIST Scan; + SLINK Link; + + while (!list_Empty(Nodes)) { + Node = (NODE)list_NCar(&Nodes); + if (list_PointerMember(Goal,Node)) { + list_Delete(Nodes); + return TRUE; + } + for (Scan = sort_NodeLinks(Node);!list_Empty(Scan);Scan = list_Cdr(Scan)) { + Link = (SLINK)list_Car(Scan); + if (sort_LinkFire(Link) == 0) { + Head = sort_LinkOutput(Link); + Nodes = list_Cons(Head,Nodes); + } + } + } + return FALSE; +} + +static void sort_EvalSubsortSpecial(SORTTHEORY Theory, LIST Nodes) +/********************************************************* + INPUT: A sort theory and a list of nodes from this theory. + RETURNS: None. + EFFECT: Starting from the nodes in <Nodes> the subsort + graph is exploited as long as links fire and + new nodes become true. Only links without residues + are considered. +*******************************************************/ +{ + NODE Node,Head; + LIST Scan; + SLINK Link; + + while (!list_Empty(Nodes)) { + Node = (NODE)list_NCar(&Nodes); + for (Scan = sort_NodeLinks(Node);!list_Empty(Scan);Scan = list_Cdr(Scan)) { + Link = (SLINK)list_Car(Scan); + if (sort_LinkDecrementFire(Link) == 0) { + Head = sort_LinkOutput(Link); + if (!sort_NodeValue(Theory, Head)) { + sort_PutNodeTrue(Theory, Head); + Nodes = list_Cons(Head,Nodes); + } + } + } + } +} + +static void sort_EvalSubsort(SORTTHEORY Theory, LIST Nodes) +/********************************************************* + INPUT: A sort theory and a list of nodes from this theory. + RETURNS: None. + EFFECT: Starting from the nodes in <Nodes> the subsort + graph is exploited as long as links fire and + new nodes become true. + Only ONE condition for each node becoming + valid is established. +*******************************************************/ +{ + NODE Node,Head; + LIST Scan,Help; + SLINK Link; + CONDITION Cond; + + while (!list_Empty(Nodes)) { + Node = (NODE)list_Car(Nodes); + Scan = Nodes; + Nodes = list_Cdr(Nodes); + list_Free(Scan); + + for (Scan = sort_NodeLinks(Node); + !list_Empty(Scan); + Scan = list_Cdr(Scan)) { + Link = (SLINK)list_Car(Scan); + if (sort_LinkDecrementFire(Link) == 0) { + Head = sort_LinkOutput(Link); + if (!sort_NodeValue(Theory, Head)) { + Cond = sort_ConditionCreate(symbol_FirstVariable(),list_Nil(),list_Nil(),list_Nil(),list_Nil()); + for (Help=sort_LinkInput(Link);!list_Empty(Help);Help=list_Cdr(Help)) + if (!list_Empty(sort_NodeConditions(list_Car(Help)))) + Cond = sort_ExtendConditionByCondition(Cond,list_Car(sort_NodeConditions(list_Car(Help)))); + sort_ExtendConditionByLink(Cond,Link); + sort_DeleteConditionList(sort_NodeConditions(Head)); + sort_PutNodeConditions(Head,list_List(Cond)); + sort_PutNodeTrue(Theory, Head); + Nodes = list_Cons(Head,Nodes); + } + } + } + } +} + + +CONDITION sort_TheoryIsSubsortOfNoResidues(SORTTHEORY Theory, SORT Sort1, SORT Sort2) +/********************************************************* + INPUT: A sort theory and two sorts. + RETURNS: A condition if <Sort1> is a subsort of <Sort2> and NULL otherwise. +*******************************************************/ +{ + LIST Scan,Clauses; + SLINK Link; + NODE Node; + SORT Top; + +#ifdef CHECK + if (!sort_IsSort(Sort1) || !sort_IsSort(Sort2)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sort_TheoryIsSubsortOfNoResidues :"); + misc_ErrorReport(" Illegal sort input.\n"); + misc_FinishErrorReport(); + } +#endif + + sort_TheoryIncrementMark(Theory); + + /*fputs("\n Subsort Test: ", stdout); + sort_Print(Sort1); + putchar(' '); + sort_Print(Sort2);*/ + + for (Scan=sort_TheorySuborigcls(Theory);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Link = (SLINK)list_Third(list_Car(Scan)); + sort_LinkResetFire(Link); + } + + for (Scan=Sort1;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Node = (NODE)list_Car(Scan); + sort_DeleteConditionList(sort_NodeConditions(Node)); + sort_PutNodeConditions(Node,list_List(sort_ConditionCreate(symbol_FirstVariable(), + list_Nil(),list_Nil(),list_Nil(),list_Nil()))); + sort_PutNodeTrue(Theory, Node); + } + + Top = sort_TopSort(); + for (Scan=sort_TheorySuborigcls(Theory);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Link = (SLINK)list_Third(list_Car(Scan)); + if (list_Empty(sort_LinkInput(Link)) && sort_LinkNoResidues(Link)) { + Node = sort_LinkOutput(Link); + Top = sort_AddBaseNode(Top,Node); + sort_DeleteConditionList(sort_NodeConditions(Node)); + sort_PutNodeConditions(Node,list_List(sort_ConditionCreateNoResidues(list_List(sort_LinkClause(Link))))); + sort_PutNodeTrue(Theory,Node); + } + } + + sort_EvalSubsortNoResidues(Theory,sort_Intersect(Top,sort_Copy(Sort1))); + Top = sort_TopSort(); + + Clauses = list_Nil(); + + for (Scan=Sort2;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Node = (NODE)list_Car(Scan); + if (!sort_NodeValue(Theory,Node)) { + /*puts(" FALSE");*/ + list_Delete(Clauses); + return NULL; + } + else + if (!list_Empty(sort_NodeConditions(Node))) + Clauses = list_Nconc(list_Copy(sort_ConditionClauses(list_Car(sort_NodeConditions(Node)))), + Clauses); + } + /*printf(" TRUE %lu\n",(unsigned long)Clauses);*/ + return sort_ConditionCreateNoResidues(Clauses); +} + +BOOL sort_TheoryIsSubsortOf(SORTTHEORY Theory, SORT Sort1, SORT Sort2) +/********************************************************* + INPUT: A sort theory and two sorts. + RETURNS: TRUE if <Sort1> is a subsort of <Sort2> and NULL otherwise. +*******************************************************/ +{ + LIST Scan; + SLINK Link; + NODE Node; + + sort_TheoryIncrementMark(Theory); + + /*fputs("\n Subsort Test: ", stdout); + sort_Print(Sort1); + putchar(' '); + sort_Print(Sort2);*/ + + for (Scan=sort_TheorySuborigcls(Theory);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Link = (SLINK)list_Third(list_Car(Scan)); + sort_LinkResetFire(Link); + } + + for (Scan=Sort1;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Node = (NODE)list_Car(Scan); + sort_PutNodeTrue(Theory, Node); + } + + sort_EvalSubsortSpecial(Theory,sort_Copy(Sort1)); + + for (Scan=Sort2;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Node = (NODE)list_Car(Scan); + if (!sort_NodeValue(Theory,Node)) + return FALSE; + } + + return TRUE; + +} + +BOOL sort_TheoryIsSubsortOfExtra(SORTTHEORY Theory, SORT Extra, SORT Sort1, SORT Sort2) +/********************************************************* + INPUT: A sort theory and three sorts. + RETURNS: TRUE if <Sort1> is a subsort of <Sort2> and <Extra> is + useful for that purpose +*******************************************************/ +{ + LIST Scan; + SLINK Link; + NODE Node; + + sort_TheoryIncrementMark(Theory); + + /*fputs("\n Subsort Test: ", stdout); + sort_Print(Sort1); + putchar(' '); + sort_Print(Sort2);*/ + + for (Scan=sort_TheorySuborigcls(Theory);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Link = (SLINK)list_Third(list_Car(Scan)); + sort_LinkResetFire(Link); + } + + for (Scan=Sort1;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Node = (NODE)list_Car(Scan); + sort_PutNodeTrue(Theory, Node); + } + + sort_EvalSubsortSpecial(Theory,sort_Copy(Sort1)); + + for (Scan=Sort2;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Node = (NODE)list_Car(Scan); + if (!sort_NodeValue(Theory,Node)) + return FALSE; + } + + return sort_TestSubsortSpecial(Theory,sort_Copy(Extra),Sort2); + +} + +LIST sort_TheoryComputeAllSubsortHits(SORTTHEORY Theory, SORT Sort1, SORT Sort2) +/********************************************************* + INPUT: A sort theory and two sorts. + RETURNS: All possible sorts that are subsets of <Sort1> that are subsorts + of <Sort2> together with all conditions. +*******************************************************/ +{ + LIST Scan,Result,Search,Scan2,Visited; + SLINK Link; + NODE Node; + SOJU Cand; + BOOL Valid,ValidStart; + NAT StartMark; + + sort_TheoryIncrementMark(Theory); + StartMark = sort_TheoryMark(Theory); + + /*fputs("\n Exhaustive Subsort Test: ", stdout); + sort_Print(Sort1); + putchar(' '); + sort_Print(Sort2);*/ + + for (Scan=sort_TheorySuborigcls(Theory);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Link = (SLINK)list_Third(list_Car(Scan)); + sort_LinkResetFire(Link); + } + + for (Scan=Sort1;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Node = (NODE)list_Car(Scan); + sort_DeleteConditionList(sort_NodeConditions(Node)); + sort_PutNodeConditions(Node,list_List(sort_ConditionCreate(symbol_FirstVariable(), + list_Nil(),list_Nil(),list_Nil(),list_Nil()))); + sort_PutNodeTrue(Theory, Node); + sort_PutNodeStartTrue(Theory,Node); + } + + sort_EvalSubsort(Theory,sort_Copy(Sort1)); + + for (Scan=Sort2;!list_Empty(Scan);Scan=list_Cdr(Scan)) {/* Subsort condition must hold */ + Node = (NODE)list_Car(Scan); + if (!sort_NodeValue(Theory,Node)) + return list_Nil(); + } + + Result = list_Nil(); + Search = list_List(sort_PairCreate(sort_Copy(Sort2),sort_ConditionCreateNoResidues(list_Nil()))); + Visited = list_Nil(); + fputs("\n\n Starting Soju Search:", stdout); + + while (!list_Empty(Search)) { + Cand = (SOJU)list_Car(Search); + Scan = Search; + Search = list_Cdr(Search); + list_Free(Scan); + putchar('\n'); + sort_PairPrint(Cand); + + if (!sort_TheorySortMember(Theory,Visited,sort_PairSort(Cand))) { + Visited = list_Cons(sort_Copy(sort_PairSort(Cand)),Visited); + ValidStart = TRUE; + Valid = TRUE; + for (Scan=sort_PairSort(Cand);!list_Empty(Scan) && (ValidStart || Valid);Scan=list_Cdr(Scan)) { + Node = (NODE)list_Car(Scan); + if (sort_NodeMark(Node) != StartMark) { + Valid = FALSE; + ValidStart = FALSE; + } + else + if (sort_NodeStart(Node) != StartMark) + ValidStart = FALSE; + } + if (Valid) { + if (ValidStart) + Result = list_Cons(sort_PairCopy(Cand),Result); + + for (Scan=sort_PairSort(Cand);!list_Empty(Scan);Scan=list_Cdr(Scan)) { + Node = (NODE)list_Car(Scan); + for (Scan2=sort_TheorySuborigcls(Theory);!list_Empty(Scan2);Scan2=list_Cdr(Scan2)) { + Link = (SLINK)list_Third(list_Car(Scan2)); + if (sort_LinkOutput(Link) == Node && !list_Empty(sort_LinkInput(Link))) + Search = list_Cons(sort_PairCreate(list_PointerDeleteDuplicates(sort_Intersect(sort_DeleteBaseNode(sort_Copy(sort_PairSort(Cand)),Node),sort_Copy(sort_LinkInput(Link)))), + sort_ExtendConditionByLink(sort_ConditionCopy(sort_PairCondition(Cand)),Link)), + Search); + } + } + } + sort_PairDelete(Cand); + } + } + list_DeleteWithElement(Visited,(void (*)(POINTER)) sort_Delete); + + return Result; +} + +static SORT sort_VarSort(SORTTHEORY Theory, SYMBOL Var, CLAUSE Clause, int i) +/********************************************************* + INPUT: A variable symbol, a clause and a literal index in the clause. + RETURNS: The sort of <Var> with respect to the sort constraint + literals (possibly in the antecedent) + in <Clause> except literal <i> that is not considered. + MEMORY: Both Sorts are destroyed. +*******************************************************/ +{ + SORT Result; + int j; + TERM Atom; + + Result = sort_TopSort(); + + for (j=clause_FirstConstraintLitIndex(Clause);j<=clause_LastAntecedentLitIndex(Clause);j++) + if (j != i) { + Atom = clause_LiteralAtom(clause_GetLiteral(Clause,j)); + if (symbol_IsBaseSort(term_TopSymbol(Atom)) && + term_TopSymbol(term_FirstArgument(Atom)) == Var) + Result = sort_Intersect(Result,sort_TheorySortOfSymbol(Theory,term_TopSymbol(Atom))); + } + + return Result; +} + + +static BOOL sort_MatchNoResidues(SORTTHEORY Theory, TERM Term1, TERM Term2, CLAUSE Clause, LIST* Clauses) +/********************************************************* + INPUT: A sort theory, two terms, a clause and list of clauses + as an additional return parameter. + RETURNS: TRUE iff there exists a well-sorted matcher from <Term1> to <Term2> + The sorts of variables in <Term1> is determined by the sort constraint in <Clause> + The sorts of subterms of <Term2> are assumed to be already computed and stored. +*******************************************************/ +{ + int l; + SUBST subst,scan; + SORT varsort; + LIST NewClauses; + SOJU Pair; + CONDITION Cond; + + l = clause_Length(Clause); + NewClauses = list_Nil(); + + cont_StartBinding(); + unify_Match(cont_LeftContext(),Term1,Term2); + subst = subst_ExtractMatcher(); + cont_BackTrack(); + + /*putchar('\n'); term_Print(Term1);fputs("->",stdout); + term_Print(Term2);putchar(':');subst_Print(subst); + putchar('\n');*/ + for (scan=subst;!subst_Empty(scan);scan=subst_Next(scan)) { + varsort = sort_VarSort(Theory,subst_Dom(scan),Clause,l); + Pair = hash_Get(subst_Cod(scan)); + if ((Cond = sort_TheoryIsSubsortOfNoResidues(Theory,sort_PairSort(Pair),varsort)) == NULL) { + sort_DeleteOne(varsort); + list_Delete(NewClauses); + subst_Free(subst); + return FALSE; + } else { + NewClauses = list_Nconc(NewClauses, + list_Copy(sort_ConditionClauses(sort_PairCondition(Pair)))); + NewClauses = list_Nconc(NewClauses,sort_ConditionClauses(Cond)); + sort_ConditionPutClauses(Cond,list_Nil()); + sort_ConditionDelete(Cond); + } + + sort_DeleteOne(varsort); + } + + subst_Free(subst); + *Clauses = list_Nconc(NewClauses,*Clauses); + return TRUE; +} + + +static SOJU sort_ComputeSortInternNoResidues(SORTTHEORY Theory, TERM Term, + CLAUSE Clause, int i, + FLAGSTORE Flags, + PRECEDENCE Precedence) +/********************************************************* + INPUT: A Term, a sort theory representing a set of + clauses, a clause wrt that variable sorts are + computed, where the literal <i> is discarded, + a flag store and a precedence. + The sorts of 'Term's args have to be known. + RETURNS: The sort of 'Term' wrt. the sort theory of the + clause set. Be careful, the Sort-entries of + 'Term' and its subterms are changed. +*******************************************************/ +{ + SORT Sort; + LIST HelpList, Scan, Clauses; + TERM QueryTerm; + + Sort = sort_TopSort(); + Clauses = list_Nil(); + + if (term_IsVariable(Term)) + Sort = sort_VarSort(Theory,term_TopSymbol(Term),Clause,i); + else { + HelpList = st_GetGen(cont_LeftContext(), sort_TheoryIndex(Theory), Term); + for (Scan=HelpList;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + SYMBOL Top; + LITERAL ActLit; + TERM Atom; + CLAUSE ActClause; + + QueryTerm = (TERM)list_First(Scan); + + if (!term_IsVariable(QueryTerm)) { /* Currently also subort declarations are in the index ...*/ + Atom = (TERM)list_First(term_SupertermList(QueryTerm)); + Top = term_TopSymbol(Atom); + ActLit = (LITERAL)list_First(term_SupertermList(Atom)); + ActClause = clause_LiteralOwningClause(ActLit); + if (clause_IsSortTheoryClause(ActClause, Flags, Precedence) && + sort_MatchNoResidues(Theory,QueryTerm,Term, ActClause,&Clauses) && + !sort_ContainsSymbol(Sort,Top)) { + Sort = sort_Intersect(Sort,sort_TheorySortOfSymbol(Theory,Top)); + Clauses = list_Cons(ActClause,Clauses); + } + } + } + list_Delete(HelpList); + } + return (sort_PairCreate(Sort,sort_ConditionCreateNoResidues(Clauses))); +} + + +SOJU sort_ComputeSortNoResidues(SORTTHEORY Theory, TERM Term, CLAUSE Clause, + int i, FLAGSTORE Flags, PRECEDENCE Precedence) +/********************************************************* + INPUT: A Term and an Index representing a set of + clauses, a clause to access + variable-sort-information where the literal <i> + is discarded, a flag store and a precedence. + RETURNS: The sort of 'Term' wrt. the sort theory of the + clause set and the clauses used for this + computation. + Be careful, the Sort-entries of + 'Term' and its subterms are changed, if they + already existed. +*******************************************************/ +{ + int SubtermStack; + SOJU SortPair; + + SortPair = (SOJU)NULL; + SubtermStack = stack_Bottom(); + sharing_PushOnStack(Term); + + + while (!stack_Empty(SubtermStack)){ + Term = stack_PopResult(); + + if (!(SortPair = (SOJU)hash_Get(Term))) { + SortPair = sort_ComputeSortInternNoResidues(Theory,Term,Clause,i, + Flags, Precedence); + /*fputs("\n Computed:",stdout);term_Print(Term); + putchar(':');sort_PairPrint(SortPair);putchar('\n');*/ + hash_Put(Term,SortPair); + } + } + + SortPair = sort_PairCopy(SortPair); + hash_ResetWithValue((void (*)(POINTER)) sort_DeleteSortPair); + + return(SortPair); +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * Creating and Analyzing Sort Theories * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +static BOOL sort_SortTheoryIsTrivial(SORTTHEORY Theory, LIST Clauses) +/********************************************************* + INPUT: A sort theory and a list of clauses that generated the theory. + RETURNS: TRUE iff all considered base sorts are top. +*******************************************************/ +{ + LIST Sorts; + CLAUSE Clause; + int i,n; + CONDITION Cond; + + Sorts = list_Nil(); + + /* fputs("\n\nAnalyzing Theory:", stdout); */ + + while (!list_Empty(Clauses)) { + Clause = (CLAUSE)list_Car(Clauses); + n = clause_Length(Clause); + Clauses = list_Cdr(Clauses); + + /* fputs("\n\t", stdout);clause_Print(Clause); */ + + for (i=clause_FirstConstraintLitIndex(Clause); i<n; i++) + Sorts = list_Cons((POINTER)term_TopSymbol(clause_LiteralAtom( + clause_GetLiteral(Clause,i))), Sorts); + + Sorts = list_PointerDeleteDuplicates(Sorts); + } + + Clauses = Sorts; + while (!list_Empty(Clauses)) { + list_Rplaca(Clauses,sort_TheorySortOfSymbol(Theory,(SYMBOL)list_Car(Clauses))); + Clauses = list_Cdr(Clauses); + } + + n = list_Length(Sorts); + i = 0; + Clauses = Sorts; + + /* printf("\n\t There are %d different sorts.",n); */ + + while (!list_Empty(Clauses)) { + if ((Cond = sort_TheoryIsSubsortOfNoResidues(Theory,sort_TopSort(),list_Car(Clauses)))) { + sort_ConditionDelete(Cond); + i++; + } + sort_DeleteOne(list_Car(Clauses)); + Clauses = list_Cdr(Clauses); + } + + list_Delete(Sorts); + + return (i == n); /* All sorts are trivial */ +} + + +static LIST sort_ApproxPseudoLinear(LIST Constraint, TERM Head, SYMBOL Var) +/************************************************************** + INPUT: A list of constraint literals, the head literal term + and a variable maximal for all variables. + RETURNS: The new list of constraint literals. + EFFECT: The succedent literal is made pseudo-linear. + The function is DESTRUCTIVE. +***************************************************************/ +{ + TERM Atom; + LIST RenVars,Scan1,Scan2,Lits; + SYMBOL OldVar, NewVar; + + RenVars = term_RenamePseudoLinear(Head,Var); + Lits = list_Nil(); + + for (Scan1=RenVars;!list_Empty(Scan1);Scan1=list_Cdr(Scan1)) { + OldVar = (SYMBOL)list_PairFirst(list_Car(Scan1)); + NewVar = (SYMBOL)list_PairSecond(list_Car(Scan1)); + list_PairFree(list_Car(Scan1)); + for (Scan2=Constraint;!list_Empty(Scan2);Scan2=list_Cdr(Scan2)) { + Atom = (TERM)list_Car(Constraint); + if (symbol_Equal(term_TopSymbol(term_FirstArgument(Atom)),OldVar)) + Lits = list_Cons(term_Create(term_TopSymbol(Atom), + list_List(term_Create(NewVar,list_Nil()))), Lits); + } + } + list_Delete(RenVars); + + Lits = list_Nconc(Constraint,Lits); + + return Lits; +} + + +static LIST sort_ApproxHornClauses(CLAUSE Clause, FLAGSTORE Flags, + PRECEDENCE Precedence) +/************************************************************** + INPUT: A clause to make special horn clauses from, a flag + store and a precedence. + RETURNS: The list of clauses according to the rule + ClauseDeletion. + MEMORY: Allocates memory for the clauses and the list. +***************************************************************/ +{ + LIST Result, NewConstraint,NewSuccedent; + CLAUSE NewClause; + LITERAL LitK; + int i,length,j,lc,pli; + +#ifdef CHECK + if (!clause_IsClause(Clause, Flags, Precedence)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sort_ApproxHornClauses :"); + misc_ErrorReport(" Illegal input. Input not a clause.\n"); + misc_FinishErrorReport(); + } +#endif + + Result = list_Nil(); + + if (clause_HasOnlyVarsInConstraint(Clause, Flags, Precedence) && + clause_HasSortInSuccedent(Clause, Flags, Precedence)) { + length = clause_Length(Clause); + + for (i = clause_FirstSuccedentLitIndex(Clause); i < length; i++) { + LitK = clause_GetLiteral(Clause, i); + + if (symbol_Arity(term_TopSymbol(clause_LiteralSignedAtom(LitK))) == 1) { + pli = i; + NewSuccedent = list_List(term_Copy(clause_LiteralSignedAtom(LitK))); + NewConstraint = list_Nil(); + lc = clause_LastConstraintLitIndex(Clause); + + for (j = clause_FirstLitIndex(); j <= lc; j++) + if (clause_LitsHaveCommonVar(LitK, clause_GetLiteral(Clause, j))) + NewConstraint = list_Cons(term_Copy(clause_LiteralAtom( + clause_GetLiteral(Clause, j))), NewConstraint); + + if (!list_Empty(NewConstraint)) + NewConstraint = sort_ApproxPseudoLinear(NewConstraint, + list_Car(NewSuccedent), + clause_MaxVar(Clause)); + + NewClause = clause_Create(NewConstraint, list_Nil(), NewSuccedent, + Flags, Precedence); + clause_SetSplitLevel(NewClause, 0); + clause_SetFlag(NewClause,WORKEDOFF); + clause_SetFromClauseDeletion(NewClause); + clause_SetParentClauses(NewClause, list_List((POINTER)clause_Number(Clause))); + clause_AddParentLiteral(NewClause, pli); + + list_Delete(NewConstraint); + list_Delete(NewSuccedent); + Result = list_Cons(NewClause, Result); + } + } + } + return(Result); +} + +LIST sort_ApproxMaxDeclClauses(CLAUSE Clause, FLAGSTORE Flags, + PRECEDENCE Precedence) +/************************************************************** + INPUT: A declaration clause to make special horn clauses + from, a flag store and a precedence. + RETURNS: The list of Horn clauses that are pseudo-linear declaration + clauses generated from maximal declarations in <Clause> + MEMORY: Allocates memory for the clauses and the list. +***************************************************************/ +{ + LIST Result, NewConstraint,NewSuccedent; + CLAUSE NewClause; + LITERAL LitK; + int i,length,j,lc,pli; + +#ifdef CHECK + if (!clause_IsClause(Clause, Flags, Precedence) || + !clause_IsDeclarationClause(Clause)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In sort_ApproxMaxDeclClauses :"); + misc_ErrorReport(" Illegal input.\n"); + misc_FinishErrorReport(); + } +#endif + + Result = list_Nil(); + length = clause_Length(Clause); + + for (i = clause_FirstSuccedentLitIndex(Clause); i < length; i++) { + LitK = clause_GetLiteral(Clause, i); + + if (clause_LiteralIsMaximal(LitK) && + symbol_IsBaseSort(term_TopSymbol(clause_LiteralSignedAtom(LitK)))) { + pli = i; + NewSuccedent = list_List(term_Copy(clause_LiteralSignedAtom(LitK))); + NewConstraint = list_Nil(); + lc = clause_LastConstraintLitIndex(Clause); + + for (j = clause_FirstLitIndex(); j <= lc; j++) + if (clause_LitsHaveCommonVar(LitK, clause_GetLiteral(Clause, j))) + NewConstraint = list_Cons(term_Copy(clause_LiteralAtom(clause_GetLiteral(Clause, j))), + NewConstraint); + + if (!list_Empty(NewConstraint)) + NewConstraint = sort_ApproxPseudoLinear(NewConstraint, + list_Car(NewSuccedent), + clause_MaxVar(Clause)); + + NewClause = clause_Create(NewConstraint, list_Nil(), NewSuccedent, + Flags, Precedence); + clause_SetSplitLevel(NewClause, 0); + clause_SetFlag(NewClause,WORKEDOFF); + clause_SetFromClauseDeletion(NewClause); + clause_SetParentClauses(NewClause, list_List(Clause)); /* The clause itself is added! */ + clause_AddParentLiteral(NewClause, pli); + + list_Delete(NewConstraint); + list_Delete(NewSuccedent); + Result = list_Cons(NewClause, Result); + } + } + return(Result); +} + + +static LIST sort_ApproxClauses(LIST Clauses, FLAGSTORE Flags, + PRECEDENCE Precedence) +/************************************************************** + INPUT: A list of top level clauses, a flag store and a + precedence. + RETURNS: A list of approximated clauses from <Clauses> which must + be used for sort deletion. + EFFECT: None. +***************************************************************/ +{ + LIST Result,ApproxClauses; + CLAUSE ActClause; + + Result = list_Nil(); + + while (!list_Empty(Clauses)) { + ActClause = (CLAUSE)list_Car(Clauses); + ApproxClauses = sort_ApproxHornClauses(ActClause, Flags, Precedence); + Result = list_Nconc(ApproxClauses,Result); + Clauses = list_Cdr(Clauses); + } + + return Result; +} + +LIST sort_EliminateSubsumedClauses(LIST Clauses) +/********************************************************* + INPUT: A list of clauses. + RETURNS: <Clauses> without subsumed clauses. +*******************************************************/ +{ + LIST RedundantClauses,Iter,Scan; + BOOL Kept; + + RedundantClauses = list_Nil(); + for (Scan = Clauses; !list_Empty(Scan);Scan=list_Cdr(Scan)) { + Kept = TRUE; + for (Iter = Clauses;!list_Empty(Iter) && Kept; Iter = list_Cdr(Iter)) + if (list_Car(Iter) != list_Car(Scan) && + !list_PointerMember(RedundantClauses,list_Car(Iter)) && + subs_Subsumes(list_Car(Iter),list_Car(Scan),subs_NoException(),subs_NoException())) { + Kept = FALSE; + RedundantClauses = list_Cons(list_Car(Scan),RedundantClauses); + } + } + Clauses = list_NPointerDifference(Clauses,RedundantClauses); + clause_DeleteClauseList(RedundantClauses); + return Clauses; +} + + +SORTTHEORY sort_ApproxStaticSortTheory(LIST Clauses, FLAGSTORE Flags, + PRECEDENCE Precedence) +/********************************************************* + INPUT: A list of clauses, a flag store and a + precedence. + RETURNS: NULL if the approximated sort theory is trivial, + the approximated sort theory otherwise. +*******************************************************/ +{ + LIST Scan,ApproxClauses; + CLAUSE Clause; + SORTTHEORY Result; + + Result = sort_TheoryCreate(); + ApproxClauses = sort_ApproxClauses(Clauses, Flags, Precedence); + ApproxClauses = sort_EliminateSubsumedClauses(ApproxClauses); + + /*fputs("\n\n Approx Sort Theory:", stdout); + for (Scan = ApproxClauses; !list_Empty(Scan);Scan=list_Cdr(Scan)) { + fputs("\n\t",stdout); clause_Print(list_Car(Scan)); + }*/ + + for (Scan = ApproxClauses; !list_Empty(Scan);Scan=list_Cdr(Scan)) { + Clause = (CLAUSE)list_Car(Scan); + sort_TheoryInsertClause(Result,Clause,Clause, + clause_GetLiteral(Clause,clause_FirstSuccedentLitIndex(Clause))); + } + + if (sort_SortTheoryIsTrivial(Result,ApproxClauses)) { + sort_TheoryDelete(Result); + Result = (SORTTHEORY)NULL; + } + + + if (flag_GetFlagValue(Flags, flag_DOCSST)) { + fputs("\n\n Approx Sort Theory:", stdout); + if (Result) { + puts("\n"); + sort_TheoryPrint(Result); + } + else + fputs(" trivial.", stdout); + } + list_Delete(ApproxClauses); + + return Result; +} + + +SORTTHEORY sort_ApproxDynamicSortTheory(LIST Clauses) +/********************************************************* + INPUT: A list of clauses. + RETURNS: The approximated dynamic sort theory for <Clauses> + Only maximal declarations are considered. +*******************************************************/ +{ + return (SORTTHEORY)NULL; +} + +STR sort_AnalyzeSortStructure(LIST Clauses, FLAGSTORE Flags, + PRECEDENCE Precedence) +/********************************************************* + INPUT: A list of clauses, a flag store and a + precedence. + RETURNS: SORTEQMANY if all positive equations are many + sorted. + SORTEQDEC if all positive equations are sort + decreasing. + SORTEQNONE otherwise. + For the check, the static sort theory is + considered. +*******************************************************/ +{ + SORTTHEORY Theory; + LIST Scan; + CLAUSE Clause,Copy; + int i,l; + TERM Atom,Left,Right; + SOJU SojuLeft,SojuRight; + CONDITION Cond; + BOOL ManySorted, Decreasing; + + Theory = sort_TheoryCreate(); + ManySorted = TRUE; + Decreasing = TRUE; + + for (Scan=Clauses;!list_Empty(Scan);Scan=list_Cdr(Scan)) { + /* Extract static sort theory */ + Clause = (CLAUSE)list_Car(Scan); + if (clause_IsPotentialSortTheoryClause(Clause, Flags, Precedence)) { + Copy = clause_Copy(Clause); + symbol_AddProperty(term_TopSymbol(clause_GetLiteralTerm(Copy, + clause_FirstSuccedentLitIndex(Copy))), + DECLSORT); + list_Delete(clause_ParentClauses(Copy)); + clause_SetParentClauses(Copy,list_Nil()); + list_Delete(clause_ParentLiterals(Copy)); + clause_SetParentLiterals(Copy,list_Nil()); + clause_SetNumber(Copy,clause_Number(Clause)); + clause_SetSortConstraint(Copy,FALSE, Flags, Precedence); + sort_TheoryInsertClause(Theory,Clause,Copy, + clause_GetLiteral(Copy,clause_FirstSuccedentLitIndex(Copy))); + } + } + + /*putchar('\n'); + sort_TheoryPrint(Theory); + putchar('\n');*/ + + for (Scan=Clauses;!list_Empty(Scan) && Decreasing;Scan=list_Cdr(Scan)) { + Clause = (CLAUSE)list_Car(Scan); + l = clause_Length(Clause); + for (i=clause_FirstSuccedentLitIndex(Clause);i<l && Decreasing;i++) { + Atom = clause_GetLiteralTerm(Clause,i); + if (fol_IsEquality(Atom)) { + Left = term_FirstArgument(Atom); + Right = term_SecondArgument(Atom); + SojuLeft = sort_ComputeSortNoResidues(Theory, Left, Clause, i, + Flags, Precedence); + SojuRight = sort_ComputeSortNoResidues(Theory, Right,Clause, i, + Flags, Precedence); + if (sort_IsTopSort(sort_PairSort(SojuRight)) || sort_IsTopSort(sort_PairSort(SojuLeft))) { + /*fputs("\nNon decreasing equation ",stdout); term_PrintPrefix(Atom); + fputs(" in clause: ",stdout);clause_Print(Clause);putchar('\n');*/ + ManySorted = FALSE; + Decreasing = FALSE; + } + else { + if (!sort_Eq(sort_PairSort(SojuRight), sort_PairSort(SojuLeft))) { + ManySorted = FALSE; + Cond = sort_TheoryIsSubsortOfNoResidues(Theory, sort_PairSort(SojuRight), + sort_PairSort(SojuLeft)); + if (Cond && !clause_LiteralIsOrientedEquality(clause_GetLiteral(Clause,i))) { + sort_ConditionDelete(Cond); + Cond = sort_TheoryIsSubsortOfNoResidues(Theory, sort_PairSort(SojuLeft), + sort_PairSort(SojuRight)); + } + if (Cond) + sort_ConditionDelete(Cond); + else { + /*fputs("\nNon decreasing equation ",stdout); term_PrintPrefix(Atom); + fputs(" in clause: ",stdout);clause_Print(Clause);putchar('\n');*/ + Decreasing = FALSE; + } + } + } + sort_PairDelete(SojuLeft); + sort_PairDelete(SojuRight); + } + } + } + sort_TheoryDelete(Theory); + if (ManySorted) + return SORTEQMANY; + if (Decreasing) + return SORTEQDECR; + + return SORTEQNONE; +} + |