| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * INTERFACE FOR ALL ORDERING IMPLEMENTATIONS * */ |
| /* * * */ |
| /* * $Module: ORDER * */ |
| /* * * */ |
| /* * Copyright (C) 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 "flags.h" |
| #include "order.h" |
| #include "kbo.h" |
| #include "rpos.h" |
| #include "symbol.h" |
| |
| NAT ord_VARCOUNT[symbol__MAXSTANDARDVAR][2]; |
| PRECEDENCE ord_PRECEDENCE; |
| |
| |
| static ord_RESULT ord_CheckDomPred(TERM T1, TERM T2, PRECEDENCE P) |
| /************************************************************** |
| INPUT: Two terms and a precedence. |
| RETURNS: An ordering result with respect to a possible domination |
| of leading predicates in <T1> or <T2>. |
| ***************************************************************/ |
| { |
| if ((term_IsAtom(T1) && symbol_HasProperty(term_TopSymbol(T1), DOMPRED)) || |
| (term_IsAtom(T2) && symbol_HasProperty(term_TopSymbol(T2), DOMPRED))) { |
| if (term_IsAtom(T1)) { |
| if (term_IsAtom(T2)) { |
| if (symbol_HasProperty(term_TopSymbol(T1), DOMPRED) && |
| (!symbol_HasProperty(term_TopSymbol(T2), DOMPRED) || |
| symbol_PrecedenceGreater(P,term_TopSymbol(T1),term_TopSymbol(T2)))) |
| return ord_GREATER_THAN; |
| if (!symbol_HasProperty(term_TopSymbol(T1), DOMPRED) || |
| term_TopSymbol(T1) != term_TopSymbol(T2)) |
| return ord_SMALLER_THAN; |
| /* If the top symbols are equal, do the normal comparison */ |
| } else { |
| /* T1 is an atom, T2 is not, so T1 is greater */ |
| return ord_GREATER_THAN; |
| } |
| } else { |
| /* T1 is not an atom, so T2 must be an atom */ |
| return ord_SMALLER_THAN; |
| } |
| } |
| return ord_UNCOMPARABLE; |
| } |
| |
| |
| ord_RESULT ord_Compare(TERM T1, TERM T2, FLAGSTORE FlagStore, PRECEDENCE P) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| ***************************************************************/ |
| { |
| ord_RESULT Aux; |
| |
| #ifdef CHECK |
| if (fol_IsEquality(T1) || fol_IsEquality(T2)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In ord_Compare:"); |
| misc_ErrorReport("\n Illegal input. One input term is an equality."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Aux = ord_CheckDomPred(T1, T2, P); |
| if (Aux != ord_UNCOMPARABLE) |
| return Aux; |
| else { |
| ord_PRECEDENCE = P; |
| switch(flag_GetFlagValue(FlagStore, flag_ORD)) { |
| case flag_ORDKBO: return kbo_Compare(T1, T2); break; |
| case flag_ORDRPOS: return rpos_Compare(T1, T2); break; |
| default: |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In ord_Compare:"); |
| misc_ErrorReport("\n Illegal ordering type."); |
| misc_FinishErrorReport(); |
| } |
| } |
| return ord_UNCOMPARABLE; |
| } |
| |
| |
| BOOL ord_CompareEqual(TERM T1, TERM T2, FLAGSTORE Flags) |
| /************************************************************** |
| INPUT: Two terms and a flag store. |
| RETURNS: TRUE, iff the two terms are equal with respect to the |
| reduction ordering selected by the 'flag_ORD' flag. |
| ***************************************************************/ |
| { |
| switch(flag_GetFlagValue(Flags, flag_ORD)) { |
| case flag_ORDKBO: return term_Equal(T1, T2); break; |
| case flag_ORDRPOS: return rpos_Equal(T1, T2); break; |
| default: |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In ord_Compare: Illegal ordering type."); |
| misc_FinishErrorReport(); |
| return FALSE; /* unreachable code ... */ |
| } |
| } |
| |
| ord_RESULT ord_ContCompare(CONTEXT C1, TERM T1, CONTEXT C2, TERM T2, |
| FLAGSTORE FlagStore, PRECEDENCE P) |
| { |
| ord_RESULT Aux; |
| |
| #ifdef CHECK |
| if (fol_IsEquality(T1) || fol_IsEquality(T2)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In ord_ContCompare:"); |
| misc_ErrorReport("\n Illegal input. One input term is an equality."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Aux = ord_CheckDomPred(T1, T2, P); |
| if (Aux != ord_UNCOMPARABLE) |
| return Aux; |
| else { |
| ord_PRECEDENCE = P; |
| switch(flag_GetFlagValue(FlagStore, flag_ORD)) { |
| case flag_ORDKBO: return kbo_ContCompare(C1, T1, C2, T2); break; |
| case flag_ORDRPOS: return rpos_ContCompare(C1, T1, C2, T2); break; |
| default: |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In ord_ContCompare:"); |
| misc_ErrorReport("\n Illegal ordering type."); |
| misc_FinishErrorReport(); |
| } |
| } |
| return ord_UNCOMPARABLE; |
| } |
| |
| |
| BOOL ord_ContGreater(CONTEXT C1, TERM T1, CONTEXT C2, TERM T2, |
| FLAGSTORE FlagStore, PRECEDENCE P) |
| { |
| ord_RESULT Aux; |
| |
| #ifdef CHECK |
| if (fol_IsEquality(T1) || fol_IsEquality(T2)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In ord_ContGreater:"); |
| misc_ErrorReport("\n Illegal input. One input term is an equality."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| Aux = ord_CheckDomPred(T1, T2, P); |
| if (Aux != ord_UNCOMPARABLE) |
| return (Aux == ord_GREATER_THAN); |
| else { |
| ord_PRECEDENCE = P; |
| switch(flag_GetFlagValue(FlagStore, flag_ORD)) { |
| case flag_ORDKBO: return kbo_ContGreater(C1, T1, C2, T2); break; |
| case flag_ORDRPOS: return rpos_ContGreater(C1, T1, C2, T2); break; |
| default: |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In ord_ContGreater:"); |
| misc_ErrorReport("\n Illegal ordering type."); |
| misc_FinishErrorReport(); |
| } |
| } |
| return FALSE; /* This line is never reached ... */ |
| } |
| |
| |
| ord_RESULT ord_Not(ord_RESULT Result) |
| /************************************************************** |
| INPUT: An ord_RESULT |
| RETURNS: The negation with respect to argument switching. |
| ***************************************************************/ |
| { |
| if (Result == ord_UNCOMPARABLE || Result == ord_EQUAL) |
| return Result; |
| |
| if (Result == ord_GREATER_THAN) |
| return ord_SMALLER_THAN; |
| |
| return ord_GREATER_THAN; |
| } |
| |
| |
| void ord_Print(ord_RESULT Result) |
| /************************************************************** |
| INPUT: An ord_Result. |
| RETURNS: None, prints the Result as a string to stdout. |
| ***************************************************************/ |
| { |
| switch(Result) { |
| case ord_UNCOMPARABLE: fputs(" uncomparable ",stdout); break; |
| case ord_EQUAL: fputs(" equal ",stdout); break; |
| case ord_GREATER_THAN: fputs(" greater than ",stdout); break; |
| case ord_SMALLER_THAN: fputs(" smaller than ",stdout); break; |
| default: fputs(" Nonsense! ",stdout); |
| } |
| } |
| |
| |
| ord_RESULT ord_LiteralCompare(TERM Lit1, BOOL Orient1, TERM Lit2, BOOL Orient2, |
| BOOL Check, FLAGSTORE FlagStore, |
| PRECEDENCE Precedence) |
| /********************************************************* |
| INPUT: Two term literals and two flags indicating whether these |
| two literals are oriented equalities. |
| Additionally a check flag that indicates whether |
| the orientation flags are sufficient or necessary and sufficient: |
| If Check=TRUE then if flag is FALSE it is interpreted that it is not |
| known whether the (possible) equation can be oriented oriented. |
| However, if flag is TRUE we assume that it is oriented. |
| A flag store. |
| A precedence. |
| RETURNS: The result if these literals are compared with |
| respect to the ordering. Dependent on their sign, the literals |
| are compared as multiset of their topsymbol terms, |
| where any literal is considered to be an equation |
| and non equational literals are considered to be |
| equations with the artificial, non-existent, minimal |
| constant tt. |
| EFFECT: The arguments of the literals are possibly, destructively flipped. |
| **********************************************************/ |
| { |
| ord_RESULT result,auxResult,AuxRl1r2,AuxRr1r2,AuxRr1l2,Comp1,Comp2; |
| BOOL pos1,pos2; |
| |
| pos1 = pos2 = TRUE; |
| Comp1 = Comp2 = result = ord_UNCOMPARABLE; |
| if (symbol_Equal(term_TopSymbol(Lit1),fol_Not())) { |
| Lit1 = term_FirstArgument(Lit1); |
| pos1 = FALSE; |
| } |
| if (symbol_Equal(term_TopSymbol(Lit2),fol_Not())) { |
| Lit2 = term_FirstArgument(Lit2); |
| pos2 = FALSE; |
| } |
| |
| if (fol_IsEquality(Lit1)) { /* Real equation */ |
| if (fol_IsEquality(Lit2)) { |
| TERM l1,r1,l2,r2,aux; |
| l1 = term_FirstArgument(Lit1); |
| r1 = term_SecondArgument(Lit1); |
| l2 = term_FirstArgument(Lit2); |
| r2 = term_SecondArgument(Lit2); |
| if (Orient1 || |
| (Check && |
| ((Comp1 = ord_Compare(l1,r1,FlagStore,Precedence)) == ord_GREATER_THAN || |
| Comp1 == ord_SMALLER_THAN))) { |
| if (Comp1 == ord_SMALLER_THAN) { |
| aux = l1; l1 = r1; r1 = aux; |
| } |
| if (Orient2 || |
| (Check && |
| ((Comp2 = ord_Compare(l2,r2,FlagStore,Precedence))==ord_GREATER_THAN || |
| Comp2 == ord_SMALLER_THAN))) { |
| /* Both equations are oriented */ |
| if (Comp2 == ord_SMALLER_THAN) { |
| aux = l2; l2 = r2; r2 = aux; |
| } |
| result = ord_Compare(l1,l2, FlagStore, Precedence); |
| if (result == ord_EQUAL) { |
| if (pos1) { |
| if (pos2) |
| return ord_Compare(r1,r2, FlagStore, Precedence); |
| else |
| return ord_SMALLER_THAN; |
| } |
| else |
| if (pos2) |
| return ord_GREATER_THAN; |
| else |
| return ord_Compare(r1,r2, FlagStore, Precedence); |
| } |
| return result; |
| } |
| else { /* Lit2 is not oriented equation */ |
| if (term_Equal(l1,l2)) { |
| result = ord_Compare(r1,r2, FlagStore, Precedence); |
| if (result == ord_EQUAL) { |
| if (pos1 && !pos2) |
| return ord_SMALLER_THAN; |
| else |
| if (!pos1 && pos2) |
| return ord_GREATER_THAN; |
| } |
| return result; |
| } |
| if (term_Equal(l1,r2)) { |
| result = ord_Compare(r1,l2, FlagStore, Precedence); |
| if (result == ord_EQUAL) { |
| if (pos1 && !pos2) |
| return ord_SMALLER_THAN; |
| else |
| if (!pos1 && pos2) |
| return ord_GREATER_THAN; |
| } |
| return result; |
| } |
| result = ord_Compare(l1,l2, FlagStore, Precedence); |
| AuxRl1r2 = ord_Compare(l1,r2, FlagStore, Precedence); |
| if (result == AuxRl1r2) |
| return result; |
| AuxRr1r2 = ord_Compare(r1,r2, FlagStore, Precedence); |
| if (result == AuxRr1r2) |
| return result; |
| if (AuxRl1r2 == AuxRr1r2 && AuxRl1r2 == ord_SMALLER_THAN) |
| return ord_SMALLER_THAN; |
| AuxRr1l2 = ord_Compare(r1,l2, FlagStore, Precedence); |
| if (result == AuxRr1l2 && result == ord_SMALLER_THAN) |
| return ord_SMALLER_THAN; |
| return ord_UNCOMPARABLE; |
| } |
| } |
| else /* Lit1 is unorientable equation */ |
| if (Orient2 || |
| (Check && |
| ((Comp2 = ord_Compare(term_FirstArgument(Lit2), |
| term_SecondArgument(Lit2), |
| FlagStore, Precedence) == ord_GREATER_THAN) || |
| Comp2 == ord_SMALLER_THAN))) { /* Lit2 is orientable equation */ |
| if (Comp2 == ord_SMALLER_THAN) { |
| aux = l2; l2 = r2; r2 = aux; |
| } |
| if (term_Equal(l1,l2)) { |
| result = ord_Compare(r1,r2, FlagStore, Precedence); |
| if (result == ord_EQUAL) { |
| if (pos1 && !pos2) |
| return ord_SMALLER_THAN; |
| else |
| if (!pos1 && pos2) |
| return ord_GREATER_THAN; |
| } |
| return result; |
| } |
| if (term_Equal(r1,l2)) { |
| result = ord_Compare(l1,r2, FlagStore, Precedence); |
| if (result == ord_EQUAL) { |
| if (pos1 && !pos2) |
| return ord_SMALLER_THAN; |
| else |
| if (!pos1 && pos2) |
| return ord_GREATER_THAN; |
| } |
| return result; |
| } |
| |
| result = ord_Compare(l1,l2, FlagStore, Precedence); |
| AuxRr1l2 = ord_Compare(r1,l2, FlagStore, Precedence); |
| if (result == AuxRr1l2) |
| return result; |
| AuxRr1r2 = ord_Compare(r1,r2, FlagStore, Precedence); |
| if (result == AuxRr1r2) |
| return result; |
| if (AuxRr1l2 == AuxRr1r2 && AuxRr1l2 == ord_GREATER_THAN) |
| return ord_GREATER_THAN; |
| AuxRl1r2 = ord_Compare(l1,r2, FlagStore, Precedence); |
| if (result == AuxRl1r2 && result == ord_GREATER_THAN) |
| return ord_GREATER_THAN; |
| return ord_UNCOMPARABLE; |
| } |
| else { /* Both literals are unorientable equations */ |
| if (term_Equal(l1,l2)) { |
| result = ord_Compare(r1,r2, FlagStore, Precedence); |
| if (result == ord_EQUAL) { |
| if (pos1 && !pos2) |
| return ord_SMALLER_THAN; |
| else if (!pos1 && pos2) |
| return ord_GREATER_THAN; |
| } |
| return result; |
| } |
| if (term_Equal(r1,l2)) { |
| result = ord_Compare(l1,r2, FlagStore, Precedence); |
| if (result == ord_EQUAL) { |
| if (pos1 && !pos2) |
| return ord_SMALLER_THAN; |
| else if (!pos1 && pos2) |
| return ord_GREATER_THAN; |
| } |
| return result; |
| } |
| if (term_Equal(l1,r2)) { |
| result = ord_Compare(r1,l2, FlagStore, Precedence); |
| if (result == ord_EQUAL) { |
| if (pos1 && !pos2) |
| return ord_SMALLER_THAN; |
| else if (!pos1 && pos2) |
| return ord_GREATER_THAN; |
| } |
| return result; |
| } |
| if (term_Equal(r1,r2)) { |
| result = ord_Compare(l1,l2, FlagStore, Precedence); |
| if (result == ord_EQUAL) { |
| if (pos1 && !pos2) |
| return ord_SMALLER_THAN; |
| else if (!pos1 && pos2) |
| return ord_GREATER_THAN; |
| } |
| return result; |
| } |
| result = ord_Compare(l1,l2, FlagStore, Precedence); |
| if (result == ord_UNCOMPARABLE) { |
| result = ord_Compare(l1,r2, FlagStore, Precedence); |
| if (result == ord_UNCOMPARABLE) { |
| if (ord_Compare(r1,l2, FlagStore, Precedence) == ord_GREATER_THAN && |
| ord_Compare(r1,r2, FlagStore, Precedence) == ord_GREATER_THAN) |
| return ord_GREATER_THAN; |
| return ord_UNCOMPARABLE; |
| } |
| if (result == ord_GREATER_THAN) { |
| if (ord_Compare(r1,l2, FlagStore, Precedence) == ord_GREATER_THAN) |
| return ord_GREATER_THAN; |
| return ord_UNCOMPARABLE; |
| } |
| if (result == ord_SMALLER_THAN) { |
| if (ord_Compare(r1,l2, FlagStore, Precedence) == ord_SMALLER_THAN || |
| ord_Compare(r1,r2, FlagStore, Precedence) == ord_SMALLER_THAN) |
| return ord_SMALLER_THAN; |
| return ord_UNCOMPARABLE; |
| } |
| } |
| if (result == ord_GREATER_THAN) { |
| if ((result = ord_Compare(l1,r2,FlagStore,Precedence)) == ord_GREATER_THAN || |
| (auxResult = ord_Compare(r1,r2,FlagStore,Precedence)) == ord_GREATER_THAN) |
| return ord_GREATER_THAN; |
| if (result == ord_UNCOMPARABLE || auxResult == ord_UNCOMPARABLE) |
| return ord_UNCOMPARABLE; |
| return ord_SMALLER_THAN; |
| } |
| if (result == ord_SMALLER_THAN) { |
| if ((result = ord_Compare(r1,l2,FlagStore,Precedence)) == ord_SMALLER_THAN || |
| (auxResult = ord_Compare(r1,r2,FlagStore,Precedence)) == ord_SMALLER_THAN) |
| return ord_SMALLER_THAN; |
| if (result == ord_UNCOMPARABLE || auxResult == ord_UNCOMPARABLE) |
| return ord_UNCOMPARABLE; |
| return ord_GREATER_THAN; |
| } |
| } |
| } |
| else {/* Second Atom is not an equation */ |
| /* They can't be equal ! */ |
| result = ord_Compare(term_FirstArgument(Lit1),Lit2,FlagStore,Precedence); |
| if (!Orient1 && result != ord_GREATER_THAN) { |
| auxResult = ord_Compare(term_SecondArgument(Lit1),Lit2,FlagStore,Precedence); |
| if (auxResult == ord_GREATER_THAN) |
| result = ord_GREATER_THAN; |
| else if (result != auxResult) |
| result = ord_UNCOMPARABLE; |
| } |
| } |
| } |
| else /* First Atom is not an equation */ |
| /* They can't be equal ! */ |
| if (fol_IsEquality(Lit2)) { |
| result = ord_Compare(Lit1,term_FirstArgument(Lit2), FlagStore, Precedence); |
| if (!Orient2 && result != ord_SMALLER_THAN) { |
| auxResult = ord_Compare(Lit1,term_SecondArgument(Lit2),FlagStore,Precedence); |
| if (auxResult == ord_SMALLER_THAN) |
| result = ord_SMALLER_THAN; |
| else if (result != auxResult) |
| result = ord_UNCOMPARABLE; |
| } |
| } else { /* None of the atoms is an equation */ |
| result = ord_Compare(Lit1,Lit2, FlagStore, Precedence); |
| if (result == ord_EQUAL) { |
| if (pos1 && !pos2) |
| result = ord_SMALLER_THAN; |
| else if (!pos1 && pos2) |
| result = ord_GREATER_THAN; |
| } |
| } |
| |
| return result; |
| } |
