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/rules-ur.c | 385 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 385 insertions(+) create mode 100644 test/spass/rules-ur.c (limited to 'test/spass/rules-ur.c') diff --git a/test/spass/rules-ur.c b/test/spass/rules-ur.c new file mode 100644 index 00000000..bd076517 --- /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 + that are unifiable with . If is true, + only literals from unit clauses are returned, if + is false, only literals from non-unit clauses are + returned. + EFFECT: is a copy of 's atom where some substitution + was applied and equality literals might have been swapped. + 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 == TRUE they must be from unit clauses, + if == 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 in + after application of . + 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_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 . + is a list of pairs (l1,l2) of unifiable literals, + where l1 is from and l2 is from a unit clause. + is a list of literals from where + we haven't found unifiable literals from unit clauses + so far. + is the overall substitution for + (not for the unit-clauses!). + is the maximal variable encountered so far. + 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 . + is a list of pairs (l1,l2) of unifiable literals, + where l1 is from and l2 is from a unit clause. + At this point the list has at most one element. + is the substitution for . + is the maximal variable encountered so far. + 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, + 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++) { + /* 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; +} -- cgit