From 6c196ec8a41d6ed506c133c8b33dba9684f9a7a6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 12:34:43 +0000 Subject: Updated raytracer test. Added SPASS test. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- test/spass/rpos.c | 521 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 521 insertions(+) create mode 100644 test/spass/rpos.c (limited to 'test/spass/rpos.c') diff --git a/test/spass/rpos.c b/test/spass/rpos.c new file mode 100644 index 00000000..edd1b8b7 --- /dev/null +++ b/test/spass/rpos.c @@ -0,0 +1,521 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * RECURSIVE PATH ORDERING WITH STATUS * */ +/* * * */ +/* * $Module: RPOS * */ +/* * * */ +/* * 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: 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 "rpos.h" + + +/**************************************************************/ +/* Top Down Version */ +/**************************************************************/ + +static LIST rpos_MultisetDifference(TERM T1, TERM T2) +/************************************************************** + INPUT: Two terms. + RETURNS: The multiset difference between the arguments + of both terms with respect to rpos_Equal. +***************************************************************/ +{ + LIST result; + + result = list_Copy(term_ArgumentList(T1)); + result = list_NMultisetDifference(result, term_ArgumentList(T2), + (BOOL (*)(POINTER,POINTER)) rpos_Equal); + return result; +} + + +static ord_RESULT rpos_MulGreaterEqual(TERM T1, TERM T2) +/************************************************************** + INPUT: Two terms with equal top symbols and multiset status. + RETURNS: ord_GREATER_THAN if is greater than , + ord_EQUAL if both terms are equal and + ord_UNCOMPARABLE otherwise. +***************************************************************/ +{ + LIST l1, l2; + + l1 = rpos_MultisetDifference(T1, T2); + if (list_Empty(l1)) + /* If |M| = |N| and M-N = {} then N-M = {} */ + return ord_Equal(); /* Terms are equal */ + else { + LIST scan; + BOOL greater; + + l2 = rpos_MultisetDifference(T2, T1); + + for (greater = TRUE; !list_Empty(l2) && greater; l2 = list_Pop(l2)) { + for (scan = l1, greater = FALSE; !list_Empty(scan) && !greater; scan = list_Cdr(scan)) + greater = rpos_Greater(list_Car(scan), list_Car(l2)); + } + list_Delete(l1); /* l2 was freed in the outer for loop */ + if (greater) + return ord_GreaterThan(); + else + return ord_Uncomparable(); + } +} + +static ord_RESULT rpos_LexGreaterEqual(TERM T1, TERM T2) +/************************************************************** + INPUT: Two terms with equal top symbols and lexicographic status. + RETURNS: ord_GREATER_THAN if is greater than , + ord_EQUAL if both terms are equal and + ord_UNCOMPARABLE otherwise. +***************************************************************/ +{ + ord_RESULT result; + LIST l1, l2, scan1, scan2; + + if (symbol_HasProperty(term_TopSymbol(T1), ORDRIGHT)) { + l1 = list_Reverse(term_ArgumentList(T1)); /* Create new lists */ + l2 = list_Reverse(term_ArgumentList(T2)); + } else { + l1 = term_ArgumentList(T1); + l2 = term_ArgumentList(T2); + } + /* First ignore equal arguments */ + result = ord_Equal(); + for (scan1 = l1, scan2 = l2; !list_Empty(scan1); + scan1 = list_Cdr(scan1), scan2 = list_Cdr(scan2)) { + result = rpos_GreaterEqual(list_Car(scan1), list_Car(scan2)); + if (!ord_IsEqual(result)) + break; + } + + if (ord_IsEqual(result)) /* All arguments are equal, so the terms */ + /* empty */; /* are equal with respect to RPOS */ + else if (ord_IsGreaterThan(result)) { + /* Check if T1 > each remaining argument of T2 */ + for (scan2 = list_Cdr(scan2); !list_Empty(scan2) && rpos_Greater(T1, list_Car(scan2)); + scan2 = list_Cdr(scan2)); /* Empty body */ + if (list_Empty(scan2)) + result = ord_GreaterThan(); + else + result = ord_Uncomparable(); + } + else { + /* Argument of T1 was not >= argument of T2. */ + + /* Try to find an argument of T1 that is >= T2 */ + for (scan1 = list_Cdr(scan1), result = ord_Uncomparable(); + !list_Empty(scan1) && !ord_IsGreaterThan(result); + scan1 = list_Cdr(scan1)) { + if (!ord_IsUncomparable(rpos_GreaterEqual(list_Car(scan1), T2))) + result = ord_GreaterThan(); + } + } + + if (symbol_HasProperty(term_TopSymbol(T1), ORDRIGHT)) { + list_Delete(l1); /* Delete the lists create above */ + list_Delete(l2); + } + return result; +} + + +BOOL rpos_Equal(TERM T1, TERM T2) +/************************************************************** + INPUT: Two terms. + RETURNS: TRUE, if is equal to and + FALSE otherwise. +***************************************************************/ +{ + LIST l1, l2; + + if (!term_EqualTopSymbols(T1, T2)) + return FALSE; + else if (!term_IsComplex(T1)) /* Equal variable or constant */ + return TRUE; + else { + if (symbol_HasProperty(term_TopSymbol(T1), ORDMUL)) { /* MUL case */ + l1 = rpos_MultisetDifference(T1, T2); + if (list_Empty(l1)) + return TRUE; + else { + list_Delete(l1); + return FALSE; + } + } else { /* LEX case */ + for (l1 = term_ArgumentList(T1), l2 = term_ArgumentList(T2); + !list_Empty(l1) && rpos_Equal(list_Car(l1), list_Car(l2)); + l1 = list_Cdr(l1), l2 = list_Cdr(l2)) + /* empty */; + return list_Empty(l1); /* All arguments were equal */ + } + } +} + + +ord_RESULT rpos_GreaterEqual(TERM T1, TERM T2) +/************************************************************** + INPUT: Two terms. + RETURNS: ord_GREATER_THAN if is greater than + ord_EQUAL if both terms are equal + ord_UNCOMPARABLE otherwise. + CAUTION: The precedence from the order module is used to determine + the precedence of symbols! +***************************************************************/ +{ + LIST scan; + + if (term_IsVariable(T1)) { + if (term_EqualTopSymbols(T1, T2)) + return ord_Equal(); /* T2 is the same variable */ + else + /* A variable can't be greater than another term */ + return ord_Uncomparable(); + } else if (term_IsVariable(T2)) { /* T1 isn't a variable */ + if (term_ContainsSymbol(T1, term_TopSymbol(T2))) + return ord_GreaterThan(); + else + return ord_Uncomparable(); + } else if (term_EqualTopSymbols(T1, T2)) { + if (symbol_HasProperty(term_TopSymbol(T1), ORDMUL)) + return rpos_MulGreaterEqual(T1, T2); + else + return rpos_LexGreaterEqual(T1, T2); + } else { + if (symbol_PrecedenceGreater(ord_PRECEDENCE, term_TopSymbol(T1), + term_TopSymbol(T2))) { + /* Different top symbols, symbol of T1 > symbol of T2. */ + /* Try if T1 > each argument of T2. */ + for (scan = term_ArgumentList(T2); !list_Empty(scan); scan = list_Cdr(scan)) + if (!rpos_Greater(T1, list_Car(scan))) + return ord_Uncomparable(); + return ord_GreaterThan(); + } else { + /* Try to find an argument of T1 that is >= T2 */ + for (scan = term_ArgumentList(T1); !list_Empty(scan); scan = list_Cdr(scan)) + if (!ord_IsUncomparable(rpos_GreaterEqual(list_Car(scan), T2))) + return ord_GreaterThan(); /* Argument of T1 >= T2 */ + return ord_Uncomparable(); + } + } +} + +ord_RESULT rpos_Compare(TERM T1, TERM T2) +/************************************************************** + INPUT: Two terms. + RETURNS: The relation between the two terms with respect to the + RPOS ordering: + ord_GREATER_THAN if is greater than , + ord_EQUAL if both terms are equal, + ord_SMALLER_THAN if is greater than and + ord_UNCOMPARABLE otherwise. + CAUTION: The precedence from the order module is used to determine + the precedence of symbols! +***************************************************************/ +{ + ord_RESULT result; + + result = rpos_GreaterEqual(T1, T2); + if (!ord_IsUncomparable(result)) + return result; + else if (rpos_Greater(T2, T1)) + return ord_SmallerThan(); + else + return ord_UNCOMPARABLE; +} + +/**************************************************************/ +/* Term comparison with respect to bindings */ +/**************************************************************/ + +static LIST rpos_ContMultisetDifference(CONTEXT C1, TERM T1, CONTEXT C2, TERM T2) +/************************************************************** + INPUT: Two contexts and two terms. + RETURNS: The multiset difference between the arguments + of both terms with respect to rpos_ContEqual. + EFFECT: Variable bindings are considered. +***************************************************************/ +{ + LIST result, scan1, scan2; + + /* Don't apply bindings at top level, since that happened */ + /* in rpos_ContGreaterEqual */ + + /* We can't use list_NMultisetDifference, since that function */ + /* expects an equality functions for terms that takes two terms */ + /* as arguments. We also need the two contexts resolve variable */ + /* bindings. */ + result = list_Copy(term_ArgumentList(T1)); + for (scan2 = term_ArgumentList(T2); !list_Empty(scan2); + scan2 = list_Cdr(scan2)) { + /* Delete at most one occurrence of the */ + /* current element of list2 from list1 */ + for (scan1 = result; !list_Empty(scan1); scan1 = list_Cdr(scan1)) { + if (list_Car(scan1) != NULL && + rpos_ContEqual(C1, list_Car(scan1), C2, list_Car(scan2))) { + /* arg of list1 wasn't deleted earlier and terms are equal */ + list_Rplaca(scan1, NULL); /* Mark argument of T1 as deleted */ + break; + } + } + } + return list_PointerDeleteElement(result, NULL); /* Delete all marked terms */ +} + + +static ord_RESULT rpos_ContMulGreaterEqual(CONTEXT C1, TERM T1, + CONTEXT C2, TERM T2) +/************************************************************** + INPUT: Two contexts and two terms with equal top symbols + and multiset status. + RETURNS: ord_GREATER_THAN if is greater than , + ord_EQUAL if both terms are equal and + ord_UNCOMPARABLE otherwise. + EFFECT: Variable bindings are considered. +***************************************************************/ +{ + LIST l1, l2; + + /* Don't apply bindings at top level, since that happened */ + /* in rpos_ContGreaterEqual. */ + + l1 = rpos_ContMultisetDifference(C1, T1, C2, T2); + if (list_Empty(l1)) + /* If |M| = |N| and M-N = {} then N-M = {} */ + return ord_Equal(); /* Terms are equal */ + else { + LIST scan; + BOOL greater; + + l2 = rpos_ContMultisetDifference(C2, T2, C1, T1); + + for (greater = TRUE; !list_Empty(l2) && greater; l2 = list_Pop(l2)) { + for (scan = l1, greater = FALSE; !list_Empty(scan) && !greater; + scan = list_Cdr(scan)) + greater = rpos_ContGreater(C1, list_Car(scan), C2, list_Car(l2)); + } + list_Delete(l1); /* l2 was freed in the outer for loop */ + if (greater) + return ord_GreaterThan(); + else + return ord_Uncomparable(); + } +} + +static ord_RESULT rpos_ContLexGreaterEqual(CONTEXT C1, TERM T1, + CONTEXT C2, TERM T2) +/************************************************************** + INPUT: Two contexts and two terms with equal top symbols + and lexicographic status. + RETURNS: ord_GREATER_THAN if is greater than , + ord_EQUAL if both terms are equal and + ord_UNCOMPARABLE otherwise. + EFFECT: Variable bindings are considered. +***************************************************************/ +{ + ord_RESULT result; + LIST l1, l2, scan1, scan2; + + /* Don't apply bindings at top level, since that happened */ + /* in rpos_ContGreaterEqual */ + + if (symbol_HasProperty(term_TopSymbol(T1), ORDRIGHT)) { + l1 = list_Reverse(term_ArgumentList(T1)); /* Create new lists */ + l2 = list_Reverse(term_ArgumentList(T2)); + } else { + l1 = term_ArgumentList(T1); + l2 = term_ArgumentList(T2); + } + /* First ignore equal arguments */ + result = ord_Equal(); + for (scan1 = l1, scan2 = l2; !list_Empty(scan1); + scan1 = list_Cdr(scan1), scan2 = list_Cdr(scan2)) { + result = rpos_ContGreaterEqual(C1, list_Car(scan1), C2, list_Car(scan2)); + if (!ord_IsEqual(result)) + break; + } + + if (ord_IsEqual(result)) /* All arguments are equal, so the terms */ + /* empty */; /* are equal with respect to RPOS */ + else if (ord_IsGreaterThan(result)) { + /* Check if T1 > each remaining argument of T2 */ + for (scan2 = list_Cdr(scan2); + !list_Empty(scan2) && rpos_ContGreater(C1, T1, C2, list_Car(scan2)); + scan2 = list_Cdr(scan2)); /* Empty body */ + if (list_Empty(scan2)) + result = ord_GreaterThan(); + else + result = ord_Uncomparable(); + } + else { + /* Argument of T1 was not >= argument of T2. */ + /* Try to find an argument of T1 that is >= T2 */ + for (scan1 = list_Cdr(scan1), result = ord_Uncomparable(); + !list_Empty(scan1) && !ord_IsGreaterThan(result); + scan1 = list_Cdr(scan1)) { + if (!ord_IsUncomparable(rpos_ContGreaterEqual(C1,list_Car(scan1),C2,T2))) + result = ord_GreaterThan(); + } + } + + if (symbol_HasProperty(term_TopSymbol(T1), ORDRIGHT)) { + list_Delete(l1); /* Delete the lists create above */ + list_Delete(l2); + } + return result; +} + + +BOOL rpos_ContEqual(CONTEXT C1, TERM T1, CONTEXT C2, TERM T2) +/************************************************************** + INPUT: Two contexts and two terms. + RETURNS: TRUE, if is equal to and + FALSE otherwise. + EFFECT: Variable bindings are considered. +***************************************************************/ +{ + LIST l1, l2; + + T1 = cont_Deref(&C1, T1); + T2 = cont_Deref(&C2, T2); + + if (!term_EqualTopSymbols(T1, T2)) + return FALSE; + else if (!term_IsComplex(T1)) + return TRUE; + else { + if (symbol_HasProperty(term_TopSymbol(T1), ORDMUL)) { + l1 = rpos_ContMultisetDifference(C1, T1, C2, T2); + if (list_Empty(l1)) + return TRUE; + else { + list_Delete(l1); + return FALSE; + } + } else { /* LEX case */ + for (l1 = term_ArgumentList(T1), l2 = term_ArgumentList(T2); + !list_Empty(l1) && rpos_ContEqual(C1,list_Car(l1),C2,list_Car(l2)); + l1 = list_Cdr(l1), l2 = list_Cdr(l2)); /* empty body */ + return list_Empty(l1); /* All arguments were equal */ + } + } +} + + +ord_RESULT rpos_ContGreaterEqual(CONTEXT C1, TERM T1, CONTEXT C2, TERM T2) +/************************************************************** + INPUT: Two contexts and two terms. + RETURNS: ord_GREATER_THAN if is greater than + ord_EQUAL if both terms are equal + ord_UNCOMPARABLE otherwise. + EFFECT: Variable bindings are considered. + CAUTION: The precedence from the order module is used to determine + the precedence of symbols! +***************************************************************/ +{ + LIST scan; + + T1 = cont_Deref(&C1, T1); + T2 = cont_Deref(&C2, T2); + + if (term_IsVariable(T1)) { + if (term_EqualTopSymbols(T1, T2)) + return ord_Equal(); /* T2 is the same variable */ + else + /* A variable can't be greater than another term */ + return ord_Uncomparable(); + } else if (term_IsVariable(T2)) { /* T1 isn't a variable */ + if (cont_TermContainsSymbol(C1, T1, term_TopSymbol(T2))) + return ord_GreaterThan(); + else + return ord_Uncomparable(); + } else if (term_EqualTopSymbols(T1, T2)) { + if (symbol_HasProperty(term_TopSymbol(T1), ORDMUL)) + return rpos_ContMulGreaterEqual(C1, T1, C2, T2); + else + return rpos_ContLexGreaterEqual(C1, T1, C2, T2); + } else { + if (symbol_PrecedenceGreater(ord_PRECEDENCE, term_TopSymbol(T1), + term_TopSymbol(T2))) { + /* Different top symbols, symbol of T1 > symbol of T2. */ + /* Try if T1 > each argument of T2. */ + for (scan = term_ArgumentList(T2); !list_Empty(scan); scan = list_Cdr(scan)) + if (!rpos_ContGreater(C1, T1, C2, list_Car(scan))) + return ord_Uncomparable(); + return ord_GreaterThan(); + } else { + /* Try to find an argument of T1 that is >= T2 */ + for (scan = term_ArgumentList(T1); !list_Empty(scan); scan = list_Cdr(scan)) + if (!ord_IsUncomparable(rpos_ContGreaterEqual(C1,list_Car(scan),C2,T2))) + return ord_GreaterThan(); /* Argument of T1 >= T2 */ + return ord_Uncomparable(); + } + } +} + +ord_RESULT rpos_ContCompare(CONTEXT C1, TERM T1, CONTEXT C2, TERM T2) +/************************************************************** + INPUT: Two contexts and two terms. + RETURNS: The relation between the two terms with respect to the + RPOS ordering: + ord_GREATER_THAN if is greater than , + ord_EQUAL if both terms are equal, + ord_SMALLER_THAN if is greater than and + ord_UNCOMPARABLE otherwise. + EFFECT: Variable bindings are considered. + CAUTION: The precedence from the order module is used to determine + the precedence of symbols! +***************************************************************/ +{ + ord_RESULT result; + + T1 = cont_Deref(&C1, T1); + T2 = cont_Deref(&C2, T2); + + result = rpos_ContGreaterEqual(C1, T1, C2, T2); + if (!ord_IsUncomparable(result)) + return result; + else if (rpos_ContGreater(C2, T2, C1, T1)) + return ord_SmallerThan(); + else + return ord_UNCOMPARABLE; +} + -- cgit