| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * 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$ * */ |
| /* $State$ * */ |
| /* $Date$ * */ |
| /* $Author$ * */ |
| /* * * */ |
| /* * 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; |
| } |
| |