Updated raytracer test. Added SPASS test.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 385 insertions, 0 deletions

diff --git a/test/spass/rules-ur.c b/test/spass/rules-ur.c
new file mode 100644
index 0000000..bd07651
--- /dev/null
+++ b/test/spass/rules-ur.c
@@ -0,0 +1,385 @@
+/**************************************************************/
+/* ********************************************************** */
+/* *                                                        * */
+/* *                UR-RESOLUTION                           * */
+/* *                                                        * */
+/* *  $Module:   INFERENCE RULES                            * */
+/* *                                                        * */
+/* *  Copyright (C) 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$ */
+
+/**************************************************************/
+/* Includes                                                   */
+/**************************************************************/
+
+#include "rules-ur.h"
+#include "list.h"
+
+
+static LIST inf_GetURPartnerLits(TERM Atom, LITERAL Lit,
+				 BOOL Unit, SHARED_INDEX Index)
+/**************************************************************
+  INPUT:   An atom, a literal, a boolean flag and a SHARED_INDEX.
+  RETURNS: A list of literals with sign complementary to <Lit>
+           that are unifiable with <Atom>. If <Unit> is true,
+	   only literals from unit clauses are returned, if <Unit>
+	   is false, only literals from non-unit clauses are
+	   returned.
+  EFFECT:  <Atom> is a copy of <Lit>'s atom where some substitution
+           was applied and equality literals might have been swapped.
+	   <Lit> is just needed to check whether the unifiable
+	   literals are complementary.
+***************************************************************/
+{
+  LIST    Result, Unifiers, LitScan;
+  LITERAL PLit;
+  int     length;
+
+  Result   = list_Nil();
+  Unifiers = st_GetUnifier(cont_LeftContext(), sharing_Index(Index),
+			   cont_RightContext(), Atom);
+  for ( ; !list_Empty(Unifiers); Unifiers = list_Pop(Unifiers)) {
+    if (!term_IsVariable(list_Car(Unifiers))) {
+      for (LitScan = sharing_NAtomDataList(list_Car(Unifiers));
+	   !list_Empty(LitScan); LitScan = list_Cdr(LitScan)) {
+	PLit   = list_Car(LitScan);
+	length = clause_Length(clause_LiteralOwningClause(PLit));
+	if (clause_LiteralsAreComplementary(Lit, PLit) &&
+	    ((Unit && length==1) || (!Unit && length!=1)))
+	  /* The partner literals must have complementary sign and
+	     if <Unit> == TRUE they must be from unit clauses,
+	     if <Unit> == FALSE they must be from non-unit clauses. */
+	  Result = list_Cons(PLit, Result);
+      }
+    }
+  }
+  return Result;
+}
+
+
+static CLAUSE inf_CreateURUnitResolvent(CLAUSE Clause, int i, SUBST Subst,
+					LIST FoundMap, FLAGSTORE Flags,
+					PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A non-unit clause, a literal index from the clause,
+           a substitution, a list of pairs (l1, l2) of literals,
+	   where l1 is from the non-unit clause and l2 is from a
+	   unit clause, a flag store and a precedence.
+  RETURNS: The resolvent of this UR resolution inference. The
+           clause consists of the literal at index <i> in <Clause>
+	   after application of <Subst>.
+  EFFECT:  The flag store and the precedence are needed to create
+           the new clause.
+***************************************************************/
+{
+  CLAUSE  Result, PClause;
+  LITERAL Lit;
+  TERM    Atom;
+  LIST    Parents;
+  NAT     depth;
+
+  /* Create atom for resolvent */
+  Atom = subst_Apply(Subst, term_Copy(clause_GetLiteralAtom(Clause, i)));
+  /* Create clause */
+  Parents = list_List(Atom);
+  if (i <= clause_LastConstraintLitIndex(Clause))
+    Result = clause_Create(Parents, list_Nil(), list_Nil(), Flags, Precedence);
+  else if (i <= clause_LastAntecedentLitIndex(Clause))
+    Result = clause_Create(list_Nil(), Parents, list_Nil(), Flags, Precedence);
+  else
+    Result = clause_Create(list_Nil(), list_Nil(), Parents, Flags, Precedence);
+  list_Delete(Parents);
+
+  /* Get parent clauses and literals, calculate depth of resolvent */
+  Parents = list_List(Clause);
+  depth   = clause_Depth(Clause);
+  for ( ; !list_Empty(FoundMap); FoundMap = list_Cdr(FoundMap)) {
+    Lit     = list_PairSecond(list_Car(FoundMap)); /* Literal from unit */ 
+    PClause = clause_LiteralOwningClause(Lit);
+    Parents = list_Cons(PClause, Parents);
+    depth   = misc_Max(depth, clause_Depth(PClause));
+    clause_AddParentClause(Result, clause_Number(PClause));
+    clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit));
+
+    Lit     = list_PairFirst(list_Car(FoundMap)); /* Is from <Clause> */
+    clause_AddParentClause(Result, clause_Number(Clause));
+    clause_AddParentLiteral(Result, clause_LiteralGetIndex(Lit));
+  }
+  clause_SetFromURResolution(Result);
+  clause_SetDepth(Result, depth+1);
+  clause_SetSplitDataFromList(Result, Parents);
+  list_Delete(Parents);
+
+  return Result;
+}
+
+
+static LIST inf_SearchURResolvents(CLAUSE Clause, int i, LIST FoundMap,
+				   LIST RestLits, SUBST Subst,
+				   SYMBOL GlobalMaxVar, SHARED_INDEX Index,
+				   FLAGSTORE Flags, PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A non-unit clause, a literal index from <Clause>.
+           <FoundMap> is a list of pairs (l1,l2) of unifiable literals,
+	   where l1 is from <Clause> and l2 is from a unit clause.
+	   <RestLits> is a list of literals from <Clause> where
+	   we haven't found unifiable literals from unit clauses
+	   so far.
+	   <Subst> is the overall substitution for <Clause>
+	   (not for the unit-clauses!).
+	   <GlobalMaxVar> is the maximal variable encountered so far.
+	   <Index> is used to search unifiable literals.
+	   The flag store and the precedence are needed to create
+	   the new clauses.
+  RETURNS: A list of UR resolution resolvents.
+***************************************************************/
+{
+  if (list_Empty(RestLits)) {
+    /* Stop the recursion */
+    return list_List(inf_CreateURUnitResolvent(Clause, i, Subst, FoundMap,
+					       Flags, Precedence));
+  } else {
+    LITERAL Lit, PLit;
+    SYMBOL  NewMaxVar;
+    SUBST   NewSubst, RightSubst;
+    TERM    AtomCopy, PAtom;
+    LIST    Result, Partners;
+    BOOL    Swapped;
+
+    Result   = list_Nil();
+    Swapped  = FALSE;
+    /* Choose the unmatched literal with the most symbols */
+    RestLits = clause_MoveBestLiteralToFront(list_Copy(RestLits), Subst,
+					     GlobalMaxVar,
+					     clause_HyperLiteralIsBetter);
+    Lit      = list_Car(RestLits);
+    RestLits = list_Pop(RestLits);
+    AtomCopy = subst_Apply(Subst, term_Copy(clause_LiteralAtom(Lit)));
+
+    /* The following 'endless' loop runs twice for equality literals */
+    /* and only once for other literals.                             */
+    while (TRUE) {
+      Partners = inf_GetURPartnerLits(AtomCopy, Lit, TRUE, Index);
+      for ( ; !list_Empty(Partners); Partners = list_Pop(Partners)) {
+	PLit    = list_Car(Partners);
+
+	/* Rename the atom */
+	PAtom   = term_Copy(clause_LiteralAtom(PLit));
+	term_StartMaxRenaming(GlobalMaxVar);
+	term_Rename(PAtom);
+	/* Get the new global maximal variable */
+	NewMaxVar = term_MaxVar(PAtom);
+	if (symbol_GreaterVariable(GlobalMaxVar, NewMaxVar))
+	  NewMaxVar = GlobalMaxVar;
+	
+	/* Get the substitution */
+	cont_Check();
+	if (!unify_UnifyNoOC(cont_LeftContext(), AtomCopy,
+			     cont_RightContext(), PAtom)) {
+	  misc_StartErrorReport();
+	  misc_ErrorReport("\n In inf_SearchURResolvents: Unification failed.");
+	  misc_FinishErrorReport();
+	}
+	subst_ExtractUnifier(cont_LeftContext(), &NewSubst,
+			     cont_RightContext(), &RightSubst);
+	cont_Reset();
+	subst_Delete(RightSubst);  /* Forget substitution for unit clause */
+	term_Delete(PAtom);  /* Was just needed to get the substitution */
+
+	/* Build the composition of the substitutions */
+	RightSubst = NewSubst;
+	NewSubst = subst_Compose(NewSubst, subst_Copy(Subst));
+	subst_Delete(RightSubst);
+
+	FoundMap    = list_Cons(list_PairCreate(Lit, PLit), FoundMap);
+	
+	Result = list_Nconc(inf_SearchURResolvents(Clause,i,FoundMap,RestLits,
+						   NewSubst,NewMaxVar,Index,
+						   Flags, Precedence),
+			    Result);
+	
+	list_PairFree(list_Car(FoundMap));
+	FoundMap = list_Pop(FoundMap);
+	subst_Delete(NewSubst);
+      }
+      /* loop control */
+      if (!fol_IsEquality(AtomCopy) || Swapped)
+	break;
+      else {
+	term_EqualitySwap(AtomCopy);
+	Swapped = TRUE;
+      }
+    }
+    /* cleanup */
+    term_Delete(AtomCopy);
+    list_Delete(RestLits);
+    
+    return Result;
+  }
+}
+
+
+static LIST inf_NonUnitURResolution(CLAUSE Clause, int SpecialLitIndex,
+				    LIST FoundMap, SUBST Subst,
+				    SYMBOL GlobalMaxVar, SHARED_INDEX Index,
+				    FLAGSTORE Flags, PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A non-unit clause, a literal index from <Clause>.
+           <FoundMap> is a list of pairs (l1,l2) of unifiable literals,
+	   where l1 is from <Clause> and l2 is from a unit clause.
+	   At this point the list has at most one element.
+	   <Subst> is the substitution for <Clause>.
+	   <GlobalMaxVar> is the maximal variable encountered so far.
+	   <Index> is used to search unifiable literals.
+	   The flag store and the precedence are needed to create
+	   the new clauses.
+  RETURNS: The list of UR resolution resolvents.
+  EFFECT:  If inf_URResolution was called with a unit clause,
+           <SpecialLitIndex> is the index of a literal from a non-unit
+	   clause, that is unifiable with the unit clause's literal,
+	   otherwise it is set to -1.
+***************************************************************/
+{
+  LIST Result, RestLits;
+  int  i, last;
+
+  Result = list_Nil();
+  RestLits = clause_GetLiteralListExcept(Clause, SpecialLitIndex);
+  last = clause_LastLitIndex(Clause);
+  for (i = clause_FirstLitIndex(); i <= last; i++) {
+    /* <i> is the index of the literal that remains in the resolvent */
+    if (i != SpecialLitIndex) {
+      RestLits = list_PointerDeleteOneElement(RestLits,
+					      clause_GetLiteral(Clause,i));
+      
+      Result = list_Nconc(inf_SearchURResolvents(Clause, i, FoundMap, RestLits,
+						 Subst, GlobalMaxVar, Index,
+						 Flags, Precedence),
+			  Result);
+      
+      RestLits = list_Cons(clause_GetLiteral(Clause, i), RestLits);
+    }
+  }
+  list_Delete(RestLits);
+  return Result;
+}
+
+
+LIST inf_URResolution(CLAUSE Clause, SHARED_INDEX Index, FLAGSTORE Flags,
+		      PRECEDENCE Precedence)
+/**************************************************************
+  INPUT:   A clause, a shared index, a flag store and a precedence.
+  RETURNS: The list of UR resolution resolvents.
+  EFFECT:  The flag store and the precedence are needed to create
+           the resolvents.
+***************************************************************/
+{
+  LIST Result;
+
+  if (clause_Length(Clause) != 1) {
+    /* Clause isn't unit clause */
+    Result = inf_NonUnitURResolution(Clause, -1, list_Nil(), subst_Nil(),
+				     clause_MaxVar(Clause), Index, Flags,
+				     Precedence);
+  }
+  else {
+    /* Clause is unit clause, so search partner literals in non-unit clauses */
+    LITERAL Lit, PLit;
+    TERM    Atom;
+    LIST    Partners, FoundMap;
+    SYMBOL  MaxVar, PMaxVar;
+    SUBST   LeftSubst, RightSubst;
+    CLAUSE  PClause;
+    int     PLitInd;
+    BOOL    Swapped;
+
+    Result   = list_Nil();
+    Lit      = clause_GetLiteral(Clause, clause_FirstLitIndex());
+    Atom     = term_Copy(clause_LiteralAtom(Lit));
+    Swapped  = FALSE;
+
+    /* The following 'endless' loop runs twice for equality literals */
+    /* and only once for other literals.                             */
+    while (TRUE) {
+      /* Get complementary literals from non-unit clauses */
+      Partners = inf_GetURPartnerLits(Atom, Lit, FALSE, Index);
+      
+      for ( ; !list_Empty(Partners); Partners = list_Pop(Partners)) {
+	PLit     = list_Car(Partners);
+	PLitInd  = clause_LiteralGetIndex(PLit);
+	PClause  = clause_LiteralOwningClause(PLit); /* non-unit clause */
+	
+	PMaxVar   = clause_MaxVar(PClause);
+	term_StartMaxRenaming(PMaxVar);
+	term_Rename(Atom);              /* Rename atom from unit clause */
+	MaxVar = term_MaxVar(Atom); 
+	if (symbol_GreaterVariable(PMaxVar, MaxVar))
+	  MaxVar = PMaxVar;
+	
+	/* Get the substitution */
+	cont_Check();
+	unify_UnifyNoOC(cont_LeftContext(), clause_LiteralAtom(PLit),
+			cont_RightContext(), Atom);
+	subst_ExtractUnifier(cont_LeftContext(), &LeftSubst,
+			     cont_RightContext(), &RightSubst);
+	cont_Reset();
+	/* We don't need the substitution for the unit clause */
+	subst_Delete(RightSubst);
+	
+	FoundMap = list_List(list_PairCreate(PLit, Lit));
+	
+	Result = list_Nconc(inf_NonUnitURResolution(PClause, PLitInd, FoundMap,
+						    LeftSubst, MaxVar, Index,
+						    Flags, Precedence),
+			    Result);
+	
+	list_DeletePairList(FoundMap);
+	subst_Delete(LeftSubst);
+      }
+      /* loop control */
+      if (!fol_IsEquality(Atom) || Swapped)
+	break;
+      else {
+	term_EqualitySwap(Atom);
+	Swapped = TRUE;
+      }
+    }  /* end of endless loop */
+    term_Delete(Atom);
+  }
+  return Result;
+}