diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 12:34:43 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 12:34:43 +0000 |
commit | 6c196ec8a41d6ed506c133c8b33dba9684f9a7a6 (patch) | |
tree | 4e1422ea2a810520d0d9b0fbb78c0014ba9f8443 /test/spass/kbo.c | |
parent | 93d89c2b5e8497365be152fb53cb6cd4c5764d34 (diff) | |
download | compcert-6c196ec8a41d6ed506c133c8b33dba9684f9a7a6.tar.gz compcert-6c196ec8a41d6ed506c133c8b33dba9684f9a7a6.zip |
Updated raytracer test. Added SPASS test.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'test/spass/kbo.c')
-rw-r--r-- | test/spass/kbo.c | 593 |
1 files changed, 593 insertions, 0 deletions
diff --git a/test/spass/kbo.c b/test/spass/kbo.c new file mode 100644 index 00000000..c598cbe5 --- /dev/null +++ b/test/spass/kbo.c @@ -0,0 +1,593 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * EXTENDED KNUTH BENDIX ORDERING * */ +/* * * */ +/* * $Module: KBO * */ +/* * * */ +/* * 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 "kbo.h" +#include "order.h" + +const int kbo_MINWEIGHT = 1; + +/**************************************************************/ +/* Functions to implement an order on terms */ +/**************************************************************/ + +static int kbo_ContCompVarCondAndWeightIntern(CONTEXT Context, TERM Term, int Index) +/************************************************************** + INPUT: + EFFECT: +***************************************************************/ +{ + int Weight; + + Weight = 0; + Term = cont_Deref(&Context,Term); + + if (term_IsStandardVariable(Term)) { + ord_VARCOUNT[term_TopSymbol(Term)][Index]++; + Weight += kbo_MINWEIGHT; + } + else { + LIST Scan; + Weight += symbol_Weight(term_TopSymbol(Term)); + for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) + Weight += kbo_ContCompVarCondAndWeightIntern(Context, list_Car(Scan), Index); + } + + return Weight; +} + +static int kbo_ContCompVarCondAndWeight(CONTEXT Context1, TERM Term1, BOOL *VarCond1, + CONTEXT Context2, TERM Term2, BOOL *VarCond2) +/************************************************************** + INPUT: Two contexts, two terms and two pointers to booleans. + EFFECT: Sets the booleans with respect to the kbo variable condition. + Computes the kbo weight difference. + The terms are interpreted with respect to the bindings in the respective + contexts. +***************************************************************/ +{ + SYMBOL MaxVar1,MaxVar2; + int i,Weight; + + *VarCond1 = *VarCond2 = TRUE; + MaxVar1 = cont_TermMaxVar(Context1,Term1); + MaxVar2 = cont_TermMaxVar(Context2,Term2); + + if (MaxVar1 < MaxVar2) + MaxVar1 = MaxVar2; + + for (i = 0; i <= MaxVar1; i++) { + ord_VARCOUNT[i][0] = 0; + ord_VARCOUNT[i][1] = 0; + } + + Weight = kbo_ContCompVarCondAndWeightIntern(Context1, Term1, 0); + Weight = Weight - kbo_ContCompVarCondAndWeightIntern(Context2, Term2, 1); + + for (i = 0; i <= MaxVar1; i++) { + if (ord_VARCOUNT[i][0] < ord_VARCOUNT[i][1]) { + *VarCond1 = FALSE; + if (!*VarCond2) + return Weight; + } + else if (ord_VARCOUNT[i][0] > ord_VARCOUNT[i][1]) { + *VarCond2 = FALSE; + if (!*VarCond1) + return Weight; + } + } + return Weight; +} + + +static int kbo_CompVarCondAndWeight(TERM Term1, BOOL *VarCond1, TERM Term2, BOOL *VarCond2) +/************************************************************** + INPUT: Two terms and two pointers to booleans. + EFFECT: Sets the booleans with respect to the kbo variable condition. + Computes the kbo weight difference. +***************************************************************/ +{ + SYMBOL MaxVar1,MaxVar2; + TERM Term; + LIST Scan; + int i,Stack,Weight; + + *VarCond1 = *VarCond2 = TRUE; + MaxVar1 = term_MaxVar(Term1); + MaxVar2 = term_MaxVar(Term2); + Stack = stack_Bottom(); + Weight = 0; + + if (MaxVar1 < MaxVar2) + MaxVar1 = MaxVar2; + + for (i = 0; i <= MaxVar1; i++) { + ord_VARCOUNT[i][0] = 0; + ord_VARCOUNT[i][1] = 0; + } + + Term = Term1; + if (term_IsStandardVariable(Term)) { + ord_VARCOUNT[term_TopSymbol(Term)][0]++; + Weight += kbo_MINWEIGHT; + } + else { + Weight += symbol_Weight(term_TopSymbol(Term)); + if (term_IsComplex(Term)) + stack_Push(term_ArgumentList(Term)); + } + while (!stack_Empty(Stack)) { + Scan = stack_Top(); + Term = (TERM)list_Car(Scan); + stack_RplacTop(list_Cdr(Scan)); + if (term_IsStandardVariable(Term)) { + Weight += kbo_MINWEIGHT; + ord_VARCOUNT[term_TopSymbol(Term)][0]++; + } + else { + Weight += symbol_Weight(term_TopSymbol(Term)); + if (term_IsComplex(Term)) + stack_Push(term_ArgumentList(Term)); + } + while (!stack_Empty(Stack) && list_Empty(stack_Top())) + stack_Pop(); + } + + Term = Term2; + if (term_IsStandardVariable(Term)) { + Weight -= kbo_MINWEIGHT; + ord_VARCOUNT[term_TopSymbol(Term)][1]++; + } + else { + Weight -= symbol_Weight(term_TopSymbol(Term)); + if (term_IsComplex(Term)) + stack_Push(term_ArgumentList(Term)); + } + while (!stack_Empty(Stack)) { + Scan = stack_Top(); + Term = (TERM)list_Car(Scan); + stack_RplacTop(list_Cdr(Scan)); + if (term_IsStandardVariable(Term)) { + Weight -= kbo_MINWEIGHT; + ord_VARCOUNT[term_TopSymbol(Term)][1]++; + } + else { + Weight -= symbol_Weight(term_TopSymbol(Term)); + if (term_IsComplex(Term)) + stack_Push(term_ArgumentList(Term)); + } + while (!stack_Empty(Stack) && list_Empty(stack_Top())) + stack_Pop(); + } + + for (i = 0; i <= MaxVar1; i++) { + if (ord_VARCOUNT[i][0] < ord_VARCOUNT[i][1]) { + *VarCond1 = FALSE; + if (!*VarCond2) + return Weight; + } + if (ord_VARCOUNT[i][0] > ord_VARCOUNT[i][1]) { + *VarCond2 = FALSE; + if (!*VarCond1) + return Weight; + } + } + return Weight; +} + + +static ord_RESULT kbo_CompareStruc(TERM Term1, TERM Term2, int WeightDiff) +/************************************************************** + INPUT: Two terms where the kbo-variable condition for <Term1> and + <Term2> is satisfied and <WeightDiff> is the kbo weight difference + between <Term1> and <Term2> + RETURNS: ord_UNCOMPARABLE, if Term1 and Term2 are uncomparable + ord_EQUAL, if Term1 and Term2 are equal + ord_GREATER_THAN, if Term1 is greater than Term2 + CAUTION: The precedence from the order module is used to determine + the precedence of symbols! +***************************************************************/ +{ + LIST Scan1,Scan2; + SYMBOL Top1,Top2; + + Top1 = term_TopSymbol(Term1); + Top2 = term_TopSymbol(Term2); + + if (WeightDiff > 0) + return ord_GREATER_THAN; + else + if (WeightDiff == 0) { + if (symbol_IsStandardVariable(Top1)) { + if (symbol_IsStandardVariable(Top2)) + return ord_EQUAL; + else + return ord_UNCOMPARABLE; + } + else + if (symbol_IsStandardVariable(Top2) || + symbol_PrecedenceGreater(ord_PRECEDENCE, Top1, Top2)) + return ord_GREATER_THAN; + else + if (Top1 == Top2) { + int RecWeightDiff; + BOOL T1VarCond, T2VarCond; + TERM RecTerm1,RecTerm2; + Scan1 = term_ArgumentList(Term1); + Scan2 = term_ArgumentList(Term2); + if (symbol_HasProperty(Top1,ORDRIGHT)) { + int i; + for (i = symbol_Arity(Top1); + i > 0 && term_Equal(list_NthElement(Scan1,i),list_NthElement(Scan2,i)); + i--); + if (i > 0) { + RecTerm1 = (TERM)list_NthElement(Scan1,i); + RecTerm2 = (TERM)list_NthElement(Scan2,i); + } + else + return ord_EQUAL; + } + else { + while (!list_Empty(Scan1) && term_Equal(list_Car(Scan1),list_Car(Scan2))) { + Scan1 = list_Cdr(Scan1); + Scan2 = list_Cdr(Scan2); + } + if (list_Empty(Scan1)) /* Implies that list_Empty(Scan2) */ + return ord_EQUAL; + else { + RecTerm1 = (TERM)list_Car(Scan1); + RecTerm2 = (TERM)list_Car(Scan2); + } + } + RecWeightDiff = kbo_CompVarCondAndWeight(RecTerm1,&T1VarCond,RecTerm2,&T2VarCond); + if (RecWeightDiff >= 0 && T1VarCond) + return kbo_CompareStruc(RecTerm1, RecTerm2, RecWeightDiff); + else + return ord_UNCOMPARABLE; + } + else + return ord_UNCOMPARABLE; + } + else + return ord_UNCOMPARABLE; + + return ord_UNCOMPARABLE; +} + + +ord_RESULT kbo_Compare(TERM Term1, TERM Term2) +/************************************************************** + INPUT: Two terms. + RETURNS: ord_UNCOMPARABLE, if Term1 and Term2 are uncomparable because of + different variables, + ord_EQUAL, if Term1 and Term2 are comparable and have the + same weight, + ord_GREATER_THAN, if Term1 is greater than Term2 wrt the kbo with + the actual precedence and the given symbol weights, + ord_SMALLER_THAN, else. + CAUTION: The precedence from the order module is used to determine + the precedence of symbols! +***************************************************************/ +{ + int WeightDiff; + BOOL T1VarCond, T2VarCond; + ord_RESULT Result; + +#ifdef CHECK + if (!term_IsTerm(Term1) || !term_IsTerm(Term2)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In kbo_Compare:"); + misc_ErrorReport("\n Illegal input."); + misc_FinishErrorReport(); + } +#endif + + + WeightDiff = kbo_CompVarCondAndWeight(Term1,&T1VarCond,Term2,&T2VarCond); + + if (T1VarCond && !T2VarCond) + return kbo_CompareStruc(Term1,Term2,WeightDiff); + + if (!T1VarCond && T2VarCond) + return ord_Not(kbo_CompareStruc(Term2,Term1,-WeightDiff)); + + if (T1VarCond && T2VarCond) { + Result = kbo_CompareStruc(Term1,Term2,WeightDiff); + if (Result == ord_UNCOMPARABLE) + return ord_Not(kbo_CompareStruc(Term2,Term1,-WeightDiff)); + else + return Result; + } + + return ord_UNCOMPARABLE; +} + +static ord_RESULT kbo_ContCompareStruc(CONTEXT Context1, TERM Term1, + CONTEXT Context2, TERM Term2, + int WeightDiff) +/************************************************************** + INPUT: Two contexts and two terms where the kbo-variable condition + for <Term1> and <Term2> is satisfied and <WeightDiff> is the + kbo weight difference between <Term1> and <Term2>. + RETURNS: ord_UNCOMPARABLE, if Term1 and Term2 are uncomparable + ord_EQUAL, if Term1 and Term2 are equal + ord_GREATER_THAN, if Term1 is greater than Term2 + The Terms are interpreted with respect to the contexts. + CAUTION: The precedence from the order module is used to determine + the precedence of symbols! +***************************************************************/ +{ + LIST Scan1,Scan2; + SYMBOL Top1,Top2; + + Term1 = cont_Deref(&Context1,Term1); + Term2 = cont_Deref(&Context2,Term2); + Top1 = term_TopSymbol(Term1); + Top2 = term_TopSymbol(Term2); + + if (WeightDiff > 0) + return ord_GREATER_THAN; + else + if (WeightDiff == 0) { + if (symbol_IsStandardVariable(Top1)) { + if (symbol_IsStandardVariable(Top2)) + return ord_EQUAL; + else + return ord_UNCOMPARABLE; + } + else + if (symbol_IsStandardVariable(Top2) || + symbol_PrecedenceGreater(ord_PRECEDENCE, Top1,Top2)) + return ord_GREATER_THAN; + else + if (Top1 == Top2) { + int RecWeightDiff; + BOOL T1VarCond, T2VarCond; + TERM RecTerm1,RecTerm2; + Scan1 = term_ArgumentList(Term1); + Scan2 = term_ArgumentList(Term2); + if (symbol_HasProperty(Top1,ORDRIGHT)) { + int i; + for (i = symbol_Arity(Top1); + i > 0 && cont_TermEqual(Context1,list_NthElement(Scan1,i), + Context2,list_NthElement(Scan2,i)); + i--); + if (i > 0) { + RecTerm1 = cont_Deref(&Context1,list_NthElement(Scan1,i)); + RecTerm2 = cont_Deref(&Context2,list_NthElement(Scan2,i)); + } + else + return ord_EQUAL; + } + else { + while (!list_Empty(Scan1) && cont_TermEqual(Context1,list_Car(Scan1),Context2,list_Car(Scan2))) { + Scan1 = list_Cdr(Scan1); + Scan2 = list_Cdr(Scan2); + } + if (list_Empty(Scan1)) /* Implies that list_Empty(Scan2) */ + return ord_EQUAL; + else { + RecTerm1 = cont_Deref(&Context1,list_Car(Scan1)); + RecTerm2 = cont_Deref(&Context2,list_Car(Scan2)); + } + } + RecWeightDiff = kbo_ContCompVarCondAndWeight(Context1,RecTerm1,&T1VarCond, + Context2,RecTerm2,&T2VarCond); + if (RecWeightDiff >= 0 && T1VarCond) + return kbo_ContCompareStruc(Context1, RecTerm1, Context2, RecTerm2, RecWeightDiff); + else + return ord_UNCOMPARABLE; + } + else + return ord_UNCOMPARABLE; + } + else + return ord_UNCOMPARABLE; + + return ord_UNCOMPARABLE; +} + + +ord_RESULT kbo_ContCompare(CONTEXT Context1, TERM Term1, CONTEXT Context2, TERM Term2) +/************************************************************** + INPUT: Two contexts and two terms. + RETURNS: ord_UNCOMPARABLE, if Term1 and Term2 are uncomparable because of + different variables, + ord_EQUAL, if Term1 and Term2 are comparable and have the + same weight, + ord_GREATER_THAN, if Term1 is greater than Term2 wrt the kbo with + the actual precedence kbo_Prec and the given + symbol_Weights, + ord_SMALLER_THAN, else. + The Terms are interpreted with respect to the contexts. + CAUTION: The precedence from the order module is used to determine + the precedence of symbols! +***************************************************************/ +{ + int WeightDiff; + BOOL T1VarCond, T2VarCond; + ord_RESULT Result; + +#ifdef CHECK + if (!term_IsTerm(Term1) || !term_IsTerm(Term2)) { + misc_StartErrorReport(); + misc_ErrorReport("\n In kbo_Compare:"); + misc_ErrorReport("\n Illegal input."); + misc_FinishErrorReport(); + } +#endif + + + WeightDiff = kbo_ContCompVarCondAndWeight(Context1, Term1, &T1VarCond, Context2, Term2, &T2VarCond); + + if (T1VarCond && !T2VarCond) + return kbo_ContCompareStruc(Context1,Term1,Context2,Term2,WeightDiff); + + if (!T1VarCond && T2VarCond) + return ord_Not(kbo_ContCompareStruc(Context2,Term2,Context1,Term1,-WeightDiff)); + + if (T1VarCond && T2VarCond) { + Result = kbo_ContCompareStruc(Context1,Term1,Context2,Term2,WeightDiff); + if (Result == ord_UNCOMPARABLE) + return ord_Not(kbo_ContCompareStruc(Context2,Term2,Context1,Term1,-WeightDiff)); + else + return Result; + } + + return ord_UNCOMPARABLE; +} + +static BOOL kbo_ContGreaterCompareStruc(CONTEXT Context1, TERM Term1, + CONTEXT Context2, TERM Term2) +/************************************************************** + INPUT: Two contexts and two terms where the kbo-variable condition + for <Term1> and <Term2> is satisfied as well as the + weight difference between the terms is zero. + RETURNS: TRUE if Term1 is greater than Term2. + The Terms are interpreted with respect to the contexts. + CAUTION: The precedence from the order module is used to determine + the precedence of symbols! +***************************************************************/ +{ + LIST Scan1,Scan2; + SYMBOL Top1,Top2; + + Term1 = cont_Deref(&Context1,Term1); + Term2 = cont_Deref(&Context2,Term2); + Top1 = term_TopSymbol(Term1); + Top2 = term_TopSymbol(Term2); + + if (symbol_IsStandardVariable(Top1)) { + if (symbol_IsStandardVariable(Top2)) + return FALSE; + else + return FALSE; + } + else + if (symbol_IsStandardVariable(Top2) || + symbol_PrecedenceGreater(ord_PRECEDENCE, Top1, Top2)) + return TRUE; + else + if (Top1 == Top2) { + int RecWeightDiff; + BOOL T1VarCond, T2VarCond; + TERM RecTerm1,RecTerm2; + Scan1 = term_ArgumentList(Term1); + Scan2 = term_ArgumentList(Term2); + if (symbol_HasProperty(Top1,ORDRIGHT)) { + int i; + for (i = symbol_Arity(Top1); + i > 0 && cont_TermEqual(Context1,list_NthElement(Scan1,i), + Context2,list_NthElement(Scan2,i)); + i--); + if (i > 0) { + RecTerm1 = cont_Deref(&Context1,list_NthElement(Scan1,i)); + RecTerm2 = cont_Deref(&Context2,list_NthElement(Scan2,i)); + } + else + return FALSE; + } + else { + while (!list_Empty(Scan1) && cont_TermEqual(Context1,list_Car(Scan1),Context2,list_Car(Scan2))) { + Scan1 = list_Cdr(Scan1); + Scan2 = list_Cdr(Scan2); + } + if (list_Empty(Scan1)) /* Implies that list_Empty(Scan2) */ + return FALSE; + else { + RecTerm1 = cont_Deref(&Context1,list_Car(Scan1)); + RecTerm2 = cont_Deref(&Context2,list_Car(Scan2)); + } + } + RecWeightDiff = kbo_ContCompVarCondAndWeight(Context1,RecTerm1,&T1VarCond, + Context2,RecTerm2,&T2VarCond); + + if (T1VarCond) { + if (RecWeightDiff > 0) + return TRUE; + else + if (RecWeightDiff == 0) + return kbo_ContGreaterCompareStruc(Context1, RecTerm1, Context2, RecTerm2); + } + } + + return FALSE; +} + + +BOOL kbo_ContGreater(CONTEXT Context1, TERM Term1, CONTEXT Context2, TERM Term2) +/************************************************************** + INPUT: Two contexts and two terms. + RETURNS: TRUE, if Term1 is greater than Term2 wrt the kbo with + the actual precedence kbo_Prec and the given symbol_Weights + CAUTION: The precedence from the order module is used to determine + the precedence of symbols! +***************************************************************/ +{ + int WeightDiff; + BOOL T1VarCond, T2VarCond; + +#ifdef CHECK + if ((!term_IsTerm(Term1)) || (!term_IsTerm(Term2)) ) { + misc_StartErrorReport(); + misc_ErrorReport("\n In kbo_ContGreater:"); + misc_ErrorReport("\n Illegal input."); + misc_FinishErrorReport(); + } +#endif + + + WeightDiff = kbo_ContCompVarCondAndWeight(Context1, Term1, &T1VarCond, Context2, Term2, &T2VarCond); + + if (T1VarCond) { + if (WeightDiff > 0) + return TRUE; + else + if (WeightDiff == 0) + return kbo_ContGreaterCompareStruc(Context1,Term1,Context2,Term2); + } + return FALSE; +} |